From 03cd4ceee5bbf58b56f909c963ec714e2d6acfda Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 23 Jan 2017 15:05:56 +0100
Subject: [PATCH] fix bug with typing of unary and binary operators (fix git
issue #37)
---
src/plugins/e-acsl/doc/Changelog | 4 +++
.../e-acsl/tests/bts/oracle/gen_bts1326.c | 2 +-
src/plugins/e-acsl/tests/gmp/arith.i | 2 ++
.../e-acsl/tests/gmp/oracle/gen_arith.c | 5 ++-
.../e-acsl/tests/gmp/oracle/gen_arith2.c | 33 ++++++++++++++++++
src/plugins/e-acsl/tests/gmp/oracle/gen_at.c | 4 +--
.../runtime/oracle/gen_function_contract.c | 6 ++--
.../e-acsl/tests/runtime/oracle/gen_result.c | 4 +--
.../tests/runtime/oracle/gen_stmt_contract.c | 2 +-
src/plugins/e-acsl/typing.ml | 34 +++++++++++++------
10 files changed, 76 insertions(+), 20 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8b4811dcab9..d7d32d53a4d 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,10 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2017/01/23] Fix bug with typing of unary and binary
+ operations in a few cases: the generated code might have
+ overflowed.
+
#########################
Plugin E-ACSL 0.8 Silicon
#########################
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index dc4cf863aa5..43b8d770a10 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -121,7 +121,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
__e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",8);
- __e_acsl_assert(*__gen_e_acsl_at == (int)((((((*__gen_e_acsl_at_2)[4L] + (*__gen_e_acsl_at_3)[3L]) + (*__gen_e_acsl_at_4)[2L]) + (*__gen_e_acsl_at_5)[1L]) + (*__gen_e_acsl_at_6)[0L]) / 5L),
+ __e_acsl_assert(*__gen_e_acsl_at == (int)((((((*__gen_e_acsl_at_2)[4L] + (long)(*__gen_e_acsl_at_3)[3L]) + (*__gen_e_acsl_at_4)[2L]) + (*__gen_e_acsl_at_5)[1L]) + (*__gen_e_acsl_at_6)[0L]) / 5L),
(char *)"Postcondition",
(char *)"atp_NORMAL_computeAverageAccel",
(char *)"*\\old(AverageAccel) ==\n(((((*\\old(Accel))[4] + (*\\old(Accel))[3]) + (*\\old(Accel))[2]) +\n (*\\old(Accel))[1])\n + (*\\old(Accel))[0])\n/ 5",
diff --git a/src/plugins/e-acsl/tests/gmp/arith.i b/src/plugins/e-acsl/tests/gmp/arith.i
index eed3887af85..df97877fb14 100644
--- a/src/plugins/e-acsl/tests/gmp/arith.i
+++ b/src/plugins/e-acsl/tests/gmp/arith.i
@@ -33,5 +33,7 @@ int main(void) {
// example from the JFLA'15 paper (but for a 64-bit architecture)
/*@ assert 1 + ((z+1) / (y-123456789123456789)) == 1; */
+ /*@ assert 1 - x == -x + 1; */ // test GIT issue #37
+
return 0;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
index 56530af0d60..c73057d06af 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -69,7 +69,7 @@ int main(void)
__e_acsl_assert(3 % -2 == 1,(char *)"Assertion",(char *)"main",
(char *)"3 % -2 == 1",21);
/*@ assert ((x * 2 + (3 + y)) - 4) + (x - y) ≡ -10; */
- __e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - y) == -10,
+ __e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - (long)y) == -10,
(char *)"Assertion",(char *)"main",
(char *)"((x * 2 + (3 + y)) - 4) + (x - y) == -10",23);
/*@ assert (0 ≡ 1) ≡ !(0 ≡ 0); */
@@ -140,6 +140,9 @@ int main(void)
__gmpz_clear(__gen_e_acsl_div_2);
}
}
+ /*@ assert 1 - x ≡ -x + 1; */
+ __e_acsl_assert(1L - x == - ((long)x) + 1L,(char *)"Assertion",
+ (char *)"main",(char *)"1 - x == -x + 1",36);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
index fc3b73b7c6f..b092d8e8ad9 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
@@ -688,6 +688,39 @@ int main(void)
__gmpz_clear(__gen_e_acsl_add_6);
}
}
+ /*@ assert 1 - x ≡ -x + 1; */
+ {
+ {
+ __e_acsl_mpz_t __gen_e_acsl__60;
+ __e_acsl_mpz_t __gen_e_acsl_x_9;
+ __e_acsl_mpz_t __gen_e_acsl_sub_5;
+ __e_acsl_mpz_t __gen_e_acsl_neg_15;
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ int __gen_e_acsl_eq_21;
+ __gmpz_init_set_si(__gen_e_acsl__60,1L);
+ __gmpz_init_set_si(__gen_e_acsl_x_9,(long)x);
+ __gmpz_init(__gen_e_acsl_sub_5);
+ __gmpz_sub(__gen_e_acsl_sub_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__60),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_9));
+ __gmpz_init(__gen_e_acsl_neg_15);
+ __gmpz_neg(__gen_e_acsl_neg_15,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_9));
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_15),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__60));
+ __gen_e_acsl_eq_21 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+ __e_acsl_assert(__gen_e_acsl_eq_21 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"1 - x == -x + 1",36);
+ __gmpz_clear(__gen_e_acsl__60);
+ __gmpz_clear(__gen_e_acsl_x_9);
+ __gmpz_clear(__gen_e_acsl_sub_5);
+ __gmpz_clear(__gen_e_acsl_neg_15);
+ __gmpz_clear(__gen_e_acsl_add_7);
+ }
+ }
__retres = 0;
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index 4a5071bb3d8..ff2254d5466 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -113,7 +113,7 @@ int h(int x)
int main(void)
{
- int __gen_e_acsl_at_3;
+ long __gen_e_acsl_at_3;
long __gen_e_acsl_at_2;
int __gen_e_acsl_at;
int __retres;
@@ -125,7 +125,7 @@ int main(void)
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
- __gen_e_acsl_at_3 = x;
+ __gen_e_acsl_at_3 = (long)x;
__gen_e_acsl_at_2 = x + 1L;
__gen_e_acsl_at = x;
/*@ assert x ≡ 0; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index 5cde7c00ea1..a27a3104873 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -233,11 +233,11 @@ void __gen_e_acsl_n(void)
*/
void __gen_e_acsl_m(void)
{
- int __gen_e_acsl_at_4;
+ long __gen_e_acsl_at_4;
int __gen_e_acsl_at_3;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __gen_e_acsl_at_4 = X;
+ __gen_e_acsl_at_4 = (long)X;
{
int __gen_e_acsl_and_2;
if (X == 5) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
@@ -312,7 +312,7 @@ void __gen_e_acsl_k(void)
(char *)"k",(char *)"X == 3 && Y == 2 ==> X == 3",42);
if (X == 3) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0;
if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
- else __gen_e_acsl_implies_3 = X + Y == 5L;
+ else __gen_e_acsl_implies_3 = X + (long)Y == 5L;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
(char *)"k",(char *)"X == 3 && Y == 2 ==> X + Y == 5",43);
k();
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
index 196e1a37605..4b706094131 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
@@ -64,10 +64,10 @@ int __gen_e_acsl_g(int x)
int __gen_e_acsl_f(int x)
{
int __gen_e_acsl_at_2;
- int __gen_e_acsl_at;
+ long __gen_e_acsl_at;
int __retres;
__gen_e_acsl_at_2 = x;
- __gen_e_acsl_at = x;
+ __gen_e_acsl_at = (long)x;
__retres = f(x);
__e_acsl_assert(__retres == (int)(__gen_e_acsl_at - __gen_e_acsl_at_2),
(char *)"Postcondition",(char *)"f",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index 79680b69a4a..820ed8e2571 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
@@ -87,7 +87,7 @@ int main(void)
37);
if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0;
if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1;
- else __gen_e_acsl_implies_3 = x + y == 5L;
+ else __gen_e_acsl_implies_3 = x + (long)y == 5L;
__e_acsl_assert(__gen_e_acsl_implies_3,(char *)"Precondition",
(char *)"main",
(char *)"x == 3 && y == 2 ==> x + y == 5",38);
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index f15a5d1612a..69d75cfcbc5 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -197,14 +197,18 @@ let ty_of_interv ?ctx i =
(* compute a new {!computed_info} by coercing the given type [ty] to the given
context [ctx]. [op] is the type for the operator. *)
-let coerce ~ctx ~op ty =
+let coerce ~arith_operand ~ctx ~op ty =
if compare ty ctx = 1 then begin
(* type larger than the expected context,
so we must introduce an explicit cast *)
{ ty; op; cast = Some ctx }
end else
- (* only add an explicit cast if the context is [Gmp] and [ty] is not *)
- if ctx = Gmp && ty <> Gmp then { ty; op; cast = Some Gmp }
+ (* only add an explicit cast if the context is [Gmp] and [ty] is not;
+ or if the term corresponding to [ty] is an operand of an arithmetic
+ operation which must be explicitely coerced in order to force the
+ operation to be of the expected type. *)
+ if (ctx = Gmp && ty <> Gmp) || arith_operand
+ then { ty; op; cast = Some ctx }
else { ty; op; cast = None }
(******************************************************************************)
@@ -221,7 +225,7 @@ let mk_ctx ~force c =
(* type the term [t] in a context [ctx]. Take --e-acsl-gmp-only into account iff
not [force]. *)
-let rec type_term ~force ?ctx t =
+let rec type_term ~force ?(arith_operand=false) ?ctx t =
let ctx = Extlib.opt_map (mk_ctx ~force) ctx in
let dup ty = ty, ty in
let compute_ctx ?ctx i =
@@ -302,7 +306,7 @@ let rec type_term ~force ?ctx t =
with Interval.Not_an_integer ->
dup Other (* real *)
in
- ignore (type_term ~force:false ~ctx t');
+ ignore (type_term ~force ~arith_operand:true ~ctx t');
(match unop with
| LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
| Neg | BNot -> dup ctx_res)
@@ -317,8 +321,18 @@ let rec type_term ~force ?ctx t =
with Interval.Not_an_integer ->
dup Other (* real *)
in
- ignore (type_term ~force ~ctx t1);
- ignore (type_term ~force ~ctx t2);
+ (* it is enough to explicitely coerce when required one operand to [ctx]
+ (through [arith_operand]) in order to force the type of the operation.
+ Heuristic: coerce the operand which is not a lval in order to lower
+ the number of explicit casts *)
+ let rec cast_first t1 t2 = match t1.term_node with
+ | TLval _ -> false
+ | TLogic_coerce(_, t) -> cast_first t t2
+ | _ -> true
+ in
+ let cast_first = cast_first t1 t2 in
+ ignore (type_term ~force ~arith_operand:cast_first ~ctx t1);
+ ignore (type_term ~force ~arith_operand:(not cast_first) ~ctx t2);
dup ctx_res
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
@@ -390,7 +404,7 @@ let rec type_term ~force ?ctx t =
dup ctx
| Tat (t, _)
- | TLogic_coerce (_, t) -> dup (type_term ~force ?ctx t).ty
+ | TLogic_coerce (_, t) -> dup (type_term ~force ~arith_operand ?ctx t).ty
| TCoerceE (t1, t2) ->
let ctx =
@@ -454,7 +468,7 @@ let rec type_term ~force ?ctx t =
let ty, op = infer t in
match ctx with
| None -> { ty; op; cast = None }
- | Some ctx -> coerce ~ctx ~op ty)
+ | Some ctx -> coerce ~arith_operand ~ctx ~op ty)
t
and type_term_lval (host, offset) =
@@ -574,7 +588,7 @@ let rec type_predicate p =
| Pfresh _ -> Error.not_yet "\\fresh"
| Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
in
- coerce ~ctx:c_int ~op c_int
+ coerce ~arith_operand:false ~ctx:c_int ~op c_int
let type_term ~force ?ctx t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
--
GitLab