Merge pull request #1876 from goblint/witness-invariant-anon-comp-field-2

Exclude `__annonCompField` offsets from witness invariants

Author: sim642

src/analyses/apron/relationAnalysis.apron.ml

@@ -613,7 +613,7 @@ struct
         if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
           RD.cil_exp_of_lincons1 lincons1
           |> Option.map e_inv
-          |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
+          |> Option.filter (InvariantCil.exp_is_suitable ~scope)
         else
           None
       )

src/analyses/apron/relationPriv.apron.ml

@@ -733,7 +733,7 @@ struct
               (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
               if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
                 RD.cil_exp_of_lincons1 lincons1
-                |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))
+                |> Option.filter (InvariantCil.exp_is_suitable ?scope:None)
               else
                 None
             )

src/analyses/varEq.ml

@@ -28,7 +28,7 @@ struct
           if B.mem MyCFG.unknown_exp s then
             a
           else (
-            let s' = B.filter (fun x -> not (InvariantCil.exp_contains_tmp x) && InvariantCil.exp_is_in_scope scope x && not (is_str_constant x)) s in
+            let s' = B.filter (fun x -> InvariantCil.exp_is_suitable ~scope x && not (is_str_constant x)) s in
             if B.cardinal s' >= 2 then (
               (* instead of returning quadratically many pairwise equalities from a cluster,
                  output linear number of equalities with just one expression *)

src/cdomain/value/cdomains/valueDomain.ml

@@ -1364,7 +1364,7 @@ struct
             Cilfacade.mkCast ~e ~newt:(TPtr (TVoid [], []))
           in
           let i =
-            if InvariantCil.(not (exp_contains_tmp c_exp) && exp_is_in_scope scope c_exp && not (var_is_tmp vi) && var_is_in_scope scope vi && not (var_is_heap vi)) then
+            if InvariantCil.(exp_is_suitable ~scope c_exp && var_is_suitable ~scope vi && not (var_is_heap vi)) then
               try
                 let addr_exp = AddrOf (Var vi, offset) in (* AddrOf or Lval? *)
                 let addr_exp, c_exp = if typeSig (Cilfacade.typeOf addr_exp) <> typeSig (Cilfacade.typeOf c_exp) then
@@ -1395,7 +1395,7 @@ struct
         | Addr.NullPtr ->
           let i =
             let addr_exp = integer 0 in
-            if InvariantCil.(not (exp_contains_tmp c_exp) && exp_is_in_scope scope c_exp) then
+            if InvariantCil.exp_is_suitable ~scope c_exp then
               Invariant.of_exp Cil.(BinOp (Eq, c_exp, addr_exp, intType))
             else
               Invariant.none
@@ -1417,13 +1417,13 @@ struct
   and vd_invariant ~vs ~offset ~lval = function
     | Compound.Int n ->
       let e = Lval lval in
-      if InvariantCil.(not (exp_contains_tmp e) && exp_is_in_scope scope e) then
+      if InvariantCil.exp_is_suitable ~scope e then
         ID.invariant e n
       else
         Invariant.none
     | Float n ->
       let e = Lval lval in
-      if InvariantCil.(not (exp_contains_tmp e) && exp_is_in_scope scope e) then
+      if InvariantCil.exp_is_suitable ~scope e then
         FD.invariant e n
       else
         Invariant.none

src/cdomain/value/domains/invariantCil.ml

@@ -90,6 +90,38 @@ let exp_contains_tmp e =
   ignore (visitCilExpr visitor e);
   !acc
 
+
+let fieldinfo_is_anon (fi: fieldinfo) =
+  String.starts_with ~prefix:"__annonCompField" fi.fname (* TODO: what if CIL-ed program explicitly has this? *)
+
+let rec offset_contains_anon_comp_offset = function
+  | NoOffset -> false
+  | Index (e, offs') -> offset_contains_anon_comp_offset offs' (* does not check e!, done by visitor *)
+  | Field (fi, offs') -> fieldinfo_is_anon fi || offset_contains_anon_comp_offset offs'
+
+class exp_contains_anon_comp_offset_visitor = object
+  inherit nopCilVisitor
+  method! voffs (offs: offset) =
+    if offset_contains_anon_comp_offset offs then
+      raise Stdlib.Exit
+    else
+      DoChildren (* recurse to Index offset expressions! *)
+end
+let exp_contains_anon_comp_offset =
+  let visitor = new exp_contains_anon_comp_offset_visitor in
+  fun e ->
+    match visitCilExpr visitor e with
+    | _ -> false
+    | exception Stdlib.Exit -> true
+
+
+let var_is_suitable ?scope v =
+  not (var_is_tmp v) && GobOption.for_all (fun scope -> var_is_in_scope scope v) scope
+
+let exp_is_suitable ?scope e =
+  not (exp_contains_tmp e || exp_contains_anon_comp_offset e) && GobOption.for_all (fun scope -> exp_is_in_scope scope e) scope
+
+
 class exp_contains_anon_type_visitor = object
   inherit nopCilVisitor
   method! vtype (t: typ) =

src/cdomains/c2poDomain.ml

@@ -293,7 +293,7 @@ module D = struct
     let not_in_scope t =
       let var = T.get_var t in
       let var = Var.to_varinfo var in
-      InvariantCil.var_is_tmp var || not (InvariantCil.var_is_in_scope scope  var)
+      not (InvariantCil.var_is_suitable ~scope var)
     in
     remove_terms not_in_scope cc
 end