From f70cb65865962c6c95251f19d71be0ba25a6fae5 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Mon, 16 Sep 2024 22:44:36 +0200
Subject: [PATCH] [e-acsl] fix logic variable escaping its scope
When translating a function we must ensure that it cannot re-use any
expressions resulting from translating logic variables from its call
site. One might think that this may not occur, since logic variables are
unique. However sometimes the same logic function needs to be translated
twice (with different signatures). In that case there are indeed
indentical logic variables for different C code to be generated, and
re-using that code would be erroneous.
See the pathological example from the previous commit.
This commit fixes this by clearing the map of logic bindings before
translating a function body.
---
src/plugins/e-acsl/doc/Changelog | 1 +
src/plugins/e-acsl/src/code_generator/env.ml | 1 +
src/plugins/e-acsl/src/code_generator/env.mli | 2 ++
src/plugins/e-acsl/src/code_generator/logic_functions.ml | 3 +++
src/plugins/e-acsl/src/code_generator/translate_terms.ml | 3 ++-
src/plugins/e-acsl/tests/constructs/oracle/gen_let.c | 3 +--
src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle | 3 +--
7 files changed, 11 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index abd2c08e061..bdd66e6ceac 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,7 @@
Plugin E-ACSL <next-release>
###############################################################################
+-* E-ACSL [2024-09-16] fix logic variable escaping its scope
-* E-ACSL [2024-09-03] handle negative integers generated by RTE
-* E-ACSL [2024-08-30] fix typing exception occurring for applications
of axiomatically defined premises and logic functions
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 15fec0f05c3..e4f729209f8 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -310,6 +310,7 @@ let rtl_call_to_new_var ~loc ?scope ?name env kf t ty func_name args =
exp, env
module Logic_binding = struct
+ let clear env = {env with var_mapping = Logic_var.Map.empty}
let add_binding env logic_v vi =
try
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 91d3aed298a..40569ada0a0 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -66,6 +66,8 @@ val rtl_call_to_new_var:
*)
module Logic_binding: sig
+ val clear : t -> t
+
val add: ?ty:typ -> t -> kernel_function -> logic_var -> varinfo * exp * t
(* Add a new C binding to the list of bindings for the logic variable. *)
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 0856f842134..289cc2bb6f4 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -203,6 +203,9 @@ let generate_kf ~loc fname env params_ty ret_ty params_ival li =
Delay its generation after filling the memoization table (for termination
of recursive function calls) *)
let gen_body () =
+ let env = (* cannot use bindings from other functions (the use site) *)
+ Env.Logic_binding.clear env
+ in
let env = Env.push env in
(* fill the typing environment with the function's parameters
before generating the code (code generation invokes typing) *)
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 a2dcfd36b7b..e898f1dca19 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -759,7 +759,8 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
| Tapp(li, [], args)
| Tapp(li, [BuiltinLabel Here], args) ->
let e, adata, env =
- Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args in
+ Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args
+ in
let adata = Assert.register_term ~loc t e adata in
e, adata, env, Analyses_types.C_number, "app"
| Tapp(_, _ :: _, _) ->
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
index 60957b9d31a..4bbf7e47df2 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
@@ -53,8 +53,7 @@ int __gen_e_acsl_f(int x)
long __gen_e_acsl_if_3;
__gen_e_acsl_f_5 = __gen_e_acsl_f_2(0);
__gen_e_acsl_v = __gen_e_acsl_f_5;
- /*@ assert Eva: initialization: \initialized(&__gen_e_acsl_v_2); */
- if (0L == __gen_e_acsl_v_2) __gen_e_acsl_if_3 = x - 1L;
+ if (0L == __gen_e_acsl_v) __gen_e_acsl_if_3 = x - 1L;
else __gen_e_acsl_if_3 = 0L;
__gen_e_acsl_if_4 = __gen_e_acsl_if_3;
}
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
index d3f26b8698b..c8232575390 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
@@ -1,4 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] let.c:12: Warning:
- accessing uninitialized left-value. assert \initialized(&__gen_e_acsl_v_2);
+[eva:alarm] let.c:17: Warning: assertion got status unknown.
--
GitLab