Skip to content

Commit

Permalink
Remove regpart
Browse files Browse the repository at this point in the history
  • Loading branch information
@karoliineh
karoliineh committed Sep 18, 2023
1 parent 4310c6e commit e5c0daa
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 118 deletions.
89 changes: 22 additions & 67 deletions src/analyses/region.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,23 +15,15 @@ struct
include Analyses.DefaultSpec

module D = RegionDomain.RegionDom
module G = RegPart
module G = Lattice.Unit
module C = D
module V =
struct
include Printable.UnitConf (struct let name = "partitions" end)
include StdV
end

let regions exp part st =
match st with
| `Lifted reg ->
let ev = Reg.eval_exp exp in
Reg.related_globals ev (part,reg)
| `Top -> Messages.info ~category:Unsound "Region state is broken :("; RegionDomain.RS.empty ()
| `Bot -> RegionDomain.RS.empty ()

let is_bullet exp part st : bool =
let is_bullet exp st : bool =
match st with
| `Lifted reg ->
begin match Reg.eval_exp exp with
Expand All @@ -41,20 +33,9 @@ struct
| `Top -> false
| `Bot -> true

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

(* 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
regions e regpart ctx.local
| _ -> Queries.Result.top q

module Lvals = SetDomain.Make (Mval.Exp)
Expand Down Expand Up @@ -87,34 +68,24 @@ struct
(* transfer functions *)
let assign ctx (lval:lval) (rval:exp) : D.t =
match ctx.local with
| `Lifted reg ->
let old_regpart = ctx.global () in
let regpart, reg = Reg.assign lval rval (old_regpart, reg) in
if not (RegPart.leq regpart old_regpart) then
ctx.sideg () regpart;
`Lifted reg
| `Lifted reg -> `Lifted (Reg.assign lval rval reg)
| x -> x

let branch ctx (exp:exp) (tv:bool) : D.t =
ctx.local
let branch ctx (exp:exp) (tv:bool) : D.t = ctx.local

let body ctx (f:fundec) : D.t =
ctx.local
let body ctx (f:fundec) : D.t = ctx.local

let return ctx (exp:exp option) (f:fundec) : D.t =
let locals = f.sformals @ f.slocals in
match ctx.local with
| `Lifted reg ->
let old_regpart = ctx.global () in
let regpart, reg = match exp with
let reg = match exp with
| Some exp ->
let module BS = (val Base.get_main ()) in
Reg.assign (BS.return_lval ()) exp (old_regpart, reg)
| None -> (old_regpart, reg)
Reg.assign (BS.return_lval ()) exp reg
| None -> reg
in
let regpart, reg = Reg.kill_vars locals (Reg.remove_vars locals (regpart, reg)) in
if not (RegPart.leq regpart old_regpart) then
ctx.sideg () regpart;
let reg = Reg.kill_vars locals (Reg.remove_vars locals reg) in
`Lifted reg
| x -> x

Expand All @@ -128,10 +99,7 @@ struct
match ctx.local with
| `Lifted reg ->
let f x r reg = Reg.assign (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
ctx.sideg () regpart;
let reg = fold_right2 f fundec.sformals args reg in
[ctx.local, `Lifted reg]
| x -> [x,x]

Expand All @@ -141,16 +109,13 @@ 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
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)
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
let module BS = (val Base.get_main ()) in
let reg = match lval with
| None -> reg
| Some lval -> Reg.assign lval (AddrOf (BS.return_lval ())) reg
in
let reg = Reg.remove_vars [BS.return_varinfo ()] reg in
`Lifted reg
end
| _ -> au

Expand All @@ -160,28 +125,18 @@ struct
| Malloc _ | Calloc _ | Realloc _ -> begin
match ctx.local, lval with
| `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
if not (RegPart.leq regpart old_regpart) then
ctx.sideg () regpart;
let reg = Reg.assign_bullet lv reg in
`Lifted reg
| _ -> ctx.local
end
| _ ->
ctx.local
| _ -> ctx.local

let startstate v =
`Lifted (RegMap.bot ())

let threadenter ctx lval f args =
[`Lifted (RegMap.bot ())]
let startstate v = `Lifted (RegMap.bot ())
let threadenter ctx lval f args = [`Lifted (RegMap.bot ())]
let threadspawn ctx lval f args fctx = ctx.local

let exitstate v = `Lifted (RegMap.bot ())

let name () = "region"
end

let _ =
MCP.register_analysis (module Spec : MCPSpec)
let _ = MCP.register_analysis (module Spec : MCPSpec)
77 changes: 26 additions & 51 deletions src/cdomains/regionDomain.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,25 +77,16 @@ end

module Reg =
struct
include Lattice.Prod (RegPart) (RegMap)
include RegMap
type set = RS.t
type elt = VF.t

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

let kill x (p,m:t): t =
p, RegMap.map (RS.kill x) m

let remove v m = RegMap.remove (v, `NoOffset) m
let remove_vars (vs: varinfo list) (cp:t): t = List.fold_right remove vs cp
let kill x m: t = RegMap.map (RS.kill x) m
let kill_vars vars st = List.fold_right kill vars st

let replace x exp (p,m:t): t =
RegPart.map (RS.replace x exp) p, RegMap.map (RS.replace x exp) m
let replace x exp m: t = RegMap.map (RS.replace x exp) m

let update x rval st =
match rval with
Expand Down Expand Up @@ -135,78 +126,62 @@ 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 (s:set) llist m: 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
p, RegMap.add_list_set llist RS.single_bullet m
RegMap.add_list_set llist RS.single_bullet m
else
RegPart.add x p, RegMap.add_list_set ys x m
RegMap.add_list_set ys x m
else
let p = RegPart.add s p in
p, closure p m
m

let assign (lval: lval) (rval: exp) (st: t): t =
let assign (lval: lval) (rval: exp) reg: 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
(* 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
let (p,m) = st in begin
if VF.equal x y then reg else
let m = reg in begin
let append_offs_y = RS.map (function
| `Left () -> `Left ()
| `Right () -> `Right ()
)
in
match is_global x, deref_x, is_global y with
| false, false, true ->
p, RegMap.add x (append_offs_y (RegPart.closure p (RS.single_vf y))) m
RegMap.add x (append_offs_y (RS.single_vf y)) reg
| false, false, false ->
p, RegMap.add x (append_offs_y (RegMap.find y m)) m
RegMap.add x (append_offs_y (RegMap.find y m)) m
(* TODO: use append_offs_y also in the following cases? *)
| false, true , true ->
add_set (RS.join (RegMap.find x m) (RS.single_vf ())) [x] st
add_set (RS.join (RegMap.find x m) (RS.single_vf ())) [x] reg
| false, true , false ->
add_set (RS.join (RegMap.find x m) (RegMap.find y m)) [x;y] st
add_set (RS.join (RegMap.find x m) (RegMap.find y m)) [x;y] reg
| true , _ , true ->
add_set (RS.join (RS.single_vf ()) (RS.single_vf ())) [] st
add_set (RS.join (RS.single_vf ()) (RS.single_vf ())) [] reg
| true , _ , false ->
add_set (RS.join (RS.single_vf ()) (RegMap.find y m)) [y] st
add_set (RS.join (RS.single_vf ()) (RegMap.find y m)) [y] reg
end
| _ -> st
| _ -> reg
end else if isIntegralType t then begin
match lval with
| Var x, NoOffset -> update x rval st
| _ -> st
| Var x, NoOffset -> update x rval reg
| _ -> reg
end else
match eval_exp (Lval lval) with
| Some (false, (x,_),_) -> remove x st
| _ -> st
| Some (false, (x,_),_) -> remove x reg
| _ -> reg

let assign_bullet lval (p,m:t):t =
let assign_bullet lval m: t =
match eval_exp (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) =
match deref_vfd with
| Some (true, vfd, os) ->
let vfd_class =
if is_global 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))) (); *)
vfd_class
| Some (false, vfd, os) ->
if is_global vfd then RegPart.find_class (VFB.of_vf vfd) p else RS.empty ()
| None -> Messages.info ~category:Unsound "Access to unknown address could be global"; RS.empty ()
| Some (_,x,_) -> RegMap.add x RS.single_bullet m
| _ -> m
end

(* TODO: remove Lift *)
Expand Down

0 comments on commit e5c0daa

Please sign in to comment.