From fceda1b22dedef49dc9fbfc627c7ce437b5ca4ae Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 9 Aug 2022 17:08:26 +0200
Subject: [PATCH] [e-acsl] improve support for functions returning structures
---
.../e-acsl/src/code_generator/assigns.ml | 19 +++--
.../e-acsl/src/code_generator/assigns.mli | 6 +-
.../src/code_generator/logic_functions.ml | 12 ++-
src/plugins/e-acsl/tests/arith/functions.c | 1 +
.../tests/arith/oracle/functions.res.oracle | 18 ++++-
.../e-acsl/tests/arith/oracle/gen_functions.c | 73 ++++++++++++-------
6 files changed, 87 insertions(+), 42 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/assigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml
index eaa80b49e8f..bf8e2dddc4c 100644
--- a/src/plugins/e-acsl/src/code_generator/assigns.ml
+++ b/src/plugins/e-acsl/src/code_generator/assigns.ml
@@ -81,10 +81,15 @@ let rec get_assigns_from ~loc env lprofile lv =
(* Special case when the function takes an extra argument as its result:
For the argument [__e_acsl_mpz_t *__retres_arg], this function generates the
- expression [( *__retres_arg )[0]] *)
-let get_gmp_integer ~loc vi =
- Smart_exp.lval
- ~loc
- (Mem
- (Smart_exp.lval ~loc (Var vi, NoOffset)),
- (Index (Cil.zero ~loc, NoOffset)))
+ expression [( *__retres_arg )[0]]. For a struct argument, this function just
+ generates the variable corresponding to the argument. *)
+let get_assigned_var ~loc vi ret_gmp =
+ let var =
+ if ret_gmp then
+ Smart_exp.lval
+ ~loc
+ (Mem
+ (Smart_exp.lval ~loc (Var vi, NoOffset)),
+ (Index (Cil.zero ~loc, NoOffset)))
+ else Smart_exp.lval ~loc (Var vi, NoOffset)
+ in Logic_utils.expr_to_term var
diff --git a/src/plugins/e-acsl/src/code_generator/assigns.mli b/src/plugins/e-acsl/src/code_generator/assigns.mli
index c245cd4de58..650214584a2 100644
--- a/src/plugins/e-acsl/src/code_generator/assigns.mli
+++ b/src/plugins/e-acsl/src/code_generator/assigns.mli
@@ -31,7 +31,7 @@ val get_assigns_from :
(* @returns the list of expressions that are allowed to be used to assign the
the result of a logic function *)
-val get_gmp_integer :
- loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.exp
+val get_assigned_var :
+ loc:Cil_types.location -> Cil_types.varinfo -> bool -> Cil_types.term
(* @returns the expression that gets assigned when the result of the function is
- a pointer on a GMP type *)
+ passed as an additional argument *)
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 331ec21a4ea..a0b88104c04 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -55,7 +55,14 @@ let term_to_exp_ref
(* @return true iff the result of the function is provided by reference as the
first extra argument at each call *)
-let result_as_extra_argument = Gmp_types.Z.is_t
+let result_as_extra_argument typ =
+ let is_composite = function
+ | TComp _ | TPtr _ | TArray _ -> true
+ | TInt _ | TVoid _ | TFloat _ | TFun _ | TNamed _ | TEnum _
+ | TBuiltin_va_list _ -> false
+ in
+ Gmp_types.Z.is_t typ ||
+ is_composite typ
(* TODO: to be extended to any compound type? E.g. returning a struct is not
good practice... *)
@@ -151,6 +158,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
in
(* build the varinfo storing the result *)
let res_as_extra_arg = result_as_extra_argument ret_ty in
+ let ret_gmp = Gmp_types.Z.is_t ret_ty in
let ret_vi, ret_ty, params_with_ret, params_ty_with_ret =
let vname = "__retres" in
if res_as_extra_arg then
@@ -209,7 +217,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
let assigned_var =
Logic_const.new_identified_term
(if res_as_extra_arg then
- Logic_utils.expr_to_term (Assigns.get_gmp_integer ~loc ret_vi)
+ Assigns.get_assigned_var ~loc ret_vi ret_gmp
else
Logic_const.tresult fundec.svar.vtype)
in
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index 428a12d2cb2..f4b773c2774 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -67,6 +67,7 @@ int main(void) {
mystruct m;
m.k = 8;
m.l = 9;
+ /*@ assert \let r = t1(m); r.k == 8; */;
/*@ assert t2(t1(m)) == 17; */;
k(9);
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
index 722a30329dc..cc5b0778cf1 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
@@ -1,4 +1,7 @@
[e-acsl] beginning translation.
+[e-acsl] functions.c:70: Warning:
+ E-ACSL construct `function application' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] functions.c:48: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
@@ -46,16 +49,23 @@
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions.c:70: Warning:
+ function __e_acsl_assert_register_struct: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] functions.c:70: Warning: assertion got status unknown.
+[eva:alarm] functions.c:71: Warning:
+ function __e_acsl_assert_register_struct: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] functions.c:71: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions.c:28: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:75: Warning:
+[eva:alarm] functions.c:76: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] functions.c:75: Warning:
+[eva:alarm] functions.c:76: Warning:
function __e_acsl_assert_register_double: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:75: Warning:
+[eva:alarm] functions.c:76: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:77: Warning: assertion got status unknown.
+[eva:alarm] functions.c:78: Warning: assertion got status unknown.
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 192abded1c0..7d6406619df 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -325,63 +325,84 @@ int main(void)
m.k = 8;
m.l = 9;
{
+ mystruct __gen_e_acsl_r;
mystruct __gen_e_acsl_t1_2;
- long __gen_e_acsl_t2_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
__gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
- __gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_2);
+ __gen_e_acsl_r = __gen_e_acsl_t1_2;
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_11,"r.k",0,
+ __gen_e_acsl_r.k);
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"m");
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"t1(m)");
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_11,"t2(t1(m))",
- 0,__gen_e_acsl_t2_2);
__gen_e_acsl_assert_data_11.blocking = 1;
__gen_e_acsl_assert_data_11.kind = "Assertion";
- __gen_e_acsl_assert_data_11.pred_txt = "t2(t1(m)) == 17";
+ __gen_e_acsl_assert_data_11.pred_txt = "\\let r = t1(m); r.k == 8";
__gen_e_acsl_assert_data_11.file = "functions.c";
__gen_e_acsl_assert_data_11.fct = "main";
__gen_e_acsl_assert_data_11.line = 70;
- __e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_11);
+ __e_acsl_assert(__gen_e_acsl_r.k == 8,& __gen_e_acsl_assert_data_11);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
}
- /*@ assert t2(t1(m)) == 17; */ ;
- __gen_e_acsl_k(9);
- double d = 2.0;
+ /*@ assert \let r = t1(m); r.k == 8; */ ;
{
- double __gen_e_acsl_f2_2;
+ mystruct __gen_e_acsl_t1_4;
+ long __gen_e_acsl_t2_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0};
- __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
- __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"d",d);
- __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"f2(d)",
- __gen_e_acsl_f2_2);
+ __gen_e_acsl_t1_4 = __gen_e_acsl_t1(m);
+ __gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_4);
+ __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"m");
+ __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"t1(m)");
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_12,"t2(t1(m))",
+ 0,__gen_e_acsl_t2_2);
__gen_e_acsl_assert_data_12.blocking = 1;
__gen_e_acsl_assert_data_12.kind = "Assertion";
- __gen_e_acsl_assert_data_12.pred_txt = "f2(d) > 0";
+ __gen_e_acsl_assert_data_12.pred_txt = "t2(t1(m)) == 17";
__gen_e_acsl_assert_data_12.file = "functions.c";
__gen_e_acsl_assert_data_12.fct = "main";
- __gen_e_acsl_assert_data_12.line = 75;
- __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_12);
+ __gen_e_acsl_assert_data_12.line = 71;
+ __e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_12);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
}
- /*@ assert f2(d) > 0; */ ;
+ /*@ assert t2(t1(m)) == 17; */ ;
+ __gen_e_acsl_k(9);
+ double d = 2.0;
{
- int __gen_e_acsl_f_sum_2;
+ double __gen_e_acsl_f2_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_13 =
{.values = (void *)0};
- __gen_e_acsl_f_sum_2 = __gen_e_acsl_f_sum(100);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_13,"f_sum(100)",
- 0,__gen_e_acsl_f_sum_2);
+ __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
+ __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_13,"d",d);
+ __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_13,"f2(d)",
+ __gen_e_acsl_f2_2);
__gen_e_acsl_assert_data_13.blocking = 1;
__gen_e_acsl_assert_data_13.kind = "Assertion";
- __gen_e_acsl_assert_data_13.pred_txt = "f_sum(100) == 100";
+ __gen_e_acsl_assert_data_13.pred_txt = "f2(d) > 0";
__gen_e_acsl_assert_data_13.file = "functions.c";
__gen_e_acsl_assert_data_13.fct = "main";
- __gen_e_acsl_assert_data_13.line = 77;
- __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
- & __gen_e_acsl_assert_data_13);
+ __gen_e_acsl_assert_data_13.line = 76;
+ __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_13);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_13);
}
+ /*@ assert f2(d) > 0; */ ;
+ {
+ int __gen_e_acsl_f_sum_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_14 =
+ {.values = (void *)0};
+ __gen_e_acsl_f_sum_2 = __gen_e_acsl_f_sum(100);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,"f_sum(100)",
+ 0,__gen_e_acsl_f_sum_2);
+ __gen_e_acsl_assert_data_14.blocking = 1;
+ __gen_e_acsl_assert_data_14.kind = "Assertion";
+ __gen_e_acsl_assert_data_14.pred_txt = "f_sum(100) == 100";
+ __gen_e_acsl_assert_data_14.file = "functions.c";
+ __gen_e_acsl_assert_data_14.fct = "main";
+ __gen_e_acsl_assert_data_14.line = 78;
+ __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
+ & __gen_e_acsl_assert_data_14);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
+ }
/*@ assert f_sum(100) == 100; */ ;
__retres = 0;
__e_acsl_memory_clean();
--
GitLab