[Dive] Rework callstack abstraction

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 --- *)

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

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