Merge branch 'fix/eva/recursion-manual' into 'stable/vanadium'

[Eva] User manual: documents the analysis of recursive calls

See merge request frama-c/frama-c!3193

doc/value/examples/parametrizing/makefile

@@ -17,7 +17,9 @@ TARGETS = \
 	loop-unroll-nested.log \
 	loop-unroll-insuf.log \
 	split-array.log \
-	split-fabs.log
+	split-fabs.log \
+	recursion-simple.log \
+	recursion-imprecise.log
 
 .SECONDEXPANSION:
 .PHONY: all clean
@@ -39,3 +41,5 @@ slevel.1.log: FCFLAGS += -eva-slevel 55
 slevel.2.log: FCFLAGS += -eva-slevel 28
 ilevel.2.log: FCFLAGS += -eva-ilevel 16
 split-fabs.log: FCFLAGS += -eva-domains equality
+recursion-simple.log: FCFLAGS += -eva-unroll-recursive-calls 10
+recursion-imprecise.log: FCFLAGS += -eva-unroll-recursive-calls 4

doc/value/examples/parametrizing/recursion-imprecise.c

+/*@ assigns \result \from x; */
+int mod3 (int x) {
+  Frama_C_show_each(x);
+  if ((x / 3) * 3 == x) return 0;
+  else return 1 + mod3(x-1);
+}
+
+void main (int x) {
+  int r = mod3(x);
+}

doc/value/examples/parametrizing/recursion-imprecise.log

+[kernel] Parsing recursion-imprecise.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] recursion-imprecise.c:3: Frama_C_show_each: [-2147483648..2147483647]
+[eva:recursion] recursion-imprecise.c:5: 
+  detected recursive call of function mod3.
+[eva:alarm] recursion-imprecise.c:5: Warning: 
+  signed overflow. assert -2147483648 ≤ x - 1;
+[eva] recursion-imprecise.c:3: Frama_C_show_each: [-2147483648..2147483646]
+[eva] recursion-imprecise.c:3: Frama_C_show_each: [-2147483648..2147483644]
+[eva] recursion-imprecise.c:3: Frama_C_show_each: [-2147483648..2147483643]
+[eva] recursion-imprecise.c:5: Warning: 
+  Using specification of function mod3 for recursive calls of depth 4.
+  Analysis of function mod3 is thus incomplete and its soundness
+  relies on the written specification.
+[eva] using specification for function mod3
+[eva:alarm] recursion-imprecise.c:5: Warning: 
+  signed overflow. assert 1 + tmp ≤ 2147483647;
+                   (tmp from mod3(x - 1))
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function mod3:
+  __retres ∈ [-2147483647..2147483647]
+[eva:final-states] Values at end of function main:
+  r ∈ [-2147483644..2147483647]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    1 warning
+    by the Frama-C kernel:    0 errors    0 warnings
+  ----------------------------------------------------------------------------
+  2 alarms generated by the analysis:
+       2 integer overflows
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------

doc/value/examples/parametrizing/recursion-simple.c

+/*@ assigns \result \from i; */
+int factorial (int i) {
+  if(i <= 1) return 1;
+  return i * factorial (i - 1);
+}
+
+void main(void) {
+  int x = factorial(8);
+  int y = factorial(20);
+}

doc/value/examples/parametrizing/recursion-simple.log

+[kernel] Parsing recursion-simple.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:recursion] recursion-simple.c:4: 
+  detected recursive call of function factorial.
+[eva] recursion-simple.c:4: Warning: 
+  Using specification of function factorial for recursive calls of depth 10.
+  Analysis of function factorial is thus incomplete and its soundness
+  relies on the written specification.
+[eva] using specification for function factorial
+[eva:alarm] recursion-simple.c:4: Warning: 
+  signed overflow. assert -2147483648 ≤ i * tmp;
+                   (tmp from factorial(i - 1))
+[eva:alarm] recursion-simple.c:4: Warning: 
+  signed overflow. assert i * tmp ≤ 2147483647;
+                   (tmp from factorial(i - 1))
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function factorial:
+  __retres ∈ [-2147483646..2147483646]
+[eva:final-states] Values at end of function main:
+  x ∈ {40320}
+  y ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    1 warning
+    by the Frama-C kernel:    0 errors    0 warnings
+  ----------------------------------------------------------------------------
+  2 alarms generated by the analysis:
+       2 integer overflows
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------

doc/value/main.tex

@@ -1361,12 +1361,24 @@ the 32-bit word read is made of the last two bytes from \lstinline|t[0]|
 and the first two bytes from \lstinline|t[1]|.
 
 \subsubsection{Call to an unknown function}
-The origin \lstinline$Library function L$ is used for the result of
-recursive functions or calls to function pointers whose value is not known
-precisely.
+The origin \lstinline$Library function L$ arises from the interpretation
+of a function specification, when an \lstinline|assigns| clause applies to
+pointer values.
+A function specification is only used for:
+\begin{itemize}
+\item
+  functions whose body is not provided, and for which no Eva builtins
+  exist. See section~\ref{builtins-list} for a list of available builtins.
+\item
+  recursive functions that cannot be completely analyzed;
+  see section~\ref{recursion} for more details.
+\item
+  functions given to the \verb+-eva-use-spec+ option;
+  see section~\ref{val-use-spec} for more details.
+\end{itemize}
 
 \subsubsection{Fusion of values with different alignments}
-The notation \lstinline$Merge L$ that memory states  with incompatible
+The notation \lstinline$Merge L$ indicates that memory states with incompatible
 alignments are fused together. In the example below,
 the memory states from
 the then branch and from the else branch contain in the array
@@ -2301,8 +2313,10 @@ prototypes (e.g. \lstinline|stdio.h| for \lstinline|printf|) are included.
 Calls to variadic functions in the C standard library also include
 ACSL specifications, which \Eva{} uses to interpret their behavior.
 
-Recursive functions are allowed in Frama-C, but they
-are not handled in the current version of the \Eva{} plug-in.
+Recursive functions are partially supported by \Eva{}: only a bounded
+number of recursive calls can be analyzed, and a user-written specification
+is required to interpret other calls.
+See section \ref{recursion} for more details.
 
 \section{Analyzing a partial or a complete application}
 
@@ -3330,6 +3344,80 @@ informed assumptions. However, no guarantee is made that those assumptions
 over-approximate the real behavior of the function. The inferred
 contract should be verified carefully by the user.
 
+\subsection{Analyzing recursive functions}
+\label{recursion}
+
+By default, recursive calls are not analyzed; instead, \Eva{} uses the
+specification written by the user for the recursive function to interpret
+its recursive calls. The analysis of the function is then incomplete,
+as only its non-recursive calls are analyzed: values are inferred and
+alarms are emitted only for these calls.
+For the recursive calls, the analysis' soundness relies entirely on the
+specification provided by the user, which is not verified, and a warning
+is emitted.
+
+\begin{logs}
+[eva] file.c: Warning:
+  Using specification of function <name> for recursive calls.
+  Analysis of function <name> is thus incomplete and its soundness
+  relies on the written specification.
+\end{logs}
+
+If no ACSL contract is provided for the recursive function,
+a minimal specification is inferred by the \FramaC kernel
+from the function type, and an error is emitted.
+The specification is only generated to allow the analysis to continue
+past the recursive call, without any guarantees that it describes correctly
+the real behaviors of the function.
+In particular, only \lstinline|assigns| clauses are created, without any
+preconditions.
+It is the user's responsibility to replace this generated specification by
+a correct one.
+
+\subsubsection{Unrolling recursive calls}
+
+Option \lstinline|-eva-unroll-recursive-calls n| allows the precise analysis
+of recursive calls up to a depth of <n>. The function specification is only used
+when encountering a recursive call of depth greater than <n>.
+
+On the example below, analyzed with \lstinline|-eva-unroll-recursive-calls 10|:
+\begin{itemize}
+\item
+  the first call \lstinline|factorial(8)| is soundly and precisely analyzed
+  without any warnings;
+\item
+  the analysis of the second call \lstinline|factorial(20)| is incomplete and
+  produces a warning, as it resorts to the function specification for the tenth
+  recursive call.
+\end{itemize}
+
+\lstinputlisting{examples/parametrizing/recursion-simple.c}
+
+With option \lstinline|-eva-unroll-recursive-calls|,
+the analysis of a recursive function can thus be complete and sound,
+when the number of recursive calls can be bounded by the analysis.
+In that case, no ACSL specification is required for the analysis of the
+recursive function.
+
+However, even when the number of recursive calls is bounded in practice,
+the \Eva{} analysis might be too imprecise to be complete.
+
+\lstinputlisting{examples/parametrizing/recursion-imprecise.c}
+
+The above example presents a recursive function \lstinline|mod3|, which
+computes the congruence modulo 3 in up to three recursive calls.
+However, Eva is unable to perform a complete analysis of this function
+in the general case and will instead rely on the \lstinline|mod3| specification,
+as it cannot reduce the new argument value of the recursive calls, as shown
+by the successive values printed by the \lstinline|Frama_C_show_each| directive:
+
+\lstinputlisting[linerange={12-19}]
+                {examples/parametrizing/recursion-imprecise.log}
+
+Finally, note that the unrolling of a very large number of recursive calls can
+considerably slow down the analysis.
+
+
 \subsection{Using the specification of a function instead of its body}
 \label{val-use-spec}