From ee1a912184d59a1fc6b2f5065bf880143893bbdc Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Wed, 18 Sep 2024 01:34:13 +0200
Subject: [PATCH] [e-acsl] fix internal predicates/terms in assertion strings
Logic normalization transforms predicates and terms from the original
code. Currently the assertion string that is shown to the user when the
assertion fails shows these transformed forms. This should not be the
case, as the user cannot understand where they stem from.
Therefore we need to determine the original forms and use them when
generating the assertion strings.
This commit extends the memoization modules in Logic_normalizer to be
bidirectional maps, such that the original form of a term or predicate
can be determined.
---
.../e-acsl/src/code_generator/assert.ml | 6 +++++-
.../arith/oracle/gen_extended_quantifiers.c | 4 ++--
.../e-acsl/tests/arith/oracle/gen_functions.c | 13 +++++-------
.../examples/oracle/gen_functions_contiki.c | 3 +--
.../oracle/gen_extended_quantifiers.c | 2 +-
.../e-acsl/tests/libc/oracle/gen_mem.c | 20 +++++++++----------
.../tests/temporal/oracle/gen_t_memcpy.c | 12 +++++------
7 files changed, 30 insertions(+), 30 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index a49425e216c..10512e24c50 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -203,7 +203,10 @@ let register ~loc ?(force=false) name e adata =
adata
let register_term ~loc ?force t e adata =
- let name = Format.asprintf "@[%a@]" Printer.pp_term t in
+ let name =
+ Format.asprintf "@[%a@]"
+ Printer.pp_term (Logic_normalizer.get_orig_term t)
+ in
register ~loc name ?force e adata
let register_pred ~loc env ?force p e adata =
@@ -212,6 +215,7 @@ let register_pred ~loc env ?force p e adata =
because they should be the only predicate in an assertion clause. *)
adata
else
+ let p = Logic_normalizer.get_orig_pred p in
let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
register ~loc name ?force e adata
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
index 598514c5351..0b32c4d4818 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
@@ -404,7 +404,7 @@ int main(void)
}
}
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
- "\\sum(2, 10, \\lambda integer k; k - 2 >= 0? 1: 0)",
+ "\\numof(2, 10, \\lambda integer k; k - 2 >= 0)",
0,__gen_e_acsl_accumulator_8);
__gen_e_acsl_assert_data_8.blocking = 1;
__gen_e_acsl_assert_data_8.kind = "Assertion";
@@ -450,7 +450,7 @@ int main(void)
}
}
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_9,
- "\\sum(4294967295U - 5, 4294967295U, \\lambda integer k; k % 2 == 1? 1: 0)",
+ "\\numof(4294967295U - 5, 4294967295U, \\lambda integer k; k % 2 == 1)",
0,__gen_e_acsl_accumulator_9);
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "Assertion";
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index fe353dc2402..9f9358add8a 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -464,9 +464,8 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_16 =
{.values = (void *)0};
__gen_e_acsl_p_here_here_2 = __gen_e_acsl_p_here_here(27);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,
- "__gen_e_acsl_p_here_here(27)",0,
- __gen_e_acsl_p_here_here_2);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,"p_here(27)",
+ 0,__gen_e_acsl_p_here_here_2);
__gen_e_acsl_assert_data_16.blocking = 1;
__gen_e_acsl_assert_data_16.kind = "Assertion";
__gen_e_acsl_assert_data_16.pred_txt = "p_here(27)";
@@ -482,9 +481,8 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_17 =
{.values = (void *)0};
__gen_e_acsl_f_here_here_2 = __gen_e_acsl_f_here_here(27);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_17,
- "__gen_e_acsl_f_here_here(27)",0,
- __gen_e_acsl_f_here_here_2);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_17,"f_here(27)",
+ 0,__gen_e_acsl_f_here_here_2);
__gen_e_acsl_assert_data_17.blocking = 1;
__gen_e_acsl_assert_data_17.kind = "Assertion";
__gen_e_acsl_assert_data_17.pred_txt = "f_here(27) == 27";
@@ -501,8 +499,7 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_18 =
{.values = (void *)0};
__gen_e_acsl_f3_here_2 = __gen_e_acsl_f3_here(5);
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_18,
- "__gen_e_acsl_f3_here(5)",0,
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_18,"f3(5)",0,
__gen_e_acsl_f3_here_2);
__gen_e_acsl_assert_data_18.blocking = 1;
__gen_e_acsl_assert_data_18.kind = "Assertion";
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
index 8b29d96a787..6cf2e62d180 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
+++ b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
@@ -61,8 +61,7 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_length_here_2 = __gen_e_acsl_length_here(l);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"l",(void *)l);
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data,
- "__gen_e_acsl_length_here(l)",0,
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data,"length(l)",0,
__gen_e_acsl_length_here_2);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
index 80cf5b33238..82a6d17354d 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
@@ -212,7 +212,7 @@ int main(void)
__gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,
- "\\sum(2, 10, \\lambda integer k; k - 2 >= 0? 1: 0)",
+ "\\numof(2, 10, \\lambda integer k; k - 2 >= 0)",
0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_3));
__gen_e_acsl_assert_data_3.blocking = 1;
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
index 62c4f08984c..81522c937fe 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
@@ -420,8 +420,8 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n)
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"s",s);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_s: __gen_e_acsl_valid_or_empty_here(s, n)",
- 0,__gen_e_acsl_valid_or_empty_here_2);
+ "valid_s: valid_or_empty(s, n)",0,
+ __gen_e_acsl_valid_or_empty_here_2);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(s, n)";
@@ -484,8 +484,8 @@ void *__gen_e_acsl_memmove(void *dest, void const *src, size_t n)
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
- 0,__gen_e_acsl_valid_or_empty_here_3);
+ "valid_dest: valid_or_empty(dest, n)",0,
+ __gen_e_acsl_valid_or_empty_here_3);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
@@ -504,8 +504,8 @@ void *__gen_e_acsl_memmove(void *dest, void const *src, size_t n)
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
(void *)src);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
- 0,__gen_e_acsl_valid_read_or_empty_here_2);
+ "valid_src: valid_read_or_empty(src, n)",0,
+ __gen_e_acsl_valid_read_or_empty_here_2);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Precondition";
__gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";
@@ -594,8 +594,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
- 0,__gen_e_acsl_valid_or_empty_here_4);
+ "valid_dest: valid_or_empty(dest, n)",0,
+ __gen_e_acsl_valid_or_empty_here_4);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
@@ -614,8 +614,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
(void *)src);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
- 0,__gen_e_acsl_valid_read_or_empty_here_3);
+ "valid_src: valid_read_or_empty(src, n)",0,
+ __gen_e_acsl_valid_read_or_empty_here_3);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Precondition";
__gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index 2ee59ac2142..e03df15a615 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -756,8 +756,8 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n)
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"s",s);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_s: __gen_e_acsl_valid_or_empty_here(s, n)",
- 0,__gen_e_acsl_valid_or_empty_here_2);
+ "valid_s: valid_or_empty(s, n)",0,
+ __gen_e_acsl_valid_or_empty_here_2);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(s, n)";
@@ -851,8 +851,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
- 0,__gen_e_acsl_valid_or_empty_here_3);
+ "valid_dest: valid_or_empty(dest, n)",0,
+ __gen_e_acsl_valid_or_empty_here_3);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
@@ -871,8 +871,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
(void *)src);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
- 0,__gen_e_acsl_valid_read_or_empty_here_2);
+ "valid_src: valid_read_or_empty(src, n)",0,
+ __gen_e_acsl_valid_read_or_empty_here_2);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Precondition";
__gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";
--
GitLab