From cd760e389252a82880910f3a8a4cd8c3f6b81f7b Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sat, 21 Dec 2024 00:53:35 +0100
Subject: [PATCH] [Eva] build the engine modules recursively
- the useful modules definitions are moved to Engine_sig
- the engine contains the modules circularly dependent on the
engine
- every module circularly dependent on the engine receive the Engine
as a functor parameter
- Analysis instanciate the Engine recursively
---
src/plugins/eva/engine/analysis.ml | 39 ++++++-----
src/plugins/eva/engine/analysis.mli | 19 ++----
src/plugins/eva/engine/compute_functions.ml | 68 +++++++++++---------
src/plugins/eva/engine/compute_functions.mli | 15 ++---
src/plugins/eva/engine/engine_sig.ml | 65 +++++++++++++++++++
src/plugins/eva/engine/transfer_stmt.ml | 29 ++-------
src/plugins/eva/engine/transfer_stmt.mli | 16 +----
7 files changed, 138 insertions(+), 113 deletions(-)
create mode 100644 src/plugins/eva/engine/engine_sig.ml
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index c3b9861d3fd..c55cb183796 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -78,28 +78,27 @@ module type Results = sig
end
module type S = sig
- include Abstractions.S_with_evaluation
+ include Engine_sig.S
include Results with type state := Dom.state
and type value := Val.t
and type location := Loc.location
end
-module type Analyzer = sig
- include S
- val compute_from_entry_point : kernel_function -> lib_entry:bool -> unit
- (* val compute_from_init_state: kernel_function -> Dom.t -> unit *)
-end
-
-
module Make (Abstract: Abstractions.S) = struct
- module Abstract = struct
+ module rec Engine : Engine_sig.S
+ with module Ctx = Abstract.Ctx
+ and module Val = Abstract.Val
+ and module Loc = Abstract.Loc
+ and module Dom = Abstract.Dom =
+ struct
include Abstract
module Eval = Evaluation.Make (Ctx) (Val) (Loc) (Dom)
+ module Compute = C
end
+ and C : Engine_sig.Compute = Compute_functions.Make (Engine)
- include Abstract
- include Compute_functions.Make (Abstract)
+ include Engine
let find stmt f =
if is_computed ()
@@ -115,15 +114,15 @@ module Make (Abstract: Abstractions.S) = struct
find stmt (Dom.Store.get_stmt_state ~after :> stmt -> Dom.t or_top_bottom)
let get_stmt_state_by_callstack ?selection ~after stmt =
- find stmt (Abstract.Dom.Store.get_stmt_state_by_callstack ?selection ~after)
+ find stmt (Dom.Store.get_stmt_state_by_callstack ?selection ~after)
let get_global_state () =
- (Abstract.Dom.Store.get_global_state () :> Dom.t or_top_bottom)
+ (Dom.Store.get_global_state () :> Dom.t or_top_bottom)
let get_initial_state kf =
if is_computed () then
if Function_calls.is_called kf
- then (Abstract.Dom.Store.get_initial_state kf :> Dom.t or_top_bottom)
+ then (Dom.Store.get_initial_state kf :> Dom.t or_top_bottom)
else `Bottom
else `Top
@@ -154,15 +153,15 @@ module Make (Abstract: Abstractions.S) = struct
end
-
let default = Abstractions.Config.of_list [Cvalue_domain.registered, None]
-module Default : Analyzer = Make (val Abstractions.make default)
+module DefaultAbstractions = (val Abstractions.make default)
+module Default : S = Make (DefaultAbstractions)
(* Reference to the current configuration (built by Abstractions.configure from
the parameters of Eva regarding the abstractions used in the analysis) and
the current Analyzer module. *)
-let ref_analyzer = ref (default, (module Default : Analyzer))
+let ref_analyzer = ref (default, (module Default : S))
(* Returns the current Analyzer module. *)
let current_analyzer () = (module (val (snd !ref_analyzer)): S)
@@ -176,7 +175,7 @@ let register_hook = Analyzer_Hook.extend
(* Sets the current Analyzer module for a given configuration.
Calls the hooks above. *)
-let set_current_analyzer config (analyzer: (module Analyzer)) =
+let set_current_analyzer config (analyzer: (module S)) =
Analyzer_Hook.apply (module (val analyzer): S);
ref_analyzer := (config, analyzer)
@@ -184,7 +183,7 @@ let set_current_analyzer config (analyzer: (module Analyzer)) =
and sets it as the current analyzer. *)
let make_analyzer config =
let analyzer =
- if Abstractions.Config.(equal config default) then (module Default : Analyzer)
+ if Abstractions.Config.(equal config default) then (module Default : S)
else
let module Abstract = (val Abstractions.make config) in
let module Analyzer = Make (Abstract) in
@@ -217,7 +216,7 @@ let force_compute () =
(* The new analyzer can be accesed through hooks *)
Self.ComputationState.set Computing;
let module Analyzer = (val snd !ref_analyzer) in
- try Analyzer.compute_from_entry_point ~lib_entry kf
+ try Analyzer.Compute.compute_from_entry_point ~lib_entry kf
with Self.Abort ->
Self.(ComputationState.set Aborted);
Self.error "The analysis has been aborted: results are incomplete."
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index 436a53aa7c6..b1c00bbb76c 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -48,24 +48,19 @@ module type Results = sig
end
-module Make (Abstract: Abstractions.S) : sig
-
- val compute_from_entry_point : kernel_function -> lib_entry:bool -> unit
- val compute_from_init_state: kernel_function -> Abstract.Dom.t -> unit
-
- include Results with type state := Abstract.Dom.state
- and type value := Abstract.Val.t
- and type location := Abstract.Loc.location
-end
-
-
module type S = sig
- include Abstractions.S_with_evaluation
+ include Engine_sig.S
include Results with type state := Dom.state
and type value := Val.t
and type location := Loc.location
end
+module Make (Abstract: Abstractions.S) : S
+ with module Ctx = Abstract.Ctx
+ and module Val = Abstract.Val
+ and module Loc = Abstract.Loc
+ and module Dom = Abstract.Dom
+
val current_analyzer : unit -> (module S)
(** The abstractions used in the latest analysis, and its results. *)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 84a84a278f1..dfd18af97e0 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -151,28 +151,32 @@ let register_signal_handler () =
let restore_sigint = register_handler Sys.sigint interrupt in
fun () -> restore_sigusr1 (); restore_sigint ()
-module Make (Abstract: Abstractions.S_with_evaluation) = struct
+module Make (Engine: Engine_sig.S) = struct
- module PowersetDomain = Powerset.Make (Abstract.Dom)
+ module PowersetDomain = Powerset.Make (Engine.Dom)
- module Transfer = Transfer_stmt.Make (Abstract)
- module Logic = Transfer_logic.Make (Abstract.Dom) (PowersetDomain)
- module Spec = Transfer_specification.Make (Abstract) (PowersetDomain) (Logic)
- module Init = Initialization.Make (Abstract.Dom) (Abstract.Eval) (Transfer)
+ module Transfer = Transfer_stmt.Make (Engine)
+ module Logic = Transfer_logic.Make (Engine.Dom) (PowersetDomain)
+ module Spec = Transfer_specification.Make (Engine) (PowersetDomain) (Logic)
+ module Init = Initialization.Make (Engine.Dom) (Engine.Eval) (Transfer)
module Computer =
Iterator.Computer
- (Abstract) (PowersetDomain) (Transfer) (Init) (Logic) (Spec)
+ (Engine) (PowersetDomain) (Transfer) (Init) (Logic) (Spec)
- include Cvalue_domain.Getters (Abstract.Dom)
+ include Cvalue_domain.Getters (Engine.Dom)
+
+ type state = Engine.Dom.t
+ type loc = Engine.Loc.location
+ type value = Engine.Val.t
let get_cval =
- match Abstract.Val.get Main_values.CVal.key with
+ match Engine.Val.get Main_values.CVal.key with
| None -> fun _ -> assert false
| Some get -> fun value -> get value
let get_ploc =
- match Abstract.Loc.get Main_locations.PLoc.key with
+ match Engine.Loc.get Main_locations.PLoc.key with
| None -> fun _ -> assert false
| Some get -> fun location -> get location
@@ -186,7 +190,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* ----- Mem Exec cache --------------------------------------------------- *)
- module MemExec = Mem_exec.Make (Abstract.Val) (Abstract.Dom)
+ module MemExec = Mem_exec.Make (Engine.Val) (Engine.Dom)
let compute_and_cache_call compute kinstr call init_state =
let args =
@@ -196,9 +200,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| None ->
let call_result = compute kinstr call init_state in
let () =
- if call_result.Transfer.cacheable = Eval.Cacheable
+ if call_result.Engine_sig.cacheable = Eval.Cacheable
then
- let final_states = call_result.Transfer.states in
+ let final_states = call_result.states in
MemExec.store_computed_call call.kf init_state args final_states
in
call_result
@@ -219,7 +223,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
"Reusing old results for call to %a" Kernel_function.pretty call.kf;
apply_call_results_hooks call init_state (`Reuse i);
(* call can be cached since it was cached once *)
- Transfer.{ states; cacheable = Cacheable; }
+ Engine_sig.{ states; cacheable = Cacheable; }
(* ----- Body or specification analysis ----------------------------------- *)
@@ -274,7 +278,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
if Parameters.ValShowProgress.get () then
Self.feedback
"Done for function %a" Kernel_function.pretty call.kf;
- Transfer.{ states = resulting_states; cacheable; }
+ Engine_sig.{ states = resulting_states; cacheable; }
(* ----- Use of cvalue builtins ------------------------------------------- *)
@@ -293,7 +297,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let join_states = function
| [] -> `Bottom
| (_k,s) :: l ->
- `Value (List.fold_left Abstract.Dom.join s (List.map snd l))
+ `Value (List.fold_left Engine.Dom.join s (List.map snd l))
(* Interprets a call to [kf] at callsite [kinstr] in the state [state]
by using a cvalue builtin. *)
@@ -311,7 +315,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
match final_state with
| `Bottom ->
apply_call_results_hooks call state (`Builtin ([], None));
- Transfer.{ states; cacheable = Eval.Cacheable; }
+ Engine_sig.{ states; cacheable = Cacheable; }
| `Value final_state ->
let cvalue_call = get_cvalue_call call in
let post = get_cvalue_or_top final_state in
@@ -321,17 +325,17 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
in
let insert cvalue_state =
Partition.Key.empty,
- Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
+ Engine.Dom.set Cvalue_domain.State.key cvalue_state final_state
in
let states = List.map insert cvalue_states in
- Transfer.{ states; cacheable; }
+ Engine_sig.{ states; cacheable; }
(* Uses cvalue builtin only if the cvalue domain is available. Otherwise, only
use the called function specification. *)
let compute_builtin =
- if Abstract.Dom.mem Cvalue_domain.State.key
- && Abstract.Val.mem Main_values.CVal.key
- && Abstract.Loc.mem Main_locations.PLoc.key
+ if Engine.Dom.mem Cvalue_domain.State.key
+ && Engine.Val.mem Main_values.CVal.key
+ && Engine.Loc.mem Main_locations.PLoc.key
then compute_builtin
else fun (_, _, _, spec) -> compute_using_spec_or_body (`Spec spec)
@@ -340,7 +344,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Interprets a [call] at callsite [kinstr] in the state [state],
using a builtin, the specification or the body of the called function,
according to [Function_calls.register]. *)
- let compute_call kinstr call recursion state =
+ let compute_call' kinstr call recursion state =
let recursion_depth = Option.map (fun r -> r.depth) recursion in
let target =
Function_calls.define_analysis_target ?recursion_depth kinstr call.kf
@@ -354,7 +358,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
then compute_and_cache_call compute kinstr call state
else compute kinstr call state
- let () = Transfer.compute_call_ref := (fun stmt -> compute_call (Kstmt stmt))
+ let compute_call stmt = compute_call' (Kstmt stmt)
(* ----- Main call -------------------------------------------------------- *)
@@ -362,22 +366,22 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let restore_signals = register_signal_handler () in
let compute () =
let callstack = Eva_utils.init_call_stack kf in
- Abstract.Dom.Store.register_initial_state callstack kf init_state;
+ Engine.Dom.Store.register_initial_state callstack kf init_state;
let call = { kf; callstack; arguments = []; rest = []; return = None; } in
- let final_result = compute_call Kglobal call None init_state in
- let final_states = List.map snd (final_result.Transfer.states) in
+ let final_result = compute_call' Kglobal call None init_state in
+ let final_states = List.map snd (final_result.states) in
let final_state = PowersetDomain.(final_states |> of_list |> join) in
Eva_utils.clear_call_stack ();
- Abstract.Dom.Store.mark_as_computed ();
+ Engine.Dom.Store.mark_as_computed ();
Self.(ComputationState.set Computed);
post_analysis ();
- Abstract.Dom.post_analysis final_state;
+ Engine.Dom.post_analysis final_state;
Summary.print_summary ();
Statistics.export_as_csv ();
restore_signals ()
in
let cleanup () =
- Abstract.Dom.Store.mark_as_computed ();
+ Engine.Dom.Store.mark_as_computed ();
Self.(ComputationState.set Aborted);
post_analysis_cleanup ~aborted:true
in
@@ -395,7 +399,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
in
match initial_state with
| `Bottom ->
- Abstract.Dom.Store.mark_as_computed ();
+ Engine.Dom.Store.mark_as_computed ();
Self.(ComputationState.set Aborted);
Self.result "Eva not started because globals \
initialization is not computable.";
@@ -406,7 +410,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let compute_from_init_state kf init_state =
pre_analysis ();
let b = Parameters.ResultsAll.get () in
- Abstract.Dom.Store.register_global_state b (`Value init_state);
+ Engine.Dom.Store.register_global_state b (`Value init_state);
compute kf init_state
end
diff --git a/src/plugins/eva/engine/compute_functions.mli b/src/plugins/eva/engine/compute_functions.mli
index a79baded6ee..3d2c02c1ce2 100644
--- a/src/plugins/eva/engine/compute_functions.mli
+++ b/src/plugins/eva/engine/compute_functions.mli
@@ -22,14 +22,7 @@
(** Value analysis of entire functions, using Eva engine. *)
-open Cil_types
-
-module Make (Abstract: Abstractions.S_with_evaluation)
- : sig
-
- (** Compute a call to the main function. *)
- val compute_from_entry_point: kernel_function -> lib_entry:bool -> unit
-
- (** Compute a call to the main function from the given initial state. *)
- val compute_from_init_state: kernel_function -> Abstract.Dom.t -> unit
- end
+module Make (Engine : Engine_sig.S) : Engine_sig.Compute
+ with type state = Engine.Dom.t
+ and type value = Engine.Val.t
+ and type loc = Engine.Loc.location
diff --git a/src/plugins/eva/engine/engine_sig.ml b/src/plugins/eva/engine/engine_sig.ml
new file mode 100644
index 00000000000..8597c629984
--- /dev/null
+++ b/src/plugins/eva/engine/engine_sig.ml
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Eval
+
+type 'state call_result = {
+ states: (Partition.key * 'state) list;
+ cacheable: cacheable;
+}
+
+module type Compute =
+sig
+ type state
+ type loc
+ type value
+
+ (** Compute a call to the main function. *)
+ val compute_from_entry_point: kernel_function -> lib_entry:bool -> unit
+
+ (** Compute a call to the main function from the given initial state. *)
+ val compute_from_init_state: kernel_function -> state -> unit
+
+ (** Compute a call during an analysis *)
+ val compute_call:
+ stmt -> (loc, value) call -> recursion option -> state -> state call_result
+end
+
+
+module type S = sig
+ (* The four abstractions (values, locations, states and evaluation context). *)
+ include Abstractions.S
+
+ (* The evaluator for these abstractions *)
+ module Eval : Evaluation_sig.S
+ with type state = Dom.t
+ and type context = Ctx.t
+ and type value = Val.t
+ and type loc = Loc.location
+ and type origin = Dom.origin
+
+ module Compute : Compute
+ with type state = Dom.t
+ and type value = Val.t
+ and type loc = Loc.location
+end
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 373b1bc3c8a..839d17ea3a3 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -38,12 +38,6 @@ module type S = sig
state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
unit or_bottom
val enter_scope: kernel_function -> varinfo list -> state -> state
- type call_result = {
- states: (Partition.key * state) list;
- cacheable: Eval.cacheable;
- }
- val compute_call_ref:
- (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
end
(* Reference filled in by the callwise-inout callback *)
@@ -111,12 +105,12 @@ let substitution_visitor table =
in
{ Eva_ast.Rewrite.default with rewrite_varinfo }
-module Make (Abstract: Abstractions.S_with_evaluation) = struct
+module Make (Engine: Engine_sig.S) = struct
- module Value = Abstract.Val
- module Location = Abstract.Loc
- module Domain = Abstract.Dom
- module Eval = Abstract.Eval
+ module Value = Engine.Val
+ module Location = Engine.Loc
+ module Domain = Engine.Dom
+ module Eval = Engine.Eval
include Cvalue_domain.Getters (Domain)
type state = Domain.t
@@ -288,17 +282,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Function Calls *)
(* ------------------------------------------------------------------------ *)
- type call_result = {
- states: (Partition.key * state) list;
- cacheable: cacheable;
- }
-
- (* Forward reference to [Eval_funs.compute_call] *)
- let compute_call_ref :
- (stmt -> (loc, value) call -> recursion option -> state ->
- call_result) ref
- = ref (fun _ -> assert false)
-
(* Returns the result of a call. *)
let process_call stmt call recursion valuation state =
Eva_utils.push_call_stack call.kf stmt;
@@ -310,7 +293,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
| `Value state ->
let callstack = Eva_utils.current_call_stack () in
Domain.Store.register_initial_state callstack call.kf state;
- !compute_call_ref stmt call recursion state
+ Engine.Compute.compute_call stmt call recursion state
| `Bottom ->
{ states = []; cacheable = Cacheable; }
in
diff --git a/src/plugins/eva/engine/transfer_stmt.mli b/src/plugins/eva/engine/transfer_stmt.mli
index 92a1f591657..34ae3b01fd3 100644
--- a/src/plugins/eva/engine/transfer_stmt.mli
+++ b/src/plugins/eva/engine/transfer_stmt.mli
@@ -47,23 +47,9 @@ module type S = sig
unit or_bottom
val enter_scope: kernel_function -> varinfo list -> state -> state
-
- type call_result = {
- states: (Partition.key * state) list;
- cacheable: Eval.cacheable;
- }
-
- val compute_call_ref:
- (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
end
-module Make (Abstract: Abstractions.S_with_evaluation)
+module Make (Abstract: Engine_sig.S)
: S with type state = Abstract.Dom.t
and type value = Abstract.Val.t
and type loc = Abstract.Loc.location
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
--
GitLab