[eacsl:codegen] Update translation to use the `Contract`

src/plugins/e-acsl/Makefile.in

@@ -87,6 +87,7 @@ SRC_CODE_GENERATOR:= \
 	logic_array \
 	translate \
 	contract \
+	translate_annots \
 	temporal \
 	memory_observer \
 	literal_observer \

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

@@ -119,6 +119,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.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate.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/dependencies/dep_eva.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/dependencies/dep_eva.enabled.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/dependencies/dep_eva.disabled.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL

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

@@ -232,7 +232,7 @@ let add_new_block_in_stmt env kf stmt =
   in
   let mk_post_env env stmt =
     Annotations.fold_code_annot
-      (fun _ a env -> Translate.translate_post_code_annotation kf stmt env a)
+      (fun _ a env -> Translate_annots.post_code_annotation kf stmt env a)
       stmt
       env
   in
@@ -252,7 +252,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.translate_post_spec kf Kglobal env (Annotations.funspec kf)
+          Translate_annots.post_funspec kf Kglobal env
         else
           env
       in
@@ -450,7 +450,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.translate_pre_spec kf Kglobal env funspec
+        Translate_annots.pre_funspec kf Kglobal env funspec
       else env
     else
       env
@@ -459,7 +459,7 @@ and inject_in_stmt env kf stmt =
   let env =
     if Functions.check kf then
       Annotations.fold_code_annot
-        (fun _ a env -> Translate.translate_pre_code_annotation kf stmt env a)
+        (fun _ a env -> Translate_annots.pre_code_annotation kf stmt env a)
         stmt
         env
     else

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

@@ -1147,216 +1147,6 @@ let untyped_term_to_exp typ t =
   if not (Env.has_no_new_stmt env) then raise (No_simple_term_translation t);
   e
 
-(* ************************************************************************** *)
-(* [translate_*] translates a given ACSL annotation into the corresponding C
-   statement (if any) for runtime assertion checking. *)
-(* ************************************************************************** *)
-
-let must_translate ppt =
-  Options.Valid.get ()
-  || match Property_status.get ppt with
-  | Never_tried
-  | Inconsistent _
-  | Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
-    true
-  | Best (True, _) ->
-    (* [TODO] generating code for "valid under hypotheses" properties could be
-       useful for some use cases (in particular, when E-ACSL does not stop on
-       the very first error).
-       ==> introduce a new option or modify the behavior of -e-acsl-valid,
-       see e-acsl#35 *)
-    false
-
-let must_translate_opt = function
-  | None -> false
-  | Some ppt -> must_translate ppt
-
-let assumes_predicate bhv =
-  List.fold_left
-    (fun acc p ->
-       let pred = p.ip_content.tp_statement in
-       let loc = pred.pred_loc in
-       Logic_const.pand ~loc
-         (acc,
-          Logic_const.unamed ~loc pred.pred_content))
-    Logic_const.ptrue
-    bhv.b_assumes
-
-let translate_preconditions kf kinstr env behaviors =
-  let env = Env.set_annotation_kind env Smart_stmt.Precondition in
-  let do_behavior env b =
-    let assumes_pred = assumes_predicate b in
-    List.fold_left
-      (fun env p ->
-         let pred = p.ip_content.tp_statement in
-         let do_it env =
-           if must_translate (Property.ip_of_requires kf kinstr b p) then
-             let loc = pred.pred_loc in
-             let p =
-               Logic_const.pimplies
-                 ~loc
-                 (assumes_pred,
-                  Logic_const.unamed ~loc pred.pred_content)
-             in
-             translate_named_predicate kf env p
-           else
-             env
-         in
-         handle_error do_it env)
-      env
-      b.b_requires
-  in
-  List.fold_left do_behavior env behaviors
-
-let translate_postconditions kf kinstr env behaviors =
-  let env = Env.set_annotation_kind env Smart_stmt.Postcondition in
-  (* generate one guard by postcondition of each behavior *)
-  let do_behavior env b =
-    let env =
-      handle_error
-        (fun env ->
-           let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
-           let ppt = Property.ip_assigns_of_behavior kf kinstr ~active b in
-           if b.b_assigns <> WritesAny && must_translate_opt ppt
-           then not_yet env "assigns clause in behavior";
-           (* ignore b.b_extended since we never translate them *)
-           env)
-        env
-    in
-    let assumes_pred = assumes_predicate b in
-    List.fold_left
-      (fun env ((t, p) as tp) ->
-         if must_translate (Property.ip_of_ensures kf kinstr b tp) then
-           let do_it env =
-             match t with
-             | Normal ->
-               let p = p.ip_content.tp_statement in
-               let loc = p.pred_loc in
-               let p =
-                 Logic_const.pimplies
-                   ~loc
-                   (Logic_const.pold ~loc assumes_pred,
-                    Logic_const.unamed ~loc p.pred_content)
-               in
-               translate_named_predicate kf env p
-             | Exits | Breaks | Continues | Returns ->
-               not_yet env "abnormal termination case in behavior"
-           in
-           handle_error do_it env
-         else env)
-      env
-      b.b_post_cond
-  in
-  (* fix ordering of behaviors' iterations *)
-  let bhvs =
-    List.sort (fun b1 b2 -> String.compare b1.b_name b2.b_name) behaviors
-  in
-  List.fold_left do_behavior env bhvs
-
-let translate_pre_spec kf kinstr env spec =
-  let unsupported f x = ignore (handle_error (fun env -> f x; env) env) in
-  let convert_unsupported_clauses env =
-    unsupported
-      (fun spec ->
-         let ppt = Property.ip_decreases_of_spec kf kinstr spec in
-         if must_translate_opt ppt then not_yet env "variant clause")
-      spec;
-    (* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
-    unsupported
-      (fun spec ->
-         let ppt = Property.ip_terminates_of_spec kf kinstr spec in
-         if must_translate_opt ppt then not_yet env "terminates clause")
-      spec;
-    let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
-    let ppts = Property.ip_complete_of_spec kf kinstr ~active spec in
-    unsupported
-      (fun ppts ->
-         List.iter
-           (fun ppt ->
-              if must_translate ppt then not_yet env "complete behaviors")
-           ppts)
-      ppts;
-    let ppts = Property.ip_disjoint_of_spec kf kinstr ~active spec in
-    unsupported
-      (fun ppts ->
-         List.iter
-           (fun ppt ->
-              if must_translate ppt then not_yet env "disjoint behaviors")
-           ppts)
-      ppts;
-    env
-  in
-  let env = convert_unsupported_clauses env in
-  handle_error
-    (fun env -> translate_preconditions kf kinstr env spec.spec_behavior)
-    env
-
-let translate_post_spec kf kinstr env spec =
-  handle_error
-    (fun env -> translate_postconditions kf kinstr env spec.spec_behavior)
-    env
-
-let translate_pre_code_annotation kf stmt env annot =
-  let convert env = match annot.annot_content with
-    | AAssert(l, p) ->
-      if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
-        let env = Env.set_annotation_kind env Smart_stmt.Assertion in
-        if l <> [] then
-          not_yet env "@[assertion applied only on some behaviors@]";
-        translate_named_predicate kf env p.tp_statement
-      else
-        env
-    | AStmtSpec(l, spec) ->
-      if l <> [] then
-        not_yet env "@[statement contract applied only on some behaviors@]";
-      translate_pre_spec kf (Kstmt stmt) env spec ;
-    | AInvariant(l, loop_invariant, p) ->
-      if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
-        let env = Env.set_annotation_kind env Smart_stmt.Invariant in
-        if l <> [] then
-          not_yet env "@[invariant applied only on some behaviors@]";
-        let env = translate_named_predicate kf env p.tp_statement in
-        if loop_invariant then
-          Env.add_loop_invariant env p.tp_statement
-        else env
-      else
-        env
-    | AVariant _ ->
-      if must_translate (Property.ip_of_code_annot_single kf stmt annot)
-      then not_yet env "variant"
-      else env
-    | AAssigns _ ->
-      (* TODO: it is not a precondition --> should not be handled here,
-         to be fixed when implementing e-acsl#29 *)
-      let ppts = Property.ip_of_code_annot kf stmt annot in
-      List.iter
-        (fun ppt -> if must_translate ppt then not_yet env "assigns")
-        ppts;
-      env
-    | AAllocation _ ->
-      let ppts = Property.ip_of_code_annot kf stmt annot in
-      List.iter
-        (fun ppt -> if must_translate ppt then not_yet env "allocation")
-        ppts;
-      env
-    | APragma _ -> not_yet env "pragma"
-    | AExtended _ -> env (* never translate extensions. *)
-  in
-  handle_error convert env
-
-let translate_post_code_annotation kf stmt env annot =
-  let convert env = match annot.annot_content with
-    | AStmtSpec(_, spec) -> translate_post_spec kf (Kstmt stmt) env spec
-    | AAssert _
-    | AInvariant _
-    | AVariant _
-    | AAssigns _
-    | AAllocation _
-    | APragma _
-    | AExtended _ -> env
-  in
-  handle_error convert env
-
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    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
+open Cil_datatype
+
+(* ************************************************************************** *)
+(* Functions that translate a given ACSL annotation into the corresponding C
+   statements (if any) for runtime assertion checking. *)
+(* ************************************************************************** *)
+
+let must_translate ppt =
+  Options.Valid.get ()
+  || match Property_status.get ppt with
+  | Never_tried
+  | Inconsistent _
+  | Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
+    true
+  | Best (True, _) ->
+    (* [TODO] generating code for "valid under hypotheses" properties could be
+       useful for some use cases (in particular, when E-ACSL does not stop on
+       the very first error).
+       ==> introduce a new option or modify the behavior of -e-acsl-valid,
+       see e-acsl#35 *)
+    false
+
+let must_translate_opt = function
+  | None -> false
+  | Some ppt -> must_translate ppt
+
+let () =
+  Contract.must_translate_ppt_ref := must_translate;
+  Contract.must_translate_ppt_opt_ref := must_translate_opt
+
+let pre_funspec kf kinstr env funspec =
+  let unsupported f x = ignore (Env.handle_error (fun env -> f x; env) env) in
+  let convert_unsupported_clauses env =
+    unsupported
+      (fun spec ->
+         let ppt = Property.ip_decreases_of_spec kf kinstr spec in
+         if must_translate_opt ppt then Env.not_yet env "variant clause")
+      funspec;
+    (* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
+    unsupported
+      (fun spec ->
+         let ppt = Property.ip_terminates_of_spec kf kinstr spec in
+         if must_translate_opt ppt then Env.not_yet env "terminates clause")
+      funspec;
+    env
+  in
+  let env = convert_unsupported_clauses env in
+  let loc = Kernel_function.get_location kf in
+  let contract = Contract.create ~loc funspec in
+  Contract.translate_preconditions kf kinstr env contract
+
+let post_funspec kf kinstr env =
+  Contract.translate_postconditions kf kinstr env
+
+let pre_code_annotation kf stmt env annot =
+  let convert env = match annot.annot_content with
+    | AAssert(l, p) ->
+      if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
+        let env = Env.set_annotation_kind env Smart_stmt.Assertion in
+        if l <> [] then
+          Env.not_yet env "@[assertion applied only on some behaviors@]";
+        Translate.translate_predicate kf env p.tp_statement
+      else
+        env
+    | AStmtSpec(l, spec) ->
+      if l <> [] then
+        Env.not_yet env "@[statement contract applied only on some behaviors@]";
+      let loc = Stmt.loc stmt in
+      let contract = Contract.create ~loc spec in
+      Contract.translate_preconditions kf (Kstmt stmt) env contract
+    | AInvariant(l, loop_invariant, p) ->
+      if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
+        let env = Env.set_annotation_kind env Smart_stmt.Invariant in
+        if l <> [] then
+          Env.not_yet env "@[invariant applied only on some behaviors@]";
+        let env = Translate.translate_predicate kf env p.tp_statement in
+        if loop_invariant then
+          Env.add_loop_invariant env p.tp_statement
+        else env
+      else
+        env
+    | AVariant _ ->
+      if must_translate (Property.ip_of_code_annot_single kf stmt annot)
+      then Env.not_yet env "variant"
+      else env
+    | AAssigns _ ->
+      (* TODO: it is not a precondition --> should not be handled here,
+         to be fixed when implementing e-acsl#29 *)
+      let ppts = Property.ip_of_code_annot kf stmt annot in
+      List.iter
+        (fun ppt -> if must_translate ppt then Env.not_yet env "assigns")
+        ppts;
+      env
+    | AAllocation _ ->
+      let ppts = Property.ip_of_code_annot kf stmt annot in
+      List.iter
+        (fun ppt -> if must_translate ppt then Env.not_yet env "allocation")
+        ppts;
+      env
+    | APragma _ -> Env.not_yet env "pragma"
+    | AExtended _ -> env (* never translate extensions. *)
+  in
+  Env.handle_error convert env
+
+let post_code_annotation kf stmt env annot =
+  let convert env = match annot.annot_content with
+    | AStmtSpec(_, _) -> Contract.translate_postconditions kf (Kstmt stmt) env
+    | AAssert _
+    | AInvariant _
+    | AVariant _
+    | AAssigns _
+    | AAllocation _
+    | APragma _
+    | AExtended _ -> env
+  in
+  Env.handle_error convert env
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)

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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    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
+
+(** Functions that translate a given ACSL annotation into the corresponding C
+    statements (if any) for runtime assertion checking. These C statements are
+    part of the resulting environment. *)
+
+val must_translate: Property.t -> bool
+(** Return true if the given property must be translated (ie. if the valid
+    properties must be translated or if its status is not [True]), false
+    otherwise. *)
+
+val must_translate_opt: Property.t option -> bool
+(** Same than [must_translate] but for [Property.t option]. Return false if the
+    option is [None]. *)
+
+val pre_funspec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
+(** Translate the preconditions of the given function contract in the
+    environment. The contract is attached to the kernel_function.
+
+    The function contract is pushed in the environment, some care should be
+    taken to call {!post_funspec} at the right time to pop the right
+    contract. *)
+
+val post_funspec: kernel_function -> kinstr -> Env.t -> Env.t
+(** Translate the postconditions of the current function contract in the
+    environment.
+
+    The function contract previously built by {!pre_funspec} is popped
+    from the environment. Some care should be taken to call this function at
+    the right time to pop the right contract. *)
+
+val pre_code_annotation:
+  kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
+(** Translate the preconditions of the given code annotation in the
+    environment.
+
+    If available, the statement contract is pushed in the environment, some care
+    should be taken to call {!post_code_annotation} at the right time
+    to pop the right contract. *)
+
+val post_code_annotation:
+  kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
+(** Translate the postconditions of the current code annotation in the
+    environment.
+
+    If necessarry, the statement contract previously built by
+    {!pre_code_annotation} is popped from the environment. Some care
+    should be taken to call this function at the right time to pop the right
+    contract. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)