From 62a6836681b47d302c0ef2e8143ab3a59c7e69ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 25 Sep 2017 08:39:04 +0200
Subject: [PATCH] [Eva] prints start call finalize call
---
.../value/domains/traces/traces_domain.ml | 89 ++++++++++-----
tests/value/traces/oracle/test1.res.oracle | 89 ++++++++-------
tests/value/traces/oracle/test2.err.oracle | 0
tests/value/traces/oracle/test2.res.oracle | 108 ++++++++++++++++++
tests/value/traces/test2.i | 22 ++++
5 files changed, 236 insertions(+), 72 deletions(-)
create mode 100644 tests/value/traces/oracle/test2.err.oracle
create mode 100644 tests/value/traces/oracle/test2.res.oracle
create mode 100644 tests/value/traces/test2.i
diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml
index 5bc65500f86..b7d352f791e 100644
--- a/src/plugins/value/domains/traces/traces_domain.ml
+++ b/src/plugins/value/domains/traces/traces_domain.ml
@@ -207,10 +207,56 @@ module Traces = struct
let g = join_graph m c.graph in
{ start = c.start; current = n; graph = g}
+
+ let is_included c1 c2 =
+ (* start is the same *)
+ c1.start = c2.start &&
+ (* there are epsilons transition (Msg) between c1.current and
+ c2.current *)
+ let rec epsilon_path current stop g =
+ Node.equal current stop ||
+ begin
+ Node.compare current stop <= 0 &&
+ match Graph.find current g with
+ | exception Not_found -> false
+ | l ->
+ let exists = function
+ | Msg (n,_) -> epsilon_path n stop g
+ | _ -> false
+ in
+ List.exists exists l
+ end
+ in
+ epsilon_path c1.current c2.current c2.graph
+ &&
+ (* The graph is c1.graph is included into c2.graph *)
+ let rec decide_both k l1 l2 =
+ match l1, l2 with
+ | [], _ -> true
+ | _, [] -> false
+ | h1 :: t1, h2 :: t2 ->
+ let c = Edge.compare h1 h2 in
+ if c = 0
+ then decide_both k t1 t2
+ else if c < 0
+ then false
+ else decide_both k l1 t2
+ in
+ Graph.binary_predicate
+ Hptmap_sig.NoCache
+ Graph.UniversalPredicate
+ ~decide_fast:Graph.decide_fast_inclusion
+ ~decide_fst:(fun _ _ -> false)
+ ~decide_snd:(fun _ _ -> true)
+ ~decide_both
+ c1.graph c2.graph
+
let join c1 c2 =
match view c1, view c2 with
| `Top, _ -> c1
| _, `Top -> c2
+ | `Other c1, `Other c2 when is_included c1 c2 -> c2
+ | `Other c1, `Other c2 when is_included c2 c1 -> c1
| `Other c1, `Other c2 ->
if c1.start <> c2.start then assert false
else
@@ -235,30 +281,6 @@ module Traces = struct
{start = c1.start; current = n; graph = g}
let narrow _c1 c2 = `Value c2
-
- let is_included c1 c2 =
- c1.start = c2.start &&
- (* don't compare current we are at the same place *)
- let rec decide_both k l1 l2 =
- match l1, l2 with
- | [], _ -> true
- | _, [] -> false
- | h1 :: t1, h2 :: t2 ->
- let c = Edge.compare h1 h2 in
- if c = 0
- then decide_both k t1 t2
- else if c < 0
- then false
- else decide_both k l1 t2
- in
- Graph.binary_predicate
- Hptmap_sig.NoCache
- Graph.UniversalPredicate
- ~decide_fast:Graph.decide_fast_inclusion
- ~decide_fst:(fun _ _ -> false)
- ~decide_snd:(fun _ _ -> true)
- ~decide_both
- c1.graph c2.graph
end
let key = Structure.Key_Domain.create_key "traces domain"
@@ -299,9 +321,17 @@ module Internal = struct
let assume _stmt e pos _valuation state =
`Value(Traces.add_edge state (Assume(0,e,pos)))
- let start_call _stmt _call _valuation state = `Value state
+ let start_call _stmt call _valuation state =
+ let msg =
+ Format.asprintf "start_call: %a" (Pretty_utils.pp_list ~sep:",@ "
+ (fun fmt v -> Cil_datatype.Varinfo.pretty fmt v.Eval.formal))
+ call.Eval.arguments in
+ let state = Traces.add_edge state (Msg(0,msg)) in
+ `Value state
- let finalize_call _stmt _call ~pre:_ ~post = `Value post
+ let finalize_call _stmt call ~pre:_ ~post =
+ `Value (Traces.add_edge post (Msg(0,Format.asprintf "finalize_call: %a"
+ (Pretty_utils.pp_opt Cil_datatype.Varinfo.pretty) call.Eval.return)))
let update _valuation state = `Value state
@@ -320,9 +350,10 @@ module Internal = struct
let reuse _kf _bases ~current_input:_ ~previous_output:state = state
let empty () = Traces.empty
- let introduce_globals _vars state = state
- let initialize_variable _ _ ~initialized:_ _ state = state
- let initialize_variable_using_type _ _ state = state
+ let introduce_globals _vars state = Traces.add_edge state (Msg(0,"introduce globals"))
+ let initialize_variable lv _ ~initialized:_ _ state =
+ Traces.add_edge state (Msg(0,Format.asprintf "initialize variable: %a" Printer.pp_lval lv ))
+ let initialize_variable_using_type _ _ state = Traces.add_edge state (Msg(0,"initialize variable using type"))
(* TODO *)
let logic_assign _assign _location ~pre:_ _state = top
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index f16e857bb12..47b04471d6d 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -10,50 +10,53 @@ tests/value/traces/test1.i:14:[value] Frama_C_dump_each:
tmp ∈ {4; 5}
# Value.Traces_domain.Traces.t:
start: 0
- {[ 0 -> ([ EnterScope: tmp -> 1 ])
- 1 -> ([ Assign: tmp = 0; -> 2 ])
- 2 -> ([ Assume: c false -> 3; Assume: c true -> 4 ])
- 3 -> ([ Assign: tmp = 2; -> 7 ])
- 4 -> ([ Assign: tmp = 1; -> 6 ])
- 6 -> ([ EnterScope: i -> 11 ])
- 7 -> ([ EnterScope: i -> 9 ])
- 9 -> ([ Assign: int i = 0; -> 10 ])
- 10 -> ([ enter_loop -> 15 ])
+ {[ 0 -> ([ initialize variable using type -> 1 ])
+ 1 -> ([ EnterScope: tmp -> 2 ])
+ 2 -> ([ Assign: tmp = 0; -> 3 ])
+ 3 -> ([ Assume: c false -> 4; Assume: c true -> 5 ])
+ 4 -> ([ Assign: tmp = 2; -> 8 ])
+ 5 -> ([ Assign: tmp = 1; -> 7 ])
+ 7 -> ([ EnterScope: i -> 13 ])
+ 8 -> ([ EnterScope: i -> 10 ])
+ 10 -> ([ initialize variable: i -> 11 ])
11 -> ([ Assign: int i = 0; -> 12 ])
- 12 -> ([ enter_loop -> 14 ])
- 14 -> ([ Assume: i < 3 true -> 17 ])
- 15 -> ([ Assume: i < 3 true -> 18 ])
- 17 -> ([ Assign: tmp ++; -> 20 ])
- 18 -> ([ Assign: tmp ++; -> 19 ])
- 19 -> ([ Assign: i ++; -> 21 ])
- 20 -> ([ Assign: i ++; -> 22 ])
- 21 -> ([ incr_loop_counter -> 25 ])
- 22 -> ([ incr_loop_counter -> 24 ])
- 24 -> ([ Assume: i < 3 true -> 28 ])
- 25 -> ([ Assume: i < 3 true -> 29 ])
- 28 -> ([ Assign: tmp ++; -> 31 ])
- 29 -> ([ Assign: tmp ++; -> 30 ])
- 30 -> ([ Assign: i ++; -> 33 ])
- 31 -> ([ Assign: i ++; -> 32 ])
- 32 -> ([ incr_loop_counter -> 37 ])
- 33 -> ([ incr_loop_counter -> 36 ])
- 36 -> ([ Assume: i < 3 true -> 40 ])
- 37 -> ([ Assume: i < 3 true -> 41 ])
- 40 -> ([ Assign: tmp ++; -> 43 ])
- 41 -> ([ Assign: tmp ++; -> 42 ])
- 42 -> ([ Assign: i ++; -> 45 ])
- 43 -> ([ Assign: i ++; -> 44 ])
- 44 -> ([ incr_loop_counter -> 49 ])
- 45 -> ([ incr_loop_counter -> 48 ])
- 48 -> ([ Assume: i < 3 false -> 52 ])
- 49 -> ([ Assume: i < 3 false -> 53 ])
- 52 -> ([ leave_loop -> 55 ])
- 53 -> ([ leave_loop -> 54 ])
- 54 -> ([ LeaveScope: i -> 57 ])
- 55 -> ([ LeaveScope: i -> 56 ])
- 56 -> ([ join -> 58 ])
- 57 -> ([ join -> 58 ]) ]}
- current: 58]
+ 12 -> ([ enter_loop -> 18 ])
+ 13 -> ([ initialize variable: i -> 14 ])
+ 14 -> ([ Assign: int i = 0; -> 15 ])
+ 15 -> ([ enter_loop -> 17 ])
+ 17 -> ([ Assume: i < 3 true -> 20 ])
+ 18 -> ([ Assume: i < 3 true -> 21 ])
+ 20 -> ([ Assign: tmp ++; -> 23 ])
+ 21 -> ([ Assign: tmp ++; -> 22 ])
+ 22 -> ([ Assign: i ++; -> 24 ])
+ 23 -> ([ Assign: i ++; -> 25 ])
+ 24 -> ([ incr_loop_counter -> 28 ])
+ 25 -> ([ incr_loop_counter -> 27 ])
+ 27 -> ([ Assume: i < 3 true -> 31 ])
+ 28 -> ([ Assume: i < 3 true -> 32 ])
+ 31 -> ([ Assign: tmp ++; -> 34 ])
+ 32 -> ([ Assign: tmp ++; -> 33 ])
+ 33 -> ([ Assign: i ++; -> 36 ])
+ 34 -> ([ Assign: i ++; -> 35 ])
+ 35 -> ([ incr_loop_counter -> 40 ])
+ 36 -> ([ incr_loop_counter -> 39 ])
+ 39 -> ([ Assume: i < 3 true -> 43 ])
+ 40 -> ([ Assume: i < 3 true -> 44 ])
+ 43 -> ([ Assign: tmp ++; -> 46 ])
+ 44 -> ([ Assign: tmp ++; -> 45 ])
+ 45 -> ([ Assign: i ++; -> 48 ])
+ 46 -> ([ Assign: i ++; -> 47 ])
+ 47 -> ([ incr_loop_counter -> 52 ])
+ 48 -> ([ incr_loop_counter -> 51 ])
+ 51 -> ([ Assume: i < 3 false -> 55 ])
+ 52 -> ([ Assume: i < 3 false -> 56 ])
+ 55 -> ([ leave_loop -> 58 ])
+ 56 -> ([ leave_loop -> 57 ])
+ 57 -> ([ LeaveScope: i -> 60 ])
+ 58 -> ([ LeaveScope: i -> 59 ])
+ 59 -> ([ join -> 61 ])
+ 60 -> ([ join -> 61 ]) ]}
+ current: 61]
==END OF DUMP==
[value] Recording results for main
[value] done for function main
diff --git a/tests/value/traces/oracle/test2.err.oracle b/tests/value/traces/oracle/test2.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
new file mode 100644
index 00000000000..a0188abe8a2
--- /dev/null
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -0,0 +1,108 @@
+[kernel] Parsing tests/value/traces/test2.i (no preprocessing)
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value:initial-state] Values of globals at initialization
+
+[value] computing for function loop <- main.
+ Called from tests/value/traces/test2.i:18.
+[value] Recording results for loop
+[value] Done for function loop
+[value] computing for function loop <- main.
+ Called from tests/value/traces/test2.i:18.
+[value] Recording results for loop
+[value] Done for function loop
+tests/value/traces/test2.i:20:[value] Frama_C_dump_each:
+ # Cvalue domain:
+ c ∈ [--..--]
+ tmp ∈ {4; 5}
+ # Value.Traces_domain.Traces.t:
+ start: 0
+ {[ 0 -> ([ initialize variable using type -> 1 ])
+ 1 -> ([ EnterScope: tmp -> 2 ])
+ 2 -> ([ Assign: tmp = 0; -> 3 ])
+ 3 -> ([ Assume: c false -> 4; Assume: c true -> 5 ])
+ 4 -> ([ Assign: tmp = 2; -> 8 ])
+ 5 -> ([ Assign: tmp = 1; -> 7 ])
+ 7 -> ([ start_call: j -> 9 ])
+ 8 -> ([ start_call: j -> 53 ])
+ 9 -> ([ EnterScope: i -> 10 ])
+ 10 -> ([ initialize variable: i -> 11 ])
+ 11 -> ([ Assign: int i = 0; -> 12 ])
+ 12 -> ([ enter_loop -> 13 ])
+ 13 -> ([ Assume: i < 3 true -> 14 ])
+ 14 -> ([ Assign: j ++; -> 15 ])
+ 15 -> ([ Assign: i ++; -> 16 ])
+ 16 -> ([ incr_loop_counter -> 17 ])
+ 17 -> ([ Assume: i < 3 true -> 19 ])
+ 19 -> ([ Assign: j ++; -> 20 ])
+ 20 -> ([ Assign: i ++; -> 21 ])
+ 21 -> ([ incr_loop_counter -> 23 ])
+ 23 -> ([ Assume: i < 3 true -> 25 ])
+ 25 -> ([ Assign: j ++; -> 26 ])
+ 26 -> ([ Assign: i ++; -> 27 ])
+ 27 -> ([ incr_loop_counter -> 29 ])
+ 29 -> ([ Assume: i < 3 false -> 31 ])
+ 31 -> ([ leave_loop -> 32 ])
+ 32 -> ([ LeaveScope: i -> 33 ])
+ 33 -> ([ EnterScope: \result<loop> -> 34 ])
+ 34 -> ([ Assign: return j; -> 35 ])
+ 35 -> ([ LeaveScope: j -> 49 ])
+ 49 -> ([ finalize_call: \result<loop> -> 50 ])
+ 50 -> ([ Assign: tmp = loop(tmp); -> 51 ])
+ 51 -> ([ LeaveScope: \result<loop> -> 52 ])
+ 52 -> ([ join -> 116 ])
+ 53 -> ([ EnterScope: i -> 55 ])
+ 55 -> ([ initialize variable: i -> 56 ])
+ 56 -> ([ Assign: int i = 0; -> 57 ])
+ 57 -> ([ enter_loop -> 58 ])
+ 58 -> ([ Assume: i < 3 true -> 59 ])
+ 59 -> ([ Assign: j ++; -> 60 ])
+ 60 -> ([ Assign: i ++; -> 61 ])
+ 61 -> ([ incr_loop_counter -> 62 ])
+ 62 -> ([ Assume: i < 3 true -> 64 ])
+ 64 -> ([ Assign: j ++; -> 65 ])
+ 65 -> ([ Assign: i ++; -> 66 ])
+ 66 -> ([ incr_loop_counter -> 68 ])
+ 68 -> ([ Assume: i < 3 true -> 70 ])
+ 70 -> ([ Assign: j ++; -> 71 ])
+ 71 -> ([ Assign: i ++; -> 72 ])
+ 72 -> ([ incr_loop_counter -> 74 ])
+ 74 -> ([ Assume: i < 3 false -> 76 ])
+ 76 -> ([ leave_loop -> 77 ])
+ 77 -> ([ LeaveScope: i -> 78 ])
+ 78 -> ([ EnterScope: \result<loop> -> 79 ])
+ 79 -> ([ Assign: return j; -> 80 ])
+ 80 -> ([ LeaveScope: j -> 112 ])
+ 112 -> ([ finalize_call: \result<loop> -> 113 ])
+ 113 -> ([ Assign: tmp = loop(tmp); -> 114 ])
+ 114 -> ([ LeaveScope: \result<loop> -> 115 ])
+ 115 -> ([ join -> 116 ]) ]}
+ current: 116]
+ ==END OF DUMP==
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value:final-states] Values at end of function loop:
+ j ∈ {4; 5}
+[value:final-states] Values at end of function main:
+ tmp ∈ {4; 5}
+[from] Computing for function loop
+[from] Done for function loop
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function loop:
+ \result FROM j
+[from] Function main:
+ \result FROM c
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function loop:
+ j; i
+[inout] Inputs for function loop:
+ \nothing
+[inout] Out (internal) for function main:
+ tmp
+[inout] Inputs for function main:
+ \nothing
diff --git a/tests/value/traces/test2.i b/tests/value/traces/test2.i
new file mode 100644
index 00000000000..c04aebeee14
--- /dev/null
+++ b/tests/value/traces/test2.i
@@ -0,0 +1,22 @@
+/* run.config
+ STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10"
+*/
+
+
+int loop(int j){
+ for(int i = 0; i < 3; i++){
+ j ++;
+ }
+ return j;
+}
+
+int main(int c){
+ int tmp;
+ tmp = 0;
+ if (c) tmp = 1;
+ else tmp = 2;
+ tmp = loop(tmp);
+ //@ slevel merge;
+ Frama_C_dump_each();
+ return c;
+}
--
GitLab