Merge pull request #1247 from goblint/region-escape-svcomp

Fix region escaping in per-thread-array-init-race

src/analyses/region.ml

@@ -177,7 +177,15 @@ struct
 
   let threadenter ctx ~multiple lval f args =
     [`Lifted (RegMap.bot ())]
-  let threadspawn ctx ~multiple lval f args fctx = ctx.local
+  let threadspawn ctx ~multiple lval f args fctx =
+    match ctx.local with
+    | `Lifted reg ->
+      let old_regpart = ctx.global () in
+      let regpart, reg = List.fold_right Reg.assign_escape args (old_regpart, reg) in
+      if not (RegPart.leq regpart old_regpart) then
+        ctx.sideg () regpart;
+      `Lifted reg
+    | x -> x
 
   let exitstate v = `Lifted (RegMap.bot ())
 

src/cdomains/regionDomain.ml

@@ -157,13 +157,13 @@ struct
 
   (* This is the main logic for dealing with the bullet and finding it an
    * owner... *)
-  let add_set (s:set) llist (p,m:t): t =
+  let add_set ?(escape=false) (s:set) llist (p,m:t): t =
     if RS.has_bullet s then
       let f key value (ys, x) =
         if RS.has_bullet value then key::ys, RS.join value x else ys,x in
       let ys,x = RegMap.fold f m (llist, RS.remove_bullet s) in
       let x = RS.remove_bullet x in
-      if RS.is_empty x then
+      if not escape && RS.is_empty x then
         p, RegMap.add_list_set llist RS.single_bullet m
       else
         RegPart.add x p, RegMap.add_list_set ys x m
@@ -215,6 +215,25 @@ struct
     | Some (_,x,_) -> p, RegMap.add x RS.single_bullet m
     | _ -> p,m
 
+  (* Copied & modified from assign. *)
+  let assign_escape (rval: exp) (st: t): t =
+    (*    let _ = printf "%a = %a\n" (printLval plainCilPrinter) lval (printExp plainCilPrinter) rval in *)
+    let t = Cilfacade.typeOf rval in
+    if isPointerType t then begin (* TODO: this currently allows function pointers, e.g. in iowarrior, but should it? *)
+      match eval_exp rval with
+      (* TODO: should offs_x matter? *)
+      | Some (deref_y,y,offs_y) ->
+        let (p,m) = st in begin
+          match is_global y with
+          | true  ->
+            add_set ~escape:true (RS.single_vf y) [] st
+          | false  ->
+            add_set ~escape:true (RegMap.find y m) [y] st
+        end
+      | _ -> st
+    end else
+      st
+
   let related_globals (deref_vfd: eval_t) (p,m: t): elt list =
     let add_o o2 (v,o) = (v, F.add_offset o o2) in
     match deref_vfd with

tests/regression/09-regions/38-escape_malloc.c

@@ -9,7 +9,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 void *t_fun(void *arg) {
   int *p = (int *) arg;
   pthread_mutex_lock(&mutex1);
-  (*p)++; // TODO RACE!
+  (*p)++; // RACE!
   pthread_mutex_unlock(&mutex1);
   return NULL;
 }
@@ -20,7 +20,7 @@ int main(void) {
   // TODO: q escapes as region owner
   pthread_create(&id, NULL, t_fun, (void *) q);
   pthread_mutex_lock(&mutex2);
-  (*q)++; // TODO RACE!
+  (*q)++; // RACE!
   pthread_mutex_unlock(&mutex2);
   pthread_join (id, NULL);
   return 0;

tests/regression/09-regions/41-per-thread-array-init-race.c

@@ -0,0 +1,40 @@
+// PARAM: --set ana.activated[+] region --enable ana.sv-comp.functions
+// Per-thread array pointers passed via argument but initialized before thread create.
+// Extracted from silver searcher.
+#include <stdlib.h>
+#include <pthread.h>
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+extern int __VERIFIER_nondet_int();
+
+void *thread(void *arg) {
+  int *p = arg;
+  int i = *p; // RACE!
+  return NULL;
+}
+
+int main() {
+  int threads_total = __VERIFIER_nondet_int();
+  assume_abort_if_not(threads_total >= 0);
+
+  pthread_t *tids = malloc(threads_total * sizeof(pthread_t));
+  int *is = calloc(threads_total, sizeof(int));
+
+  // create threads
+  for (int i = 0; i < threads_total; i++) {
+    pthread_create(&tids[i], NULL, &thread, &is[i]); // may fail but doesn't matter
+    is[i] = i; // RACE!
+  }
+
+  // join threads
+  for (int i = 0; i < threads_total; i++) {
+    pthread_join(tids[i], NULL);
+  }
+
+  free(tids);
+  free(is);
+
+  return 0;
+}