From 5f2db26878ad47f97710634ee4b9ca775fe0af67 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 22 Sep 2020 10:32:31 +0200
Subject: [PATCH] [eacsl:codegen] Update translation to use the `Contract`
---
src/plugins/e-acsl/Makefile.in | 1 +
src/plugins/e-acsl/headers/header_spec.txt | 2 +
.../e-acsl/src/code_generator/injector.ml | 8 +-
.../e-acsl/src/code_generator/translate.ml | 210 ------------------
.../src/code_generator/translate_annots.ml | 145 ++++++++++++
.../src/code_generator/translate_annots.mli | 77 +++++++
6 files changed, 229 insertions(+), 214 deletions(-)
create mode 100644 src/plugins/e-acsl/src/code_generator/translate_annots.ml
create mode 100644 src/plugins/e-acsl/src/code_generator/translate_annots.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index f7b3af2154a..65408186eef 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -87,6 +87,7 @@ SRC_CODE_GENERATOR:= \
logic_array \
translate \
contract \
+ translate_annots \
temporal \
memory_observer \
literal_observer \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index ac18901b534..cf2b2a13c0e 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index cac63d6330a..75ec65a7b49 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 0d42015860e..81b165d36f9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/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 ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
new file mode 100644
index 00000000000..a65ac3567b9
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -0,0 +1,145 @@
+(**************************************************************************)
+(* *)
+(* 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:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.mli b/src/plugins/e-acsl/src/code_generator/translate_annots.mli
new file mode 100644
index 00000000000..8e4504b2ddf
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.mli
@@ -0,0 +1,77 @@
+(**************************************************************************)
+(* *)
+(* 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:
+*)
--
GitLab