From 5b7da9d77e10ce050cd5081678f07a6a91f5a672 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Jul 2023 15:00:37 +0200
Subject: [PATCH] [Eva] Removes Value_types.Callstack.
---
.../abstract_interp/eva_types.ml | 2 -
.../abstract_interp/eva_types.mli | 1 -
.../abstract_interp/value_types.ml | 89 -------------------
.../abstract_interp/value_types.mli | 35 --------
src/plugins/eva/Eva.mli | 3 -
src/plugins/eva/types/callstack.mli | 3 -
6 files changed, 133 deletions(-)
diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index d7638929c79..b04b176cbff 100644
--- a/src/kernel_services/abstract_interp/eva_types.ml
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -139,8 +139,6 @@ struct
in
(cs.entry_point, Cil_types.Kglobal) :: l
- let to_legacy cs = List.rev (to_call_list cs)
-
(* Stable hash and pretty-printing *)
let stmt_hash s =
diff --git a/src/kernel_services/abstract_interp/eva_types.mli b/src/kernel_services/abstract_interp/eva_types.mli
index 08b9105f7bb..5dadaf28974 100644
--- a/src/kernel_services/abstract_interp/eva_types.mli
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -53,7 +53,6 @@ sig
val top_call : t -> Cil_types.kernel_function * Cil_types.kinstr
val last_caller : t -> Cil_types.kernel_function option
- val to_legacy : t -> Value_types.callstack
val to_kf_list : t -> Cil_types.kernel_function list
val to_stmt_list : t -> Cil_types.stmt list
val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
diff --git a/src/kernel_services/abstract_interp/value_types.ml b/src/kernel_services/abstract_interp/value_types.ml
index de2fbcb8ba0..d7d070d20e3 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 f4920979902..811e97b24fd 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/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index defe1cf1ad8..b1cda1de9bd 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -170,9 +170,6 @@ module Callstack: sig
(** {2 Conversion} *)
- (** This function is likely to be removed in future versions*)
- val to_legacy : t -> Value_types.callstack
-
(** 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
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 4587358500b..c3ede6737cf 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -75,9 +75,6 @@ val last_caller : t -> Cil_types.kernel_function option
(** {2 Conversion} *)
-(** This function is likely to be removed in future versions*)
-val to_legacy : t -> Value_types.callstack
-
(** 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
--
GitLab