From 9bbfa14c828114fbd4ca9f858d736f2dbc9dd146 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 19 Jun 2019 17:07:20 +0200
Subject: [PATCH] [Eva] Update section Loop Unrolling
---
.../parametrizing/loop-unroll-const.c | 11 +
.../parametrizing/loop-unroll-const.log | 222 ++++++++++++++++++
.../parametrizing/loop-unroll-insuf.c | 5 +
.../parametrizing/loop-unroll-insuf.log | 23 ++
.../parametrizing/loop-unroll-nested.c | 13 +
.../parametrizing/loop-unroll-nested.log | 43 ++++
doc/value/examples/parametrizing/makefile | 5 +-
doc/value/main.tex | 53 +++--
8 files changed, 348 insertions(+), 27 deletions(-)
create mode 100644 doc/value/examples/parametrizing/loop-unroll-const.c
create mode 100644 doc/value/examples/parametrizing/loop-unroll-const.log
create mode 100644 doc/value/examples/parametrizing/loop-unroll-insuf.c
create mode 100644 doc/value/examples/parametrizing/loop-unroll-insuf.log
create mode 100644 doc/value/examples/parametrizing/loop-unroll-nested.c
create mode 100644 doc/value/examples/parametrizing/loop-unroll-nested.log
diff --git a/doc/value/examples/parametrizing/loop-unroll-const.c b/doc/value/examples/parametrizing/loop-unroll-const.c
new file mode 100644
index 00000000000..dad47c0b399
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-const.c
@@ -0,0 +1,11 @@
+#define NROWS 10
+void main(void) {
+ int a[NROWS][20] = {0};
+ //@ loop unroll NROWS;
+ for (int i = 0; i < 10; i++) {
+ //@ loop unroll (10+10);
+ for (int j = 0; j < 20; j++) {
+ a[i][j] += i + j;
+ }
+ }
+}
diff --git a/doc/value/examples/parametrizing/loop-unroll-const.log b/doc/value/examples/parametrizing/loop-unroll-const.log
new file mode 100644
index 00000000000..9071ef76070
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-const.log
@@ -0,0 +1,222 @@
+[kernel] Parsing loop-unroll-const.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] loop-unroll-const.c:7: Trace partitioning superposing up to 100 states
+[eva] loop-unroll-const.c:7: Trace partitioning superposing up to 200 states
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ a[0][0] ∈ {0}
+ [0][1] ∈ {1}
+ [0][2] ∈ {2}
+ [0][3] ∈ {3}
+ [0][4] ∈ {4}
+ [0][5] ∈ {5}
+ [0][6] ∈ {6}
+ [0][7] ∈ {7}
+ [0][8] ∈ {8}
+ [0][9] ∈ {9}
+ [0][10] ∈ {10}
+ [0][11] ∈ {11}
+ [0][12] ∈ {12}
+ [0][13] ∈ {13}
+ [0][14] ∈ {14}
+ [0][15] ∈ {15}
+ [0][16] ∈ {16}
+ [0][17] ∈ {17}
+ [0][18] ∈ {18}
+ [0][19] ∈ {19}
+ [1][0] ∈ {1}
+ [1][1] ∈ {2}
+ [1][2] ∈ {3}
+ [1][3] ∈ {4}
+ [1][4] ∈ {5}
+ [1][5] ∈ {6}
+ [1][6] ∈ {7}
+ [1][7] ∈ {8}
+ [1][8] ∈ {9}
+ [1][9] ∈ {10}
+ [1][10] ∈ {11}
+ [1][11] ∈ {12}
+ [1][12] ∈ {13}
+ [1][13] ∈ {14}
+ [1][14] ∈ {15}
+ [1][15] ∈ {16}
+ [1][16] ∈ {17}
+ [1][17] ∈ {18}
+ [1][18] ∈ {19}
+ [1][19] ∈ {20}
+ [2][0] ∈ {2}
+ [2][1] ∈ {3}
+ [2][2] ∈ {4}
+ [2][3] ∈ {5}
+ [2][4] ∈ {6}
+ [2][5] ∈ {7}
+ [2][6] ∈ {8}
+ [2][7] ∈ {9}
+ [2][8] ∈ {10}
+ [2][9] ∈ {11}
+ [2][10] ∈ {12}
+ [2][11] ∈ {13}
+ [2][12] ∈ {14}
+ [2][13] ∈ {15}
+ [2][14] ∈ {16}
+ [2][15] ∈ {17}
+ [2][16] ∈ {18}
+ [2][17] ∈ {19}
+ [2][18] ∈ {20}
+ [2][19] ∈ {21}
+ [3][0] ∈ {3}
+ [3][1] ∈ {4}
+ [3][2] ∈ {5}
+ [3][3] ∈ {6}
+ [3][4] ∈ {7}
+ [3][5] ∈ {8}
+ [3][6] ∈ {9}
+ [3][7] ∈ {10}
+ [3][8] ∈ {11}
+ [3][9] ∈ {12}
+ [3][10] ∈ {13}
+ [3][11] ∈ {14}
+ [3][12] ∈ {15}
+ [3][13] ∈ {16}
+ [3][14] ∈ {17}
+ [3][15] ∈ {18}
+ [3][16] ∈ {19}
+ [3][17] ∈ {20}
+ [3][18] ∈ {21}
+ [3][19] ∈ {22}
+ [4][0] ∈ {4}
+ [4][1] ∈ {5}
+ [4][2] ∈ {6}
+ [4][3] ∈ {7}
+ [4][4] ∈ {8}
+ [4][5] ∈ {9}
+ [4][6] ∈ {10}
+ [4][7] ∈ {11}
+ [4][8] ∈ {12}
+ [4][9] ∈ {13}
+ [4][10] ∈ {14}
+ [4][11] ∈ {15}
+ [4][12] ∈ {16}
+ [4][13] ∈ {17}
+ [4][14] ∈ {18}
+ [4][15] ∈ {19}
+ [4][16] ∈ {20}
+ [4][17] ∈ {21}
+ [4][18] ∈ {22}
+ [4][19] ∈ {23}
+ [5][0] ∈ {5}
+ [5][1] ∈ {6}
+ [5][2] ∈ {7}
+ [5][3] ∈ {8}
+ [5][4] ∈ {9}
+ [5][5] ∈ {10}
+ [5][6] ∈ {11}
+ [5][7] ∈ {12}
+ [5][8] ∈ {13}
+ [5][9] ∈ {14}
+ [5][10] ∈ {15}
+ [5][11] ∈ {16}
+ [5][12] ∈ {17}
+ [5][13] ∈ {18}
+ [5][14] ∈ {19}
+ [5][15] ∈ {20}
+ [5][16] ∈ {21}
+ [5][17] ∈ {22}
+ [5][18] ∈ {23}
+ [5][19] ∈ {24}
+ [6][0] ∈ {6}
+ [6][1] ∈ {7}
+ [6][2] ∈ {8}
+ [6][3] ∈ {9}
+ [6][4] ∈ {10}
+ [6][5] ∈ {11}
+ [6][6] ∈ {12}
+ [6][7] ∈ {13}
+ [6][8] ∈ {14}
+ [6][9] ∈ {15}
+ [6][10] ∈ {16}
+ [6][11] ∈ {17}
+ [6][12] ∈ {18}
+ [6][13] ∈ {19}
+ [6][14] ∈ {20}
+ [6][15] ∈ {21}
+ [6][16] ∈ {22}
+ [6][17] ∈ {23}
+ [6][18] ∈ {24}
+ [6][19] ∈ {25}
+ [7][0] ∈ {7}
+ [7][1] ∈ {8}
+ [7][2] ∈ {9}
+ [7][3] ∈ {10}
+ [7][4] ∈ {11}
+ [7][5] ∈ {12}
+ [7][6] ∈ {13}
+ [7][7] ∈ {14}
+ [7][8] ∈ {15}
+ [7][9] ∈ {16}
+ [7][10] ∈ {17}
+ [7][11] ∈ {18}
+ [7][12] ∈ {19}
+ [7][13] ∈ {20}
+ [7][14] ∈ {21}
+ [7][15] ∈ {22}
+ [7][16] ∈ {23}
+ [7][17] ∈ {24}
+ [7][18] ∈ {25}
+ [7][19] ∈ {26}
+ [8][0] ∈ {8}
+ [8][1] ∈ {9}
+ [8][2] ∈ {10}
+ [8][3] ∈ {11}
+ [8][4] ∈ {12}
+ [8][5] ∈ {13}
+ [8][6] ∈ {14}
+ [8][7] ∈ {15}
+ [8][8] ∈ {16}
+ [8][9] ∈ {17}
+ [8][10] ∈ {18}
+ [8][11] ∈ {19}
+ [8][12] ∈ {20}
+ [8][13] ∈ {21}
+ [8][14] ∈ {22}
+ [8][15] ∈ {23}
+ [8][16] ∈ {24}
+ [8][17] ∈ {25}
+ [8][18] ∈ {26}
+ [8][19] ∈ {27}
+ [9][0] ∈ {9}
+ [9][1] ∈ {10}
+ [9][2] ∈ {11}
+ [9][3] ∈ {12}
+ [9][4] ∈ {13}
+ [9][5] ∈ {14}
+ [9][6] ∈ {15}
+ [9][7] ∈ {16}
+ [9][8] ∈ {17}
+ [9][9] ∈ {18}
+ [9][10] ∈ {19}
+ [9][11] ∈ {20}
+ [9][12] ∈ {21}
+ [9][13] ∈ {22}
+ [9][14] ∈ {23}
+ [9][15] ∈ {24}
+ [9][16] ∈ {25}
+ [9][17] ∈ {26}
+ [9][18] ∈ {27}
+ [9][19] ∈ {28}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 16 statements reached (out of 16): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/loop-unroll-insuf.c b/doc/value/examples/parametrizing/loop-unroll-insuf.c
new file mode 100644
index 00000000000..5058c9d4046
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-insuf.c
@@ -0,0 +1,5 @@
+void main() {
+ //@ loop unroll 20; // should be 21
+ for (int i = 0 ; i <= 20 ; i ++) {
+ }
+}
\ No newline at end of file
diff --git a/doc/value/examples/parametrizing/loop-unroll-insuf.log b/doc/value/examples/parametrizing/loop-unroll-insuf.log
new file mode 100644
index 00000000000..7527748a566
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-insuf.log
@@ -0,0 +1,23 @@
+[kernel] Parsing loop-unroll-insuf.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva:loop-unroll] loop-unroll-insuf.c:3: loop not completely unrolled
+[eva] loop-unroll-insuf.c:3: starting to merge loop iterations
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ i ∈ {21}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 6 statements reached (out of 6): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/loop-unroll-nested.c b/doc/value/examples/parametrizing/loop-unroll-nested.c
new file mode 100644
index 00000000000..7205a6d088a
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-nested.c
@@ -0,0 +1,13 @@
+int t1[] = {1, 2, 3}, t2[] = {4, 5}, t3[] = {6, 7, 8, 9};
+int *t[] = {t1, t2, t3};
+int sizes[] = {3, 2, 4};
+void main(void) {
+ int S = 0;
+ // loop unroll 3;
+ for (int i = 0 ; i < 3 ; i++) {
+ // loop unroll sizes[i];
+ for (int j = 0 ; j < sizes[i] ; j++) {
+ S += t[i][j];
+ }
+ }
+}
diff --git a/doc/value/examples/parametrizing/loop-unroll-nested.log b/doc/value/examples/parametrizing/loop-unroll-nested.log
new file mode 100644
index 00000000000..5ff936dc948
--- /dev/null
+++ b/doc/value/examples/parametrizing/loop-unroll-nested.log
@@ -0,0 +1,43 @@
+[kernel] Parsing loop-unroll-nested.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ t1[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ t2[0] ∈ {4}
+ [1] ∈ {5}
+ t3[0] ∈ {6}
+ [1] ∈ {7}
+ [2] ∈ {8}
+ [3] ∈ {9}
+ t[0] ∈ {{ &t1[0] }}
+ [1] ∈ {{ &t2[0] }}
+ [2] ∈ {{ &t3[0] }}
+ sizes[0] ∈ {3}
+ [1] ∈ {2}
+ [2] ∈ {4}
+[eva] loop-unroll-nested.c:9: starting to merge loop iterations
+[eva:alarm] loop-unroll-nested.c:10: Warning:
+ signed overflow. assert S + *(t[i] + j) ≤ 2147483647;
+[eva] loop-unroll-nested.c:7: starting to merge loop iterations
+[eva:alarm] loop-unroll-nested.c:10: Warning:
+ out of bounds read. assert \valid_read(t[i] + j);
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ S ∈ [0..2147483647]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 16 statements reached (out of 16): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 2 alarms generated by the analysis:
+ 1 invalid memory access
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/makefile b/doc/value/examples/parametrizing/makefile
index 5c550ea370e..74f6d633930 100644
--- a/doc/value/examples/parametrizing/makefile
+++ b/doc/value/examples/parametrizing/makefile
@@ -14,7 +14,10 @@ TARGETS = \
nor.1.log \
nor.2.log \
ilevel.1.log \
- ilevel.2.log
+ ilevel.2.log \
+ loop-unroll-const.log \
+ loop-unroll-nested.log \
+ loop-unroll-insuf.log
.SECONDEXPANSION:
.PHONY: all clean
diff --git a/doc/value/main.tex b/doc/value/main.tex
index a541d32a9a7..62fb14dd0f0 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -3308,29 +3308,35 @@ iteration, avoiding merging states from different iterations.
This leads to increased cost in terms of analysis, but usually the cost
increase is worth the improvement in precision.
-Such annotations must be placed before just before the loop (i.e. before the
+Such annotations must be placed just before the loop (i.e. before the
\lstinline|while|, \lstinline|for| or \lstinline|do| introducing the loop),
and one annotation is required per loop, including nested ones. For instance:
-\begin{lstlisting}
-#define NROWS 10
-void main() {
- int a[NROWS][20] = {0};
- //@ loop unroll NROWS;
- for (int i = 0; i < 10; i++) {
- //@ loop unroll (10+10);
- for (int j = 0; j < 20; j++) {
- a[i][j] += i + j;
- }
- }
-}
-\end{lstlisting}
+\lstinputlisting{examples/parametrizing/loop-unroll-const.c}
-Note that constants obtained via \lstinline|#define| macros can be used in
-annotations, as well as constant expressions. The annotations above will ensure
+The annotations above will ensure
that \Eva{} will unroll the loops and keep the analysis precise; otherwise,
the array access \lstinline|a[i][j]| might generate alarms due to imprecisions.
+The \lstinline|loop unroll| parameter can be any C expression such that there
+is only one possible integer value found by \Eva{} for this expression.
+Constants obtained via \lstinline|#define| macros, variables which always have
+a unique value or a combination of these with arithmetic operator are
+suitable. For expressions which do not obviously represent only one integer,
+the acceptability of the annotation depends on the precision of the analyzer.
+Note that there are interesting cases of non-constant expression for
+unrolling annotations. The example below shows a function with two nested loops.
+
+\lstinputlisting{examples/parametrizing/loop-unroll-nested.c}
+
+The number of iterations of the outer one is constant while the number of
+iterations of the inner one is variable but depends on the current iteration of
+the outer loop. However, if we instructs \Eva{} to unroll the outer loop then
+the parameter \lstinline|sizes[i]| of the \lstinline|loop unroll| annotation
+always evaluate to a single possible integer and thus the inner loop annotation
+is accepted. Note that, in this example, it is also possible to use an upper
+bound like $4$.
+
The unrolling mechanism is independent of \lstinline|-eva-slevel|
(see next subsection): annotated loops are always unrolled at least the specified
number of times. If the loop has not been entirely unrolled, however,
@@ -3340,17 +3346,12 @@ While it is sometimes useful to unroll only the first iterations, the usual
objective is full unrolling; for this reason, the user is informed whenever
the specified unrolling value is insufficient to unroll the loop entirely:
-\begin{lstlisting}
-void main() {
- //@ loop unroll 20; // should be 21
- for (int i = 0 ; i <= 20 ; i ++) {
- }
-}
-\end{lstlisting}
+\begin{minipage}{\linewidth}% prevents page break in listing
+\lstinputlisting{examples/parametrizing/loop-unroll-insuf.c}
+\end{minipage}
-\begin{lstlisting}
-[eva:loop-unroll] insuf-loop.c:3: loop not completely unrolled
-\end{lstlisting}
+\lstinputlisting[linerange={7-7}]
+ {examples/parametrizing/loop-unroll-insuf.log}
The message can be deactived via \lstinline|-eva-warn-key loop-unroll=inactive|.
--
GitLab