From e4231ef0d4bf8b4809b66e9af1c33cd87625b614 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Mar 2024 17:44:35 +0200 Subject: [PATCH 1/5] Add witness invariant test for typedefs --- tests/regression/witness/typedef.t/run.t | 163 +++++++++++++++++++ tests/regression/witness/typedef.t/typedef.c | 15 ++ 2 files changed, 178 insertions(+) create mode 100644 tests/regression/witness/typedef.t/run.t create mode 100644 tests/regression/witness/typedef.t/typedef.c diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t new file mode 100644 index 0000000000..62f8409048 --- /dev/null +++ b/tests/regression/witness/typedef.t/run.t @@ -0,0 +1,163 @@ + $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' typedef.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 6 + dead: 0 + total lines: 6 + [Info][Witness] witness generation summary: + total generation entries: 14 + + $ yamlWitnessStrip < witness.yml + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: q == (void *)(& a) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: p == (void *)(& x) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: a.f == 43 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: '*((myint *)p) == 42' + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: ((s *)q)->f == 43 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: p == (void *)(& x) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: a.f == 43 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: '*((myint *)p) == 42' + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: p == (void *)(& x) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: '*((myint *)p) == 42' + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 9 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C diff --git a/tests/regression/witness/typedef.t/typedef.c b/tests/regression/witness/typedef.t/typedef.c new file mode 100644 index 0000000000..1e60ad084d --- /dev/null +++ b/tests/regression/witness/typedef.t/typedef.c @@ -0,0 +1,15 @@ +typedef int myint; + +typedef struct { + int f; +} s; + +int main() { + myint x = 42; + void *p = &x; + + s a; + a.f = 43; + void *q = &a; + return 0; +} From 0aa6a908470be1a3a94fd91de46660230915eb25 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Mar 2024 17:46:10 +0200 Subject: [PATCH 2/5] Unroll typedefs for witness invariants We have problems parsing them for validation: https://github.com/goblint/cil/issues/159. --- src/cdomain/value/domains/invariantCil.ml | 13 +++++++++++-- src/witness/witnessUtil.ml | 6 +++++- tests/regression/witness/typedef.t/run.t | 8 ++++---- 3 files changed, 20 insertions(+), 7 deletions(-) diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml index ef0687d6eb..0419bc2d65 100644 --- a/src/cdomain/value/domains/invariantCil.ml +++ b/src/cdomain/value/domains/invariantCil.ml @@ -13,15 +13,24 @@ class exp_replace_original_name_visitor = object method! vvrbl (vi: varinfo) = ChangeTo (var_replace_original_name vi) end -let exp_replace_original_name e = +let exp_replace_original_name e = (* TODO: curry to create object only once *) let visitor = new exp_replace_original_name_visitor in visitCilExpr visitor e +class exp_deep_unroll_types_visitor = object + inherit nopCilVisitor + method! vtype (t: typ) = + ChangeTo (unrollTypeDeep t) +end +let exp_deep_unroll_types = + let visitor = new exp_deep_unroll_types_visitor in + visitCilExpr visitor + let var_is_in_scope scope vi = match Cilfacade.find_scope_fundec vi with | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *) - | Some fd -> + | Some fd -> if CilType.Fundec.equal fd scope then GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr) else diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 6c02546168..0e57132c8e 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -160,7 +160,11 @@ struct | e -> to_conjunct_set e let process_exp inv = - let inv' = InvariantCil.exp_replace_original_name inv in + let inv' = + inv + |> InvariantCil.exp_deep_unroll_types + |> InvariantCil.exp_replace_original_name + in if GobConfig.get_bool "witness.invariant.split-conjunction" then ES.elements (pullOutCommonConjuncts inv') else diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t index 62f8409048..27f4a5f5a3 100644 --- a/tests/regression/witness/typedef.t/run.t +++ b/tests/regression/witness/typedef.t/run.t @@ -59,7 +59,7 @@ column: 2 function: main location_invariant: - string: '*((myint *)p) == 42' + string: '*((int *)p) == 42' type: assertion format: C - entry_type: location_invariant @@ -70,7 +70,7 @@ column: 2 function: main location_invariant: - string: ((s *)q)->f == 43 + string: ((struct __anonstruct_s_109580352 *)q)->f == 43 type: assertion format: C - entry_type: location_invariant @@ -114,7 +114,7 @@ column: 2 function: main location_invariant: - string: '*((myint *)p) == 42' + string: '*((int *)p) == 42' type: assertion format: C - entry_type: location_invariant @@ -147,7 +147,7 @@ column: 2 function: main location_invariant: - string: '*((myint *)p) == 42' + string: '*((int *)p) == 42' type: assertion format: C - entry_type: location_invariant From d3ef63384451d11a56dee4931c09c1e5d8d245d5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Mar 2024 18:10:42 +0200 Subject: [PATCH 3/5] Exclude witness invariants with __anon structs --- src/cdomain/value/domains/invariantCil.ml | 16 ++++++++++++++++ src/witness/witnessUtil.ml | 1 + tests/regression/witness/typedef.t/run.t | 13 +------------ 3 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml index 0419bc2d65..9a8c11fff7 100644 --- a/src/cdomain/value/domains/invariantCil.ml +++ b/src/cdomain/value/domains/invariantCil.ml @@ -84,6 +84,22 @@ let exp_contains_tmp e = ignore (visitCilExpr visitor e); !acc +class exp_contains_anon_type_visitor = object + inherit nopCilVisitor + method! vtype (t: typ) = + match t with + | TComp ({cname; _}, _) when BatString.starts_with_stdlib ~prefix:"__anon" cname -> + raise Stdlib.Exit + | _ -> + DoChildren +end +let exp_contains_anon_type e = (* TODO: curry to create object only once *) + let visitor = new exp_contains_anon_type_visitor in + match visitCilExpr visitor e with + | _ -> false + | exception Stdlib.Exit -> true + + (* TODO: synchronize magic constant with BaseDomain *) let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@" diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 0e57132c8e..cc53e485a4 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -167,6 +167,7 @@ struct in if GobConfig.get_bool "witness.invariant.split-conjunction" then ES.elements (pullOutCommonConjuncts inv') + |> List.filter (Fun.negate InvariantCil.exp_contains_anon_type) else [inv'] end diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t index 27f4a5f5a3..dfc9d3d585 100644 --- a/tests/regression/witness/typedef.t/run.t +++ b/tests/regression/witness/typedef.t/run.t @@ -4,7 +4,7 @@ dead: 0 total lines: 6 [Info][Witness] witness generation summary: - total generation entries: 14 + total generation entries: 13 $ yamlWitnessStrip < witness.yml - entry_type: location_invariant @@ -62,17 +62,6 @@ string: '*((int *)p) == 42' type: assertion format: C - - entry_type: location_invariant - location: - file_name: typedef.c - file_hash: $FILE_HASH - line: 14 - column: 2 - function: main - location_invariant: - string: ((struct __anonstruct_s_109580352 *)q)->f == 43 - type: assertion - format: C - entry_type: location_invariant location: file_name: typedef.c From a6b7f4e717091222a7c76de435e2545ca55550f0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 4 Mar 2024 14:33:59 +0200 Subject: [PATCH 4/5] Create visitors in InvariantCil only once --- src/cdomain/value/domains/invariantCil.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml index 9a8c11fff7..813ec25818 100644 --- a/src/cdomain/value/domains/invariantCil.ml +++ b/src/cdomain/value/domains/invariantCil.ml @@ -13,9 +13,9 @@ class exp_replace_original_name_visitor = object method! vvrbl (vi: varinfo) = ChangeTo (var_replace_original_name vi) end -let exp_replace_original_name e = (* TODO: curry to create object only once *) +let exp_replace_original_name = let visitor = new exp_replace_original_name_visitor in - visitCilExpr visitor e + visitCilExpr visitor class exp_deep_unroll_types_visitor = object inherit nopCilVisitor @@ -93,11 +93,12 @@ class exp_contains_anon_type_visitor = object | _ -> DoChildren end -let exp_contains_anon_type e = (* TODO: curry to create object only once *) +let exp_contains_anon_type = let visitor = new exp_contains_anon_type_visitor in - match visitCilExpr visitor e with - | _ -> false - | exception Stdlib.Exit -> true + fun e -> + match visitCilExpr visitor e with + | _ -> false + | exception Stdlib.Exit -> true (* TODO: synchronize magic constant with BaseDomain *) From d561941b910d4f3a923f4efe42778bcf75c1b54e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 4 Mar 2024 15:49:56 +0200 Subject: [PATCH 5/5] Add option witness.invariant.typedefs --- src/config/options.schema.json | 6 + src/witness/witnessUtil.ml | 8 +- tests/regression/witness/typedef.t/run.t | 166 ++++++++++++++++++++++- 3 files changed, 178 insertions(+), 2 deletions(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index a01a5bdb31..c3d21be874 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2474,6 +2474,12 @@ "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.", "type": "boolean", "default": false + }, + "typedefs": { + "title": "witness.invariant.typedefs", + "description": "Emit invariants with typedef-ed types (e.g. in casts). Our validator cannot parse these.", + "type": "boolean", + "default": true } }, "additionalProperties": false diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index cc53e485a4..24316cbee4 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -160,9 +160,15 @@ struct | e -> to_conjunct_set e let process_exp inv = + let exp_deep_unroll_types = + if GobConfig.get_bool "witness.invariant.typedefs" then + Fun.id + else + InvariantCil.exp_deep_unroll_types + in let inv' = inv - |> InvariantCil.exp_deep_unroll_types + |> exp_deep_unroll_types |> InvariantCil.exp_replace_original_name in if GobConfig.get_bool "witness.invariant.split-conjunction" then diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t index dfc9d3d585..b06164743b 100644 --- a/tests/regression/witness/typedef.t/run.t +++ b/tests/regression/witness/typedef.t/run.t @@ -1,4 +1,4 @@ - $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' typedef.c + $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.typedefs typedef.c [Info][Deadcode] Logical lines of code (LLoC) summary: live: 6 dead: 0 @@ -150,3 +150,167 @@ string: x == 42 type: assertion format: C + + $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable witness.invariant.typedefs typedef.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 6 + dead: 0 + total lines: 6 + [Info][Witness] witness generation summary: + total generation entries: 14 + + $ yamlWitnessStrip < witness.yml + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: q == (void *)(& a) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: p == (void *)(& x) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: a.f == 43 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: '*((myint *)p) == 42' + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 14 + column: 2 + function: main + location_invariant: + string: ((s *)q)->f == 43 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: p == (void *)(& x) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: a.f == 43 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: '*((myint *)p) == 42' + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: p == (void *)(& x) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: '*((myint *)p) == 42' + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: typedef.c + file_hash: $FILE_HASH + line: 9 + column: 2 + function: main + location_invariant: + string: x == 42 + type: assertion + format: C