Skip to content

Commit

Permalink
Fix region bullet escaping (issue #107)
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Nov 17, 2023
1 parent 9202385 commit 73bf6fe
Show file tree
Hide file tree
Showing 3 changed files with 32 additions and 5 deletions.
10 changes: 9 additions & 1 deletion src/analyses/region.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ())

Expand Down
23 changes: 21 additions & 2 deletions src/cdomains/regionDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/09-regions/38-escape_malloc.c
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand All @@ -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;
Expand Down

0 comments on commit 73bf6fe

Please sign in to comment.