From 5b4e1b3c5fe7e8a2d799a8b2f32da21a81f1bb14 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sat, 8 Oct 2022 15:06:49 +0200
Subject: [PATCH] [Dive] Rework callstack abstraction
---
src/plugins/dive/build.ml | 11 +++++++++--
src/plugins/dive/callstack.ml | 13 +------------
src/plugins/dive/callstack.mli | 9 ++++++++-
3 files changed, 18 insertions(+), 15 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 9952c76cf11..2e86d33bb6c 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -231,7 +231,9 @@ let build_node_locality callstack node_kind =
let find_compatible_callstacks stmt callstack =
let kf = Kernel_function.find_englobing_kf stmt in
- if callstack <> [] && Kernel_function.equal kf (Callstack.top_kf callstack)
+ if callstack = [] (* Globals variables *)
+ then [Callstack.init kf] (* Default *)
+ else if Kernel_function.equal kf (Callstack.top_kf callstack)
then
(* slight improvement which only work when there is no recursion
and which is only usefull because you currently can't have
@@ -242,7 +244,12 @@ let find_compatible_callstacks stmt callstack =
(* Keep only callstacks which are a compatible with the current one *)
let callstacks = Eval.to_callstacks stmt in
(* TODO: missing callstacks filtered by memexec *)
- Callstack.filter_truncate callstacks callstack
+ let make_compatible cs =
+ Callstack.truncate_to_sub cs callstack |>
+ Option.value ~default:(Callstack.init kf)
+ in
+ let result = List.map make_compatible callstacks in
+ List.sort_uniq Callstack.compare result (* Remove duplicates *)
(* --- Graph building --- *)
diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml
index 3c5f769d4ce..91959b12feb 100644
--- a/src/plugins/dive/callstack.ml
+++ b/src/plugins/dive/callstack.ml
@@ -69,18 +69,7 @@ let truncate_to_sub full_cs sub_cs =
| [] -> None
| (s :: t) as cs ->
if is_prefix sub_cs cs
- then Some (List.rev acc @ sub_cs)
+ then Some (List.rev_append acc sub_cs)
else aux (s :: acc) t
in
aux [] full_cs
-
-let list_filter_map f l =
- let aux acc x =
- match f x with
- | None -> acc
- | Some y -> y :: acc
- in
- List.rev (List.fold_left aux [] l)
-
-let filter_truncate l sub_cs =
- list_filter_map (fun cs -> truncate_to_sub cs sub_cs) l
diff --git a/src/plugins/dive/callstack.mli b/src/plugins/dive/callstack.mli
index 68e2ded40c5..f179281b11f 100644
--- a/src/plugins/dive/callstack.mli
+++ b/src/plugins/dive/callstack.mli
@@ -35,6 +35,13 @@ val pop : t -> (Cil_types.kernel_function * Cil_types.stmt * t) option
val pop_downto : Cil_types.kernel_function -> t -> t
val top_kf : t -> Cil_types.kernel_function
val push : Cil_types.kernel_function * Cil_types.stmt -> t -> t
+
+(* Dive use partial callstack where the first call in the callstack are
+ abstracted away. Thus, Dive callstack are prefixes of complete callstacks. *)
+
+(* [is_prefix sub full] returns true whenever [sub] is a prefix of [full] *)
val is_prefix : t -> t -> bool
+
+(* [truncate_to_sub full sub] removes [full] tail until [sub] becomes a suffix.
+ Returns None if [sub] is not included in [full] *)
val truncate_to_sub : t -> t -> t option
-val filter_truncate : t list -> t -> t list
--
GitLab