Commit 03cd4cee authored by Julien Signoles's avatar Julien Signoles Committed by Kostyantyn Vorobyov
Browse files

fix bug with typing of unary and binary operators (fix git issue #37)

parent 176c8663
......@@ -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
#########################
......
......@@ -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",
......
......@@ -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;
}
......@@ -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;
}
......
......@@ -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;
}
......
......@@ -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; */
......
......@@ -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();
......
......@@ -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",
......
......@@ -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);
......
......@@ -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'."
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment