From 84c7824afcadfc7aef5246e141d5ef98d2e8d822 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 23 Mar 2016 08:59:23 +0100
Subject: [PATCH] [typing] fix bug with floats/reals; more generally force
typing of every non-integer term
---
.../tests/bts/oracle/bts1307.res.oracle | 3 +-
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 6 +-
.../e-acsl-runtime/oracle/valid.res.oracle | 4 +-
src/plugins/e-acsl/typing.ml | 159 +++++++++---------
src/plugins/e-acsl/typing.mli | 2 +-
5 files changed, 92 insertions(+), 82 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index 7785f52bb95..1b9b45f9fc2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -6,4 +6,5 @@ tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] user error: type long double not implemented. Using double instead
-FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status invalid.
+tests/bts/bts1307.i:23:[value] warning: function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
+tests/bts/bts1307.i:23:[value] warning: function __gen_e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index d15f8673865..121b10cc72f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -254,9 +254,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
sizeof(float));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
- __e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + (long double)(
- (long double)5 - ((long double)(
- 5 / 80) * *__gen_e_acsl_at_3) * 0.4),
+ __e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + ((long double)5 -
+ ((long double)(
+ 5 / 80) * *__gen_e_acsl_at_3) * 0.4),
(char *)"Postcondition",(char *)"foo",
(char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in)+(5-((5/80)**\\old(Mwmax))*0.4)",
11);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 58ac8f9ec26..e1eb42c942a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -5,13 +5,15 @@ tests/e-acsl-runtime/valid.c:14:[e-acsl] warning: E-ACSL construct `complete beh
Ignoring annotation.
tests/e-acsl-runtime/valid.c:14:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 85e3cb650dc..341dc9f7aa9 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -192,11 +192,11 @@ let rec type_term env ~ctx t =
let ty =
try
let i = Interval.infer env t in
- type_term_lval env tlv;
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
Other
in
+ type_term_lval env tlv;
dup ty
| Toffset(_, t')
@@ -210,7 +210,7 @@ let rec type_term env ~ctx t =
ignore (type_term env ~ctx:Other t');
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
- Other
+ assert false
in
dup ty
@@ -223,50 +223,51 @@ let rec type_term env ~ctx t =
ignore (type_term env ~ctx:Other t2);
ty_of_interv ~ctx i
with Interval.Not_an_integer ->
- Other
+ assert false
in
dup ty
| TUnOp (unop, t') ->
- let ty =
- let i = Interval.infer env t in
- let i' = Interval.infer env t' in
- let ctx = mk_ctx (ty_of_interv ~ctx (Interval.join i i')) in
- ignore (type_term env ~ctx t');
- ctx
+ let ctx =
+ try
+ let i = Interval.infer env t in
+ let i' = Interval.infer env t' in
+ mk_ctx (ty_of_interv ~ctx (Interval.join i i'))
+ with Interval.Not_an_integer ->
+ Other (* real *)
in
+ ignore (type_term env ~ctx t');
(match unop with
- | LNot -> c_int, ty (* converted into [t == 0] in casse of GMP *)
- | Neg | BNot -> dup ty)
+ | LNot -> c_int, ctx (* converted into [t == 0] in casse of GMP *)
+ | Neg | BNot -> dup ctx)
| TBinOp((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2) ->
- let ty =
- let i = Interval.infer env t in
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
- let ctx =
+ let ctx =
+ try
+ let i = Interval.infer env t in
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)))
- in
- ignore (type_term env ~ctx t1);
- ignore (type_term env ~ctx t2);
- ctx
+ with Interval.Not_an_integer ->
+ Other (* real *)
in
- dup ty
+ ignore (type_term env ~ctx t1);
+ ignore (type_term env ~ctx t2);
+ dup ctx
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
assert (compare ctx c_int >= 0);
- let ty =
- let ctx =
- try
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
- mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
- with Interval.Not_an_integer ->
- Other
- in
- ignore (type_term env ~ctx t1);
- ignore (type_term env ~ctx t2);
- match ctx with
+ let ctx =
+ try
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
+ mk_ctx (ty_of_interv ~ctx (Interval.join i1 i2))
+ with Interval.Not_an_integer ->
+ Other
+ in
+ ignore (type_term env ~ctx t1);
+ ignore (type_term env ~ctx t2);
+ let ty = match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx
in
@@ -274,14 +275,16 @@ let rec type_term env ~ctx t =
| TBinOp ((LAnd | LOr), t1, t2) ->
let ty =
- assert (compare ctx c_int >= 1);
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
- (* both operands fit in an int. *)
- ignore (type_term env ~ctx:c_int t1);
- ignore (type_term env ~ctx:c_int t2);
- ty_of_interv ~ctx (Interval.join i1 i2)
+ try
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
+ ty_of_interv ~ctx (Interval.join i1 i2)
+ with Interval.Not_an_integer ->
+ Other
in
+ (* both operands fit in an int. *)
+ ignore (type_term env ~ctx:c_int t1);
+ ignore (type_term env ~ctx:c_int t2);
dup ty
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
@@ -290,55 +293,51 @@ let rec type_term env ~ctx t =
| TCastE(_, t')
| TCoerce(t', _) ->
- let ty =
- (* in any case, must type the subterms *)
+ let ctx =
try
let i = Interval.infer env t' in
- (* nothing to do more: [i] is already more precise than what we could
- infer from the arguments of the cast. Also, do not type the
+ (* nothing to do more: [i] is already more precise than what we
+ could infer from the arguments of the cast. Also, do not type the
internal term: possibly it is not even an integer *)
- let ty = ty_of_interv ~ctx i in
- ignore (type_term env ~ctx:ty t');
- ty
+ ty_of_interv ~ctx i
with Interval.Not_an_integer ->
- ignore (type_term env ~ctx:Other t');
Other
in
- dup ty
+ ignore (type_term env ~ctx t');
+ dup ctx
| Tif (t1, t2, t3) ->
- let ty =
- let ctx = mk_ctx c_int in
- ignore (type_term env ~ctx t1);
- let i = Interval.infer env t in
- let ctx =
- try
- let i2 = Interval.infer env t2 in
- let i3 = Interval.infer env t3 in
- mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)))
- with Interval.Not_an_integer ->
- Other
- in
- ignore (type_term env ~ctx t2);
- ignore (type_term env ~ctx t3);
- ctx
+ let ctx = mk_ctx c_int in
+ ignore (type_term env ~ctx t1);
+ let i = Interval.infer env t in
+ let ctx =
+ try
+ let i2 = Interval.infer env t2 in
+ let i3 = Interval.infer env t3 in
+ mk_ctx (ty_of_interv ~ctx (Interval.join i (Interval.join i2 i3)))
+ with Interval.Not_an_integer ->
+ Other
in
- dup ty
+ ignore (type_term env ~ctx t2);
+ ignore (type_term env ~ctx t3);
+ dup ctx
| Tat (t, _)
| TLogic_coerce (_, t) -> dup (type_term env ~ctx t).ty
| TCoerceE (t1, t2) ->
- let ty =
- let i = Interval.infer env t in
- let i1 = Interval.infer env t1 in
- let i2 = Interval.infer env t2 in
- let ty = ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2)) in
- ignore (type_term env ~ctx:ty t1);
- ignore (type_term env ~ctx:ty t2);
- ty
+ let ctx =
+ try
+ let i = Interval.infer env t in
+ let i1 = Interval.infer env t1 in
+ let i2 = Interval.infer env t2 in
+ ty_of_interv ~ctx (Interval.join i (Interval.join i1 i2))
+ with Interval.Not_an_integer ->
+ Other
in
- dup ty
+ ignore (type_term env ~ctx t1);
+ ignore (type_term env ~ctx t2);
+ dup ctx
| TAddrOf tlv
| TStartOf tlv ->
@@ -516,13 +515,21 @@ let get_integer_op t = (Memo.get t).op
let get_integer_op_of_predicate p =
(type_predicate_named Interval.Env.empty (* the env is useless *) p).op
+let extract_typ t ty =
+ try typ_of_integer_ty ty
+ with Not_an_integer ->
+ let ty = t.term_type in
+ if Cil.isLogicRealType ty then TFloat(FLongDouble, [])
+ else if Cil.isLogicFloatType ty then Logic_utils.logicCType ty
+ else assert false
+
let get_typ t =
let info = Memo.get t in
- try typ_of_integer_ty info.ty with Not_an_integer -> assert false
+ extract_typ t info.ty
let get_op t =
let info = Memo.get t in
- try typ_of_integer_ty info.op with Not_an_integer -> assert false
+ extract_typ t info.op
let get_cast t =
Cil.CurrentLoc.set t.term_loc;
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index a65d34c137f..93b80b960c4 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -58,7 +58,7 @@ val get_integer_op: term -> integer_ty
val get_integer_op_of_predicate: predicate named -> integer_ty
val get_typ: term -> typ
-(** Get the type of the given term which must be an integer.
+(** Get the type of the given term.
{!type_named_predicate} must already have been called on the englobing
predicate. *)
--
GitLab