Minimal write-only restarting is insufficient: add ana.malloc.include-node

src/analyses/mallocWrapperAnalysis.ml

@@ -13,19 +13,27 @@ struct
       let bot_name = "Unreachable node"
     end)
 
-  module Node = struct
-    include Node
+  module NodeFundec =
+  struct
+    include Printable.Either (Node) (CilType.Fundec)
+
     (* Description that gets appended to the varinfo-name in user output. *)
-    let describe_varinfo (v: varinfo) node =
-      let loc = UpdateCil.getLoc node in
+    let describe_varinfo (v: varinfo) node_fundec =
+      let loc =
+        match node_fundec with
+        | `Left node -> UpdateCil.getLoc node
+        | `Right fundec -> fundec.svar.vdecl
+      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 node_fundec =
+      match node_fundec with
+      | `Left (Node.Statement s) -> "(alloc@sid:" ^ (string_of_int s.sid) ^ ")"
+      | `Left _ -> failwith "A function entry or return node can not be the node after a malloc"
+      | `Right fundec -> "(alloc@" ^ fundec.svar.vname ^ ")"
   end
 
-  module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(Node)
+  module NodeFundecVarinfoMap = RichVarinfo.BiVarinfoMap.Make(NodeFundec)
   let name () = "mallocWrapper"
   module D = PL
   module C = D
@@ -67,31 +75,42 @@ struct
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
-  type marshal = NodeVarinfoMap.marshal
+  type marshal = NodeFundecVarinfoMap.marshal
 
-  let get_heap_var = NodeVarinfoMap.to_varinfo
+  let get_heap_var = NodeFundecVarinfoMap.to_varinfo
   let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Queries.result =
     match q with
     | Q.HeapVar ->
       let node = match ctx.local with
         | `Lifted vinfo -> vinfo
         | _ -> ctx.node
       in
-      let var = get_heap_var node in
-      var.vdecl <- UpdateCil.getLoc node; (* TODO: does this do anything bad for incremental? *)
+      let node_fundec =
+        if get_bool "ana.malloc.include-node" then
+          `Left node
+        else
+          `Right (Node.find_fundec node)
+      in
+      let loc =
+        match node_fundec with
+        | `Left node -> UpdateCil.getLoc node
+        | `Right fundec -> fundec.svar.vdecl
+      in
+      let var = get_heap_var node_fundec in
+      var.vdecl <- loc; (* TODO: does this do anything bad for incremental? *)
       `Lifted var
     | Q.IsHeapVar v ->
-      NodeVarinfoMap.mem_varinfo v
+      NodeFundecVarinfoMap.mem_varinfo v
     | Q.IsMultiple v ->
-      NodeVarinfoMap.mem_varinfo v
+      NodeFundecVarinfoMap.mem_varinfo v
     | _ -> Queries.Result.top q
 
   let init marshal =
     List.iter (fun wrapper -> Hashtbl.replace wrappers wrapper ()) (get_string_list "ana.malloc.wrappers");
-    NodeVarinfoMap.unmarshal marshal
+    NodeFundecVarinfoMap.unmarshal marshal
 
   let finalize () =
-    NodeVarinfoMap.marshal ()
+    NodeFundecVarinfoMap.marshal ()
 end
 
 let _ =

src/solvers/td3.ml

@@ -54,8 +54,8 @@ module WP =
 
     let print_data data str =
       if GobConfig.get_bool "dbg.verbose" then
-        Printf.printf "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n"
-          str (HM.length data.rho) (HM.length data.stable) (HM.length data.infl) (HM.length data.wpoint) (HM.length data.side_dep) (HM.length data.side_infl)
+        Printf.printf "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|rho_write|=%d\n"
+          str (HM.length data.rho) (HM.length data.stable) (HM.length data.infl) (HM.length data.wpoint) (HM.length data.side_dep) (HM.length data.side_infl) (HM.length data.rho_write)
 
     let exists_key f hm = HM.fold (fun k _ a -> a || f k) hm false
 
@@ -143,9 +143,9 @@ module WP =
       let prev_dep_vals = HM.create 10 in
 
       let () = print_solver_stats := fun () ->
-        Printf.printf "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n"
-          (HM.length rho) (HM.length called) (HM.length stable) (HM.length infl) (HM.length wpoint) (HM.length side_dep) (HM.length side_infl);
-        print_context_stats rho
+          Printf.printf "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|rho_write|=%d\n"
+            (HM.length rho) (HM.length called) (HM.length stable) (HM.length infl) (HM.length wpoint) (HM.length side_dep) (HM.length side_infl) (HM.length rho_write);
+          print_context_stats rho
       in
 
       if GobConfig.get_bool "incremental.load" then print_data data "Loaded data for incremental analysis";
@@ -722,6 +722,7 @@ module WP =
         print_endline "Removing data for changed and removed functions...";
         let delete_marked s = HM.iter (fun k _ -> HM.remove s k) marked_for_deletion in
         delete_marked rho;
+        delete_marked rho_write;
         delete_marked infl;
         delete_marked wpoint;
 
@@ -813,6 +814,7 @@ module WP =
         delete_marked stable;
         delete_marked side_dep;
         delete_marked side_infl;
+        delete_marked superstable;
         print_data data "Data after clean-up";
 
         (* TODO: reluctant doesn't call destabilize on removed functions or old copies of modified functions (e.g. after removing write), so those globals don't get restarted *)
@@ -979,6 +981,7 @@ module WP =
       (* restart write-only *)
       HM.iter (fun x w ->
           HM.iter (fun y d ->
+              (* ignore (Pretty.printf "rho_write restart %a\n" S.Var.pretty_trace y); *)
               HM.replace rho y (S.Dom.bot ());
             ) w
         ) rho_write;

src/util/options.schema.json

@@ -779,6 +779,13 @@
                 "kmalloc", "__kmalloc", "usb_alloc_urb", "__builtin_alloca",
                 "kzalloc"
               ]
+            },
+            "include-node" : {
+              "title": "ana.malloc.include-node",
+              "description":
+                "Whether the node at which memory is allocated is part of its variable ID",
+              "type": "boolean",
+              "default" : true
             }
           },
           "additionalProperties": false

tests/incremental/13-restart-write/04-malloc-node.c

@@ -0,0 +1,21 @@
+#include <pthread.h>
+#include <assert.h>
+
+void *t_fun(void *arg) {
+  int *iarg = (int*) arg;
+  *iarg = 1;
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  int *iarg;
+
+  for (int i = 0; i < 10; i++) {
+    iarg = malloc(sizeof(int));
+    *iarg = 0;
+    pthread_create(&id, NULL, t_fun, (void*) iarg);
+  }
+
+  return 0;
+}

tests/incremental/13-restart-write/04-malloc-node.json

@@ -0,0 +1,17 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        }
+    },
+    "ana": {
+        "thread": {
+            "include-node": false
+        },
+        "malloc": {
+            "include-node": false
+        }
+    }
+}

tests/incremental/13-restart-write/04-malloc-node.patch

@@ -0,0 +1,13 @@
+diff --git tests/incremental/13-restart-write/04-malloc-node.c tests/incremental/13-restart-write/04-malloc-node.c
+index 87bbc0f14..3cd6dc5c7 100644
+--- tests/incremental/13-restart-write/04-malloc-node.c
++++ tests/incremental/13-restart-write/04-malloc-node.c
+@@ -11,6 +11,8 @@ int main() {
+   pthread_t id;
+   int *iarg;
+
++  assert(1);
++
+   for (int i = 0; i < 10; i++) {
+     iarg = malloc(sizeof(int));
+     *iarg = 0;

tests/incremental/13-restart-write/05-race-call-remove.c

@@ -0,0 +1,20 @@
+#include <pthread.h>
+#include <assert.h>
+
+int g;
+
+void *t_fun(void *arg) {
+  g++; // RACE!
+  return NULL;
+}
+
+void foo() {
+  g++; // RACE!
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  foo();
+  return 0;
+}

tests/incremental/13-restart-write/05-race-call-remove.json

@@ -0,0 +1,14 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        }
+    },
+    "ana": {
+        "thread": {
+            "include-node": false
+        }
+    }
+}

tests/incremental/13-restart-write/05-race-call-remove.patch

@@ -0,0 +1,25 @@
+diff --git tests/incremental/13-restart-write/05-race-call-remove.c tests/incremental/13-restart-write/05-race-call-remove.c
+index cf9f5c713..20e09db1a 100644
+--- tests/incremental/13-restart-write/05-race-call-remove.c
++++ tests/incremental/13-restart-write/05-race-call-remove.c
+@@ -4,17 +4,16 @@
+ int g;
+
+ void *t_fun(void *arg) {
+-  g++; // RACE!
++  g++; // NORACE (unique thread)
+   return NULL;
+ }
+
+ void foo() {
+-  g++; // RACE!
++  g++; // NORACE
+ }
+
+ int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+-  foo();
+   return 0;
+ }
+\ No newline at end of file