Malloc uniqueness

src/analyses/base.ml

@@ -2428,8 +2428,10 @@ 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))));
+          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

src/analyses/libraryFunctions.ml

@@ -42,7 +42,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. *)
+  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,60 @@ 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.prev_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, f.vname with
+    | Malloc _, _ | Calloc _, _ | Realloc _, _ ->
+      let counter, wrapper_node = ctx.local in
+      (MallocCounter.add_malloc counter ctx.prev_node, wrapper_node)
+    | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ctx lval f args = [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
-        | _ -> ctx.node
+      let node = match wrapper_node with
+        | `Lifted wrapper_node -> wrapper_node
+        | _ -> ctx.prev_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 +140,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis (module Spec)

src/cdomains/arrayDomain.ml

@@ -458,7 +458,7 @@ struct
             (e,(xl,a,xr))
           else
             let left = if equals_zero i then Val.bot () else Val.join xl @@ Val.join
-              (match Q.may_be_equal ask e' i' with (* TODO: untested *)
+                  (match Q.may_be_equal ask e' i' with (* TODO: untested *)
               | false -> Val.bot()
               | _ -> xm) (* if e' may be equal to i', but e' may not be smaller than i' then we only need xm *)
               (
@@ -475,7 +475,7 @@ struct
               )
             in
             let right = if equals_maxIndex i then Val.bot () else  Val.join xr @@  Val.join
-              (match Q.may_be_equal ask e' i' with (* TODO: untested *)
+                  (match Q.may_be_equal ask e' i' with (* TODO: untested *)
               | false -> Val.bot()
               | _ -> xm)
 

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

@@ -872,7 +872,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/extract/pml_arinc.ml

@@ -17,7 +17,7 @@ let init ?(nproc=99) ?(nsema=99) ?(nevent=99) ?(nbboard=99) () = (* TODO better
   let nsema   = fst @@ var (Byte nsema) "nsema" in
   let nevent  = fst @@ var (Byte nevent) "nevent" in
   let nbboard = fst @@ var (Byte nbboard) "nbboard" in
-
+  
   (* Pml.do_; (* ppx_monadic: from now on ; is bind *) *)
   (* switched to ocaml-monadic because ppx_monadic was constraining us to ocaml <4.08, now have to use ;%bind instead of just ; and `let%bind x = e in` instead of `x <-- e;` *)
   (* Dropped ocaml-monadic and used let* syntax introduced in OCaml 4.08. Use `let* () = e in` instead of `e;%bind` *)

src/incremental/compareCIL.ml

@@ -137,7 +137,7 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
     with
       Not_found -> map
   in
-
+  
   let changes = empty_change_info () in
   global_typ_acc := [];
   let findChanges map global global_rename_mapping =

src/util/options.schema.json

@@ -735,6 +735,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)

tests/regression/11-heap/04-malloc_unique_addresses.c

@@ -0,0 +1,27 @@
+// PARAM: --set ana.malloc.unique_address_count 2
+
+// Copied from 29/07. Here, unique addresses are allocated for both x and y.
+// Therefore, it is not necessary to specify wrapper function.
+
+#include <stdlib.h>
+#include <stdint.h>
+
+void* myalloc(size_t s) {
+    return malloc(s);
+}
+
+int main() {
+  int* x = myalloc(sizeof(int));
+  int* y = myalloc(sizeof(int));
+  int *p;
+
+  *x = 0;
+  *y = 1;
+
+  assert(*x == 0);
+  assert(*y == 1);
+
+  p = x; x = y; y = p;
+  assert(*x == 1);
+  assert(*y == 0);
+}

tests/regression/11-heap/05-malloc_not_unique_address.c

@@ -0,0 +1,23 @@
+// PARAM: --set ana.malloc.unique_address_count 1
+
+// Copied from 11/05. Here, malloc will allocate an unique address for x only.
+
+#include <stdlib.h>
+#include <stdint.h>
+
+void* myalloc(size_t s) {
+    return malloc(s);
+}
+
+int main() {
+  int* x = myalloc(sizeof(int));
+  int* y = myalloc(sizeof(int));
+  int* z = myalloc(sizeof(int));
+
+  *x = 0;
+  *y = 1;
+  *z = 0;
+
+  assert(*x == 0);
+  assert(*y == 1); // UNKNOWN!
+}

tests/regression/11-heap/06-wrapper_plus_unique_addresses.c

@@ -0,0 +1,34 @@
+// PARAM: --set ana.malloc.wrappers "['myalloc2']" --set ana.malloc.unique_address_count 2
+
+
+// Copied from 02/21. Here, only the inner wrapper function is specified. This should tests
+// the combination of uniqueness analysis and malloc wrapper analysis.
+
+#include <stdlib.h>
+#include <assert.h>
+
+void *myalloc(size_t n) {
+  return malloc(n);
+}
+
+void *myalloc2(size_t n) {
+  return myalloc(n);
+}
+
+int main() {
+  int *x = myalloc2(sizeof(int));
+  int *y = myalloc2(sizeof(int));
+  int *p;
+
+  *x = 0;
+  *y = 1;
+
+  assert(*x == 0);
+  assert(*y == 1);
+
+  p = x; x = y; y = p;
+  assert(*x == 1);
+  assert(*y == 0);
+
+  return 0;
+}