Merge pull request #855 from goblint/fix_evalAssert

Fix EvalAssert transformation to work on coreutil programs

Author: jerhard

src/cdomains/valueDomain.ml

@@ -1239,14 +1239,32 @@ struct
               in
               let offset = offs_to_offset offs in
 
+              let cast_to_void_ptr e = 
+                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
                   let addr_exp = AddrOf (Var vi, offset) in (* AddrOf or Lval? *)
+                  let addr_exp, c_exp = if typeSig (typeOf addr_exp) <> typeSig (typeOf c_exp) then
+                      cast_to_void_ptr addr_exp, cast_to_void_ptr c_exp
+                    else 
+                      addr_exp, c_exp
+                  in 
                   Invariant.of_exp Cil.(BinOp (Eq, c_exp, addr_exp, intType))
                 else
                   Invariant.none
               in
-              let i_deref = deref_invariant ~vs vi ~offset ~lval:(Mem c_exp, NoOffset) in
+              let i_deref =
+                match Cilfacade.typeOfLval (Var vi, offset) with
+                | typ ->
+                  (* Address set for a void* variable contains pointers to values of non-void type,
+                     so insert pointer cast to make invariant expression valid (no field/index on void). *)
+                  let newt = TPtr (typ, []) in
+                  let c_exp = Cilfacade.mkCast ~e:c_exp ~newt in
+                  deref_invariant ~vs vi ~offset ~lval:(Mem c_exp, NoOffset)
+                | exception Cilfacade.TypeOfError _ -> (* typeOffset: Index on a non-array on calloc-ed alloc variables *)
+                  Invariant.none
+              in
 
               Some (Invariant.(acc || (i && i_deref)))
             | Addr.NullPtr ->
@@ -1285,9 +1303,9 @@ struct
       else
         Invariant.none
     | `Address n -> ad_invariant ~vs ~offset ~lval n
-    | `Blob n -> blob_invariant ~vs ~offset ~lval n
     | `Struct n -> Structs.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
     | `Union n -> Unions.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
+    | `Blob n when GobConfig.get_bool "ana.base.invariant.blobs" -> blob_invariant ~vs ~offset ~lval n
     | _ -> Invariant.none (* TODO *)
 
   and deref_invariant ~vs vi ~offset ~lval =

src/framework/control.ml

@@ -580,7 +580,13 @@ struct
                 ; context = (fun () -> ctx_failwith "No context in query context.")
                 ; edge    = MyCFG.Skip
                 ; local  = local
-                ; global = (fun g -> EQSys.G.spec (GHT.find gh (EQSys.GVar.spec g)))
+                ; global =
+                  (fun g ->
+                    try
+                      EQSys.G.spec (GHT.find gh (EQSys.GVar.spec g))
+                    with Not_found ->
+                      M.warn ~category:MessageCategory.Unsound "Global %a not found during transformation, proceeding with bot." Spec.V.pretty g;
+                      Spec.G.bot ())
                 ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in query context.")
                 ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
                 ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")

src/transform/evalAssert.ml

@@ -26,7 +26,7 @@ module EvalAssert = struct
   let surroundByAtomic = true
 
   (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
-  let ass = makeVarinfo true "assert" (TVoid [])
+  let ass = makeVarinfo true "__VERIFIER_assert" (TVoid [])
   let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid [])
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
@@ -138,8 +138,14 @@ module EvalAssert = struct
       in
       ChangeDoChildrenPost (s, instrument_statement)
   end
+
   let transform (ask: ?node:Node.t -> Cil.location -> Queries.ask) file = begin
     visitCilFile (new visitor ask) file;
+
+    (* Add function declarations before function definitions.
+       This way, asserts may reference functions defined later. *)
+    Cilfacade.add_function_declarations file;
+
     let assert_filename = GobConfig.get_string "trans.output" in
     let oc = Stdlib.open_out assert_filename in
     dumpFile defaultCilPrinter oc assert_filename file; end

src/util/cilfacade.ml

@@ -296,32 +296,32 @@ let locs = Hashtbl.create 200
 
 (** Visitor to count locs appearing inside a fundec. *)
 class countFnVisitor = object
-    inherit nopCilVisitor
-    method! vstmt s =
-      match s.skind with
-      | Return (_, loc)
-      | Goto (_, loc)
-      | ComputedGoto (_, loc)
-      | Break loc
-      | Continue loc
-      | If (_,_,_,loc,_)
-      | Switch (_,_,_,loc,_)
-      | Loop (_,loc,_,_,_)
-        -> Hashtbl.replace locs loc.line (); DoChildren
-      | _ ->
-        DoChildren
-
-    method! vinst = function
-      | Set (_,_,loc,_)
-      | Call (_,_,_,loc,_)
-      | Asm (_,_,_,_,_,loc)
-        -> Hashtbl.replace locs loc.line (); SkipChildren
-      | _ -> SkipChildren
-
-    method! vvdec _ = SkipChildren
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
+  inherit nopCilVisitor
+  method! vstmt s =
+    match s.skind with
+    | Return (_, loc)
+    | Goto (_, loc)
+    | ComputedGoto (_, loc)
+    | Break loc
+    | Continue loc
+    | If (_,_,_,loc,_)
+    | Switch (_,_,_,loc,_)
+    | Loop (_,loc,_,_,_)
+      -> Hashtbl.replace locs loc.line (); DoChildren
+    | _ ->
+      DoChildren
+
+  method! vinst = function
+    | Set (_,_,loc,_)
+    | Call (_,_,_,loc,_)
+    | Asm (_,_,_,_,_,loc)
+      -> Hashtbl.replace locs loc.line (); SkipChildren
+    | _ -> SkipChildren
+
+  method! vvdec _ = SkipChildren
+  method! vexpr _ = SkipChildren
+  method! vlval _ = SkipChildren
+  method! vtype _ = SkipChildren
 end
 
 let fnvis = new countFnVisitor
@@ -346,16 +346,16 @@ module StmtH = Hashtbl.Make (CilType.Stmt)
 
 let stmt_fundecs: fundec StmtH.t ResettableLazy.t =
   ResettableLazy.from_fun (fun () ->
-    let h = StmtH.create 113 in
-    iterGlobals !current_file (function
-        | GFun (fd, _) ->
-          List.iter (fun stmt ->
-              StmtH.replace h stmt fd
-            ) fd.sallstmts
-        | _ -> ()
-      );
-    h
-  )
+      let h = StmtH.create 113 in
+      iterGlobals !current_file (function
+          | GFun (fd, _) ->
+            List.iter (fun stmt ->
+                StmtH.replace h stmt fd
+              ) fd.sallstmts
+          | _ -> ()
+        );
+      h
+    )
 
 let pseudo_return_to_fun = StmtH.create 113
 
@@ -369,14 +369,14 @@ module VarinfoH = Hashtbl.Make (CilType.Varinfo)
 
 let varinfo_fundecs: fundec VarinfoH.t ResettableLazy.t =
   ResettableLazy.from_fun (fun () ->
-    let h = VarinfoH.create 111 in
-    iterGlobals !current_file (function
-        | GFun (fd, _) ->
-          VarinfoH.replace h fd.svar fd
-        | _ -> ()
-      );
-    h
-  )
+      let h = VarinfoH.create 111 in
+      iterGlobals !current_file (function
+          | GFun (fd, _) ->
+            VarinfoH.replace h fd.svar fd
+          | _ -> ()
+        );
+      h
+    )
 
 (** Find [fundec] by the function's [varinfo] (has the function name and type). *)
 let find_varinfo_fundec vi = VarinfoH.find (ResettableLazy.force varinfo_fundecs) vi (* vi argument must be explicit, otherwise force happens immediately *)
@@ -386,14 +386,14 @@ module StringH = Hashtbl.Make (Printable.Strings)
 
 let name_fundecs: fundec StringH.t ResettableLazy.t =
   ResettableLazy.from_fun (fun () ->
-    let h = StringH.create 111 in
-    iterGlobals !current_file (function
-        | GFun (fd, _) ->
-          StringH.replace h fd.svar.vname fd
-        | _ -> ()
-      );
-    h
-  )
+      let h = StringH.create 111 in
+      iterGlobals !current_file (function
+          | GFun (fd, _) ->
+            StringH.replace h fd.svar.vname fd
+          | _ -> ()
+        );
+      h
+    )
 
 (** Find [fundec] by the function's name. *)
 (* TODO: why unused? *)
@@ -408,19 +408,19 @@ type varinfo_role =
 
 let varinfo_roles: varinfo_role VarinfoH.t ResettableLazy.t =
   ResettableLazy.from_fun (fun () ->
-    let h = VarinfoH.create 113 in
-    iterGlobals !current_file (function
-        | GFun (fd, _) ->
-          VarinfoH.replace h fd.svar Function; (* function itself can be used as a variable (function pointer) *)
-          List.iter (fun vi -> VarinfoH.replace h vi (Formal fd)) fd.sformals;
-          List.iter (fun vi -> VarinfoH.replace h vi (Local fd)) fd.slocals
-        | GVar (vi, _, _)
-        | GVarDecl (vi, _) ->
-          VarinfoH.replace h vi Global
-        | _ -> ()
-      );
-    h
-  )
+      let h = VarinfoH.create 113 in
+      iterGlobals !current_file (function
+          | GFun (fd, _) ->
+            VarinfoH.replace h fd.svar Function; (* function itself can be used as a variable (function pointer) *)
+            List.iter (fun vi -> VarinfoH.replace h vi (Formal fd)) fd.sformals;
+            List.iter (fun vi -> VarinfoH.replace h vi (Local fd)) fd.slocals
+          | GVar (vi, _, _)
+          | GVarDecl (vi, _) ->
+            VarinfoH.replace h vi Global
+          | _ -> ()
+        );
+      h
+    )
 
 (** Find the role of the [varinfo]. *)
 let find_varinfo_role vi = VarinfoH.find (ResettableLazy.force varinfo_roles) vi (* vi argument must be explicit, otherwise force happens immediately *)
@@ -449,15 +449,15 @@ let find_scope_fundec vi =
 let original_names: string VarinfoH.t ResettableLazy.t =
   (* only invert environment map when necessary (e.g. witnesses) *)
   ResettableLazy.from_fun (fun () ->
-    let h = VarinfoH.create 113 in
-    Hashtbl.iter (fun original_name (envdata, _) ->
-        match envdata with
-        | Cabs2cil.EnvVar vi when vi.vname <> "" -> (* TODO: fix temporary variables with empty names being in here *)
-          VarinfoH.replace h vi original_name
-        | _ -> ()
-      ) Cabs2cil.environment;
-    h
-  )
+      let h = VarinfoH.create 113 in
+      Hashtbl.iter (fun original_name (envdata, _) ->
+          match envdata with
+          | Cabs2cil.EnvVar vi when vi.vname <> "" -> (* TODO: fix temporary variables with empty names being in here *)
+            VarinfoH.replace h vi original_name
+          | _ -> ()
+        ) Cabs2cil.environment;
+      h
+    )
 
 (** Find the original name (in input source code) of the [varinfo].
     If it was renamed by CIL, then returns the original name before renaming.
@@ -480,3 +480,21 @@ let stmt_pretty_short () x =
   | Instr (y::ys) -> dn_instr () y
   | If (exp,_,_,_,_) -> dn_exp () exp
   | _ -> dn_stmt () x
+
+(** Given a [Cil.file], reorders its [globals], inserts function declarations before function definitions.
+    This function may be used after a code transformation to ensure that the order of globals yields a compilable program. *)
+let add_function_declarations (file: Cil.file): unit =
+  let globals = file.globals in
+  let functions, non_functions = List.partition (fun g -> match g with GFun _ -> true | _ -> false) globals in
+  let upto_last_type, non_types = GobList.until_last_with (fun g -> match g with GType _ -> true | _ -> false) non_functions in
+  let declaration_from_GFun f = match f with
+    | GFun (f, _) when String.starts_with ~prefix:"__builtin" f.svar.vname ->
+      (* Builtin functions should not occur in asserts generated, so there is no need to add declarations for them.*)
+      None 
+    | GFun (f, _) ->
+      Some (GVarDecl (f.svar, locUnknown))
+    | _ -> failwith "Expected GFun, but was something else."
+  in
+  let fun_decls = List.filter_map declaration_from_GFun functions in
+  let globals = upto_last_type @ fun_decls @ non_types @ functions in
+  file.globals <- globals

src/util/gobList.ml

@@ -27,3 +27,12 @@ let rec fold_while_some (f : 'a -> 'b -> 'a option) (acc: 'a) (xs: 'b list): 'a
     end
 
 let equal = List.eq
+
+(** Given a predicate and a list, returns two lists [(l1, l2)].
+    [l1] contains the prefix of the list until the last element that satisfies the predicate, [l2] contains all subsequent elements. The order of elements is preserved. *)
+let until_last_with (pred: 'a -> bool) (xs: 'a list) =
+  let rec until_last_helper last seen = function
+    | [] -> List.rev last, List.rev seen
+    | h::t -> if pred h then until_last_helper (h::seen@last) [] t else until_last_helper last (h::seen) t
+  in
+  until_last_helper [] [] xs

src/util/options.schema.json

@@ -717,6 +717,12 @@
                   "description": "Generate base analysis invariants",
                   "type": "boolean",
                   "default": true
+                },
+                "blobs": {
+                  "title": "ana.base.invariant.blobs",
+                  "description": "Whether to dump assertions about all blobs. Enabling this option may lead to unsound asserts.",
+                  "type": "boolean",
+                  "default": false
                 }
               },
               "additionalProperties": false

tests/regression/61-evalAssert/01-union_evalAssert.c

@@ -0,0 +1,33 @@
+// PARAM: --set trans.activated[+] "assert"
+
+// Running the assert transformation on this test used to yield code that cannot be compiled with gcc, due to superfluous offsets on a pointer
+struct s {
+    int a;
+    int b;
+};
+
+union u {
+    struct s str;
+    int i;
+};
+
+
+int main(){
+    union u un;
+
+    struct s* ptr;
+
+    un.str.a = 1;
+    un.str.b = 2;
+
+    ptr = &un.str;
+    int r;
+    int x;
+    if(r){
+        x = 2;
+    } else {
+        x = 3;
+    }
+
+    return 0;
+}