From 4456b1ab7656117ea5f2ec9b7896d5f59256e29a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Jul 2023 10:22:42 +0200
Subject: [PATCH] [Eva] Callstack: adds stable hash and pretty-printing
functions.
---
.../abstract_interp/eva_types.ml | 51 +++++++++++++++++++
.../abstract_interp/eva_types.mli | 2 +
src/plugins/eva/Eva.mli | 7 +++
src/plugins/eva/types/callstack.mli | 7 +++
4 files changed, 67 insertions(+)
diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index 6d07a666499..d7638929c79 100644
--- a/src/kernel_services/abstract_interp/eva_types.ml
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -20,6 +20,10 @@
(* *)
(**************************************************************************)
+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 *)
@@ -136,4 +140,51 @@ struct
(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 =
+ 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
index 57944aea8df..08b9105f7bb 100644
--- a/src/kernel_services/abstract_interp/eva_types.mli
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -37,6 +37,8 @@ sig
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
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 7cf6b0097b1..dd1fc5ab89c 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -139,6 +139,13 @@ module Callstack: sig
with type t = callstack
and module Hashtbl = Eva_types.Callstack.Hashtbl
+ (** Print a call stack without displaying call sites. *)
+ val pretty_short : 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
+
(** [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. *)
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 6460b8d5bc2..cb693ca3c45 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -44,6 +44,13 @@ include Datatype.S_with_collections
with type t = callstack
and module Hashtbl = Eva_types.Callstack.Hashtbl
+(** Print a call stack without displaying call sites. *)
+val pretty_short : 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
+
(** [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. *)
--
GitLab