Merge branch 'feature/doc/invalid-pointer' into 'master'

Documentation of the options -warn-invalid-pointer and -warn-pointer-downcast

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

doc/rte/rte.tex

@@ -805,6 +805,9 @@ signed overflows \\
 \lstinline|-warn-signed-downcast| & boolean (false) & Generate annotations for
 signed integer downcast \\
 \hline
+\lstinline|-warn-pointer-downcast| & boolean (true) & Generate annotations for
+downcast of pointer values \\
+\hline
 \lstinline|-warn-left-shift-negative| & boolean (true) & Generate annotations for
 left shift on negative values \\
 \hline
@@ -814,9 +817,12 @@ right shift on negative values \\
 \lstinline|-warn-invalid-bool| & boolean (true) & Generate annotations for
 \lstinline|_Bool| trap representations \\
 \hline
-\lstinline|-warn-special-float| &  string: \lstinline|non-finite|, (\lstinline|nan|) or \lstinline|none|  & generate annotations when
+\lstinline|-warn-special-float| &  string: (\lstinline|non-finite|), \lstinline|nan| or \lstinline|none|  & generate annotations when
 special floats are produced: infinite floats or NaN (by default), only on NaN or never. \\
 \hline
+\lstinline|-warn-invalid-pointer| & boolean (false) & Generate annotations for
+invalid pointer arithmetic \\
+\hline
 \end{tabular}
 \caption{\framac kernel options, impacting \rte{}} \label{kernel}
 \end{center}

doc/userman/user-analysis.tex

@@ -152,6 +152,23 @@ With \texttt{-safe-arrays}, the two accesses to \lstinline|v| are considered
 invalid. (Accessing \lstinline|v.b[-2]| or \lstinline|v.b[3]| remains incorrect,
 regardless of the value of the option.)
 
+\item \optiondef{-}{warn-invalid-pointer} may be used to check that the code
+  does not perform illegal pointer arithmetics, creating pointers that do not
+  point inside an object or one past an object.
+  This option is disabled by default, allowing the creation of such invalid
+  pointers without alarm — but the dereferencing of an invalid pointer
+  \emph{always} generates an alarm.
+
+  For instance, no error is detected by default in the following example, as
+  the dereferencing is correct. However, if option
+  \texttt{-warn-invalid-pointer} is enabled, an error is detected at line 4.
+  \begin{ccode}
+    int x;
+    int *p = &x;
+    p++;  // valid
+    p++;  // undefined behavior
+    *(p-2) = 1;
+  \end{ccode}
 
 \item \optiondef{-}{unspecified-access} may be used to check when the
   evaluation of an expression depends on the order in which its sub-expressions
@@ -179,6 +196,16 @@ Here, the \texttt{x} might be incremented by \texttt{g} before or after the
 call to \texttt{f}, but since the two write accesses occur in different
 functions, \texttt{-unspecified-access} does not detect that.
 
+\item \optiondef{-}{warn-pointer-downcast} may be used to check that the code
+  does not downcast a pointer to an integer type. This option is set by default.
+  In the following example, analyzers report by default an error on the third
+  line. Disabling the option removes this verification.
+  \begin{ccode}
+    int x;
+    uintptr_t addr = &x;
+    int a = &x;
+  \end{ccode}
+
 \item \optiondef{-}{warn-signed-downcast} may be used to check that the analyzed
   code does not downcast an integer to a signed integer type. This option is
   \emph{not} set by default. Without it, the analyzers do not perform such a

doc/userman/user-changes.tex

@@ -8,6 +8,8 @@ release. First we list changes of the last release.
 \begin{itemize}
 \item \textbf{Preparing the Sources:} added option
   \texttt{-cpp-extra-args-per-file}.
+\item \textbf{Customizing Analyzers:} added options
+  \texttt{-warn-invalid-pointer} and \texttt{-warn-pointer-downcast}
 \end{itemize}
 
 \section*{20.0 (Calcium)}

doc/value/examples/alarms/pointer_arith.c

+void main () {
+  int x, *p = &x;
+  p++;
+  p++;
+}

doc/value/examples/alarms/pointer_conversion.c

+#include <stdint.h>
+void main () {
+  char c;
+  uintptr_t a = &c;
+  char *p = (char *) (a + 1);
+  char *q = (char *) (a + 2);
+}

doc/value/main.tex

@@ -31,6 +31,7 @@
 
 \newcommand{\framacversion}%
            {\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
+\newcommand{\isoc}{\textsf{C99}}
 
 \newcommand{\Eva}{\textsf{Eva}}
 
@@ -630,7 +631,7 @@ no run-time error could happen when running the program.
 The alarm means that \Eva{} could not prove that the value \verb|ks[i]|
 accessed in \verb|skein_block.c:69| was definitely initialized before being
 read. Reading an initialized value is an undefined behavior according to the
-ISO C99 standard (and can even lead to security vulnerabilities).
+\isoc{} standard (and can even lead to security vulnerabilities).
 
 As is often the case, this alarm is related to the approximation introduced
 in \verb|skein_block.c:56|, which is the loop responsible for initializing
@@ -1460,6 +1461,58 @@ to the attitude described in \ref{norme_pratique}. An option
 to warn about these lines could happen if there was demand for
 this feature.
 
+\subsubsection{Invalid pointer arithmetic}
+
+By default, \Eva{} does \emph{not} emit alarms on invalid pointer arithmetic:
+alarms are only emitted when an invalid pointer is dereferenced or wrongly used
+in a comparison, not at the creation of such pointers.
+
+However, if the \lstinline|-warn-invalid-pointer| option is enabled,
+\Eva{} emits an alarm when an operation may create a pointer that does
+not point inside an object or one past an object,
+even if this pointer is not used afterward.
+
+This may happen on:
+\begin{itemize}
+\item addition (or subtraction) of an integer from a pointer, when the analysis
+  is unable to prove that the resulting pointer points inside, or one past,
+  the same object pointed to by the initial pointer.
+  In this case, the emitted alarm reports a possible undefined behavior.
+\item conversion of an integer into a pointer. Except for the constant~0,
+  such a conversion is always an implementation-defined behavior
+  according to the \isoc{} standard. However, a footnote also explains that
+  conversion between pointers and integers is ``\emph{intended to
+  be consistent with the addressing structure of the execution environment}''.
+  This is why Eva also also authorizes conversion of integers:
+  \begin{itemize}
+  \item in the range of valid absolute addresses
+    (according to \texttt{absolute-valid-range})
+  \item computed from the address of an object \lstinline|o| such that the
+    resulting pointer points inside or one past the object \lstinline|o|.
+  \end{itemize}
+  In all other cases, an alarm is emitted, which reports the possible
+  implementation-defined behavior mentioned above.
+\end{itemize}
+
+In the example below, the first increment of the pointer \lstinline|p| is valid,
+although the resulting pointer should not be dereferenced. The second increment
+leads to an invalid alarm when option \lstinline|-warn-invalid-pointer| is on.
+\listinginput{1}{examples/alarms/pointer_arith.c}
+\begin{logs}
+  [eva:alarm] pointer_arith.c:4: Warning:
+    invalid pointer creation. assert \object_pointer(p + 1);
+\end{logs}
+
+In the same way, in the example below, the first conversion at line~5
+does not generate an alarm, but the second conversion leads to an invalid alarm
+with option \lstinline|-warn-invalid-pointer|.
+
+\listinginput{1}{examples/alarms/pointer_conversion.c}
+\begin{logs}
+  [eva:alarm] pointer_arith.c:6: Warning:
+    invalid pointer creation. assert \object_pointer((char *)(a + 2));
+\end{logs}
+
 
 \subsubsection{Division by zero}
 When dividing by an expression that the analysis
@@ -1494,7 +1547,7 @@ simpler than this one. Do not be surprised by them.
 Another arithmetic alarm is the alarm emitted for logical
 shift operations on integers where the second operand may be
 larger than the size in bits of the first operand's type. 
-Such an operation is left undefined by the ISO/IEC 9899:1999 standard, and
+Such an operation is left undefined by the \isoc{} standard, and
 indeed, processors are often built in a way that such an
 operation does not produce the \lstinline|0| or \lstinline|-1|
 result that could have been expected. Here is an example
@@ -1506,7 +1559,7 @@ shift.c:4: ... invalid RHS operand for shift. assert 0 <= c < 32;
 
 \Eva{} also detects shifts on negative integers.
 Left-shifting a negative integer is an undefined behavior according to the
-ISO C99 standard, and leads to an alarm by default.
+\isoc{} standard, and leads to an alarm by default.
 These alarms can be disabled by using the option
 \lstinline|-no-warn-left-shift-negative|.
 Right-shifting a negative integer is an implementation-defined operation,
@@ -1525,7 +1578,7 @@ By default, \Eva{} emits alarms for --- and reduces the
 sets of possible results of --- signed arithmetic computations where
 the possibility of an overflow exists. Indeed,
 such overflows have an undefined behavior according to
-paragraph 6.5.5 of the ISO/IEC 9899:1999 standard.
+paragraph 6.5.5 of the \isoc{} standard.
 %
 If useful, it is also possible to assume that signed integers overflow
 according to a 2's complement representation. The option
@@ -1536,10 +1589,16 @@ as potentially overflowing. This warning can also be disabled by option
 
 By default, no alarm is emitted for arithmetic operations on unsigned integers
 for which an overflow may happen, since such operations have
-defined semantics according to the ISO/IEC 9899:1999 standard.
+defined semantics according to the \isoc{} standard.
 If one wishes to signal and prevent such unsigned overflows,
 option \verb+-warn-unsigned-overflow+ can be used.
 
+By default, Eva emits alarms for downcasts of pointer values to (signed
+or unsigned) integer types. Such downcasts are indeed  undefined behavior
+according to section 6.3.2.3, §6 of the \isoc{} standard.
+However, option \lstinline|-no-warn-pointer-downcast| can be used to disable
+these alarms.
+
 Finally, by default, no alarm is emitted for downcasts to signed or unsigned
 integers. In the signed case, the least significant bits
 of the original value are used, and are interpreted according
@@ -1658,7 +1717,7 @@ of the call.
 
 By default, \Eva{} emits an alarm whenever a trap representation might be read
 from an lvalue of type \texttt{\_Bool}.
-According to the ISO/IEC 9899:1999 standard, the \texttt{\_Bool} type contains
+According to the \isoc{} standard, the \texttt{\_Bool} type contains
 the values 0 and 1, but any other value might be a trap representation, that is,
 an object representation that does not represent a valid value of the type.
 Trap representations can be created through unions or pointer casts.
@@ -1810,7 +1869,7 @@ compiler, if we may ask such a rhetorical
 question, is right? They all are, because the program is undefined.
 When function \lstinline|copy()| is called from \lstinline|main()|,
 the assignment \lstinline|*p = *q;| breaks
-C99's 6.5.16.1:3 rule. This rule states that 
+\isoc{}'s 6.5.16.1:3 rule. This rule states that 
 in an assignment from lvalue to lvalue,
 the left and right lvalues must overlap either exactly or not at all.
 
@@ -2116,7 +2175,7 @@ limited form, but imprecisions may accumulate quickly
 
 \Eva{} does not check all the properties that could be
 expected of it\footnote{There are 245 unspecified or undefined
-  behaviors in Annex J of the ISO C99 standard.}. Support for each of
+  behaviors in Annex J of the \isoc{} standard.}. Support for each of
 these missing features could arrive if the need was expressed. Below
 are some of the existing limitations.
 

man/frama-c.1

@@ -25,7 +25,7 @@
 .\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
 .\" and run `make man/frama-c.1`.
 
-.TH FRAMA-C 1 2020-03-05
+.TH FRAMA-C 1 2020-04-02
 .SH NAME
 .PP
 frama\-c[.byte] \- a static analyzer for C programs
@@ -737,6 +737,12 @@ parser:decimal\-float=once\f[] (and variants) instead.
 .RS
 .RE
 .TP
+.B [\-no]\-warn\-invalid\-pointer
+generate alarms for invalid pointer arithmetic.
+Defaults to no.
+.RS
+.RE
+.TP
 .B [\-no]\-warn\-left\-shift\-negative
 generate alarms for signed left shifts on negative values.
 Defaults to yes.
@@ -749,6 +755,13 @@ Defaults to no.
 .RS
 .RE
 .TP
+.B [\-no]\-warn\-pointer\-downcast
+generates alarms when the downcast of a pointer may exceed the
+destination range.
+Defaults to yes.
+.RS
+.RE
+.TP
 .B [\-no]\-warn\-signed\-downcast
 generates alarms when signed downcasts may exceed the destination range.
 Defaults to no.

man/frama-c.1.header

@@ -25,4 +25,4 @@
 .\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
 .\" and run `make man/frama-c.1`.
 
-.TH FRAMA-C 1 2020-03-05
+.TH FRAMA-C 1 2020-04-02

man/frama-c.1.md

@@ -450,12 +450,19 @@ the case (this is the default).
 **Deprecated**: use **-kernel-warn-key parser:decimal-float=once**
 (and variants) instead.
 
+[-no]-warn-invalid-pointer
+: generate alarms for invalid pointer arithmetic. Defaults to no.
+
 [-no]-warn-left-shift-negative
 : generate alarms for signed left shifts on negative values. Defaults to yes.
 
 [-no]-warn-right-shift-negative
 : generate alarms for signed right shifts on negative values. Defaults to no.
 
+[-no]-warn-pointer-downcast
+: generates alarms when the downcast of a pointer may exceed the destination
+range. Defaults to yes.
+
 [-no]-warn-signed-downcast
 : generates alarms when signed downcasts may exceed the destination range.
 Defaults to no.