From cfaddfa0a0708313b5c387d23a259f7d8bba0ad8 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 15 Mar 2022 10:32:44 +0100
Subject: [PATCH] [e-acsl] register data after rte checks
---
.../e-acsl/src/code_generator/assert.ml | 28 +++++++++++++++++--
.../e-acsl/src/code_generator/assert.mli | 5 ++++
.../code_generator/translate_predicates.ml | 2 ++
.../src/code_generator/translate_rtes.ml | 4 ++-
4 files changed, 35 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index 3dfc72367d6..22335bcb773 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -42,6 +42,11 @@ type data = {
want to register some data in the context of [None] if we do not want to. *)
type t = data option
+let pending_register_data : stmt Queue.t Stack.t = Stack.create()
+
+let push_pending_register_data () =
+ Stack.push (Queue.create()) pending_register_data
+
let no_data = None
(** C type for the [assert_data_t] structure. *)
@@ -131,7 +136,7 @@ let ikind_to_string = function
| ILongLong -> "longlong"
| IULongLong -> "ulonglong"
-let do_register_data ~loc env { data_ptr } name e =
+let add_pending_register_data ~loc { data_ptr } name e =
let ty = Cil.typeOf e in
let fct, args =
if Gmp_types.Z.is_t ty then
@@ -161,7 +166,23 @@ let do_register_data ~loc env { 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
- Env.add_stmt env stmt
+ 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
+
+let do_pending_register_data env =
+ if Stack.is_empty pending_register_data then env
+ else
+ let queue = Stack.pop pending_register_data in
+ let rec do_queue env=
+ if Queue.is_empty queue then env
+ else
+ let stmt = Queue.pop queue in
+ do_queue (Env.add_stmt env stmt)
+ in do_queue env
let register ~loc env ?(force=false) name e adata =
if Options.Assert_print_data.get () then
@@ -177,7 +198,8 @@ let register ~loc env ?(force=false) name e adata =
Some adata, env
| Some adata, _ ->
let adata = { adata with data_registered = true } in
- Some adata, do_register_data ~loc env adata name e
+ add_pending_register_data ~loc adata name e;
+ Some adata, env
| None, _ -> None, env
else
adata, env
diff --git a/src/plugins/e-acsl/src/code_generator/assert.mli b/src/plugins/e-acsl/src/code_generator/assert.mli
index d52e907cb1e..c3e1492780b 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.mli
+++ b/src/plugins/e-acsl/src/code_generator/assert.mli
@@ -57,6 +57,11 @@ val clean: loc:location -> Env.t -> t -> Env.t
not given to [runtime_check] or [runtime_check_with_msg], otherwise the
memory allocated in the C structure will not be freed. *)
+val push_pending_register_data: unit -> unit
+
+val do_pending_register_data:
+ Env.t -> Env.t
+
val register:
loc:location ->
Env.t ->
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 571e1a98388..74c612f88de 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -311,6 +311,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
- [env]: the current environment.
- [p]: the predicate to translate. *)
and to_exp ~adata ?inplace ?name kf ?rte env p =
+ Assert.push_pending_register_data();
let p = Logic_normalizer.get_pred p in
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
Extlib.flatten
@@ -326,6 +327,7 @@ and to_exp ~adata ?inplace ?name kf ?rte env p =
~lenv:(Env.Local_vars.get env)
p
in
+ let env = Assert.do_pending_register_data env in
Extlib.nest
adata
(Typed_number.add_cast
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 8e76febe0cc..85349be86be 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
@@ -59,6 +59,7 @@ let () =
Translate_predicates.translate_rte_annots_ref := rte_annots
let exp ?filter kf env e =
+ Assert.push_pending_register_data();
let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
let l = Rte.exp kf stmt e in
let l =
@@ -67,7 +68,8 @@ let exp ?filter kf env e =
| None -> l
in
List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
- rte_annots Printer.pp_exp e kf env l
+ 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;
--
GitLab