From 751bdaa405d61df7e7efe1a1440dfd04c171a5aa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 15 Jan 2025 09:59:52 +0100
Subject: [PATCH] [Eva] Adds more comments to Engine_sig.
---
src/plugins/eva/engine/compute_functions.ml | 2 ++
src/plugins/eva/engine/engine_sig.ml | 34 +++++++++++++--------
2 files changed, 23 insertions(+), 13 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index dfd18af97e0..c2abf4c3b4a 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -358,6 +358,8 @@ module Make (Engine: Engine_sig.S) = struct
then compute_and_cache_call compute kinstr call state
else compute kinstr call state
+ (* Exported in [Engine_sig.Compute] and used by [Transfer_stmt] when
+ interpreting a call statement. *)
let compute_call stmt = compute_call' (Kstmt stmt)
(* ----- Main call -------------------------------------------------------- *)
diff --git a/src/plugins/eva/engine/engine_sig.ml b/src/plugins/eva/engine/engine_sig.ml
index 8597c629984..13f1581e360 100644
--- a/src/plugins/eva/engine/engine_sig.ml
+++ b/src/plugins/eva/engine/engine_sig.ml
@@ -23,40 +23,48 @@
open Cil_types
open Eval
+(** Results of the analysis of a function call:
+ - the list of computed abstract states at the return statement of the called
+ function, associated with their partition key;
+ - whether the results can safely be stored in the memexec cache. *)
type 'state call_result = {
states: (Partition.key * 'state) list;
cacheable: cacheable;
}
+(** Analysis of functions, built by the functor [Compute_functions.Make]. *)
module type Compute =
sig
type state
type loc
type value
- (** Compute a call to the main function. *)
+ (** Analysis of a program from the given main function. Computed states for
+ each statement are stored in the result tables of each enabled abstract
+ domain. This is called by [Analysis.compute].
+ The initial abstract state is computed according to [lib_entry]:
+ - if false, non-volatile global variables are initialized according
+ to their initializers (zero if no explicit initializer).
+ - if true, non-const global variables are initialized at top. *)
val compute_from_entry_point: kernel_function -> lib_entry:bool -> unit
- (** Compute a call to the main function from the given initial state. *)
+ (** Analysis of a program from the given main function and initial state. *)
val compute_from_init_state: kernel_function -> state -> unit
- (** Compute a call during an analysis *)
+ (** Analysis of a function call during the Eva analysis. This function is
+ called by [Transfer_stmt] when interpreting a call statement.
+ [compute_call stmt call recursion state] analyzes the call [call] at
+ statement [stmt] in the input abstract state [state].
+ If [recursion] is not [None], the call is a recursive call. *)
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
+ (** The four abstractions: values, locations, states and evaluation context,
+ plus the evaluation engine for these abstractions. *)
+ include Abstractions.S_with_evaluation
module Compute : Compute
with type state = Dom.t
--
GitLab