[eacsl] Update `__e_acsl_assert()` to use a structure holding all the data

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c

@@ -36,31 +36,38 @@ int eacsl_runtime_sound_verdict = 1;
 
 #ifndef E_ACSL_EXTERNAL_ASSERT
 /*! \brief Default implementation of E-ACSL runtime assertions */
-void eacsl_runtime_assert(int predicate, int blocking, const char *kind,
-                          const char *fct, const char *pred_txt,
-                          const char *file, int line) {
+void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
   if (eacsl_runtime_sound_verdict) {
     if (!predicate) {
+      // clang-format off
       STDERR("%s: In function '%s'\n"
              "%s:%d: Error: %s failed:\n"
              "\tThe failing predicate is:\n"
              "\t%s.\n",
-             file, fct, file, line, kind, pred_txt);
-      if (blocking) {
+             data->file, data->fct,
+             data->file, data->line, data->kind,
+             data->pred_txt);
+      // clang-format on
+      if (data->blocking) {
 #  ifndef E_ACSL_NO_ASSERT_FAIL /* Do fail on assertions */
 #    ifdef E_ACSL_FAIL_EXITCODE /* Fail by exit with a given code */
         exit(E_ACSL_FAIL_EXITCODE);
 #    else
-        raise_abort(file, line); /* Raise abort signal */
+        raise_abort(data->file, data->line); /* Raise abort signal */
 #    endif
 #  endif
       }
     }
-  } else
+  } else {
+    // clang-format off
     STDERR("%s: In function '%s'\n"
            "%s:%d: Warning: no sound verdict for %s (guess: %s).\n"
            "\tthe considered predicate is:\n"
            "\t%s\n",
-           file, fct, file, line, kind, predicate ? "ok" : "FAIL", pred_txt);
+           data->file, data->fct,
+           data->file, data->line, data->kind, predicate ? "ok" : "FAIL",
+           data->pred_txt);
+    // clang-format on
+  }
 }
 #endif

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h

@@ -31,6 +31,7 @@
 #include "../internals/e_acsl_alias.h"
 
 #define eacsl_runtime_sound_verdict export_alias(sound_verdict)
+#define eacsl_assert_data_t         export_alias(assert_data_t)
 #define eacsl_runtime_assert        export_alias(assert)
 
 /*! E-ACSL instrumentation automatically sets this global to 0 if its verdict
@@ -39,26 +40,38 @@
     For arithmetic properties, the verdict is always sound (?). */
 extern int __attribute__((FC_BUILTIN)) eacsl_runtime_sound_verdict;
 
+/*! Data holding context information for E-ACSL assertions. */
+typedef struct eacsl_assert_data_t {
+  /*! integer representing if the assertion is blocking or not */
+  int blocking;
+  /*! C string representing a kind of annotation (e.g., "Assertion") */
+  const char *kind;
+  /*! stringified predicate */
+  const char *pred_txt;
+  /*! un-instrumented file of predicate placement */
+  const char *file;
+  /*! function of predicate placement in the un-instrumented file */
+  const char *fct;
+  /*! line of predicate placement in the un-instrumented file */
+  int line;
+  /*! values contributing to the predicate */
+  void *values;
+} __attribute__((__FC_BUILTIN__)) eacsl_assert_data_t;
+
 /*! \brief Runtime assertion verifying a given predicate
- *  \param pred  integer code of a predicate
- *  \param blocking integer representing if the assertion is blocking or not
- *  \param kind  C string representing a kind of annotation (e.g., "Assertion")
- *  \param fct
- *  \param pred_txt  stringified predicate
- *  \param file un-instrumented file of predicate placement
- *  \param line line of predicate placement in the un-instrumented file */
-/*@ assigns \nothing;
+ *  \param predicate integer code of a predicate
+ *  \param data context data for the predicate. */
+/*@ requires \valid_read(data) && \initialized(data);
+  @ assigns \nothing;
   @ behavior blocking:
-  @   assumes blocking != 0;
-  @   requires pred != 0;
+  @   assumes data->blocking != 0;
+  @   requires predicate != 0;
   @ behavior non_blocking:
-  @   assumes blocking == 0;
-  @   check requires pred != 0;
+  @   assumes data->blocking == 0;
+  @   check requires predicate != 0;
   @ complete behaviors;
   @ disjoint behaviors; */
-void eacsl_runtime_assert(int pred, int blocking, const char *kind,
-                          const char *fct, const char *pred_txt,
-                          const char *file, int line)
+void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data)
     __attribute__((FC_BUILTIN));
 
 #endif // E_ACSL_ASSERT_H

src/plugins/e-acsl/src/code_generator/assert.ml

@@ -31,7 +31,10 @@ open Cil_types
 type data = {
   (** Indicates if some data have been registered in the context or not. *)
   data_registered: bool;
-  (* FIXME: fields added to hold information about the C variable in MR !3288 *)
+  (** [varinfo] representing the C variable for the assertion data. *)
+  data_vi: varinfo;
+  (** [exp] representing a pointer to the C variable for the assertion data. *)
+  data_ptr: exp;
 }
 
 (** External type representing the assertion context. Either [Some data] if we
@@ -40,10 +43,32 @@ type t = data option
 
 let no_data = None
 
+(** C type for the [assert_data_t] structure. *)
+let assert_data_ctyp_lazy =
+  lazy (Globals.Types.find_type
+          Logic_typing.Typedef (Functions.RTL.mk_api_name "assert_data_t"))
+
 let empty ~loc kf env =
-  (* FIXME: C variable created in MR !3288 *)
-  ignore (loc, kf);
-  let data = { data_registered = false } in
+  let assert_data_cty = Lazy.force assert_data_ctyp_lazy in
+  let data_vi, _, env =
+    Env.new_var
+      ~loc
+      ~name:"assert_data"
+      env
+      kf
+      None
+      assert_data_cty
+      (fun vi _ ->
+         [ Smart_stmt.struct_local_init
+             ~loc
+             vi
+             [ "values", Smart_exp.null ~loc ] ])
+  in
+  let data =
+    { data_registered = false;
+      data_vi;
+      data_ptr = Cil.mkAddrOfVi data_vi }
+  in
   Some data , env
 
 let with_data_from ~loc kf env from =
@@ -75,8 +100,8 @@ let register ~loc kf env ?(force=false) name e adata =
          The registration can be forced for expressions like [sizeof(int)] for
          instance that are [Const] values but not directly known. *)
       Some adata, env
-    | Some _adata, _ ->
-      let adata = { data_registered = true } in
+    | Some adata, _ ->
+      let adata = { adata with data_registered = true } in
       (* FIXME: value registered to [adata] in MR !3288 *)
       ignore (loc, kf, env, name);
       Some adata, env
@@ -108,7 +133,17 @@ let kind_to_string loc k =
      | Smart_stmt.Variant -> "Variant"
      | Smart_stmt.RTE -> "RTE")
 
-let runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env e =
+let runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env predicate_e =
+  let env = Env.push env in
+  let data_ptr, data_vi, env =
+    match adata with
+    | Some { data_ptr; data_vi } ->
+      data_ptr, data_vi, env
+    | None ->
+      let adata, env = empty ~loc kf env in
+      let adata = Option.get adata in
+      adata.data_ptr, adata.data_vi, env
+  in
   let blocking =
     match pred_kind with
     | Assert -> Cil.one ~loc
@@ -116,23 +151,33 @@ let runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env e =
     | Admit ->
       Options.fatal "No runtime check should be generated for 'admit' clauses"
   in
+  let kind = kind_to_string loc kind in
+  let pred_txt = Cil.mkString ~loc msg in
   let start_pos = fst loc in
-  let file = start_pos.Filepath.pos_path in
-  let line = start_pos.Filepath.pos_lnum in
-  (* FIXME: [adata] support in MR !3288 *)
-  ignore adata;
-  let stmt =
-    Smart_stmt.rtl_call ~loc
-      "assert"
-      [ e;
-        blocking;
-        kind_to_string loc kind;
-        Cil.mkString ~loc (Functions.RTL.get_original_name kf);
-        Cil.mkString ~loc msg;
-        Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
-        Cil.integer loc line ]
+  let file =
+    Cil.mkString
+      ~loc
+      (Filepath.Normalized.to_pretty_string start_pos.Filepath.pos_path)
+  in
+  let fct = Cil.mkString ~loc (Functions.RTL.get_original_name kf) in
+  let line = Cil.integer ~loc start_pos.Filepath.pos_lnum in
+  let stmts =
+    [ Smart_stmt.rtl_call ~loc "assert" [ predicate_e; data_ptr ];
+      Smart_stmt.assigns_field ~loc data_vi "line" line;
+      Smart_stmt.assigns_field ~loc data_vi "fct" fct;
+      Smart_stmt.assigns_field ~loc data_vi "file" file;
+      Smart_stmt.assigns_field ~loc data_vi "pred_txt" pred_txt;
+      Smart_stmt.assigns_field ~loc data_vi "kind" kind;
+      Smart_stmt.assigns_field ~loc data_vi "blocking" blocking ]
+  in
+  let block, env =
+    Env.pop_and_get
+      env
+      (Smart_stmt.block_from_stmts (List.rev stmts))
+      ~global_clear:false
+      Env.Middle
   in
-  stmt, env
+  Smart_stmt.block_stmt block, env
 
 let runtime_check ~adata ~pred_kind kind kf env e p =
   let loc = p.pred_loc in