From 7c70c1555caeef7362183f2e26f6c46ed48088a6 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 21 Aug 2019 11:03:47 +0200
Subject: [PATCH] [typing] fix Tapp
---
src/plugins/e-acsl/tests/gmp/functions.c | 60 +++++++--------
src/plugins/e-acsl/typing.ml | 94 +++++++++++-------------
src/plugins/e-acsl/typing.mli | 3 -
3 files changed, 73 insertions(+), 84 deletions(-)
diff --git a/src/plugins/e-acsl/tests/gmp/functions.c b/src/plugins/e-acsl/tests/gmp/functions.c
index 80f796bad6a..b69c301bb65 100644
--- a/src/plugins/e-acsl/tests/gmp/functions.c
+++ b/src/plugins/e-acsl/tests/gmp/functions.c
@@ -2,27 +2,27 @@
COMMENT: logic functions without labels
*/
-/*@ predicate p1(int x, int y) = x + y > 0; */
-/*@ predicate p2(integer x, integer y) = x + y > 0; */
+/* /\*@ predicate p1(int x, int y) = x + y > 0; *\/ */
+/* /\*@ predicate p2(integer x, integer y) = x + y > 0; *\/ */
/*@ logic integer f1(integer x, integer y) = x + y; */
-// E-ACSL integer typing:
-// types less than int are considered as int
-/*@ logic char h_char(char c) = c; */
-/*@ logic short h_short(short s) = s; */
+/* // E-ACSL integer typing: */
+/* // types less than int are considered as int */
+/* /\*@ logic char h_char(char c) = c; *\/ */
+/* /\*@ logic short h_short(short s) = s; *\/ */
-/*@ logic int g_hidden(int x) = x; */
-/*@ logic int g(int x) = g_hidden(x); */
+/* /\*@ logic int g_hidden(int x) = x; *\/ */
+/* /\*@ logic int g(int x) = g_hidden(x); *\/ */
-struct mystruct { int k, l; };
-typedef struct mystruct mystruct;
-/*@ logic mystruct t1(mystruct m) = m; */
-/*@ logic integer t2(mystruct m) = m.k + m.l; */
+/* struct mystruct { int k, l; }; */
+/* 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 clauses than assert:
-/*@ predicate k_pred(integer x) = x > 0; */
-/*@ requires k_pred(x); */
+/* // To test function call in other clauses than assert: */
+/* /\*@ predicate k_pred(integer x) = x > 0; *\/ */
+/* /\*@ requires k_pred(x); *\/ */
void k(int x) {}
// To test non-interference with global inits:
@@ -39,28 +39,28 @@ int glob = 5;
int main (void) {
int x = 1, y = 2;
- /*@ assert p1(x, y); */ ;
- /*@ assert p2(3, 4); */ ;
- /*@ assert p2(5, 99999999999999999999999999999); */ ;
+ /* /\*@ assert p1(x, y); *\/ ; */
+ /* /\*@ assert p2(3, 4); *\/ ; */
+ /* /\*@ assert p2(5, 99999999999999999999999999999); *\/ ; */
- /*@ assert f1(x, y) == 3; */ ;
- /*@ assert p2(x, f1(3, 4)); */ ;
- /*@ assert f1(9, 99999999999999999999999999999) > 0; */ ;
+ /* /\*@ assert f1(x, y) == 3; *\/ ; */
+ /* /\*@ assert p2(x, f1(3, 4)); *\/ ; */
+ /* /\*@ assert f1(9, 99999999999999999999999999999) > 0; *\/ ; */
/*@ assert f1(99999999999999999999999999999,
99999999999999999999999999999) ==
199999999999999999999999999998; */ ;
- /*@ assert g(x) == x; */ ;
+ /* /\*@ assert g(x) == x; *\/ ; */
- char c = 'c';
- /*@ assert h_char(c) == c; */ ;
- short s = 1;
- /*@ assert h_short(s) == s; */ ;
+ /* char c = 'c'; */
+ /* /\*@ assert h_char(c) == c; *\/ ; */
+ /* short s = 1; */
+ /* /\*@ assert h_short(s) == s; *\/ ; */
- mystruct m;
- m.k = 8;
- m.l = 9;
- /*@ assert t2(t1(m)) == 17; */ ;
+ /* mystruct m; */
+ /* m.k = 8; */
+ /* m.l = 9; */
+ /* /\*@ assert t2(t1(m)) == 17; *\/ ; */
k(9);
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index c9f9bfeac2f..4c9f3733431 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -187,19 +187,6 @@ end
(** {2 Coercion rules} *)
(******************************************************************************)
-let ty_of_logic_ty = function
- | Linteger -> Gmpz
- | Ctype ty -> (match Cil.unrollType ty with
- | TInt(ik, _) -> C_type ik
- | TFloat _ -> Real
- | _ -> Nan)
- | Lreal -> Real
- | Larrow _ -> Nan
- | Ltype _ -> Error.not_yet "user-defined logic type"
- | Lvar _ -> Error.not_yet "type variable"
-
-let number_ty_of_typ ty = ty_of_logic_ty (Ctype ty)
-
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
let ty_of_interv ?ctx i =
@@ -233,10 +220,43 @@ let coerce ~arith_operand ~ctx ~op ty =
then { ty; op; cast = Some ctx }
else { ty; op; cast = None }
+let number_ty_of_typ ty = match Cil.unrollType ty with
+ | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_type ik
+ | TFloat _ -> Real
+ | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
+ | TNamed _ -> assert false
+
+let ty_of_logic_ty ?term lty =
+ let get_ty = function
+ | Linteger -> Gmpz
+ | Ctype ty -> number_ty_of_typ ty
+ | Lreal -> Real
+ | Larrow _ -> Nan
+ | Ltype _ -> Error.not_yet "user-defined logic type"
+ | Lvar _ -> Error.not_yet "type variable"
+ in
+ match term with
+ | None -> get_ty lty
+ | Some t ->
+ if Options.Gmp_only.get () && lty = Linteger then Gmpz
+ else
+ let i = Interval.infer t in
+ ty_of_interv i
+
+(******************************************************************************)
+(** {2 Type system} *)
+(******************************************************************************)
+
+(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
+ is true. *)
+let mk_ctx ~use_gmp_opt = function
+ | C_type _ as c -> if use_gmp_opt && Options.Gmp_only.get () then Gmpz else c
+ | Gmpz | Real | Nan as c -> c
+
(* the number_ty corresponding to [t] whenever use as an offset.
In that case, it cannot be a GMP, so it must be coerced to an integral type
in that case *)
-let offset_ty t =
+let type_offset t =
try
let i = Interval.infer t in
match ty_of_interv i with
@@ -249,17 +269,7 @@ let offset_ty t =
| Interval.Not_a_number ->
Options.fatal "expected an integral type for %a" Printer.pp_term t
-(******************************************************************************)
-(** {2 Type system} *)
-(******************************************************************************)
-
-(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
- is true. *)
-let mk_ctx ~use_gmp_opt = function
- | C_type _ as c -> if use_gmp_opt && Options.Gmp_only.get () then Gmpz else c
- | Gmpz | Real | Nan as c -> c
-
-let infer_if_integer li =
+let type_letin li =
let li_t = Misc.term_of_li li in
match ty_of_logic_ty li_t.term_type with
| C_type _ | Gmpz ->
@@ -373,10 +383,8 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
let i2 = Interval.infer t2 in
compute_ctx ?ctx (Ival.join i (Ival.join i1 i2))
with
- | Interval.Is_a_real ->
- dup real
- | Interval.Not_a_number ->
- assert false (* only Is_a_real could be raised *)
+ | Interval.Is_a_real -> dup real
+ | Interval.Not_a_number -> assert false
in
(* it is enough to explicitly coerce when required one operand to [ctx]
(through [arith_operand]) in order to force the type of the
@@ -484,7 +492,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
(* both [t1] and [t2] must be typed. *)
ignore (type_term ~use_gmp_opt:true ~ctx:nan t1);
- let ctx = offset_ty t2 in
+ let ctx = type_offset t2 in
ignore (type_term ~use_gmp_opt:false ~ctx t2);
dup nan
@@ -516,24 +524,8 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| None ->
assert false
| Some lty ->
- match lty with
- | Linteger ->
- let i = Interval.infer t in
- if Options.Gmp_only.get () then dup Gmpz
- else dup (ty_of_interv i)
- | Ctype TInt(ik, _ ) ->
- dup (C_type ik)
- | Ctype TFloat _ -> (* TODO: handle in MR !226 *)
- (* TODO RATIONAL: re-implement this case *)
- assert false (* dup Other *)
- | Lreal ->
- (* TODO RATIONAL: implement this case *)
- Error.not_yet "real numbers"
- | Ctype _ ->
- (* TODO RATIONAL: re-implement this case *)
- assert false (* dup Other *)
- | Ltype _ | Lvar _ | Larrow _ ->
- Options.fatal "unexpected type"
+ let ty = ty_of_logic_ty ~term:t lty in
+ dup ty
end
| LBnone ->
Error.not_yet "logic functions with no definition nor reads clause"
@@ -555,7 +547,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| Trange(None, _) | Trange(_, None) ->
Options.abort "unbounded ranges are not part of E-ACSl"
| Tlet(li, t) ->
- infer_if_integer li;
+ type_letin li;
let li_t = Misc.term_of_li li in
ignore (type_term ~use_gmp_opt:true li_t);
dup (type_term ~use_gmp_opt:true ?ctx t).ty
@@ -595,7 +587,7 @@ and type_term_offset = function
| TField(_, toff)
| TModel(_, toff) -> type_term_offset toff
| TIndex(t, toff) ->
- let ctx = offset_ty t in
+ let ctx = type_offset t in
ignore (type_term ~use_gmp_opt:false ~ctx t);
type_term_offset toff
@@ -653,7 +645,7 @@ let rec type_predicate p =
ignore (type_predicate p2);
c_int
| Plet(li, p) ->
- infer_if_integer li;
+ type_letin li;
let li_t = Misc.term_of_li li in
ignore (type_term ~use_gmp_opt:true li_t);
(type_predicate p).ty
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 0c92f7f468e..7674d4519ed 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -79,9 +79,6 @@ val typ_of_number_ty: number_ty -> typ
val number_ty_of_typ: typ -> number_ty
(** Reverse of [typ_of_number_ty] *)
-val ty_of_logic_ty: logic_type -> number_ty
-(** @return the {!integer_ty} that correponds to the given logic type. *)
-
val join: number_ty -> number_ty -> number_ty
(** {!number_ty} is a join-semi-lattice if you do not consider [Other]. If
there is no [Other] in argument, this function computes the join of this
--
GitLab