Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add cram tests for YAML witnesses #1357

Merged
merged 18 commits into from
Apr 4, 2024
Merged
Show file tree
Hide file tree
Changes from 18 commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion goblint.opam
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
available: os-distribution != "alpine" & arch != "arm64"
pin-depends: [
# published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
[ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ]
[ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
# TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
]
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.locked
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ post-messages: [
pin-depends: [
[
"goblint-cil.2.0.3"
"git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64"
"git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f"
]
[
"ppx_deriving.5.2.1"
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.template
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
available: os-distribution != "alpine" & arch != "arm64"
pin-depends: [
# published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
[ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ]
[ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
# TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
]
Expand Down
1 change: 0 additions & 1 deletion src/witness/yamlWitness.ml
Original file line number Diff line number Diff line change
Expand Up @@ -387,7 +387,6 @@ struct
let query = Queries.Invariant Invariant.default_context in
begin match R.ask_local pre_lvar query with
| `Lifted c_inv ->
let loc = Node.location n in
(* Find unknowns for which the preceding start state satisfies the precondtion *)
let xs = find_matching_states lvar in

Expand Down
14 changes: 14 additions & 0 deletions src/witness/yamlWitnessType.ml
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,7 @@ struct
column: int;
function_: string;
}
[@@deriving ord]

let to_yaml {file_name; file_hash; line; column; function_} =
`O [
Expand Down Expand Up @@ -138,6 +139,7 @@ struct
type_: string;
format: string;
}
[@@deriving ord]

let to_yaml {string; type_; format} =
`O [
Expand All @@ -160,6 +162,7 @@ struct
location: Location.t;
loop_invariant: Invariant.t;
}
[@@deriving ord]

let entry_type = "loop_invariant"

Expand All @@ -182,6 +185,7 @@ struct
location: Location.t;
location_invariant: Invariant.t;
}
[@@deriving ord]

let entry_type = "location_invariant"

Expand All @@ -203,6 +207,7 @@ struct
type t = {
flow_insensitive_invariant: Invariant.t;
}
[@@deriving ord]

let entry_type = "flow_insensitive_invariant"

Expand All @@ -224,6 +229,7 @@ struct
loop_invariant: Invariant.t;
precondition: Invariant.t;
}
[@@deriving ord]

let entry_type = "precondition_loop_invariant"

Expand Down Expand Up @@ -251,6 +257,7 @@ struct
value: string;
format: string;
}
[@@deriving ord]

let invariant_type = "loop_invariant"

Expand Down Expand Up @@ -282,6 +289,7 @@ struct
type t =
| LocationInvariant of LocationInvariant.t
| LoopInvariant of LoopInvariant.t
[@@deriving ord]

let invariant_type = function
| LocationInvariant _ -> LocationInvariant.invariant_type
Expand Down Expand Up @@ -309,6 +317,7 @@ struct
type t = {
invariant_type: InvariantType.t;
}
[@@deriving ord]

let to_yaml {invariant_type} =
`O [
Expand All @@ -327,6 +336,7 @@ struct
type t = {
content: Invariant.t list;
}
[@@deriving ord]

let entry_type = "invariant_set"

Expand All @@ -346,6 +356,7 @@ struct
type_: string;
file_hash: string;
}
[@@deriving ord]

let to_yaml {uuid; type_; file_hash} =
`O [
Expand All @@ -369,6 +380,7 @@ struct
type_: string;
format: string;
}
[@@deriving ord]

let to_yaml {string; type_; format} =
`O [
Expand All @@ -391,6 +403,7 @@ struct
target: Target.t;
certification: Certification.t;
}
[@@deriving ord]

let entry_type = "loop_invariant_certificate"

Expand Down Expand Up @@ -424,6 +437,7 @@ struct
| LoopInvariantCertificate of LoopInvariantCertificate.t
| PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t
| InvariantSet of InvariantSet.t
[@@deriving ord]

let entry_type = function
| LocationInvariant _ -> LocationInvariant.entry_type
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
int main() {
int i = 0;
while (i < 10)
i++;
return 0;
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Suppress backtrace with code locations, especially for CI.
$ export OCAMLRUNPARAM=b=0

$ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' 11-unrolled-loop-invariant.c
[Error] YAML witnesses are incompatible with syntactic loop unrolling (https://github.com/goblint/analyzer/pull/1370).
Fatal error: exception Failure("Option error")
[2]

TODO: Fix loop unrolling with YAML witnesses: https://github.com/goblint/analyzer/pull/1370
5 changes: 3 additions & 2 deletions tests/regression/56-witness/05-prec-problem.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types[+] precondition_loop_invariant
//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]'
#include <stdlib.h>
#include <goblint.h>

Expand All @@ -9,7 +9,8 @@ int foo(int* ptr1, int* ptr2){
} else {
result = 1;
}
// Look at the generated witness.yml to check whether there are contradictory precondition_loop_invariant[s]

while (0); // cram test checks for precondition invariant soundness
return result;
}

Expand Down
62 changes: 62 additions & 0 deletions tests/regression/56-witness/05-prec-problem.t
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
$ goblint --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]' 05-prec-problem.c
[Success][Assert] Assertion "y != z" will succeed (05-prec-problem.c:22:5-22:28)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 13
dead: 0
total lines: 13
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (05-prec-problem.c:13:12-13:13)
[Info][Witness] witness generation summary:
total generation entries: 6

TODO: Don't generate duplicate entries from each context: should have generated just 3.

Witness shouldn't contain two unsound precondition_loop_invariant-s with precondition `*ptr1 == 5 && *ptr2 == 5`,
and separately invariants `result == 0` and `result == 1`.
The sound invariant is `result == 1 || result == 0`.

$ yamlWitnessStrip < witness.yml
- entry_type: precondition_loop_invariant
location:
file_name: 05-prec-problem.c
file_hash: $FILE_HASH
line: 13
column: 4
function: foo
loop_invariant:
string: result == 1 || result == 0
type: assertion
format: C
precondition:
string: '*ptr1 == 5 && *ptr2 == 5'
type: assertion
format: C
- entry_type: precondition_loop_invariant
location:
file_name: 05-prec-problem.c
file_hash: $FILE_HASH
line: 13
column: 4
function: foo
loop_invariant:
string: '*ptr2 == 5'
type: assertion
format: C
precondition:
string: '*ptr1 == 5 && *ptr2 == 5'
type: assertion
format: C
- entry_type: precondition_loop_invariant
location:
file_name: 05-prec-problem.c
file_hash: $FILE_HASH
line: 13
column: 4
function: foo
loop_invariant:
string: '*ptr1 == 5'
type: assertion
format: C
precondition:
string: '*ptr1 == 5 && *ptr2 == 5'
type: assertion
format: C
59 changes: 57 additions & 2 deletions tests/regression/56-witness/08-witness-all-locals.t
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,40 @@
[Info][Witness] witness generation summary:
total generation entries: 3

TODO: check witness.yml content with yamlWitnessStrip
$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
function: main
location_invariant:
string: y == 10
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
function: main
location_invariant:
string: x == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 7
column: 4
function: main
location_invariant:
string: x == 5
type: assertion
format: C

Fewer entries are emitted if locals from nested block scopes are excluded:

Expand All @@ -19,4 +52,26 @@ Fewer entries are emitted if locals from nested block scopes are excluded:
[Info][Witness] witness generation summary:
total generation entries: 2

TODO: check witness.yml content with yamlWitnessStrip
$ yamlWitnessStrip < witness.yml
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 9
column: 2
function: main
location_invariant:
string: x == 5
type: assertion
format: C
- entry_type: location_invariant
location:
file_name: 08-witness-all-locals.c
file_hash: $FILE_HASH
line: 7
column: 4
function: main
location_invariant:
string: x == 5
type: assertion
format: C
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ int main() {
if (x < y) {
__goblint_check(x == 0); // UNKNOWN (intentional by unassume)
__goblint_check(x >= 0);
__goblint_check(x < y);
__goblint_check(x < y); // TODO: https://github.com/goblint/analyzer/issues/1373
}
return 0;
}
24 changes: 24 additions & 0 deletions tests/regression/56-witness/dune
Original file line number Diff line number Diff line change
@@ -1,2 +1,26 @@
(rule
(aliases runtest runaprontest)
(enabled_if %{lib-available:apron})
(deps
(package goblint)
../../../goblint ; update_suite calls local goblint
(:update_suite ../../../scripts/update_suite.rb)
(glob_files ??-*.c)
(glob_files ??-*.yml)) ; excluding witness.yml, etc. which might exist due to running update_suite outside of dune
(locks /update_suite)
(action
(chdir ../../..
(progn
(run %{update_suite} apron-unassume-interval)
(run %{update_suite} apron-unassume-branch)
(run %{update_suite} apron-unassume-global)
(run %{update_suite} apron-unassume-priv)
(run %{update_suite} apron-unassume-priv2)
(run %{update_suite} apron-unassume-strengthening)
(run %{update_suite} mine-tutorial-ex4.10)
(run %{update_suite} hh-ex3)
(run %{update_suite} bh-ex1-poly)
(run %{update_suite} apron-unassume-precheck)))))

(cram
(deps (glob_files *.c) (glob_files ??-*.yml)))
3 changes: 3 additions & 0 deletions tests/regression/70-transform/01-ordering.t
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
Suppress backtrace with code locations, especially for CI.
$ export OCAMLRUNPARAM=b=0

Check that assert transform is not allowed to happen after dead code removal
$ ./transform.sh --stderr remove_dead_code assert -- 01-empty.c
[Error] trans.activated: the 'assert' transform may not occur after the 'remove_dead_code' transform
Expand Down
Loading
Loading