From 833c3cb014c4c89808ed059df0b805e2335ca3c9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 30 May 2024 14:20:17 +0200
Subject: [PATCH] [Eva] Updates user manual with the new garbled mix origin
Misaligned writes.
---
doc/eva/examples/merge.c | 2 +-
doc/eva/examples/misa_write.c | 7 ++++++
doc/eva/main.tex | 43 +++++++++++++++++++++++------------
3 files changed, 37 insertions(+), 15 deletions(-)
create mode 100644 doc/eva/examples/misa_write.c
diff --git a/doc/eva/examples/merge.c b/doc/eva/examples/merge.c
index dbc936c0106..838b22d29bf 100644
--- a/doc/eva/examples/merge.c
+++ b/doc/eva/examples/merge.c
@@ -1,5 +1,5 @@
int x,y;
-char t[8];
+char t[10];
int main(int c)
{
diff --git a/doc/eva/examples/misa_write.c b/doc/eva/examples/misa_write.c
new file mode 100644
index 00000000000..42680662405
--- /dev/null
+++ b/doc/eva/examples/misa_write.c
@@ -0,0 +1,7 @@
+int x;
+int *t[2];
+
+int main(int i){
+ int **ptr = (int **) ((unsigned long) t + i);
+ *ptr = &x;
+}
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 76628e4e00d..13521e3d5c2 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -1337,8 +1337,20 @@ some of these approximations.
Most origins are of the form \lstinline|Cause L|, where \lstinline|L|
is an (optional) line or the application indicating where the approximation
took place. Origin causes are one of the following:
+
+\subsubsection{Arithmetic operation}
+The origin \lstinline$Arithmetic L$ denotes arithmetic operations over
+addresses, whose result cannot be precisely represented by the analyzer.
+\csource{examples/ari.c}
+In this example, the return value for \lstinline|f| is:
+
+\begin{logs}
+{{ garbled mix of &{x; y} (origin: Arithmetic {ari.c:4}) }}
+\end{logs}
+
\subsubsection{Misaligned read}
-The origin \lstinline$Misaligned L$ indicates that
+
+The origin \lstinline$Misaligned read L$ indicates that
misaligned reads prevented the computation to be precise.
A misaligned read is a memory read-access where the bits read were not
previously written as a single write that modified the whole set of
@@ -1347,7 +1359,7 @@ bits exactly.
An example of a program leading to a misaligned read is the following:
\csource{examples/misa.c}
The value returned by the function \lstinline|main| is\\
-\lstinline|{{ garbled mix of &{ x; y } (origin: Misaligned { misa.c:6 }) }}|.\\
+\lstinline|{{ garbled mix of &{x; y} (origin: Misaligned read {misa.c:6}) }}|.\\
The analyzer is by default configured for a 64-bit architecture,
and that consequently the read memory access is not an out-of-bound access.
If it was, an alarm would be emitted, and the
@@ -1359,6 +1371,21 @@ but due to the offset of six bytes,
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{Misaligned writes}
+
+The origin \lstinline$Misaligned write L$ indicates that the interpretation of
+a misaligned write to an imprecise location has created a garbled mix at this
+memory location.
+
+An example of a program where a misaligned write creates a garbled mix
+is the following:
+\csource{examples/misa_write.c}
+
+The interpretation of the last assignment by the analysis writes
+the imprecise value
+\lstinline|{{ garbled mix of &{x} (origin: Misaligned write {misa.c:6}) }}|
+into the array \lstinline|t|.
+
\subsubsection{Call to an unknown function}
The origin \lstinline$Library function L$ arises from the interpretation
of a function specification, when an \lstinline|assigns| clause applies to
@@ -1402,18 +1429,6 @@ called well values.
Computations that are imprecise because of a well value are marked
as \lstinline|origin: Well|.
-\subsubsection{Arithmetic operation}
-The origin \lstinline$Arithmetic L$
-indicates that arithmetic operations
-take place without the analyzer being able to represent the result
-precisely.
-\csource{examples/ari.c}
-In this example, the return value for \lstinline|f| is:
-
-\begin{logs}
-{{ garbled mix of &{ x; y } (origin: Arithmetic { ari.c:4 }) }}
-\end{logs}
-
\section{What is checked by \Eva{}}\label{obligations}
\Eva{} warns about possible run-time errors in the analyzed
--
GitLab