[Eva] Update section Loop Unrolling

doc/value/examples/parametrizing/loop-unroll-const.c

+#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;
+    }
+  }
+}

doc/value/examples/parametrizing/loop-unroll-const.log

+[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.
+  ----------------------------------------------------------------------------

doc/value/examples/parametrizing/loop-unroll-insuf.c

+void main() {
+  //@ loop unroll 20; // should be 21
+  for (int i = 0 ; i <= 20 ; i ++) {
+  }
+}
\ No newline at end of file

doc/value/examples/parametrizing/loop-unroll-insuf.log

+[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.
+  ----------------------------------------------------------------------------

doc/value/examples/parametrizing/loop-unroll-nested.c

+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];
+    }
+  }
+}

doc/value/examples/parametrizing/loop-unroll-nested.log

+[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.
+  ----------------------------------------------------------------------------

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

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|.