From 35d900faa860ee1f083d5018352871f12d8fe98d Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 6 Oct 2020 10:52:44 +0200
Subject: [PATCH] [eacsl:codegen] Fix soundness bug when translating a range
with a logic variable
---
src/plugins/e-acsl/src/analyses/typing.ml | 2 +-
src/plugins/e-acsl/src/analyses/typing.mli | 7 +++++--
src/plugins/e-acsl/src/code_generator/memory_translate.ml | 2 +-
src/plugins/e-acsl/src/code_generator/translate.ml | 5 +++++
src/plugins/e-acsl/tests/memory/ranges_in_builtins.c | 3 +++
5 files changed, 15 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index e413aea96d1..df114cc3a82 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -707,7 +707,7 @@ let type_term ~use_gmp_opt ?ctx t =
Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
ignore (type_term ~use_gmp_opt ?ctx t)
-let type_named_predicate ?(must_clear=true) p =
+let type_named_predicate ~must_clear p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
Printer.pp_predicate p;
if must_clear then begin
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 7a7fd0f80d5..c35a8e81952 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -101,9 +101,12 @@ val type_term: use_gmp_opt:bool -> ?ctx:number_ty -> term -> unit
[use_gmp_opt] is false, then the conversion to the given context is done
even if -e-acsl-gmp-only is set. *)
-val type_named_predicate: ?must_clear:bool -> predicate -> unit
+val type_named_predicate: must_clear:bool -> predicate -> unit
(** Compute the type of each term of the given predicate.
- Set {!must_clear} to false in order to not reset the environment. *)
+
+ If {!must_clear} is true, the typing environment is reset before translating
+ the predicate. The environment should be reset when translating a new
+ assertion, and kept otherwise. *)
val clear: unit -> unit
(** Remove all the previously computed types. *)
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 2b496a89f87..f691e41ca97 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -420,7 +420,7 @@ let call_with_tset ~loc ~arg_from_range ~arg_from_term ?(prepend_n_args=false) k
in
(* There's no more quantifiers in the arguments now, we can call back
[prediate_to_exp] to translate the predicate as usual *)
- Typing.type_named_predicate ~must_clear:true p_quantified;
+ Typing.type_named_predicate ~must_clear:false p_quantified;
!predicate_to_exp_ref kf env p_quantified
| [] ->
(* No arguments require quantifiers, so we can directly translate the
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 860c165a18a..9ad2815d009 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1050,6 +1050,11 @@ and predicate_to_exp ?name kf ?rte env p =
e
and generalized_untyped_predicate_to_exp ?name kf ?rte ?must_clear_typing 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 must_clear = match must_clear_typing with None -> rte | Some b -> b in
Typing.type_named_predicate ~must_clear p;
diff --git a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
index 4cb9d45b44a..7af22946ecf 100644
--- a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
@@ -48,6 +48,9 @@ int main(void) {
/*@ assert !\valid_read(&t3[6][1][0] + (2..10)); */
/*@ assert \valid_read(&t3[(n-1)..(n+2)][1]); */
+ int t4[10][10][10];
+ /*@ assert \let x = 5; \valid(&t4[4][0..x][2]); */
+
struct S s;
s.a[0] = 7; s.a[1] = 8;
/*@ assert \initialized(&s.a[0] + (1..1)); */ ;
--
GitLab