Skip to content
GitLab
Commit 975c9cfd authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Merge branch 'fix/eva/split-predicate' into 'master' 

[Eva] Fixes partitioning splits on ACSL predicates.

See merge request frama-c/frama-c!4046
parents 3c6a2fc8 65d9b00f
Hide whitespace changes
Inline Side-by-side
src/plugins/eva/partitioning/partition.ml
View file @ 975c9cfd
......@@ -470,20 +470,24 @@ struct
let states = function _ -> Abstract.Dom.top in
Abstract_domain.{ states; result = None }
in
let source = fst (predicate.Cil_types.pred_loc) in
let aux positive =
let+ state' =
Abstract.Dom.reduce_by_predicate env state predicate positive in
let x = Abstract.Dom.evaluate_predicate env state' predicate in
if x == Unknown
then
Self.warning ~source ~once:true
"failing to learn perfectly from split predicate";
if Abstract.Dom.equal state' state then raise Operation_failed;
let value = if positive then Integer.one else Integer.zero in
value, state'
in
Bottom.list_values [ aux true; aux false ]
match Abstract.Dom.evaluate_predicate env state predicate with
| True -> [ Integer.one, state ]
| False -> [ Integer.zero, state ]
| Unknown ->
let source = fst (predicate.Cil_types.pred_loc) in
let aux positive =
let+ state' =
Abstract.Dom.reduce_by_predicate env state predicate positive in
let x = Abstract.Dom.evaluate_predicate env state' predicate in
if x == Unknown
then
Self.warning ~source ~once:true
"failing to learn perfectly from split predicate";
if Abstract.Dom.equal state' state then raise Operation_failed;
let value = if positive then Integer.one else Integer.zero in
value, state'
in
Bottom.list_values [ aux true; aux false ]
(* --- Applying partitioning actions onto flows --------------------------- *)
......
tests/value/oracle/partitioning-annots.0.res.oracle
View file @ 975c9cfd
......@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function test_slevel <- main.
Called from partitioning-annots.c:205.
[eva] partitioning-annots.c:170: starting to merge loop iterations
[eva] partitioning-annots.c:175: starting to merge loop iterations
Called from partitioning-annots.c:223.
[eva] partitioning-annots.c:188: starting to merge loop iterations
[eva] partitioning-annots.c:193: starting to merge loop iterations
[eva] Recording results for test_slevel
[eva] Done for function test_slevel
[eva] computing for function test_unroll <- main.
Called from partitioning-annots.c:206.
Called from partitioning-annots.c:224.
[eva:loop-unroll:partial] partitioning-annots.c:26: loop not completely unrolled
[eva] partitioning-annots.c:26: starting to merge loop iterations
[eva:loop-unroll:partial] partitioning-annots.c:34: loop not completely unrolled
......@@ -25,7 +25,7 @@
[eva] Recording results for test_unroll
[eva] Done for function test_unroll
[eva] computing for function test_split <- main.
Called from partitioning-annots.c:207.
Called from partitioning-annots.c:225.
[eva] computing for function Frama_C_interval <- test_split <- main.
Called from partitioning-annots.c:73.
[eva] using specification for function Frama_C_interval
......@@ -65,7 +65,7 @@
[eva] Recording results for test_split
[eva] Done for function test_split
[eva] computing for function test_dynamic_split <- main.
Called from partitioning-annots.c:208.
Called from partitioning-annots.c:226.
[eva] partitioning-annots.c:95: Warning:
this partitioning parameter cannot be evaluated safely on all states
[eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
......@@ -89,6 +89,11 @@
[eva] partitioning-annots.c:109: Frama_C_show_each_no_split: {0}, {0; 1; 2}
[eva] Recording results for test_dynamic_split
[eva] Done for function test_dynamic_split
[eva] computing for function test_dynamic_split_predicate <- main.
Called from partitioning-annots.c:227.
[eva] partitioning-annots.c:124: starting to merge loop iterations
[eva] Recording results for test_dynamic_split_predicate
[eva] Done for function test_dynamic_split_predicate
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
......@@ -96,6 +101,10 @@
Frama_C_entropy_source ∈ [--..--]
a ∈ {0}
b ∈ {0; 1; 2}
[eva:final-states] Values at end of function test_dynamic_split_predicate:
x ∈ [0..44]
y ∈ [0..44]
c ∈ [--..--]
[eva:final-states] Values at end of function test_slevel:
a[0..9] ∈ {42}
b[0..9] ∈ {42} or UNINITIALIZED
......@@ -140,6 +149,8 @@
[from] Computing for function Frama_C_interval <-test_dynamic_split
[from] Done for function Frama_C_interval
[from] Done for function test_dynamic_split
[from] Computing for function test_dynamic_split_predicate
[from] Done for function test_dynamic_split_predicate
[from] Computing for function test_slevel
[from] Done for function test_slevel
[from] Computing for function test_split
......@@ -155,6 +166,8 @@
\result FROM Frama_C_entropy_source; min; max
[from] Function test_dynamic_split:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
[from] Function test_dynamic_split_predicate:
NO EFFECTS
[from] Function test_slevel:
NO EFFECTS
[from] Function test_split:
......@@ -170,6 +183,10 @@
Frama_C_entropy_source; a; b
[inout] Inputs for function test_dynamic_split:
Frama_C_entropy_source; nondet
[inout] Out (internal) for function test_dynamic_split_predicate:
x; y; c; i
[inout] Inputs for function test_dynamic_split_predicate:
nondet
[inout] Out (internal) for function test_slevel:
a[0..9]; b[0..9]; c[0..9]; d[0..9]; e[0..3]; i; i_0; i_1; i_2; i_3
[inout] Inputs for function test_slevel:
......
tests/value/oracle/partitioning-annots.2.res.oracle
View file @ 975c9cfd
......@@ -6,41 +6,41 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] using specification for function Frama_C_interval
[eva] partitioning-annots.c:127:
[eva] partitioning-annots.c:145:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva] partitioning-annots.c:125: starting to merge loop iterations
[eva] partitioning-annots.c:143: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
Called from partitioning-annots.c:127.
Called from partitioning-annots.c:145.
[eva] Done for function Frama_C_interval
[eva:alarm] partitioning-annots.c:134: Warning:
[eva:alarm] partitioning-annots.c:152: Warning:
accessing uninitialized left-value. assert \initialized(&A[i]);
[eva] partitioning-annots.c:139: Frama_C_show_each: {9}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {8}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {7}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {6}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {5}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {4}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {3}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {2}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {1}, {42}
[eva] partitioning-annots.c:139: Frama_C_show_each: {0}, {42}
[eva] partitioning-annots.c:140: assertion got status valid.
[eva] partitioning-annots.c:143: Frama_C_show_each: {{ "Value 42 not found" }}
[eva] partitioning-annots.c:157: Frama_C_show_each: {9}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {8}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {7}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {6}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {5}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {4}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {3}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {2}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {1}, {42}
[eva] partitioning-annots.c:157: Frama_C_show_each: {0}, {42}
[eva] partitioning-annots.c:158: assertion got status valid.
[eva] partitioning-annots.c:161: Frama_C_show_each: {{ "Value 42 not found" }}
[eva] Recording results for test_loop_split
[eva] done for function test_loop_split
[eva] ====== VALUES COMPUTED ======
......
tests/value/oracle/partitioning-annots.3.res.oracle
View file @ 975c9cfd
......@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_history.
Called from partitioning-annots.c:149.
Called from partitioning-annots.c:167.
[eva] using specification for function Frama_C_interval
[eva] partitioning-annots.c:149:
[eva] partitioning-annots.c:167:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] partitioning-annots.c:155: Frama_C_show_each: {0; 1}, {0; 1}
[eva:alarm] partitioning-annots.c:158: Warning:
[eva] partitioning-annots.c:173: Frama_C_show_each: {0; 1}, {0; 1}
[eva:alarm] partitioning-annots.c:176: Warning:
division by zero. assert j ≢ 0;
[eva] Recording results for test_history
[eva] done for function test_history
......
tests/value/oracle/partitioning-annots.4.res.oracle
View file @ 975c9cfd
......@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_history.
Called from partitioning-annots.c:149.
Called from partitioning-annots.c:167.
[eva] using specification for function Frama_C_interval
[eva] partitioning-annots.c:149:
[eva] partitioning-annots.c:167:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] partitioning-annots.c:155: Frama_C_show_each: {0}, {0}
[eva] partitioning-annots.c:155: Frama_C_show_each: {1}, {1}
[eva] partitioning-annots.c:173: Frama_C_show_each: {0}, {0}
[eva] partitioning-annots.c:173: Frama_C_show_each: {1}, {1}
[eva] Recording results for test_history
[eva] done for function test_history
[eva] ====== VALUES COMPUTED ======
......
tests/value/oracle_apron/partitioning-annots.0.res.oracle 0 → 100644
View file @ 975c9cfd
105,106c105,106
< x ∈ [0..44]
< y ∈ [0..44]
---
> x ∈ [31..44]
> y ∈ [31..44]
tests/value/oracle_apron/partitioning-annots.3.res.oracle
View file @ 975c9cfd
15,16d14
< [eva:alarm] partitioning-annots.c:158: Warning:
< [eva:alarm] partitioning-annots.c:176: Warning:
< division by zero. assert j ≢ 0;
tests/value/oracle_multidim/partitioning-annots.2.res.oracle
View file @ 975c9cfd
30,31d29
< [eva:alarm] partitioning-annots.c:134: Warning:
< [eva:alarm] partitioning-annots.c:152: Warning:
< accessing uninitialized left-value. assert \initialized(&A[i]);
tests/value/oracle_octagon/partitioning-annots.0.res.oracle 0 → 100644
View file @ 975c9cfd
105,106c105,106
< x ∈ [0..44]
< y ∈ [0..44]
---
> x ∈ {31; 32; 44}
> y ∈ {31; 32; 44}
tests/value/partitioning-annots.c
View file @ 975c9cfd
/* run.config*
STDOPT: #"-eva-default-loop-unroll 10"
STDOPT: +"-main test_split -eva-partition-value k"
STDOPT: #"-main test_loop_split -eva-partition-history 1"
......@@ -109,6 +109,24 @@ void test_dynamic_split()
Frama_C_show_each_no_split(a, b);
}
void test_dynamic_split_predicate()
{
int x, y;
//@ dynamic_split \initialized(&x);
int c = nondet;
if (c != 1) {
x = 42;
}
y = 2;
if (c != 1)
x += y; // No alarm on x initialization with the dynamic partitioning.
else {
for (int i = 0; i < 32; i++)
x = i;
}
y = x; // No alarm on x initialization with the dynamic partitioning.
}
void test_loop_split()
{
int A[N];
......@@ -165,7 +183,7 @@ void test_slevel()
for (int i = 0; i < N; i++) {
a[i] = 42;
}
//@slevel default;
for (int i = 0; i < N; i++) {
b[i] = 42;
......@@ -188,7 +206,7 @@ void test_slevel()
//@slevel merge;
; // Otherwise previous annotation is ignored
}
//@slevel 0;
;
//@slevel full;
......@@ -206,5 +224,5 @@ void main(void)
test_unroll();
test_split();
test_dynamic_split();
test_dynamic_split_predicate();
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment