From 00d652d1145f727493338642eb963a177e334af5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 27 Sep 2017 01:08:16 +0200
Subject: [PATCH] [Eva] fix logic assigns
- TODO mark not defined functions particularly
---
.../value/domains/traces/traces_domain.ml | 57 +++++---
tests/value/traces/oracle/test1.res.oracle | 136 +++++++++++-------
tests/value/traces/oracle/test2.res.oracle | 4 +-
tests/value/traces/test1.i | 5 +-
4 files changed, 124 insertions(+), 78 deletions(-)
diff --git a/src/plugins/value/domains/traces/traces_domain.ml b/src/plugins/value/domains/traces/traces_domain.ml
index 334f722ea51..9a00862d791 100644
--- a/src/plugins/value/domains/traces/traces_domain.ml
+++ b/src/plugins/value/domains/traces/traces_domain.ml
@@ -135,6 +135,10 @@ type t = { start : int; current : int; graph : Graph.t}
(* Lattice structure for the abstract state above *)
module Traces = struct
+ (** impossible for normal values start must be bigger than current *)
+ let empty = { start = 0; current = 0; graph = Graph.empty }
+ let top = { start = 0; current = -1; graph = Graph.empty }
+
(* Frama-C "datatype" for type [inout] *)
include Datatype.Make_with_collections(struct
include Datatype.Serializable_undefined
@@ -161,7 +165,9 @@ module Traces = struct
let equal = Datatype.from_compare
let pretty fmt m =
- Format.fprintf fmt "@[<hv>@[start: %i@]@ %a@ @[current: %i]" m.start Graph.pretty m.graph m.current
+ if m == top then Format.fprintf fmt "TOP"
+ else
+ Format.fprintf fmt "@[<hv>@[start: %i@]@ %a@ @[current: %i]" m.start Graph.pretty m.graph m.current
let hash m =
Hashtbl.seeded_hash m.start (Hashtbl.seeded_hash m.current (Graph.hash m.graph))
@@ -170,10 +176,6 @@ module Traces = struct
end)
- (** impossible for normal values start must be bigger than current *)
- let empty = { start = 0; current = 0; graph = Graph.empty }
- let top = { start = 0; current = -1; graph = Graph.empty }
-
let view m =
if m == top then `Top
else
@@ -202,18 +204,20 @@ module Traces = struct
~decide:merge_edge g1 g2
let add_edge c edge =
- let n = Edge.Counter.next () in
- let e = match edge with
- | Assign (_,loc,typ,exp) -> Assign(n,loc,typ,exp)
- | Assume (_,a,b) -> Assume(n,a,b)
- | EnterScope (_,vs) -> EnterScope(n,vs)
- | LeaveScope (_,vs) -> LeaveScope(n,vs)
- | Msg (_,s) -> Msg(n,s)
- | Top -> Top
- in
- let m = Graph.singleton c.current [e] in
- let g = join_graph m c.graph in
- { start = c.start; current = n; graph = g}
+ if c == top then c
+ else
+ let n = Edge.Counter.next () in
+ let e = match edge with
+ | Assign (_,loc,typ,exp) -> Assign(n,loc,typ,exp)
+ | Assume (_,a,b) -> Assume(n,a,b)
+ | EnterScope (_,vs) -> EnterScope(n,vs)
+ | LeaveScope (_,vs) -> LeaveScope(n,vs)
+ | Msg (_,s) -> Msg(n,s)
+ | Top -> Top
+ in
+ let m = Graph.singleton c.current [e] in
+ let g = join_graph m c.graph in
+ { start = c.start; current = n; graph = g}
let is_included c1 c2 =
@@ -330,7 +334,8 @@ module Internal = struct
`Value(Traces.add_edge state (Assume(0,e,pos)))
let start_call _stmt call _valuation state =
- let msg = Format.asprintf "start_call: %s" (Kernel_function.get_name call.Eval.kf) in
+ let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
+ (Kernel_function.is_definition call.Eval.kf) in
let state = Traces.add_edge state (Msg(0,msg)) in
let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in
let state = Traces.add_edge state (EnterScope(0,formals)) in
@@ -369,11 +374,21 @@ module Internal = struct
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"))
+ let initialize_variable_using_type init_kind varinfo state =
+ let msg = Format.asprintf "initialize@ variable@ using@ type@ %a@ %a"
+ (fun fmt init_kind ->
+ match init_kind with
+ | Abstract_domain.Main_Formal -> Format.pp_print_string fmt "Main_Formal"
+ | Abstract_domain.Library_Global -> Format.pp_print_string fmt "Library_Global"
+ | Abstract_domain.Spec_Return kf -> Format.fprintf fmt "Spec_Return(%s)" (Kernel_function.get_name kf))
+ init_kind
+ Cil_datatype.Varinfo.pretty varinfo
+ in
+ Traces.add_edge state (Msg(0,msg))
(* TODO *)
- let logic_assign _assign _location ~pre:_ _state = top
+ let logic_assign _assign _location ~pre:_ state =
+ Traces.add_edge state (Msg(0,"logic assign"))
(* Logic *)
let evaluate_predicate _ _ _ = Alarmset.Unknown
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index ab55a710790..48b3a822116 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -1,76 +1,104 @@
[kernel] Parsing tests/value/traces/test1.i (no preprocessing)
+tests/value/traces/test1.i:8:[kernel] warning: Calling undeclared function Frama_C_interval. Old style K&R code?
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
-
-tests/value/traces/test1.i:14:[value] Frama_C_dump_each:
+ g ∈ {42}
+[value] computing for function Frama_C_interval <- main.
+ Called from tests/value/traces/test1.i:8.
+tests/value/traces/test1.i:8:[kernel] warning: Neither code nor specification for function Frama_C_interval, generating default assigns from the prototype
+[value] using specification for function Frama_C_interval
+[value] Done for function Frama_C_interval
+tests/value/traces/test1.i:17:[value] Frama_C_dump_each:
# Cvalue domain:
+ g ∈ {42}
c ∈ [--..--]
- tmp ∈ {4; 5}
+ tmp ∈ {5; 45}
# 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 -> ([ EnterScope: i -> 13 ])
- 8 -> ([ EnterScope: i -> 10 ])
- 10 -> ([ initialize variable: i -> 11 ])
- 11 -> ([ Assign: i = 0 -> 12 ])
- 12 -> ([ enter_loop -> 18 ])
- 13 -> ([ initialize variable: i -> 14 ])
- 14 -> ([ Assign: i = 0 -> 15 ])
- 15 -> ([ enter_loop -> 17 ])
- 17 -> ([ Assume: i < 3 true -> 20 ])
- 18 -> ([ Assume: i < 3 true -> 21 ])
- 20 -> ([ Assign: tmp = tmp + 1 -> 23 ])
- 21 -> ([ Assign: tmp = tmp + 1 -> 22 ])
- 22 -> ([ Assign: i = i + 1 -> 24 ])
- 23 -> ([ Assign: i = i + 1 -> 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 = tmp + 1 -> 34 ])
- 32 -> ([ Assign: tmp = tmp + 1 -> 33 ])
- 33 -> ([ Assign: i = i + 1 -> 36 ])
- 34 -> ([ Assign: i = i + 1 -> 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 = tmp + 1 -> 46 ])
- 44 -> ([ Assign: tmp = tmp + 1 -> 45 ])
- 45 -> ([ Assign: i = i + 1 -> 48 ])
- 46 -> ([ Assign: i = i + 1 -> 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]
+ {[ 0 -> ([ introduce globals -> 1 ])
+ 1 -> ([ initialize variable: g -> 2 ])
+ 2 -> ([ Assign: g = 42 -> 3 ])
+ 3 -> ([ initialize variable using type Main_Formal
+ c -> 4 ])
+ 4 -> ([ EnterScope: tmp -> 5 ])
+ 5 -> ([ start_call: Frama_C_interval (false) -> 6 ])
+ 6 -> ([ EnterScope: x_0 x_1 -> 7 ])
+ 7 -> ([ Assign: x_0 = 0 -> 8 ])
+ 8 -> ([ Assign: x_1 = 1 -> 9 ])
+ 9 -> ([ EnterScope: \result<Frama_C_interval> -> 10 ])
+ 10 -> ([ initialize variable using type Spec_Return(Frama_C_interval)
+ \result<Frama_C_interval> -> 11 ])
+ 11 -> ([ logic assign -> 12 ])
+ 12 -> ([ LeaveScope: x_0 x_1 -> 13 ])
+ 13 -> ([ finalize_call: Frama_C_interval -> 14 ])
+ 14 -> ([ Assign: c = \result<Frama_C_interval> -> 15 ])
+ 15 -> ([ LeaveScope: \result<Frama_C_interval> -> 16 ])
+ 16 -> ([ Assign: tmp = 0 -> 17 ])
+ 17 -> ([ Assume: c false -> 18; Assume: c true -> 19 ])
+ 18 -> ([ Assign: tmp = 2 -> 22 ])
+ 19 -> ([ Assign: tmp = g -> 21 ])
+ 21 -> ([ EnterScope: i -> 27 ])
+ 22 -> ([ EnterScope: i -> 24 ])
+ 24 -> ([ initialize variable: i -> 25 ])
+ 25 -> ([ Assign: i = 0 -> 26 ])
+ 26 -> ([ enter_loop -> 32 ])
+ 27 -> ([ initialize variable: i -> 28 ])
+ 28 -> ([ Assign: i = 0 -> 29 ])
+ 29 -> ([ enter_loop -> 31 ])
+ 31 -> ([ Assume: i < 3 true -> 34 ])
+ 32 -> ([ Assume: i < 3 true -> 35 ])
+ 34 -> ([ Assign: tmp = tmp + 1 -> 37 ])
+ 35 -> ([ Assign: tmp = tmp + 1 -> 36 ])
+ 36 -> ([ Assign: i = i + 1 -> 38 ])
+ 37 -> ([ Assign: i = i + 1 -> 39 ])
+ 38 -> ([ incr_loop_counter -> 42 ])
+ 39 -> ([ incr_loop_counter -> 41 ])
+ 41 -> ([ Assume: i < 3 true -> 45 ])
+ 42 -> ([ Assume: i < 3 true -> 46 ])
+ 45 -> ([ Assign: tmp = tmp + 1 -> 48 ])
+ 46 -> ([ Assign: tmp = tmp + 1 -> 47 ])
+ 47 -> ([ Assign: i = i + 1 -> 50 ])
+ 48 -> ([ Assign: i = i + 1 -> 49 ])
+ 49 -> ([ incr_loop_counter -> 54 ])
+ 50 -> ([ incr_loop_counter -> 53 ])
+ 53 -> ([ Assume: i < 3 true -> 57 ])
+ 54 -> ([ Assume: i < 3 true -> 58 ])
+ 57 -> ([ Assign: tmp = tmp + 1 -> 60 ])
+ 58 -> ([ Assign: tmp = tmp + 1 -> 59 ])
+ 59 -> ([ Assign: i = i + 1 -> 62 ])
+ 60 -> ([ Assign: i = i + 1 -> 61 ])
+ 61 -> ([ incr_loop_counter -> 66 ])
+ 62 -> ([ incr_loop_counter -> 65 ])
+ 65 -> ([ Assume: i < 3 false -> 69 ])
+ 66 -> ([ Assume: i < 3 false -> 70 ])
+ 69 -> ([ leave_loop -> 72 ])
+ 70 -> ([ leave_loop -> 71 ])
+ 71 -> ([ LeaveScope: i -> 74 ])
+ 72 -> ([ LeaveScope: i -> 73 ])
+ 73 -> ([ join -> 75 ])
+ 74 -> ([ join -> 75 ]) ]}
+ current: 75]
==END OF DUMP==
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
- tmp ∈ {4; 5}
+ c ∈ [--..--]
+ tmp ∈ {5; 45}
[from] Computing for function main
+[from] Computing for function Frama_C_interval <-main
+[from] Done for function Frama_C_interval
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ \result FROM x_0; x_1
[from] Function main:
- \result FROM c
+ \result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- tmp; i
+ c; tmp; i
[inout] Inputs for function main:
- \nothing
+ g
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 7a40e8f876e..4bb771e5685 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -24,8 +24,8 @@ tests/value/traces/test2.i:20:[value] Frama_C_dump_each:
3 -> ([ Assume: c false -> 4; Assume: c true -> 5 ])
4 -> ([ Assign: tmp = 2 -> 8 ])
5 -> ([ Assign: tmp = 1 -> 7 ])
- 7 -> ([ start_call: loop -> 9 ])
- 8 -> ([ start_call: loop -> 55 ])
+ 7 -> ([ start_call: loop (true) -> 9 ])
+ 8 -> ([ start_call: loop (true) -> 55 ])
9 -> ([ EnterScope: j -> 10 ])
10 -> ([ Assign: j = tmp -> 11 ])
11 -> ([ EnterScope: i -> 12 ])
diff --git a/tests/value/traces/test1.i b/tests/value/traces/test1.i
index 968a978ea61..5cedf0de7d9 100644
--- a/tests/value/traces/test1.i
+++ b/tests/value/traces/test1.i
@@ -2,10 +2,13 @@
STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10"
*/
+int g = 42;
+
int main(int c){
+ c = Frama_C_interval(0,1);
int tmp;
tmp = 0;
- if (c) tmp = 1;
+ if (c) tmp = g;
else tmp = 2;
for(int i = 0; i < 3; i++){
tmp ++;
--
GitLab