[Dive] Hack to reduce the impact of loosing memexeced dependencies

src/plugins/dive/build.ml

@@ -259,16 +259,29 @@ let build_node_deps context node =
       match stmt.skind with
       | Instr _ when not effects.Studia.Writes.direct -> ()
       | Instr instr ->
-        (* Keep only callstacks which are a compatible with the current one *)
-        let states = Db.Value.get_stmt_state_callstack ~after:false stmt in
-        let callstacks = match states with
-          | None -> assert false
-          | Some table ->
-            let module Table = Value_types.Callstack.Hashtbl in
-            Table.fold (fun cs _ acc -> cs :: acc) table []
+        let callstacks =
+          if callstack <> [] &&
+             Kernel_function.(equal
+                                (find_englobing_kf stmt)
+                                (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
+               all callstacks due to memexec -> in this particular case
+               we are sure not to miss the only admissible callstack *)
+            [callstack]
+          else
+            (* Keep only callstacks which are a compatible with the current one *)
+            let states = Db.Value.get_stmt_state_callstack ~after:false stmt in
+            let callstacks = match states with
+              | None -> assert false
+              | Some table ->
+                let module Table = Value_types.Callstack.Hashtbl in
+                Table.fold (fun cs _ acc -> cs :: acc) table []
+            in
+            (* TODO: missing callstacks filtered by memexec *)
+            Callstack.filter_truncate callstacks callstack
         in
-        (* TODO: missing callstacks filtered by memexec *)
-        let callstacks = Callstack.filter_truncate callstacks callstack in
         (* Create a dependency for each of them *)
         List.iter (fun cs -> build_instr_deps cs stmt instr) callstacks
       | _ -> assert false

src/plugins/dive/callstack.ml

@@ -35,6 +35,11 @@ let pop cs =
   | [(_,Kglobal)] -> None
   | (kf,Kstmt stmt) :: t -> Some (kf,stmt,t)
 
+let top_kf cs =
+  match cs with
+  | [] | (_,Kglobal) :: _ :: _ | [(_,Kstmt _)] -> assert false (* Invariant *)
+  | (kf,_) :: _ -> kf
+
 let rec pop_downto top_kf = function
   | [] -> failwith "the callstack doesn't contain this function"
   | ((kf,_kinstr) :: tail) as cs ->
@@ -62,10 +67,10 @@ let rec is_prefix cs1 cs2 =
 let truncate_to_sub full_cs sub_cs =
   let rec aux acc = function
     | [] -> None
-  | (s :: t) as cs ->
-    if is_prefix sub_cs cs
-    then Some (List.rev acc @ sub_cs)
-    else aux (s :: acc) t
+    | (s :: t) as cs ->
+      if is_prefix sub_cs cs
+      then Some (List.rev acc @ sub_cs)
+      else aux (s :: acc) t
   in
   aux [] full_cs
 

src/plugins/dive/callstack.mli

@@ -27,12 +27,13 @@ include Datatype.S_with_collections with type t := t
 
 (* The callstacks manipulated here have the following invariant:
    - the callstack is never an empty list
-   - the last item of the list has alwas a Kglobal
+   - the last item of the list has always a Kglobal
    - all elements of the list except the last have a Kstmt *)
 
 val init : Cil_types.kernel_function -> t
 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
 val is_prefix : t -> t -> bool
 val truncate_to_sub : t -> t -> t option

src/plugins/dive/tests/dive/global.i

+/* run.config
+STDOPT: +"-dive-from main::z"
+*/
+
+float g;
+
+float main(float x)
+{
+  float y = x + 1;
+  g = y;
+  float z = g + x;
+  return z;
+}
+

src/plugins/dive/tests/dive/oracle/global.dot

+digraph G {
+  cp0 [style="invis,dotted", ];
+  cp1 [label=<z>, shape=box, ];
+  cp2 [style="invis,dotted", ];
+  cp3 [label=<g>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp4 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp5 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  
+  subgraph cluster_cs_1 { label=<main>; cp5;cp4;cp1;cp0;
+     };
+  subgraph cluster_file_1 { label=<tests/dive/global.i>; cp3;cp2;
+     };
+  
+  cp3 -> cp1;
+  cp4 -> cp1;
+  cp4 -> cp5;
+  cp5 -> cp3;
+  
+  }
\ No newline at end of file

src/plugins/dive/tests/dive/oracle/global.res.oracle

+[kernel] Parsing tests/dive/global.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/global.i:11: Warning: 
+  non-finite float value. assert \is_finite((float)(g + x));
+[eva] done for function main
+[dive] output to tests/dive/result/global.dot

src/plugins/dive/tests/dive/oracle/various.dot

@@ -47,8 +47,8 @@ digraph G {
   subgraph cluster_file_1 { label=<tests/dive/various.i>; cp6;cp5;
      };
   
-  cp1 -> cp2 [style="bold", ];
-  cp2 -> cp1 [style="bold", ];
+  cp1 -> cp2;
+  cp2 -> cp1;
   cp2 -> cp18;
   cp4 -> cp1;
   cp4 -> cp4;