Unroll typedefs in witness invariants

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 =
   let visitor = new exp_replace_original_name_visitor in
-  visitCilExpr visitor e
+  visitCilExpr visitor
+
+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
@@ -75,6 +84,23 @@ 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 =
+  let visitor = new exp_contains_anon_type_visitor in
+  fun e ->
+    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@"
 

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

src/witness/witnessUtil.ml

@@ -160,9 +160,20 @@ struct
     | e -> to_conjunct_set e
 
   let process_exp inv =
-    let inv' = InvariantCil.exp_replace_original_name inv in
+    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
+      |> exp_deep_unroll_types
+      |> InvariantCil.exp_replace_original_name
+    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