Malloc uniqueness

src/analyses/mallocWrapperAnalysis.ml

@@ -3,8 +3,9 @@
 open Prelude.Ana
 open Analyses
 open GobConfig
+open ThreadIdDomain
 
-module Spec : Analyses.MCPSpec =
+module Spec () : Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
@@ -13,21 +14,61 @@ struct
       let bot_name = "Unreachable node"
     end)
 
-  module Node = struct
-    include Node
-    (* Description that gets appended to the varinfo-name in user output. *)
-    let describe_varinfo (v: varinfo) 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 Int.equal 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 Domain = struct
+    include Lattice.Prod (MallocCounter) (PL)
+
+    let join (counter1, node1) (counter2, node2) =
+      (MallocCounter.join counter1 counter2, node1)
+
+    let has_wrapper_node (_, wrapper_node) = not @@ PL.is_top wrapper_node
+
+    let get_count (counter, _) node = MallocCounter.find (`Lifted node) counter
+
+  end
+
+  module ThreadNode = struct
+    include Printable.Prod3 (ThreadIdDomain.ThreadLifted) (Node) (Chain)
+
+    (* Description that gets appended to the varinfo-name in user ouptut. *)
+    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 "(allocs@%s@%s(#%s))" (ThreadLifted.show t) (Node.show node) (Chain.show c)
+
   end
 
-  module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(Node)
+  module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)
   let name () = "mallocWrapper"
-  module D = PL
+
+  module D = Domain
   module C = D
 
   module Q = Queries
@@ -48,51 +89,73 @@ 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 counter, wrapper_node = ctx.local in
+    let new_counter =
+      if Hashtbl.mem wrappers f.svar.vname then
+        MallocCounter.add_malloc counter ctx.prev_node
+      else counter
+    in
+    let new_wrapper_node =
+      if Hashtbl.mem wrappers f.svar.vname then
+        if not @@ D.has_wrapper_node ctx.local then
+          (`Lifted ctx.prev_node) (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *)
+        else wrapper_node (* if an interesting callee is called by an interesting caller, then we remember the caller context *)
+      else PL.top () (* if an uninteresting callee is called, then we forget what was called before *)
+    in
+    let caller_ctx = (new_counter, wrapper_node) in
+    let callee_ctx = (new_counter, new_wrapper_node) in
+    [(caller_ctx, callee_ctx)]
 
   let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
-    ctx.local
+    D.join ctx.local au
 
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    ctx.local
+  let special (ctx: (D.t, G.t, C.t, V.t) ctx) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let counter, wrapper_node = ctx.local in
+    match LibraryFunctions.classify f.vname arglist with
+    | `Malloc _ | `Calloc _ | `Realloc _ -> (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 _, 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 var = get_heap_var (ctx.ask Q.CurrentThreadId, node, D.get_count ctx.local node) 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 =
+    Printexc.record_backtrace true;
     List.iter (fun wrapper -> Hashtbl.replace wrappers wrapper ()) (get_string_list "ana.malloc.wrappers");
     NodeVarinfoMap.unmarshal marshal
 
   let finalize () =
     NodeVarinfoMap.marshal ()
 end
 
+let after_config () =
+  MCP.register_analysis (module Spec ())
+
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  AfterConfig.register after_config

src/cdomains/valueDomain.ml

@@ -901,7 +901,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/util/options.schema.json

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

tests/regression/11-heap/03-threads_malloc_no_race.c

@@ -0,0 +1,35 @@
+// No race should be reported because thread1 and thread2 are both unique
+// and work with their own allocated memory
+
+#include <stdlib.h>
+#include <pthread.h>
+
+int *f()
+{
+    int *x = malloc(sizeof(int));
+    return x;
+}
+
+void *thread1(void *v)
+{
+    int *x = f();
+    (*x)++; // NORACE
+}
+
+void *thread2(void *v)
+{
+    int *x = f();
+    (*x)++; // NORACE
+}
+
+int main(int argc, char **argv)
+{
+	pthread_t tid1;
+	pthread_t tid2;
+
+    pthread_create(&tid1, NULL, thread1, NULL);
+    pthread_create(&tid2, NULL, thread2, NULL);
+
+    pthread_join(tid1, NULL);
+    pthread_join(tid2, NULL);
+}

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;
+}

tests/regression/11-heap/07-strong_updates.c

@@ -0,0 +1,25 @@
+// PARAM: --set ana.malloc.unique_address_count 2
+
+// Both variables x and y are unique and can be strongly (destructively) updated.
+
+#include <assert.h>
+#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));
+
+  *x = 0;
+  *y = 1;
+
+  *x = 2;
+  *y = 3;
+
+  assert (*x == 2);
+  assert (*y == 3);
+}

tests/regression/11-heap/08-no_strong_update.c

@@ -0,0 +1,25 @@
+// PARAM: --set ana.malloc.unique_address_count 1
+
+// Copied from 11/05. Here, variable y is not unique and cannot be strongly updated.
+
+#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;
+
+  *x = 2;
+  *y = 3;
+
+  assert (*x == 2);
+  assert (*y == 3); // UNKNOWN!
+}