From 73bf6fee56c6f4fe0114b677efa80369ee80654c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 17 Nov 2023 12:07:43 +0200
Subject: [PATCH] Fix region bullet escaping (issue #107)

---
 src/analyses/region.ml                        | 10 +++++++-
 src/cdomains/regionDomain.ml                  | 23 +++++++++++++++++--
 .../regression/09-regions/38-escape_malloc.c  |  4 ++--
 3 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 652526543c..5b10586aba 100644
--- a/src/analyses/region.ml
+++ b/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 ())
 
diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml
index b577e3499f..681eb79007 100644
--- a/src/cdomains/regionDomain.ml
+++ b/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
diff --git a/tests/regression/09-regions/38-escape_malloc.c b/tests/regression/09-regions/38-escape_malloc.c
index 9f5b44531e..c849d5bbe3 100644
--- a/tests/regression/09-regions/38-escape_malloc.c
+++ b/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;