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
new file mode 100644
index 0000000000000000000000000000000000000000..229782bc556f4a22fe3107eb5a01799935788973
--- /dev/null
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -0,0 +1,188 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let stable_hash x = Hashtbl.seeded_hash 0 x
+
+let dkey_callstack = Kernel.register_category "callstack"
+
+module Callstack =
+struct
+ module Thread = Int (* Threads are identified by integers *)
+ module Kf = Kernel_function
+ module Stmt = Cil_datatype.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 = {
+ thread: int;
+ entry_point: Kernel_function.t;
+ stack: Call.t list;
+ }
+
+ module Prototype =
+ struct
+ include Datatype.Serializable_undefined
+
+ type t = callstack = {
+ thread: int;
+ entry_point: Kernel_function.t;
+ stack: Call.t list;
+ }
+ [@@deriving eq, ord]
+
+ let name = "Eva.Callstack"
+
+ let reprs =
+ List.concat_map (fun stack ->
+ List.map (fun entry_point -> { thread = 0; entry_point; stack })
+ Kernel_function.reprs)
+ Calls.reprs
+
+ let pretty fmt cs =
+ let pp_call fmt (kf,stmt) =
+ Format.fprintf fmt "%a :: %a <-@ "
+ Kf.pretty kf
+ Cil_datatype.Location.pretty (Stmt.loc stmt)
+ in
+ Format.fprintf fmt "@[<hv>";
+ List.iter (pp_call fmt) cs.stack;
+ 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
+
+ include Datatype.Make_with_collections (Prototype)
+
+ let pretty_debug = pretty
+
+ let compare_lex cs1 cs2 =
+ if cs1 == cs2 then 0 else
+ let c = Thread.compare cs1.thread cs2.thread in
+ if c <> 0 then c else
+ let c = Kernel_function.compare cs1.entry_point cs2.entry_point in
+ if c <> 0 then c else
+ Calls.compare (List.rev cs1.stack) (List.rev cs2.stack)
+
+ (* Stack manipulation *)
+
+ let init ?(thread=0) kf = { thread; entry_point=kf; stack = [] }
+
+ let push kf stmt cs =
+ { cs with stack = (kf, stmt) :: cs.stack }
+
+ let pop cs =
+ match cs.stack with
+ | [] -> None
+ | _ :: tail -> Some { cs with stack = tail }
+
+ let top cs =
+ match cs.stack with
+ | [] -> None
+ | (kf, stmt) :: _ -> Some (kf, stmt)
+
+ let top_kf cs =
+ match cs.stack with
+ | (kf, _stmt) :: _ -> kf
+ | [] -> cs.entry_point
+
+ let top_callsite cs =
+ match cs.stack with
+ | [] -> Cil_types.Kglobal
+ | (_kf, stmt) :: _ -> Cil_types.Kstmt stmt
+
+ let top_call cs =
+ match cs.stack with
+ | (kf, stmt) :: _ -> kf, Cil_types.Kstmt stmt
+ | [] -> cs.entry_point, Cil_types.Kglobal
+
+ let top_caller cs =
+ match cs.stack with
+ | _ :: (kf, _) :: _ -> Some kf
+ | [_] -> Some cs.entry_point
+ | [] -> None
+
+ (* Conversion *)
+
+ let to_kf_list cs = cs.entry_point :: List.rev_map fst cs.stack
+ let to_stmt_list cs = List.rev_map snd cs.stack
+
+ let to_call_list cs =
+ let l =
+ List.rev_map (fun (kf, stmt) -> (kf, Cil_types.Kstmt stmt)) cs.stack
+ in
+ (cs.entry_point, Cil_types.Kglobal) :: l
+
+ (* Stable hash and pretty-printing *)
+
+ let stmt_hash s =
+ let pos = fst (Cil_datatype.Stmt.loc s) in
+ stable_hash (pos.Filepath.pos_path, pos.Filepath.pos_lnum)
+
+ let kf_hash kf = stable_hash (Kernel_function.get_name kf)
+
+ let rec calls_hash = function
+ | [] -> 0
+ | (kf, stmt) :: tl -> stable_hash (kf_hash kf, stmt_hash stmt, calls_hash tl)
+
+ let stable_hash { thread; entry_point; stack } =
+ let p = stable_hash (thread, kf_hash entry_point, calls_hash stack) in
+ p mod 11_316_496 (* 58 ** 4 *)
+
+ let base58_map = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
+
+ (* Converts [i] into a fixed-length, 4-wide string in base-58 *)
+ let base58_of_int n =
+ let buf = Bytes.create 4 in
+ Bytes.set buf 0 (String.get base58_map (n mod 58));
+ let n = n / 58 in
+ Bytes.set buf 1 (String.get base58_map (n mod 58));
+ let n = n / 58 in
+ Bytes.set buf 2 (String.get base58_map (n mod 58));
+ let n = n / 58 in
+ Bytes.set buf 3 (String.get base58_map (n mod 58));
+ Bytes.to_string buf
+
+ let pretty_hash fmt callstack =
+ if Kernel.is_debug_key_enabled dkey_callstack then
+ Format.fprintf fmt "<%s> " (base58_of_int (stable_hash callstack))
+ else Format.ifprintf fmt ""
+
+ let pretty_short fmt callstack =
+ Format.fprintf fmt "%a" pretty_hash callstack;
+ let list = List.rev (to_kf_list callstack) in
+ Pretty_utils.pp_flowlist ~left:"" ~sep:" <- " ~right:""
+ (fun fmt kf -> Kernel_function.pretty fmt kf)
+ fmt list
+
+ let pretty fmt callstack =
+ Format.fprintf fmt "@[<hv>%a" pretty_hash callstack;
+ pretty fmt callstack;
+ Format.fprintf fmt "@]"
+end
diff --git a/src/kernel_services/abstract_interp/eva_types.mli b/src/kernel_services/abstract_interp/eva_types.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d5406e1d64876766c4d68ce28d7ca537e70e4539
--- /dev/null
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -0,0 +1,63 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** This module is here for compatibility reasons only and will be removed in
+ future versions. Use [Eva.Callstack] instead *)
+
+module Callstack :
+sig
+ type call = Cil_types.kernel_function * Cil_types.stmt
+
+ module Call : Datatype.S with type t = call
+
+ type callstack = {
+ thread: int;
+ entry_point: Cil_types.kernel_function;
+ stack: call list;
+ }
+
+ include Datatype.S_with_collections with type t = callstack
+
+ val pretty_hash : Format.formatter -> t -> unit
+ val pretty_short : Format.formatter -> t -> unit
+ val pretty_debug : Format.formatter -> t -> unit
+
+ val compare_lex : t -> t -> int
+
+ val init : ?thread:int -> Cil_types.kernel_function -> t
+
+ val push : Cil_types.kernel_function -> Cil_types.stmt -> t -> t
+ val pop : t -> 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.kinstr
+ val top_call : t -> Cil_types.kernel_function * Cil_types.kinstr
+ val top_caller : t -> Cil_types.kernel_function option
+
+ val to_kf_list : t -> Cil_types.kernel_function list
+ val to_stmt_list : t -> Cil_types.stmt list
+ val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
+end
+[@@alert db_deprecated
+ "Eva_types is only provided for compatibility reason and will be removed \
+ in a future version of Frama-C. Please use the Eva.Callstack in the \
+ public API instead."]
diff --git a/src/kernel_services/abstract_interp/value_types.ml b/src/kernel_services/abstract_interp/value_types.ml
index de2fbcb8ba0f702ae0537818c03c585572dfca65..d7d070d20e3053df8e3337c8921a6b9bd037c536 100644
--- a/src/kernel_services/abstract_interp/value_types.ml
+++ b/src/kernel_services/abstract_interp/value_types.ml
@@ -20,95 +20,6 @@
(* *)
(**************************************************************************)
-module OCamlHashtbl = Hashtbl
-open Cil_types
-
-type call_site = kernel_function * kinstr
-
-module Callsite = struct
- include Datatype.Pair_with_collections(Kernel_function)(Cil_datatype.Kinstr)
- (struct let module_name = "Value_callbacks.Callpoint" end)
-
- let pretty fmt (kf, ki) =
- Format.fprintf fmt "%a@@%t" Kernel_function.pretty kf
- (fun fmt ->
- match ki with
- | Kglobal -> Format.pp_print_string fmt "<main>"
- | Kstmt stmt -> Format.pp_print_int fmt stmt.sid
- )
-end
-
-let dkey_callstack = Kernel.register_category "callstack"
-
-type callstack = call_site list
-
-module Callstack = struct
- include Datatype.With_collections
- (Datatype.List(Callsite))
- (struct let module_name = "Value_types.Callstack" end)
-
- (* Use default Datatype printer for debug only *)
- let pretty_debug = pretty
-
- let stmt_hash s =
- let pos = fst (Cil_datatype.Stmt.loc s) in
- OCamlHashtbl.seeded_hash 0
- (pos.Filepath.pos_path, pos.Filepath.pos_lnum)
-
- let kf_hash kf =
- let name = Kernel_function.get_name kf in
- OCamlHashtbl.seeded_hash 0 name
-
- let ki_hash = function
- | Kglobal -> 1
- | Kstmt s -> 5 * stmt_hash s
-
- let rec hash = function
- | [] -> 0
- | (kf, ki) :: r ->
- let p = OCamlHashtbl.seeded_hash 0 (kf_hash kf, ki_hash ki, hash r) in
- p mod 11_316_496 (* 58 ** 4 *)
-
- let base58_map = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
-
- (* Converts [i] into a fixed-length, 4-wide string in base-58 *)
- let base58_of_int n =
- let buf = Bytes.create 4 in
- Bytes.set buf 0 (String.get base58_map (n mod 58));
- let n = n / 58 in
- Bytes.set buf 1 (String.get base58_map (n mod 58));
- let n = n / 58 in
- Bytes.set buf 2 (String.get base58_map (n mod 58));
- let n = n / 58 in
- Bytes.set buf 3 (String.get base58_map (n mod 58));
- Bytes.to_string buf
-
- let pretty_hash fmt callstack =
- if Kernel.is_debug_key_enabled dkey_callstack then
- Format.fprintf fmt "<%s> " (base58_of_int (hash callstack))
- else Format.ifprintf fmt ""
-
- let pretty_short fmt callstack =
- Format.fprintf fmt "%a" pretty_hash callstack;
- Pretty_utils.pp_flowlist ~left:"" ~sep:" <- " ~right:""
- (fun fmt (kf,_) -> Kernel_function.pretty fmt kf)
- fmt
- callstack
-
- let pretty fmt callstack =
- Format.fprintf fmt "@[<hv>%a" pretty_hash callstack;
- List.iter (fun (kf,ki) ->
- Kernel_function.pretty fmt kf;
- match ki with
- | Kglobal -> ()
- | Kstmt stmt -> Format.fprintf fmt " :: %a <-@ "
- Cil_datatype.Location.pretty
- (Cil_datatype.Stmt.loc stmt)
- ) callstack;
- Format.fprintf fmt "@]"
-
-end
-
type 'a callback_result =
| Normal of 'a
| NormalStore of 'a * int
diff --git a/src/kernel_services/abstract_interp/value_types.mli b/src/kernel_services/abstract_interp/value_types.mli
index f492097990283c38c1702685c30ce3c6fc89f5d9..811e97b24fd8645dacd03b2224d5186e007f8c6a 100644
--- a/src/kernel_services/abstract_interp/value_types.mli
+++ b/src/kernel_services/abstract_interp/value_types.mli
@@ -23,41 +23,6 @@
(** Declarations that are useful for plugins written on top of the results
of Value. *)
-open Cil_types
-
-(* TODO: These types are already defined in Value_util. *)
-type call_site = kernel_function * kinstr
-(** Value call-site.
- A callsite [(f,p)] represents a call at function [f] invoked
- {i from} program point [p].
-*)
-
-type callstack = call_site list
-(** Value callstacks, as used e.g. in Db.Value hooks.
-
- The head call site [(f,p)] is the most recent one,
- where current function [f] has been called from program point [p].
-
- Therefore, the tail call site is expected to be [(main,Kglobal)]
- where [main] is the global entry point.
-
- Moreover, given two consecutive call-sites […(_,p);(g,_)…] in a callstack,
- program point [p] is then expected to live in function [g].
-*)
-
-module Callsite: Datatype.S_with_collections with type t = call_site
-module Callstack: sig
- include Datatype.S_with_collections with type t = callstack
- val pretty_debug : Format.formatter -> t -> unit
-
- (** Print a hash of the callstack when '-kernel-msg-key callstack'
- is enabled (prints nothing otherwise). *)
- val pretty_hash : Format.formatter -> t -> unit
-
- (** Print a call stack without displaying call sites. *)
- val pretty_short : Format.formatter -> t -> unit
-end
-
type 'a callback_result =
| Normal of 'a
| NormalStore of 'a * int
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 5567a74eefc59512a1aeb82db309194b16e4d71b..1e38b3a9b5af9d933c78c89446a7e60f886e1018 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -127,7 +127,8 @@ module Operational_inputs = struct
let get_external = mk_fun "Operational_inputs.get_external"
module Record_Inout_Callbacks =
- Hook.Build (struct type t = Value_types.callstack * Inout_type.t end)
+ Hook.Build (struct type t = Eva_types.Callstack.t * Inout_type.t end)
+ [@@alert "-db_deprecated"]
let pretty fmt x =
Format.fprintf fmt "@[<v>";
@@ -236,8 +237,11 @@ module Value = struct
let size = 256
+ [@@@ alert "-db_deprecated"]
+ type callstack = Eva_types.Callstack.callstack
+
module States_by_callstack =
- Value_types.Callstack.Hashtbl.Make(Cvalue.Model)
+ Eva_types.Callstack.Hashtbl.Make(Cvalue.Model)
module Table_By_Callstack =
Cil_state_builder.Stmt_hashtbl(States_by_callstack)
@@ -365,19 +369,17 @@ module Value = struct
Cvalue.Model.pretty v)
*)
- type callstack = (kernel_function * kinstr) list
-
module Record_Value_Callbacks =
Hook.Build
(struct
- type t = (kernel_function * kinstr) list * (state Stmt.Hashtbl.t) Lazy.t
+ type t = callstack * (state Stmt.Hashtbl.t) Lazy.t
end)
module Record_Value_Callbacks_New =
Hook.Build
(struct
type t =
- (kernel_function * kinstr) list *
+ callstack *
((state Stmt.Hashtbl.t) Lazy.t * (state Stmt.Hashtbl.t) Lazy.t)
Value_types.callback_result
end)
@@ -385,24 +387,24 @@ module Value = struct
module Record_Value_After_Callbacks =
Hook.Build
(struct
- type t = (kernel_function * kinstr) list * (state Stmt.Hashtbl.t) Lazy.t
+ type t = callstack * (state Stmt.Hashtbl.t) Lazy.t
end)
module Record_Value_Superposition_Callbacks =
Hook.Build
(struct
- type t = (kernel_function * kinstr) list * (state list Stmt.Hashtbl.t) Lazy.t
+ type t = callstack * (state list Stmt.Hashtbl.t) Lazy.t
end)
module Call_Value_Callbacks =
Hook.Build
- (struct type t = state * (kernel_function * kinstr) list end)
+ (struct type t = state * callstack end)
module Call_Type_Value_Callbacks =
Hook.Build(struct
type t = [`Builtin of Value_types.call_froms | `Spec of funspec
| `Def | `Memexec]
- * state * (kernel_function * kinstr) list end)
+ * state * callstack end)
;;
@@ -418,7 +420,7 @@ module Value = struct
let no_results = mk_fun "Value.no_results"
let update_callstack_table ~after stmt callstack v =
- let open Value_types in
+ let open Eva_types in
let find,add =
if after
then AfterTable_By_Callstack.find, AfterTable_By_Callstack.add
@@ -437,9 +439,8 @@ module Value = struct
Callstack.Hashtbl.add r callstack v;
add stmt r
- let merge_initial_state cs state =
- let open Value_types in
- let kf = match cs with (kf, _) :: _ -> kf | _ -> assert false in
+ let merge_initial_state cs kf state =
+ let open Eva_types in
let by_callstack =
try Called_Functions_By_Callstack.find kf
with Not_found ->
@@ -459,7 +460,7 @@ module Value = struct
with Not_found ->
let state =
try
- let open Value_types in
+ let open Eva_types in
let by_callstack = Called_Functions_By_Callstack.find kf in
Callstack.Hashtbl.fold
(fun _cs state acc -> Cvalue.Model.join acc state)
@@ -507,7 +508,7 @@ module Value = struct
match ho with
| None -> Cvalue.Model.bottom
| Some h ->
- Value_types.Callstack.Hashtbl.fold (fun _cs state acc ->
+ Eva_types.Callstack.Hashtbl.fold (fun _cs state acc ->
Cvalue.Model.join acc state
) h Cvalue.Model.bottom
in
@@ -539,7 +540,7 @@ module Value = struct
assert (is_computed ()); (* this assertion fails during Eva analysis *)
match get_stmt_state_callstack ~after stmt with
| None -> acc
- | Some h -> Value_types.Callstack.Hashtbl.fold (fun _ -> f) h acc
+ | Some h -> Eva_types.Callstack.Hashtbl.fold (fun _ -> f) h acc
let fold_state_callstack f acc ~after ki =
assert (is_computed ()); (* this assertion fails during Eva analysis *)
@@ -559,7 +560,7 @@ module Value = struct
| None -> false
| Some h ->
try
- Value_types.Callstack.Hashtbl.iter
+ Eva_types.Callstack.Hashtbl.iter
(fun _cs state ->
if Cvalue.Model.is_reachable state
then raise Is_reachable) h;
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 5dc9c539f9b4cdccfa158fca7f7d303bc374b108..518f3ad3f8a2978179ee41c074c49676c40738e8 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -134,15 +134,19 @@ module Value : sig
(** Return [true] iff the value analysis has been done.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
+ [@@@alert "-db_deprecated"]
+
+ type callstack = Eva_types.Callstack.callstack
+
module Table_By_Callstack:
State_builder.Hashtbl with type key = stmt
- and type data = state Value_types.Callstack.Hashtbl.t
+ and type data = state Eva_types.Callstack.Hashtbl.t
(** Table containing the results of the value analysis, ie.
the state before the evaluation of each reachable statement. *)
module AfterTable_By_Callstack:
State_builder.Hashtbl with type key = stmt
- and type data = state Value_types.Callstack.Hashtbl.t
+ and type data = state Eva_types.Callstack.Hashtbl.t
(** Table containing the state of the value analysis after the evaluation
of each reachable and evaluable statement. Filled only if
[Value_parameters.ResultsAfter] is set. *)
@@ -216,12 +220,12 @@ module Value : sig
val get_initial_state : kernel_function -> state
val get_initial_state_callstack :
- kernel_function -> state Value_types.Callstack.Hashtbl.t option
+ kernel_function -> state Eva_types.Callstack.Hashtbl.t option
val get_state : ?after:bool -> kinstr -> state
(** [after] is false by default. *)
val get_stmt_state_callstack:
- after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t option
+ after:bool -> stmt -> state Eva_types.Callstack.Hashtbl.t option
val get_stmt_state : ?after:bool -> stmt -> state
(** [after] is false by default.
@@ -406,19 +410,20 @@ module Value : sig
(** {3 Callbacks} *)
- type callstack = Value_types.callstack
-
(** Actions to perform at end of each function analysis. Not compatible with
option [-memexec-all] *)
module Record_Value_Callbacks:
- Hook.Iter_hook with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
+ Hook.Iter_hook
+ with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
module Record_Value_Superposition_Callbacks:
- Hook.Iter_hook with type param = callstack * (state list Stmt.Hashtbl.t) Lazy.t
+ Hook.Iter_hook
+ with type param = callstack * (state list Stmt.Hashtbl.t) Lazy.t
module Record_Value_After_Callbacks:
- Hook.Iter_hook with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
+ Hook.Iter_hook
+ with type param = callstack * (state Stmt.Hashtbl.t) Lazy.t
(**/**)
(* Temporary API, do not use *)
@@ -493,7 +498,7 @@ module Value : sig
(kernel_function -> call_kinstr:kinstr -> state -> (exp*t) list
-> Cvalue.V_Offsetmap.t option (** returned value of [kernel_function] *) * state) ref
*)
- val merge_initial_state : callstack -> state -> unit
+ val merge_initial_state : callstack -> kernel_function -> state -> unit
(** Store an additional possible initial state for the given callstack as
well as its values for actuals. *)
@@ -657,8 +662,9 @@ module Operational_inputs : sig
(**/**)
(* Internal use *)
module Record_Inout_Callbacks:
- Hook.Iter_hook with type param = Value_types.callstack * Inout_type.t
- (**/**)
+ Hook.Iter_hook with type param = Eva_types.Callstack.t * Inout_type.t
+ [@@alert "-db_deprecated"]
+ (**/**)
end
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index acfa92afaa6498c25af003240e6b683123fe89b6..016d29aa3e101ea5fce05287237a543353ff1790 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -275,6 +275,7 @@ let find_compatible_callstacks stmt callstack =
let callstacks = Eval.to_callstacks stmt in
(* TODO: missing callstacks filtered by memexec *)
let make_compatible cs =
+ let cs = List.rev (Eva.Callstack.to_call_list cs) in
Callstack.truncate_to_sub cs callstack |>
Option.value ~default:(Callstack.init kf)
in
diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml
index f9d329ef16cdd90fae218dcf7d93669d60059f2d..8f94e127823b61085b9b25315ffa0fd97d4353e9 100644
--- a/src/plugins/dive/callstack.ml
+++ b/src/plugins/dive/callstack.ml
@@ -22,10 +22,11 @@
open Cil_types
-include Value_types.Callstack
+module Callsite = Datatype.Pair (Kernel_function) (Cil_datatype.Kinstr)
+type call_site = Callsite.t
-type call_site = Value_types.call_site
-module Callsite = Value_types.Callsite
+include Datatype.With_collections (Datatype.List (Callsite))
+ (struct let module_name = "Dive.Callstack" end)
let init kf = [(kf,Kglobal)]
diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml
index ef3c84076d6d3a39afe77c1c39c0786fc8602102..d6aeae490d92bb6f49896e464b6cef67087a53ec 100644
--- a/src/plugins/dive/dive_graph.ml
+++ b/src/plugins/dive/dive_graph.ml
@@ -177,7 +177,7 @@ let output_to_dot out_channel g =
let build_label s = `HtmlLabel (Extlib.html_escape s) in
let module FileTable = Datatype.String.Hashtbl in
- let module CallstackTable = Value_types.Callstack.Hashtbl in
+ let module CallstackTable = Callstack.Hashtbl in
let file_table = FileTable.create 13
and callstack_table = CallstackTable.create 13 in
let file_counter = ref 0 in
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index db84313b85ad427fb3c61cacc7507d1c02809886..aa5f15a1aa332ffe18f788769d042ec12723c6b9 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -115,6 +115,75 @@ module Analysis: sig
val save_results: Cil_types.kernel_function -> bool
end
+module Callstack: sig
+ [@@@ alert "-db_deprecated"]
+
+ (** A call is identified by the function called and the call statement *)
+ type call = Cil_types.kernel_function * Cil_types.stmt
+
+ module Call : Datatype.S with type t = call
+
+ (** Eva callstacks. *)
+ type callstack = Eva_types.Callstack.callstack = {
+ thread: int;
+ (* An identifier of the thread's callstack. *)
+ entry_point: Cil_types.kernel_function;
+ (** The first function function of the callstack. *)
+ stack: call list;
+ (** A call stack is a list of calls. The head is the latest call. *)
+ }
+
+ include Datatype.S_with_collections
+ with type t = callstack
+ and module Hashtbl = Eva_types.Callstack.Hashtbl
+
+ (** Prints a callstack without displaying call sites. *)
+ val pretty_short : Format.formatter -> t -> unit
+
+ (** Prints a hash of the callstack when '-kernel-msg-key callstack'
+ is enabled (prints nothing otherwise). *)
+ val pretty_hash : Format.formatter -> t -> unit
+
+ (** [compare_lex] compares callstack lexicographically, slightly slower
+ than [compare] but in a more natural order, giving more importance
+ to the function at bottom of the callstack - the first functions called. *)
+ val compare_lex : t -> t -> int
+
+ (*** {2 Stack manipulation} *)
+
+ (*** Constructor *)
+ val init : ?thread:int -> Cil_types.kernel_function -> t
+
+ (** Adds a new call to the top of the callstack. *)
+ val push : Cil_types.kernel_function -> Cil_types.stmt -> t -> t
+
+ (** Removes the topmost call from the callstack. *)
+ val pop : t -> 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.kinstr
+ val top_call : t -> Cil_types.kernel_function * Cil_types.kinstr
+
+ (** Returns the function that called the topmost function of the callstack. *)
+ val top_caller : t -> Cil_types.kernel_function option
+
+ (** {2 Conversion} *)
+
+ (** Gives the list of kf in the callstack from the entry point to the top of the
+ callstack (i.e. reverse order of the call stack). *)
+ val to_kf_list : t -> Cil_types.kernel_function list
+
+ (** Gives the list of call statements from the bottom to the top of the
+ callstack (i.e. reverse order of the call stack). *)
+ val to_stmt_list : t -> Cil_types.stmt list
+
+ (** Gives the list of call from the bottom to the top of the callstack
+ (i.e. reverse order of the call stack). *)
+ val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
+
+end
+
module Results: sig
(** Eva's result API is a new interface to access the results of an analysis,
@@ -158,8 +227,6 @@ module Results: sig
all requests in the function will lead to a Top error. *)
val are_available : Cil_types.kernel_function -> bool
- type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
-
type request
type value
@@ -222,16 +289,16 @@ module Results: sig
(** Only consider the given callstack.
Replaces previous calls to [in_callstack] or [in_callstacks]. *)
- val in_callstack : callstack -> request -> request
+ val in_callstack : Callstack.t -> request -> request
(** Only consider the callstacks from the given list.
Replaces previous calls to [in_callstack] or [in_callstacks]. *)
- val in_callstacks : callstack list -> request -> request
+ val in_callstacks : Callstack.t list -> request -> request
(** Only consider callstacks satisfying the given predicate. Several filters
can be added. If callstacks are also selected with [in_callstack] or
[in_callstacks], only the selected callstacks will be filtered. *)
- val filter_callstack : (callstack -> bool) -> request -> request
+ val filter_callstack : (Callstack.t -> bool) -> request -> request
(** Working with callstacks *)
@@ -241,11 +308,11 @@ module Results: sig
reached by the analysis, or if no information has been saved at this point
(for instance with the -eva-no-results option).
Use [is_empty request] to distinguish these two cases. *)
- val callstacks : request -> callstack list
+ val callstacks : request -> Callstack.t list
(** Returns a list of subrequests for each reachable callstack from
the given request. *)
- val by_callstack : request -> (callstack * request) list
+ val by_callstack : request -> (Callstack.t * request) list
(** State requests *)
@@ -616,7 +683,6 @@ module Cvalue_callbacks: sig
in a future version. Please contact us if you need to register callbacks
to be executed during an Eva analysis. *)
- type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
type state = Cvalue.Model.t
type analysis_kind =
@@ -630,7 +696,7 @@ module Cvalue_callbacks: sig
the function called, the kind of analysis performed by Eva for this call,
and the cvalue state at the beginning of the call. *)
val register_call_hook:
- (callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit)
+ (Callstack.t -> Cil_types.kernel_function -> analysis_kind -> state -> unit)
-> unit
@@ -650,7 +716,7 @@ module Cvalue_callbacks: sig
function call. Arguments of the callback are the callstack of the call,
the function called and the cvalue states resulting from its analysis. *)
val register_call_results_hook:
- (callstack -> Cil_types.kernel_function -> call_results -> unit)
+ (Callstack.t -> Cil_types.kernel_function -> call_results -> unit)
-> unit
end
@@ -733,7 +799,7 @@ module Eva_results: sig
For technical reasons, the top of the callstack must currently
be preserved. *)
val change_callstacks:
- (Value_types.callstack -> Value_types.callstack) -> results -> results
+ (Callstack.t -> Callstack.t) -> results -> results
val eval_tlval_as_location :
?result:Cil_types.varinfo ->
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index d810aa0d99919467335cedb4939e4c56408bd45a..8e0c351b98b2d9c605e8d7723dc47640200387b9 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -26,9 +26,8 @@ open Cil_types
module Kmap = Kernel_function.Hashtbl
module Smap = Cil_datatype.Stmt.Hashtbl
-module CS = Value_types.Callstack
-module CSet = CS.Set
-module CSmap = CS.Hashtbl
+module CSet = Callstack.Set
+module CSmap = Callstack.Hashtbl
module Md = Markdown
module Jfct = Kernel_ast.Function
@@ -49,7 +48,6 @@ type evaluation_point = General_requests.evaluation_point =
(* A term and the program point where it should be evaluated. *)
type probe = term * evaluation_point
-type callstack = Value_types.callstack
type truth = Abstract_interp.truth
(* The result of an evaluation:
@@ -138,7 +136,7 @@ let probe marker =
module type Ranking_sig = sig
val stmt : stmt -> int
- val sort : callstack list -> callstack list
+ val sort : Callstack.t list -> Callstack.t list
end
module Ranking : Ranking_sig = struct
@@ -198,18 +196,15 @@ module Ranking : Ranking_sig = struct
let stmt = let rk = new ranker in rk#rank
- let rec ranks (rks : int list) (cs : callstack) : int list =
- match cs with
- | [] -> rks
- | (_,Kglobal)::wcs -> ranks rks wcs
- | (_,Kstmt s)::wcs -> ranks (stmt s :: rks) wcs
+ let ranks (cs : Callstack.t) : int list =
+ List.map stmt (Callstack.to_stmt_list cs)
let order : int list -> int list -> int = Stdlib.compare
- let sort (wcs : callstack list) : callstack list =
+ let sort (wcs : Callstack.t list) : Callstack.t list =
List.map fst @@
List.sort (fun (_,rp) (_,rq) -> order rp rq) @@
- List.map (fun cs -> cs , ranks [] cs) wcs
+ List.map (fun cs -> cs , ranks cs) wcs
end
@@ -217,9 +212,9 @@ end
(* --- Domain Utilities --- *)
(* -------------------------------------------------------------------------- *)
-module Jcallstack : S with type t = callstack = struct
+module Jcallstack : S with type t = Callstack.t = struct
module I = Data.Index
- (Value_types.Callstack.Map)
+ (Callstack.Map)
(struct let name = "eva-callstack-id" end)
let jtype = Data.declare ~package ~name:"callstack" I.jtype
type t = I.t
@@ -227,9 +222,9 @@ module Jcallstack : S with type t = callstack = struct
let of_json = I.of_json
end
-module Jcalls : Request.Output with type t = callstack = struct
+module Jcalls : Request.Output with type t = Callstack.t = struct
- type t = callstack
+ type t = Callstack.t
let jtype = Package.(Jarray (Jrecord [
"callee" , Jfct.jtype ;
@@ -238,23 +233,25 @@ module Jcalls : Request.Output with type t = callstack = struct
"rank" , Joption Jnumber ;
]))
- let rec jcallstack jcallee ki cs : json list =
- match ki , cs with
- | Kglobal , _ | _ , [] -> [ `Assoc [ "callee", jcallee ] ]
- | Kstmt stmt , (called,ki) :: cs ->
- let jcaller = Jfct.to_json called in
- let callsite = `Assoc [
- "callee", jcallee ;
- "caller", jcaller ;
- "stmt", Jstmt.to_json stmt ;
- "rank", Jint.to_json (Ranking.stmt stmt) ;
- ]
- in
- callsite :: jcallstack jcaller ki cs
-
- let to_json = function
- | [] -> `List []
- | (callee,ki)::cs -> `List (jcallstack (Jfct.to_json callee) ki cs)
+ let jcallsite ~jcaller ~jcallee stmt =
+ `Assoc [
+ "callee", jcallee ;
+ "caller", jcaller ;
+ "stmt", Jstmt.to_json stmt ;
+ "rank", Jint.to_json (Ranking.stmt stmt) ;
+ ]
+
+ 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)
+ (List.rev cs.stack)
+ in
+ `List l
end
@@ -353,9 +350,9 @@ let filter_variables bases =
(* -------------------------------------------------------------------------- *)
module type EvaProxy = sig
- val kf_callstacks : kernel_function -> callstack list
- val stmt_callstacks : stmt -> callstack list
- val evaluate : probe -> callstack option -> evaluations
+ val kf_callstacks : kernel_function -> Callstack.t list
+ val stmt_callstacks : stmt -> Callstack.t list
+ val evaluate : probe -> Callstack.t option -> evaluations
end
module Proxy(A : Analysis.S) : EvaProxy = struct
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index 4f17d70e897baac10ce641654653c972c309e88a..77b26cbe8cc5bcb6e6cd6812c283f612ecb56eed 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -38,7 +38,7 @@ let wkey_imprecise_alloc = Self.register_warn_category
module Base_hptmap = Hptmap.Make
(Base.Base)
- (Value_types.Callstack)
+ (Callstack)
(Hptmap.Comp_unused)
(struct let v = [ [ ] ] end)
(struct let l = [ Ast.self ] end)
@@ -57,9 +57,9 @@ let () = Ast.add_monotonic_state Dynamic_Alloc_Bases.self
(* -------------------------- Auxiliary functions -------------------------- *)
let current_call_site () =
- match Eva_utils.call_stack () with
- | (_kf, Kstmt stmt) :: _ -> stmt
- | _ -> Cil.dummyStmt
+ match Callstack.top_callsite (Eva_utils.current_call_stack ()) with
+ | Kglobal -> Cil.dummyStmt
+ | Kstmt stmt -> stmt
(* Remove some parts of the callstack:
- Remove the bottom of the call tree until we get to the call site
@@ -67,29 +67,26 @@ let current_call_site () =
these call site correspond to a different use of a malloc function,
so it is interesting to keep their bases separated. *)
let call_stack_no_wrappers () =
- let stack = Eva_utils.call_stack () in
- assert (stack != []);
- let wrappers = Parameters.AllocFunctions.get() in
+ let cs = Eva_utils.current_call_stack () in
+ let wrappers = Parameters.AllocFunctions.get () in
let rec bottom_filter = function
- | [] -> assert false
- | [_] as stack -> stack (* Do not empty the stack completely *)
+ | [] | [_] as stack -> stack
| (kf,_)::((kf', _):: _ as rest) as stack ->
- if Datatype.String.Set.mem (Kernel_function.get_name kf) wrappers then
- if Datatype.String.Set.mem (Kernel_function.get_name kf') wrappers then
- bottom_filter rest
- else
- stack
- else
- stack
+ if Datatype.String.Set.mem (Kernel_function.get_name kf) wrappers
+ && Datatype.String.Set.mem (Kernel_function.get_name kf') wrappers
+ then bottom_filter rest
+ else stack
in
- bottom_filter stack
+ { cs with stack = bottom_filter cs.stack }
-let register_malloced_base ?(stack=call_stack_no_wrappers ()) b =
- let stack_without_top = List.tl stack in
+let register_malloced_base ~stack b =
+ let stack_without_top =
+ Option.value ~default:stack (Callstack.pop stack)
+ in
Dynamic_Alloc_Bases.set
(Base_hptmap.add b stack_without_top (Dynamic_Alloc_Bases.get ()))
-let fold_dynamic_bases (f: Base.t -> Value_types.Callstack.t -> 'a -> 'a) init =
+let fold_dynamic_bases (f: Base.t -> Callstack.t -> 'a -> 'a) init =
Base_hptmap.fold f (Dynamic_Alloc_Bases.get ()) init
let is_automatically_deallocated base =
@@ -120,20 +117,17 @@ let extract_size sizev_bytes =
(* Name of the base that will be given to a malloced variable, determined
using the callstack. *)
-let base_name prefix stack =
+let base_name prefix cs =
let stmt_line stmt = (fst (Cil_datatype.Stmt.loc stmt)).Filepath.pos_lnum in
- match stack with
- | [] -> assert false
- | [kf, Kglobal] -> (* Degenerate case *)
- Format.asprintf "__%s_%a" prefix Kernel_function.pretty kf
- | (_, Kglobal) :: _ :: _ -> assert false
- | (_, Kstmt callsite) :: qstack ->
+ match cs.Callstack.stack with
+ | [] ->
+ (* Degenerate case *)
+ Format.asprintf "__%s_%a" prefix Kernel_function.pretty cs.entry_point
+ | (_, callsite) :: qstack ->
(* Use the whole call-stack to generate the name *)
let rec loop_full = function
- | [_, Kglobal] -> Format.sprintf "_%s" (Kernel.MainFunction.get ())
- | (_, Kglobal) :: _ :: _ -> assert false
- | [] -> assert false (* impossible, we should have seen a Kglobal *)
- | (kf, Kstmt line)::b ->
+ | [] -> Format.sprintf "_%s" (Kernel_function.get_name cs.entry_point)
+ | (kf, line) :: b ->
let line = stmt_line line in
let node_str = Format.asprintf "_l%d__%a"
line Kernel_function.pretty kf
@@ -141,14 +135,14 @@ let base_name prefix stack =
(loop_full b) ^ node_str
in
(* Use only the name of the caller to malloc for the name *)
- let caller = function
- | [] -> assert false (* caught above *)
- | (kf, _) :: _ -> Format.asprintf "_%a" Kernel_function.pretty kf
+ let caller =
+ let kf = Callstack.top_kf { cs with stack = qstack } in
+ Format.asprintf "_%a" Kernel_function.pretty kf
in
let full_name = false in
Format.asprintf "__%s%s_l%d"
prefix
- (if full_name then loop_full qstack else caller qstack)
+ (if full_name then loop_full qstack else caller)
(stmt_line callsite)
type var = Weak | Strong
@@ -217,7 +211,7 @@ let guess_intended_malloc_type stack sizev constant_size =
| _ -> raise Exit
in
try
- match snd (List.hd stack) with
+ match Callstack.top_callsite stack with
| Kstmt {skind = Instr (Call (Some lv, _, _, _))} ->
mk_typed_size (Cil.typeOfLval lv)
| Kstmt {skind = Instr(Local_init(vi, _, _))} -> mk_typed_size vi.vtype
@@ -380,7 +374,7 @@ let string_of_region = function
(* Only called when the 'weakest base' needs to be allocated. *)
let create_weakest_base region =
- let stack = [ fst (Globals.entry_point ()), Kglobal ] in
+ let stack = { (Eva_utils.current_call_stack ()) with stack = [] } in
let type_base =
TArray (Cil.charType, None, [])
in
@@ -413,8 +407,8 @@ let alloc_weakest_base region =
stack. Currently, the callstacks are truncated according to
[-eva-alloc-functions]. *)
module MallocedByStack = (* varinfo list Callstack.hashtbl *)
- State_builder.Hashtbl(Value_types.Callstack.Hashtbl)
- (Datatype.List(Base))
+ State_builder.Hashtbl (Callstack.Hashtbl)
+ (Datatype.List (Base))
(struct
let name = "Value.Builtins_malloc.MallocedByStack"
let size = 17
@@ -686,7 +680,7 @@ let free_automatic_bases stack state =
let bases_to_free =
Base_hptmap.fold (fun base stack' acc ->
if is_automatically_deallocated base &&
- Value_types.Callstack.equal stack stack'
+ Callstack.equal stack stack'
then Base.Hptset.add base acc
else acc
) (Dynamic_Alloc_Bases.get ()) Base.Hptset.empty
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.mli b/src/plugins/eva/domains/cvalue/builtins_malloc.mli
index 8cd4f9ddabf4ba775b258e6fc96fca993996285d..399b01a97c65de424fe157642df55c4b3f22c98b 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.mli
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.mli
@@ -23,7 +23,7 @@
(** Dynamic allocation related builtins.
Most functionality is exported as builtins. *)
-val fold_dynamic_bases: (Base.t -> Value_types.Callstack.t -> 'a -> 'a) -> 'a -> 'a
+val fold_dynamic_bases: (Base.t -> Callstack.t -> 'a -> 'a) -> 'a -> 'a
(** [fold_dynamic_bases f init] folds [f] to each dynamically allocated base,
with initial accumulator [init].
Note that this also includes bases created by [alloca] and [VLAs]. *)
@@ -34,7 +34,7 @@ val alloc_size_ok: Cvalue.V.t -> Alarmset.status
small enough, [False] that the allocation is guaranteed to fail (because
the size is always greater than SIZE_MAX). *)
-val free_automatic_bases: Value_types.Callstack.t -> Cvalue.Model.t -> Cvalue.Model.t
+val free_automatic_bases: Callstack.t -> Cvalue.Model.t -> Cvalue.Model.t
(** Performs the equivalent of [free] for each location that was allocated via
[alloca()] in the current function (as per [Eva_utils.call_stack ()]).
This function must be called during finalization of a function call. *)
@@ -44,7 +44,3 @@ val freeable: Cvalue.V.t -> Abstract_interp.truth
value points to an allocated memory block that can be safely released using
the C function free. Note that \freeable(\null) does not hold, despite NULL
being a valid argument to the C function free. *)
-
-(**/**)
-val register_malloced_base: ?stack:Value_types.Callstack.t -> Base.t -> unit
-(* Should not be used by casual users. *)
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index b543ce8a78c89f9ec93388d8b0c7824fc4e464b0..4a34203eed44a62880082513b6b35d4e872b9621 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -92,7 +92,7 @@ let memcpy_check_indeterminate_offsetmap offsm =
currently called function. *)
let deps_nth_arg n =
let open Function_Froms in
- let (kf,_) = List.hd (Eva_utils.call_stack()) in
+ let kf = Callstack.top_kf (Eva_utils.current_call_stack ()) in
try
let vi = List.nth (Kernel_function.get_formals kf) n in
Deps.add_data_dep Deps.bottom (Locations.zone_of_varinfo vi)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 5989aa87bfc229e1f85701ad7cc85777f18b8634..7822ad59369304d3781cdaa189f1c2abfb0fac4a 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -460,8 +460,8 @@ module State = struct
end)
let register_global_state b _ = Storage.set b
- let register_initial_state callstack (state, _clob) =
- Db.Value.merge_initial_state callstack state
+ let register_initial_state callstack kf (state, _clob) =
+ Db.Value.merge_initial_state callstack kf state
let register_state_before_stmt callstack stmt (state, _clob) =
Db.Value.update_callstack_table ~after:false stmt callstack state
let register_state_after_stmt callstack stmt (state, _clob) =
@@ -473,7 +473,6 @@ module State = struct
else `Value (state, Locals_scoping.top ())
let lift_tbl tbl =
- let open Value_types in
let h = Callstack.Hashtbl.create 7 in
let process callstack state =
Callstack.Hashtbl.replace h callstack (state, Locals_scoping.top ())
@@ -485,10 +484,10 @@ module State = struct
match selection with
| None -> tbl
| Some list ->
- let new_tbl = Value_types.Callstack.Hashtbl.create (List.length list) in
+ let new_tbl = Callstack.Hashtbl.create (List.length list) in
let add cs =
- let s = Value_types.Callstack.Hashtbl.find_opt tbl cs in
- Option.iter (Value_types.Callstack.Hashtbl.replace new_tbl cs) s
+ let s = Callstack.Hashtbl.find_opt tbl cs in
+ Option.iter (Callstack.Hashtbl.replace new_tbl cs) s
in
List.iter add list;
new_tbl
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 22b674e46ea768e152224753ce32f0caff4c4ad3..222f8bbe68349524dabe96f1d9b91d1ed3e1e438 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -205,7 +205,7 @@ let actualize_formals state arguments =
let start_call _stmt call _recursion _valuation state =
let with_formals = actualize_formals state call.arguments in
- let stack_with_call = Eva_utils.call_stack () in
+ let stack_with_call = Eva_utils.current_call_stack () in
Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
`Value with_formals
@@ -214,8 +214,9 @@ let finalize_call stmt call _recursion ~pre:_ ~post:state =
To minimize computations, only do it for function definitions. *)
let state' =
if Kernel_function.is_definition call.kf then
- let stack = (call.kf, Kstmt stmt) :: (Eva_utils.call_stack ()) in
- Builtins_malloc.free_automatic_bases stack state
+ let callstack = Eva_utils.current_call_stack () in
+ let callstack = Callstack.push call.kf stmt callstack in
+ Builtins_malloc.free_automatic_bases callstack state
else state
in
`Value state'
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index 4349b82595669625eee09b6bed667205575083ee..0305ca8a35fdbb53e57fdbe620642bffc3d7151a 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -610,8 +610,8 @@ module Restrict
let lift_register f state = f (get_state state)
- let register_initial_state callstack =
- lift_register (Domain.Store.register_initial_state callstack)
+ let register_initial_state callstack kf =
+ lift_register (Domain.Store.register_initial_state callstack kf)
let register_state_before_stmt callstack stmt =
lift_register (Domain.Store.register_state_before_stmt callstack stmt)
let register_state_after_stmt callstack stmt =
@@ -628,7 +628,7 @@ module Restrict
| `Top -> `Top
| `Bottom -> `Bottom
| `Value t ->
- let module Hashtbl = Value_types.Callstack.Hashtbl in
+ let module Hashtbl = Callstack.Hashtbl in
let table = Hashtbl.create (Hashtbl.length t) in
Hashtbl.iter (fun key s -> Hashtbl.add table key (inject s)) t;
`Value table
diff --git a/src/plugins/eva/domains/domain_product.ml b/src/plugins/eva/domains/domain_product.ml
index faa5590ceb6a9ba58aa1edecb081afeec0f8a784..45b71568bd946df35b2042012551fa803f82b1b1 100644
--- a/src/plugins/eva/domains/domain_product.ml
+++ b/src/plugins/eva/domains/domain_product.ml
@@ -302,7 +302,6 @@ module Make
Right.reuse kf bases ~current_input:right_input ~previous_output:right_output
let merge_tbl left_tbl right_tbl =
- let open Value_types in
let tbl = Callstack.Hashtbl.create 7 in
let merge callstack left =
try
@@ -315,7 +314,6 @@ module Make
if Callstack.Hashtbl.length tbl > 0 then `Value tbl else `Bottom
let lift_tbl f tbl =
- let open Value_types in
let new_tbl = Callstack.Hashtbl.create 7 in
let lift cs t = Callstack.Hashtbl.replace new_tbl cs (f t) in
Callstack.Hashtbl.iter lift tbl;
@@ -333,9 +331,9 @@ module Make
let register_global_state b state =
Left.Store.register_global_state b (state >>-: fst);
Right.Store.register_global_state b (state >>-: snd)
- let register_initial_state callstack (left, right) =
- Left.Store.register_initial_state callstack left;
- Right.Store.register_initial_state callstack right
+ let register_initial_state callstack kf (left, right) =
+ Left.Store.register_initial_state callstack kf left;
+ Right.Store.register_initial_state callstack kf right
let register_state_before_stmt callstack stmt (left, right) =
Left.Store.register_state_before_stmt callstack stmt left;
Right.Store.register_state_before_stmt callstack stmt right
diff --git a/src/plugins/eva/domains/domain_store.ml b/src/plugins/eva/domains/domain_store.ml
index 99d9a6c63ce295c49d2cb8bcecee3082d72e9e84..9d8f48ecd40af05f3c35dbbe25ce5540429587d9 100644
--- a/src/plugins/eva/domains/domain_store.ml
+++ b/src/plugins/eva/domains/domain_store.ml
@@ -32,22 +32,22 @@ end
module type S = sig
type t
val register_global_state: bool -> t or_bottom -> unit
- val register_initial_state: Value_types.callstack -> t -> unit
- val register_state_before_stmt: Value_types.callstack -> stmt -> t -> unit
- val register_state_after_stmt: Value_types.callstack -> stmt -> t -> unit
+ val register_initial_state: Callstack.t -> kernel_function -> t -> unit
+ val register_state_before_stmt: Callstack.t -> stmt -> t -> unit
+ val register_state_after_stmt: Callstack.t -> stmt -> t -> unit
(** Allows accessing the states inferred by an Eva analysis after it has
been computed with the domain enabled. *)
val get_global_state: unit -> t or_bottom
val get_initial_state: kernel_function -> t or_bottom
val get_initial_state_by_callstack:
- ?selection:callstack list ->
- kernel_function -> t Value_types.Callstack.Hashtbl.t or_top_bottom
+ ?selection:Callstack.t list ->
+ kernel_function -> t Callstack.Hashtbl.t or_top_bottom
val get_stmt_state: after:bool -> stmt -> t or_bottom
val get_stmt_state_by_callstack:
- ?selection:callstack list ->
- after:bool -> stmt -> t Value_types.Callstack.Hashtbl.t or_top_bottom
+ ?selection:Callstack.t list ->
+ after:bool -> stmt -> t Callstack.Hashtbl.t or_top_bottom
val mark_as_computed: unit -> unit
val is_computed: unit -> bool
@@ -105,7 +105,7 @@ module Make (Domain: InputDomain) = struct
end)
module States_by_callstack =
- Value_types.Callstack.Hashtbl.Make (Domain)
+ Callstack.Hashtbl.Make (Domain)
module Table_By_Callstack =
Cil_state_builder.Stmt_hashtbl(States_by_callstack)
@@ -158,7 +158,6 @@ module Make (Domain: InputDomain) = struct
end)
let update_callstack_table ~after stmt callstack v =
- let open Value_types in
let find,add =
if after
then AfterTable_By_Callstack.find, AfterTable_By_Callstack.add
@@ -184,10 +183,8 @@ module Make (Domain: InputDomain) = struct
| `Bottom -> ()
| `Value state -> Global_State.set state
- let register_initial_state callstack state =
+ let register_initial_state callstack kf state =
if Storage.get () then
- let open Value_types in
- let kf = match callstack with (kf, _) :: _ -> kf | _ -> assert false in
let by_callstack =
try Called_Functions_By_Callstack.find kf
with Not_found ->
@@ -217,7 +214,7 @@ module Make (Domain: InputDomain) = struct
try
let by_callstack = Called_Functions_By_Callstack.find kf in
let state =
- Value_types.Callstack.Hashtbl.fold
+ Callstack.Hashtbl.fold
(fun _cs state acc -> Bottom.join Domain.join acc (`Value state))
by_callstack `Bottom
in
@@ -229,10 +226,10 @@ module Make (Domain: InputDomain) = struct
match selection with
| None -> tbl
| Some list ->
- let new_tbl = Value_types.Callstack.Hashtbl.create (List.length list) in
+ let new_tbl = Callstack.Hashtbl.create (List.length list) in
let add cs =
- let state_opt = Value_types.Callstack.Hashtbl.find_opt tbl cs in
- Option.iter (Value_types.Callstack.Hashtbl.replace new_tbl cs) state_opt
+ let state_opt = Callstack.Hashtbl.find_opt tbl cs in
+ Option.iter (Callstack.Hashtbl.replace new_tbl cs) state_opt
in
List.iter add list;
new_tbl
@@ -263,7 +260,7 @@ module Make (Domain: InputDomain) = struct
match ho with
| None -> `Bottom
| Some h ->
- Value_types.Callstack.Hashtbl.fold
+ Callstack.Hashtbl.fold
(fun _cs state acc -> Bottom.join Domain.join acc (`Value state))
h `Bottom
in
diff --git a/src/plugins/eva/domains/domain_store.mli b/src/plugins/eva/domains/domain_store.mli
index 2eff08d35a87f5d9553b4ae615af97d04a60d065..f8779d56e301db38200b1346aa25da495c684e9a 100644
--- a/src/plugins/eva/domains/domain_store.mli
+++ b/src/plugins/eva/domains/domain_store.mli
@@ -39,22 +39,22 @@ module type S = sig
false, register functions do nothing, and get functions return Top. *)
val register_global_state: bool -> t or_bottom -> unit
- val register_initial_state: Value_types.callstack -> t -> unit
- val register_state_before_stmt: Value_types.callstack -> stmt -> t -> unit
- val register_state_after_stmt: Value_types.callstack -> stmt -> t -> unit
+ val register_initial_state: Callstack.t -> kernel_function -> t -> unit
+ val register_state_before_stmt: Callstack.t -> stmt -> t -> unit
+ val register_state_after_stmt: Callstack.t -> stmt -> t -> unit
(** Allows accessing the states inferred by an Eva analysis after it has
been computed with the domain enabled. *)
val get_global_state: unit -> t or_bottom
val get_initial_state: kernel_function -> t or_bottom
val get_initial_state_by_callstack:
- ?selection:callstack list ->
- kernel_function -> t Value_types.Callstack.Hashtbl.t or_top_bottom
+ ?selection:Callstack.t list ->
+ kernel_function -> t Callstack.Hashtbl.t or_top_bottom
val get_stmt_state: after:bool -> stmt -> t or_bottom
val get_stmt_state_by_callstack:
- ?selection:callstack list ->
- after:bool -> stmt -> t Value_types.Callstack.Hashtbl.t or_top_bottom
+ ?selection:Callstack.t list ->
+ after:bool -> stmt -> t Callstack.Hashtbl.t or_top_bottom
val mark_as_computed: unit -> unit
val is_computed: unit -> bool
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 6877dfd4327e79a383f3fca9c87c3ee06e1952cb..a5aae82cd3584e41c471019a26e2bfd4477b48c1 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -105,7 +105,7 @@
(mode (promote (only Eva.mli)))
(deps
gen-api.sh Eva.header
- engine/analysis.mli utils/results.mli parameters.mli
+ engine/analysis.mli types/callstack.mli utils/results.mli parameters.mli
utils/eva_annotations.mli eval.mli domains/cvalue/builtins.mli
utils/cvalue_callbacks.mli legacy/logic_inout.mli utils/eva_results.mli
utils/unit_tests.mli)
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index f64faf0f84f798badce9ffb4be393f58c4dcf988..ddc557787c5bfa11923b37a338ec8741745af230 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -55,13 +55,13 @@ module type Results = sig
val get_global_state: unit -> state or_top_bottom
val get_stmt_state : after:bool -> stmt -> state or_top_bottom
val get_stmt_state_by_callstack:
- ?selection:callstack list ->
- after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_bottom
+ ?selection:Callstack.t list ->
+ after:bool -> stmt -> state Callstack.Hashtbl.t or_top_bottom
val get_initial_state:
kernel_function -> state or_top_bottom
val get_initial_state_by_callstack:
- ?selection:callstack list ->
- kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_bottom
+ ?selection:Callstack.t list ->
+ kernel_function -> state Callstack.Hashtbl.t or_top_bottom
val eval_expr : state -> exp -> value evaluated
val copy_lvalue: state -> lval -> value flagged_value evaluated
diff --git a/src/plugins/eva/engine/analysis.mli b/src/plugins/eva/engine/analysis.mli
index dc017343ef221e88d4369946e52ffc6463218251..8dd74f365d0902882070a351b18b404853d35eef 100644
--- a/src/plugins/eva/engine/analysis.mli
+++ b/src/plugins/eva/engine/analysis.mli
@@ -31,13 +31,13 @@ module type Results = sig
val get_global_state: unit -> state or_top_bottom
val get_stmt_state : after:bool -> stmt -> state or_top_bottom
val get_stmt_state_by_callstack:
- ?selection:callstack list ->
- after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_bottom
+ ?selection:Callstack.t list ->
+ after:bool -> stmt -> state Callstack.Hashtbl.t or_top_bottom
val get_initial_state:
kernel_function -> state or_top_bottom
val get_initial_state_by_callstack:
- ?selection:callstack list ->
- kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_bottom
+ ?selection:Callstack.t list ->
+ kernel_function -> state Callstack.Hashtbl.t or_top_bottom
val eval_expr : state -> exp -> value evaluated
val copy_lvalue: state -> lval -> value flagged_value evaluated
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 11a90011b3aec48f415ac7bc8bfc4059ac70d5f4..58c9b2173fc58a6df8e25d14c75c92d26822ddc8 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -240,7 +240,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
if pp then
Self.feedback
"@[computing for function %a.@\nCalled from %a.@]"
- Value_types.Callstack.pretty_short call.callstack
+ Callstack.pretty_short call.callstack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc kinstr);
let cvalue_state = get_cvalue_or_top state in
let compute, kind =
@@ -344,22 +344,21 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* ----- Main call -------------------------------------------------------- *)
- let store_initial_state kf init_state =
- Abstract.Dom.Store.register_initial_state (Eva_utils.call_stack ()) init_state;
+ let store_initial_state callstack kf init_state =
+ Abstract.Dom.Store.register_initial_state callstack kf init_state;
let cvalue_state = get_cvalue_or_top init_state in
- Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
+ Db.Value.Call_Value_Callbacks.apply (cvalue_state, callstack)
let compute kf init_state =
let restore_signals = register_signal_handler () in
let compute () =
- Eva_utils.push_call_stack kf Kglobal;
- store_initial_state kf init_state;
- let callstack = [kf, Kglobal] in
+ let callstack = Eva_utils.init_call_stack kf in
+ store_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_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);
diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml
index 9e641c47631d8bb00a3a77537d174723b84387de..8e0817904cab16f7cb9a1ca1b6f9acaeb6cf5466 100644
--- a/src/plugins/eva/engine/function_calls.ml
+++ b/src/plugins/eva/engine/function_calls.ml
@@ -49,12 +49,14 @@ module Callers = Kernel_function.Map.Make (StmtSet)
module CallersTable = Kernel_function.Make_Table (Callers) (val info "Callers")
let register_call kinstr kf =
- match kinstr, Eva_utils.call_stack () with
+ let callstack = Eva_utils.current_call_stack () in
+ let kf', kinstr' = Callstack.top_call callstack in
+ assert (Kernel_function.equal kf kf');
+ assert (Cil_datatype.Kinstr.equal kinstr kinstr');
+ match kinstr, Callstack.top_caller callstack with
| Kglobal, _ -> CallersTable.add kf Kernel_function.Map.empty
- | Kstmt _, ([] | [_]) -> assert false
- | Kstmt stmt, (kf', kinstr') :: (caller, _) :: _ ->
- assert (Kernel_function.equal kf kf');
- assert (Cil_datatype.Kinstr.equal kinstr kinstr');
+ | Kstmt _, None -> assert false
+ | Kstmt stmt, Some caller ->
let callsite = StmtSet.singleton stmt in
let change calls =
let prev_stmts = Kernel_function.Map.find_opt caller calls in
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index ba5c5ea1c1539b2d72543981a0f827cab92722e1..ed47b68bad299b793f3b1cfc6e84dcb5d3652d8a 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -309,14 +309,18 @@ module Make
let initialize_global_variable ~lib_entry vi init state =
Cil.CurrentLoc.set vi.vdecl;
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
+ state
+
+
(* Compute the initial state with all global variable initialized. *)
let compute_global_state ~lib_entry () =
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 7979fd721696059972af7faf81b24327e98c4c0f..fc546c883ccd75cee7a4ca1ba01d5dfebbd4736c 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -450,7 +450,7 @@ module Make_Dataflow
(* TODO: apply on all domains. *)
let states = Partitioning.contents f in
let cvalue_states = gather_cvalues states in
- let callstack = Eva_utils.call_stack () in
+ let callstack = Eva_utils.current_call_stack () in
Cvalue_callbacks.apply_statement_hooks callstack stmt cvalue_states
let update_vertex ?(widening : bool = false) (v : vertex)
@@ -702,7 +702,7 @@ module Make_Dataflow
in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
and merged_post_cvalues = lazy (lift_to_cvalues merged_post_states) in
- let callstack = Eva_utils.call_stack () in
+ let callstack = Eva_utils.current_call_stack () in
if save_results then begin
let register_pre = Domain.Store.register_state_before_stmt callstack
and register_post = Domain.Store.register_state_after_stmt callstack in
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index 30d7fb29e4c0284fe6429a221de6d49f68dd1760..b2fb66139b2ce3db51094c6f76ebd585d7d11ac3 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -192,8 +192,9 @@ let make_recursion call depth =
{ depth; substitution; base_substitution; withdrawal; base_withdrawal; }
let make call =
- let is_same_kf (f, _) = Kernel_function.equal f call.kf in
- let previous_calls = List.filter is_same_kf call.callstack in
+ let is_same_kf = Kernel_function.equal call.kf in
+ let all_calls = Callstack.to_kf_list call.callstack in
+ let previous_calls = List.filter is_same_kf all_calls in
let depth = List.length previous_calls - 1 in
if depth > 0
then Some (make_recursion call depth)
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 3d17e1177e9756eeeafe100a238db064756dc675..200ac09480a6f30ee880aeb71118a1a631be1d91 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -313,7 +313,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Returns the result of a call, and a boolean that indicates whether a
builtin has been used to interpret the call. *)
let process_call stmt call recursion valuation state =
- Eva_utils.push_call_stack call.kf (Kstmt stmt);
+ Eva_utils.push_call_stack call.kf stmt;
let cleanup () =
Eva_utils.pop_call_stack ();
(* Changed by compute_call_ref, called from process_call *)
@@ -325,7 +325,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Process the call according to the domain decision. *)
match Domain.start_call stmt call recursion domain_valuation state with
| `Value state ->
- Domain.Store.register_initial_state (Eva_utils.call_stack ()) 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
| `Bottom ->
{ states = []; cacheable = Cacheable; builtin=false }
@@ -534,7 +535,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Create an Eval.call *)
let create_call stmt kf args =
let return = Library_functions.get_retres_vi kf in
- let callstack = (kf, Kstmt stmt) :: Eva_utils.call_stack () in
+ let callstack = Callstack.push kf stmt (Eva_utils.current_call_stack ()) in
let arguments, rest =
let formals = Kernel_function.get_formals kf in
let rec format_arguments acc args formals = match args, formals with
@@ -728,8 +729,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Legacy callbacks for the cvalue domain, usually called by
{Cvalue_transfer.start_call}. *)
- let apply_cvalue_callback kf ki_call state =
- let stack_with_call = (kf, ki_call) :: Eva_utils.call_stack () in
+ let apply_cvalue_callback kf stmt state =
+ let call_stack = Eva_utils.current_call_stack () in
+ let stack_with_call = Callstack.push kf stmt call_stack in
let cvalue_state = get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
let kind = `Builtin None in
@@ -752,7 +754,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* The special Frama_C_ functions to print states are handled here. *)
if apply_special_directives ~subdivnb kf args state
then
- let () = apply_cvalue_callback kf ki_call state in
+ let () = apply_cvalue_callback kf stmt state in
[(Partition.Key.empty, state)]
else
(* Create the call. *)
diff --git a/src/plugins/eva/eval.ml b/src/plugins/eva/eval.ml
index f0c0403a672540d8c414d63a8cc17e95f64b69c4..c08bf95bb6c864b0ca6bf378c554ed7eb5fced51 100644
--- a/src/plugins/eva/eval.ml
+++ b/src/plugins/eva/eval.ml
@@ -239,13 +239,9 @@ type ('loc, 'value) argument = {
avalue: ('loc, 'value) assigned;
}
-
-type call_site = kernel_function * kinstr
-type callstack = call_site list
-
type ('loc, 'value) call = {
kf: kernel_function;
- callstack: callstack;
+ callstack: Callstack.t;
arguments: ('loc, 'value) argument list;
rest: (exp * ('loc, 'value) assigned) list;
return: varinfo option;
diff --git a/src/plugins/eva/eval.mli b/src/plugins/eva/eval.mli
index 08793e093b818ab4da6b4cdb5cceb3695db5d70f..cee30db5319525e4a12c72c0a2ad0e6a09d15824 100644
--- a/src/plugins/eva/eval.mli
+++ b/src/plugins/eva/eval.mli
@@ -223,21 +223,10 @@ type ('loc, 'value) argument = {
avalue: ('loc, 'value) assigned; (** The value of the concrete argument. *)
}
-(** A call_stack is a list, telling which function was called at which
- site. The head of the list tells about the latest call. *)
-
-(** A call site: the function called, and the call statement
- (or [Kglobal] for the main function. *)
-type call_site = kernel_function * kinstr
-
-(* A call stack is a list of call sites. The head is the latest call.
- The last element is the main function. *)
-type callstack = call_site list
-
(** A function call. *)
type ('loc, 'value) call = {
kf: kernel_function; (** The called function. *)
- callstack: callstack; (** The current callstack
+ callstack: Callstack.t; (** The current callstack
(with this call on top). *)
arguments: ('loc, 'value) argument list; (** The arguments of the call. *)
rest: (exp * ('loc, 'value) assigned) list; (** Extra-arguments. *)
diff --git a/src/plugins/eva/gui/gui_callstacks_filters.ml b/src/plugins/eva/gui/gui_callstacks_filters.ml
index c8817ff00aaa9c2f5b04f82d830492109e8ca0dd..f4af6ba1b8016f7529c2a4329364297781c4d420 100644
--- a/src/plugins/eva/gui/gui_callstacks_filters.ml
+++ b/src/plugins/eva/gui/gui_callstacks_filters.ml
@@ -22,17 +22,19 @@
open Cil_types
-type rcallstack = Value_types.callstack
+type rcallstack = (Cil_types.kernel_function * Cil_types.kinstr) list
let empty = []
-let from_callstack = List.rev
+let from_callstack cs = Callstack.to_call_list cs
let callstack_matches_callstack (rcs1:rcallstack) (rcs2:rcallstack) =
let rec aux q1 q2 = match q1, q2 with
| [], _ | _, [] -> true
- | call1 :: q1, call2 :: q2 ->
- Value_types.Callsite.equal call1 call2 && aux q1 q2
+ | (kf1, kinstr1) :: q1, (kf2, kinstr2) :: q2 ->
+ Kernel_function.equal kf1 kf2
+ && Cil_datatype.Kinstr.equal kinstr1 kinstr2
+ && aux q1 q2
in
aux rcs1 rcs2
@@ -62,7 +64,7 @@ let has_matching_callstack ~after csf stmt =
| `Bottom -> false
| `Value h ->
try
- Value_types.Callstack.Hashtbl.iter
+ Callstack.Hashtbl.iter
(fun cs' _state ->
let rcs' = from_callstack cs' in
if callstack_matches csf rcs' then raise Exit
@@ -95,7 +97,7 @@ let register_to_zone_functions (module Eval: Gui_eval.S) =
let eval_filter csf stmt ev v =
match Eval.Analysis.get_stmt_state_by_callstack ~after:false stmt with
| `Value h ->
- Value_types.Callstack.Hashtbl.fold
+ Callstack.Hashtbl.fold
(fun cs state acc ->
let rcs' = from_callstack cs in
if callstack_matches csf rcs' then
diff --git a/src/plugins/eva/gui/gui_callstacks_filters.mli b/src/plugins/eva/gui/gui_callstacks_filters.mli
index b5bb5924d36f560eafa26d4061520c2823145da0..39da15edb11ae559db931ffb99a84682c07c8da7 100644
--- a/src/plugins/eva/gui/gui_callstacks_filters.mli
+++ b/src/plugins/eva/gui/gui_callstacks_filters.mli
@@ -26,7 +26,7 @@
type rcallstack
val empty: rcallstack
-val from_callstack: Value_types.callstack -> rcallstack
+val from_callstack: Callstack.t -> rcallstack
(** Filters on callstacks. [None] means that all callstacks are active *)
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 25d985d9e4d77693633421bc8e3567105bd11f26..bc338ad9cd9f916018566fb902f00affa3b8defe 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -93,7 +93,7 @@ module type S = sig
type ('env, 'expr, 'v) evaluation_functions = {
eval_and_warn: 'env -> 'expr -> 'v * bool (* alarm *) * bool (* red *);
- env: Analysis.Dom.t -> Value_types.callstack -> 'env;
+ env: Analysis.Dom.t -> Callstack.t -> 'env;
equal: 'v -> 'v -> bool;
bottom: 'v;
join: 'v -> 'v -> 'v;
@@ -124,7 +124,7 @@ module type S = sig
val predicate_with_red:
gui_loc ->
- (Eval_terms.eval_env * (kinstr * Value_types.callstack),
+ (Eval_terms.eval_env * (kinstr * Callstack.t),
Red_statuses.alarm_or_property * predicate,
Eval_terms.predicate_status or_bottom
) evaluation_functions
@@ -152,7 +152,7 @@ module Make (X: Analysis.S) = struct
type ('env, 'expr, 'v) evaluation_functions = {
eval_and_warn: 'env -> 'expr -> 'v * bool * bool;
- env: X.Dom.t -> Value_types.callstack -> 'env;
+ env: X.Dom.t -> Callstack.t -> 'env;
equal: 'v -> 'v -> bool;
bottom: 'v;
join: 'v -> 'v -> 'v;
@@ -323,7 +323,7 @@ module Make (X: Analysis.S) = struct
match Db.Value.get_initial_state_callstack kf with
| None -> Cvalue.Model.top (* should not happen *)
| Some h ->
- try Value_types.Callstack.Hashtbl.find h callstack
+ try Callstack.Hashtbl.find h callstack
with Not_found -> Cvalue.Model.top (* should not happen either *)
let env_here kf here callstack =
@@ -355,8 +355,8 @@ module Make (X: Analysis.S) = struct
(* Maps from callstacks to Value states before and after a GUI location.
The 'after' map is not always available. *)
type states_by_callstack = {
- states_before: X.Dom.t Value_types.Callstack.Hashtbl.t or_top_bottom;
- states_after: X.Dom.t Value_types.Callstack.Hashtbl.t or_top_bottom;
+ states_before: X.Dom.t Callstack.Hashtbl.t or_top_bottom;
+ states_after: X.Dom.t Callstack.Hashtbl.t or_top_bottom;
}
let top_states_by_callstacks = { states_before = `Top; states_after = `Top }
@@ -542,7 +542,7 @@ module Make (X: Analysis.S) = struct
let make_data_all_callstacks_from_states ev ~before ~after expr =
let exn = ref [] in
- let single_callstack = (Value_types.Callstack.Hashtbl.length before) = 1 in
+ let single_callstack = (Callstack.Hashtbl.length before) = 1 in
let v_join_before = ref ev.bottom in
let v_join_after = ref ev.bottom in
let ok_join = ref true in
@@ -565,14 +565,14 @@ module Make (X: Analysis.S) = struct
let ev = { ev with eval_and_warn } in
(* Rows by callstack *)
let list =
- Value_types.Callstack.Hashtbl.fold
+ Callstack.Hashtbl.fold
(fun callstack before acc ->
let before = ev.env before callstack in
let after = match after with
| `Top | `Bottom as x -> x
| `Value after ->
try
- let after = Value_types.Callstack.Hashtbl.find after callstack in
+ let after = Callstack.Hashtbl.find after callstack in
`Value (ev.env after callstack)
(* If a callstack exists before the statement but is not found
after, then the post state for this callstack is bottom. *)
diff --git a/src/plugins/eva/gui/gui_eval.mli b/src/plugins/eva/gui/gui_eval.mli
index 31916a24c65376e536cebd2d9796e21e203f0b44..52be333c333b9f80a9fe5adf38fb87f9a486b5fb 100644
--- a/src/plugins/eva/gui/gui_eval.mli
+++ b/src/plugins/eva/gui/gui_eval.mli
@@ -61,7 +61,7 @@ module type S = sig
(** This is the record that encapsulates all evaluation functions *)
type ('env, 'expr, 'v) evaluation_functions = {
eval_and_warn: 'env -> 'expr -> 'v * bool (* alarm *) * bool (* red *);
- env: Analysis.Dom.t -> Value_types.callstack -> 'env;
+ env: Analysis.Dom.t -> Callstack.t -> 'env;
equal: 'v -> 'v -> bool;
bottom: 'v;
join: 'v -> 'v -> 'v;
@@ -108,7 +108,7 @@ module type S = sig
val predicate_with_red:
gui_loc ->
- (Eval_terms.eval_env * (kinstr * Value_types.callstack),
+ (Eval_terms.eval_env * (kinstr * Callstack.t),
Red_statuses.alarm_or_property * predicate,
Eval_terms.predicate_status Lattice_bounds.or_bottom
) evaluation_functions
diff --git a/src/plugins/eva/gui/gui_types.ml b/src/plugins/eva/gui/gui_types.ml
index 94f675343aa8ecb17515ad6137ae9596a5a033d3..3f989adaf5db8eb63d43507cab31ea63783d8d19 100644
--- a/src/plugins/eva/gui/gui_types.ml
+++ b/src/plugins/eva/gui/gui_types.ml
@@ -25,20 +25,20 @@ open Cil_types
type gui_callstack =
| GC_Filtered (* Some results have been hidden by a filter *)
| GC_Consolidated (* Join of all possible callstacks *)
- | GC_Single of Value_types.callstack (* Only one callstack possible here *)
- | GC_Callstack of Value_types.callstack (* One of multiple callstacks *)
+ | GC_Single of Callstack.t (* Only one callstack possible here *)
+ | GC_Callstack of Callstack.t (* One of multiple callstacks *)
let hash_gui_callstack = function
| GC_Filtered -> 0
| GC_Consolidated -> 1
- | GC_Single cs -> 2 * Value_types.Callstack.hash cs
- | GC_Callstack cs -> 4 * Value_types.Callstack.hash cs
+ | GC_Single cs -> 2 * Callstack.hash cs
+ | GC_Callstack cs -> 4 * Callstack.hash cs
let compare_gui_callstack cs1 cs2 = match cs1, cs2 with
| GC_Filtered, GC_Filtered -> 0
| GC_Consolidated, GC_Consolidated -> 0
| GC_Single cs1, GC_Single cs2 | GC_Callstack cs1, GC_Callstack cs2 ->
- Value_types.Callstack.compare cs1 cs2
+ Callstack.compare cs1 cs2
| _, GC_Filtered -> 1
| GC_Filtered, _ -> -1
| _, GC_Consolidated -> 1
@@ -227,44 +227,45 @@ let gui_loc_loc = function
let kf_of_gui_loc = function
| GL_Stmt (kf, _) | GL_Pre kf | GL_Post kf -> kf
+let pop_last_call cs =
+ match cs.Callstack.stack with
+ | (_, stmt) :: ((kf, _) :: _ as stack)-> Some (stmt, kf, { cs with stack })
+ | [_, stmt] -> Some (stmt, cs.entry_point, { cs with stack = [] })
+ | [] -> None
+
(* This pretty-printer drops the toplevel kf, which is always the function
in which we are pretty-printing the expression/term *)
let pretty_callstack fmt cs =
- match cs with
- | [_, Kglobal] -> ()
- | (_kf_cur, Kstmt callsite) :: q -> begin
- let rec aux callsite = function
- | (kf, callsite') :: q -> begin
- Format.fprintf fmt "%a (%a%t)"
- Kernel_function.pretty kf
- Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc callsite)
- (fun fmt ->
- if Gui_parameters.debug_atleast 1 then
- Format.fprintf fmt ", %d" callsite.sid);
- match callsite' with
- | Kglobal -> ()
- | Kstmt callsite' ->
- Format.fprintf fmt " â†@ ";
- aux callsite' q
- end
- | _ -> assert false
- in
- Format.fprintf fmt "@[<hv>%a" Value_types.Callstack.pretty_hash cs;
- aux callsite q;
- Format.fprintf fmt "@]"
- end
- | _ -> assert false
+ match pop_last_call cs with
+ | None -> ()
+ | Some (stmt, caller, q) ->
+ let rec aux stmt caller cs =
+ Format.fprintf fmt "%a (%a%t)"
+ Kernel_function.pretty caller
+ Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc stmt)
+ (fun fmt ->
+ if Gui_parameters.debug_atleast 1 then
+ Format.fprintf fmt ", %d" stmt.sid);
+ match pop_last_call cs with
+ | None -> ()
+ | Some (stmt, caller, q) ->
+ Format.fprintf fmt " â†@ ";
+ aux stmt caller q
+ in
+ Format.fprintf fmt "@[<hv>%a" Callstack.pretty_hash cs;
+ aux stmt caller q;
+ Format.fprintf fmt "@]"
(* This pretty-printer prints only the lists of the functions, not
the locations *)
let pretty_callstack_short fmt cs =
- match cs with
- | [_, Kglobal] -> ()
- | (_kf_cur, Kstmt _callsite) :: q ->
- Format.fprintf fmt "%a" Value_types.Callstack.pretty_hash cs;
+ match Callstack.pop cs with
+ | None -> ()
+ | Some q ->
+ Format.fprintf fmt "%a" Callstack.pretty_hash cs;
+ let list = List.rev (Callstack.to_kf_list q) in
Pretty_utils.pp_flowlist ~left:"@[" ~sep:" â†@ " ~right:"@]"
- (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt q
- | _ -> assert false
+ Kernel_function.pretty fmt list
(*
diff --git a/src/plugins/eva/gui/gui_types.mli b/src/plugins/eva/gui/gui_types.mli
index e4d5018d9c10a678c9a4c719d470f9280ff5d719..04b713cd82aa5d8f73ccb4d14baa58a38cbeddfe 100644
--- a/src/plugins/eva/gui/gui_types.mli
+++ b/src/plugins/eva/gui/gui_types.mli
@@ -23,8 +23,8 @@
type gui_callstack =
| GC_Filtered
| GC_Consolidated
- | GC_Single of Value_types.callstack
- | GC_Callstack of Value_types.callstack
+ | GC_Single of Callstack.t
+ | GC_Callstack of Callstack.t
val hash_gui_callstack : gui_callstack -> int
val compare_gui_callstack : gui_callstack -> gui_callstack -> int
@@ -69,9 +69,9 @@ val gui_loc_loc : gui_loc -> Cil_types.location
val kf_of_gui_loc : gui_loc -> Cil_types.kernel_function
val pretty_callstack :
- Format.formatter -> Value_types.callstack -> unit
+ Format.formatter -> Callstack.t -> unit
val pretty_callstack_short :
- Format.formatter -> Value_types.callstack -> unit
+ Format.formatter -> Callstack.t -> unit
type 'a gui_res =
| GR_Empty
diff --git a/src/plugins/eva/legacy/eval_annots.ml b/src/plugins/eva/legacy/eval_annots.ml
index 6ce1404d2491364dfcf653b5435a65fe4e865778..ca814b26cfbc3252f2e1a491436c22efa230b1e5 100644
--- a/src/plugins/eva/legacy/eval_annots.ml
+++ b/src/plugins/eva/legacy/eval_annots.ml
@@ -117,7 +117,7 @@ let c_labels kf cs =
if stmt.labels != [] then
try
let hstate = Db.Value.Table_By_Callstack.find stmt in
- let state = Value_types.Callstack.Hashtbl.find hstate cs in
+ let state = Callstack.Hashtbl.find hstate cs in
Cil_datatype.Logic_label.Map.add (StmtLabel (ref stmt)) state acc
with Not_found -> acc
else acc
@@ -143,7 +143,7 @@ let eval_by_callstack kf stmt p =
Unknown
| Some states ->
try
- match Value_types.Callstack.Hashtbl.fold aux_callstack states `Bottom with
+ match Callstack.Hashtbl.fold aux_callstack states `Bottom with
| `Bottom -> Eval_terms.Unknown (* probably never reached *)
| `Value status -> status
with Exit -> Eval_terms.Unknown
diff --git a/src/plugins/eva/legacy/eval_annots.mli b/src/plugins/eva/legacy/eval_annots.mli
index e6e9691cce40c3c99ee614e85f5adad33f51651d..bb4b33cac7a70b9ffb9fa0d2fb474bff0b2ee8aa 100644
--- a/src/plugins/eva/legacy/eval_annots.mli
+++ b/src/plugins/eva/legacy/eval_annots.mli
@@ -26,4 +26,4 @@ val has_requires: spec -> bool
val mark_invalid_initializers: unit -> unit
val mark_unreachable: unit -> unit
val mark_green_and_red: unit -> unit
-val c_labels: kernel_function -> Value_types.callstack -> Eval_terms.labels_states
+val c_labels: kernel_function -> Callstack.t -> Eval_terms.labels_states
diff --git a/src/plugins/eva/types/callstack.ml b/src/plugins/eva/types/callstack.ml
new file mode 100644
index 0000000000000000000000000000000000000000..160bfd2d48e272a3ee48bbc0de225a1994ea53f5
--- /dev/null
+++ b/src/plugins/eva/types/callstack.ml
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Eva_types.Callstack
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9e4a7654bbf600985ea25750c94a9dbd0ccc8767
--- /dev/null
+++ b/src/plugins/eva/types/callstack.mli
@@ -0,0 +1,92 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+[@@@ api_start]
+[@@@ alert "-db_deprecated"]
+
+(** A call is identified by the function called and the call statement *)
+type call = Cil_types.kernel_function * Cil_types.stmt
+
+module Call : Datatype.S with type t = call
+
+(** Eva callstacks. *)
+type callstack = Eva_types.Callstack.callstack = {
+ thread: int;
+ (* An identifier of the thread's callstack. *)
+ entry_point: Cil_types.kernel_function;
+ (** The first function function of the callstack. *)
+ stack: call list;
+ (** A call stack is a list of calls. The head is the latest call. *)
+}
+
+include Datatype.S_with_collections
+ with type t = callstack
+ and module Hashtbl = Eva_types.Callstack.Hashtbl
+
+(** Prints a callstack without displaying call sites. *)
+val pretty_short : Format.formatter -> t -> unit
+
+(** Prints a hash of the callstack when '-kernel-msg-key callstack'
+ is enabled (prints nothing otherwise). *)
+val pretty_hash : Format.formatter -> t -> unit
+
+(** [compare_lex] compares callstack lexicographically, slightly slower
+ than [compare] but in a more natural order, giving more importance
+ to the function at bottom of the callstack - the first functions called. *)
+val compare_lex : t -> t -> int
+
+(*** {2 Stack manipulation} *)
+
+(*** Constructor *)
+val init : ?thread:int -> Cil_types.kernel_function -> t
+
+(** Adds a new call to the top of the callstack. *)
+val push : Cil_types.kernel_function -> Cil_types.stmt -> t -> t
+
+(** Removes the topmost call from the callstack. *)
+val pop : t -> 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.kinstr
+val top_call : t -> Cil_types.kernel_function * Cil_types.kinstr
+
+(** Returns the function that called the topmost function of the callstack. *)
+val top_caller : t -> Cil_types.kernel_function option
+
+(** {2 Conversion} *)
+
+(** Gives the list of kf in the callstack from the entry point to the top of the
+ callstack (i.e. reverse order of the call stack). *)
+val to_kf_list : t -> Cil_types.kernel_function list
+
+(** Gives the list of call statements from the bottom to the top of the
+ callstack (i.e. reverse order of the call stack). *)
+val to_stmt_list : t -> Cil_types.stmt list
+
+(** Gives the list of call from the bottom to the top of the callstack
+ (i.e. reverse order of the call stack). *)
+val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
+
+[@@@ api_end]
+
+val pretty_debug : Format.formatter -> t -> unit
diff --git a/src/plugins/eva/utils/cvalue_callbacks.ml b/src/plugins/eva/utils/cvalue_callbacks.ml
index c8fcd6074d88d87f531d5cbff03c3d9d205b0d0c..e1843e4c1f7c09e2264b40778cc66f0cf90c3602 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.ml
+++ b/src/plugins/eva/utils/cvalue_callbacks.ml
@@ -24,7 +24,6 @@ open Cil_types
let dkey = Self.dkey_callbacks
-type callstack = (kernel_function * kinstr) list
type state = Cvalue.Model.t
type analysis_kind =
@@ -35,7 +34,7 @@ type analysis_kind =
module Call =
Hook.Build
- (struct type t = callstack * kernel_function * analysis_kind * state end)
+ (struct type t = Callstack.t * kernel_function * analysis_kind * state end)
let register_call_hook f =
Call.extend (fun (callstack, kf, kind, state) -> f callstack kf kind state)
@@ -53,7 +52,7 @@ type call_results =
| Reuse of int
module Call_Results =
- Hook.Build (struct type t = callstack * kernel_function * call_results end)
+ Hook.Build (struct type t = Callstack.t * kernel_function * call_results end)
let register_call_results_hook f =
Call_Results.extend (fun (callstack, kf, results) -> f callstack kf results)
@@ -74,7 +73,7 @@ let apply_call_results_hooks callstack kf call_results =
module Statement =
- Hook.Build (struct type t = callstack * stmt * state list end)
+ Hook.Build (struct type t = Callstack.t * stmt * state list end)
let register_statement_hook f =
Statement.extend (fun (callstack, stmt, states) -> f callstack stmt states)
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index abc2408b9ec12f4e3b05aa3e0a1eab2a55d6c873..2d93d634a4d0f18dbce55cce70826734c0377c2a 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.mli
+++ b/src/plugins/eva/utils/cvalue_callbacks.mli
@@ -28,7 +28,6 @@
in a future version. Please contact us if you need to register callbacks
to be executed during an Eva analysis. *)
-type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
type state = Cvalue.Model.t
type analysis_kind =
@@ -42,7 +41,7 @@ type analysis_kind =
the function called, the kind of analysis performed by Eva for this call,
and the cvalue state at the beginning of the call. *)
val register_call_hook:
- (callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit)
+ (Callstack.t -> Cil_types.kernel_function -> analysis_kind -> state -> unit)
-> unit
@@ -62,17 +61,17 @@ type call_results =
function call. Arguments of the callback are the callstack of the call,
the function called and the cvalue states resulting from its analysis. *)
val register_call_results_hook:
- (callstack -> Cil_types.kernel_function -> call_results -> unit)
+ (Callstack.t -> Cil_types.kernel_function -> call_results -> unit)
-> unit
[@@@ api_end]
val register_statement_hook:
- (callstack -> Cil_types.stmt -> state list -> unit) -> unit
+ (Callstack.t -> Cil_types.stmt -> state list -> unit) -> unit
val apply_call_hooks:
- callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit
+ Callstack.t -> Cil_types.kernel_function -> analysis_kind -> state -> unit
val apply_call_results_hooks:
- callstack -> Cil_types.kernel_function -> call_results -> unit
+ Callstack.t -> Cil_types.kernel_function -> call_results -> unit
val apply_statement_hooks:
- callstack -> Cil_types.stmt -> state list -> unit
+ Callstack.t -> Cil_types.stmt -> state list -> unit
diff --git a/src/plugins/eva/utils/eva_perf.ml b/src/plugins/eva/utils/eva_perf.ml
index 1efc3d7c32ab56ef25903adfc736f74add3278af..4c0ae010c6ff1309e2e1fd7e93d48f702691b2bf 100644
--- a/src/plugins/eva/utils/eva_perf.ml
+++ b/src/plugins/eva/utils/eva_perf.ml
@@ -218,7 +218,8 @@ module Imperative_callstack_trie(M:sig type t val default:unit -> t end) = struc
n
in find_subtree subnode.subtree b (Some subnode)
- let find_subtree t callstack = find_subtree t (List.rev callstack) None
+ let find_subtree t callstack =
+ find_subtree t (Callstack.to_call_list callstack) None
let find t callstack = (find_subtree t callstack).self
@@ -285,25 +286,25 @@ let display fmt =
end
;;
-let caller_callee_callinfo = function
- | (callee_kf,_)::(caller_kf,_)::_ ->
- (let caller_flat = Kernel_function.Hashtbl.find flat caller_kf in
- try
+let caller_callee_callinfo callstack =
+ match Callstack.top_caller callstack with
+ | Some caller_kf ->
+ let callee_kf = Callstack.top_kf callstack in
+ let caller_flat = Kernel_function.Hashtbl.find flat caller_kf in
+ (try
Kernel_function.Hashtbl.find caller_flat.called_functions callee_kf
with Not_found ->
let call_info = Call_info.create() in
Kernel_function.Hashtbl.add caller_flat.called_functions callee_kf call_info;
call_info)
- | [_] -> Call_info.main
- | [] -> assert false
+ | None -> Call_info.main
;;
let start_doing_perf callstack =
if Parameters.ValShowPerf.get()
then begin
let time = Sys.time() in
- assert (callstack != []);
- let kf = fst (List.hd callstack) in
+ let kf = Callstack.top_kf callstack in
let flat_info =
try Kernel_function.Hashtbl.find flat kf
with Not_found ->
@@ -325,7 +326,7 @@ let stop_doing_perf callstack =
if Parameters.ValShowPerf.get()
then begin
let time = Sys.time() in
- let kf = fst (List.hd callstack) in
+ let kf = Callstack.top_kf callstack in
let flat_info = Kernel_function.Hashtbl.find flat kf in
Call_info.after_call flat_info.call_info time;
let node = Perf_by_callstack.find perf callstack in
@@ -365,14 +366,13 @@ let stack_flamegraph = ref []
(* pretty-prints the functions in a Value callstack, starting by main (i.e.
in reverse order). *)
-let pretty_callstack oc l =
+let pretty_callstack oc callstack =
let rec aux oc = function
| [] -> () (* does not happen in theory *)
- | [main, _] -> Printf.fprintf oc "%s" (Kernel_function.get_name main)
- | (f, _) :: q ->
- Printf.fprintf oc "%a;%s" aux q (Kernel_function.get_name f)
+ | [main] -> Printf.fprintf oc "%s" (Kernel_function.get_name main)
+ | kf :: q -> Printf.fprintf oc "%s;%a" (Kernel_function.get_name kf) aux q
in
- aux oc l
+ aux oc (Callstack.to_kf_list callstack)
(* update the [self_total_time] information for the function being analyzed,
assuming that the current time is [time] *)
@@ -385,9 +385,8 @@ let update_self_total_time time =
(* called when a new function is being analyzed *)
let start_doing_flamegraph callstack =
- match callstack with
- | [] -> assert false
- | [_] ->
+ match callstack.Callstack.stack with
+ | [] ->
(* Analysis of main *)
if not (Parameters.ValPerfFlamegraphs.is_empty ()) then begin
let file = Parameters.ValPerfFlamegraphs.get () in
@@ -401,7 +400,7 @@ let start_doing_flamegraph callstack =
(Printexc.to_string e);
oc_flamegraph := None (* to be on the safe side *)
end
- | _ :: _ :: _ ->
+ | _ :: _ ->
if !oc_flamegraph <> None then
(* Flamegraphs are being computed. Update time spent in current function
so far, then push a slot for the analysis of the new function *)
diff --git a/src/plugins/eva/utils/eva_perf.mli b/src/plugins/eva/utils/eva_perf.mli
index 2c0a2edd183946a7d6970bd7139e2560a7f62ec5..cb4a2af9a1eb768e56c5e454594206e1ef4b0fdf 100644
--- a/src/plugins/eva/utils/eva_perf.mli
+++ b/src/plugins/eva/utils/eva_perf.mli
@@ -22,11 +22,11 @@
(** Call [start_doing] when starting analyzing a new function. The new
function is on the top of the call stack.*)
-val start_doing: Value_types.callstack -> unit
+val start_doing: Callstack.t -> unit
(** Call [start_doing] when finishing analyzing a function. The
function must still be on the top of the call stack. *)
-val stop_doing: Value_types.callstack -> unit
+val stop_doing: Callstack.t -> unit
(** Display a complete summary of performance informations. Can be
called during the analysis. *)
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index 7bd81b39928f5550e41c6a0a6d3a2265afe3fc2d..7b7d2b98ddf18c4f3ae8d33b2b647abbebba07b1 100644
--- a/src/plugins/eva/utils/eva_results.ml
+++ b/src/plugins/eva/utils/eva_results.ml
@@ -35,7 +35,7 @@ let partition_terminating_instr stmt =
let terminating = ref [] in
let non_terminating = ref [] in
let add x xs = xs := x :: !xs in
- Value_types.Callstack.Hashtbl.iter (fun cs state ->
+ Callstack.Hashtbl.iter (fun cs state ->
if Db.Value.is_reachable state
then add cs terminating
else add cs non_terminating) h;
@@ -49,7 +49,7 @@ let is_non_terminating_instr stmt =
(* {2 Saving and restoring state} *)
-type stmt_by_callstack = Cvalue.Model.t Value_types.Callstack.Hashtbl.t
+type stmt_by_callstack = Cvalue.Model.t Callstack.Hashtbl.t
module AlarmsStmt =
Datatype.Pair_with_collections (Alarms) (Stmt)
@@ -72,7 +72,7 @@ type results = {
let get_results () =
let vue = Emitter.get Eva_utils.emitter in
let main = Some (fst (Globals.entry_point ())) in
- let module CS = Value_types.Callstack in
+ let module CS = Callstack in
let copy_states iter =
let h = Stmt.Hashtbl.create 128 in
let copy stmt hstack = Stmt.Hashtbl.add h stmt (CS.Hashtbl.copy hstack) in
@@ -144,16 +144,16 @@ let set_results results =
let aux_callstack callstack state =
Db.Value.update_callstack_table ~after stmt callstack state;
in
- Value_types.Callstack.Hashtbl.iter aux_callstack h
+ Callstack.Hashtbl.iter aux_callstack h
in
Stmt.Hashtbl.iter (aux_states ~after:false) results.before_states;
Stmt.Hashtbl.iter (aux_states ~after:true) results.after_states;
(* Kf initial state *)
- let aux_initial_state _kf h =
+ let aux_initial_state kf h =
let aux_callstack callstack state =
- Db.Value.merge_initial_state callstack state
+ Db.Value.merge_initial_state callstack kf state
in
- Value_types.Callstack.Hashtbl.iter aux_callstack h
+ Callstack.Hashtbl.iter aux_callstack h
in
Kernel_function.Hashtbl.iter aux_initial_state results.kf_initial_states;
Function_calls.set_results results.kf_callers;
@@ -204,7 +204,7 @@ struct
end
-module CallstackH = HExt(Value_types.Callstack.Hashtbl)
+module CallstackH = HExt(Callstack.Hashtbl)
module StmtH = HExt(Stmt.Hashtbl)
module KfH = HExt(Kernel_function.Hashtbl)
module PropertyH = HExt(Property.Hashtbl)
diff --git a/src/plugins/eva/utils/eva_results.mli b/src/plugins/eva/utils/eva_results.mli
index bc5d4c7d8cd7cf276098184a9abb3b4a94b27bf3..ee688e7b7d7dc4e997c3fa22aaf592d847bcf79c 100644
--- a/src/plugins/eva/utils/eva_results.mli
+++ b/src/plugins/eva/utils/eva_results.mli
@@ -44,7 +44,7 @@ val merge: results -> results -> results
For technical reasons, the top of the callstack must currently
be preserved. *)
val change_callstacks:
- (Value_types.callstack -> Value_types.callstack) -> results -> results
+ (Callstack.t -> Callstack.t) -> results -> results
val eval_tlval_as_location :
?result:Cil_types.varinfo ->
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 7dbc948a1e05968b67aeee3d0ae3c17ccae81c3e..73dc03924ed0497f7e611994aeb9631803134333 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -22,35 +22,53 @@
open Cil_types
-(* Callstacks related types and functions *)
+(* Callstacks related functions *)
-let call_stack : Value_types.callstack ref = ref []
-(* let call_stack_for_callbacks : (kernel_function * kinstr) list ref = ref [] *)
+let current_callstack : Callstack.t option ref = ref None
let clear_call_stack () =
- call_stack := []
-
-let pop_call_stack () =
- Eva_perf.stop_doing !call_stack;
- call_stack := List.tl !call_stack
-;;
-
-let push_call_stack kf ki =
- call_stack := (kf,ki) :: !call_stack;
- Eva_perf.start_doing !call_stack
-;;
-
+ match !current_callstack with
+ | None -> ()
+ | Some cs ->
+ Eva_perf.stop_doing cs;
+ current_callstack := None
+
+let init_call_stack kf =
+ assert (!current_callstack = None);
+ let cs = Callstack.init kf in
+ current_callstack := Some cs;
+ Eva_perf.start_doing cs;
+ cs
+
+let current_call_stack_opt () = !current_callstack
+
+let current_call_stack () =
+ match !current_callstack with
+ | None -> Self.fatal "Callstack not initialized"
+ | Some cs -> cs
let current_kf () =
- let (kf,_) = (List.hd !call_stack) in kf;;
+ let cs = current_call_stack () in
+ Callstack.top_kf cs
-let call_stack () = !call_stack
+let push_call_stack kf stmt =
+ let cs = current_call_stack () in
+ let new_cs = Callstack.push kf stmt cs in
+ current_callstack := Some new_cs;
+ Eva_perf.start_doing new_cs
+
+let pop_call_stack () =
+ let cs = current_call_stack () in
+ Eva_perf.stop_doing cs;
+ current_callstack := Callstack.pop cs
let pp_callstack fmt =
if Parameters.PrintCallstacks.get () then
- Format.fprintf fmt "@ stack: %a"
- Value_types.Callstack.pretty (call_stack())
-;;
+ match !current_callstack with
+ | None -> () (* Stack not initialized; happens when handling global initializations *)
+ | Some cs ->
+ Format.fprintf fmt "@ stack: %a" Callstack.pretty cs
+
(* Assertions emitted during the analysis *)
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index e02e47c866017db14b252a76791b8f7cf046af87..2e3ab131c5c85d921a2eecf7bc1d6fa42912b002 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -25,13 +25,31 @@ open Cil_types
(** {2 Callstacks related types and functions} *)
(** Functions dealing with call stacks. *)
+
+(** Clears the current callstack: future accesses to the current callstack
+ will fail. *)
val clear_call_stack : unit -> unit
+
+(** Initializes the current callstack with the main entry point. *)
+val init_call_stack : kernel_function -> Callstack.t
+
+(** Push a new call to the current callstack. *)
+val push_call_stack : kernel_function -> stmt -> unit
+
+(** Removes the topmost call from the current callstack. *)
val pop_call_stack : unit -> unit
-val push_call_stack : kernel_function -> kinstr -> unit
-(** The current function is the one on top of the call stack. *)
+(** Returns the current function, at the top of the current callstack.
+ Fails if no callstack has been initialized. This should only be called
+ during the analysis of a function. *)
val current_kf : unit -> kernel_function
-val call_stack : unit -> Value_types.callstack
+
+(** Returns the current callstack; fails if it has not been initialized.
+ This should only be called during the analysis of a function. *)
+val current_call_stack : unit -> Callstack.t
+
+(** Returns the current callstack, or [None] if it has not been initialized. *)
+val current_call_stack_opt : unit -> Callstack.t option
(** Prints the current callstack. *)
val pp_callstack : Format.formatter -> unit
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index ee1b6d4caa868e1bf5e81dd531e13f9ef9403472..bb7d45ac49ff7e8a7bad98b07171ae33ef87585b 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -28,6 +28,7 @@ module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
module Domain_builder = Domain_builder
module Eva_dynamic = Eva_dynamic
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index 36d0eb3b8ce5419317d81c0adbe116529dbec7f3..8fb57decf5b6c805f6776917c96f537c42709bc1 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -32,6 +32,7 @@ module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
module Domain_builder = Domain_builder
module Eva_dynamic = Eva_dynamic
diff --git a/src/plugins/eva/utils/red_statuses.ml b/src/plugins/eva/utils/red_statuses.ml
index dac25fbeb277d1236cb19281984c73c50a17f611..af80f2255c20882ec87a421a26b08ac8a7ddebc2 100644
--- a/src/plugins/eva/utils/red_statuses.ml
+++ b/src/plugins/eva/utils/red_statuses.ml
@@ -51,7 +51,9 @@ module AlarmOrProp = Datatype.Make_with_collections(struct
| Prop p -> 175 + Property.hash p
end)
-module Callstacks = Value_types.Callstack.Set
+module Info = struct let module_name = "CallstackOption" end
+module CallstackOption = Datatype.Option_with_collections (Callstack) (Info)
+module Callstacks = CallstackOption.Set
(* For each alarm or predicate, stores the set of callstacks for which it was
evaluated to False. *)
@@ -81,7 +83,8 @@ let add_red_ap kinstr ap =
try AlarmOrProp.Map.find ap current_map
with Not_found -> Callstacks.empty
in
- let new_callstacks = Callstacks.add (Eva_utils.call_stack ()) callstacks in
+ let new_callstacks =
+ Callstacks.add (Eva_utils.current_call_stack_opt ()) callstacks in
let new_map = AlarmOrProp.Map.add ap new_callstacks current_map in
RedStatusesTable.replace kinstr new_map;
Hook.apply ap
@@ -122,7 +125,7 @@ let is_red_in_callstack kinstr ap callstack =
try
let map = RedStatusesTable.find kinstr in
let callstacks = AlarmOrProp.Map.find ap map in
- Callstacks.mem callstack callstacks
+ Callstacks.mem (Some callstack) callstacks
with Not_found -> false
let get_all () =
diff --git a/src/plugins/eva/utils/red_statuses.mli b/src/plugins/eva/utils/red_statuses.mli
index d18cb14e1eb2b111a201654375f5d72a56540170..12ad7c0588ce8a549193d153bb8f8f5e8d17d807 100644
--- a/src/plugins/eva/utils/red_statuses.mli
+++ b/src/plugins/eva/utils/red_statuses.mli
@@ -40,7 +40,7 @@ val is_red: Property.t -> bool
(* Whether a red status has been emitted for an alarm or a property at the given
kinstr in the given callstack. *)
val is_red_in_callstack:
- kinstr -> alarm_or_property -> Value_types.callstack -> bool
+ kinstr -> alarm_or_property -> Callstack.t -> bool
(* Returns the unsorted list of all alarms and properties for which a red status
has been emitted during the analysis. Also returns the kinstr of the alarm or
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index 2d048a8995e6b381a6c223c74ea543cf108c16be..bc78a896d00c381e9616a2a675b4f7a6b3152029 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -28,10 +28,7 @@ let are_available kf =
| Analyzed (Complete | Partial) -> true
| SpecUsed | Builtin _ | Unreachable | Analyzed NoResults -> false
-module Callstack = Value_types.Callstack
-
-type callstack = Callstack.t
-type 'a by_callstack = (callstack * 'a) list
+type 'a by_callstack = (Callstack.t * 'a) list
type control_point =
| Initial
@@ -41,8 +38,8 @@ type control_point =
type context = {
control_point : control_point;
- selector : callstack list option;
- filter: (callstack -> bool) list;
+ selector : Callstack.t list option;
+ filter: (Callstack.t -> bool) list;
}
type request =
@@ -133,7 +130,7 @@ struct
| `Value state -> ByCallstack [cs,state]
let by_callstack : context ->
- [< `Bottom | `Top | `Value of 'a Value_types.Callstack.Hashtbl.t ] ->
+ [< `Bottom | `Top | `Value of 'a Callstack.Hashtbl.t ] ->
('a, restricted_to_callstack) t =
fun req -> function
| `Top -> Top
@@ -149,13 +146,13 @@ struct
(* Accessors *)
- let callstacks : ('a, restricted_to_callstack) t -> callstack list = function
+ let callstacks: ('a, restricted_to_callstack) t -> Callstack.t list = function
| Top | Bottom -> [] (* What else to do when Top is given ? *)
| ByCallstack l -> List.map fst l
(* Fold *)
- let fold (f : callstack -> 'a -> 'b -> 'b) (acc : 'b) :
+ let fold (f : Callstack.t -> 'a -> 'b -> 'b) (acc : 'b) :
('a, restricted_to_callstack) t -> 'b =
function
| Top | Bottom -> acc (* What else to do when Top is given ? *)
@@ -245,7 +242,8 @@ struct
A.get_stmt_state_by_callstack ?selection ~after:true stmt
|> by_callstack ctx
| Initial ->
- A.get_global_state () |> singleton []
+ let cs = Callstack.init (fst (Globals.entry_point ())) in
+ A.get_global_state () |> singleton cs
| Start kf ->
A.get_initial_state_by_callstack ?selection kf |> by_callstack ctx
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index eb362d580b9c100f1c60c2057e8dd5d866e5415b..122dfe95a676937703d5ddf4261f7a88147923c1 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -63,8 +63,6 @@
all requests in the function will lead to a Top error. *)
val are_available : Cil_types.kernel_function -> bool
-type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
-
type request
type value
@@ -127,16 +125,16 @@ val in_cvalue_state : Cvalue.Model.t -> request
(** Only consider the given callstack.
Replaces previous calls to [in_callstack] or [in_callstacks]. *)
-val in_callstack : callstack -> request -> request
+val in_callstack : Callstack.t -> request -> request
(** Only consider the callstacks from the given list.
Replaces previous calls to [in_callstack] or [in_callstacks]. *)
-val in_callstacks : callstack list -> request -> request
+val in_callstacks : Callstack.t list -> request -> request
(** Only consider callstacks satisfying the given predicate. Several filters
can be added. If callstacks are also selected with [in_callstack] or
[in_callstacks], only the selected callstacks will be filtered. *)
-val filter_callstack : (callstack -> bool) -> request -> request
+val filter_callstack : (Callstack.t -> bool) -> request -> request
(** Working with callstacks *)
@@ -146,11 +144,11 @@ val filter_callstack : (callstack -> bool) -> request -> request
reached by the analysis, or if no information has been saved at this point
(for instance with the -eva-no-results option).
Use [is_empty request] to distinguish these two cases. *)
-val callstacks : request -> callstack list
+val callstacks : request -> Callstack.t list
(** Returns a list of subrequests for each reachable callstack from
the given request. *)
-val by_callstack : request -> (callstack * request) list
+val by_callstack : request -> (Callstack.t * request) list
(** State requests *)
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 3d84dfa8af17e98be504a70776c3cd68e2fc023c..791a86676b1e06340b141955ee0a9d4c7ac72bc7 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -66,7 +66,7 @@ let record_callwise_dependencies_in_db call_site froms =
let call_for_individual_froms callstack _kf call_type value_initial_state =
if From_parameters.ForceCallDeps.get () then begin
- let current_function, call_site = List.hd callstack in
+ let current_function, call_site = Eva.Callstack.top_call callstack in
let register_from froms =
record_callwise_dependencies_in_db call_site froms;
match !call_froms_stack with
@@ -102,7 +102,7 @@ let call_for_individual_froms callstack _kf call_type value_initial_state =
end
let end_record call_stack froms =
- let (current_function_value, call_site) = List.hd call_stack in
+ let current_function_value, call_site = Eva.Callstack.top_call call_stack in
record_callwise_dependencies_in_db call_site froms;
(* pop + record in top of stack the froms of function that just finished *)
match !call_froms_stack with
diff --git a/src/plugins/inout/cumulative_analysis.ml b/src/plugins/inout/cumulative_analysis.ml
index 02490caad65bd6a940c807d6c1ee97abda12ecfb..9fd6d8dcfe08947ead6ec1cc3ed539dfc867a6cc 100644
--- a/src/plugins/inout/cumulative_analysis.ml
+++ b/src/plugins/inout/cumulative_analysis.ml
@@ -39,9 +39,9 @@ let specialize_state_on_call ?stmt kf =
match stmt with
| None -> Eva.Results.(at_start_of kf |> get_cvalue_model)
| Some stmt ->
- let filter = function
- | (_, Kstmt s) :: _ -> Cil_datatype.Stmt.equal s stmt
- | _ -> false
+ let filter = fun cs -> match Eva.Callstack.top_callsite cs with
+ | Kstmt s -> Cil_datatype.Stmt.equal s stmt
+ | Kglobal -> false
in
Eva.Results.(at_start_of kf |> filter_callstack filter |> get_cvalue_model)
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index d3240b5f5a6713dccf230a2a31951d017fd9c6b1..055cedeea1a352bad1fae4b51ee301bf9ce99943 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -207,13 +207,16 @@ module Internals =
let size = 17
end)
-module CallsiteHash = Value_types.Callsite.Hashtbl
+module Callsite =
+ Datatype.Pair_with_collections (Kernel_function) (Cil_datatype.Kinstr)
+ (struct let module_name = "From.Callsite" end)
+module CallsiteHash = Callsite.Hashtbl
(* Results of an an entire call, represented by a pair (stmt, kernel_function).
*)
module CallwiseResults =
State_builder.Hashtbl
- (Value_types.Callsite.Hashtbl)
+ (Callsite.Hashtbl)
(Inout_type)
(struct
let size = 17
@@ -569,7 +572,7 @@ module Callwise = struct
let call_inout_stack = ref []
let call_for_callwise_inout callstack _kf call_type state =
- let (current_function, ki as call_site) = List.hd callstack in
+ let current_function, ki as call_site = Eva.Callstack.top_call callstack in
let merge_inout inout =
Db.Operational_inputs.Record_Inout_Callbacks.apply (callstack, inout);
if ki = Kglobal
@@ -618,8 +621,7 @@ module Callwise = struct
let end_record call_stack inout =
merge_local_table_in_global_ones (snd (List.hd !call_inout_stack));
-
- let (current_function, _ as call_site) = List.hd call_stack in
+ let (current_function, _) as call = Eva.Callstack.top_call call_stack in
(* pop + record in top of stack the inout of function that just finished*)
match !call_inout_stack with
| (current_function2, _) :: (((_caller, table) :: _) as tail) ->
@@ -628,10 +630,10 @@ module Callwise = struct
Kernel_function.pretty current_function (* g *)
Kernel_function.pretty current_function2 (* f *);
call_inout_stack := tail;
- merge_call_in_local_table call_site table inout;
+ merge_call_in_local_table call table inout;
| _ -> (* the entry point, probably *)
- merge_call_in_global_tables call_site inout;
+ merge_call_in_global_tables call inout;
call_inout_stack := [];
CallwiseResults.mark_as_computed ()
diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index 3d35dd91f99e0642024a0478f144c252abeb9464..176678b5e498016794add8061f174db1042246fd 100644
--- a/src/plugins/nonterm/nonterm_run.ml
+++ b/src/plugins/nonterm/nonterm_run.ml
@@ -91,17 +91,16 @@ let pretty_stmt_kind fmt stmt =
let pp_numbered_stacks fmt callstacks =
if List.length callstacks < 2 then
Format.fprintf fmt "stack: %a"
- (Pretty_utils.pp_list ~sep:": " Value_types.Callstack.pretty) callstacks
+ (Pretty_utils.pp_list ~sep:": " Eva.Callstack.pretty) callstacks
else
(* number callstacks *)
let numbered_callstacks =
- let count = ref 0 in
- List.map (fun cs -> incr count; (!count, cs)) callstacks
+ List.mapi (fun i cs -> (i+1, cs)) callstacks
in
Format.fprintf fmt "%a"
(Pretty_utils.pp_list ~sep:"@\n"
(Pretty_utils.pp_pair ~pre:"stack " ~sep:": "
- Format.pp_print_int Value_types.Callstack.pretty))
+ Format.pp_print_int Eva.Callstack.pretty))
numbered_callstacks
let wkey_stmt = Self.register_warn_category "stmt"
@@ -306,21 +305,6 @@ let collect_nonterminating_statements fd nonterm_stacks =
) vis#get_instr_stmts;
!new_nonterm_stmts
-let rec cmp_callstacks_aux cs1 cs2 =
- match cs1, cs2 with
- | [], [] -> 0
- | [], _ -> -1
- | _, [] -> 1
- | (kf1, ki1) :: r1, (kf2, ki2) :: r2 ->
- let c = Cil_datatype.Kinstr.compare ki1 ki2 in
- if c <> 0 then c else
- let c = Kernel_function.compare kf1 kf2 in
- if c <> 0 then c else
- cmp_callstacks_aux r1 r2
-
-let cmp_callstacks cs1 cs2 =
- if cs1 == cs2 then 0 else cmp_callstacks_aux (List.rev cs1) (List.rev cs2)
-
let run () =
if not (Ast.is_computed ()) then
Self.abort "nonterm requires a computed AST";
@@ -344,7 +328,7 @@ let run () =
let warned_kfs =
Stmt.Hptset.fold (fun stmt acc ->
let cs = Hashtbl.find nonterm_stacks stmt in
- let cs = List.sort cmp_callstacks cs in
+ let cs = List.sort Eva.Callstack.compare_lex cs in
warn_nonterminating_statement stmt cs;
Kernel_function.Set.add (Kernel_function.find_englobing_kf stmt) acc
) new_nonterm_stmts Kernel_function.Set.empty
diff --git a/src/plugins/users/users_register.ml b/src/plugins/users/users_register.ml
index d4ec19e6516847d2d1c3d979e46be3c5ae2bf37b..25fd111322f8f8abfc1fc2e866dc0fd388b8e707 100644
--- a/src/plugins/users/users_register.ml
+++ b/src/plugins/users/users_register.ml
@@ -49,15 +49,16 @@ let compute_users _ =
if Eva.Results.is_called kf
then
let callstacks = Eva.Results.(at_start_of kf |> callstacks) in
- let process_callstack list =
- let process_element (user, _call_site) =
+ let process_callstack callstack =
+ let users = List.tl (List.rev (Eva.Callstack.to_kf_list callstack)) in
+ let process_element user =
ignore
(Users.memo
~change:(Kernel_function.Hptset.add kf)
(fun _ -> Kernel_function.Hptset.singleton kf)
user)
in
- List.iter process_element (List.tl list)
+ List.iter process_element users
in
List.iter process_callstack callstacks
in