From c14f7338bfdb51cf866dfa44ae6dd0e85eed3cac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 2 Apr 2021 13:02:10 +0200
Subject: [PATCH] [Eva] Fixes the location of the message about the automatic
loop unrolling.
When two loops follow each other, the automatic loop unrolling is performed on
the transition edge between the two, where the current statement (from
Cil.CurrentLoc) is still the first loop.
Adds a test for this case.
---
src/plugins/value/partitioning/partition.ml | 3 +-
tests/value/auto_loop_unroll.c | 29 +++++++++++++
.../oracle/auto_loop_unroll.0.res.oracle | 43 ++++++++++++++++---
.../oracle/auto_loop_unroll.1.res.oracle | 35 ++++++++++++---
4 files changed, 95 insertions(+), 15 deletions(-)
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index fe65ccb612e..a7138c912d6 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -412,7 +412,8 @@ struct
match AutoLoopUnroll.compute ~max_unroll x stmt with
| None -> min_unroll
| Some i ->
- Value_parameters.warning ~once:true ~current:true
+ let source = fst (Cil_datatype.Stmt.loc stmt) in
+ Value_parameters.warning ~once:true ~current:true ~source
~wkey:Value_parameters.wkey_loop_unroll
"Automatic loop unrolling.";
i
diff --git a/tests/value/auto_loop_unroll.c b/tests/value/auto_loop_unroll.c
index ec9519bbcc7..1d083a1c841 100644
--- a/tests/value/auto_loop_unroll.c
+++ b/tests/value/auto_loop_unroll.c
@@ -384,6 +384,34 @@ void non_natural_loops () {
res = 0;
}
+/* Tests the automatic loop unrolling on loops that follow directly each other. */
+void following_loops () {
+ int i = 0, j = 0;
+ while (i < 15) {
+ i++;
+ j++;
+ }
+ while (i < 30) {
+ i++;
+ j++;
+ }
+ Frama_C_show_each_30(j);
+ i = 0;
+ j = 0;
+ while (i < 15 && undet) {
+ i++;
+ j++;
+ }
+ while (i < 30) {
+ i++;
+ j++;
+ }
+ /* The equality relation between [i] and [j] is lost between the two loops,
+ where all states exiting the first loop are joined. However, the unrolling
+ prevents the value of [j] to be completely imprecise. */
+ Frama_C_show_each_30(j);
+}
+
void main () {
simple_loops ();
various_loops ();
@@ -392,4 +420,5 @@ void main () {
temporary_variables ();
loops_with_goto ();
non_natural_loops ();
+ following_loops ();
}
diff --git a/tests/value/oracle/auto_loop_unroll.0.res.oracle b/tests/value/oracle/auto_loop_unroll.0.res.oracle
index 9f0232a5ddc..f34b2d3391c 100644
--- a/tests/value/oracle/auto_loop_unroll.0.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.0.res.oracle
@@ -6,7 +6,7 @@
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
- Called from tests/value/auto_loop_unroll.c:388.
+ Called from tests/value/auto_loop_unroll.c:416.
[eva] tests/value/auto_loop_unroll.c:24: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:25: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -27,7 +27,7 @@
[eva] Recording results for simple_loops
[eva] Done for function simple_loops
[eva] computing for function various_loops <- main.
- Called from tests/value/auto_loop_unroll.c:389.
+ Called from tests/value/auto_loop_unroll.c:417.
[eva] tests/value/auto_loop_unroll.c:57: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:58: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -146,7 +146,7 @@
[eva] Recording results for various_loops
[eva] Done for function various_loops
[eva] computing for function complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:390.
+ Called from tests/value/auto_loop_unroll.c:418.
[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:154: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -205,7 +205,7 @@
[eva] Recording results for complex_loops
[eva] Done for function complex_loops
[eva] computing for function various_conditions <- main.
- Called from tests/value/auto_loop_unroll.c:391.
+ Called from tests/value/auto_loop_unroll.c:419.
[eva] tests/value/auto_loop_unroll.c:211: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -245,7 +245,7 @@
[eva] Recording results for various_conditions
[eva] Done for function various_conditions
[eva] computing for function temporary_variables <- main.
- Called from tests/value/auto_loop_unroll.c:392.
+ Called from tests/value/auto_loop_unroll.c:420.
[eva] tests/value/auto_loop_unroll.c:262: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:262: Warning:
signed overflow. assert i + 1 ≤ 2147483647;
@@ -279,7 +279,7 @@
[eva] Recording results for temporary_variables
[eva] Done for function temporary_variables
[eva] computing for function loops_with_goto <- main.
- Called from tests/value/auto_loop_unroll.c:393.
+ Called from tests/value/auto_loop_unroll.c:421.
[eva] tests/value/auto_loop_unroll.c:298: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -321,7 +321,7 @@
[eva] Recording results for loops_with_goto
[eva] Done for function loops_with_goto
[eva] computing for function non_natural_loops <- main.
- Called from tests/value/auto_loop_unroll.c:394.
+ Called from tests/value/auto_loop_unroll.c:422.
[eva:alarm] tests/value/auto_loop_unroll.c:371: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
[eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647]
@@ -333,9 +333,30 @@
Frama_C_show_each_1_51: [1..2147483647]
[eva] Recording results for non_natural_loops
[eva] Done for function non_natural_loops
+[eva] computing for function following_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:423.
+[eva] tests/value/auto_loop_unroll.c:390: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:392: Warning:
+ signed overflow. assert j + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:396: Warning:
+ signed overflow. assert j + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:394: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647]
+[eva] tests/value/auto_loop_unroll.c:401: starting to merge loop iterations
+[eva:alarm] tests/value/auto_loop_unroll.c:403: Warning:
+ signed overflow. assert j + 1 ≤ 2147483647;
+[eva:alarm] tests/value/auto_loop_unroll.c:407: Warning:
+ signed overflow. assert j + 1 ≤ 2147483647;
+[eva] tests/value/auto_loop_unroll.c:405: starting to merge loop iterations
+[eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647]
+[eva] Recording results for following_loops
+[eva] Done for function following_loops
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function following_loops:
+ i ∈ {30}
+ j ∈ [0..2147483647]
[eva:final-states] Values at end of function incr:
__retres ∈ [1..2147483647]
[eva:final-states] Values at end of function incr_g:
@@ -383,6 +404,8 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
g ∈ {64}
+[from] Computing for function following_loops
+[from] Done for function following_loops
[from] Computing for function incr
[from] Done for function incr
[from] Computing for function incr_g
@@ -410,6 +433,8 @@
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
+[from] Function following_loops:
+ NO EFFECTS
[from] Function incr:
\result FROM i
[from] Function incr_g:
@@ -433,6 +458,10 @@
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function following_loops:
+ i; j
+[inout] Inputs for function following_loops:
+ undet
[inout] Out (internal) for function incr:
__retres
[inout] Inputs for function incr:
diff --git a/tests/value/oracle/auto_loop_unroll.1.res.oracle b/tests/value/oracle/auto_loop_unroll.1.res.oracle
index 315adc3135a..1826be4c45b 100644
--- a/tests/value/oracle/auto_loop_unroll.1.res.oracle
+++ b/tests/value/oracle/auto_loop_unroll.1.res.oracle
@@ -6,7 +6,7 @@
undet ∈ [--..--]
g ∈ {0}
[eva] computing for function simple_loops <- main.
- Called from tests/value/auto_loop_unroll.c:388.
+ Called from tests/value/auto_loop_unroll.c:416.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:24: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:24:
Trace partitioning superposing up to 100 states
@@ -25,7 +25,7 @@
[eva] Recording results for simple_loops
[eva] Done for function simple_loops
[eva] computing for function various_loops <- main.
- Called from tests/value/auto_loop_unroll.c:389.
+ Called from tests/value/auto_loop_unroll.c:417.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:57: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:62: Automatic loop unrolling.
@@ -287,7 +287,7 @@
[eva] Recording results for various_loops
[eva] Done for function various_loops
[eva] computing for function complex_loops <- main.
- Called from tests/value/auto_loop_unroll.c:390.
+ Called from tests/value/auto_loop_unroll.c:418.
[eva] tests/value/auto_loop_unroll.c:152: starting to merge loop iterations
[eva:alarm] tests/value/auto_loop_unroll.c:154: Warning:
signed overflow. assert res + 1 ≤ 2147483647;
@@ -346,7 +346,7 @@
[eva] Recording results for complex_loops
[eva] Done for function complex_loops
[eva] computing for function various_conditions <- main.
- Called from tests/value/auto_loop_unroll.c:391.
+ Called from tests/value/auto_loop_unroll.c:419.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:211: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:216: Automatic loop unrolling.
@@ -366,7 +366,7 @@
[eva] Recording results for various_conditions
[eva] Done for function various_conditions
[eva] computing for function temporary_variables <- main.
- Called from tests/value/auto_loop_unroll.c:392.
+ Called from tests/value/auto_loop_unroll.c:420.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:262: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: {20}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:267: Automatic loop unrolling.
@@ -384,7 +384,7 @@
[eva] Recording results for temporary_variables
[eva] Done for function temporary_variables
[eva] computing for function loops_with_goto <- main.
- Called from tests/value/auto_loop_unroll.c:393.
+ Called from tests/value/auto_loop_unroll.c:421.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:298: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:307: Automatic loop unrolling.
@@ -417,16 +417,29 @@
[eva] Recording results for loops_with_goto
[eva] Done for function loops_with_goto
[eva] computing for function non_natural_loops <- main.
- Called from tests/value/auto_loop_unroll.c:394.
+ Called from tests/value/auto_loop_unroll.c:422.
[eva:loop-unroll] tests/value/auto_loop_unroll.c:370: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50}
[eva:loop-unroll] tests/value/auto_loop_unroll.c:379: Automatic loop unrolling.
[eva] tests/value/auto_loop_unroll.c:383: Frama_C_show_each_1_51: [1..51]
[eva] Recording results for non_natural_loops
[eva] Done for function non_natural_loops
+[eva] computing for function following_loops <- main.
+ Called from tests/value/auto_loop_unroll.c:423.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:390: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:394: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30}
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:401: Automatic loop unrolling.
+[eva:loop-unroll] tests/value/auto_loop_unroll.c:405: Automatic loop unrolling.
+[eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45]
+[eva] Recording results for following_loops
+[eva] Done for function following_loops
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function following_loops:
+ i ∈ {30}
+ j ∈ [15..45]
[eva:final-states] Values at end of function incr:
__retres ∈ [1..25]
[eva:final-states] Values at end of function incr_g:
@@ -474,6 +487,8 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
g ∈ {64}
+[from] Computing for function following_loops
+[from] Done for function following_loops
[from] Computing for function incr
[from] Done for function incr
[from] Computing for function incr_g
@@ -501,6 +516,8 @@
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
+[from] Function following_loops:
+ NO EFFECTS
[from] Function incr:
\result FROM i
[from] Function incr_g:
@@ -524,6 +541,10 @@
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
g FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function following_loops:
+ i; j
+[inout] Inputs for function following_loops:
+ undet
[inout] Out (internal) for function incr:
__retres
[inout] Inputs for function incr:
--
GitLab