From 1c7016e9c3e991a06e9a0ccf7e2f3be1605662dd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 29 May 2024 17:10:13 +0200
Subject: [PATCH] [region] function domain

---
 src/plugins/region/analysis.ml  | 21 ++++++++++-----------
 src/plugins/region/analysis.mli | 12 ++++--------
 src/plugins/region/code.ml      | 24 ++++++++++++++++++++++++
 src/plugins/region/code.mli     |  8 ++++++++
 src/plugins/region/register.ml  |  6 +-----
 5 files changed, 47 insertions(+), 24 deletions(-)

diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml
index de7aae0ea8b..1cc735b099b 100644
--- a/src/plugins/region/analysis.ml
+++ b/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)
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/analysis.mli b/src/plugins/region/analysis.mli
index 51f263146c5..b9b7d7729a3 100644
--- a/src/plugins/region/analysis.mli
+++ b/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
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index 61315d1ef60..41a9563d90d 100644
--- a/src/plugins/region/code.ml
+++ b/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 ;
+  }
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/code.mli b/src/plugins/region/code.mli
index ee2e7b9aeca..1ae6e52fc2c 100644
--- a/src/plugins/region/code.mli
+++ b/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
diff --git a/src/plugins/region/register.ml b/src/plugins/region/register.ml
index 349df39bff2..54cd5cdd62b 100644
--- a/src/plugins/region/register.ml
+++ b/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
-- 
GitLab