[eacsl] Use the label analysis to translate `\at` values

src/plugins/e-acsl/Makefile.in

@@ -62,7 +62,6 @@ ANALYSES_CMI:=$(addprefix src/analyses/, $(ANALYSES_CMI))
 
 SRC_ANALYSES:= \
 	analyses_datatype \
-	label \
 	rte \
 	lscope \
 	e_acsl_visitor \
@@ -95,10 +94,10 @@ SRC_CODE_GENERATOR:= \
 	logic_functions \
 	loops \
 	quantif \
-	at_with_lscope \
 	memory_translate \
 	logic_array \
 	translate_utils \
+	translate_ats \
 	translate_terms \
 	translate_predicates \
 	translate_rtes \

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

@@ -92,8 +92,6 @@ src/analyses/exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/labels.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/labels.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
@@ -112,8 +110,6 @@ src/code_generator/assert.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/assert.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/assigns.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/assigns.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/at_with_lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/at_with_lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/contract.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/contract.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/contract_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
@@ -151,6 +147,8 @@ src/code_generator/temporal.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/temporal.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_annots.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_annots.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_ats.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_ats.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_predicates.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_predicates.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_rtes.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL

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

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
-(*                                                                        *)
-(*  Copyright (C) 2012-2021                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-open Cil_types
-module Error = Error.Make(struct let phase = Options.Dkey.translation end)
-
-let get_first_inner_stmt stmt =
-  match stmt.labels, stmt.skind with
-  | [], _ -> stmt
-  | _ :: _, Block { bstmts = dest_stmt :: _ } ->
-    dest_stmt
-  | labels, _ ->
-    Options.fatal "Unexpected stmt:\nlabels: [%a]\nstmt: %a"
-      (Pretty_utils.pp_list ~sep:"; " Cil_types_debug.pp_label) labels
-      Printer.pp_stmt stmt
-
-let get_stmt kf llabel =
-  let stmt = match llabel with
-    | StmtLabel { contents = stmt } -> stmt
-    | BuiltinLabel Here -> Error.not_yet "Label 'Here'"
-    | BuiltinLabel(Old | Pre) ->
-      (try Kernel_function.find_first_stmt kf
-       with Kernel_function.No_Statement -> assert false (* Frama-C invariant*))
-    | BuiltinLabel(Post) ->
-      (try Kernel_function.find_return kf
-       with Kernel_function.No_Statement -> assert false (* Frama-C invariant*))
-    | BuiltinLabel _ ->
-      Error.not_yet (Format.asprintf "Label '%a'" Printer.pp_logic_label llabel)
-    | FormalLabel _ ->
-      Error.not_yet "FormalLabel"
-  in
-  (* the pointed statement has been visited and modified by the injector:
-     get its new version. *)
-  get_first_inner_stmt stmt
-
-(*
-Local Variables:
-compile-command: "make -C ../../../../.."
-End:
-*)

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

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
-(*                                                                        *)
-(*  Copyright (C) 2012-2021                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-open Cil_types
-
-val get_stmt: kernel_function -> logic_label -> stmt
-(** @return the statement where the logic label points to. *)
-
-(*
-Local Variables:
-compile-command: "make -C ../../../../.."
-End:
-*)

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

@@ -196,6 +196,11 @@ let register_pred ~loc env ?force p e adata =
     let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
     register ~loc env name ?force e adata
 
+let register_pred_or_term ~loc env ?force pot e adata =
+  match pot with
+  | PoT_term t -> register_term ~loc env ?force t e adata
+  | PoT_pred p -> register_pred ~loc env ?force p e adata
+
 let kind_to_string loc k =
   Cil.mkString
     ~loc

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

@@ -97,6 +97,19 @@ val register_pred:
     parameter [force] has the same signification than for the function
     [register]. *)
 
+val register_pred_or_term:
+  loc:location ->
+  Env.t ->
+  ?force:bool ->
+  pred_or_term ->
+  exp ->
+  t ->
+  t * Env.t
+(** [register_pred_or_term ~loc kf env ?force pot e adata] registers the data
+    [e] corresponding to the predicate or term [pot] to the assertion context
+    [adata]. The parameter [force] has the same signification than for the
+    function [register]. *)
+
 val runtime_check:
   adata:t ->
   pred_kind:predicate_kind ->

src/plugins/e-acsl/src/code_generator/env.mli

@@ -186,6 +186,10 @@ end
 (** {2 Context for error handling} *)
 (* ************************************************************************** *)
 
+module Context: sig
+  val save: t -> unit
+end
+
 val handle_error: (t -> t) -> t -> t
 (** Run the closure with the given environment and handle potential errors.
     Restore the globals of the environment to the last time [Env.Context.save]
@@ -200,7 +204,6 @@ val handle_error_with_args: (t * 'a -> t * 'a) -> t * 'a -> t * 'a
 val not_yet: t -> string -> 'a
 (** Save the current context and raise [Error.Not_yet] exception. *)
 
-
 (* ************************************************************************** *)
 (** {2 Current environment kinstr} *)
 (* ************************************************************************** *)

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

@@ -443,7 +443,7 @@ and inject_in_stmt env kf stmt =
   in
   let env = Env.set_kinstr env (Kstmt stmt) in
   (* initial environment *)
-  let env =
+  let env, translate_pre_funspec =
     if Kernel_function.is_first_stmt kf stmt then
       let env =
         if Kernel_function.is_main kf then
@@ -454,11 +454,18 @@ and inject_in_stmt env kf stmt =
           in
           Temporal.handle_function_parameters kf env
       in
-      (* translate the precondition of the function *)
-      if Functions.check kf then
-        let funspec = Annotations.funspec kf in
-        Translate_annots.pre_funspec kf env funspec
-      else env
+      (* check if the precondition of the function needs to be translated *)
+      env, Functions.check kf
+    else
+      env, false
+  in
+  (* translate all \at() predicates and terms that reference the current stmt *)
+  let env = Translate_ats.for_stmt env kf stmt in
+  (* translate the precondition of the function *)
+  let env =
+    if translate_pre_funspec then
+      let funspec = Annotations.funspec kf in
+      Translate_annots.pre_funspec kf env funspec
     else
       env
   in
@@ -497,7 +504,7 @@ and inject_in_block (env: Env.t) kf blk =
   (* now inject code that de-allocates the necessary observation variables and
      blocks of the runtime memory that have been previously allocated *)
   (* calls to [free] for de-allocating variables observing \at(_,_) *)
-  let free_stmts = At_with_lscope.Free.find_all kf in
+  let free_stmts = Translate_ats.Free.find_all kf in
   match blk.blocals, free_stmts with
   | [], [] ->
     env
@@ -511,7 +518,7 @@ and inject_in_block (env: Env.t) kf blk =
           (* now that [free] stmts for [kf] have been inserted,
              there is no more need to keep the corresponding entries in the
              table managing them. *)
-          At_with_lscope.Free.remove_all kf;
+          Translate_ats.Free.remove_all kf;
           (* The free statements are passed in the same order than the malloc
              ones. In order to free the variable in the reverse order, the list
              is reversed before appending the return statement. Moreover,
@@ -573,12 +580,12 @@ let add_generated_variables_in_function env fundec =
 (* Memory management for \at on purely logic variables: put [malloc] stmts at
    proper locations *)
 let add_malloc_and_free_stmts kf fundec =
-  let malloc_stmts = At_with_lscope.Malloc.find_all kf in
+  let malloc_stmts = Translate_ats.Malloc.find_all kf in
   let fstmts = malloc_stmts @ fundec.sbody.bstmts in
   fundec.sbody.bstmts <- fstmts;
   (* now that [malloc] stmts for [kf] have been inserted, there is no more need
      to keep the corresponding entries in the table managing them. *)
-  At_with_lscope.Malloc.remove_all kf
+  Translate_ats.Malloc.remove_all kf
 
 let inject_in_fundec main fundec =
   let vi = fundec.svar in

src/plugins/e-acsl/src/code_generator/at_with_lscope.ml → src/plugins/e-acsl/src/code_generator/translate_ats.ml

@@ -20,62 +20,72 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Generate C implementations of E-ACSL [\at()] terms and predicates. *)
+
 open Cil_types
+open Cil_datatype
 open Analyses_types
+open Analyses_datatype
+module Error = Translation_error
 
 (**************************************************************************)
 (********************** Forward references ********************************)
 (**************************************************************************)
 
-let predicate_to_exp_ref
+let term_to_exp_ref
   : (adata:Assert.t ->
+     ?inplace:bool ->
      kernel_function ->
      Env.t ->
-     predicate ->
+     term ->
      exp * Assert.t * Env.t) ref
   =
-  ref (fun ~adata:_ _kf _env _p ->
-      Extlib.mk_labeled_fun "predicate_to_exp_ref")
+  ref (fun ~adata:_ ?inplace:_ _kf _env _t ->
+      Extlib.mk_labeled_fun "term_to_exp_ref")
 
-let term_to_exp_ref
+let predicate_to_exp_ref
   : (adata:Assert.t ->
+     ?inplace:bool ->
+     ?name:string ->
      kernel_function ->
+     ?rte:bool ->
      Env.t ->
-     term ->
+     predicate ->
      exp * Assert.t * Env.t) ref
   =
-  ref (fun ~adata:_ _kf _env _t -> Extlib.mk_labeled_fun "term_to_exp_ref")
+  ref (fun ~adata:_ ?inplace:_ ?name:_ _kf ?rte:_ _env _p ->
+      Extlib.mk_labeled_fun "predicate_to_exp_ref")
 
 (*****************************************************************************)
 (**************************** Handling memory ********************************)
 (*****************************************************************************)
 
-(* Remove all the bindings for [kf]. [Cil_datatype.Kf.Hashtbl] does not
-   provide the [remove_all] function. Thus we need to keep calling [remove]
-   until all entries are removed. *)
+(** Remove all the bindings for [kf]. [Kf.Hashtbl] does not provide the
+    [remove_all] function. Thus we need to keep calling [remove] until all
+    entries are removed. *)
 let rec remove_all tbl kf =
-  if Cil_datatype.Kf.Hashtbl.mem tbl kf then begin
-    Cil_datatype.Kf.Hashtbl.remove tbl kf;
+  if Kf.Hashtbl.mem tbl kf then begin
+    Kf.Hashtbl.remove tbl kf;
     remove_all tbl kf
   end
 
 module Malloc = struct
-  let tbl = Cil_datatype.Kf.Hashtbl.create 7
-  let add kf stmt = Cil_datatype.Kf.Hashtbl.add tbl kf stmt
-  let find_all kf = Cil_datatype.Kf.Hashtbl.find_all tbl kf
+  let tbl = Kf.Hashtbl.create 7
+  let add kf stmt = Kf.Hashtbl.add tbl kf stmt
+  let find_all kf = Kf.Hashtbl.find_all tbl kf
   let remove_all kf = remove_all tbl kf
 end
 
 module Free = struct
-  let tbl = Cil_datatype.Kf.Hashtbl.create 7
-  let add kf stmt = Cil_datatype.Kf.Hashtbl.add tbl kf stmt
-  let find_all kf = Cil_datatype.Kf.Hashtbl.find_all tbl kf
+  let tbl = Kf.Hashtbl.create 7
+  let add kf stmt = Kf.Hashtbl.add tbl kf stmt
+  let find_all kf = Kf.Hashtbl.find_all tbl kf
   let remove_all kf = remove_all tbl kf
 end
 
-(**************************************************************************)
-(*************************** Translation **********************************)
-(**************************************************************************)
+(* ************************************************************************** *)
+(* Helper functions for "with lscope" translation *)
+(* ************************************************************************** *)
 
 (* Builds the terms [t_size] and [t_shifted] from each
    [Lvs_quantif(tmin, lv, tmax)] from [lscope]
@@ -171,7 +181,7 @@ let size_from_sizes_and_shifts ~loc = function
       sizes_and_shifts
 
 (* Build the left-value corresponding to [*(at + index)]. *)
-let lval_at_index ~loc kf env (e_at, vi_at, t_index) =
+let lval_at_index ~loc kf env (e_at, t_index) =
   Typing.type_term
     ~use_gmp_opt:false
     ~ctx:Typing.c_int
@@ -181,7 +191,7 @@ let lval_at_index ~loc kf env (e_at, vi_at, t_index) =
   let e_index, _, env = term_to_exp ~adata:Assert.no_data kf env t_index in
   let e_index = Cil.constFold false e_index in
   let e_addr =
-    Cil.new_exp ~loc (BinOp(PlusPI, e_at, e_index, vi_at.vtype))
+    Cil.new_exp ~loc (BinOp(PlusPI, e_at, e_index, Cil.typeOf e_at))
   in
   let lval_at_index = Mem e_addr, NoOffset in
   lval_at_index, env
@@ -219,23 +229,74 @@ let index_from_sizes_and_shifts ~loc sizes_and_shifts =
   in
   sum
 
-let put_block_at_label env kf block label =
-  let stmt = Label.get_stmt kf label in
-  let env_ref = ref env in
-  let o = object
-    inherit Visitor.frama_c_inplace
-    method !vstmt_aux stmt =
-      assert (!env_ref == env);
-      env_ref := Env.extend_stmt_in_place env stmt ~label block;
-      Cil.ChangeTo stmt
-  end
+(* [indexed_exp ~loc kf env e_at]
+   [e_at] represents an array generated by [pretranslate_to_exp_with_lscope]
+   and filled during the traversal of the [lscope].
+   The function returns an expression indexing the array [e_at] using the
+   variables created when traversing the [lscope] to retrieve the [\at] value
+   during the traversal. *)
+let indexed_exp ~loc kf env e_at =
+  let lscope_vars = Lscope.get_all (Env.Logic_scope.get env) in
+  let lscope_vars = List.rev lscope_vars in
+  let sizes_and_shifts =
+    sizes_and_shifts_from_quantifs ~loc kf lscope_vars []
+  in
+  let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
+  let lval_at_index, env = lval_at_index ~loc kf env (e_at, t_index) in
+  let e = Smart_exp.lval ~loc lval_at_index in
+  e, env
+
+(* ************************************************************************** *)
+(* Translation *)
+(* ************************************************************************** *)
+
+let pretranslate_to_exp ~loc kf env pot =
+  Options.debug ~level:4 "pre-translating %a in local environment '%a'"
+    PredOrTerm.pretty pot
+    Typing.Function_params_ty.pretty (Env.Local_vars.get env);
+  let t_opt =
+    match pot with
+    | PoT_term t -> Some t
+    | PoT_pred _ -> None
+  in
+  let e, _ , env =
+    let adata = Assert.no_data in
+    match pot with
+    | PoT_term t -> !term_to_exp_ref ~adata ~inplace:true kf env t
+    | PoT_pred p -> !predicate_to_exp_ref ~adata ~inplace:true kf env p
   in
-  ignore (Visitor.visitFramacStmt o stmt);
-  !env_ref
+  let ty = Cil.typeOf e in
+  let _, var_e, env =
+    Env.new_var
+      ~loc
+      ~scope:Function
+      ~name:"at"
+      env
+      kf
+      t_opt
+      ty
+      (fun var_vi var_e ->
+         let init_set =
+           if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
+         in
+         [ init_set ~loc (Cil.var var_vi) var_e e ])
+  in
+  var_e, env
 
-let to_exp ~loc kf env pot label =
+(* [pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot] immediately
+   translates the given [pred_or_term] in the current environment for each value
+   of the given [lscope]. The result is stored in a dynamically allocated array
+   and the expression returned is a pointer to this array.
+   The function [indexed_exp] can later be used to retrieve the translation for
+   a specific value of the [lscope]. *)
+let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
+  Options.debug ~level:4
+    "pre-translating %a in local environment '%a' with lscope '%a'"
+    PredOrTerm.pretty pot
+    Typing.Function_params_ty.pretty (Env.Local_vars.get env)
+    Lscope.D.pretty lscope;
   let term_to_exp = !term_to_exp_ref in
-  let lscope_vars = Lscope.get_all (Env.Logic_scope.get env) in
+  let lscope_vars = Lscope.get_all lscope in
   let lscope_vars = List.rev lscope_vars in
   let sizes_and_shifts =
     sizes_and_shifts_from_quantifs ~loc kf lscope_vars []
@@ -256,7 +317,7 @@ let to_exp ~loc kf env pot label =
       end
   in
   let ty_ptr = TPtr(ty, []) in
-  let vi_at, e_at, env = Env.new_var
+  let _, e_at, env = Env.new_var
       ~loc
       ~name:"at"
       ~scope:Varname.Function
@@ -309,13 +370,15 @@ let to_exp ~loc kf env pot label =
   let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
   (* Innermost block *)
   let mk_innermost_block env =
-    let term_to_exp = !term_to_exp_ref ~adata:Assert.no_data in
-    let named_predicate_to_exp = !predicate_to_exp_ref ~adata:Assert.no_data in
+    let term_to_exp = !term_to_exp_ref ~adata:Assert.no_data ~inplace:true in
+    let predicate_to_exp =
+      !predicate_to_exp_ref ~adata:Assert.no_data ~inplace:true
+    in
     match pot with
     | PoT_pred p ->
       let env = Env.push env in
-      let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
-      let e, _, env = named_predicate_to_exp kf env p in
+      let lval, env = lval_at_index ~loc kf env (e_at, t_index) in
+      let e, _, env = predicate_to_exp kf env p in
       let e = Cil.constFold false e in
       let storing_stmt =
         Smart_stmt.assigns ~loc ~result:lval e
@@ -330,7 +393,7 @@ let to_exp ~loc kf env pot label =
       begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
         | Typing.(C_integer _ | C_float _ | Nan) ->
           let env = Env.push env in
-          let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
+          let lval, env = lval_at_index ~loc kf env (e_at, t_index) in
           let e, _, env = term_to_exp kf env t in
           let e = Cil.constFold false e in
           let storing_stmt =
@@ -349,7 +412,7 @@ let to_exp ~loc kf env pot label =
       end
   in
   (* Storing loops *)
-  let lscope_vars = Lscope.get_all (Env.Logic_scope.get env) in
+  let lscope_vars = Lscope.get_all lscope in
   let lscope_vars = List.rev lscope_vars in
   let env = Env.push env in
   let storing_loops_stmts, env =
@@ -362,15 +425,87 @@ let to_exp ~loc kf env pot label =
       ~global_clear:false
       Env.After
   in
-  (* Put at label *)
-  let env = put_block_at_label env kf storing_loops_block label in
+  (* Put block in the current env *)
+  let env = Env.add_stmt env (Smart_stmt.block_stmt storing_loops_block) in
   (* Returning *)
-  let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
-  let e = Smart_exp.lval ~loc lval_at_index in
-  e, env
+  e_at, env
 
-(*
-Local Variables:
-compile-command: "make -C ../../../../.."
-End:
-*)
+let for_stmt env kf stmt =
+  let at_for_stmt =
+    Error.retrieve_preprocessing
+      "blabla"
+      Labels.Translation.at_for_stmt
+      stmt
+      Printer.pp_stmt
+  in
+  Options.debug ~level:4 "pre-translating %d ats for stmt %d at %a"
+    (List.length at_for_stmt)
+    stmt.sid
+    Printer.pp_location (Stmt.loc stmt);
+  let stmt_translations = PredOrTerm.Hashtbl.create 7 in
+  List.fold_left
+    (fun env ((_, _, lscope, pot, _) as at_data) ->
+       let e_or_err, env =
+         try
+           match PredOrTerm.Hashtbl.find_opt stmt_translations pot with
+           | Some e_or_err -> e_or_err, env
+           | None ->
+             let loc = Stmt.loc stmt in
+             let e, env =
+               if Lscope.is_used lscope pot then
+                 pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot
+               else
+                 pretranslate_to_exp ~loc kf env pot
+             in
+             (Result.Ok (Labels.Translation.Done e)), env
+         with Error.(Typing_error _ | Not_yet _) as exn ->
+           (Result.Error exn), env
+       in
+       PredOrTerm.Hashtbl.replace stmt_translations pot e_or_err;
+       Labels.Translation.set ~force:true at_data e_or_err;
+       env)
+    env
+    at_for_stmt
+
+let to_exp ~loc ~adata kf env pot label =
+  let kinstr = Env.get_kinstr env in
+  let lscope = Env.Logic_scope.get env in
+  try
+    let e_or_err = Labels.Translation.get (kf, kinstr, lscope, pot, label) in
+    let e, adata, env =
+      match e_or_err with
+      | Result.Ok (Labels.Translation.Done e) ->
+        let e, env =
+          if Lscope.is_used lscope pot then
+            indexed_exp ~loc kf env e
+          else
+            e, env
+        in
+        let adata, env =
+          Assert.register_pred_or_term ~loc env pot e adata
+        in
+        e, adata, env
+      | Result.Ok Labels.Translation.Inplace -> begin
+          match pot with
+          | PoT_term t -> !term_to_exp_ref ~adata ~inplace:true kf env t
+          | PoT_pred p -> !predicate_to_exp_ref ~adata ~inplace:true kf env p
+        end
+      | Result.Ok Labels.Translation.Queued ->
+        let potstr =
+          match pot with PoT_term _ -> "term" | PoT_pred _ -> "predicate"
+        in
+        Options.abort ~source:(fst loc)
+          "%s '%a' was used before being translated.@ \
+           This usually happen when using a label defined after the place@ \
+           where the %s should be translated"
+          potstr
+          PredOrTerm.pretty pot
+          potstr
+      | Result.Error exn ->
+        Env.Context.save env;
+        raise exn
+    in
+    e, adata, env
+  with Not_found ->
+    Options.fatal ~source:(fst loc) "no translation for %a"
+      Labels.pp_at_data (kf, kinstr, lscope, pot, label)

src/plugins/e-acsl/src/code_generator/at_with_lscope.mli → src/plugins/e-acsl/src/code_generator/translate_ats.mli

@@ -20,61 +20,76 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Generate C implementations of E-ACSL [\at()] terms and predicates. *)
+
 open Cil_types
-open Cil_datatype
 open Analyses_types
 
-(* Convert \at on terms or predicates in which we can find purely
-   logic variable. *)
-
 (**************************************************************************)
 (*************************** Translation **********************************)
 (**************************************************************************)
 
+val for_stmt: Env.t -> kernel_function -> stmt -> Env.t
+(** Translate all [\at()] predicates and terms for the given statement in the
+    current environment. *)
+
 val to_exp:
-  loc:Location.t -> kernel_function -> Env.t ->
-  pred_or_term -> logic_label -> exp * Env.t
+  loc:location ->
+  adata:Assert.t ->
+  kernel_function ->
+  Env.t ->
+  pred_or_term ->
+  logic_label ->
+  exp * Assert.t * Env.t
+(** @return the C expression corresponding to the given [pred_or_term].
+
+    The expression is either translated in-place or retrieved from a
+    pre-translation phase. *)
 
 (*****************************************************************************)
 (**************************** Handling memory ********************************)
 (*****************************************************************************)
 
 (* The different possible evaluations of the [\at] under study are
-   stored in a memory location that needs to be alloted then freed.
+   stored in a memory location that needs to be allocated then freed.
    This part is designed for that purpose. *)
 
 module Malloc: sig
   val find_all: kernel_function -> stmt list
-  (* Return the list of [malloc] stmts that need to be inserted into [kf]. *)
+  (** @return the list of [malloc] stmts that need to be inserted into [kf]. *)
 
   val remove_all: kernel_function -> unit
-  (* Remove all [malloc] stmts for [kf] from the internal table. *)
+  (** Remove all [malloc] stmts for [kf] from the internal table. *)
 end
 
 module Free: sig
   val find_all: kernel_function -> stmt list
-  (* Return the list of [free] stmts that need to be inserted into [kf]. *)
+  (** @return the list of [free] stmts that need to be inserted into [kf]. *)
 
   val remove_all: kernel_function -> unit
-  (* Remove all [free] stmts for [kf] from the internal table. *)
+  (** Remove all [free] stmts for [kf] from the internal table. *)
 end
 
 (**************************************************************************)
 (********************** Forward references ********************************)
 (**************************************************************************)
 
-val predicate_to_exp_ref:
+val term_to_exp_ref:
   (adata:Assert.t ->
+   ?inplace:bool ->
    kernel_function ->
    Env.t ->
-   predicate ->
+   term ->
    exp * Assert.t * Env.t) ref
 
-val term_to_exp_ref:
+val predicate_to_exp_ref:
   (adata:Assert.t ->
+   ?inplace:bool ->
+   ?name:string ->
    kernel_function ->
+   ?rte:bool ->
    Env.t ->
-   term ->
+   predicate ->
    exp * Assert.t * Env.t) ref
 
 (*

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

@@ -66,8 +66,11 @@ let relation_to_binop = function
 
 (* Convert an ACSL predicate into a corresponding C expression (if any) in the
    given environment. Also extend this environment which includes the generating
-   constructs. *)
-let rec predicate_content_to_exp ~adata ?name kf env p =
+   constructs.
+   If [inplace] is true, then the root predicate is immediately translated
+   regardless of its label. Otherwise [Translate_ats] is used to retrieve the
+   translation. *)
+let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
   let loc = p.pred_loc in
   let lenv = Env.Local_vars.get env in
   Cil.CurrentLoc.set loc;
@@ -202,25 +205,11 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
     let e, env = Quantif.quantif_to_exp kf env p in
     let adata, env = Assert.register_pred ~loc env p e adata in
     e, adata, env
-  | Pat(p, BuiltinLabel Here) ->
-    to_exp ~adata kf env p
   | Pat(p', label) ->
-    let lscope = Env.Logic_scope.get env in
-    let pot = PoT_pred p' in
-    if Lscope.is_used lscope pot then
-      let e, env = At_with_lscope.to_exp ~loc kf env pot label in
-      let adata, env = Assert.register_pred ~loc env p e adata in
-      e, adata, env
-    else begin
-      (* convert [t'] to [e] in a separated local env *)
-      let e, adata, env = to_exp ~adata kf (Env.push env) p' in
-      let e, env, sty =
-        Translate_utils.at_to_exp_no_lscope kf env None label e
-      in
-      assert (sty = Typed_number.C_number);
-      let adata, env = Assert.register_pred ~loc env p e adata in
-      e, adata, env
-    end
+    if inplace then
+      to_exp ~adata kf env p'
+    else
+      Translate_ats.to_exp ~loc ~adata kf env (PoT_pred p) label
   | Pvalid_read(BuiltinLabel Here, t) as pc
   | (Pvalid(BuiltinLabel Here, t) as pc) ->
     let call_valid ~adata t p =
@@ -309,7 +298,19 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
   | Pfreeable _ -> Env.not_yet env "labeled \\freeable"
   | Pfresh _ -> Env.not_yet env "\\fresh"
 
-and to_exp ~adata ?name kf ?rte env p =
+(** [to_exp ~adata ?inplace ?name kf ?rte env p] converts an ACSL predicate into
+    a corresponding C expression.
+    - [adata]: assertion context.
+    - [inplace]: if the root predicate has a label, indicates if it should be
+      immediately translated or if [Translate_ats] should be used to retrieve
+      the translation.
+    - [name]: name to use for generated variables.
+    - [kf]: The enclosing function.
+    - [rte]: if true, generate and translate RTE before translating the
+      predicate.
+    - [env]: The current environment.
+    - [p]: The predicate to translate. *)
+and to_exp ~adata ?inplace ?name kf ?rte env p =
   let p = Logic_normalizer.get_pred p in
   let rte = match rte with None -> Env.generate_rte env | Some b -> b in
   Extlib.flatten
@@ -317,7 +318,7 @@ and to_exp ~adata ?name kf ?rte env p =
        ~rte:false
        ~f:(fun env ->
            let e, adata, env =
-             predicate_content_to_exp ~adata ?name kf env p
+             predicate_content_to_exp ?inplace ~adata ?name kf env p
            in
            let env = if rte then !translate_rte_exp_ref kf env e else env in
            let cast =
@@ -385,12 +386,15 @@ let predicate_to_exp_without_rte ~adata kf env p =
   (* forget optional argument ?rte and ?name*)
   to_exp ~adata kf env p
 
+let predicate_to_exp_without_inplace ~adata ?name kf ?rte env p =
+  to_exp ~adata ?name kf ?rte env p
+
 let () =
-  Translate_utils.predicate_to_exp_ref := to_exp;
+  Translate_utils.predicate_to_exp_ref := predicate_to_exp_without_inplace;
+  Translate_ats.predicate_to_exp_ref := to_exp;
   Loops.translate_predicate_ref := do_it;
   Loops.predicate_to_exp_ref := predicate_to_exp_without_rte;
   Quantif.predicate_to_exp_ref := predicate_to_exp_without_rte;
-  At_with_lscope.predicate_to_exp_ref := predicate_to_exp_without_rte;
   Memory_translate.predicate_to_exp_ref := predicate_to_exp_without_rte;
   Logic_functions.predicate_to_exp_ref := predicate_to_exp_without_rte
 

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

@@ -261,7 +261,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
   | _ ->
     assert false
 
-and context_insensitive_term_to_exp ~adata kf env t =
+and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
   let loc = t.term_loc in
   let lenv = Env.Local_vars.get env in
   match t.term_node with
@@ -799,23 +799,14 @@ and context_insensitive_term_to_exp ~adata kf env t =
            env)
     in
     e, adata, env, Typed_number.C_number, ""
-  | Tat(t, BuiltinLabel Here) ->
-    let e, adata, env = to_exp ~adata kf env t in
-    e, adata, env, Typed_number.C_number, ""
   | Tat(t', label) ->
-    let lscope = Env.Logic_scope.get env in
-    let pot = PoT_term t' in
-    if Lscope.is_used lscope pot then
-      let e, env = At_with_lscope.to_exp ~loc kf env pot label in
-      let adata, env = Assert.register_term ~loc env t e adata in
-      e, adata, env, Typed_number.C_number, ""
-    else
-      let e, _, env = to_exp ~adata:Assert.no_data kf (Env.push env) t' in
-      let e, env, sty =
-        Translate_utils.at_to_exp_no_lscope kf env (Some t) label e
-      in
-      let adata, env = Assert.register_term ~loc env t e adata in
-      e, adata, env, sty, ""
+    let e, adata, env =
+      if inplace then
+        to_exp ~adata kf env t'
+      else
+        Translate_ats.to_exp ~loc ~adata kf env (PoT_term t) label
+    in
+    e, adata, env, Typed_number.C_number, ""
   | Tbase_addr(BuiltinLabel Here, t') ->
     let name = "base_addr" in
     let e, _, env =
@@ -876,7 +867,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
 (* Convert an ACSL term into a corresponding C expression (if any) in the given
    environment. Also extend this environment in order to include the generating
    constructs. *)
-and to_exp ~adata kf env t =
+and to_exp ~adata ?inplace kf env t =
   let generate_rte = Env.generate_rte env in
   Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)in local \
                                    environment '%a'"
@@ -888,7 +879,7 @@ and to_exp ~adata kf env t =
        ~rte:false
        ~f:(fun env ->
            let e, adata, env, sty, name =
-             context_insensitive_term_to_exp ~adata kf env t
+             context_insensitive_term_to_exp ?inplace ~adata kf env t
            in
            let env =
              if generate_rte then !translate_rte_exp_ref kf env e else env
@@ -909,12 +900,14 @@ and to_exp ~adata kf env t =
          )
        env)
 
+let term_to_exp_without_inplace ~adata kf env t = to_exp ~adata kf env t
+
 let () =
-  Translate_utils.term_to_exp_ref := to_exp;
-  Loops.term_to_exp_ref := to_exp;
-  At_with_lscope.term_to_exp_ref := to_exp;
-  Memory_translate.term_to_exp_ref := to_exp;
-  Logic_functions.term_to_exp_ref := to_exp
+  Translate_utils.term_to_exp_ref := term_to_exp_without_inplace;
+  Translate_ats.term_to_exp_ref := to_exp;
+  Loops.term_to_exp_ref := term_to_exp_without_inplace;
+  Memory_translate.term_to_exp_ref := term_to_exp_without_inplace;
+  Logic_functions.term_to_exp_ref := term_to_exp_without_inplace
 
 exception No_simple_translation of term
 

src/plugins/e-acsl/src/code_generator/translate_terms.mli

@@ -26,11 +26,20 @@ open Cil_types
 
 val to_exp:
   adata:Assert.t ->
+  ?inplace:bool ->
   kernel_function ->
   Env.t ->
   term ->
   exp * Assert.t * Env.t
-(** Convert an ACSL term into a corresponding C expression. *)
+(** [to_exp ~adata ?inplace kf env t] converts an ACSL term into a
+    corresponding C expression.
+    - [adata]: assertion context.
+    - [inplace]: if the root term has a label, indicates if it should be
+      immediately translated or if [Translate_ats] should be used to retrieve
+      the translation.
+    - [kf]: The enclosing function.
+    - [env]: The current environment.
+    - [t]: The term to translate. *)
 
 exception No_simple_translation of term
 (** Exceptin raised if [untyped_to_exp] would generate new statements in

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

@@ -22,9 +22,7 @@
 
 (** Utility functions for generating C implementations. *)
 
-module E_acsl_label = Label
 open Cil_types
-open Cil_datatype
 module Error = Translation_error
 
 (**************************************************************************)
@@ -304,51 +302,6 @@ let env_of_li ~adata ~loc kf env li =
   | Larrow _ ->
     Env.not_yet env "lambda-abstraction"
 
-let at_to_exp_no_lscope kf env t_opt label e =
-  let stmt = E_acsl_label.get_stmt kf label in
-  (* generate a new variable denoting [\at(t',label)].
-     That is this variable which is the resulting expression.
-     ACSL typing rule ensures that the type of this variable is the same as
-     the one of [e]. *)
-  let loc = Stmt.loc stmt in
-  let res_v, res, new_env =
-    Env.new_var
-      ~loc
-      ~name:"at"
-      ~scope:Varname.Function
-      env
-      kf
-      t_opt
-      (Cil.typeOf e)
-      (fun _ _ -> [])
-  in
-  let env_ref = ref new_env in
-  (* visitor modifying in place the labeled statement in order to store [e]
-     in the resulting variable at this location (which is the only correct
-     one). *)
-  let o = object
-    inherit Visitor.frama_c_inplace
-    method !vstmt_aux stmt =
-      (* either a standard C affectation or a call to an initializer according
-         to the type of [e] *)
-      let ty = Cil.typeOf e in
-      let init_set =
-        if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
-      in
-      let new_stmt = init_set ~loc (Cil.var res_v) res e in
-      assert (!env_ref == new_env);
-      (* generate the new block of code for the labeled statement and the
-         corresponding environment *)
-      let block, new_env =
-        Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
-      in
-      env_ref := Env.extend_stmt_in_place new_env stmt ~label block;
-      Cil.ChangeTo stmt
-  end
-  in
-  ignore (Visitor.visitFramacStmt o stmt);
-  res, !env_ref, Typed_number.C_number
-
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/src/code_generator/translate_utils.mli

@@ -96,17 +96,6 @@ val env_of_li:
 (** [env_of_li ~adata ~loc kf env li] translates the logic info [li] in the
     given environment with the given assertion context. *)
 
-val at_to_exp_no_lscope:
-  kernel_function ->
-  Env.t ->
-  term option ->
-  logic_label ->
-  exp ->
-  exp * Env.t * Typed_number.strnum
-(** [at_to_exp_no_lscope kf env t_opt llabel e] generates an expression
-    representing the expression [e] at the label [llabel].
-    [t_opt] is the term representing [\at(e, llabel)]. *)
-
 (**************************************************************************)
 (********************** Forward references ********************************)
 (**************************************************************************)