From 7e510b1e8b757c1656b2badc2482e2c7137f5986 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Mon, 23 May 2022 14:06:14 +0200
Subject: [PATCH] [e-acsl] code review
---
.../e-acsl/src/code_generator/assert.ml | 32 +++++++++----------
.../e-acsl/src/code_generator/assert.mli | 14 ++++----
.../e-acsl/src/code_generator/contract.ml | 3 +-
src/plugins/e-acsl/src/code_generator/libc.ml | 8 ++---
.../e-acsl/src/code_generator/logic_array.ml | 8 ++---
.../e-acsl/src/code_generator/loops.ml | 13 +++-----
.../src/code_generator/memory_translate.ml | 3 +-
.../src/code_generator/translate_ats.ml | 2 +-
.../code_generator/translate_predicates.ml | 12 +++----
.../src/code_generator/translate_rtes.ml | 4 +--
.../src/code_generator/translate_terms.ml | 26 +++++++--------
11 files changed, 58 insertions(+), 67 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index 22335bcb773..d44043c3078 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -166,12 +166,9 @@ let add_pending_register_data ~loc { data_ptr } name e =
let name = Cil.mkString ~loc name in
let args = data_ptr :: name :: args in
let stmt = Smart_stmt.rtl_call ~loc fct args in
- let queue =
- if Stack.is_empty pending_register_data
- then Queue.create ()
- else Stack.pop pending_register_data in
- Queue.add stmt queue;
- Stack.push queue pending_register_data
+ match Stack.top_opt pending_register_data with
+ | None -> Stack.push (Queue.create()) pending_register_data
+ | Some queue -> Queue.add stmt queue
let do_pending_register_data env =
if Stack.is_empty pending_register_data then env
@@ -182,9 +179,10 @@ let do_pending_register_data env =
else
let stmt = Queue.pop queue in
do_queue (Env.add_stmt env stmt)
- in do_queue env
+ in
+ do_queue env
-let register ~loc env ?(force=false) name e adata =
+let register ~loc ?(force=false) name e adata =
if Options.Assert_print_data.get () then
match adata, e.enode with
| Some adata, Const _ when not force ->
@@ -195,31 +193,31 @@ let register ~loc env ?(force=false) name e adata =
name "3" and value [3].
The registration can be forced for expressions like [sizeof(int)] for
instance that are [Const] values but not directly known. *)
- Some adata, env
+ Some adata
| Some adata, _ ->
let adata = { adata with data_registered = true } in
add_pending_register_data ~loc adata name e;
- Some adata, env
- | None, _ -> None, env
+ Some adata
+ | None, _ -> None
else
- adata, env
+ adata
-let register_term ~loc env ?force t e adata =
+let register_term ~loc ?force t e adata =
let name = Format.asprintf "@[%a@]" Printer.pp_term t in
- register ~loc env name ?force e adata
+ register ~loc name ?force e adata
let register_pred ~loc env ?force p e adata =
if Env.annotation_kind env == RTE then
(* When translating RTE, we do not want to print the result of the predicate
because they should be the only predicate in an assertion clause. *)
- adata, env
+ adata
else
let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
- register ~loc env name ?force e adata
+ register ~loc name ?force e adata
let register_pred_or_term ~loc env ?force pot e adata =
match pot with
- | PoT_term t -> register_term ~loc env ?force t e adata
+ | PoT_term t -> register_term ~loc ?force t e adata
| PoT_pred p -> register_pred ~loc env ?force p e adata
let kind_to_string loc k =
diff --git a/src/plugins/e-acsl/src/code_generator/assert.mli b/src/plugins/e-acsl/src/code_generator/assert.mli
index c3e1492780b..d3c5bc1f131 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.mli
+++ b/src/plugins/e-acsl/src/code_generator/assert.mli
@@ -58,18 +58,21 @@ val clean: loc:location -> Env.t -> t -> Env.t
memory allocated in the C structure will not be freed. *)
val push_pending_register_data: unit -> unit
+(** data registering must be delayed after RTE checks to avoid crashes.
+ [push_pending_register_data] adds a regisration in the pending ones that
+ will be generated after the RTE. *)
val do_pending_register_data:
Env.t -> Env.t
+(** [do_pending_register_data] performs all the pending restrations*)
val register:
loc:location ->
- Env.t ->
?force:bool ->
string ->
exp ->
t ->
- t * Env.t
+ t
(** [register ~loc env ?force name e adata] registers the data [e] corresponding
to the name [name] to the assertion context [adata].
If [force] is false (default), the data is not registered if the expression
@@ -78,12 +81,11 @@ val register:
val register_term:
loc:location ->
- Env.t ->
?force:bool ->
term ->
exp ->
t ->
- t * Env.t
+ t
(** [register_term ~loc env ?force t e adata] registers the data [e]
corresponding to the term [t] to the assertion context [adata]. The
parameter [force] has the same signification than for the function
@@ -96,7 +98,7 @@ val register_pred:
predicate ->
exp ->
t ->
- t * Env.t
+ t
(** [register_pred ~loc env ?force p e adata] registers the data [e]
corresponding to the predicate [p] to the assertion context [adata]. The
parameter [force] has the same signification than for the function
@@ -109,7 +111,7 @@ val register_pred_or_term:
pred_or_term ->
exp ->
t ->
- t * Env.t
+ t
(** [register_pred_or_term ~loc kf env ?force pot e adata] registers the data
[e] corresponding to the predicate or term [pot] to the assertion context
[adata]. The parameter [force] has the same signification than for the
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 879ee0ceadf..7df4b992fbd 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -507,10 +507,9 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract
(* Create assertions for complete and disjoint behaviors checks *)
let create_assert_stmt env bop msg =
let adata, env = Assert.empty ~loc kf env in
- let adata, env =
+ let adata =
Assert.register
~loc
- env
"number of active behaviors"
active_bhvrs_e
adata
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 2121d714196..ac785dbf7b4 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -224,7 +224,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
Logic_const.prel ~loc (Rge, t, Cil.lzero ~loc ())
in
let adata, env = Assert.empty ~loc kf env in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
let assertion, env =
Assert.runtime_check
~adata
@@ -248,9 +248,9 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
let upper_guard_pp = Logic_const.prel ~loc (Rle, t, sizet_max_t) in
let upper_guard = Cil.mkBinOp ~loc Le e sizet_max_e in
let adata, env = Assert.empty ~loc kf env in
- let adata, env = Assert.register_term ~loc env t e adata in
- let adata, env =
- Assert.register ~loc env "SIZE_MAX" sizet_max_e adata
+ let adata = Assert.register_term ~loc t e adata in
+ let adata =
+ Assert.register ~loc "SIZE_MAX" sizet_max_e adata
in
let assertion, env =
Assert.runtime_check
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index a156e946340..571e94bb1d1 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -242,12 +242,8 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
let p = { p with pred_name = "array_coercion" :: p.pred_name } in
Typing.preprocess_predicate (Env.Local_vars.get env) p;
let adata, env = Assert.empty ~loc kf env in
- let adata, env =
- Assert.register ~loc env "destination length" len adata
- in
- let adata, env =
- Assert.register ~loc env "current length" len_orig adata
- in
+ let adata = Assert.register ~loc "destination length" len adata in
+ let adata = Assert.register ~loc "current length" len_orig adata in
let stmt, env =
Assert.runtime_check ~adata ~pred_kind:Assert RTE kf env e p
in
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 11e6b986d01..e37356f2704 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -131,18 +131,16 @@ let handle_annotations env kf stmt =
Printer.pp_term t
in
let adata, env = Assert.empty ~loc kf env in
- let adata, env =
+ let adata =
Assert.register
~loc
- env
(Format.asprintf "old %a" Printer.pp_term t_old)
e_old
adata
in
- let adata, env =
+ let adata =
Assert.register
~loc
- env
(Format.asprintf "current %a" Printer.pp_term t)
e
adata
@@ -180,10 +178,9 @@ let handle_annotations env kf stmt =
Printer.pp_relation Rge
in
let adata1, env = Assert.empty ~loc kf env in
- let adata1, env =
+ let adata1 =
Assert.register
~loc
- env
(Format.asprintf "old %a" Printer.pp_term t)
e_old
adata1
@@ -223,10 +220,10 @@ let handle_annotations env kf stmt =
in
Assert.register
~loc
- env
(Format.asprintf "current %a" Printer.pp_term t)
e
- adata2
+ adata2,
+ env
else
adata2, env
in
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 28c79c7a0fd..c500760a4a1 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -309,10 +309,9 @@ let term_to_ptr_and_size ~adata ~loc kf env t =
in
let ty = Misc.cty t.term_type in
let sizeof = Smart_exp.ptr_sizeof ~loc ty in
- let adata, env =
+ let adata =
Assert.register
~loc:t.term_loc
- env
(Format.asprintf "%a" Printer.pp_exp sizeof)
sizeof
adata
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index db66a9ec78b..0d12bfa2e85 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -526,7 +526,7 @@ let to_exp ~loc ~adata kf env pot label =
else
Smart_exp.lval ~loc (Cil.var vi), env
in
- let adata, env=
+ let adata =
Assert.register_pred_or_term ~loc env pot e adata
in
e, adata, env
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index 74c612f88de..55ae1ad1f49 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -81,7 +81,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
| 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 env p e adata in
+ let adata = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pdangling _ -> Env.not_yet env "\\dangling"
| Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
@@ -203,7 +203,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
e, adata, env
| Pforall _ | Pexists _ ->
let e, env = Quantif.quantif_to_exp kf env p in
- let adata, env = Assert.register_pred ~loc env p e adata in
+ let adata = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pat(p', label) ->
if inplace then
@@ -221,7 +221,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
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 env p e adata in
+ let adata = Assert.register_pred ~loc env p e adata in
e, adata, env
in
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
@@ -260,7 +260,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
tlist
p
in
- let adata, env = Assert.register_pred ~loc env p e adata in
+ let adata = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pinitialized(BuiltinLabel Here, t) ->
let e, adata, env =
@@ -283,7 +283,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
[ t ]
p
in
- let adata, env = Assert.register_pred ~loc env p e adata in
+ let adata = Assert.register_pred ~loc env p e adata in
e, adata, env)
in
e, adata, env
@@ -293,7 +293,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
let e, adata, env =
Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
in
- let adata, env = Assert.register_pred ~loc env p e adata in
+ let adata = Assert.register_pred ~loc env p e adata in
e, adata, env
| Pfreeable _ -> Env.not_yet env "labeled \\freeable"
| Pfresh _ -> Env.not_yet env "\\fresh"
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
index 85349be86be..6c54a45e3fb 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
@@ -68,8 +68,8 @@ let exp ?filter kf env e =
| None -> l
in
List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
- let env = rte_annots Printer.pp_exp e kf env l
- in Assert.do_pending_register_data env
+ let env = rte_annots Printer.pp_exp e kf env l in
+ Assert.do_pending_register_data env
let () =
Translate_terms.translate_rte_exp_ref := exp;
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index c5530b377bc..c9672f2a0f1 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -256,7 +256,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
let final_stmt = (Cil.mkBlock [ init_k_stmt; for_stmt ]) in
Env.Logic_binding.remove env k;
let env = Env.add_stmt env (Smart_stmt.block_stmt final_stmt) in
- let adata, env = Assert.register_term ~loc env t acc_as_exp adata in
+ let adata = Assert.register_term ~loc t acc_as_exp adata in
acc_as_exp, adata, env, Typed_number.C_number, ""
| _ ->
assert false
@@ -271,29 +271,29 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
| TLval lv ->
let lv, env, name = tlval_to_lval kf env lv in
let e = Smart_exp.lval ~loc lv in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, name
| TSizeOf ty ->
let e = Cil.sizeOf ~loc ty in
- let adata, env = Assert.register_term ~loc env ~force:true t e adata in
+ let adata = Assert.register_term ~loc ~force:true t e adata in
e, adata, env, Typed_number.C_number, "sizeof"
| TSizeOfE t' ->
let e', _, env = to_exp ~adata:Assert.no_data kf env t' in
let e = Cil.sizeOf ~loc (Cil.typeOf e') in
- let adata, env = Assert.register_term ~loc env ~force:true t e adata in
+ let adata = Assert.register_term ~loc ~force:true t e adata in
e, adata, env, Typed_number.C_number, "sizeof"
| TSizeOfStr s ->
let e = Cil.new_exp ~loc (SizeOfStr s) in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, "sizeofstr"
| TAlignOf ty ->
let e = Cil.new_exp ~loc (AlignOf ty) in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, "alignof"
| TAlignOfE t' ->
let e', _, env = to_exp ~adata:Assert.no_data kf env t' in
let e = Cil.new_exp ~loc (AlignOfE e') in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, "alignof"
| TUnOp(Neg | BNot as op, t') ->
let ty = Typing.get_typ ~lenv t in
@@ -746,12 +746,12 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
| TAddrOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
let e = Cil.mkAddrOf ~loc lv in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, "addrof"
| TStartOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
let e = Cil.mkAddrOrStartOf ~loc lv in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, "startof"
| Tapp(li, _, [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ])
when li.l_body = LBnone && (li.l_var_info.lv_name = "\\sum" ||
@@ -763,7 +763,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
| Tapp(li, [], args) ->
let e, adata, env =
Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, "app"
| Tapp(_, _ :: _, _) ->
Env.not_yet env "logic functions with labels"
@@ -819,7 +819,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
env
t'
in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, name
| Tbase_addr _ -> Env.not_yet env "labeled \\base_addr"
| Toffset(BuiltinLabel Here, t') ->
@@ -828,7 +828,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
let e, adata, env =
Memory_translate.call ~adata ~loc kf name size_t env t'
in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, name
| Toffset _ -> Env.not_yet env "labeled \\offset"
| Tblock_length(BuiltinLabel Here, t') ->
@@ -837,7 +837,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
let e, adata, env =
Memory_translate.call ~adata ~loc kf name size_t env t'
in
- let adata, env = Assert.register_term ~loc env t e adata in
+ let adata = Assert.register_term ~loc t e adata in
e, adata, env, Typed_number.C_number, name
| Tblock_length _ -> Env.not_yet env "labeled \\block_length"
| Tnull ->
--
GitLab