From 49eb96a169b1e5c55aa04cae06c1b34613fa3b16 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 10 May 2021 17:59:58 +0200
Subject: [PATCH] [Eva] User manual: documents the analysis of recursive calls.
---
doc/value/examples/parametrizing/makefile | 6 +-
.../parametrizing/recursion-imprecise.c | 10 +++
.../parametrizing/recursion-imprecise.log | 42 ++++++++++
.../examples/parametrizing/recursion-simple.c | 10 +++
.../parametrizing/recursion-simple.log | 40 ++++++++++
doc/value/main.tex | 80 ++++++++++++++++++-
6 files changed, 185 insertions(+), 3 deletions(-)
create mode 100644 doc/value/examples/parametrizing/recursion-imprecise.c
create mode 100644 doc/value/examples/parametrizing/recursion-imprecise.log
create mode 100644 doc/value/examples/parametrizing/recursion-simple.c
create mode 100644 doc/value/examples/parametrizing/recursion-simple.log
diff --git a/doc/value/examples/parametrizing/makefile b/doc/value/examples/parametrizing/makefile
index 70b98e3bff9..1cb5d4e3551 100644
--- a/doc/value/examples/parametrizing/makefile
+++ b/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
diff --git a/doc/value/examples/parametrizing/recursion-imprecise.c b/doc/value/examples/parametrizing/recursion-imprecise.c
new file mode 100644
index 00000000000..e8ec1cdbc6a
--- /dev/null
+++ b/doc/value/examples/parametrizing/recursion-imprecise.c
@@ -0,0 +1,10 @@
+/*@ 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);
+}
diff --git a/doc/value/examples/parametrizing/recursion-imprecise.log b/doc/value/examples/parametrizing/recursion-imprecise.log
new file mode 100644
index 00000000000..65134c588fb
--- /dev/null
+++ b/doc/value/examples/parametrizing/recursion-imprecise.log
@@ -0,0 +1,42 @@
+[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.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/examples/parametrizing/recursion-simple.c b/doc/value/examples/parametrizing/recursion-simple.c
new file mode 100644
index 00000000000..b41681d4e14
--- /dev/null
+++ b/doc/value/examples/parametrizing/recursion-simple.c
@@ -0,0 +1,10 @@
+/*@ 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);
+}
diff --git a/doc/value/examples/parametrizing/recursion-simple.log b/doc/value/examples/parametrizing/recursion-simple.log
new file mode 100644
index 00000000000..62e18509655
--- /dev/null
+++ b/doc/value/examples/parametrizing/recursion-simple.log
@@ -0,0 +1,40 @@
+[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.
+ ----------------------------------------------------------------------------
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 4123d592d89..f8e92ed33ae 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -2301,8 +2301,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 +3332,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}
--
GitLab