Merge branch 'feature/julien/new_project_initialization' into 'master'

[E-ACSL] new way of initializing the AST before the E-ACSL translation

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

src/kernel_services/ast_data/globals.ml

@@ -359,6 +359,27 @@ module Functions = struct
     else
       res
 
+  let mem_name fct_name =
+    try
+      ignore (find_by_name fct_name);
+      true
+    with Not_found ->
+      false
+
+  let mem_def_name fct_name =
+    try
+      ignore (find_def_by_name fct_name);
+      true
+    with Not_found ->
+      false
+
+  let mem_decl_name fct_name =
+    try
+      ignore (find_decl_by_name fct_name);
+      true
+    with Not_found ->
+      false
+
   let () =
     Parameter_builder.find_kf_by_name := find_by_name;
     Parameter_builder.find_kf_def_by_name := find_def_by_name;
@@ -741,10 +762,18 @@ module Types = struct
       TypeNameToGlobal.mark_as_computed ()
     end
 
+  let mem_enum_tag x =
+    resolve_types ();
+    Enums.mem x
+
   let find_enum_tag x =
     resolve_types ();
     Enums.find x
 
+  let mem_type namespace s =
+    resolve_types ();
+    Types.mem (s, namespace)
+
   let find_type namespace s =
     resolve_types ();
     Types.find (s, namespace)

src/kernel_services/ast_data/globals.mli

@@ -103,6 +103,20 @@ module Functions: sig
   val get_params: kernel_function -> varinfo list
   val get_vi: kernel_function -> varinfo
 
+  (** {2 Membership} *)
+
+  val mem_name: string -> bool
+  (** @return [true] iff there is a function with such a name
+      @since Frama-C+dev *)
+
+  val mem_def_name: string -> bool
+  (** @return [true] iff there is a function definition with such a name
+      @since Frama-C+dev *)
+
+  val mem_decl_name: string -> bool
+  (** @return [true] iff there is a function declaration with such a name
+      @since Frama-C+dev *)
+
   (** {2 Searching} *)
 
   val find_by_name : string -> kernel_function
@@ -219,10 +233,20 @@ module Types : sig
   (** The two functions below are suitable for use in functor
       {!Logic_typing.Make} *)
 
+  val mem_enum_tag: string -> bool
+  (** @return [true] iff there is an enum constant with the given name in the
+      AST.
+      @since Frama-C+dev *)
+
   val find_enum_tag: string -> exp * typ
   (** Find an enum constant from its name in the AST.
       @raise Not_found when no such constant exists. *)
 
+  val mem_type: Logic_typing.type_namespace -> string -> bool
+  (** @return [true] iff there is a type with the given name in the given
+      namespace in the AST.
+      @since Frama-C+dev *)
+
   val find_type: Logic_typing.type_namespace -> string -> typ
   (** Find a type from its name in the AST.
       @raise Not_found when no such type  exists. *)

src/kernel_services/ast_data/property_status.ml

@@ -168,6 +168,7 @@ module Status =
     end)
 
 let self = Status.self
+let () = Ast.add_monotonic_state self
 
 let iter_on_statuses f ip =
   try
@@ -231,6 +232,7 @@ end = struct
       end)
 
   let self = S.self
+  let () = Ast.add_monotonic_state self
 
   let _mem e path =
     try

src/kernel_services/plugin_entry_points/db.ml

@@ -526,8 +526,20 @@ module Value = struct
 
   let add_formals_to_state = mk_fun "add_formals_to_state"
 
+  let get_fundec_from_stmt stmt =
+    let kf =
+      try
+        Kernel_function.find_englobing_kf stmt
+      with Not_found ->
+        Kernel.fatal "Unknown statement '%a'" Printer.pp_stmt stmt
+    in
+    try
+      Kernel_function.get_definition kf
+    with Kernel_function.No_Definition ->
+      Kernel.fatal "No definition for function %a" Kernel_function.pretty kf
+
   let noassert_get_stmt_state ~after s =
-    if !no_results (Kernel_function.(get_definition (find_englobing_kf s)))
+    if !no_results (get_fundec_from_stmt s)
     then Cvalue.Model.top
     else
       let (find, add), find_by_callstack =
@@ -586,7 +598,7 @@ module Value = struct
 
   exception Is_reachable
   let is_reachable_stmt stmt =
-    if !no_results (Kernel_function.(get_definition (find_englobing_kf stmt)))
+    if !no_results (get_fundec_from_stmt stmt)
     then true
     else
       let ho = try Some (Table_By_Callstack.find stmt) with Not_found -> None in

src/plugins/e-acsl/Makefile.in

@@ -44,6 +44,13 @@ SRC_LIBRARIES:= \
 	varname
 SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES))
 
+# project initializer
+SRC_PROJECT_INITIALIZER:= \
+	rtl \
+	prepare_ast
+SRC_PROJECT_INITIALIZER:=\
+  $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
+
 # analyses
 SRC_ANALYSES:= \
 	rte \
@@ -55,13 +62,6 @@ SRC_ANALYSES:= \
 	typing
 SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
 
-# project initializer
-SRC_PROJECT_INITIALIZER:= \
-	keep_status \
-	prepare_ast
-SRC_PROJECT_INITIALIZER:=\
-  $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
-
 # code generator
 SRC_CODE_GENERATOR:= \
 	constructor \
@@ -100,8 +100,8 @@ PLUGIN_NAME:=E_ACSL
 PLUGIN_CMO:= src/local_config \
 	src/options \
 	$(SRC_LIBRARIES) \
-	$(SRC_ANALYSES) \
 	$(SRC_PROJECT_INITIALIZER) \
+	$(SRC_ANALYSES) \
 	$(SRC_CODE_GENERATOR) \
 	src/main
 

src/plugins/e-acsl/doc/Changelog

@@ -25,6 +25,11 @@
 Plugin E-ACSL <next-release>
 ############################
 
+-* E-ACSL       [2020-08-28] Fix crash that may occur when translating
+	        properties that have been proved valid by another plug-in
+	        (frama-c/e-acsl#106).
+-! E-ACSL       [2020-08-28] Remove option -e-acsl-prepare-ast.
+-! E-ACSL       [2020-08-28] Remove option -e-acsl-check.
 -  E-ACSL       [2020-08-07] Add support for logical array comparison
                 (frama-c/e-acsl#99).
 -  E-ACSL       [2020-07-28] Add support of bitwise operators

src/plugins/e-acsl/doc/userman/biblio.bib

@@ -59,6 +59,25 @@
   url = {publis/hdr.pdf}
 }
 
+@inproceedings{kosmatov20rv,
+  author = {Kosmatov, Nikolai and Maurica, Fonenantsoa and Signoles, Julien},
+  title = {{Efficient Runtime Assertion Checking for Properties over
+             Mathematical Numbers}},
+  booktitle = {International Conference on Runtime Verification (RV)},
+  year = 2020,
+  month = oct,
+}
+
+@inproceedings{ly18hilt,
+  author = {Dara Ly and Nikolai Kosmatov and Fr\'ed\'eric Loulergue
+            and Julien Signoles},
+  title = {Soundness of a Dataflow Analysis for Memory Monitoring},
+  booktitle = {Workshop on Languages and Tools for Ensuring Cyber-Resilience in
+Critical Software-Intensive Systems (HILT)},
+  year = 2018,
+  month = nov,
+}
+
 @inproceedings{rvcubes17tool,
   author = {Julien Signoles and Nikolai Kosmatov and Kostyantyn Vorobyov},
   title = {{E-ACSL, a Runtime Verification Tool for Safety and Security of C

src/plugins/e-acsl/doc/userman/changes.tex

@@ -5,6 +5,14 @@ release. First we list changes of the last release.
 
 \section*{E-ACSL \eacslpluginversion}
 
+\begin{itemize}
+\item \textbf{Simple Example}: Remove option \texttt{-e-acsl-check}
+\item \textbf{Combining E-ACSL with Other PLug-ins}: \texttt{-e-acsl-prepare} is
+  no more necessary.
+\end{itemize}
+
+\section*{E-ACSL 19.0 Potassium}
+
 \begin{itemize}
 \item \textbf{Runtime Monitor Behavior}: Document global variable
   \texttt{\_\_e\_acsl\_sound\_verdict} usable in \texttt{\_\_e\_acsl\_assert}.

src/plugins/e-acsl/doc/userman/limitations.tex

@@ -152,9 +152,6 @@ $f$ such that:
 \end{itemize}
 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}
 

src/plugins/e-acsl/doc/userman/main.tex

@@ -50,8 +50,9 @@ evolve in the future.
 \section*{Acknowledgements}
 
 We gratefully thank the people who contributed to this document:
-Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner, Nikola\"i Kosmatov,
-Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and Guillaume Petiot.
+Basile Desloges, Pierre-Lo\"ic Garoche, Jens Gerlach, Florent Kirchner,
+Nikola\"i Kosmatov, Andr\'e Oliveira Maroneze, Fonenantsoa Maurica, and
+Guillaume Petiot.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 

src/plugins/e-acsl/doc/userman/provides.tex

@@ -416,7 +416,7 @@ script.
 mathematical integers which does not fit in any integral \C type. To circumvent
 this issue, \eacsl uses the \gmp library\footnote{\url{http://gmplib.org}}.
 Thus, even if \eacsl does its best to use standard integral types instead of
-\gmp~\cite{sac13,jfla15}, it may generate such integers from time to time. It is
+\gmp~\cite{kosmatov20rv}, it may generate such integers from time to time. It is
 notably the case if your program contains \lstinline|long long|, either signed
 or unsigned.
 
@@ -544,8 +544,8 @@ model~\cite{pldi16}.
 \subsubsection{Maximized Memory Tracking}
 
 By default \eacsl uses static analysis to reduce instrumentation and therefore
-runtime and memory overheads~\cite{scp16}. With respect to memory tracking this
-means that
+runtime and memory overheads~\cite{ly18hilt}. With respect to memory tracking
+this means that
 \eacsl may omit recording memory blocks irrelevant for runtime analysis.  It
 is, however, still possible to systematically instrument the code for handling
 potential memory-related annotations even when it is not required.  This
@@ -980,22 +980,6 @@ The present implementation of \eacslgcc does not fully support combining \eacsl
 with other \framac plug-ins. However it is still possible to instrument programs
 with \eacsl directly and use \eacslgcc to compile the generated code.
 
-If you run the \eacsl plug-in after another one, it first generates
-a new temporary project in which it links the analyzed program against its own
-library in order to generate the \framac internal representation of the \C
-program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
-even if the \eacsl plug-in keeps the maximum amount of information, the results
-of already executed analyzers (such as validity status of annotations) are not
-known in this new project.
-
-\begin{important}
-If you want to keep results of former analysis, you have to set the option
-\shortopt{e-acsl-prepare} when the first analysis is asked for. The standard
-example is running \eacsl after \Eva\index{Eva}: in such a case,
-\shortopt{e-acsl-prepare} must be provided together with the \Eva's
-\shortopt{val} option.
-\end{important}
-
 In this context, the \eacsl plug-in does not generate code for annotations
 proven valid by another plug-in, except if you explicitly set the option
 \shortopt{e-acsl-valid}. For instance, \Eva~\cite{eva} is able to
@@ -1003,21 +987,14 @@ prove that there is no potential overflow in the previous program, so the \eacsl
 plug-in does not generate additional code for checking them if you run the
 following command.
 \begin{shell}
-\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
+\$ frama-c -rte combine.i -then -val -then -e-acsl \
           -then-last -print -ocode monitored_combine.i
 \end{shell}
-The additional code will be generated with one of the two following commands.
+The additional code will be generated with the two following command.
 \begin{shell}
-\$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
-          -e-acsl-valid -then-last -print -ocode monitored_combine.i
 \$ frama-c -rte combine.i -then -val -then -e-acsl \
-          -then-last -print -ocode monitored_combine.i
+          -e-acsl-valid -then-last -print -ocode monitored_combine.i
 \end{shell}
-In the first case, that is because it is explicitly required by the option
-\shortopt{e-acsl-valid} while, in the second case, that is because the option
-\shortopt{e-acsl-prepare} is not provided on the command line which results in
-the fact that the result of the value analysis are unknown when the \eacsl
-plug-in is running.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1044,20 +1021,6 @@ check.i:4:[e-acsl] warning: E-ACSL construct `right shift' is not yet supported.
 [e-acsl] translation done in project "foobar".
 \end{shell}
 
-Further, the \eacsl plug-in option \shortopt{e-acsl-check} does not generate a
-new project but verifies that each annotation is translatable. Then it produces
-a summary as shown in the following example (left or right shifts in annotations
-are not yet supported by the \eacsl plug-in~\cite{eacsl-implem}).
-
-\begin{shell}
-\$ frama-c -e-acsl-check check.i
-<skip preprocessing commands>
-check.i:4:[e-acsl] warning: E-ACSL construct `left/right shift' is not yet supported.
-  Ignoring annotation.
-[e-acsl] 0 annotation was ignored, being untypable.
-[e-acsl] 1 annotation was ignored, being unsupported.
-\end{shell}
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%>>>

src/plugins/e-acsl/headers/header_spec.txt

@@ -100,8 +100,8 @@ src/local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/main.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/options.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/options.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/project_initializer/keep_status.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/project_initializer/keep_status.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/project_initializer/rtl.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/project_initializer/rtl.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/project_initializer/prepare_ast.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/project_initializer/prepare_ast.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 tests/print.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL

src/plugins/e-acsl/man/e-acsl-gcc.sh.1

@@ -206,8 +206,7 @@ executable found in the system path is used.
 .TP
 .B --then
 separate with a \fB-then\fP the first \fBFrama-C\fP options from the actual
-launch of the \fBE-ACSL\fP plugin. Prepends \fB-e-acsl-prepare\fP to the list
-of options passed to \fBFrama-C\fP.
+launch of the \fBE-ACSL\fP plugin.
 .TP
 .B --e-acsl-extra=\fI<OPTS>
 add \fI<OPTS>\fP to the list of options that will be given to the \fBE-ACSL\fP

src/plugins/e-acsl/scripts/e-acsl-gcc.sh

@@ -557,7 +557,6 @@ do
     --then)
       shift;
       OPTION_THEN=-then
-      FRAMAC_FLAGS="-e-acsl-prepare $FRAMAC_FLAGS"
     ;;
     # Extra E-ACSL options
     --e-acsl-extra)
@@ -754,7 +753,9 @@ CPPFLAGS="$OPTION_CPPFLAGS"
 LDFLAGS="$OPTION_LDFLAGS"
 
 # Extra Frama-C Flags E-ACSL needs
-FRAMAC_FLAGS="$FRAMAC_FLAGS -variadic-no-translation"
+FRAMAC_FLAGS="$FRAMAC_FLAGS \
+  -remove-unused-specified-functions \
+  -variadic-no-translation"
 
 # C, CPP and LD flags for compilation of E-ACSL-generated sources
 EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT"

src/plugins/e-acsl/src/analyses/lscope.ml

@@ -47,6 +47,8 @@ let exists lv t =
   in
   List.exists is_lv t
 
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+
 exception Lscope_used
 let is_used lscope pot =
   let o = object inherit Visitor.frama_c_inplace
@@ -57,8 +59,14 @@ let is_used lscope pot =
   in
   try
     (match pot with
-     | Misc.PoT_pred p -> ignore (Visitor.visitFramacPredicate o p)
-     | Misc.PoT_term t -> ignore (Visitor.visitFramacTerm o t));
+     | PoT_pred p -> ignore (Visitor.visitFramacPredicate o p)
+     | PoT_term t -> ignore (Visitor.visitFramacTerm o t));
     false
   with Lscope_used ->
     true
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)

src/plugins/e-acsl/src/analyses/lscope.mli

@@ -48,6 +48,13 @@ val get_all: t -> lscope_var list
    The first element is the first [lscope_var] that was added to [t], the
    second element is the second [lscope_var] that was added to [t], an so on. *)
 
-val is_used: t -> Misc.pred_or_term -> bool
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+val is_used: t -> pred_or_term -> bool
 (* [is_used lscope pot] returns [true] iff [pot] uses a variable from
    [lscope]. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)

src/plugins/e-acsl/src/analyses/mmodel_analysis.ml

@@ -27,7 +27,7 @@ module Dataflow = Dataflow2
 
 let must_never_monitor vi =
   (* E-ACSL, please do not monitor yourself! *)
-  Functions.RTL.is_rtl_name vi.vname
+  Rtl.Symbols.mem_vi vi.vname
   ||
   (* extern ghost variables are usually used (by the Frama-C libc) to
        represent some internal invisible states in ACSL specifications. They do
@@ -620,7 +620,7 @@ end = struct
   let compute init_set kf =
     Options.feedback ~dkey ~level:2 "entering in function %a."
       Kernel_function.pretty kf;
-    assert (not (Misc.is_library_loc (Kernel_function.get_location kf)));
+    assert (not (Rtl.Symbols.mem_kf kf));
     let tbl, is_init =
       try Env.find kf, true
       with Not_found -> Stmt.Hashtbl.create 17, false
@@ -660,7 +660,7 @@ end = struct
     tbl
 
   let get ?init kf =
-    if Misc.is_library_loc (Kernel_function.get_location kf) then
+    if Rtl.Symbols.mem_kf kf then
       Varinfo.Hptset.empty
     else
       try
@@ -799,6 +799,6 @@ let use_model () =
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/analyses/mmodel_analysis.mli

@@ -44,6 +44,6 @@ val must_model_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
 
 (*
   Local Variables:
-  compile-command: "make"
+  compile-command: "make -C ../../../../.."
   End:
  *)

src/plugins/e-acsl/src/analyses/rte.ml

@@ -24,17 +24,6 @@
 (** {2 Generic code} *)
 (* ************************************************************************** *)
 
-let apply_rte f x =
-  let signed = Kernel.SignedOverflow.get () in
-  let unsigned = Kernel.UnsignedOverflow.get () in
-  Kernel.SignedOverflow.off ();
-  Kernel.UnsignedOverflow.off ();
-  let finally () =
-    Kernel.SignedOverflow.set signed;
-    Kernel.UnsignedOverflow.set unsigned
-  in
-  Extlib.try_finally ~finally f x
-
 let warn_rte warn exn =
   if warn then
     Options.warning "@[@[cannot run RTE:@ %s.@]@ \
@@ -48,30 +37,24 @@ Ignoring potential runtime errors in annotations."
 open Cil_datatype
 
 let stmt ?(warn=true) =
-  try 
-    let f = 
-      Dynamic.get
-	~plugin:"RteGen" 
-	"stmt_annotations" 
-	(Datatype.func2 Kernel_function.ty Stmt.ty 
-	   (let module L = Datatype.List(Code_annotation) in L.ty))
-    in
-    (fun x y -> apply_rte (f x) y)
+  try
+    Dynamic.get
+      ~plugin:"RteGen"
+      "stmt_annotations"
+      (Datatype.func2 Kernel_function.ty Stmt.ty
+         (let module L = Datatype.List(Code_annotation) in L.ty))
   with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
     ->
       warn_rte warn exn;
       fun _ _ -> []
 
 let exp ?(warn=true) =
-  try 
-    let f = 
-      Dynamic.get
-	~plugin:"RteGen" 
-	"exp_annotations" 
-	(Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty 
-	   (let module L = Datatype.List(Code_annotation) in L.ty))
-    in
-    (fun x y z -> apply_rte (f x y) z)
+  try
+    Dynamic.get
+      ~plugin:"RteGen"
+      "exp_annotations"
+      (Datatype.func3 Kernel_function.ty Stmt.ty Exp.ty
+         (let module L = Datatype.List(Code_annotation) in L.ty))
   with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
     ->
       warn_rte warn exn;
@@ -79,6 +62,6 @@ let exp ?(warn=true) =
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/analyses/rte.mli

@@ -32,6 +32,6 @@ val exp: ?warn:bool -> kernel_function -> stmt -> exp -> code_annotation list
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
 End:
 *)