diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml index de7aae0ea8b5ecfd4cfbcca92569752857ce8566..1cc735b099b60327566d7646d5230943a5087b56 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 51f263146c51610ba4ac49e7c67063d791593779..b9b7d7729a3b9b165bb97e6f88798b8ffb5b432c 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 61315d1ef60ed873aa92d7798ccb352767c5d530..41a9563d90d99c4cf0379e560a04174366bca765 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 ee2e7b9aecabc7fe920b26b46e3ab0351421442b..1ae6e52fc2cad0299423705efccb09c2267fc9af 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 349df39bff297a037ff7c91895e375c7adebeb16..54cd5cdd62b1d0f0a2e294a2b7ebce49a6390fca 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