From 52c031d1ee1d1433be62d99fcfec33d76534b591 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Mar 2019 14:45:31 +0100
Subject: [PATCH] [interval] improve non-recursive logic functions case
---
src/plugins/e-acsl/interval.ml | 90 +++++------
src/plugins/e-acsl/tests/gmp/functions.c | 4 +-
.../tests/gmp/oracle/functions.0.res.oracle | 2 -
.../e-acsl/tests/gmp/oracle/gen_functions.c | 144 ++++++++----------
4 files changed, 107 insertions(+), 133 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index f2cea60613c..03083cf1602 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -208,7 +208,7 @@ let rec infer t =
let i2 = infer t2 in
Ival.meet i1 i2
- | Tapp (li, _, _args) ->
+ | Tapp (li, _, args) ->
(match li.l_type with
| None -> assert false (* [None] only possible for predicates *)
| Some Linteger ->
@@ -216,53 +216,47 @@ let rec infer t =
| LBpred _ ->
Ival.zero_or_one
| LBterm t' ->
- let i =
- if Misc.is_recursive li then
- (* 1) Build a system of interval equations that
- constrain the solution:
- do so by returning a variable when encoutering
- a call of a recursive function instead of
- performing the usual interval inference
- BEWARE: we might be tempted to memoize the
- solution for a given function signature
- HOWEVER: it cannot be done in a straightforward
- manner due to the cases of functions that use
- C (global) variables in their definition (as the values of
- those variables can change between two function calls). *)
- let ieqs = Fixpoint.Ieqs.empty in
- let ivar, ieqs, _ = build_ieqs t ieqs [] in
- (* 2) Solve it:
- The problem is probably undecidable in the general case.
- Thus we just look for reasonably precise approximations
- without being too computationally expensive:
- simply iterate over a finite set of pre-defined intervals.
- See [Fixpoint.solve] for details. *)
- let chain_of_ivalmax =
- [| Integer.one; Integer.billion_one; Integer.max_int64 |]
- (* This set can be changed based on experimental evidences,
- but it works fine for now. *)
- in
- let i = Fixpoint.solve ieqs ivar chain_of_ivalmax in
- i
- else begin
- List.iter2
- (fun lv arg ->
- try
- let i = interv_of_typ_containing_interv (infer arg) in
- Env.add lv i
- with Not_an_integer ->
- ())
- li.l_profile
- _args;
- let i =
- try infer t'
- with Not_an_integer -> Ival.inject_range None None
- in
- List.iter (fun lv -> Env.remove lv) li.l_profile;
- i
- end
- in
- i
+ (* TODO: should not be necessary to distinguish the recursive case.
+ Stack overflow if not distingued *)
+ if Misc.is_recursive li then
+ (* 1) Build a system of interval equations that constrain the
+ solution: do so by returning a variable when encoutering a call
+ of a recursive function instead of performing the usual interval
+ inference BEWARE: we might be tempted to memoize the solution
+ for a given function signature HOWEVER: it cannot be done in a
+ straightforward manner due to the cases of functions that use C
+ (global) variables in their definition (as the values of those
+ variables can change between two function calls). *)
+ let ieqs = Fixpoint.Ieqs.empty in
+ let ivar, ieqs, _ = build_ieqs t ieqs [] in
+ (* 2) Solve it:
+ The problem is probably undecidable in the general case.
+ Thus we just look for reasonably precise approximations
+ without being too computationally expensive:
+ simply iterate over a finite set of pre-defined intervals.
+ See [Fixpoint.solve] for details. *)
+ let chain_of_ivalmax =
+ [| Integer.one; Integer.billion_one; Integer.max_int64 |]
+ (* This set can be changed based on experimental evidences,
+ but it works fine for now. *)
+ in
+ Fixpoint.solve ieqs ivar chain_of_ivalmax
+ else begin (* non-recursive case *)
+ (* add the arguments to the context *)
+ List.iter2
+ (fun lv arg ->
+ try
+ let i = infer arg in
+ Env.add lv i
+ with Not_an_integer ->
+ ())
+ li.l_profile
+ args;
+ let i = infer t' in
+ (* remove arguments from the context *)
+ List.iter (fun lv -> Env.remove lv) li.l_profile;
+ i
+ end
| LBnone ->
Error.not_yet "logic functions with no definition nor reads clause"
| LBreads _ ->
diff --git a/src/plugins/e-acsl/tests/gmp/functions.c b/src/plugins/e-acsl/tests/gmp/functions.c
index 61bb3857359..28bc4017c14 100644
--- a/src/plugins/e-acsl/tests/gmp/functions.c
+++ b/src/plugins/e-acsl/tests/gmp/functions.c
@@ -20,7 +20,7 @@ typedef struct mystruct mystruct;
/*@ logic mystruct t1(mystruct m) = m; */
/*@ logic integer t2(mystruct m) = m.k + m.l; */
-// To test function call in other than assert:
+// To test function call in other clauses than assert:
/*@ predicate k_pred(integer x) = x > 0; */
/*@ requires k_pred(x); */
void k(int x) {}
@@ -68,4 +68,4 @@ int main (void) {
/*@ assert f2(d) > 0; */ ;
/*@ assert p_notyet(27); */ ;
/*@ assert f_notyet(27) == 27; */ ;
-}
\ No newline at end of file
+}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
index c60cf271f5f..e336cb46d69 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
@@ -32,8 +32,6 @@
[eva] using specification for function __gmpz_clear
[eva:alarm] tests/gmp/functions.c:44: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:47: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/functions.c:48: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
index 9e926f5e7cf..fd3c27e93ad 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -17,19 +17,19 @@ int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
*/
int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
-int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg);
-
int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
-void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+void __gen_e_acsl_f1_4(__e_acsl_mpz_struct * __retres_arg,
__e_acsl_mpz_struct * __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
-void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+int __gen_e_acsl_f1_2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
@@ -126,59 +126,59 @@ int main(void)
}
/*@ assert p2(x, f1(3, 4)); */
{
- long __gen_e_acsl_f1_tapp_2;
+ int __gen_e_acsl_f1_tapp_2;
int __gen_e_acsl_p2_tapp_3;
- __gen_e_acsl_f1_tapp_2 = __gen_e_acsl_f1(3,4);
- __gen_e_acsl_p2_tapp_3 = __gen_e_acsl_p2_3(x,__gen_e_acsl_f1_tapp_2);
+ __gen_e_acsl_f1_tapp_2 = __gen_e_acsl_f1_2(3,4);
+ __gen_e_acsl_p2_tapp_3 = __gen_e_acsl_p2(x,__gen_e_acsl_f1_tapp_2);
__e_acsl_assert(__gen_e_acsl_p2_tapp_3,(char *)"Assertion",
(char *)"main",(char *)"p2(x, f1(3, 4))",47);
}
/*@ assert f1(9, 99999999999999999999999999999) > 0; */
{
- __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl__3;
__e_acsl_mpz_t __gen_e_acsl_f1_tapp_3;
- __e_acsl_mpz_t __gen_e_acsl__5;
- int __gen_e_acsl_gt_3;
- __gmpz_init_set_str(__gen_e_acsl__4,"99999999999999999999999999999",10);
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_gt_2;
+ __gmpz_init_set_str(__gen_e_acsl__3,"99999999999999999999999999999",10);
__gmpz_init(__gen_e_acsl_f1_tapp_3);
/*@ assert
Eva: initialization:
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3);
*/
- __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3,9,
- (__e_acsl_mpz_struct *)__gen_e_acsl__4);
- __gmpz_init_set_si(__gen_e_acsl__5,0L);
- __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
+ __gen_e_acsl_f1_3((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_3,9,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__3);
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
(char *)"f1(9, 99999999999999999999999999999) > 0",48);
- __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl__3);
__gmpz_clear(__gen_e_acsl_f1_tapp_3);
- __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl__4);
}
/*@ assert
f1(99999999999999999999999999999, 99999999999999999999999999999) ≡
199999999999999999999999999998;
*/
{
- __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl__5;
__e_acsl_mpz_t __gen_e_acsl_f1_tapp_4;
- __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl__6;
int __gen_e_acsl_eq;
- __gmpz_init_set_str(__gen_e_acsl__6,"99999999999999999999999999999",10);
+ __gmpz_init_set_str(__gen_e_acsl__5,"99999999999999999999999999999",10);
__gmpz_init(__gen_e_acsl_f1_tapp_4);
- __gen_e_acsl_f1_3((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_4,
- (__e_acsl_mpz_struct *)__gen_e_acsl__6,
- (__e_acsl_mpz_struct *)__gen_e_acsl__6);
- __gmpz_init_set_str(__gen_e_acsl__7,"199999999999999999999999999998",10);
+ __gen_e_acsl_f1_4((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl__5);
+ __gmpz_init_set_str(__gen_e_acsl__6,"199999999999999999999999999998",10);
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998",
49);
- __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl__5);
__gmpz_clear(__gen_e_acsl_f1_tapp_4);
- __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl__6);
}
/*@ assert g(x) ≡ x; */
{
@@ -309,51 +309,58 @@ long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
return __retres;
}
-void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg)
{
- __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_y_2;
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __gmpz_init_set(__gen_e_acsl_y_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)__gen_e_acsl_x_arg);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_clear(__gen_e_acsl_y_2);
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ return;
+}
+
+int __gen_e_acsl_f1_2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+{
+ long __retres;
+ __retres = (int)(__gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg);
+ return __retres;
+}
+
+void __gen_e_acsl_f1_4(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
__e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
__e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gmpz_init_set(__gen_e_acsl_x_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
__gmpz_init_set(__gen_e_acsl_y_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)__gen_e_acsl_x_arg);
__gmpz_init(__gen_e_acsl_add_3);
__gmpz_add(__gen_e_acsl_add_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
__gmpz_init_set(__retres_arg,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_clear(__gen_e_acsl_y_3);
__gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl_y_3);
__gmpz_clear(__gen_e_acsl_add_3);
return;
}
-void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __e_acsl_mpz_t __gen_e_acsl_y_4;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set(__gen_e_acsl_x_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
- __gmpz_init_set(__gen_e_acsl_y_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_4));
- __gmpz_init_set(__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- __gmpz_clear(__gen_e_acsl_y_4);
- __gmpz_clear(__gen_e_acsl_add_4);
- return;
-}
-
int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg)
{
@@ -380,31 +387,6 @@ int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
return __retres;
}
-int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg)
-{
- int __retres;
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __e_acsl_mpz_t __gen_e_acsl_y_2;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_gt_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)__gen_e_acsl_x_arg);
- __gmpz_init_set_si(__gen_e_acsl_y_2,__gen_e_acsl_y_arg);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __retres = __gen_e_acsl_gt_2 > 0;
- __gmpz_clear(__gen_e_acsl_x_2);
- __gmpz_clear(__gen_e_acsl_y_2);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__3);
- return __retres;
-}
-
int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
{
int __retres;
--
GitLab