[region] function domain

src/plugins/region/analysis.ml

@@ -22,27 +22,20 @@
 
 open Cil_datatype
 
-type domain = {
-  pre: Memory.map ;
-  post: Memory.map ;
-  exit: Memory.map ;
-  stmt: Memory.map Stmt.Map.t ;
-}
-
 (* -------------------------------------------------------------------------- *)
 (* ---  Projectification                                                  --- *)
 (* -------------------------------------------------------------------------- *)
 
-module DOMAIN : Datatype.S with type t = domain =
+module DOMAIN : Datatype.S with type t = Code.domain =
   Datatype.Make
     (struct
-      type t = domain
+      type t = Code.domain
       include Datatype.Undefined
       let name = "Region.Analysis.MEMORY"
       let mem_project = Datatype.never_any_project
       let reprs =
         let m = Memory.create () in
-        [{ pre = m; post = m; exit = m; stmt = Stmt.Map.empty }]
+        Code.[{ map = m; body = Stmt.Map.empty ; spec = Property.Map.empty }]
     end)
 
 module STATE = State_builder.Hashtbl(Kernel_function.Hashtbl)(DOMAIN)
@@ -56,6 +49,12 @@ module STATE = State_builder.Hashtbl(Kernel_function.Hashtbl)(DOMAIN)
 (* ---  Memoized Access                                                   --- *)
 (* -------------------------------------------------------------------------- *)
 
-let get kf = STATE.find kf
+let domain kf =
+  try STATE.find kf with Not_found ->
+    Options.feedback ~ontty:`Transient "Function %a" Kernel_function.pretty kf ;
+    let domain = Code.domain kf in
+    STATE.add kf domain ; domain
+
+let compute kf = ignore (domain kf)
 
 (* -------------------------------------------------------------------------- *)

src/plugins/region/analysis.mli

@@ -21,13 +21,9 @@
 (**************************************************************************)
 
 open Cil_types
-open Cil_datatype
 
-type domain = {
-  pre: Memory.map ;
-  post: Memory.map ;
-  exit: Memory.map ;
-  stmt: Memory.map Stmt.Map.t ;
-}
+(** Memoized *)
+val domain : kernel_function -> Code.domain
 
-val get : kernel_function -> domain
+(** Memoized *)
+val compute : kernel_function -> unit

src/plugins/region/code.ml

@@ -208,3 +208,27 @@ and block (r:rmap) (m:map) (b:block) =
   List.iter (stmt r m) b.bstmts
 
 (* -------------------------------------------------------------------------- *)
+(* --- Function                                                           --- *)
+(* -------------------------------------------------------------------------- *)
+
+type domain = {
+  map : map ;
+  body : map Stmt.Map.t ;
+  spec : map Property.Map.t ;
+}
+
+let domain kf =
+  let m = Memory.create () in
+  let r = ref Stmt.Map.empty in
+  begin
+    try
+      let fundec = Kernel_function.get_definition kf in
+      block r m fundec.sbody ;
+    with Kernel_function.No_Definition -> ()
+  end ; {
+    map = m ;
+    body = !r ;
+    spec = Property.Map.empty ;
+  }
+
+(* -------------------------------------------------------------------------- *)

src/plugins/region/code.mli

@@ -28,3 +28,11 @@ val lval : map -> stmt -> lval -> node
 val exp : map -> stmt -> exp -> node option
 val instr : map -> stmt -> instr -> unit
 val stmt : map Stmt.Map.t ref -> map -> stmt -> unit
+
+type domain = {
+  map : map ;
+  body : map Stmt.Map.t ;
+  spec : map Property.Map.t ;
+}
+
+val domain : kernel_function -> domain

src/plugins/region/register.ml

@@ -31,11 +31,7 @@ let main () =
     begin
       Ast.compute () ;
       R.feedback "Analyzing regions" ;
-      Globals.Functions.iter
-        begin fun (kf: Kernel_function.t) ->
-          R.feedback ~ontty:`Transient
-            "Function %a" Kernel_function.pretty kf
-        end ;
+      Globals.Functions.iter Analysis.compute ;
     end
 
 let () = Boot.Main.extend main