diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index 813638711ecc5da986c606ddbdba6d24ec7a3420..62c147d84b92c0866338d3397e53b00c342c57d9 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -29,7 +29,7 @@ module Error: sig
exception Not_yet of string
end
-module Translate: sig
+module Translate_terms: sig
exception No_simple_term_translation of term
val untyped_term_to_exp: typ option -> term -> exp
(** @raise Typing_error when the given term cannot be typed (something wrong
@@ -37,7 +37,9 @@ module Translate: sig
@raise Not_yet when the given term contains an unsupported construct.
@raise No_simple_term_translation when the given term cannot be translated
into a single expression. *)
+end
+module Translate_predicates: sig
exception No_simple_predicate_translation of predicate
val untyped_predicate_to_exp: predicate -> exp
(** @raise Typing_error when the given predicate cannot be typed
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e612b3823432ce3b1cdab6e9c6e92d0a14a0af2a..25672c530b45fa6983742a093f233076eb1393e4 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -90,7 +90,10 @@ SRC_CODE_GENERATOR:= \
at_with_lscope \
memory_translate \
logic_array \
- translate \
+ translate_utils \
+ translate_terms \
+ translate_predicates \
+ translate_rtes \
contract \
translate_annots \
temporal \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 506060af0d6c30ca0c8d838b30fd6adbb1c21a62..4c8e1b257363ff9294e43b8253cadbc90388bd94 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -135,10 +135,16 @@ src/code_generator/smart_stmt.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/smart_stmt.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
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/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/code_generator/translate_rtes.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_terms.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_terms.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_utils.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_utils.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/typed_number.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/typed_number.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/libraries/builtins.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 7f300b20d9cfcabe150b5f3000f55a85cd6137c6..1ed15a8d5531a994fad67c17f5a928748b6079ce 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -23,16 +23,6 @@
open Cil_types
open Contract_types
-(**************************************************************************)
-(********************** Forward references ********************************)
-(**************************************************************************)
-
-let must_translate_ppt_ref : (Property.t -> bool) ref =
- Extlib.mk_fun "must_translate_ppt_ref"
-
-let must_translate_ppt_opt_ref : (Property.t option -> bool) ref =
- Extlib.mk_fun "must_translate_ppt_opt_ref"
-
(**************************************************************************)
(********************** Contract ********************************)
(**************************************************************************)
@@ -109,7 +99,7 @@ end = struct
let set_assumes ~loc env kf contract idx assumes =
let idx_e = Cil.integer ~loc idx in
let assumes_e, _, env =
- Translate.generalized_untyped_predicate_to_exp
+ Translate_predicates.generalized_untyped_predicate_to_exp
~adata:Assert.no_data
kf
env
@@ -332,12 +322,12 @@ let check_default_requires kf kinstr env contract =
| Some b ->
fold_left_handle_error
(fun env ip_requires ->
- if !must_translate_ppt_ref
+ if Translate_utils.must_translate
(Property.ip_of_requires kf kinstr b ip_requires) then
let tp_requires = ip_requires.ip_content in
let loc = tp_requires.tp_statement.pred_loc in
Cil.CurrentLoc.set loc;
- Translate.translate_predicate kf env tp_requires
+ Translate_predicates.translate_predicate kf env tp_requires
else
env)
env
@@ -361,7 +351,7 @@ let check_other_requires kf kinstr env contract =
let env, stmts =
fold_left_handle_error_with_args
(fun (env, stmts) ip_requires ->
- if !must_translate_ppt_ref
+ if Translate_utils.must_translate
(Property.ip_of_requires kf kinstr b ip_requires) then
let tp_requires = ip_requires.ip_content in
let pred_kind = tp_requires.tp_kind in
@@ -378,7 +368,7 @@ let check_other_requires kf kinstr env contract =
(* Create runtime check *)
let adata, env = Assert.empty ~loc kf env in
let requires_e, adata, env =
- Translate.generalized_untyped_predicate_to_exp
+ Translate_predicates.generalized_untyped_predicate_to_exp
~adata
kf
env
@@ -450,7 +440,6 @@ type translate_ppt =
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 must_translate = !must_translate_ppt_ref in
let loc = contract.location in
Cil.CurrentLoc.set loc;
let do_clause env bhvrs =
@@ -459,13 +448,13 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env co
let must_translate_complete =
match ppt_to_translate with
| Both | Complete ->
- must_translate (Property.ip_of_complete kf kinstr ~active bhvrs_list)
+ Translate_utils.must_translate (Property.ip_of_complete kf kinstr ~active bhvrs_list)
| Disjoint -> false
in
let must_translate_disjoint =
match ppt_to_translate with
| Both | Disjoint ->
- must_translate (Property.ip_of_disjoint kf kinstr ~active bhvrs_list)
+ Translate_utils.must_translate (Property.ip_of_disjoint kf kinstr ~active bhvrs_list)
| Complete -> false
in
@@ -646,7 +635,7 @@ let check_post_conds kf kinstr env contract =
(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_ppt_opt_ref ppt
+ if b.b_assigns <> WritesAny && Translate_utils.must_translate_opt ppt
then Env.not_yet env "assigns clause in behavior";
(* ignore b.b_extended since we never translate them *)
env)
@@ -655,7 +644,7 @@ let check_post_conds kf kinstr env contract =
if Cil.is_default_behavior b then
fold_left_handle_error
(fun env ((termination, ip_post_cond) as tp) ->
- if !must_translate_ppt_ref
+ if Translate_utils.must_translate
(Property.ip_of_ensures kf kinstr b tp) then
let tp_post_cond = ip_post_cond.ip_content in
let loc = tp_post_cond.tp_statement.pred_loc in
@@ -664,7 +653,7 @@ let check_post_conds kf kinstr env contract =
| Normal ->
(* If translating the default behavior, directly translate the
predicate *)
- Translate.translate_predicate kf env tp_post_cond
+ Translate_predicates.translate_predicate kf env tp_post_cond
| Exits | Breaks | Continues | Returns ->
Error.print_not_yet "abnormal termination case in behavior";
env
@@ -680,7 +669,7 @@ let check_post_conds kf kinstr env contract =
let env, stmts =
fold_left_handle_error_with_args
(fun (env, stmts) ((termination, ip_post_cond) as tp) ->
- if !must_translate_ppt_ref
+ if Translate_utils.must_translate
(Property.ip_of_ensures kf kinstr b tp) then
let tp_post_cond = ip_post_cond.ip_content in
let pred_kind = tp_post_cond.tp_kind in
@@ -702,7 +691,7 @@ let check_post_conds kf kinstr env contract =
(* Create runtime check *)
let adata, env = Assert.empty ~loc kf env in
let post_cond_e, adata, env =
- Translate.generalized_untyped_predicate_to_exp
+ Translate_predicates.generalized_untyped_predicate_to_exp
~adata
kf
env
diff --git a/src/plugins/e-acsl/src/code_generator/contract.mli b/src/plugins/e-acsl/src/code_generator/contract.mli
index df12966e4ec39959efff34f9be6c204db020e27b..d9db3d14ae98b26aabfa28db85446595b90912c8 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.mli
+++ b/src/plugins/e-acsl/src/code_generator/contract.mli
@@ -37,11 +37,3 @@ val translate_preconditions: kernel_function -> kinstr -> Env.t -> t -> Env.t
val translate_postconditions: kernel_function -> kinstr -> Env.t -> Env.t
(** Translate the postconditions of the given contract into the environment *)
-
-(**************************************************************************)
-(********************** Forward references ********************************)
-(**************************************************************************)
-
-val must_translate_ppt_ref: (Property.t -> bool) ref
-
-val must_translate_ppt_opt_ref: (Property.t option -> bool) ref
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index e564026ed9b2e53a47dd788c793b5e9eb13efe38..1a953ebb8fe88f7f6869e5062ff5b22d3dd2162a 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -215,7 +215,7 @@ let add_new_block_in_stmt env kf stmt =
List.iter
(Typing.preprocess_rte ~lenv:(Env.Local_vars.get env))
rtes;
- Translate.translate_rte_annots Printer.pp_stmt stmt kf env rtes
+ Translate_rtes.translate_rte_annots Printer.pp_stmt stmt kf env rtes
end else
env
in
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index c048c5cd1ba2fa62b50cace5520ac1600abdd8ca..5c1a5f60c8e6e3d349fa0aa8c636b475aae37461 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -191,7 +191,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
| Typing.Gmpz ->
let e, _, env =
- Translate.gmp_to_sizet
+ Translate_utils.gmp_to_sizet
~adata:Assert.no_data
~loc
~name
@@ -203,7 +203,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
e, env
| Typing.(C_integer _ | C_float _) as nty ->
(* We know that [t] can be translated to a C type, so we start with that *)
- let e, _, env = Translate.term_to_exp ~adata:Assert.no_data kf env t in
+ let e, _, env = Translate_terms.term_to_exp ~adata:Assert.no_data kf env t in
(* Then we can check if the expression will fit in a [size_t] *)
let sizet = Cil.(theMachine.typeOfSizeOf) in
let sizet_kind = Cil.(theMachine.kindOfSizeOf) in
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 4e331d96729e361527c2da395a4307b189b992bf..2a5e0a68adecde5556a6eee78f339655f409245d 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -23,7 +23,7 @@
open Cil_types
open Cil
-(** Forward reference for [Translate.predicate_to_exp]. *)
+(** Forward reference for [Translate_predicates.to_exp]. *)
let predicate_to_exp_ref
: (adata:Assert.t ->
kernel_function ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index f83509dfe9708e7841fd87d643bed55c4b73e585..3b88b8ccdd46375e72525393afb15213d10fce68 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -28,42 +28,19 @@ open Cil_datatype
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 "decreases clause")
+ if Translate_utils.must_translate_opt ppt then Env.not_yet env "decreases 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")
+ if Translate_utils.must_translate_opt ppt then Env.not_yet env "terminates clause")
funspec;
env
in
@@ -81,12 +58,12 @@ let post_funspec 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
+ if Translate_utils.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@]";
Env.with_rte env true
- ~f:(fun env -> Translate.translate_predicate kf env p)
+ ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
else
env
| AStmtSpec(l, spec) ->
@@ -98,13 +75,13 @@ let pre_code_annotation kf stmt env annot =
~f:(fun env ->
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
+ if Translate_utils.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 =
Env.with_rte env true
- ~f:(fun env -> Translate.translate_predicate kf env p)
+ ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
in
if loop_invariant then
Env.add_loop_invariant env p
@@ -112,7 +89,7 @@ let pre_code_annotation kf stmt env annot =
else
env
| AVariant (t, measure) ->
- if must_translate (Property.ip_of_code_annot_single kf stmt annot)
+ if Translate_utils.must_translate (Property.ip_of_code_annot_single kf stmt annot)
then Env.set_loop_variant env ?measure t
else env
| AAssigns _ ->
@@ -120,13 +97,13 @@ let pre_code_annotation kf stmt env annot =
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")
+ (fun ppt -> if Translate_utils.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")
+ (fun ppt -> if Translate_utils.must_translate ppt then Env.not_yet env "allocation")
ppts;
env
| APragma _ -> Env.not_yet env "pragma"
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.mli b/src/plugins/e-acsl/src/code_generator/translate_annots.mli
index 7fcd0651c9f1345bc10e9507b46de26fcd3ee633..3c5669a3f974b29795a5de18093a8cbacf95a12b 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.mli
@@ -26,15 +26,6 @@ open Cil_types
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.
@@ -72,6 +63,6 @@ val post_code_annotation:
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f0616ff49528e58e49342092f81aa1771c223588
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -0,0 +1,395 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Generate C implementations of E-ACSL predicates. *)
+
+open Cil_types
+open Cil_datatype
+let dkey = Options.dkey_translation
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let translate_rte_annots_ref
+ : ((Format.formatter -> code_annotation -> unit) ->
+ code_annotation ->
+ kernel_function ->
+ Env.t ->
+ code_annotation list ->
+ Env.t) ref
+ =
+ ref (fun _pp _elt _kf _env _l ->
+ Extlib.mk_labeled_fun "translate_rte_annots_ref")
+
+let translate_rte_exp_ref
+ : (?filter:(code_annotation -> bool) ->
+ kernel_function ->
+ Env.t ->
+ exp ->
+ Env.t) ref
+ =
+ ref (fun ?filter:_ _kf _env _e ->
+ Extlib.mk_labeled_fun "translate_rte_exp_ref")
+
+(* ************************************************************************** *)
+(* Transforming predicates into C expressions (if any) *)
+(* ************************************************************************** *)
+
+let relation_to_binop = function
+ | Rlt -> Lt
+ | Rgt -> Gt
+ | Rle -> Le
+ | Rge -> Ge
+ | Req -> Eq
+ | Rneq -> Ne
+
+(* 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 =
+ let loc = p.pred_loc in
+ let lenv = Env.Local_vars.get env in
+ Cil.CurrentLoc.set loc;
+ match p.pred_content with
+ | Pfalse -> Cil.zero ~loc, adata, env
+ | Ptrue -> Cil.one ~loc, adata, env
+ | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
+ | Papp (li, [], args) ->
+ let e, adata, env =
+ Logic_functions.app_to_exp ~adata ~loc kf env li args in
+ let adata, env = Assert.register_pred ~loc kf env p e adata in
+ e, adata, env
+ | Pdangling _ -> Env.not_yet env "\\dangling"
+ | Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
+ | Pvalid_function _ -> Env.not_yet env "\\valid_function"
+ | Prel(rel, t1, t2) ->
+ let ity =
+ Typing.get_integer_op_of_predicate ~lenv p
+ in
+ Translate_utils.comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
+ | Pand(p1, p2) ->
+ (* p1 && p2 <==> if p1 then p2 else false *)
+ Extlib.flatten
+ (Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
+ let e2, adata, env2 =
+ predicate_to_exp ~adata kf (Env.push env1) p2 in
+ let res2 = e2, env2 in
+ let env3 = Env.push env2 in
+ let name = match name with None -> "and" | Some n -> n in
+ Extlib.nest
+ adata
+ (Translate_utils.conditional_to_exp
+ ~name
+ ~loc
+ kf
+ None
+ e1
+ res2
+ (Cil.zero loc, env3))
+ ))
+ | Por(p1, p2) ->
+ (* p1 || p2 <==> if p1 then true else p2 *)
+ Extlib.flatten
+ (Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
+ let env' = Env.push env1 in
+ let e2, adata, env2 =
+ predicate_to_exp ~adata kf (Env.push env') p2
+ in
+ let res2 = e2, env2 in
+ let name = match name with None -> "or" | Some n -> n in
+ Extlib.nest
+ adata
+ (Translate_utils.conditional_to_exp
+ ~name
+ ~loc
+ kf
+ None
+ e1
+ (Cil.one loc, env')
+ res2)
+ ))
+ | Pxor _ -> Env.not_yet env "xor"
+ | Pimplies(p1, p2) ->
+ (* (p1 ==> p2) <==> !p1 || p2 *)
+ predicate_to_exp
+ ~adata
+ ~name:"implies"
+ kf
+ env
+ (Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
+ | Piff(p1, p2) ->
+ (* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
+ predicate_to_exp
+ ~adata
+ ~name:"equiv"
+ kf
+ env
+ (Logic_const.pand ~loc
+ (Logic_const.pimplies ~loc (p1, p2),
+ Logic_const.pimplies ~loc (p2, p1)))
+ | Pnot p ->
+ let e, adata, env = predicate_to_exp ~adata kf env p in
+ Smart_exp.lnot ~loc e, adata, env
+ | Pif(t, p2, p3) ->
+ Extlib.flatten
+ (Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, adata, env1 = Translate_terms.term_to_exp ~adata kf env t in
+ let e2, adata, env2 =
+ predicate_to_exp ~adata kf (Env.push env1) p2 in
+ let res2 = e2, env2 in
+ let e3, adata, env3 =
+ predicate_to_exp ~adata kf (Env.push env2) p3
+ in
+ let res3 = e3, env3 in
+ Extlib.nest
+ adata
+ (Translate_utils.conditional_to_exp ~loc kf None e1 res2 res3)
+ ))
+ | Plet(li, p) ->
+ let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
+ let env = Env.Logic_scope.extend env lvs in
+ let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+ let e, adata, env = predicate_to_exp ~adata kf env p in
+ Interval.Env.remove li.l_var_info;
+ e, adata, env
+ | Pforall _ | Pexists _ ->
+ let e, env = Quantif.quantif_to_exp kf env p in
+ let adata, env = Assert.register_pred ~loc kf env p e adata in
+ e, adata, env
+ | Pat(p, BuiltinLabel Here) ->
+ predicate_to_exp ~adata kf env p
+ | Pat(p', label) ->
+ let lscope = Env.Logic_scope.get env in
+ let pot = Lscope.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 kf env p e adata in
+ e, adata, env
+ else begin
+ (* convert [t'] to [e] in a separated local env *)
+ let e, adata, env = predicate_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 kf env p e adata in
+ e, adata, env
+ end
+ | Pvalid_read(BuiltinLabel Here, t) as pc
+ | (Pvalid(BuiltinLabel Here, t) as pc) ->
+ let call_valid ~adata t p =
+ let name = match pc with
+ | Pvalid _ -> "valid"
+ | Pvalid_read _ -> "valid_read"
+ | _ -> assert false
+ in
+ let e, adata, env =
+ Memory_translate.call_valid ~adata ~loc kf name Cil.intType env t p
+ in
+ let adata, env = Assert.register_pred ~loc kf env p e adata in
+ e, adata, env
+ in
+ (* we already transformed \valid(t) into \initialized(&t) && \valid(t):
+ now convert this right-most valid. *)
+ call_valid ~adata t p
+ | Pvalid _ -> Env.not_yet env "labeled \\valid"
+ | Pvalid_read _ -> Env.not_yet env "labeled \\valid_read"
+ | Pseparated tlist ->
+ let env =
+ List.fold_left
+ (fun env t ->
+ let name = "separated_guard" in
+ let p = Logic_const.pvalid_read ~loc (BuiltinLabel Here, t) in
+ let p = { p with pred_name = name :: p.pred_name } in
+ let tp = Logic_const.toplevel_predicate ~kind:Assert p in
+ let annot = Logic_const.new_code_annotation (AAssert ([],tp)) in
+ Typing.preprocess_rte (Env.Local_vars.get env) annot;
+ !translate_rte_annots_ref Printer.pp_code_annotation annot kf env [annot]
+ )
+ env
+ tlist
+ in
+ let e, adata, env =
+ Memory_translate.call_with_size
+ ~adata
+ ~loc
+ kf
+ "separated"
+ Cil.intType
+ env
+ tlist
+ p
+ in
+ let adata, env = Assert.register_pred ~loc kf env p e adata in
+ e, adata, env
+ | Pinitialized(BuiltinLabel Here, t) ->
+ let e, adata, env =
+ (match t.term_node with
+ (* optimisation when we know that the initialisation is ok *)
+ | TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, adata, env
+ | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
+ when
+ vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
+ Cil.one ~loc, adata, env
+ | _ ->
+ let e, adata, env =
+ Memory_translate.call_with_size
+ ~adata
+ ~loc
+ kf
+ "initialized"
+ Cil.intType
+ env
+ [ t ]
+ p
+ in
+ let adata, env = Assert.register_pred ~loc kf env p e adata in
+ e, adata, env)
+ in
+ e, adata, env
+ | Pinitialized _ -> Env.not_yet env "labeled \\initialized"
+ | Pallocable _ -> Env.not_yet env "\\allocate"
+ | Pfreeable(BuiltinLabel Here, t) ->
+ let e, adata, env =
+ Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
+ in
+ let adata, env = Assert.register_pred ~loc kf env p e adata in
+ e, adata, env
+ | Pfreeable _ -> Env.not_yet env "labeled \\freeable"
+ | Pfresh _ -> Env.not_yet env "\\fresh"
+
+and predicate_to_exp ~adata ?name kf ?rte env p =
+ match Logic_normalizer.get_pred p with
+ | PoT_term t -> Translate_terms.term_to_exp ~adata kf env t
+ | 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
+ ~f:(fun env ->
+ let e, adata, env =
+ predicate_content_to_exp ~adata ?name kf env p
+ in
+ let env = if rte then !translate_rte_exp_ref kf env e else env in
+ let cast =
+ Typing.get_cast_of_predicate
+ ~lenv:(Env.Local_vars.get env)
+ p
+ in
+ Extlib.nest
+ adata
+ (Typed_number.add_cast
+ ~loc:p.pred_loc
+ ?name
+ env
+ kf
+ cast
+ Typed_number.C_number
+ None
+ e)
+ ))
+
+let generalized_untyped_predicate_to_exp ~adata ?name kf ?rte env p =
+ (* If [rte] is true, it means we're translating the root predicate of an
+ assertion and we need to generate the RTE for it. The typing environment
+ must be cleared. Otherwise, if [rte] is false, it means we're already
+ translating RTE predicates as part of the translation of another root
+ predicate, and the typing environment must be kept. *)
+ let rte = match rte with None -> Env.generate_rte env | Some b -> b in
+ let e, adata, env = predicate_to_exp ~adata ?name kf ~rte env p in
+ assert (Typ.equal (Cil.typeOf e) Cil.intType);
+ let env = Env.Logic_scope.reset env in
+ e, adata, env
+
+let translate_predicate ?pred_to_print kf env p =
+ match p.tp_kind with
+ | Assert | Check ->
+ Options.feedback ~dkey ~level:3 "translating predicate %a"
+ Printer.pp_toplevel_predicate p;
+ let pred_to_print =
+ match pred_to_print with
+ | Some pred ->
+ Options.feedback ~dkey ~level:3 "(predicate to print %a)"
+ Printer.pp_predicate pred;
+ pred
+ | None -> p.tp_statement
+ in
+ let adata, env = Assert.empty ~loc:p.tp_statement.pred_loc kf env in
+ let e, adata, env =
+ generalized_untyped_predicate_to_exp ~adata kf env p.tp_statement
+ in
+ let stmt, env =
+ Assert.runtime_check
+ ~adata
+ ~pred_kind:p.tp_kind
+ (Env.annotation_kind env)
+ kf
+ env
+ e
+ pred_to_print
+ in
+ Env.add_stmt
+ env
+ kf
+ stmt
+ | Admit -> env
+
+let predicate_to_exp_without_rte ~adata kf env p =
+ (* forget optional argument ?rte and ?name*)
+ predicate_to_exp ~adata kf env p
+
+let () =
+ Translate_utils.predicate_to_exp_ref := predicate_to_exp;
+ Loops.translate_predicate_ref := translate_predicate;
+ 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
+
+exception No_simple_predicate_translation of predicate
+
+(* This function is used by Guillaume.
+ However, it is correct to use it only in specific contexts. *)
+let untyped_predicate_to_exp p =
+ let env = Env.push Env.empty in
+ let env = Env.rte env false in
+ let e, _, env =
+ try generalized_untyped_predicate_to_exp
+ ~adata:Assert.no_data
+ (Kernel_function.dummy ())
+ env
+ p
+ with Rtl.Symbols.Unregistered _ -> raise (No_simple_predicate_translation p)
+ in
+ if not (Env.has_no_new_stmt env)
+ then raise (No_simple_predicate_translation p);
+ e
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.mli b/src/plugins/e-acsl/src/code_generator/translate_predicates.mli
similarity index 68%
rename from src/plugins/e-acsl/src/code_generator/translate.mli
rename to src/plugins/e-acsl/src/code_generator/translate_predicates.mli
index ea9ff115508bf94e49e6d0a16814b6898bd77210..8bdae9d2b9e911519c64de6e48208f389cf996cc 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.mli
@@ -22,7 +22,7 @@
open Cil_types
-(** Generate C implementations of E-ACSL predicates and terms. *)
+(** Generate C implementations of E-ACSL predicates. *)
val predicate_to_exp:
adata:Assert.t ->
@@ -54,56 +54,33 @@ val translate_predicate:
If [pred_to_print] is set, then the runtime check will use this predicate as
message. *)
-val term_to_exp:
- adata:Assert.t ->
- kernel_function ->
- Env.t ->
- term ->
- exp * Assert.t * Env.t
-(** Convert an ACSL term into a corresponding C expression. *)
-
-val translate_rte_annots:
- (Format.formatter -> 'a -> unit) ->
- 'a ->
- kernel_function ->
- Env.t ->
- code_annotation list ->
- Env.t
-(** Translate the given RTE annotations into runtime checks in the given
- environment. *)
-
-val gmp_to_sizet:
- adata:Assert.t ->
- loc:location ->
- name:string ->
- ?check_lower_bound:bool ->
- ?pp:term ->
- kernel_function ->
- Env.t ->
- term ->
- exp * Assert.t * Env.t
-(** Translate the given GMP integer to an expression of type [size_t]. RTE
- checks are generated to ensure that the GMP value holds in this type.
- The parameter [name] is used to generate relevant predicate names.
- If [check_lower_bound] is set to [false], then the GMP value is assumed to
- be positive.
- If [pp] is provided, this term is used in the messages of the RTE checks. *)
-
-exception No_simple_term_translation of term
-(** Exceptin raised if [untyped_term_to_exp] would generate new statements in
- the environment *)
-
exception No_simple_predicate_translation of predicate
(** Exceptin raised if [untyped_predicate_to_exp] would generate new statements
in the environment *)
-val untyped_term_to_exp: typ option -> term -> exp
-(** Convert an untyped ACSL term into a corresponding C expression. *)
-
val untyped_predicate_to_exp: predicate -> exp
(** Convert an untyped ACSL predicate into a corresponding C expression. This
expression is valid only in certain contexts and shouldn't be used. *)
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val translate_rte_annots_ref:
+ ((Format.formatter -> code_annotation -> unit) ->
+ code_annotation ->
+ kernel_function ->
+ Env.t ->
+ code_annotation list ->
+ Env.t) ref
+
+val translate_rte_exp_ref:
+ (?filter:(code_annotation -> bool) ->
+ kernel_function ->
+ Env.t ->
+ exp ->
+ Env.t) ref
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
new file mode 100644
index 0000000000000000000000000000000000000000..59be7b215c3b7324fa1479b5898de2314ac7f1ff
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
@@ -0,0 +1,79 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Generate and translate RTE annotations. *)
+
+open Cil_types
+let dkey = Options.dkey_translation
+
+let translate_rte_annots pp elt kf env l =
+ let old_kind = Env.annotation_kind env in
+ let env = Env.set_annotation_kind env Smart_stmt.RTE in
+ let env =
+ List.fold_left
+ (fun env a -> match a.annot_content with
+ | AAssert(_, p) ->
+ Env.handle_error
+ (fun env ->
+ Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
+ (* The logic scope MUST NOT be reset here since we still might
+ be in the middle of the translation of the original
+ predicate. *)
+ 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
+ ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
+ in
+ let env = Env.Logic_scope.set_reset env lscope_reset_old in
+ env)
+ env
+ | _ -> assert false)
+ env
+ l
+ in
+ Env.set_annotation_kind env old_kind
+
+let () =
+ Translate_predicates.translate_rte_annots_ref := translate_rte_annots
+
+let translate_rte ?filter kf env e =
+ let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
+ let l = Rte.exp kf stmt e in
+ let l =
+ match filter with
+ | Some f -> List.filter f l
+ | None -> l
+ in
+ List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
+ translate_rte_annots Printer.pp_exp e kf env l
+
+let () =
+ Translate_terms.translate_rte_exp_ref := translate_rte;
+ Translate_predicates.translate_rte_exp_ref := translate_rte;
+ Logic_array.translate_rte_ref := translate_rte
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.mli b/src/plugins/e-acsl/src/code_generator/translate_rtes.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8934e503dcb0a2fdc51959c8e023cbeb725e336e
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.mli
@@ -0,0 +1,45 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+(** Generate and translate RTE annotations. *)
+
+val translate_rte_annots:
+ (Format.formatter -> 'a -> unit) ->
+ 'a ->
+ kernel_function ->
+ Env.t ->
+ code_annotation list ->
+ Env.t
+(** Translate the given RTE annotations into runtime checks in the given
+ environment. *)
+
+val translate_rte: ?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp -> Env.t
+(** Generate RTE annotations from the given expression and translate them in the
+ given environment. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
similarity index 60%
rename from src/plugins/e-acsl/src/code_generator/translate.ml
rename to src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 4a67b008be38c97f542b72a4addecb33f77803da..e403fc6441e79ec6ec566d83269af31a5df8dcb7 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -20,25 +20,29 @@
(* *)
(**************************************************************************)
-(** Generate C implementations of E-ACSL predicates and terms. *)
+(** Generate C implementations of E-ACSL terms. *)
-module E_acsl_label = Label
open Cil_types
-open Cil_datatype
let dkey = Options.dkey_translation
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let translate_rte_exp_ref
+ : (?filter:(code_annotation -> bool) ->
+ kernel_function ->
+ Env.t ->
+ exp ->
+ Env.t) ref
+ =
+ ref (fun ?filter:_ _kf _env _e ->
+ Extlib.mk_labeled_fun "translate_rte_exp_ref")
+
(* ************************************************************************** *)
-(* Transforming terms and predicates into C expressions (if any) *)
+(* Transforming terms into C expressions (if any) *)
(* ************************************************************************** *)
-let relation_to_binop = function
- | Rlt -> Lt
- | Rgt -> Gt
- | Rle -> Le
- | Rge -> Ge
- | Req -> Eq
- | Rneq -> Ne
-
let constant_to_exp ~loc env t c =
let lenv = Env.Local_vars.get env in
let mk_real s =
@@ -82,46 +86,6 @@ let constant_to_exp ~loc env t c =
else mk_real lr.r_literal
| LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), Typed_number.C_number
-let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
- let env = Env.pop (Env.pop env3) in
- match e1.enode with
- | Const(CInt64(n, _, _)) when Integer.is_zero n ->
- e3, Env.transfer ~from:env3 env
- | Const(CInt64(n, _, _)) when Integer.is_one n ->
- e2, Env.transfer ~from:env2 env
- | _ ->
- let ty = match t_opt with
- | None (* predicate *) -> Cil.intType
- | Some t -> Typing.get_typ ~lenv:(Env.Local_vars.get env) t
- in
- let _, e, env =
- Env.new_var
- ~loc
- ~name
- env
- kf
- t_opt
- ty
- (fun v ev ->
- let lv = Cil.var v in
- let ty = Cil.typeOf ev in
- let init_set =
- assert (not (Gmp_types.Q.is_t ty));
- Gmp.init_set
- in
- let affect e = init_set ~loc lv ev e in
- let then_blk, _ =
- let s = affect e2 in
- Env.pop_and_get env2 s ~global_clear:false Env.Middle
- in
- let else_blk, _ =
- let s = affect e3 in
- Env.pop_and_get env3 s ~global_clear:false Env.Middle
- in
- [ Smart_stmt.if_stmt ~loc ~cond:e1 then_blk ~else_blk ])
- in
- e, env
-
(* Create and initialize a variable in the [env] according to [ty], [name] and [exp_init],
return a tuple [varinfo * exp] and the [env] extended with the new variable. *)
let create_and_init_var ~loc kf ty name exp_init env =
@@ -360,7 +324,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let ctx = Typing.get_number_ty ~lenv t in
Typing.type_term ~use_gmp_opt:true ~ctx ~lenv zero;
let e, adata, env =
- comparison_to_exp
+ Translate_utils.comparison_to_exp
~adata
kf
~loc
@@ -426,7 +390,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
(* do not generate [e2] from [t2] twice *)
let guard, _, env =
let name = Misc.name_of_binop bop ^ "_guard" in
- comparison_to_exp
+ Translate_utils.comparison_to_exp
~adata:Assert.no_data ~loc kf env Typing.gmpz ~e1:e2 ~name Ne t2 zero t
in
let p = Logic_const.prel ~loc (Rneq, t2, zero) in
@@ -464,7 +428,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
(* comparison operators *)
let ity = Typing.get_integer_op ~lenv t in
let e, adata, env =
- comparison_to_exp ~adata ~loc kf env ity bop t1 t2 (Some t)
+ Translate_utils.comparison_to_exp ~adata ~loc kf env ity bop t1 t2 (Some t)
in
e, adata, env, Typed_number.C_number, ""
| TBinOp((Shiftlt | Shiftrt) as bop, t1, t2) ->
@@ -576,7 +540,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
[ result_e; e1; e2_as_bitcnt_e ]
in
- (* Put t in an option to use with comparison_to_exp and
+ (* Put t in an option to use with Translate_utils.comparison_to_exp and
Env.new_var_and_mpz_init *)
let t = Some t in
@@ -599,7 +563,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
then check e1 >= 0 *)
let e1_guard, _, env =
let name = e1_name ^ bop_name ^ "_guard" in
- comparison_to_exp
+ Translate_utils.comparison_to_exp
~adata:Assert.no_data
~loc
kf
@@ -665,8 +629,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
let res2 = e2, env2 in
Extlib.nest
adata
- (conditional_to_exp
- ~name:"or" loc kf (Some t) e1 (Cil.one loc, env') res2)
+ (Translate_utils.conditional_to_exp
+ ~name:"or" ~loc kf (Some t) e1 (Cil.one loc, env') res2)
))
in
e, adata, env, Typed_number.C_number, ""
@@ -684,8 +648,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
let env3 = Env.push env2 in
Extlib.nest
adata
- (conditional_to_exp
- ~name:"and" loc kf (Some t) e1 res2 (Cil.zero loc, env3))
+ (Translate_utils.conditional_to_exp
+ ~name:"and" ~loc kf (Some t) e1 res2 (Cil.zero loc, env3))
))
in
e, adata, env, Typed_number.C_number, ""
@@ -797,7 +761,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let res3 = e3, env3 in
Extlib.nest
adata
- (conditional_to_exp loc kf (Some t) e1 res2 res3)
+ (Translate_utils.conditional_to_exp ~loc kf (Some t) e1 res2 res3)
))
in
e, adata, env, Typed_number.C_number, ""
@@ -813,7 +777,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
e, adata, env, Typed_number.C_number, ""
else
let e, _, env = term_to_exp ~adata:Assert.no_data kf (Env.push env) t' in
- let e, env, sty = at_to_exp_no_lscope env kf (Some t) label e 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 kf env t e adata in
e, adata, env, sty, ""
| Tbase_addr(BuiltinLabel Here, t') ->
@@ -863,7 +827,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
| Tlet(li, t) ->
let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.Logic_scope.extend env lvs in
- let adata, env = env_of_li ~adata li kf env loc in
+ let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
let e, adata, env = term_to_exp ~adata kf env t in
Interval.Env.remove li.l_var_info;
e, adata, env, Typed_number.C_number, ""
@@ -884,7 +848,7 @@ and term_to_exp ~adata kf env t =
let e, adata, env, sty, name =
context_insensitive_term_to_exp ~adata kf env t
in
- let env = if generate_rte then translate_rte kf env e else env in
+ let env = if generate_rte then !translate_rte_exp_ref kf env e else env in
let cast = Typing.get_cast ~lenv:(Env.Local_vars.get env) t in
let name = if name = "" then None else Some name in
Extlib.nest
@@ -900,604 +864,14 @@ and term_to_exp ~adata kf env t =
e)
))
-(* generate the C code equivalent to [t1 bop t2]. *)
-and comparison_to_exp
- ~adata
- ~loc
- ?e1
- kf
- env
- ity
- bop
- ?(name = Misc.name_of_binop bop)
- t1
- t2
- t_opt
- =
- let e1, adata, env =
- match e1 with
- | None ->
- let e1, adata, env = term_to_exp ~adata kf env t1 in
- e1, adata, env
- | Some e1 ->
- e1, adata, env
- in
- let ty1 = Cil.typeOf e1 in
- let e2, adata, env = term_to_exp ~adata kf env t2 in
- let ty2 = Cil.typeOf e2 in
- let e, env =
- match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with
- | Logic_aggr.Array, Logic_aggr.Array ->
- Logic_array.comparison_to_exp
- ~loc
- kf
- env
- ~name
- bop
- e1
- e2
- | Logic_aggr.StructOrUnion, Logic_aggr.StructOrUnion ->
- Env.not_yet env "comparison between two structs or unions"
- | Logic_aggr.NotAggregate, Logic_aggr.NotAggregate -> begin
- match ity with
- | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
- Cil.mkBinOp ~loc bop e1 e2, env
- | Typing.Gmpz ->
- let _, e, env = Env.new_var
- ~loc
- env
- kf
- t_opt
- ~name
- Cil.intType
- (fun v _ ->
- [ Smart_stmt.rtl_call ~loc
- ~result:(Cil.var v)
- ~prefix:""
- "__gmpz_cmp"
- [ e1; e2 ] ])
- in
- Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
- | Typing.Rational ->
- Rational.cmp ~loc bop e1 e2 env kf t_opt
- | Typing.Real ->
- Error.not_yet "comparison involving real numbers"
- end
- | _, _ ->
- Options.fatal
- ~current:true
- "Comparison involving incompatible types: '%a' and '%a'"
- Printer.pp_typ ty1
- Printer.pp_typ ty2
- in
- e, adata, env
-
-and at_to_exp_no_lscope env kf 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
-
-and env_of_li ~adata li kf env loc =
- match li.l_var_info.lv_type with
- | Ctype _ | Linteger | Lreal ->
- let t = Misc.term_of_li li in
- let lenv = Env.Local_vars.get env in
- let ty = Typing.get_typ ~lenv t in
- let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
- let e, adata, env = term_to_exp ~adata kf env t in
- let stmt = match Typing.get_number_ty ~lenv t with
- | Typing.(C_integer _ | C_float _ | Nan) ->
- Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
- | Typing.Gmpz ->
- Gmp.init_set ~loc (Cil.var vi) vi_e e
- | Typing.Rational ->
- Rational.init_set ~loc (Cil.var vi) vi_e e
- | Typing.Real ->
- Error.not_yet "real number"
- in
- adata, Env.add_stmt env kf stmt
- | Ltype _ ->
- Env.not_yet env "user-defined logic type"
- | Lvar _ ->
- Env.not_yet env "type variable"
- | Larrow _ ->
- Env.not_yet env "lambda-abstraction"
-
-(* Convert an ACSL predicate into a corresponding C expression (if any) in the
- given environment. Also extend this environment which includes the generating
- constructs. *)
-and predicate_content_to_exp ~adata ?name kf env p =
- let loc = p.pred_loc in
- let lenv = Env.Local_vars.get env in
- Cil.CurrentLoc.set loc;
- match p.pred_content with
- | Pfalse -> Cil.zero ~loc, adata, env
- | Ptrue -> Cil.one ~loc, adata, env
- | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
- | Papp (li, [], args) ->
- let e, adata, env =
- Logic_functions.app_to_exp ~adata ~loc kf env li args in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
- e, adata, env
- | Pdangling _ -> Env.not_yet env "\\dangling"
- | Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
- | Pvalid_function _ -> Env.not_yet env "\\valid_function"
- | Prel(rel, t1, t2) ->
- let ity =
- Typing.get_integer_op_of_predicate ~lenv p
- in
- comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
- | Pand(p1, p2) ->
- (* p1 && p2 <==> if p1 then p2 else false *)
- Extlib.flatten
- (Env.with_rte_and_result env true
- ~f:(fun env ->
- let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
- let e2, adata, env2 =
- predicate_to_exp ~adata kf (Env.push env1) p2 in
- let res2 = e2, env2 in
- let env3 = Env.push env2 in
- let name = match name with None -> "and" | Some n -> n in
- Extlib.nest
- adata
- (conditional_to_exp
- ~name
- loc
- kf
- None
- e1
- res2
- (Cil.zero loc, env3))
- ))
- | Por(p1, p2) ->
- (* p1 || p2 <==> if p1 then true else p2 *)
- Extlib.flatten
- (Env.with_rte_and_result env true
- ~f:(fun env ->
- let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
- let env' = Env.push env1 in
- let e2, adata, env2 =
- predicate_to_exp ~adata kf (Env.push env') p2
- in
- let res2 = e2, env2 in
- let name = match name with None -> "or" | Some n -> n in
- Extlib.nest
- adata
- (conditional_to_exp
- ~name
- loc
- kf
- None
- e1
- (Cil.one loc, env')
- res2)
- ))
- | Pxor _ -> Env.not_yet env "xor"
- | Pimplies(p1, p2) ->
- (* (p1 ==> p2) <==> !p1 || p2 *)
- predicate_to_exp
- ~adata
- ~name:"implies"
- kf
- env
- (Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
- | Piff(p1, p2) ->
- (* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
- predicate_to_exp
- ~adata
- ~name:"equiv"
- kf
- env
- (Logic_const.pand ~loc
- (Logic_const.pimplies ~loc (p1, p2),
- Logic_const.pimplies ~loc (p2, p1)))
- | Pnot p ->
- let e, adata, env = predicate_to_exp ~adata kf env p in
- Smart_exp.lnot ~loc e, adata, env
- | Pif(t, p2, p3) ->
- Extlib.flatten
- (Env.with_rte_and_result env true
- ~f:(fun env ->
- let e1, adata, env1 = term_to_exp ~adata kf env t in
- let e2, adata, env2 =
- predicate_to_exp ~adata kf (Env.push env1) p2 in
- let res2 = e2, env2 in
- let e3, adata, env3 =
- predicate_to_exp ~adata kf (Env.push env2) p3
- in
- let res3 = e3, env3 in
- Extlib.nest
- adata
- (conditional_to_exp loc kf None e1 res2 res3)
- ))
- | Plet(li, p) ->
- let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
- let env = Env.Logic_scope.extend env lvs in
- let adata, env = env_of_li ~adata li kf env loc in
- let e, adata, env = predicate_to_exp ~adata kf env p in
- Interval.Env.remove li.l_var_info;
- e, adata, env
- | Pforall _ | Pexists _ ->
- let e, env = Quantif.quantif_to_exp kf env p in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
- e, adata, env
- | Pat(p, BuiltinLabel Here) ->
- predicate_to_exp ~adata kf env p
- | Pat(p', label) ->
- let lscope = Env.Logic_scope.get env in
- let pot = Lscope.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 kf env p e adata in
- e, adata, env
- else begin
- (* convert [t'] to [e] in a separated local env *)
- let e, adata, env = predicate_to_exp ~adata kf (Env.push env) p' in
- let e, env, sty = at_to_exp_no_lscope env kf None label e in
- assert (sty = Typed_number.C_number);
- let adata, env = Assert.register_pred ~loc kf env p e adata in
- e, adata, env
- end
- | Pvalid_read(BuiltinLabel Here, t) as pc
- | (Pvalid(BuiltinLabel Here, t) as pc) ->
- let call_valid ~adata t p =
- let name = match pc with
- | Pvalid _ -> "valid"
- | Pvalid_read _ -> "valid_read"
- | _ -> assert false
- in
- let e, adata, env =
- Memory_translate.call_valid ~adata ~loc kf name Cil.intType env t p
- in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
- e, adata, env
- in
- (* we already transformed \valid(t) into \initialized(&t) && \valid(t):
- now convert this right-most valid. *)
- call_valid ~adata t p
- | Pvalid _ -> Env.not_yet env "labeled \\valid"
- | Pvalid_read _ -> Env.not_yet env "labeled \\valid_read"
- | Pseparated tlist ->
- let env =
- List.fold_left
- (fun env t ->
- let name = "separated_guard" in
- let p = Logic_const.pvalid_read ~loc (BuiltinLabel Here, t) in
- let p = { p with pred_name = name :: p.pred_name } in
- let tp = Logic_const.toplevel_predicate ~kind:Assert p in
- let annot = Logic_const.new_code_annotation (AAssert ([],tp)) in
- Typing.preprocess_rte (Env.Local_vars.get env) annot;
- translate_rte_annots Printer.pp_code_annotation annot kf env [annot]
- )
- env
- tlist
- in
- let e, adata, env =
- Memory_translate.call_with_size
- ~adata
- ~loc
- kf
- "separated"
- Cil.intType
- env
- tlist
- p
- in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
- e, adata, env
- | Pinitialized(BuiltinLabel Here, t) ->
- let e, adata, env =
- (match t.term_node with
- (* optimisation when we know that the initialisation is ok *)
- | TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, adata, env
- | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
- when
- vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
- Cil.one ~loc, adata, env
- | _ ->
- let e, adata, env =
- Memory_translate.call_with_size
- ~adata
- ~loc
- kf
- "initialized"
- Cil.intType
- env
- [ t ]
- p
- in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
- e, adata, env)
- in
- e, adata, env
- | Pinitialized _ -> Env.not_yet env "labeled \\initialized"
- | Pallocable _ -> Env.not_yet env "\\allocate"
- | Pfreeable(BuiltinLabel Here, t) ->
- let e, adata, env =
- Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
- in
- let adata, env = Assert.register_pred ~loc kf env p e adata in
- e, adata, env
- | Pfreeable _ -> Env.not_yet env "labeled \\freeable"
- | Pfresh _ -> Env.not_yet env "\\fresh"
-
-and predicate_to_exp ~adata ?name kf ?rte env p =
- match Logic_normalizer.get_pred p with
- | PoT_term t -> term_to_exp ~adata kf env t
- | 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
- ~f:(fun env ->
- let e, adata, env =
- predicate_content_to_exp ~adata ?name kf env p
- in
- let env = if rte then translate_rte kf env e else env in
- let cast =
- Typing.get_cast_of_predicate
- ~lenv:(Env.Local_vars.get env)
- p
- in
- Extlib.nest
- adata
- (Typed_number.add_cast
- ~loc:p.pred_loc
- ?name
- env
- kf
- cast
- Typed_number.C_number
- None
- e)
- ))
-
-and generalized_untyped_predicate_to_exp ~adata ?name kf ?rte env p =
- (* If [rte] is true, it means we're translating the root predicate of an
- assertion and we need to generate the RTE for it. The typing environment
- must be cleared. Otherwise, if [rte] is false, it means we're already
- translating RTE predicates as part of the translation of another root
- predicate, and the typing environment must be kept. *)
- let rte = match rte with None -> Env.generate_rte env | Some b -> b in
- let e, adata, env = predicate_to_exp ~adata ?name kf ~rte env p in
- assert (Typ.equal (Cil.typeOf e) Cil.intType);
- let env = Env.Logic_scope.reset env in
- e, adata, env
-
-and translate_rte_annots:
- 'a. (Format.formatter -> 'a -> unit) -> 'a ->
- kernel_function -> Env.t -> code_annotation list -> Env.t =
- fun pp elt kf env l ->
- let old_kind = Env.annotation_kind env in
- let env = Env.set_annotation_kind env Smart_stmt.RTE in
- let env =
- List.fold_left
- (fun env a -> match a.annot_content with
- | AAssert(_, p) ->
- Env.handle_error
- (fun env ->
- Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
- (* The logic scope MUST NOT be reset here since we still might
- be in the middle of the translation of the original
- predicate. *)
- 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
- ~f:(fun env -> translate_predicate kf env p)
- in
- let env = Env.Logic_scope.set_reset env lscope_reset_old in
- env)
- env
- | _ -> assert false)
- env
- l
- in
- Env.set_annotation_kind env old_kind
-
-and translate_rte ?filter kf env e =
- let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
- let l = Rte.exp kf stmt e in
- let l =
- match filter with
- | Some f -> List.filter f l
- | None -> l
- in
- List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
- translate_rte_annots Printer.pp_exp e kf env l
-
-and translate_predicate ?pred_to_print kf env p =
- match p.tp_kind with
- | Assert | Check ->
- Options.feedback ~dkey ~level:3 "translating predicate %a"
- Printer.pp_toplevel_predicate p;
- let pred_to_print =
- match pred_to_print with
- | Some pred ->
- Options.feedback ~dkey ~level:3 "(predicate to print %a)"
- Printer.pp_predicate pred;
- pred
- | None -> p.tp_statement
- in
- let adata, env = Assert.empty ~loc:p.tp_statement.pred_loc kf env in
- let e, adata, env =
- generalized_untyped_predicate_to_exp ~adata kf env p.tp_statement
- in
- let stmt, env =
- Assert.runtime_check
- ~adata
- ~pred_kind:p.tp_kind
- (Env.annotation_kind env)
- kf
- env
- e
- pred_to_print
- in
- Env.add_stmt
- env
- kf
- stmt
- | Admit -> env
-
-let predicate_to_exp_without_rte ~adata kf env p =
- (* forget optional argument ?rte and ?name*)
- predicate_to_exp ~adata kf env p
-
-let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
- let lenv = Env.Local_vars.get env in
- let pp = match pp with Some size_pp -> size_pp | None -> t in
- let sizet = Cil.(theMachine.typeOfSizeOf) in
- let stmts = [] in
- (* Lower guard *)
- let stmts, env =
- if check_lower_bound then begin
- let zero_term = Cil.lzero ~loc () in
- let pred_name = Format.sprintf "%s_greater_or_eq_than_0" name in
- let lower_guard_pp = Logic_const.prel ~loc (Rge, pp, zero_term) in
- let lower_guard_pp =
- { lower_guard_pp with
- pred_name = pred_name :: lower_guard_pp.pred_name }
- in
- let lower_guard = Logic_const.prel ~loc (Rge, t, zero_term) in
- Typing.type_named_predicate ~lenv lower_guard;
- let adata_lower_guard, env = Assert.empty ~loc kf env in
- let lower_guard, adata_lower_guard, env =
- predicate_to_exp ~adata:adata_lower_guard kf env lower_guard
- in
- let assertion, env =
- Assert.runtime_check
- ~adata:adata_lower_guard
- ~pred_kind:Assert
- Smart_stmt.RTE
- kf
- env
- lower_guard
- lower_guard_pp
- in
- assertion :: stmts, env
- end
- else stmts, env
- in
- (* Upper guard *)
- let sizet_max =
- Logic_const.tint ~loc (Cil.max_unsigned_number (Cil.bitsSizeOf sizet))
- in
- let pred_name = Format.sprintf "%s_lesser_or_eq_than_SIZE_MAX" name in
- let upper_guard_pp = Logic_const.prel ~loc (Rle, pp, sizet_max) in
- let upper_guard_pp =
- { upper_guard_pp with
- pred_name = pred_name :: upper_guard_pp.pred_name }
- in
- let upper_guard = Logic_const.prel ~loc (Rle, t, sizet_max) in
- Typing.type_named_predicate ~lenv upper_guard;
- let adata_upper_guard, env = Assert.empty ~loc kf env in
- let upper_guard, adata_upper_guard, env =
- predicate_to_exp ~adata:adata_upper_guard kf env upper_guard
- in
- let assertion, env =
- Assert.runtime_check
- ~adata:adata_upper_guard
- ~pred_kind:Assert
- Smart_stmt.RTE
- kf
- env
- upper_guard
- upper_guard_pp
- in
- let stmts = assertion :: stmts in
- (* Translate term [t] into an exp of type [size_t] *)
- let gmp_e, adata, env = term_to_exp ~adata kf env t in
- let _, e, env = Env.new_var
- ~loc
- ~name:"size"
- env
- kf
- None
- sizet
- (fun vi _ ->
- let rtl_call =
- Smart_stmt.rtl_call ~loc
- ~result:(Cil.var vi)
- ~prefix:""
- "__gmpz_get_ui"
- [ gmp_e ]
- in
- List.rev (rtl_call :: stmts))
- in
- e, adata, env
-
let () =
+ Translate_utils.term_to_exp_ref := term_to_exp;
Loops.term_to_exp_ref := term_to_exp;
- Loops.translate_predicate_ref := translate_predicate;
- Loops.predicate_to_exp_ref := predicate_to_exp_without_rte;
- Quantif.predicate_to_exp_ref := predicate_to_exp_without_rte;
At_with_lscope.term_to_exp_ref := term_to_exp;
- At_with_lscope.predicate_to_exp_ref := predicate_to_exp_without_rte;
Memory_translate.term_to_exp_ref := term_to_exp;
- Memory_translate.predicate_to_exp_ref := predicate_to_exp_without_rte;
- Memory_translate.gmp_to_sizet_ref := gmp_to_sizet;
- Logic_functions.term_to_exp_ref := term_to_exp;
- Logic_functions.predicate_to_exp_ref := predicate_to_exp_without_rte;
- Logic_array.translate_rte_ref := translate_rte
+ Logic_functions.term_to_exp_ref := term_to_exp
exception No_simple_term_translation of term
-exception No_simple_predicate_translation of predicate
-
-(* This function is used by Guillaume.
- However, it is correct to use it only in specific contexts. *)
-let untyped_predicate_to_exp p =
- let env = Env.push Env.empty in
- let env = Env.rte env false in
- let e, _, env =
- try generalized_untyped_predicate_to_exp
- ~adata:Assert.no_data
- (Kernel_function.dummy ())
- env
- p
- with Rtl.Symbols.Unregistered _ -> raise (No_simple_predicate_translation p)
- in
- if not (Env.has_no_new_stmt env)
- then raise (No_simple_predicate_translation p);
- e
(* This function is used by plug-in [Cfp]. *)
let untyped_term_to_exp typ t =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.mli b/src/plugins/e-acsl/src/code_generator/translate_terms.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ac50cf18e8028b31038586a4041abf63dfce9105
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.mli
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+(** Generate C implementations of E-ACSL terms. *)
+
+val term_to_exp:
+ adata:Assert.t ->
+ kernel_function ->
+ Env.t ->
+ term ->
+ exp * Assert.t * Env.t
+(** Convert an ACSL term into a corresponding C expression. *)
+
+exception No_simple_term_translation of term
+(** Exceptin raised if [untyped_term_to_exp] would generate new statements in
+ the environment *)
+
+val untyped_term_to_exp: typ option -> term -> exp
+(** Convert an untyped ACSL term into a corresponding C expression. *)
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val translate_rte_exp_ref:
+ (?filter:(code_annotation -> bool) ->
+ kernel_function ->
+ Env.t ->
+ exp ->
+ Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5b7e7871488d30b22bdc6f9dd21a885c5e638402
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -0,0 +1,349 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Utility functions for generating C implementations. *)
+
+module E_acsl_label = Label
+open Cil_types
+open Cil_datatype
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let term_to_exp_ref
+ : (adata:Assert.t ->
+ kernel_function ->
+ Env.t ->
+ term ->
+ exp * Assert.t * Env.t) ref
+ =
+ ref (fun ~adata:_ _kf _env _t -> Extlib.mk_labeled_fun "term_to_exp_ref")
+
+let predicate_to_exp_ref
+ : (adata:Assert.t ->
+ ?name:string ->
+ kernel_function ->
+ ?rte:bool ->
+ Env.t ->
+ predicate ->
+ exp * Assert.t * Env.t) ref
+ =
+ ref (fun ~adata:_ ?name:_ _kf ?rte:_ _env _p ->
+ Extlib.mk_labeled_fun "predicate_to_exp_ref")
+
+(**************************************************************************)
+(********************** Utility functions *********************************)
+(**************************************************************************)
+
+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 gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
+ let lenv = Env.Local_vars.get env in
+ let pp = match pp with Some size_pp -> size_pp | None -> t in
+ let sizet = Cil.(theMachine.typeOfSizeOf) in
+ let stmts = [] in
+ (* Lower guard *)
+ let stmts, env =
+ if check_lower_bound then begin
+ let zero_term = Cil.lzero ~loc () in
+ let pred_name = Format.sprintf "%s_greater_or_eq_than_0" name in
+ let lower_guard_pp = Logic_const.prel ~loc (Rge, pp, zero_term) in
+ let lower_guard_pp =
+ { lower_guard_pp with
+ pred_name = pred_name :: lower_guard_pp.pred_name }
+ in
+ let lower_guard = Logic_const.prel ~loc (Rge, t, zero_term) in
+ Typing.type_named_predicate ~lenv lower_guard;
+ let adata_lower_guard, env = Assert.empty ~loc kf env in
+ let lower_guard, adata_lower_guard, env =
+ !predicate_to_exp_ref ~adata:adata_lower_guard kf env lower_guard
+ in
+ let assertion, env =
+ Assert.runtime_check
+ ~adata:adata_lower_guard
+ ~pred_kind:Assert
+ Smart_stmt.RTE
+ kf
+ env
+ lower_guard
+ lower_guard_pp
+ in
+ assertion :: stmts, env
+ end
+ else stmts, env
+ in
+ (* Upper guard *)
+ let sizet_max =
+ Logic_const.tint ~loc (Cil.max_unsigned_number (Cil.bitsSizeOf sizet))
+ in
+ let pred_name = Format.sprintf "%s_lesser_or_eq_than_SIZE_MAX" name in
+ let upper_guard_pp = Logic_const.prel ~loc (Rle, pp, sizet_max) in
+ let upper_guard_pp =
+ { upper_guard_pp with
+ pred_name = pred_name :: upper_guard_pp.pred_name }
+ in
+ let upper_guard = Logic_const.prel ~loc (Rle, t, sizet_max) in
+ Typing.type_named_predicate ~lenv upper_guard;
+ let adata_upper_guard, env = Assert.empty ~loc kf env in
+ let upper_guard, adata_upper_guard, env =
+ !predicate_to_exp_ref ~adata:adata_upper_guard kf env upper_guard
+ in
+ let assertion, env =
+ Assert.runtime_check
+ ~adata:adata_upper_guard
+ ~pred_kind:Assert
+ Smart_stmt.RTE
+ kf
+ env
+ upper_guard
+ upper_guard_pp
+ in
+ let stmts = assertion :: stmts in
+ (* Translate term [t] into an exp of type [size_t] *)
+ let gmp_e, adata, env = !term_to_exp_ref ~adata kf env t in
+ let _, e, env = Env.new_var
+ ~loc
+ ~name:"size"
+ env
+ kf
+ None
+ sizet
+ (fun vi _ ->
+ let rtl_call =
+ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var vi)
+ ~prefix:""
+ "__gmpz_get_ui"
+ [ gmp_e ]
+ in
+ List.rev (rtl_call :: stmts))
+ in
+ e, adata, env
+
+let () =
+ Memory_translate.gmp_to_sizet_ref := gmp_to_sizet
+
+let comparison_to_exp
+ ~adata
+ ~loc
+ kf
+ env
+ ity
+ ?e1
+ bop
+ t1
+ t2
+ ?(name = Misc.name_of_binop bop)
+ t_opt
+ =
+ let e1, adata, env =
+ match e1 with
+ | None ->
+ let e1, adata, env = !term_to_exp_ref ~adata kf env t1 in
+ e1, adata, env
+ | Some e1 ->
+ e1, adata, env
+ in
+ let ty1 = Cil.typeOf e1 in
+ let e2, adata, env = !term_to_exp_ref ~adata kf env t2 in
+ let ty2 = Cil.typeOf e2 in
+ let e, env =
+ match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with
+ | Logic_aggr.Array, Logic_aggr.Array ->
+ Logic_array.comparison_to_exp
+ ~loc
+ kf
+ env
+ ~name
+ bop
+ e1
+ e2
+ | Logic_aggr.StructOrUnion, Logic_aggr.StructOrUnion ->
+ Env.not_yet env "comparison between two structs or unions"
+ | Logic_aggr.NotAggregate, Logic_aggr.NotAggregate -> begin
+ match ity with
+ | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
+ Cil.mkBinOp ~loc bop e1 e2, env
+ | Typing.Gmpz ->
+ let _, e, env = Env.new_var
+ ~loc
+ env
+ kf
+ t_opt
+ ~name
+ Cil.intType
+ (fun v _ ->
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var v)
+ ~prefix:""
+ "__gmpz_cmp"
+ [ e1; e2 ] ])
+ in
+ Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+ | Typing.Rational ->
+ Rational.cmp ~loc bop e1 e2 env kf t_opt
+ | Typing.Real ->
+ Error.not_yet "comparison involving real numbers"
+ end
+ | _, _ ->
+ Options.fatal
+ ~current:true
+ "Comparison involving incompatible types: '%a' and '%a'"
+ Printer.pp_typ ty1
+ Printer.pp_typ ty2
+ in
+ e, adata, env
+
+let conditional_to_exp ?(name="if") ~loc kf t_opt e1 (e2, env2) (e3, env3) =
+ let env = Env.pop (Env.pop env3) in
+ match e1.enode with
+ | Const(CInt64(n, _, _)) when Integer.is_zero n ->
+ e3, Env.transfer ~from:env3 env
+ | Const(CInt64(n, _, _)) when Integer.is_one n ->
+ e2, Env.transfer ~from:env2 env
+ | _ ->
+ let ty = match t_opt with
+ | None (* predicate *) -> Cil.intType
+ | Some t -> Typing.get_typ ~lenv:(Env.Local_vars.get env) t
+ in
+ let _, e, env =
+ Env.new_var
+ ~loc
+ ~name
+ env
+ kf
+ t_opt
+ ty
+ (fun v ev ->
+ let lv = Cil.var v in
+ let ty = Cil.typeOf ev in
+ let init_set =
+ assert (not (Gmp_types.Q.is_t ty));
+ Gmp.init_set
+ in
+ let affect e = init_set ~loc lv ev e in
+ let then_blk, _ =
+ let s = affect e2 in
+ Env.pop_and_get env2 s ~global_clear:false Env.Middle
+ in
+ let else_blk, _ =
+ let s = affect e3 in
+ Env.pop_and_get env3 s ~global_clear:false Env.Middle
+ in
+ [ Smart_stmt.if_stmt ~loc ~cond:e1 then_blk ~else_blk ])
+ in
+ e, env
+
+let env_of_li ~adata ~loc kf env li =
+ match li.l_var_info.lv_type with
+ | Ctype _ | Linteger | Lreal ->
+ let t = Misc.term_of_li li in
+ let lenv = Env.Local_vars.get env in
+ let ty = Typing.get_typ ~lenv t in
+ let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
+ let e, adata, env = !term_to_exp_ref ~adata kf env t in
+ let stmt = match Typing.get_number_ty ~lenv t with
+ | Typing.(C_integer _ | C_float _ | Nan) ->
+ Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
+ | Typing.Gmpz ->
+ Gmp.init_set ~loc (Cil.var vi) vi_e e
+ | Typing.Rational ->
+ Rational.init_set ~loc (Cil.var vi) vi_e e
+ | Typing.Real ->
+ Error.not_yet "real number"
+ in
+ adata, Env.add_stmt env kf stmt
+ | Ltype _ ->
+ Env.not_yet env "user-defined logic type"
+ | Lvar _ ->
+ Env.not_yet env "type variable"
+ | 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 ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.mli b/src/plugins/e-acsl/src/code_generator/translate_utils.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a7a7489ab8ea085c71eab0fafdc2164e4e2631c8
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.mli
@@ -0,0 +1,134 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+(** Utility functions for generating C implementations. *)
+
+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 gmp_to_sizet:
+ adata:Assert.t ->
+ loc:location ->
+ name:string ->
+ ?check_lower_bound:bool ->
+ ?pp:term ->
+ kernel_function ->
+ Env.t ->
+ term ->
+ exp * Assert.t * Env.t
+(** Translate the given GMP integer to an expression of type [size_t]. RTE
+ checks are generated to ensure that the GMP value holds in this type.
+ The parameter [name] is used to generate relevant predicate names.
+ If [check_lower_bound] is set to [false], then the GMP value is assumed to
+ be positive.
+ If [pp] is provided, this term is used in the messages of the RTE checks. *)
+
+val comparison_to_exp:
+ adata:Assert.t ->
+ loc:location ->
+ kernel_function ->
+ Env.t ->
+ Typing.number_ty ->
+ ?e1:exp ->
+ binop ->
+ term ->
+ term ->
+ ?name:string ->
+ term option ->
+ exp * Assert.t * Env.t
+(** [comparison_to_exp ~data ~loc kf env ity ?e1 ?name bop t1 t2 topt] generates
+ the C code equivalent to [t1 bop t2] in the given environment with the
+ given assertion context.
+ [ity] is the number type of the comparison when comparing scalar numbers.
+ [e1] is the expression representing [t1] if the term has already been
+ translated.
+ [name] is used to generate temporary variable names.
+ [topt] is the term holding the result of the comparison. *)
+
+val conditional_to_exp:
+ ?name:string ->
+ loc:location ->
+ kernel_function ->
+ term option ->
+ exp ->
+ exp * Env.t ->
+ exp * Env.t ->
+ exp * Env.t
+(** [conditional_to_exp ?name ~loc kf t_opt e1 (e2, env2) (e3, env3)] generates
+ the C code equivalent to [e1 ? e2 : e3] in the given environment.
+ [env2]Â and [env3] are the environment respectively for [e2] and [e3].
+ [t_opt] is the term holding the result of the conditional. *)
+
+val env_of_li:
+ adata:Assert.t ->
+ loc:location ->
+ kernel_function ->
+ Env.t ->
+ logic_info ->
+ Assert.t * Env.t
+(** [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 ********************************)
+(**************************************************************************)
+
+val term_to_exp_ref:
+ (adata:Assert.t ->
+ kernel_function ->
+ Env.t ->
+ term ->
+ exp * Assert.t * Env.t) ref
+
+val predicate_to_exp_ref:
+ (adata:Assert.t ->
+ ?name:string ->
+ kernel_function ->
+ ?rte:bool ->
+ Env.t ->
+ predicate ->
+ exp * Assert.t * Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)