From 85f6ba2f05a8d6902cf06af06c9bd15a30c378ff Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 7 Jun 2019 17:51:44 +0200
Subject: [PATCH] [Dive] Hack to reduce the impact of loosing memexeced
dependencies
---
src/plugins/dive/build.ml | 31 +++++++++++++------
src/plugins/dive/callstack.ml | 13 +++++---
src/plugins/dive/callstack.mli | 3 +-
src/plugins/dive/tests/dive/global.i | 14 +++++++++
src/plugins/dive/tests/dive/oracle/global.dot | 22 +++++++++++++
.../dive/tests/dive/oracle/global.res.oracle | 8 +++++
.../dive/tests/dive/oracle/various.dot | 4 +--
7 files changed, 79 insertions(+), 16 deletions(-)
create mode 100644 src/plugins/dive/tests/dive/global.i
create mode 100644 src/plugins/dive/tests/dive/oracle/global.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/global.res.oracle
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 337a2c6cfdd..56c8a9ff5e1 100644
--- a/src/plugins/dive/build.ml
+++ b/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
diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml
index f9d5ae7157a..490fe5dc5c6 100644
--- a/src/plugins/dive/callstack.ml
+++ b/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
diff --git a/src/plugins/dive/callstack.mli b/src/plugins/dive/callstack.mli
index 7d3dce8a4b2..c31f1ef3d08 100644
--- a/src/plugins/dive/callstack.mli
+++ b/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
diff --git a/src/plugins/dive/tests/dive/global.i b/src/plugins/dive/tests/dive/global.i
new file mode 100644
index 00000000000..d475e3862e4
--- /dev/null
+++ b/src/plugins/dive/tests/dive/global.i
@@ -0,0 +1,14 @@
+/* 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;
+}
+
diff --git a/src/plugins/dive/tests/dive/oracle/global.dot b/src/plugins/dive/tests/dive/oracle/global.dot
new file mode 100644
index 00000000000..e5d9191e202
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/global.dot
@@ -0,0 +1,22 @@
+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
diff --git a/src/plugins/dive/tests/dive/oracle/global.res.oracle b/src/plugins/dive/tests/dive/oracle/global.res.oracle
new file mode 100644
index 00000000000..18bb2bf74bd
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/global.res.oracle
@@ -0,0 +1,8 @@
+[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
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index 500799fd2fa..4ce0ff968e2 100644
--- a/src/plugins/dive/tests/dive/oracle/various.dot
+++ b/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;
--
GitLab