Merge pull request #722 from TDacik/malloc_uniqueness

Malloc uniqueness

Author: michael-schwarz

src/analyses/base.ml

@@ -2680,9 +2680,11 @@ struct
             if get_bool "sem.malloc.fail"
             then AD.join addr AD.null_ptr (* calloc can fail and return NULL *)
             else addr in
+          let ik = Cilfacade.ptrdiff_ikind () in
+          let blobsize = ID.mul (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st size) (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st n) in
           (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
-          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.from_var heap_var), TVoid [], `Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (`Blob (VD.bot (), eval_int (Analyses.ask_of_ctx ctx) gs st size, false))));
-                                                         (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), `Address (add_null (AD.from_var_offset (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.from_var heap_var), TVoid [], `Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (`Blob (VD.bot (), blobsize, false))));
+                                  (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), `Address (add_null (AD.from_var_offset (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
         | _ -> st
       end
     | Realloc { ptr = p; size }, _ ->

src/analyses/libraryFunctions.ml

@@ -41,7 +41,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 (** Linux kernel functions. *)
 let linux_descs_list: (string * LibraryDesc.t) list = (* LibraryDsl. *) [
 
-  ]
+]
 
 (** Goblint functions. *)
 let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[

src/analyses/mallocWrapperAnalysis.ml

@@ -3,8 +3,10 @@
 open Prelude.Ana
 open Analyses
 open GobConfig
+open ThreadIdDomain
+module Q = Queries
 
-module Spec : Analyses.MCPSpec =
+module Spec: Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
@@ -13,24 +15,49 @@ struct
       let bot_name = "Unreachable node"
     end)
 
-  module Node = struct
-    include Node
+  module Chain = Lattice.Chain (struct
+      let n () =
+        let p = get_int "ana.malloc.unique_address_count" in
+        if p < 0 then
+          failwith "Option ana.malloc.unique_address_count has to be non-negative"
+        else p + 1 (* Unique addresses + top address *)
+
+      let names x = if x = (n () - 1) then "top" else Format.asprintf "%d" x
+
+    end)
+
+  (* Map for counting malloc node visits up to n (of the current thread). *)
+  module MallocCounter = struct
+    include MapDomain.MapBot_LiftTop(PL)(Chain)
+
+    (* Increase counter for given node. If it does not exists yet, create it. *)
+    let add_malloc counter node =
+      let malloc = `Lifted node in
+      let count = find malloc counter in
+      if Chain.is_top count then
+        counter
+      else
+        remove malloc counter |> add malloc (count + 1)
+  end
+
+  module ThreadNode = struct
+    include Printable.Prod3 (ThreadIdDomain.ThreadLifted) (Node) (Chain)
+
     (* Description that gets appended to the varinfo-name in user output. *)
-    let describe_varinfo (v: varinfo) node =
+    let describe_varinfo (v: varinfo) (t, node, c) =
       let loc = UpdateCil.getLoc node in
       CilType.Location.show loc
 
-    let name_varinfo node = match node with
-      | Node.Statement s -> "(alloc@sid:" ^ (string_of_int s.sid) ^ ")"
-      | _ -> failwith "A function entry or return node can not be the node after a malloc"
+    let name_varinfo (t, node, c) =
+      Format.asprintf "(alloc@sid:%s@tid:%s(#%s))" (Node.show_id node) (ThreadLifted.show t) (Chain.show c)
+
   end
 
-  module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(Node)
+  module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)
   let name () = "mallocWrapper"
-  module D = PL
-  module C = D
 
-  module Q = Queries
+  module D = Lattice.Prod (MallocCounter) (PL)
+  module C = D
 
   let wrappers = Hashtbl.create 13
 
@@ -48,42 +75,64 @@ struct
     ctx.local
 
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    let calleeofinterest = Hashtbl.mem wrappers f.svar.vname in
-    let calleectx = if calleeofinterest then
-        if ctx.local = `Top then
-          `Lifted ctx.node (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *)
-        else ctx.local (* if an interesting callee is called by an interesting caller, then we remember the caller context *)
-      else D.top () in  (* if an uninteresting callee is called, then we forget what was called before *)
-    [(ctx.local, calleectx)]
-
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
-    ctx.local
-
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    ctx.local
+    let counter, wrapper_node = ctx.local in
+    let new_wrapper_node =
+      if Hashtbl.mem wrappers f.svar.vname then
+        match wrapper_node with
+        | `Lifted _ ->  wrapper_node (* if an interesting callee is called by an interesting caller, then we remember the caller context *)
+        | _ ->  (`Lifted ctx.node) (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *)
+      else
+        PL.top () (* if an uninteresting callee is called, then we forget what was called before *)
+    in
+    let callee = (counter, new_wrapper_node) in
+    [(ctx.local, callee)]
+
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc ((counter, _):D.t) : D.t =
+    (* Keep (potentially higher) counter from callee and keep wrapper node from caller *)
+    let _, lnode = ctx.local in
+    (counter, lnode)
+
+  let special (ctx: (D.t, G.t, C.t, V.t) ctx) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let desc = LibraryFunctions.find f in
+    match desc.special arglist with
+    | Malloc _ | Calloc _ | Realloc _ ->
+      let counter, wrapper_node = ctx.local in
+      (MallocCounter.add_malloc counter ctx.node, wrapper_node)
+    | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+
+  let threadenter ctx lval f args =
+    (* The new thread receives a fresh counter *)
+    [D.bot ()]
+
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   type marshal = NodeVarinfoMap.marshal
 
   let get_heap_var = NodeVarinfoMap.to_varinfo
-  let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Queries.result =
+
+
+  let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Q.result =
+    let counter, wrapper_node = ctx.local in
     match q with
     | Q.HeapVar ->
-      let node = match ctx.local with
-        | `Lifted vinfo -> vinfo
+      let node = match wrapper_node with
+        | `Lifted wrapper_node -> wrapper_node
         | _ -> ctx.node
       in
-      let var = get_heap_var node in
+      let count = MallocCounter.find (`Lifted node) counter in
+      let var = get_heap_var (ctx.ask Q.CurrentThreadId, node, count) in
       var.vdecl <- UpdateCil.getLoc node; (* TODO: does this do anything bad for incremental? *)
       `Lifted var
     | Q.IsHeapVar v ->
       NodeVarinfoMap.mem_varinfo v
     | Q.IsMultiple v ->
-      NodeVarinfoMap.mem_varinfo v
+      begin match NodeVarinfoMap.from_varinfo v with
+        | Some (_, _, c) -> Chain.is_top c || not (ctx.ask Q.MustBeUniqueThread)
+        | None -> false
+      end
     | _ -> Queries.Result.top q
 
   let init marshal =
@@ -95,4 +144,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis (module Spec)

src/cdomains/threadFlagDomain.ml

@@ -30,7 +30,7 @@ module Simple: S =
 struct
   module SimpleNames =
   struct
-    let n = 3
+    let n () = 3
     let names = function
       | 0 -> "Singlethreaded"
       | 1 -> "Multithreaded (main)"

src/cdomains/valueDomain.ml

@@ -335,7 +335,7 @@ struct
     let one_addr = let open Addr in function
         (* only allow conversion of float pointers if source and target type are the same *)
         | Addr ({ vtype = TFloat(fkind, _); _}, _) as x when (match t with TFloat (fkind', _) when fkind = fkind' -> true | _ -> false) -> x
-          (* do not allow conversion from/to float pointers*)
+        (* do not allow conversion from/to float pointers*)
         | Addr ({ vtype = TFloat(_); _}, _) -> UnknownPtr
         | _ when (match t with TFloat _ -> true | _ -> false) -> UnknownPtr
         | Addr ({ vtype = TVoid _; _} as v, offs) when not (Cilfacade.isCharType t) -> (* we had no information about the type (e.g. malloc), so we add it; ignore for casts to char* since they're special conversions (N1570 6.3.2.3.7) *)
@@ -914,7 +914,22 @@ struct
         begin
           let l', o' = shift_one_over l o in
           let x = zero_init_calloced_memory orig x t in
-          mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
+          (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
+        let do_strong_update =
+            begin match v with
+            | (Var var, _) ->
+              let blob_size_opt = ID.to_int s in
+              not @@ ask.f (Q.IsMultiple var)
+              && not @@ Cil.isVoidType t      (* Size of value is known *)
+              && Option.is_some blob_size_opt (* Size of blob is known *)
+              && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.alignOf_int t)
+            | _ -> false
+            end
+          in
+          if do_strong_update then
+            `Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
+          else
+            mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
         end
       | `Thread _, _ ->
         (* hack for pthread_t variables *)

src/domains/lattice.ml

@@ -580,8 +580,8 @@ struct
 
   let bot () = 0
   let is_bot x = x = 0
-  let top () = P.n - 1
-  let is_top x = x = P.n - 1
+  let top () = P.n () - 1
+  let is_top x = x = P.n () - 1
 
   let leq x y = x <= y
   let join x y = max x y

src/domains/printable.ml

@@ -463,7 +463,7 @@ struct
 end
 
 module type ChainParams = sig
-  val n: int
+  val n: unit -> int
   val names: int -> string
 end
 
@@ -477,7 +477,7 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (P.names x)
   let to_yojson x = `String (P.names x)
 
-  let arbitrary () = QCheck.int_range 0 (P.n - 1)
+  let arbitrary () = QCheck.int_range 0 (P.n () - 1)
   let relift x = x
 end
 

src/util/options.schema.json

@@ -749,6 +749,12 @@
                 "kmalloc", "__kmalloc", "usb_alloc_urb", "__builtin_alloca",
                 "kzalloc"
               ]
+            },
+            "unique_address_count": {
+                "title": "ana.malloc.unique_address_count",
+                "description": "Number of unique memory addresses allocated for each malloc node.",
+                "type": "integer",
+                "default": 0
             }
           },
           "additionalProperties": false

src/witness/observerAnalysis.ml

@@ -24,7 +24,7 @@ struct
   module ChainParams =
   struct
     (* let n = List.length Arg.path *)
-    let n = -1
+    let n () = -1
     let names x = "state " ^ string_of_int x
   end
   module D = Lattice.Flat (Printable.Chain (ChainParams)) (Printable.DefaultNames)

src/witness/yamlWitness.ml

@@ -194,7 +194,7 @@ struct
 
   module ChainParams =
   struct
-    let n = max_result - 1
+    let n () = max_result - 1
     let names i = show_result (Option.get (result_of_enum i))
   end
   include Lattice.Chain (ChainParams)