[Dive] Fix callstack computation for dependencies

src/plugins/dive/Makefile.in

@@ -38,7 +38,7 @@ endif
 
 PLUGIN_DIR ?=.
 PLUGIN_NAME := Dive
-PLUGIN_CMO := callstack self node_kind imprecision_graph build main
+PLUGIN_CMO := self callstack node_kind imprecision_graph build main
 PLUGIN_CMI:= graph_types
 PLUGIN_DEPENDENCIES:= Eva Studia
 PLUGIN_HAS_MLI:= yes

src/plugins/dive/build.ml

@@ -173,18 +173,24 @@ type t = {
 
 let reference_node_locality context node_locality =
   let { loc_file ; loc_callstack } = node_locality in
-  let add_file _ =
+  let rec add_file _ =
     let node_locality = { node_locality with loc_callstack = [] } in
     Graph.create_node context.graph ~node_kind:Cluster ~node_locality
-  and add_callstack _ =
-    Graph.create_node context.graph ~node_kind:Cluster ~node_locality
+  and add_callstack = function
+    | [] -> assert false
+    | _ :: t as loc_callstack ->
+      let node_locality = { node_locality with loc_callstack } in
+      if t <> [] then
+        ignore (CallstackTable.memo context.callstack_table t add_callstack);
+      Graph.create_node context.graph ~node_kind:Cluster ~node_locality
   in
-  ignore (FileTable.memo context.file_table loc_file add_file);
   match loc_callstack with
-  | [] -> ()
+  | [] ->
+    ignore (FileTable.memo context.file_table loc_file add_file)
   | cs ->
     ignore (CallstackTable.memo context.callstack_table cs add_callstack)
 
+
 let is_folded context vi =
   not (BaseSet.mem vi context.unfolded_bases)
 
@@ -214,7 +220,7 @@ let build_node context callstack location lval  =
       | None -> location
       | Some location' -> location'
     in
-    let ref = (location', callstack) in
+    let ref = (location', node_locality.loc_callstack) in
     let node = NodeTable.memo context.node_table ref build_new_node in
     Some node
   end
@@ -251,9 +257,21 @@ let build_node_deps context node =
     let writes = Studia.Writes.compute zone
     and add_deps (stmt,effects) =
       match stmt.skind with
-      | Instr instr when effects.Studia.Writes.direct ->
-        build_instr_deps callstack stmt instr
-      | _ -> ()
+      | 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 []
+        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
     in
     let count = List.length writes in
     Self.debug ~dkey "%d found" count;

src/plugins/dive/callstack.ml

@@ -24,7 +24,8 @@ open Cil_types
 
 include Value_types.Callstack
 
-type call_site = (Cil_types.kernel_function * Cil_types.kinstr)
+type call_site = Value_types.call_site
+module Callsite = Value_types.Callsite
 
 let init kf = [(kf,Kglobal)]
 
@@ -47,4 +48,34 @@ let push (kf,stmt) cs =
   | [] -> [(kf,Kglobal)]
   | cs -> (kf,Kstmt stmt) :: cs
 
+let rec is_prefix cs1 cs2 =
+  match cs1, cs2 with
+  | [], _ -> true
+  | _, [] -> false
+  | [(kf,Kglobal)], (kf',_)::_ -> Kernel_function.equal kf kf'
+  | _, [(_,Kglobal)] -> false
+  | s1 :: t1, s2 :: t2 ->
+    if Callsite.equal s1 s2
+    then is_prefix t1 t2
+    else false
 
+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
+  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

@@ -34,3 +34,6 @@ 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 push : Cil_types.kernel_function * Cil_types.stmt -> t -> t
+val is_prefix : t -> t -> bool
+val truncate_to_sub : t -> t -> t option
+val filter_truncate : t list -> t -> t list

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

 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<w>, shape=box, ];
-  cp3 [style="invis,dotted", ];
-  cp4 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp1 [label=<w>, shape=box, ];
+  cp2 [style="invis,dotted", ];
+  cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp5 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp4 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp6 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp5 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp7 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp6 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
   
-  subgraph cluster_cs_1 { label=<main>; cp7;cp6;cp2;cp1;
-    subgraph cluster_cs_2 { label=<f>; cp5;cp4;cp3;
+  subgraph cluster_cs_1 { label=<main>; cp6;cp5;cp1;cp0;
+    subgraph cluster_cs_2 { label=<f>; cp4;cp3;cp2;
        };
      };
-  subgraph cluster_file_1 { label=<tests/dive/assigned_param.i>; cp0;
-     };
   
-  cp4 -> cp2;
-  cp5 -> cp4;
+  cp3 -> cp1;
+  cp4 -> cp3;
+  cp5 -> cp3;
   cp6 -> cp4;
-  cp7 -> cp5;
   
   }
\ No newline at end of file

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

 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<res>, shape=box, ];
-  cp3 [style="invis,dotted", ];
-  cp4 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp1 [label=<res>, shape=box, ];
+  cp2 [style="invis,dotted", ];
+  cp3 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp5 [label=<c>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp4 [label=<c>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp6 [label=<w>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp5 [label=<w>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp7 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp6 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp8 [label=<y>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp7 [label=<y>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp9 [label=<i>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp8 [label=<i>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled,dotted", ];
   
-  subgraph cluster_cs_1 { label=<main>; cp9;cp2;cp1;
-    subgraph cluster_cs_2 { label=<f>; cp8;cp7;cp6;cp5;cp4;cp3;
+  subgraph cluster_cs_1 { label=<main>; cp8;cp1;cp0;
+    subgraph cluster_cs_2 { label=<f>; cp7;cp6;cp5;cp4;cp3;cp2;
        };
      };
-  subgraph cluster_file_1 { label=<tests/dive/const.i>; cp0;
-     };
   
-  cp4 -> cp2;
-  cp5 -> cp4;
+  cp3 -> cp1;
+  cp4 -> cp3;
+  cp5 -> cp3;
   cp6 -> cp4;
   cp7 -> cp5;
   cp8 -> cp6;
-  cp9 -> cp7;
-  cp9 -> cp8;
+  cp8 -> cp7;
   
   }
\ No newline at end of file

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

 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<y>, shape=box, ];
-  cp3 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp1 [label=<y>, shape=box, ];
+  cp2 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp4 [style="invis,dotted", ];
-  cp5 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp3 [style="invis,dotted", ];
+  cp4 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp6 [style="invis,dotted", ];
-  cp7 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp5 [style="invis,dotted", ];
+  cp6 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp8 [style="invis,dotted", ];
-  cp9 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp7 [style="invis,dotted", ];
+  cp8 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp10 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
-        style="filled,dotted", ];
+  cp9 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled,dotted", ];
   
-  subgraph cluster_cs_1 { label=<main>; cp3;cp2;cp1;
-    subgraph cluster_cs_2 { label=<f>; cp10;cp5;cp4;
-      subgraph cluster_cs_3 { label=<g>; cp7;cp6;
-        subgraph cluster_cs_4 { label=<h>; cp9;cp8;
+  subgraph cluster_cs_1 { label=<main>; cp2;cp1;cp0;
+    subgraph cluster_cs_2 { label=<f>; cp9;cp4;cp3;
+      subgraph cluster_cs_3 { label=<g>; cp6;cp5;
+        subgraph cluster_cs_4 { label=<h>; cp8;cp7;
            };
          };
        };
      };
-  subgraph cluster_file_1 { label=<tests/dive/pointed_param.i>; cp0;
-     };
   
-  cp3 -> cp2;
-  cp5 -> cp3;
-  cp7 -> cp5;
-  cp9 -> cp7;
-  cp10 -> cp9;
+  cp2 -> cp1;
+  cp4 -> cp2;
+  cp6 -> cp4;
+  cp8 -> cp6;
+  cp9 -> cp8;
   
   }
\ No newline at end of file

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

+digraph G {
+  cp0 [style="invis,dotted", ];
+  cp1 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp2 [style="invis,dotted", ];
+  cp3 [style="invis,dotted", ];
+  cp4 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp5 [style="invis,dotted", ];
+  cp6 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  
+  subgraph cluster_cs_1 { label=<main>; cp1;cp0;
+    subgraph cluster_cs_2 { label=<f1>; cp2;
+      subgraph cluster_cs_3 { label=<g>; cp4;cp3;
+         };
+       };
+    subgraph cluster_cs_4 { label=<f2>; cp6;cp5;
+       };
+     };
+  
+  cp1 -> cp1;
+  cp1 -> cp4;
+  cp1 -> cp6;
+  cp4 -> cp1;
+  cp6 -> cp1;
+  
+  }
\ No newline at end of file

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

+[kernel] Parsing tests/dive/pointers_to_local.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] done for function main
+[dive] output to tests/dive/result/pointers_to_local.dot

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

 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<x>, shape=box, ];
-  cp3 [style="invis,dotted", ];
-  cp4 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp1 [label=<x>, shape=box, ];
+  cp2 [style="invis,dotted", ];
+  cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp5 [style="invis,dotted", ];
-  cp6 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp4 [style="invis,dotted", ];
+  cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp7 [style="invis,dotted", ];
-  cp8 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp6 [style="invis,dotted", ];
+  cp7 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp8 [style="invis,dotted", ];
+  cp9 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp9 [style="invis,dotted", ];
-  cp10 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
-        style="filled", ];
   
-  subgraph cluster_cs_1 { label=<g>; cp2;cp1;
-     };
-  subgraph cluster_cs_2 { label=<f3>; cp4;cp3;
+  subgraph cluster_cs_1 { label=<g>; cp1;cp0;
      };
-  subgraph cluster_cs_3 { label=<f2>; cp6;cp5;
+  subgraph cluster_cs_2 { label=<f3>; cp3;cp2;
      };
-  subgraph cluster_cs_4 { label=<f1>; cp8;cp7;
+  subgraph cluster_cs_3 { label=<f2>; cp5;cp4;
      };
-  subgraph cluster_cs_5 { label=<main>; cp10;cp9;
+  subgraph cluster_cs_4 { label=<f1>; cp7;cp6;
      };
-  subgraph cluster_file_1 { label=<tests/dive/unfocused_callers.i>; cp0;
+  subgraph cluster_cs_5 { label=<main>; cp9;cp8;
      };
   
-  cp4 -> cp2;
-  cp6 -> cp2;
-  cp8 -> cp2;
-  cp10 -> cp4;
-  cp10 -> cp6;
-  cp10 -> cp8;
+  cp3 -> cp1;
+  cp5 -> cp1;
+  cp7 -> cp1;
+  cp9 -> cp3;
+  cp9 -> cp5;
+  cp9 -> cp7;
   
   }
\ No newline at end of file

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

 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<x2>, shape=box, ];
-  cp3 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp1 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp4 [style="invis,dotted", ];
-  cp5 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp6 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp3 [style="invis,dotted", ];
+  cp4 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp7 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp5 [style="invis,dotted", ];
+  cp6 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp8 [label=<z>, shape=box, ];
-  cp9 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp7 [label=<z>, shape=box, ];
+  cp8 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp10 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
-        style="filled", ];
-  cp11 [style="invis,dotted", ];
-  cp12 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp9 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp10 [style="invis,dotted", ];
+  cp11 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp13 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp12 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp14 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp13 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp15 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp14 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
         style="filled", ];
-  cp16 [style="invis,dotted", ];
-  cp17 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp15 [style="invis,dotted", ];
+  cp16 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp18 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp17 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp19 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>,
+  cp18 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>,
         shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000",
         style="bold,filled,bold", ];
-  cp20 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>,
+  cp19 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>,
         shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000",
         style="bold,filled,bold", ];
   
-  subgraph cluster_cs_1 { label=<f>; cp19;cp6;cp3;cp2;cp1;
+  subgraph cluster_cs_1 { label=<f>; cp18;cp2;cp1;cp0;
      };
-  subgraph cluster_cs_2 { label=<main>; cp20;cp15;cp13;cp10;cp9;cp8;cp5;cp4;
-    subgraph cluster_cs_3 { label=<f>; cp14;cp12;cp11;
+  subgraph cluster_cs_2 { label=<main>; cp19;cp14;cp12;cp9;cp8;cp7;cp4;cp3;
+    subgraph cluster_cs_3 { label=<f>; cp13;cp11;cp10;
        };
-    subgraph cluster_cs_4 { label=<f>; cp18;cp17;cp16;
+    subgraph cluster_cs_4 { label=<f>; cp17;cp16;cp15;
        };
      };
-  subgraph cluster_file_1 { label=<tests/dive/various.i>; cp7;cp0;
+  subgraph cluster_file_1 { label=<tests/dive/various.i>; cp6;cp5;
      };
   
-  cp3 -> cp2;
-  cp3 -> cp6;
-  cp3 -> cp19;
-  cp5 -> cp2;
-  cp5 -> cp6;
-  cp5 -> cp12;
-  cp5 -> cp17;
-  cp6 -> cp3;
-  cp7 -> cp5;
-  cp9 -> cp8;
-  cp9 -> cp20;
-  cp10 -> cp8;
-  cp10 -> cp20;
+  cp1 -> cp2 [style="bold", ];
+  cp2 -> cp1 [style="bold", ];
+  cp2 -> cp18;
+  cp4 -> cp1;
+  cp4 -> cp4;
+  cp4 -> cp11;
+  cp4 -> cp16;
+  cp6 -> cp4;
+  cp8 -> cp7;
+  cp8 -> cp19;
+  cp9 -> cp7;
+  cp9 -> cp19;
+  cp11 -> cp8;
+  cp11 -> cp13;
   cp12 -> cp9;
-  cp12 -> cp14;
-  cp13 -> cp10;
-  cp14 -> cp12;
-  cp15 -> cp13 [color="#00FF00", ];
-  cp17 -> cp13;
-  cp17 -> cp18;
-  cp18 -> cp17;
+  cp13 -> cp11;
+  cp14 -> cp12 [color="#00FF00", ];
+  cp16 -> cp12;
+  cp16 -> cp17;
+  cp17 -> cp16;
   
   }
\ No newline at end of file

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

@@ -6,7 +6,7 @@
 [eva:alarm] tests/dive/various.i:13: Warning: 
   non-finite float value.
   assert \is_finite((float)((double)((double)y * 2.0)));
-[eva:alarm] tests/dive/various.i:26: Warning: 
+[eva:alarm] tests/dive/various.i:27: Warning: 
   non-finite float value. assert \is_finite((float)(y + w));
 [eva] done for function main
 [dive] output to tests/dive/result/various.dot

src/plugins/dive/tests/dive/pointers_to_local.i

+/* run.config
+STDOPT: +"-dive-from main::x -dive-depth-limit 5"
+*/
+
+void g(float *p) {
+  float x = *p;
+  *p = x + 1.0f;
+}
+
+void f1(float *p) {
+  g(p);
+}
+
+void f2(float *p) {
+  float x = *p;
+  *p += x + 2.0f;
+}
+
+float main()
+{
+  float x = 0.0f;
+  f1(&x);
+  f2(&x);
+  return x;
+}

src/plugins/dive/tests/dive/various.i

@@ -22,6 +22,7 @@ void main()
 
   float x = 3.0 + g;
   float y = f(x);
+  x = x + 0.5f;
   float w = (*pf)(x);
   float z = y + w + 1.0;
 }