Add option witness.invariant.typedefs

goblint · Mar 4, 2024 · d561941 · d561941
1 parent a6b7f4e
commit d561941
Show file tree

Hide file tree

Showing 3 changed files with 178 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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