diff --git a/src/analyses/region.ml b/src/analyses/region.ml index 261c51b178..9f3adb2795 100644 --- a/src/analyses/region.ml +++ b/src/analyses/region.ml @@ -15,7 +15,7 @@ struct include Analyses.DefaultSpec module D = RegionDomain.RegionDom - module G = RegPart + module G = Lattice.Unit module C = D module V = struct @@ -23,15 +23,7 @@ struct 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 @@ -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) @@ -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 @@ -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] @@ -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 @@ -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) diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml index 611a616d5d..e1dfa1eafa 100644 --- a/src/cdomains/regionDomain.ml +++ b/src/cdomains/regionDomain.ml @@ -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 @@ -135,29 +126,28 @@ 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 () @@ -165,48 +155,33 @@ struct 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 *)