[Dive] Add an unevaluated precision type

src/plugins/dive/graph_types.mli

@@ -32,7 +32,7 @@ type node_locality = {
   loc_function : Cil_types.kernel_function option;
 }
 
-type node_precision = Singleton | Normal | Wide | Critical
+type node_precision = Unevaluated | Singleton | Normal | Wide | Critical
 
 type node = {
   node_key : int;

src/plugins/dive/imprecision_graph.ml

@@ -49,7 +49,7 @@ include G
 let next_node_key = ref 0
 let next_dependency_key = ref 0
 
-let create_node ?(node_precision=Singleton) ~node_kind ~node_locality g =
+let create_node ?(node_precision=Unevaluated) ~node_kind ~node_locality g =
   let node = {
     node_key = !next_node_key;
     node_kind;
@@ -68,7 +68,8 @@ let update_node_precision node new_precision =
     | Critical, _ | _, Critical -> Critical
     | Wide, _ | _, Wide -> Wide
     | Normal, _ | _, Normal -> Normal
-    | Singleton, Singleton -> Singleton
+    | Singleton, _ | _, Singleton -> Singleton
+    | Unevaluated, Unevaluated -> Unevaluated
 
 let create_dependency ~allow_folding g v1 dependency_kind v2 =
   let same_kind (_,e,_) =
@@ -143,13 +144,15 @@ let ouptput_to_dot out_channel g =
           | Alarm _ ->  [ `Shape `Doubleoctagon ; `Style `Bold ]
           | File -> [ `Style `Invis ]
         and precision = match v.node_precision with
+          | Unevaluated -> []
           | Singleton -> [`Color 0x88aaff ;
                           `Style `Filled ; `Fillcolor 0xaaccff]
-          | Normal -> []
+          | Normal -> [ `Color 0x004400 ;
+                        `Style `Filled ; `Fillcolor 0xeeffee ]
           | Wide -> [ `Color 0xff0000 ;
                       `Style `Filled ; `Fillcolor 0xffbbbb ]
           | Critical -> [ `Color 0xff0000 ; `Style `Bold ;
-                          `Style `Filled ; `Fillcolor 0xffbbbb ]
+                          `Style `Filled ; `Fillcolor 0xff0000 ]
         in
         l := precision @ kind @ !l;
         if not v.node_deps_computed then

src/plugins/dive/tests/dive/assigned_param.i

 /* run.config
-STDOPT: +"-dive-from main::w"
+STDOPT: +"-dive-from main::w -dive-depth-limit 5"
 */
 
 volatile int nondet;

src/plugins/dive/tests/dive/const.i

 /* run.config
-STDOPT: +"-dive-from main::res"
+STDOPT: +"-dive-from main::res -dive-depth-limit 5"
 */
 
 int f(int x, int y)

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

 digraph G {
-  cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ];
-  cp1 [label=<w>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-       style="filled", ];
+  cp0 [style="invis,dotted", ];
+  cp1 [label=<w>, shape=box, ];
   cp2 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp3 [label=<z>, shape=box, ];
-  cp4 [label=<x>, shape=box, ];
-  cp5 [label=<z>, shape=box, style="dotted", ];
+  cp3 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
+       style="filled", ];
+  cp4 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
+       style="filled", ];
+  cp5 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
+       style="filled", ];
   
   subgraph cluster_file_1 { label=<tests/dive/assigned_param.i>; cp0;
     subgraph cluster_function_19 { label=<f>; cp3;cp2;

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

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

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

 digraph G {
-  cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ];
+  cp0 [style="invis,dotted", ];
   cp1 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
   cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
@@ -8,8 +8,7 @@ digraph G {
        style="filled", ];
   cp4 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp5 [label=<z>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-       style="filled", ];
+  cp5 [label=<z>, shape=box, ];
   cp6 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
   cp7 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
@@ -17,12 +16,12 @@ digraph G {
   cp8 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
   cp9 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-       style="filled,dotted", ];
+       style="filled", ];
   cp10 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>,
-        shape=doubleoctagon, fillcolor="#FFBBBB", color="#FF0000",
+        shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000",
         style="bold,filled,bold", ];
   cp11 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>,
-        shape=doubleoctagon, fillcolor="#FFBBBB", color="#FF0000",
+        shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000",
         style="bold,filled,bold", ];
   
   subgraph cluster_file_1 { label=<tests/dive/various.i>; cp4;cp0;

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

 /* run.config
-STDOPT: +"-dive-from main::z,f::x2 -dive-from-function-alarms f,main"
+STDOPT: +"-dive-from main::z,f::x2 -dive-from-function-alarms f,main -dive-depth-limit 5"
 */
 
 float g;