Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Handling escaped variables in region analysis #989

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from
Draft

Handling escaped variables in region analysis #989

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
ab91237
Handle pthread arg in region analysis
vesalvojdani Feb 14, 2023
9ea11c7
Remove the special treatment for RegMap empty values (dangerous!)
vesalvojdani Feb 14, 2023
a79065a
Make region analysis use escape information.
vesalvojdani Feb 14, 2023
e6fbd23
Force thread arguments to be added, as they will escape, but have not…
vesalvojdani Feb 14, 2023
f020dde
Fix indent (rm begin/end)
vesalvojdani Feb 14, 2023
d26f8fb
Merge branch 'master' into region-escape
sim642 Nov 17, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 31 additions & 23 deletions src/analyses/region.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,18 +23,19 @@ struct
include StdV
end

let regions exp part st : Mval.Exp.t list =
match st with
let regions ctx exp part : Mval.Exp.t list =
match ctx.local with
| `Lifted reg ->
let ev = Reg.eval_exp exp in
Reg.related_globals ev (part,reg)
let ask = Analyses.ask_of_ctx ctx in
let ev = Reg.eval_exp ask exp in
Reg.related_globals ask ev (part,reg)
| `Top -> Messages.info ~category:Unsound "Region state is broken :("; []
| `Bot -> []

let is_bullet exp part st : bool =
match st with
let is_bullet ctx exp part : bool =
match ctx.local with
| `Lifted reg ->
begin match Reg.eval_exp exp with
begin match Reg.eval_exp (Analyses.ask_of_ctx ctx) exp with
| Some (_,v,_) -> (try RegionDomain.RS.is_single_bullet (RegMap.find v reg) with Not_found -> false)
| _ -> false
end
Expand All @@ -43,18 +44,18 @@ struct

let get_region ctx e =
let regpart = ctx.global () in
if is_bullet e regpart ctx.local then
if is_bullet ctx e regpart then
None
else
Some (regions e regpart ctx.local)
Some (regions ctx e regpart)

(* queries *)
let query ctx (type a) (q: a Queries.t): a Queries.result =
match q with
| Queries.Regions e ->
let regpart = ctx.global () in
if is_bullet e regpart ctx.local then Queries.Result.bot q (* TODO: remove bot *) else
let ls = List.fold_right Queries.LS.add (regions e regpart ctx.local) (Queries.LS.empty ()) in
if is_bullet ctx e regpart then Queries.Result.bot q (* TODO: remove bot *) else
let ls = List.fold_right Queries.LS.add (regions ctx e regpart) (Queries.LS.empty ()) in
ls
| _ -> Queries.Result.top q

Expand All @@ -64,11 +65,13 @@ struct
include Printable.Option (Lvals) (struct let name = "no region" end)
let name () = "region"
let may_race r1 r2 = match r1, r2 with
(* Fresh memory does not race: *)
| None, _
| _, None -> false
(* TODO: Should it happen in the first place that RegMap has empty value? Happens in 09-regions/34-escape_rc *)
| Some r1, _ when Lvals.is_empty r1 -> true
| _, Some r2 when Lvals.is_empty r2 -> true
(* The following cases are needed if RegMap has empty values, due to bugs.
When not handling escape, 09-regions/34-escape_rc would fail without this:
| Some r1, _ when Lvals.is_empty r1 -> true
| _, Some r2 when Lvals.is_empty r2 -> true *)
| Some r1, Some r2 when Lvals.disjoint r1 r2 -> false
| _, _ -> true
let should_print r = match r with
Expand All @@ -90,7 +93,7 @@ struct
match ctx.local with
| `Lifted reg ->
let old_regpart = ctx.global () in
let regpart, reg = Reg.assign lval rval (old_regpart, reg) in
let regpart, reg = Reg.assign (Analyses.ask_of_ctx ctx) lval rval (old_regpart, reg) in
if not (RegPart.leq regpart old_regpart) then
ctx.sideg () regpart;
`Lifted reg
Expand All @@ -110,7 +113,7 @@ struct
let regpart, reg = match exp with
| Some exp ->
let module BS = (val Base.get_main ()) in
Reg.assign (BS.return_lval ()) exp (old_regpart, reg)
Reg.assign (Analyses.ask_of_ctx ctx) (BS.return_lval ()) exp (old_regpart, reg)
| None -> (old_regpart, reg)
in
let regpart, reg = Reg.kill_vars locals (Reg.remove_vars locals (regpart, reg)) in
Expand All @@ -128,7 +131,7 @@ struct
in
match ctx.local with
| `Lifted reg ->
let f x r reg = Reg.assign (var x) r reg in
let f x r reg = Reg.assign (Analyses.ask_of_ctx ctx) (var x) r reg in
let old_regpart = ctx.global () in
let regpart, reg = fold_right2 f fundec.sformals args (old_regpart,reg) in
if not (RegPart.leq regpart old_regpart) then
Expand All @@ -141,18 +144,17 @@ struct

let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
match au with
| `Lifted reg -> begin
| `Lifted reg ->
let old_regpart = ctx.global () in
let module BS = (val Base.get_main ()) in
let regpart, reg = match lval with
| None -> (old_regpart, reg)
| Some lval -> Reg.assign lval (AddrOf (BS.return_lval ())) (old_regpart, reg)
| Some lval -> Reg.assign (Analyses.ask_of_ctx ctx) lval (AddrOf (BS.return_lval ())) (old_regpart, reg)
in
let regpart, reg = Reg.remove_vars [BS.return_varinfo ()] (regpart, reg) in
if not (RegPart.leq regpart old_regpart) then
ctx.sideg () regpart;
`Lifted reg
end
| _ -> au

let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
Expand All @@ -163,7 +165,7 @@ struct
| `Lifted reg, Some lv ->
let old_regpart = ctx.global () in
(* TODO: should realloc use arg region if failed/in-place? *)
let regpart, reg = Reg.assign_bullet lv (old_regpart, reg) in
let regpart, reg = Reg.assign_bullet (Analyses.ask_of_ctx ctx) lv (old_regpart, reg) in
if not (RegPart.leq regpart old_regpart) then
ctx.sideg () regpart;
`Lifted reg
Expand All @@ -175,8 +177,14 @@ struct
let startstate v =
`Lifted (RegMap.bot ())

let threadenter ctx ~multiple lval f args =
[`Lifted (RegMap.bot ())]
let threadenter ctx ~multiple lval f args: D.t list =
let fd = Cilfacade.find_varinfo_fundec f in
match args, fd.sformals with
| [exp], [param] ->
(* The parameter may not have escaped here (for the first thread). *)
let reg = Reg.assign ~thread_arg:true (Analyses.ask_of_ctx ctx) (var param) exp (ctx.global (), RegMap.bot ()) in
[`Lifted (snd reg)]
| _ -> [`Lifted (RegMap.bot ())]
let threadspawn ctx ~multiple lval f args fctx = ctx.local

let exitstate v = `Lifted (RegMap.bot ())
Expand Down
22 changes: 10 additions & 12 deletions src/cdomains/regionDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,8 +105,6 @@ struct

let closure p m = RegMap.map (RegPart.closure p) m

let is_global (v,fd) = v.vglob

let remove v (p,m) = p, RegMap.remove (v, `NoOffset) m
let remove_vars (vs: varinfo list) (cp:t): t =
List.fold_right remove vs cp
Expand All @@ -129,7 +127,7 @@ struct
| _ -> kill x st

type eval_t = (bool * elt * F.t) option
let eval_exp exp: eval_t =
let eval_exp (ask: Queries.ask) exp: eval_t =
let offsornot offs = if (get_bool "exp.region-offsets") then F.of_cil offs else `NoOffset in
(* The intuition for the offset computations is that we keep the static _suffix_ of an
* access path. These can be used to partition accesses when fields do not overlap.
Expand Down Expand Up @@ -171,11 +169,11 @@ struct
let p = RegPart.add s p in
p, closure p m

let assign (lval: lval) (rval: exp) (st: t): t =
let assign ?(thread_arg=false) (ask: Queries.ask) (lval: lval) (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 (Lval lval), eval_exp rval with
match eval_exp ask (Lval lval), eval_exp ask rval with
(* TODO: should offs_x matter? *)
| Some (deref_x, x,offs_x), Some (deref_y,y,offs_y) ->
if VF.equal x y then st else
Expand All @@ -185,7 +183,7 @@ struct
| `Right () -> `Right ()
)
in
match is_global x, deref_x, is_global y with
match BaseUtil.is_global ask (fst x), deref_x, BaseUtil.is_global ask (fst y) || thread_arg with
| false, false, true ->
p, RegMap.add x (append_offs_y (RegPart.closure p (RS.single_vf y))) m
| false, false, false ->
Expand All @@ -206,29 +204,29 @@ struct
| Var x, NoOffset -> update x rval st
| _ -> st
end else
match eval_exp (Lval lval) with
match eval_exp ask (Lval lval) with
| Some (false, (x,_),_) -> remove x st
| _ -> st

let assign_bullet lval (p,m:t):t =
match eval_exp (Lval lval) with
let assign_bullet ask lval (p,m:t):t =
match eval_exp ask (Lval lval) with
| Some (_,x,_) -> p, RegMap.add x RS.single_bullet m
| _ -> p,m

let related_globals (deref_vfd: eval_t) (p,m: t): elt list =
let related_globals (ask: Queries.ask) (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
| Some (true, vfd, os) ->
let vfd_class =
if is_global vfd then
if BaseUtil.is_global ask (fst vfd) then
RegPart.find_class (VFB.of_vf vfd) p
else
RegMap.find vfd m
in
(* Messages.warn ~msg:("ok? "^sprint 80 (V.pretty () (fst vfd)++F.pretty () (snd vfd))) (); *)
List.map (add_o os) (RS.to_vf_list vfd_class)
| Some (false, vfd, os) ->
if is_global vfd then [vfd] else []
if BaseUtil.is_global ask (fst vfd) then [vfd] else []
| None -> Messages.info ~category:Unsound "Access to unknown address could be global"; []
end

Expand Down
Loading