Make region analysis use escape information.

Author: vesalvojdani

src/analyses/region.ml

@@ -20,19 +20,20 @@ struct
     include StdV
   end
 
-  let regions exp part st : Lval.CilLval.t list =
-    match st with
+  let regions ctx exp part : Lval.CilLval.t list =
+    match ctx.local with
     | `Lifted reg ->
-      let ev = Reg.eval_exp exp in
+      let ask = Analyses.ask_of_ctx ctx in
+      let ev = Reg.eval_exp ask exp in
       let to_exp (v,f) = (v,Lval.Fields.to_offs' f) in
-      List.map to_exp (Reg.related_globals ev (part,reg))
+      List.map to_exp (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
@@ -41,18 +42,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
 
@@ -93,7 +94,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
@@ -113,7 +114,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
@@ -131,7 +132,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
@@ -146,7 +147,7 @@ struct
       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
@@ -163,7 +164,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
@@ -186,7 +187,7 @@ struct
     let fd = Cilfacade.find_varinfo_fundec f in
     match args, fd.sformals with
     | [exp], [param] -> 
-      let reg = Reg.assign (var param) exp (ctx.global (), RegMap.bot ()) in
+      let reg = Reg.assign (Analyses.ask_of_ctx ctx) (var param) exp (ctx.global (), RegMap.bot ()) in
       [`Lifted (snd reg)] 
     | _ -> [`Lifted (RegMap.bot ())]
   let threadspawn ctx lval f args fctx = ctx.local

src/cdomains/regionDomain.ml

@@ -116,8 +116,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,[]) m
   let remove_vars (vs: varinfo list) (cp:t): t =
     List.fold_right remove vs cp
@@ -140,7 +138,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.listify offs else [] in
     let rec do_offs deref def = function
       | Field (fd, offs) -> begin
@@ -170,7 +168,7 @@ struct
       | (Var x, NoOffset) when Goblintutil.is_blessed x.vtype <> None ->
         begin match Goblintutil.is_blessed x.vtype with
           | Some v -> Some (deref, (v,[]), [])
-          | _ when x.vglob -> Some (deref, (x, []), [])
+          | _ when BaseUtil.is_global ask x -> Some (deref, (x, []), [])
           | _ -> None
         end
       | (Var x, offs) -> do_offs deref (Some (deref, (x, offsornot offs), [])) offs
@@ -197,11 +195,11 @@ struct
       let p = RegPart.add s p in
       p, closure p m
 
-  let assign (lval: lval) (rval: exp) (st: t): t =
+  let assign (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
@@ -211,7 +209,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) with
             | false, false, true  ->
               p, RegMap.add x (append_offs_y (RegPart.closure p (RS.single_vf y))) m
             | false, false, false ->
@@ -232,29 +230,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,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