[Eva] update documentation about trace partitioning

doc/value/biblio.bib

@@ -115,3 +115,22 @@
   biburl    = {https://dblp.org/rec/bib/conf/sas/2018},
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
+
+
+@article{trace-partitioning,
+ author = {Rival, Xavier and Mauborgne, Laurent},
+ title = {The Trace Partitioning Abstract Domain},
+ journal = {ACM Trans. Program. Lang. Syst.},
+ issue_date = {August 2007},
+ volume = {29},
+ number = {5},
+ month = aug,
+ year = {2007},
+ issn = {0164-0925},
+ articleno = {26},
+ url = {http://doi.acm.org/10.1145/1275497.1275501},
+ doi = {10.1145/1275497.1275501},
+ acmid = {1275501},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+} 
\ No newline at end of file

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

 #define NROWS 10
-void main(void) {
+void main(void)
+{
   int a[NROWS][20] = {0};
   //@ loop unroll NROWS;
   for (int i = 0; i < 10; i++) {

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

@@ -4,8 +4,8 @@
 [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] loop-unroll-const.c:8: Trace partitioning superposing up to 100 states
+[eva] loop-unroll-const.c:8: Trace partitioning superposing up to 200 states
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:

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

-void main() {
+void main()
+{
   //@ loop unroll 20; // should be 21
   for (int i = 0 ; i <= 20 ; i ++) {
   }

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

@@ -4,8 +4,8 @@
 [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:loop-unroll] loop-unroll-insuf.c:4: loop not completely unrolled
+[eva] loop-unroll-insuf.c:4: starting to merge loop iterations
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:

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) {
+void main(void)
+{
   int S = 0;
-  // loop unroll 3;
+  //@ loop unroll 3;
   for (int i = 0 ; i < 3 ; i++) {
-    // loop unroll sizes[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

@@ -18,16 +18,10 @@
   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]
+  S ∈ {45}
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
   1 function analyzed (out of 1): 100% coverage.
@@ -35,9 +29,7 @@
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
   ----------------------------------------------------------------------------
-  2 alarms generated by the analysis:
-       1 invalid memory access
-       1 integer overflow
+  0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
   No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------

doc/value/examples/parametrizing/makefile

@@ -17,7 +17,9 @@ TARGETS = \
   ilevel.2.log \
 	loop-unroll-const.log \
 	loop-unroll-nested.log \
-	loop-unroll-insuf.log
+	loop-unroll-insuf.log \
+	split-array.log \
+	split-fabs.log
 
 .SECONDEXPANSION:
 .PHONY: all clean
@@ -38,6 +40,7 @@ context-depth.3.log: FCFLAGS += -context-width 1 -context-depth 1 -context-valid
 slevel.1.log: FCFLAGS += -slevel 55
 slevel.2.log: FCFLAGS += -slevel 28
 ilevel.2.log: FCFLAGS += -val-ilevel 16
+split-fabs.log: FCFLAGS += -eva-equality-domain
 
 nor.1.log nor.2.log: nor.c
 	time --format "\nuser time: %Us" $(FRAMAC) $(FCFLAGS) -val $< > $@ 2>&1

doc/value/examples/parametrizing/split-array.c

+int t1[] = {1, 2, 3}, t2[] = {4, 5}, t3[] = {6, 7, 8, 9};
+int *t[] = {t1, t2, t3};
+int sizes[] = {3, 2, 4};
+/*@ requires 0 <= i < 3; */
+int main(int i)
+{
+  int S = 0;
+  //@ split i;
+  //@ loop unroll sizes[i];
+  for (int j = 0 ; j < sizes[i] ; j++)
+    S += t[i][j];
+
+  return S;
+}

doc/value/examples/parametrizing/split-array.log

+[kernel] Parsing split-array.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:alarm] split-array.c:4: Warning: 
+  function main: precondition got status unknown.
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  S ∈ {6; 9; 30}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 9 statements reached (out of 9): 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/split-fabs.c

+double fabs(double x)
+{
+  return x < 0.0 ? -x : x;
+}
+
+double main(double y)
+{
+  //@ split y < 0.0;
+  if (fabs(y) > 1.0)
+    y = y < 0 ? -1.0 : 1.0;
+  //@ merge y < 0.0;
+  return y;
+}

doc/value/examples/parametrizing/split-fabs.log

+[kernel] Parsing split-fabs.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] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function fabs:
+  
+[eva:final-states] Values at end of function main:
+  y ∈ [-1. .. 1.]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 12 statements reached (out of 12): 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/main.tex

@@ -2658,6 +2658,7 @@ Section \ref{command-line} presents the general usage options of \Eva{} in the
 command-line.
 The options described in section \ref{context} are correctness options,
 while the remaining sections (\ref{boucles-traitement},
+\ref{trace-partitioning},
 \ref{controlling-approximations} and \ref{sec:eva}) deal with performance
 tuning options. Section \ref{nonterm} presents a derived analysis to
 obtain information about non-termination.
@@ -3711,6 +3712,118 @@ line~7, by an invariant, that remains to be proven.
 %% less precisely.
 
 
+\section{Improving precision with reasoning by case}
+\label{trace-partitioning}
+
+Some formal proofs about programs require to use \emph{reasoning by cases}. \Eva can
+perform such reasonings through the use of the \emph{Trace Partitioning}
+\cite{trace-partitioning} techniques. These can be enabled manually or
+automatically. It is important to note that, whatever the method used, the
+partitioning and thus the reasoning by case stops at the end of a function
+and can only be extended past the function return if there is enough
+\lstinline|slevel| in the calling function.
+
+
+\subsection{Automatic partitioning on conditional structures}
+
+It sometimes happens that the cases we want to reason on are exactly the
+cases distinguished in the program in an \lstinline|if-then-else| or a
+\lstinline|switch| not far above.  even if these blocks are already closed
+at the point we need the reasoning by cases. Unless enough
+\lstinline|slevel| is available, the cases of a conditional structures are
+approximated together as soon as the analyzer leaves the block. \Eva can delay
+this approximation until after the statement where the reasoning
+by cases is needed.
+
+The global command-line parameter \lstinline|-eva-partition-history <n>|
+will delay the approximation for all conditional structures of the whole
+program. It takes a parameter \lstinline|<n>| which allow to control the delay.
+It represents the number of junction points for which we keep the incoming
+path (the cases) separated. A value of $1$ means that \Eva will reason by
+case on the previous \lstinline|if-then-else| until another
+\lstinline|if-then-else| is closed.
+
+This option has a very high cost on the analysis, theoretically increasing the
+analysis time by 2 for $n = 1$, and doubling each time $n$ is increased by $1$.
+The cost can even be higher if there are \lstinline|switch| instructions in the
+program. However, it can remove false alarms in a fully automatic way. Thus,
+the trade off might often be worth trying.
+
+Choosing a value for \lstinline|<n>| strictly greater than 1 is often not
+needed.
+
+
+\subsection{Manual partitioning on values}
+
+The reasoning by case can be forced inside a function by using \lstinline|split|
+annotations. These annotations must be given an expression which values
+correspond to the cases being enumerated. The example below show a usage
+of this annotation.
+
+\lstinputlisting{examples/parametrizing/split-array.c}
+
+The \lstinline|split| requires that the analyzer enumerate all the 3 possible
+values for \lstinline|i| and conduct a specialized analysis of the function for
+each of these values. Thereafter, the value of \lstinline|i| is always
+evalutated by \Eva{} as a singleton and it enables the use of a
+\lstinline|loop unroll| annotation on \lstinline|i|. This way, the result of
+the function can be exactly computed as the set of three possible value instead
+of an imprecise interval.
+
+\lstinputlisting[linerange={25-26}]
+  {examples/parametrizing/split-array.log}
+
+The \lstinline|split| can be any expression that evaluate to a {\it small}
+number of integer values. In particular, it can be C comparisons like in
+the following example.
+
+\lstinputlisting{examples/parametrizing/split-fabs.c}
+
+To be analyzed properly, the equality domain must be activated with the option
+\lstinline|-eva-equality-domain| (see section \ref{sec:symbolic-equalities})
+as we need the equality relations between the input and the output of the
+function \lstinline|fabs|, i.e. the relations \lstinline|x == \result| or
+\lstinline|x == -\result|. Then, the \lstinline|split| annotation placed before
+the call to \lstinline|fabs| allows us to reason by case and infer the relevant
+equality in each case.
+
+Note in the previous example the use of \lstinline|merge| annotation. These
+annotations ends the reasoning by cases and must use the exact same expression
+as a previous \lstinline|split|. In this example, the \lstinline|merge|
+annotation is not needed as the partitioning will be ended at the end of the
+function anyway. The use of \lstinline|merge| annotations is not mandatory,
+and are these annotations exists only to allow the user to mitigate the cost of
+the reasoning by cases.
+
+Alternatively to annotations, it is possible to use the command-line to
+reason by case during the whole analysis. The command line parameter
+\lstinline|-eva-partition-value <V>| forces the analyzer to reason at all times
+on single values of the global variable \lstinline|<V>|.
+
+There are three limitations to partitioning on values.
+
+\begin{enumerate}
+\item While the number of simultaneous splits (whether local with annotations
+  or global through command line) is not bounded, there can be only one split
+  per expression. If two \lstinline|split| annotation uses the same expression,
+  only the latest one encountered on the path will be kept. Although it is a
+  limitation, it can be used to define strategies where a reasoning by case is
+  controlled accross the whole program.
+\item The expression on which the split is done must evaluate to a bounded set
+  of values. Otherwise, the analysis would not be guaranteed to terminate. The
+  analysis must be precise enough in order to prove the boundedness. When \Eva{}
+  fails to prove that the number of possible values is lower than a defined limit,
+  either because the set is unbounded or because it failed to prove it,
+  it will raise a warning and cancel the split. The limit is arbitrary and
+  can be set with the option \lstinline|-eva-split-limit <n>|.
+\item When the expression is complex, the ability of \Eva{} to reason
+  precisely by cases depends on the activated abstract domains (see section
+  \ref{sec:eva}) and their capability to learn from the expression. \Eva{} will
+  try to detect this and will cancel the split and warn the user when it is
+  not useful.
+\end{enumerate}
+
+
 \section{Controlling approximations}
 \label{controlling-approximations}