diff --git a/src/dune b/src/dune
index 599d3f7423ac6a0e1daba6de1ea8c204345e76e3..7cd55aa0b825af3628b942e63f2e0b5503c955a6 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 4e4c5c835587809ba6c80e16eb03b389d581533e..de54d6beef06179e7628d41342b308561fe4becd 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 4862853563fe7431c4a11358f27216bb71c05d29..dc6b71c84df1d3dc9f8f7c0043e4f410ba58da89 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 ae6966402a3d95bb0a717f9aa20f0327c0821201..18d459bb8869651e338068a2d54d008b7e7de21f 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 a88453bcc12d9b2403a6850ae78c299a4c1dbe4e..468a733da7b5870bc81ba26668c03f7b03741a35 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 9996485515fe99d557d6cc7a49a75f4578655d3a..4dd648dea88a98b7e190d431e52c3982f14873cf 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 ba5c5ea1c1539b2d72543981a0f827cab92722e1..c8850b93bee8a3c5dedc870fddc896544d2dba27 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 f794735b54fe1f6de26657ee333cedde9ae814a6..4a22d47031dc385f76e9856c0d396cd85b06df85 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 9ccd9540a5a2d237d11025419e29991aa8dc5196..0e9c181d9f04570c2abfa703284b6b30debcacba 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 75728f5f0eb55e5ce139d6fe0f7dbaab16d70c35..897592d765ac58fb766445584e71a1afbec070a4 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