Commit 6ff65da4 authored by Julien Signoles's avatar Julien Signoles
Browse files

[typing] improve typing of operators by preventing propagation of the context...

[typing] improve typing of operators by preventing propagation of the context to the operands. This way, it prevents to introduce useless type coercions. Indeed, the typing context is only useful to limit the number of generated casts when typing the _result_ of the operation.
parent b94b8e2d
......@@ -18,13 +18,13 @@ int main(void)
__e_acsl_assert(0 != ~ 0,(char *)"Assertion",(char *)"main",
(char *)"0 != ~0",12);
/*@ assert x+1 ≡ -2; */
__e_acsl_assert(x + 1L == -2L,(char *)"Assertion",(char *)"main",
__e_acsl_assert(x + 1L == -2,(char *)"Assertion",(char *)"main",
(char *)"x+1 == -2",14);
/*@ assert x-1 ≡ -4; */
__e_acsl_assert(x - 1L == -4L,(char *)"Assertion",(char *)"main",
__e_acsl_assert(x - 1L == -4,(char *)"Assertion",(char *)"main",
(char *)"x-1 == -4",15);
/*@ assert x*3 ≡ -9; */
__e_acsl_assert(x * 3L == -9L,(char *)"Assertion",(char *)"main",
__e_acsl_assert(x * 3L == -9,(char *)"Assertion",(char *)"main",
(char *)"x*3 == -9",16);
/*@ assert x/3 ≡ -1; */
__e_acsl_assert(x / 3 == -1,(char *)"Assertion",(char *)"main",
......@@ -66,7 +66,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) == -10L,
__e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - y) == -10,
(char *)"Assertion",(char *)"main",
(char *)"((x*2+(3+y))-4)+(x-y) == -10",23);
/*@ assert (0≡1) ≡ !(0≡0); */
......
......@@ -160,7 +160,7 @@ int __gen_e_acsl_search(int elt)
(char *)"index_bound: __gen_e_acsl_i < 10",7);
__e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
(char *)"index_bound: 0 <= __gen_e_acsl_i",7);
if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1L]) ;
if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1]) ;
else {
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop3;
......
......@@ -199,7 +199,7 @@ int main(void)
{
int __gen_e_acsl_offset_21;
__gen_e_acsl_offset_21 = __e_acsl_offset((void *)q);
__e_acsl_assert(__gen_e_acsl_offset_21 == 8 * 3UL,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_offset_21 == 8 * 3,(char *)"Assertion",
(char *)"main",(char *)"\\offset(q) == sizeof(long)*3",
53);
}
......@@ -209,7 +209,7 @@ int main(void)
{
int __gen_e_acsl_offset_22;
__gen_e_acsl_offset_22 = __e_acsl_offset((void *)q);
__e_acsl_assert(__gen_e_acsl_offset_22 == 8 * 7UL,(char *)"Assertion",
__e_acsl_assert(__gen_e_acsl_offset_22 == 8 * 7,(char *)"Assertion",
(char *)"main",(char *)"\\offset(q) == sizeof(long)*7",
55);
}
......
......@@ -43,12 +43,7 @@ int main(void)
__e_acsl_assert(t[2L] == 4,(char *)"Assertion",(char *)"main",
(char *)"t[2] == 4",13);
/*@ assert t[(2*sizeof(int))/sizeof((int)0x0)] ≡ 4; */
__e_acsl_assert((long)((long)(2 * 4) / 4) < 3,(char *)"RTE",(char *)"main",
(char *)"index_bound: (long)((long)(2*4)/4) < 3",14);
__e_acsl_assert(0 <= (long)((long)(2 * 4) / 4),(char *)"RTE",
(char *)"main",
(char *)"index_bound: 0 <= (long)((long)(2*4)/4)",14);
__e_acsl_assert(t[(2L * 4) / 4] == 4,(char *)"Assertion",(char *)"main",
__e_acsl_assert(t[(2 * 4) / 4] == 4,(char *)"Assertion",(char *)"main",
(char *)"t[(2*sizeof(int))/sizeof((int)0x0)] == 4",14);
{
int i;
......
......@@ -224,12 +224,24 @@ let mk_ctx ~force c =
let rec type_term ~force ?ctx t =
let ctx = Extlib.opt_map (mk_ctx ~force) ctx in
let dup ty = ty, ty in
let compute_ctx ?ctx i =
(* in order to get a minimal amount of generated casts for operators, the
result is typed in the given context [ctx], but not the operands.
This function returns a tuple (ctx_of_result, ctx_of_operands) *)
match ctx with
| None ->
(* no context: factorize *)
dup (mk_ctx ~force:false (ty_of_interv i))
| Some ctx ->
mk_ctx ~force:false (ty_of_interv ~ctx i),
mk_ctx ~force:false (ty_of_interv i)
in
let infer t =
Cil.CurrentLoc.set t.term_loc;
(* this pattern matching implements the formal rules of the JFLA's paper
(and of course also covers the missing cases). Also enforce the invariant
that every subterm is typed, even if it is not an integer. *)
match t.term_node with
match t.term_node with
| TConst (Integer _ | LChr _ | LEnum _)
| TSizeOf _
| TSizeOfStr _
......@@ -282,33 +294,32 @@ let rec type_term ~force ?ctx t =
dup ty
| TUnOp (unop, t') ->
let ctx =
let ctx_res, ctx =
try
let i = Interval.infer t in
let i' = Interval.infer t' in
mk_ctx ~force:false (ty_of_interv ?ctx (Ival.join i i'))
compute_ctx ?ctx (Ival.join i i')
with Interval.Not_an_integer ->
Other (* real *)
dup Other (* real *)
in
ignore (type_term ~force:false ~ctx t');
(match unop with
| LNot -> c_int, ctx (* converted into [t == 0] in case of GMP *)
| Neg | BNot -> dup ctx)
| LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
| Neg | BNot -> dup ctx_res)
| TBinOp((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2) ->
let ctx =
let ctx_res, ctx =
try
let i = Interval.infer t in
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
let ctx = ty_of_interv ?ctx (Ival.join i (Ival.join i1 i2)) in
mk_ctx ~force:false ctx
compute_ctx ?ctx (Ival.join i (Ival.join i1 i2))
with Interval.Not_an_integer ->
Other (* real *)
dup Other (* real *)
in
ignore (type_term ~force ~ctx t1);
ignore (type_term ~force ~ctx t2);
dup ctx
dup ctx_res
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
assert (match ctx with None -> true | Some c -> compare c c_int >= 0);
......
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