From dbd447ab4fcda92ddc7ee13999111e5d68d8d0e5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 23 Oct 2018 18:51:13 +0200
Subject: [PATCH] do not monitor variables with incomplete types (fix bts
#2406)
---
src/plugins/e-acsl/doc/Changelog | 2 +
src/plugins/e-acsl/doc/userman/changes.tex | 4 +-
.../e-acsl/doc/userman/limitations.tex | 13 ++-
src/plugins/e-acsl/mmodel_analysis.ml | 83 ++++++++++++++-----
src/plugins/e-acsl/tests/bts/bts2406.c | 13 +++
.../tests/bts/oracle/bts2406.res.oracle | 5 ++
.../e-acsl/tests/bts/oracle/gen_bts2406.c | 44 ++++++++++
7 files changed, 139 insertions(+), 25 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/bts/bts2406.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index db8c7d4638d..d9bb44c7d8d 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,8 @@
# configure configure
###############################################################################
+-* E-ACSL [2018/10/23] Fix bug #2406 about monitoring of variables
+ with incomplete types.
-* E-ACSL [2018/10/04] Fix bug #2386 about incorrect typing when
performing pointer subtraction.
-* E-ACSL [2018/10/04] Support for \at on purely logic variables.
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index b4969d93baf..5ffb0f549ca 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -6,13 +6,15 @@ release. First we list changes of the last release.
\section*{E-ACSL \eacslversion}
\begin{itemize}
-\item \textbf{Introduction}: Improve a bit and reference related papers.
+\item \textbf{Introduction}: Improve a bit and reference new related papers.
\item \textbf{What the Plug-in Provides}: Highlight that the memory analysis is
not yet robust.
\item \textbf{What the Plug-in Provides}: Highlight the importance of
\textbf{-e-acsl-prepare}.
\item \textbf{Known Limitations}: Replace section ``Limitations of E-ACSL
Monitoring Libraries'' by the new section ``Supported Systems''.
+\item \textbf{Known Limitations}: Add limitation about monitoring of variables
+ with incomplete types.
\end{itemize}
\section*{E-ACSL Chlorine-20180501}
diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex
index 24a3aced3ba..ec0d86ba6c2 100644
--- a/src/plugins/e-acsl/doc/userman/limitations.tex
+++ b/src/plugins/e-acsl/doc/userman/limitations.tex
@@ -143,8 +143,8 @@ instrumented code (linked against this main) could print some warnings from the
\label{sec:limits:no-code}
\index{Function!Undefined}
-The instrumentation in the generated program is partial for a program $p$ if and
-only if $p$ contains a memory-related annotation $a$ and an undefined function
+The instrumentation in the generated program is partial for a program $p$ if $p$
+contains a memory-related annotation $a$ and an undefined function
$f$ such that:
\begin{itemize}
\item either $f$ has an (even indirect) effect on a left-value occurring in $a$;
@@ -155,6 +155,15 @@ A violation of such an annotation $a$ is undetected. There is no workaround yet.
Also, the option \optionuse{-}{e-acsl-check} does not verify the annotations of
undefined functions. There is also no workaround yet.
+\subsection{Incomplete Types}
+\index{Type!Incomplete}
+
+The instrumentation in the generated program is partial for a program $p$ if $p$
+contains a memory-related annotation $a$ and a variable $v$ with an incomplete
+type definition such that $a$ depends on $v$ (even indirectly).
+
+A violation of such an annotation $a$ is undetected. There is no workaround yet.
+
\section{Recursive Functions}
\index{Function!Recursive}
diff --git a/src/plugins/e-acsl/mmodel_analysis.ml b/src/plugins/e-acsl/mmodel_analysis.ml
index 1c3f78ee9e6..e5c3136060f 100644
--- a/src/plugins/e-acsl/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/mmodel_analysis.ml
@@ -25,6 +25,15 @@ open Cil_datatype
module Dataflow = Dataflow2
+let must_never_monitor vi =
+ (* extern ghost variables are usually used (by the Frama-C libc) to
+ represent some internal invisible states in ACSL specifications. They do
+ not correspond to something concrete *)
+ (vi.vghost && vi.vstorage = Extern)
+ ||
+ (* incomplete types cannot be properly monitored. See BTS #2406. *)
+ not (Cil.isCompleteType vi.vtype)
+
(* ********************************************************************** *)
(* Backward dataflow analysis to compute a sound over-approximation of what
left-values must be tracked by the memory model library *)
@@ -225,16 +234,20 @@ module rec Transfer
let extend_to_expr always state lhost e =
let add_vi state vi =
- if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state) then
+ if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state)
+ then begin
match base_addr e with
| None -> state
| Some vi_e ->
- Options.feedback ~level:4 ~dkey
- "monitoring %a from %a."
- Printer.pp_varinfo vi_e
- Printer.pp_lval (lhost, NoOffset);
- Varinfo.Hptset.add vi_e state
- else
+ if must_never_monitor vi then state
+ else begin
+ Options.feedback ~level:4 ~dkey
+ "monitoring %a from %a."
+ Printer.pp_varinfo vi_e
+ Printer.pp_lval (lhost, NoOffset);
+ Varinfo.Hptset.add vi_e state
+ end
+ end else
state
in
match lhost with
@@ -721,44 +734,70 @@ consolidated_must_model_vi vi
false
*)
-let rec must_model_lval bhv ?kf ?stmt = function
- | Var vi, _ -> must_model_vi bhv ?kf ?stmt vi
- | Mem e, _ -> must_model_exp bhv ?kf ?stmt e
+let rec apply_on_vi_base_from_lval f bhv ?kf ?stmt = function
+ | Var vi, _ -> f bhv ?kf ?stmt vi
+ | Mem e, _ -> apply_on_vi_base_from_exp f bhv ?kf ?stmt e
-and must_model_exp bhv ?kf ?stmt e = match e.enode with
+and apply_on_vi_base_from_exp f bhv ?kf ?stmt e = match e.enode with
| Lval lv | AddrOf lv | StartOf lv ->
- must_model_lval bhv ?kf ?stmt lv
+ apply_on_vi_base_from_lval f bhv ?kf ?stmt lv
| BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) ->
- must_model_exp bhv ?kf ?stmt e1
+ apply_on_vi_base_from_exp f bhv ?kf ?stmt e1
| BinOp(MinusPP, e1, e2, _) ->
- must_model_exp bhv ?kf ?stmt e1 || must_model_exp bhv ?kf ?stmt e2
- | Info(e, _) | CastE(_, e) -> must_model_exp bhv ?kf ?stmt e
+ apply_on_vi_base_from_exp f bhv ?kf ?stmt e1
+ || apply_on_vi_base_from_exp f bhv ?kf ?stmt e2
+ | Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f bhv ?kf ?stmt e
| BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt | Lt | Gt | Le
| Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr), _, _, _)
| Const _ -> (* possible in case of static address *) false
| UnOp _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
Options.fatal "[pre_analysis] unexpected expression %a" Exp.pretty e
+let must_model_lval = apply_on_vi_base_from_lval must_model_vi
+let must_model_exp = apply_on_vi_base_from_exp must_model_vi
+
+let must_never_monitor_lval bhv ?kf ?stmt lv =
+ apply_on_vi_base_from_lval
+ (fun _bhv ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
+ bhv
+ ?kf
+ ?stmt
+ lv
+
+let must_never_monitor_exp bhv ?kf ?stmt lv =
+ apply_on_vi_base_from_exp
+ (fun _bhv ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
+ bhv
+ ?kf
+ ?stmt
+ lv
+
(* ************************************************************************** *)
(** {1 Public API} *)
(* ************************************************************************** *)
let must_model_vi ?bhv ?kf ?stmt vi =
- not (vi.vghost && vi.vstorage = Extern)
+ not (must_never_monitor vi)
&&
(Options.Full_mmodel.get ()
|| Error.generic_handle (must_model_vi bhv ?kf ?stmt) false vi)
let must_model_lval ?bhv ?kf ?stmt lv =
- Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_lval bhv ?kf ?stmt) false lv
+ not (must_never_monitor_lval bhv ?kf ?stmt lv)
+ &&
+ (Options.Full_mmodel.get ()
+ || Error.generic_handle (must_model_lval bhv ?kf ?stmt) false lv)
let must_model_exp ?bhv ?kf ?stmt exp =
- Options.Full_mmodel.get ()
- || Error.generic_handle (must_model_exp bhv ?kf ?stmt) false exp
+ not (must_never_monitor_exp bhv ?kf ?stmt exp)
+ &&
+ (Options.Full_mmodel.get ()
+ || Error.generic_handle (must_model_exp bhv ?kf ?stmt) false exp)
-let use_model () = not (Env.is_empty ()) || Options.Full_mmodel.get () ||
- Env.has_heap_allocations ()
+let use_model () =
+ not (Env.is_empty ())
+ || Options.Full_mmodel.get ()
+ || Env.has_heap_allocations ()
(*
Local Variables:
diff --git a/src/plugins/e-acsl/tests/bts/bts2406.c b/src/plugins/e-acsl/tests/bts/bts2406.c
new file mode 100644
index 00000000000..30c52958e42
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts2406.c
@@ -0,0 +1,13 @@
+/* run.config
+ COMMENT: bts #2306, do not monitor incomplete types
+*/
+
+const char tab[]; /* not monitored */
+char t[10]; /* monitored */
+
+int main(void) {
+ char *p = tab; /* monitored */
+ /*@ assert !\valid(p+(0..9)); */
+ /*@ assert \valid(t+(0..9)); */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle
new file mode 100644
index 00000000000..7204dfeb385
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle
@@ -0,0 +1,5 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva] tests/bts/bts2406.c:5: Warning:
+ during initialization of variable 'tab', size of type 'char const []'
+ cannot be computed (Size of array without number of elements.)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
new file mode 100644
index 00000000000..cc8337e0e2e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
@@ -0,0 +1,44 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+char const tab[];
+char t[10];
+void __e_acsl_globals_init(void)
+{
+ __e_acsl_store_block((void *)(t),(size_t)10);
+ __e_acsl_full_init((void *)(& t));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ char *p = (char *)(tab);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_full_init((void *)(& p));
+ /*@ assert ¬\valid(p + (0 .. 9)); */
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(p + 1 * 0),(size_t)9,
+ (void *)p,(void *)(& p));
+ __e_acsl_assert(! __gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"!\\valid(p + (0 .. 9))",10);
+ }
+ /*@ assert \valid(&t[0 .. 9]); */
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& t + 1 * 0),(size_t)9,
+ (void *)(& t),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&t[0 .. 9])",11);
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(t));
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
--
GitLab