From b856536a0f01f9837ab1c61f391fdff76294721e Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 19 Feb 2019 16:13:57 +0100
Subject: [PATCH] [Dive] Very basic testing
---
src/plugins/dive/main.ml | 11 +++--
src/plugins/dive/self.ml | 46 +++++++++++--------
src/plugins/dive/self.mli | 1 +
src/plugins/dive/tests/dive/assigned_param.i | 18 ++++++++
src/plugins/dive/tests/dive/const.i | 16 +++++++
.../dive/tests/dive/oracle/assigned_param.dot | 23 ++++++++++
.../dive/oracle/assigned_param.res.oracle | 8 ++++
src/plugins/dive/tests/dive/oracle/const.dot | 28 +++++++++++
.../dive/tests/dive/oracle/const.res.oracle | 16 +++++++
.../dive/tests/dive/oracle/various.dot | 40 ++++++++++++++++
.../dive/tests/dive/oracle/various.res.oracle | 12 +++++
src/plugins/dive/tests/dive/various.i | 28 +++++++++++
src/plugins/dive/tests/test_config | 2 +
13 files changed, 227 insertions(+), 22 deletions(-)
create mode 100644 src/plugins/dive/tests/dive/assigned_param.i
create mode 100644 src/plugins/dive/tests/dive/const.i
create mode 100644 src/plugins/dive/tests/dive/oracle/assigned_param.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
create mode 100644 src/plugins/dive/tests/dive/oracle/const.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/const.res.oracle
create mode 100644 src/plugins/dive/tests/dive/oracle/various.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/various.res.oracle
create mode 100644 src/plugins/dive/tests/dive/various.i
create mode 100644 src/plugins/dive/tests/test_config
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index e7f7f3ffa0b..51c905e88ab 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -31,9 +31,14 @@ let main () =
let depth_limit = Self.DepthLimit.get () in
Self.FromBases.iter (Build.add_var ~depth_limit context);
(* Output it *)
- let out_channel = open_out "imprecisions.dot" in
- Imprecision_graph.ouptput_to_dot out_channel (Build.get_graph context);
- close_out out_channel
+ let output_basename = Self.OutputBasename.get () in
+ if output_basename <> "" then begin
+ let filename = output_basename ^ ".dot" in
+ Self.result "output to %s" filename;
+ let out_channel = open_out filename in
+ Imprecision_graph.ouptput_to_dot out_channel (Build.get_graph context);
+ close_out out_channel
+ end;
end
let () =
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index 60d794eff33..09a9616fd6b 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -29,12 +29,19 @@ include Plugin.Register
let help = "An interactive imprecision graph generator."
end)
+module OutputBasename = Empty_string
+ (struct
+ let option_name = "-dive-output"
+ let help = "Outputs the built graph into a file with this basename."
+ let arg_name = "basename"
+ end)
+
module DepthLimit = Int
(struct
- let default = 5
let option_name = "-dive-depth-limit"
let help = "Build dependencies up to a depth of N."
let arg_name = "N"
+ let default = 3
end)
module FromAlarms = True
@@ -49,26 +56,27 @@ struct
let of_string s =
let regexp = Str.regexp "^\\([_a-zA-Z0-9]+\\)::\\([_a-zA-Z0-9]+\\)$" in
- let name, localisation, error_suffix =
- if Str.string_match regexp s 0 then
- let function_name = Str.matched_group 1 s
- and variable_name = Str.matched_group 2 s in
- try
- let kf = Globals.Functions.find_by_name function_name in
- variable_name, VLocal kf, " in function " ^ function_name
+ if Str.string_match regexp s 0 then
+ let function_name = Str.matched_group 1 s
+ and variable_name = Str.matched_group 2 s in
+ let kf = try Globals.Functions.find_by_name function_name
with Not_found ->
raise (Cannot_build ("no function '" ^ function_name ^ "'"))
- else
- let regexp = Str.regexp "^[_a-zA-Z0-9]+$" in
- if Str.string_match regexp s 0 then
- s, VGlobal, ""
- else
- raise (Cannot_build ("wrong syntax: '" ^ s ^ "'"))
- in
- try
- Globals.Vars.find_from_astinfo name localisation
- with Not_found ->
- raise (Cannot_build ("no variable '" ^ name ^ "'" ^ error_suffix))
+ in
+ try Globals.Vars.find_from_astinfo variable_name (VLocal kf)
+ with Not_found ->
+ try Globals.Vars.find_from_astinfo variable_name (VFormal kf)
+ with Not_found ->
+ raise (Cannot_build ("no variable '" ^ name ^ "' in function"
+ ^ function_name))
+ else
+ let regexp = Str.regexp "^[_a-zA-Z0-9]+$" in
+ if not (Str.string_match regexp s 0) then
+ raise (Cannot_build ("wrong syntax: '" ^ s ^ "'"));
+ try
+ Globals.Vars.find_from_astinfo name VGlobal
+ with Not_found ->
+ raise (Cannot_build ("no global variable '" ^ name ^ "'"))
let to_string vi =
match Kernel_function.find_defining_kf vi with
diff --git a/src/plugins/dive/self.mli b/src/plugins/dive/self.mli
index f56de61ab58..8d9f9f8b0ec 100644
--- a/src/plugins/dive/self.mli
+++ b/src/plugins/dive/self.mli
@@ -26,6 +26,7 @@ module type Varinfo_set = Parameter_sig.Set
with type elt = Cil_types.varinfo
and type t = Cil_datatype.Varinfo.Set.t
+module OutputBasename : Parameter_sig.String
module DepthLimit : Parameter_sig.Int
module FromAlarms : Parameter_sig.Bool
module FromBases : Varinfo_set
diff --git a/src/plugins/dive/tests/dive/assigned_param.i b/src/plugins/dive/tests/dive/assigned_param.i
new file mode 100644
index 00000000000..322aa200478
--- /dev/null
+++ b/src/plugins/dive/tests/dive/assigned_param.i
@@ -0,0 +1,18 @@
+/* run.config
+STDOPT: +"-dive-from main::w"
+*/
+
+volatile int nondet;
+
+int f(int x, int z)
+{
+ if (nondet)
+ x = z;
+ return x;
+}
+
+int main(int x, int z)
+{
+ int w = f(x,z);
+ return w + 1;
+}
diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i
new file mode 100644
index 00000000000..adc5365c8c6
--- /dev/null
+++ b/src/plugins/dive/tests/dive/const.i
@@ -0,0 +1,16 @@
+/* run.config
+STDOPT: +"-dive-from main::res"
+*/
+
+int f(int x, int y)
+{
+ const c = x + 1;
+ int w = y + 1;
+ return c + w;
+}
+
+int main(int i)
+{
+ int res = f(i, 2*i);
+ return res;
+}
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.dot b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
new file mode 100644
index 00000000000..460be6d9d72
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
@@ -0,0 +1,23 @@
+digraph G {
+ cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ];
+ cp1 [label=<w>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ 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", ];
+
+ subgraph cluster_file_1 { label=<tests/dive/assigned_param.i>; cp0;
+ subgraph cluster_function_19 { label=<f>; cp3;cp2;
+ };
+ subgraph cluster_function_24 { label=<main>; cp5;cp4;cp1;
+ };
+ };
+
+ cp2 -> cp1;
+ cp3 -> cp2;
+ cp4 -> cp2;
+ cp5 -> cp3;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle b/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
new file mode 100644
index 00000000000..01978d95470
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing tests/dive/assigned_param.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/assigned_param.i:18: Warning:
+ signed overflow. assert w + 1 ≤ 2147483647;
+[eva] done for function main
+[dive] output to tests/dive/result/assigned_param.dot
diff --git a/src/plugins/dive/tests/dive/oracle/const.dot b/src/plugins/dive/tests/dive/oracle/const.dot
new file mode 100644
index 00000000000..cce0e10e5aa
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/const.dot
@@ -0,0 +1,28 @@
+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", ];
+ 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", ];
+
+ subgraph cluster_file_1 { label=<tests/dive/const.i>; cp0;
+ subgraph cluster_function_25 { label=<main>; cp1;
+ };
+ };
+ subgraph cluster_file_2 { label=<>; cp2;
+ subgraph cluster_function_18 { label=<f>; cp7;cp6;cp5;cp4;cp3;
+ };
+ };
+
+ cp3 -> cp1;
+ cp4 -> cp3;
+ cp5 -> cp3;
+ cp6 -> cp4;
+ cp7 -> cp5;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/const.res.oracle b/src/plugins/dive/tests/dive/oracle/const.res.oracle
new file mode 100644
index 00000000000..7b0b9060658
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/const.res.oracle
@@ -0,0 +1,16 @@
+[kernel] Parsing tests/dive/const.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/const.i:14: Warning:
+ signed overflow. assert -2147483648 ≤ 2 * i;
+[eva:alarm] tests/dive/const.i:14: Warning:
+ signed overflow. assert 2 * i ≤ 2147483647;
+[eva:alarm] tests/dive/const.i:7: Warning:
+ signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] tests/dive/const.i:9: Warning:
+ signed overflow. assert -2147483648 ≤ c + w;
+[eva:alarm] tests/dive/const.i:9: Warning:
+ signed overflow. assert c + w ≤ 2147483647;
+[eva] done for function main
+[dive] output to tests/dive/result/const.dot
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
new file mode 100644
index 00000000000..e9d2bb149ea
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -0,0 +1,40 @@
+digraph G {
+ cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ];
+ cp1 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp4 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp5 [label=<z>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp6 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp8 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp9 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled,dotted", ];
+
+ subgraph cluster_file_1 { label=<tests/dive/various.i>; cp4;cp0;
+ subgraph cluster_function_19 { label=<f>; cp2;cp1;
+ };
+ subgraph cluster_function_24 { label=<main>; cp9;cp8;cp7;cp6;cp5;cp3;
+ };
+ };
+
+ cp1 -> cp2;
+ cp1 -> cp6;
+ cp1 -> cp8;
+ cp2 -> cp1;
+ cp3 -> cp1;
+ cp4 -> cp3;
+ cp6 -> cp5;
+ cp7 -> cp5;
+ cp8 -> cp7;
+ cp9 -> cp8 [color="#00FF00", ];
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/various.res.oracle b/src/plugins/dive/tests/dive/oracle/various.res.oracle
new file mode 100644
index 00000000000..fc941299b06
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/various.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/dive/various.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] tests/dive/various.i:10: starting to merge loop iterations
+[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:
+ non-finite float value. assert \is_finite((float)(y + w));
+[eva] done for function main
+[dive] output to tests/dive/result/various.dot
diff --git a/src/plugins/dive/tests/dive/various.i b/src/plugins/dive/tests/dive/various.i
new file mode 100644
index 00000000000..84c0f7788f7
--- /dev/null
+++ b/src/plugins/dive/tests/dive/various.i
@@ -0,0 +1,28 @@
+/* run.config
+STDOPT: +"-dive-from main::z,f::x2"
+*/
+
+float g;
+
+float f(float x2)
+{
+ float y;
+ for (int i = 0 ; i < 10 ; i++)
+ {
+ y = x2 + 1.0;
+ x2 = y * 2.0;
+ }
+
+ return x2;
+}
+
+void main()
+{
+ float (*pf)(float) = &f;
+
+ float x = 3.0 + g;
+ float y = f(x);
+ float w = (*pf)(x);
+ float z = y + w + 1.0;
+}
+
diff --git a/src/plugins/dive/tests/test_config b/src/plugins/dive/tests/test_config
new file mode 100644
index 00000000000..2baab62a7d7
--- /dev/null
+++ b/src/plugins/dive/tests/test_config
@@ -0,0 +1,2 @@
+LOG: @PTEST_NAME@.dot
+OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope,dive -check -eva-msg-key=-initial-state -eva-no-show-progress -dive-output @PTEST_RESULT@/@PTEST_NAME@
--
GitLab