From b4edc111c577efe7f48819971d55224d3c536ab2 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 21 Feb 2019 17:47:18 +0100
Subject: [PATCH] [Dive] Add an unevaluated precision type
---
src/plugins/dive/graph_types.mli | 2 +-
src/plugins/dive/imprecision_graph.ml | 11 +++++---
src/plugins/dive/tests/dive/assigned_param.i | 2 +-
src/plugins/dive/tests/dive/const.i | 2 +-
.../dive/tests/dive/oracle/assigned_param.dot | 14 ++++++-----
src/plugins/dive/tests/dive/oracle/const.dot | 25 ++++++++++++-------
.../dive/tests/dive/oracle/various.dot | 11 ++++----
src/plugins/dive/tests/dive/various.i | 2 +-
8 files changed, 40 insertions(+), 29 deletions(-)
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index 59fd3707a55..cea36be39f2 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/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;
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index 9c4aab6de23..3f0979ffefd 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/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
diff --git a/src/plugins/dive/tests/dive/assigned_param.i b/src/plugins/dive/tests/dive/assigned_param.i
index 322aa200478..a5d5fd969b4 100644
--- a/src/plugins/dive/tests/dive/assigned_param.i
+++ b/src/plugins/dive/tests/dive/assigned_param.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-dive-from main::w"
+STDOPT: +"-dive-from main::w -dive-depth-limit 5"
*/
volatile int nondet;
diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i
index adc5365c8c6..3534fa8e703 100644
--- a/src/plugins/dive/tests/dive/const.i
+++ b/src/plugins/dive/tests/dive/const.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-dive-from main::res"
+STDOPT: +"-dive-from main::res -dive-depth-limit 5"
*/
int f(int x, int y)
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.dot b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
index 460be6d9d72..e988a3cdc4a 100644
--- a/src/plugins/dive/tests/dive/oracle/assigned_param.dot
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
@@ -1,12 +1,14 @@
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;
diff --git a/src/plugins/dive/tests/dive/oracle/const.dot b/src/plugins/dive/tests/dive/oracle/const.dot
index cce0e10e5aa..ddf007a23e7 100644
--- a/src/plugins/dive/tests/dive/oracle/const.dot
+++ b/src/plugins/dive/tests/dive/oracle/const.dot
@@ -1,17 +1,22 @@
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
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index acc4db37e9f..d8595e7b16c 100644
--- a/src/plugins/dive/tests/dive/oracle/various.dot
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -1,5 +1,5 @@
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;
diff --git a/src/plugins/dive/tests/dive/various.i b/src/plugins/dive/tests/dive/various.i
index c8766e6a7ad..f89d87ed5c8 100644
--- a/src/plugins/dive/tests/dive/various.i
+++ b/src/plugins/dive/tests/dive/various.i
@@ -1,5 +1,5 @@
/* 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;
--
GitLab