Fix EvalAssert transformation to work on coreutil programs

src/cdomains/unionDomain.ml

@@ -29,21 +29,22 @@ struct
     | Cil.NoOffset ->
       let c_lval = Option.get lval in
       begin match lift_f with
-      | `Lifted f ->
-        let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) c_lval in
-        value_invariant ~offset ~lval:(Some f_lval) v
-      | `Top
-      | `Bot ->
-        Invariant.none
+        | `Lifted f ->
+          let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) c_lval in
+          value_invariant ~offset ~lval:(Some f_lval) v
+        | `Top
+        | `Bot ->
+          Invariant.none
       end
     (* invariant for one field *)
     | Field (f, offset) ->
-      let c_lval = Option.get lval in
       begin match lift_f with
         | `Lifted f' ->
           let v = Values.cast ~torg:f'.ftype f.ftype v in
-          let f_lval = Cil.addOffsetLval (Field (f, NoOffset)) c_lval in
-          value_invariant ~offset ~lval:(Some f_lval) v
+          (* Do not add the field offset to lval here:
+             Otherwise, for pointers to a member type of the union, this would
+             generate an assertion with illegal field offset. *)
+          value_invariant ~offset ~lval:lval v
         | `Top
         | `Bot ->
           Invariant.none

src/cdomains/valueDomain.ml

@@ -1246,7 +1246,18 @@ struct
                 else
                   Invariant.none
               in
-              let i_deref = deref_invariant ~vs ~lval vi offset (Mem c_exp, NoOffset) in
+              let i_deref =
+                match Cilfacade.typeOfLval (Var vi, offset) with
+                | TVoid _ -> Invariant.none (* TODO: Try to determine type of abstract value and introduce appropriate casts *)
+                | 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 ~lval vi offset (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 +1296,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 "witness.invariant.blobs" -> blob_invariant ~vs ~offset ~lval n
     | _ -> Invariant.none (* TODO *)
 
   (* TODO: remove duplicate lval arguments? *)

src/framework/control.ml

@@ -579,7 +579,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

@@ -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

@@ -343,32 +343,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
@@ -393,16 +393,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
 
@@ -416,14 +416,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 *)
@@ -433,14 +433,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? *)
@@ -455,19 +455,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 *)
@@ -496,15 +496,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.
@@ -527,3 +527,18 @@ 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].
+    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, _) ->
+      GVarDecl (f.svar, locUnknown)
+    | _ -> failwith "Expected GFun, but was something else."
+  in
+  let fun_decls = List.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

@@ -2102,6 +2102,12 @@
                 "Whether to dump assertions about all local variables or limitting it to modified ones where possible.",
               "type": "boolean",
               "default": true
+            },
+            "blobs": {
+              "title": "witness.invariant.blobs",
+              "description": "Whether to dump assertions about all blobs. Enabling this option may lead to unsound asserts.",
+              "type": "boolean",
+              "default": false
             }
           },
           "additionalProperties": false