From 49c690aab04fe9d4a1f32fb9aae54ba170e4e181 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 12 Jun 2023 16:54:21 +0200
Subject: [PATCH] [Eva] Generalize the callstack type to include global
initialization
---
src/dune | 3 +-
.../abstract_interp/eva_types.ml | 152 ++++++++++++------
.../abstract_interp/eva_types.mli | 13 +-
src/plugins/eva/Eva.mli | 14 +-
src/plugins/eva/api/values_request.ml | 23 +--
src/plugins/eva/engine/compute_functions.ml | 5 +-
src/plugins/eva/engine/initialization.ml | 22 ++-
src/plugins/eva/types/callstack.mli | 14 +-
src/plugins/eva/utils/eva_utils.ml | 10 +-
src/plugins/eva/utils/results.ml | 2 +-
10 files changed, 178 insertions(+), 80 deletions(-)
diff --git a/src/dune b/src/dune
index 599d3f7423a..7cd55aa0b82 100644
--- a/src/dune
+++ b/src/dune
@@ -39,6 +39,7 @@
(echo " - dune-site.plugins:" %{lib-available:dune-site.plugins} "\n")
(echo " - ppx_import:" %{lib-available:ppx_import} "\n")
(echo " - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n")
+ (echo " - ppx_deriving.ord:" %{lib-available:ppx_deriving.ord} "\n")
(echo " - ppx_deriving_yaml:" %{lib-available:ppx_deriving_yaml} "\n")
)
)
@@ -51,7 +52,7 @@
(flags :standard -w -9)
(libraries frama-c.init fpath str unix zarith ocamlgraph dynlink bytes yaml.unix yojson menhirLib dune-site dune-site.plugins)
(instrumentation (backend landmarks))
- (preprocess (staged_pps ppx_import ppx_deriving.eq ppx_deriving_yaml))
+ (preprocess (staged_pps ppx_import ppx_deriving.eq ppx_deriving.ord ppx_deriving_yaml))
)
(generate_sites_module (module config_data) (sites frama-c) (plugins (frama-c plugins) (frama-c plugins_gui)))
diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index 4e4c5c83558..de54d6beef0 100644
--- a/src/kernel_services/abstract_interp/eva_types.ml
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -25,31 +25,27 @@ struct
module Thread = Int (* Threads are identified by integers *)
module Kf = Kernel_function
module Stmt = Cil_datatype.Stmt
-
- type call = Cil_types.kernel_function * Cil_types.stmt
+ module Var = Cil_datatype.Varinfo
module Call = Datatype.Pair_with_collections(Kf)(Stmt)
(struct let module_name = "Eva.Callstack.Call" end)
-
module Calls = Datatype.List (Call)
- type callstack = {
+ type local_stack = {
thread: int;
- entry_point: Cil_types.kernel_function;
- stack: call list;
+ entry_point: Kernel_function.t;
+ stack: Call.t list;
}
-
- (* Datatype *)
-
- module Prototype =
+ module LocalStack =
struct
- include Datatype.Serializable_undefined
-
- type t = callstack
-
- let name = "Eva.Callstack"
+ type t = local_stack = {
+ thread: int;
+ entry_point: Kernel_function.t;
+ stack: Call.t list;
+ }
+ [@@deriving eq, ord]
let reprs =
List.concat_map (fun stack ->
@@ -65,22 +61,46 @@ struct
in
Format.fprintf fmt "@[<hv>";
List.iter (pp_call fmt) cs.stack;
- Format.fprintf fmt "%a@]" Kf.pretty cs.entry_point
+ Format.fprintf fmt "%a@]" Kernel_function.pretty cs.entry_point
+
+ let hash cs =
+ Hashtbl.hash
+ (cs.thread, Kernel_function.hash cs.entry_point, Calls.hash cs.stack)
+ end
+
+ type call = Call.t
- let equal cs1 cs2 =
- Thread.equal cs1.thread cs2.thread &&
- Calls.equal cs1.stack cs2.stack &&
- Kf.equal cs1.entry_point cs2.entry_point
+ type callstack =
+ | Global of Cil_datatype.Varinfo.t
+ | Local of LocalStack.t
- let compare cs1 cs2 =
- let r = Thread.compare cs1.thread cs2.thread in
- if r <> 0 then r else
- let r = Kf.compare cs1.entry_point cs2.entry_point in
- if r <> 0 then r else
- Calls.compare cs1.stack cs2.stack
+ (* Datatype *)
+
+ module Prototype =
+ struct
+ open Cil_datatype
+ include Datatype.Serializable_undefined
+
+ type t = callstack =
+ | Global of Varinfo.t
+ | Local of LocalStack.t
+ [@@deriving eq, ord]
+
+ let name = "Eva.Callstack"
+
+ let reprs =
+ List.map (fun vi -> Global vi) Varinfo.reprs @
+ List.map (fun ls -> Local ls) LocalStack.reprs
+
+ let pretty fmt cs =
+ match cs with
+ | Global vi -> Format.fprintf fmt "init %a" Varinfo.pretty vi
+ | Local ls -> LocalStack.pretty fmt ls
let hash cs =
- Hashtbl.hash (cs.thread, Kf.hash cs.entry_point, Calls.hash cs.stack)
+ match cs with
+ | Global vi -> Hashtbl.hash (1, Varinfo.hash vi)
+ | Local ls -> Hashtbl.hash (2, LocalStack.hash ls)
end
include Datatype.Make_with_collections (Prototype)
@@ -88,50 +108,86 @@ struct
(* Constructor *)
- let init ?(thread=0) entry_point = { thread ; entry_point ; stack = [] }
+ let init_global vi =
+ Global vi
+
+ let init_local ?(thread=0) kf =
+ Local { thread; entry_point=kf; stack = [] }
+
+ (* Query *)
+ let is_local = function
+ | Global _ -> false
+ | Local _ -> true
(* Stack manipulation *)
+ let local = function
+ | Global _vi ->
+ invalid_arg "invalid stack manipulation on a global callstack"
+ | Local ls -> ls
+
let push kf stmt cs =
- { cs with stack = (kf, stmt) :: cs.stack }
+ let ls = local cs in
+ Local { ls with stack = (kf, stmt) :: ls.stack }
let pop cs =
- match cs.stack with
- | [] -> None
- | (kf,stmt) :: tail -> Some (kf, stmt, { cs with stack = tail })
+ match cs with
+ | Global _vi -> None
+ | Local ls ->
+ match ls.stack with
+ | [] -> None
+ | (kf,stmt) :: tail -> Some (kf, stmt, Local { ls with stack = tail })
let top cs =
- match cs.stack with
- | [] -> None
- | (kf, stmt) :: _ -> Some (kf, stmt)
+ match cs with
+ | Global _vi -> None
+ | Local ls ->
+ match ls.stack with
+ | [] -> None
+ | (kf, stmt) :: _ -> Some (kf, stmt)
let top_kf cs =
- match cs.stack with
- | [] -> cs.entry_point
+ let ls = local cs in
+ match ls.stack with
| (kf, _stmt) :: _ -> kf
+ | [] -> ls.entry_point
let top_callsite cs =
- match cs.stack with
- | [] -> None
- | (_kf, stmt) :: _ -> Some (stmt)
+ match cs with
+ | Global _vi -> None
+ | Local ls ->
+ match ls.stack with
+ | [] -> None
+ | (_kf, stmt) :: _ -> Some (stmt)
let top_call cs =
- match cs.stack with
- | [] -> cs.entry_point, Cil_types.Kglobal
+ let ls = local cs in
+ match ls.stack with
| (kf, stmt) :: _ -> kf, Cil_types.Kstmt stmt
+ | [] -> ls.entry_point, Cil_types.Kglobal
+
(* Conversion *)
let to_legacy cs =
- let l =
- List.rev_map (fun (kf, stmt) -> (kf, Cil_types.Kstmt stmt)) cs.stack
- in
- List.rev ((cs.entry_point, Cil_types.Kglobal) :: l)
+ match cs with
+ | Global _vi -> []
+ | Local ls ->
+ let l =
+ List.rev_map (fun (kf, stmt) -> (kf, Cil_types.Kstmt stmt)) ls.stack
+ in
+ List.rev ((ls.entry_point, Cil_types.Kglobal) :: l)
let to_kf_list cs =
- cs.entry_point :: List.rev_map fst cs.stack
+ match cs with
+ | Global _vi -> []
+ | Local ls ->
+ ls.entry_point :: List.rev_map fst ls.stack
let to_stmt_list cs =
- List.rev_map snd cs.stack
+ match cs with
+ | Global _vi -> []
+ | Local ls ->
+ List.rev_map snd ls.stack
end
diff --git a/src/kernel_services/abstract_interp/eva_types.mli b/src/kernel_services/abstract_interp/eva_types.mli
index 4862853563f..dc6b71c84df 100644
--- a/src/kernel_services/abstract_interp/eva_types.mli
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -29,21 +29,30 @@ sig
module Call : Datatype.S with type t = call
- type callstack = private {
+ type local_stack = private {
thread: int;
entry_point: Cil_types.kernel_function;
stack: call list;
}
+ type callstack = private
+ | Global of Cil_types.varinfo
+ | Local of local_stack
+
include Datatype.S_with_collections with type t = callstack
- val init : ?thread:int -> Cil_types.kernel_function -> t
+ val init_global : Cil_types.varinfo -> t
+ val init_local : ?thread:int -> Cil_types.kernel_function -> t
+
+ val is_local : t -> bool
+
val push : Cil_types.kernel_function -> Cil_types.stmt -> t -> t
val pop : t -> (Cil_types.kernel_function * Cil_types.stmt * t) option
val top : t -> (Cil_types.kernel_function * Cil_types.stmt) option
val top_kf : t -> Cil_types.kernel_function
val top_callsite : t -> Cil_types.stmt option
val top_call : t -> Cil_types.kernel_function * Cil_types.kinstr
+
val to_legacy : t -> Value_types.callstack
val to_kf_list : t -> Cil_types.kernel_function list
val to_stmt_list : t -> Cil_types.stmt list
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index ae6966402a3..18d459bb886 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -122,25 +122,33 @@ module Callstack: sig
module Call : Datatype.S with type t = call
- (** [callstack] is used to describe the analysis context when analysing a
+ (** [local_stack] is used to describe the analysis context when analysing a
function. It contains the thread, the entry point and the list of
calls from the entry point.
This type is very likely to change in the future. Never use this type
directly, prefer the use of the following functions when possible. *)
- type callstack = Eva_types.Callstack.callstack = private {
+ type local_stack = Eva_types.Callstack.local_stack = private {
thread: int; (* An identifier of the thread's callstack *)
entry_point: Cil_types.kernel_function; (* The first function in the callstack *)
stack: call list;
}
+ type callstack = Eva_types.Callstack.callstack = private
+ | Global of Cil_types.varinfo
+ | Local of local_stack
+
include Datatype.S_with_collections
with type t = callstack
and module Hashtbl = Eva_types.Callstack.Hashtbl
(* Constructor *)
- val init : ?thread:int -> Cil_types.kernel_function -> t
+ val init_global : Cil_types.varinfo -> t
+ val init_local : ?thread:int -> Cil_types.kernel_function -> t
+
+ (* Query *)
+ val is_local : t -> bool
(* Stack manipulation *)
val push : Cil_types.kernel_function -> Cil_types.stmt -> t -> t
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index a88453bcc12..468a733da7b 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -243,16 +243,19 @@ module Jcalls : Request.Output with type t = callstack = struct
]
let to_json (cs : t) =
- let aux (acc, jcaller) (callee, stmt) =
- let jcallee = Jfct.to_json callee in
- jcallsite jcaller jcallee stmt :: acc, jcallee
- in
- let entry_point = Jfct.to_json cs.entry_point in
- let l, _last_callee = List.fold_left aux
- ([`Assoc [ "callee", entry_point ]], entry_point)
- cs.stack
- in
- `List (List.rev l)
+ match cs with
+ | Global _vi -> `List []
+ | Local ls ->
+ let aux (acc, jcaller) (callee, stmt) =
+ let jcallee = Jfct.to_json callee in
+ jcallsite jcaller jcallee stmt :: acc, jcallee
+ in
+ let entry_point = Jfct.to_json ls.entry_point in
+ let l, _last_callee = List.fold_left aux
+ ([`Assoc [ "callee", entry_point ]], entry_point)
+ ls.stack
+ in
+ `List (List.rev l)
end
module Jtruth : Data.S with type t = truth = struct
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 9996485515f..4dd648dea88 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -352,14 +352,14 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let compute kf init_state =
let restore_signals = register_signal_handler () in
let compute () =
- let callstack = Callstack.init kf in
+ let callstack = Callstack.init_local kf in
Eva_utils.set_call_stack callstack;
store_initial_state callstack 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_state = PowersetDomain.(final_states |> of_list |> join) in
- Eva_utils.pop_call_stack ();
+ Eva_utils.clear_call_stack ();
Self.feedback "done for function %a" Kernel_function.pretty kf;
Abstract.Dom.Store.mark_as_computed ();
Self.(set_computation_state Computed);
@@ -372,6 +372,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let cleanup () =
Abstract.Dom.Store.mark_as_computed ();
Self.(set_computation_state Aborted);
+ Eva_utils.clear_call_stack ();
post_analysis_cleanup ~aborted:true
in
Eva_utils.protect compute ~cleanup
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index ba5c5ea1c15..c8850b93bee 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -308,15 +308,21 @@ module Make
let initialize_global_variable ~lib_entry vi init state =
Cil.CurrentLoc.set vi.vdecl;
+ Eva_utils.set_call_stack (Callstack.init_global vi);
let state = Domain.enter_scope Abstract_domain.Global [vi] state in
- if vi.vsource then
- let initialize =
- if lib_entry || (vi.vstorage = Extern)
- then initialize_var_lib_entry
- else initialize_var_not_lib_entry ~local:false
- in
- initialize Kglobal vi init.init state
- else state
+ let state = if vi.vsource then
+ let initialize =
+ if lib_entry || (vi.vstorage = Extern)
+ then initialize_var_lib_entry
+ else initialize_var_not_lib_entry ~local:false
+ in
+ initialize Kglobal vi init.init state
+ else state
+ in
+ Eva_utils.clear_call_stack ();
+ state
+
+
(* Compute the initial state with all global variable initialized. *)
let compute_global_state ~lib_entry () =
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index f794735b54f..4a22d47031d 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -27,25 +27,33 @@ type call = Cil_types.kernel_function * Cil_types.stmt
module Call : Datatype.S with type t = call
-(** [callstack] is used to describe the analysis context when analysing a
+(** [local_stack] is used to describe the analysis context when analysing a
function. It contains the thread, the entry point and the list of
calls from the entry point.
This type is very likely to change in the future. Never use this type
directly, prefer the use of the following functions when possible. *)
-type callstack = Eva_types.Callstack.callstack = private {
+type local_stack = Eva_types.Callstack.local_stack = private {
thread: int; (* An identifier of the thread's callstack *)
entry_point: Cil_types.kernel_function; (* The first function in the callstack *)
stack: call list;
}
+type callstack = Eva_types.Callstack.callstack = private
+ | Global of Cil_types.varinfo
+ | Local of local_stack
+
include Datatype.S_with_collections
with type t = callstack
and module Hashtbl = Eva_types.Callstack.Hashtbl
(* Constructor *)
-val init : ?thread:int -> Cil_types.kernel_function -> t
+val init_global : Cil_types.varinfo -> t
+val init_local : ?thread:int -> Cil_types.kernel_function -> t
+
+(* Query *)
+val is_local : t -> bool
(* Stack manipulation *)
val push : Cil_types.kernel_function -> Cil_types.stmt -> t -> t
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 9ccd9540a5a..0e9c181d9f0 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -27,12 +27,18 @@ open Cil_types
let current_callstack : Callstack.t option ref = ref None
let clear_call_stack () =
- current_callstack := None
+ match !current_callstack with
+ | None -> ()
+ | Some cs ->
+ if Callstack.is_local cs then
+ Eva_perf.stop_doing (Callstack.to_legacy cs);
+ current_callstack := None
let set_call_stack cs =
assert (!current_callstack = None);
current_callstack := Some cs;
- Eva_perf.start_doing (Callstack.to_legacy cs)
+ if Callstack.is_local cs then
+ Eva_perf.start_doing (Callstack.to_legacy cs)
let current_call_stack () =
match !current_callstack with
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index 75728f5f0eb..897592d765a 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -243,7 +243,7 @@ struct
A.get_stmt_state_by_callstack ?selection ~after:true stmt
|> by_callstack ctx
| Initial ->
- let cs = Callstack.init (fst (Globals.entry_point ())) in
+ let cs = Callstack.init_local (fst (Globals.entry_point ())) in
A.get_global_state () |> singleton cs
| Start kf ->
A.get_initial_state_by_callstack ?selection kf |> by_callstack ctx
--
GitLab