[eacsl] Use kinstr in env

- Replace `Env.with_rte` and `Env.with_params` to be able to set `rte`
and `kinstr` for an environment;
- Remove `kinstr` parameters from the `Contract` function to use the
`kinstr` of the environment instead;
- Setup environment `kinstr` when injecting code into a statement or
when translating code or function annotation.

Regarding `Translate_annots.pre_funspec` and
`Translate_annots.post_funspec`, since they only translate function
annotations, the `kinstr` is directly set to `Kglobal` in the functions
instead of being taken as a parameter.

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

@@ -315,7 +315,8 @@ let fold_left_handle_error_with_args f (env, acc) l =
 
 (** Insert requires check for the default behavior of the given contract in the
     environment. *)
-let check_default_requires kf kinstr env contract =
+let check_default_requires kf env contract =
+  let kinstr = Env.get_kinstr env in
   let default_behavior =
     Cil.find_default_behavior contract.spec
   in
@@ -337,10 +338,11 @@ let check_default_requires kf kinstr env contract =
 
 (** Insert requires check for the behaviors other than the default behavior of
     the given contract in the environment *)
-let check_other_requires kf kinstr env contract =
+let check_other_requires kf env contract =
   let get_or_create_assumes_var =
     mk_get_or_create_var kf Cil.intType "assumes_value"
   in
+  let kinstr = Env.get_kinstr env in
   let do_behavior env b =
     if Cil.is_default_behavior b then
       env
@@ -440,7 +442,8 @@ type translate_ppt =
 (** For each set of behavior names in [clauses], [check_active_behaviors] counts
     the number of active behaviors and creates assertions for the
     [ppt_to_translate]. *)
-let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env contract clauses =
+let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract clauses =
+  let kinstr = Env.get_kinstr env in
   let loc = contract.location in
   Cil.CurrentLoc.set loc;
   let do_clause env bhvrs =
@@ -563,7 +566,7 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env co
 
 (** Insert complete and disjoint behaviors check for the given contract in the
     environement *)
-let check_complete_and_disjoint kf kinstr env contract =
+let check_complete_and_disjoint kf env contract =
   (* Only translate the complete and disjoint clauses if all the assumes clauses
      could be translated *)
   if contract.all_assumes_translated then
@@ -611,7 +614,6 @@ let check_complete_and_disjoint kf kinstr env contract =
         ~ppt_to_translate
         ~get_or_create_var
         kf
-        kinstr
         env
         contract
         bhvrs
@@ -630,10 +632,11 @@ let check_complete_and_disjoint kf kinstr env contract =
   end
 
 (** Insert ensures check for the given contract in the environement *)
-let check_post_conds kf kinstr env contract =
+let check_post_conds kf env contract =
   let get_or_create_assumes_var =
     mk_get_or_create_var kf Cil.intType "assumes_value"
   in
+  let kinstr = Env.get_kinstr env in
   let do_behavior env b =
     let env =
       Env.handle_error
@@ -763,14 +766,14 @@ let check_post_conds kf kinstr env contract =
     env
     contract.spec.spec_behavior
 
-let translate_preconditions kf kinstr env contract =
+let translate_preconditions kf env contract =
   let env = Env.set_annotation_kind env Smart_stmt.Precondition in
   let env = Env.push_contract env contract in
   let env = init kf env contract in
   (* Start with translating the requires predicate of the default behavior. *)
   let env =
     Env.handle_error
-      (fun env -> check_default_requires kf kinstr env contract)
+      (fun env -> check_default_requires kf env contract)
       env
   in
   (* Then setup the assumes clauses of the contract. *)
@@ -778,17 +781,17 @@ let translate_preconditions kf kinstr env contract =
   (* And finally translate the requires predicates of the rest of the behaviors,
      skipping over the default behavior. *)
   let do_it env =
-    let env = check_other_requires kf kinstr env contract in
-    let env = check_complete_and_disjoint kf kinstr env contract in
+    let env = check_other_requires kf env contract in
+    let env = check_complete_and_disjoint kf env contract in
     env
   in
   Env.handle_error do_it env
 
-let translate_postconditions kf kinstr env =
+let translate_postconditions kf env =
   let env = Env.set_annotation_kind env Smart_stmt.Postcondition in
   let contract, env = Env.pop_and_get_contract env in
   let do_it env =
-    let env = check_post_conds kf kinstr env contract in
+    let env = check_post_conds kf env contract in
     env
   in
   let env = Env.handle_error do_it env in

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

@@ -32,8 +32,8 @@ val create: loc:location -> spec -> t
 (** Create a contract from a [spec] object (either function spec or statement
     spec) *)
 
-val translate_preconditions: kernel_function -> kinstr -> Env.t -> t -> Env.t
+val translate_preconditions: kernel_function -> Env.t -> t -> Env.t
 (** Translate the preconditions of the given contract into the environement *)
 
-val translate_postconditions: kernel_function -> kinstr -> Env.t -> Env.t
+val translate_postconditions: kernel_function -> Env.t -> Env.t
 (** Translate the postconditions of the given contract into the environment *)

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

@@ -171,20 +171,6 @@ let generate_rte env =
   let local_env, _ = top env in
   local_env.rte
 
-let with_rte ~f env rte_value =
-  let old_rte_value = generate_rte env in
-  let env = set_rte env rte_value in
-  let env = f env in
-  let env = set_rte env old_rte_value in
-  env
-
-let with_rte_and_result ~f env rte_value =
-  let old_rte_value = generate_rte env in
-  let env = set_rte env rte_value in
-  let other, env = f env in
-  let env = set_rte env old_rte_value in
-  other, env
-
 (* ************************************************************************** *)
 (** {2 Kinstr} *)
 (* ************************************************************************** *)
@@ -605,6 +591,41 @@ let pop_contract env =
   let _, env = pop_and_get_contract env in
   env
 
+(* ************************************************************************** *)
+(** {2 Utilities} *)
+(* ************************************************************************** *)
+
+let with_params_and_result ?rte ?kinstr ~f env =
+  let old_rte, env =
+    match rte with
+    | Some rte ->
+      Some (generate_rte env), set_rte env rte
+    | None -> None, env
+  in
+  let old_kinstr, env =
+    match kinstr with
+    | Some kinstr ->
+      Some (get_kinstr env), set_kinstr env kinstr
+    | None -> None, env
+  in
+  let other, env = f env in
+  let env =
+    match old_kinstr with
+    | Some kinstr -> set_kinstr env kinstr
+    | None -> env
+  in
+  let env =
+    match old_rte with
+    | Some rte -> set_rte env rte
+    | None -> env
+  in
+  other, env
+
+let with_params ?rte ?kinstr ~f env =
+  let (), env =
+    with_params_and_result ?rte ?kinstr ~f:(fun env -> (), f env) env
+  in
+  env
 
 (* debugging purpose *)
 let pretty fmt env =

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

@@ -175,22 +175,6 @@ val set_rte: t -> bool -> t
 val generate_rte: t -> bool
 (** Returns the current value of RTE generation for the given environment *)
 
-val with_rte: f:(t -> t) -> t -> bool -> t
-(** [with_rte ~f env x] executes the given closure with RTE generation set to x,
-    and reset RTE generation to its original value afterwards.
-    This function does not handle exceptions at all. The user must handle them
-    either directly in the [f] closure or around the call to the function. *)
-
-val with_rte_and_result: f:(t -> 'a * t) -> t -> bool -> 'a * t
-(** [with_rte_and_result ~f env x] executes the given closure with RTE
-    generation set to x, and reset RTE generation to its original value
-    afterwards. [f] is a closure that takes an environment an returns a pair
-    where the first member is an arbitrary value and the second member is the
-    environment. The function will return the first member of the returned pair
-    of the closure along with the updated environment.
-    This function does not handle exceptions at all. The user must handle them
-    either directly in the [f] closure or around the call to the function. *)
-
 module Local_vars: sig
   val push_new: t -> t
   val add: t -> Typing.number_ty -> t
@@ -243,6 +227,31 @@ val pop_and_get_contract: t -> contract * t
 val pop_contract: t -> t
 (** Pop the top contract of the environment's stack *)
 
+(* ************************************************************************** *)
+(** {2 Utilities} *)
+(* ************************************************************************** *)
+
+val with_params: ?rte:bool -> ?kinstr:kinstr -> f:(t -> t) -> t -> t
+(** [with_params ~rte ~kinstr ~f env] executes the given closure with the given
+    environment after having set RTE generation to [rte] and current kinstr to
+    [kinstr].
+    [f] is a closure that takes an environment and returns an environment.
+    The environment returned by the closure is updated to restore the RTE
+    generation and kinstr attributes to the values of the original environment,
+    then is returned. *)
+
+val with_params_and_result:
+  ?rte:bool -> ?kinstr:kinstr -> f:(t -> 'a * t) -> t -> 'a * t
+(** [with_params_and_result ~rte ~kinstr ~f env] executes the given closure with
+    the given environment after having set RTE generation to [rte] and current
+    kinstr to [kinstr].
+    [f] is a closure that takes an environment and returns a pair where the
+    first member is an arbitrary value and the second member is the environment.
+    The environment returned by the closure is updated to restore the RTE
+    generation and kinstr attributes to the values of the original environment,
+    then the function returns the arbitrary value returned by the closure along
+    with the updated environment. *)
+
 val pretty: Format.formatter -> t -> unit
 
 (*

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

@@ -268,7 +268,7 @@ let add_new_block_in_stmt env kf stmt =
           let env = mk_post_env env stmt in
           (* also handle the postcondition of the function and clear the
              env *)
-          Translate_annots.post_funspec kf Kglobal env
+          Translate_annots.post_funspec kf env
         else
           env
       in
@@ -451,6 +451,7 @@ and inject_in_stmt env kf stmt =
     | Loop _ -> Env.push_loop env
     | _ -> env
   in
+  let env = Env.set_kinstr env (Kstmt stmt) in
   (* initial environment *)
   let env =
     if Kernel_function.is_first_stmt kf stmt then
@@ -466,7 +467,7 @@ and inject_in_stmt env kf stmt =
       (* translate the precondition of the function *)
       if Functions.check kf then
         let funspec = Annotations.funspec kf in
-        Translate_annots.pre_funspec kf Kglobal env funspec
+        Translate_annots.pre_funspec kf env funspec
       else env
     else
       env

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

@@ -144,10 +144,12 @@ let call ~adata ~loc kf name ctx env t =
   assert (name = "base_addr" || name = "block_length"
           || name = "offset" || name ="freeable");
   let (e, adata), env =
-    Env.with_rte_and_result env true
+    Env.with_params_and_result
+      ~rte:true
       ~f:(fun env ->
           let e, adata, env = !term_to_exp_ref ~adata kf env t in
           (e, adata), env)
+      env
   in
   let e, env =
     Env.rtl_call_to_new_var
@@ -219,10 +221,12 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
     ~lenv:(Env.Local_vars.get env)
     ptr;
   let (ptr, adata), env =
-    Env.with_rte_and_result env true
+    Env.with_params_and_result
+      ~rte:true
       ~f:(fun env ->
           let e, adata, env = !term_to_exp_ref ~adata kf env ptr in
           (e, adata), env)
+      env
   in
   (* size *)
   let size_term =
@@ -296,10 +300,12 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
    [p] is the predicate under test. *)
 let term_to_ptr_and_size ~adata ~loc kf env t =
   let (e, adata), env =
-    Env.with_rte_and_result env true
+    Env.with_params_and_result
+      ~rte:true
       ~f:(fun env ->
           let e, adata, env = !term_to_exp_ref ~adata kf env t in
           (e, adata), env)
+      env
   in
   let ty = Misc.cty t.term_type in
   let sizeof = Smart_exp.ptr_sizeof ~loc ty in

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

@@ -28,7 +28,8 @@ open Cil_datatype
    statements (if any) for runtime assertion checking. *)
 (* ************************************************************************** *)
 
-let pre_funspec kf kinstr env funspec =
+let pre_funspec kf env funspec =
+  let kinstr = Kglobal in
   let unsupported f x = ignore (Env.handle_error (fun env -> f x; env) env) in
   let convert_unsupported_clauses env =
     unsupported
@@ -50,14 +51,21 @@ let pre_funspec kf kinstr env funspec =
   Cil.CurrentLoc.set loc;
   let env = convert_unsupported_clauses env in
   let contract = Contract.create ~loc funspec in
-  Env.with_rte env true
-    ~f:(fun env -> Contract.translate_preconditions kf kinstr env contract)
+  Env.with_params
+    ~rte:true
+    ~kinstr
+    ~f:(fun env -> Contract.translate_preconditions kf env contract)
+    env
 
-let post_funspec kf kinstr env =
-  Env.with_rte env true
-    ~f:(fun env -> Contract.translate_postconditions kf kinstr env)
+let post_funspec kf env =
+  Env.with_params
+    ~rte:true
+    ~kinstr:Kglobal
+    ~f:(fun env -> Contract.translate_postconditions kf env)
+    env
 
 let pre_code_annotation kf stmt env annot =
+  let kinstr = Kstmt stmt in
   let convert env = match annot.annot_content with
     | AAssert(l, p) ->
       if Translate_utils.must_translate
@@ -65,8 +73,11 @@ let pre_code_annotation kf stmt env annot =
         let env = Env.set_annotation_kind env Smart_stmt.Assertion in
         if l <> [] then
           Env.not_yet env "@[assertion applied only on some behaviors@]";
-        Env.with_rte env true
+        Env.with_params
+          ~rte:true
+          ~kinstr
           ~f:(fun env -> Translate_predicates.do_it kf env p)
+          env
       else
         env
     | AStmtSpec(l, spec) ->
@@ -74,9 +85,11 @@ let pre_code_annotation kf stmt env annot =
         Env.not_yet env "@[statement contract applied only on some behaviors@]";
       let loc = Stmt.loc stmt in
       let contract = Contract.create ~loc spec in
-      Env.with_rte env true
-        ~f:(fun env ->
-            Contract.translate_preconditions kf (Kstmt stmt) env contract)
+      Env.with_params
+        ~rte:true
+        ~kinstr
+        ~f:(fun env -> Contract.translate_preconditions kf env contract)
+        env
     | AInvariant(l, loop_invariant, p) ->
       if Translate_utils.must_translate
           (Property.ip_of_code_annot_single kf stmt annot) then
@@ -84,8 +97,11 @@ let pre_code_annotation kf stmt env annot =
         if l <> [] then
           Env.not_yet env "@[invariant applied only on some behaviors@]";
         let env =
-          Env.with_rte env true
+          Env.with_params
+            ~rte:true
+            ~kinstr
             ~f:(fun env -> Translate_predicates.do_it kf env p)
+            env
         in
         if loop_invariant then
           Env.add_loop_invariant env p
@@ -121,10 +137,14 @@ let pre_code_annotation kf stmt env annot =
   Env.handle_error convert env
 
 let post_code_annotation kf stmt env annot =
+  let kinstr = Kstmt stmt in
   let convert env = match annot.annot_content with
     | AStmtSpec(_, _) ->
-      Env.with_rte env true
-        ~f:(fun env -> Contract.translate_postconditions kf (Kstmt stmt) env)
+      Env.with_params
+        ~rte:true
+        ~kinstr
+        ~f:(fun env -> Contract.translate_postconditions kf env)
+        env
     | AAssert _
     | AInvariant _
     | AVariant _

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

@@ -26,7 +26,7 @@ open Cil_types
     statements (if any) for runtime assertion checking. These C statements are
     part of the resulting environment. *)
 
-val pre_funspec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
+val pre_funspec: kernel_function -> Env.t -> funspec -> Env.t
 (** Translate the preconditions of the given function contract in the
     environment. The contract is attached to the kernel_function.
 
@@ -34,7 +34,7 @@ val pre_funspec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
     taken to call {!post_funspec} at the right time to pop the right
     contract. *)
 
-val post_funspec: kernel_function -> kinstr -> Env.t -> Env.t
+val post_funspec: kernel_function -> Env.t -> Env.t
 (** Translate the postconditions of the current function contract in the
     environment.
 

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

@@ -100,7 +100,8 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
   | Pand(p1, p2) ->
     (* p1 && p2 <==> if p1 then p2 else false *)
     Extlib.flatten
-      (Env.with_rte_and_result env true
+      (Env.with_params_and_result
+         ~rte:true
          ~f:(fun env ->
              let e1, adata, env1 = to_exp ~adata kf env p1 in
              let e2, adata, env2 =
@@ -118,11 +119,13 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
                   e1
                   res2
                   (Cil.zero loc, env3))
-           ))
+           )
+         env)
   | Por(p1, p2) ->
     (* p1 || p2 <==> if p1 then true else p2 *)
     Extlib.flatten
-      (Env.with_rte_and_result env true
+      (Env.with_params_and_result
+         ~rte:true
          ~f:(fun env ->
              let e1, adata, env1 = to_exp ~adata kf env p1 in
              let env' = Env.push env1 in
@@ -141,7 +144,8 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
                   e1
                   (Cil.one loc, env')
                   res2)
-           ))
+           )
+         env)
   | Pxor _ -> Env.not_yet env "xor"
   | Pimplies(p1, p2) ->
     (* (p1 ==> p2) <==> !p1 || p2 *)
@@ -166,7 +170,8 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
     Smart_exp.lnot ~loc e, adata, env
   | Pif(t, p2, p3) ->
     Extlib.flatten
-      (Env.with_rte_and_result env true
+      (Env.with_params_and_result
+         ~rte:true
          ~f:(fun env ->
              let e1, adata, env1 = Translate_terms.to_exp ~adata kf env t in
              let e2, adata, env2 =
@@ -179,7 +184,8 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
              Extlib.nest
                adata
                (Translate_utils.conditional_to_exp ~loc kf None e1 res2 res3)
-           ))
+           )
+         env)
   | Plet(li, p) ->
     let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
     let env = Env.Logic_scope.extend env lvs in
@@ -304,7 +310,8 @@ and to_exp ~adata ?name kf ?rte env p =
   | PoT_pred p ->
     let rte = match rte with None -> Env.generate_rte env | Some b -> b in
     Extlib.flatten
-      (Env.with_rte_and_result env false
+      (Env.with_params_and_result
+         ~rte:false
          ~f:(fun env ->
              let e, adata, env =
                predicate_content_to_exp ~adata ?name kf env p
@@ -326,7 +333,8 @@ and to_exp ~adata ?name kf ?rte env p =
                   Typed_number.C_number
                   None
                   e)
-           ))
+           )
+         env)
 
 let generalized_untyped_to_exp ~adata ?name kf ?rte env p =
   (* If [rte] is true, it means we're translating the root predicate of an

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

@@ -41,8 +41,10 @@ let rte_annots pp elt kf env l =
                 let lscope_reset_old = Env.Logic_scope.get_reset env in
                 let env = Env.Logic_scope.set_reset env false in
                 let env =
-                  Env.with_rte env false
+                  Env.with_params
+                    ~rte:false
                     ~f:(fun env -> Translate_predicates.do_it kf env p)
+                    env
                 in
                 let env = Env.Logic_scope.set_reset env lscope_reset_old in
                 env)

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

@@ -641,7 +641,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
     (* t1 || t2 <==> if t1 then true else t2 *)
     let e, adata, env =
       Extlib.flatten
-        (Env.with_rte_and_result env true
+        (Env.with_params_and_result
+           ~rte:true
            ~f:(fun env ->
                let e1, adata, env1 = to_exp ~adata kf env t1 in
                let env' = Env.push env1 in
@@ -653,14 +654,16 @@ and context_insensitive_term_to_exp ~adata kf env t =
                  adata
                  (Translate_utils.conditional_to_exp
                     ~name:"or" ~loc kf (Some t) e1 (Cil.one loc, env') res2)
-             ))
+             )
+           env)
     in
     e, adata, env, Typed_number.C_number, ""
   | TBinOp(LAnd, t1, t2) ->
     (* t1 && t2 <==> if t1 then t2 else false *)
     let e, adata, env =
       Extlib.flatten
-        (Env.with_rte_and_result env true
+        (Env.with_params_and_result
+           ~rte:true
            ~f:(fun env ->
                let e1, adata, env1 = to_exp ~adata kf env t1 in
                let e2, adata, env2 =
@@ -672,7 +675,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
                  adata
                  (Translate_utils.conditional_to_exp
                     ~name:"and" ~loc kf (Some t) e1 res2 (Cil.zero loc, env3))
-             ))
+             )
+           env)
     in
     e, adata, env, Typed_number.C_number, ""
   | TBinOp((BOr | BXor | BAnd) as bop, t1, t2) ->
@@ -770,7 +774,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
   | Tif(t1, t2, t3) ->
     let e, adata, env =
       Extlib.flatten
-        (Env.with_rte_and_result env true
+        (Env.with_params_and_result
+           ~rte:true
            ~f:(fun env ->
                let e1, adata, env1 = to_exp ~adata kf env t1 in
                let e2, adata, env2 =
@@ -790,7 +795,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
                     e1
                     res2
                     res3)
-             ))
+             )
+           env)
     in
     e, adata, env, Typed_number.C_number, ""
   | Tat(t, BuiltinLabel Here) ->
@@ -873,7 +879,8 @@ and to_exp ~adata kf env t =
     (Env.Local_vars.get env);
   let t = Logic_normalizer.get_term t in
   Extlib.flatten
-    (Env.with_rte_and_result env false
+    (Env.with_params_and_result
+       ~rte:false
        ~f:(fun env ->
            let e, adata, env, sty, name =
              context_insensitive_term_to_exp ~adata kf env t
@@ -894,7 +901,8 @@ and to_exp ~adata kf env t =
                 sty
                 (Some t)
                 e)
-         ))
+         )
+       env)
 
 let () =
   Translate_utils.term_to_exp_ref := to_exp;