From bd46f102447cf2bad74eccae105624fa7176754d Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 6 Mar 2020 11:15:03 +0100
Subject: [PATCH] [eacsl:codegen] Update inject_in_block to support the new
clean and delete globals placements
Since `memory_clean` and `delete_globals` are added after the calls to
`inject_in_block`, this function must be updated to add the free locals
statements as last statements of the innermost block instead of before
the `memory_clean` statement in the innermost block. Additionnaly, this
fix harmonize the treatment between a classic function and the function
`main()`, and fix the issue frama-c/e-acsl#105.
---
.../e-acsl/src/code_generator/injector.ml | 40 ++++++++-----------
.../gen_at_on-purely-logic-variables.c | 18 ++++-----
.../e-acsl/tests/bts/issue-eacsl-105.c | 21 ++++++++++
.../tests/bts/oracle_ci/gen_issue-eacsl-105.c | 39 ++++++++++++++++++
.../bts/oracle_ci/issue-eacsl-105.res.oracle | 2 +
.../bts/oracle_dev/issue-eacsl-105.res.oracle | 1 +
6 files changed, 89 insertions(+), 32 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/bts/issue-eacsl-105.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index b1b2c8661b5..e0eb50c7a43 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -502,7 +502,21 @@ and inject_in_block (env: Env.t) kf blk =
| [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
(* [TODO] this piece of code could be improved *)
(* de-allocate the memory blocks observing locals *)
- let add_locals stmts =
+ let last_stmts ?return_stmt () =
+ let stmts =
+ match return_stmt with
+ | Some return_stmt ->
+ (* now that [free] stmts for [kf] have been inserted,
+ there is no more need to keep the corresponding entries in the
+ table managing them. *)
+ At_with_lscope.Free.remove_all kf;
+ (* The free statements are passed in the same order than the malloc
+ ones. In order to free the variable in the reverse order, the list
+ is reversed before appending the return statement. Moreover,
+ `rev_append` is tail recursive contrary to `append` *)
+ List.rev_append free_stmts [ return_stmt ]
+ | None -> []
+ in
if Functions.instrument kf then
List.fold_left
(fun acc vi ->
@@ -515,28 +529,8 @@ and inject_in_block (env: Env.t) kf blk =
stmts
in
(* select the precise location to inject these pieces of code *)
- let rec insert_in_innermost_last_block blk = function
- | { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
- (* keep the return (enclosed in a generated block) at the end;
- preceded by clean if any *)
- let init, tl =
- if Kernel_function.is_main kf && Mmodel_analysis.use_model () then
- free_stmts @ [ potential_clean; ret ], tl
- else
- free_stmts @ [ ret ], l
- in
- (* now that [free] stmts for [kf] have been inserted,
- there is no more need to keep the corresponding entries in the
- table managing them. *)
- At_with_lscope.Free.remove_all kf;
- blk.bstmts <-
- List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
- | { skind = Block b } :: _ ->
- insert_in_innermost_last_block b (List.rev b.bstmts)
- | l ->
- blk.bstmts <- List.fold_left (fun acc v -> v :: acc) (add_locals []) l
- in
- insert_in_innermost_last_block blk (List.rev blk.bstmts);
+ insert_as_last_stmts_in_innermost_block ~last_stmts kf blk ;
+ (* allocate the memory blocks observing locals *)
if Functions.instrument kf then
blk.bstmts <-
List.fold_left
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
index 53a78260d27..007bc6daa68 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
@@ -570,13 +570,13 @@ int main(void)
__retres = 0;
__e_acsl_delete_block((void *)(t));
__e_acsl_delete_block((void *)(& n));
- free((void *)__gen_e_acsl_at_7);
- free((void *)__gen_e_acsl_at_6);
- free((void *)__gen_e_acsl_at_5);
- free((void *)__gen_e_acsl_at_4);
- free((void *)__gen_e_acsl_at_3);
- free((void *)__gen_e_acsl_at_2);
free((void *)__gen_e_acsl_at);
+ free((void *)__gen_e_acsl_at_2);
+ free((void *)__gen_e_acsl_at_3);
+ free((void *)__gen_e_acsl_at_4);
+ free((void *)__gen_e_acsl_at_5);
+ free((void *)__gen_e_acsl_at_6);
+ free((void *)__gen_e_acsl_at_7);
__e_acsl_memory_clean();
return __retres;
}
@@ -706,10 +706,10 @@ void __gen_e_acsl_f(int *t)
"\\let m = 4; \\old(*(t + m) == -4) && \\old(*(t + (m - 4))) == 9",
"tests/arith/at_on-purely-logic-variables.c",8);
__e_acsl_delete_block((void *)(& t));
- free((void *)__gen_e_acsl_at_4);
- free((void *)__gen_e_acsl_at_3);
- free((void *)__gen_e_acsl_at_2);
free((void *)__gen_e_acsl_at);
+ free((void *)__gen_e_acsl_at_2);
+ free((void *)__gen_e_acsl_at_3);
+ free((void *)__gen_e_acsl_at_4);
return;
}
}
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c
new file mode 100644
index 00000000000..23814838fe9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-105.c
@@ -0,0 +1,21 @@
+/* run.config
+ COMMENT: frama-c/e-acsl#105, test for delete block before exiting the
+ function in the presence of early return.
+*/
+
+int f() {
+ int a = 10;
+ goto lbl_1;
+
+ lbl_2:
+ /*@ assert \valid(&a); */
+ return 0;
+
+ lbl_1:
+ goto lbl_2;
+}
+
+int main(void) {
+ f();
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c
new file mode 100644
index 00000000000..8ad1e10fa53
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c
@@ -0,0 +1,39 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+int f(void)
+{
+ int __retres;
+ int a = 10;
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_full_init((void *)(& a));
+ goto lbl_1;
+ lbl_2:
+ /*@ assert \valid(&a); */
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+ (void *)(& a),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid,"Assertion","f","\\valid(&a)",
+ "tests/bts/issue-eacsl-105.c",11);
+ }
+ __retres = 0;
+ goto return_label;
+ lbl_1: goto lbl_2;
+ return_label: {
+ __e_acsl_delete_block((void *)(& a));
+ return __retres;
+ }
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ f();
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle
new file mode 100644
index 00000000000..efd02631129
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
new file mode 100644
index 00000000000..382eac9f065
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/bts/issue-eacsl-105.c (with preprocessing)
--
GitLab