From a00defc9a5a7215897261f608a05df57f5fb0ae0 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 15 Jun 2020 17:36:45 +0200
Subject: [PATCH] [eacsl:typing] Update `Typing.number_ty_of_typ` to support
GMP types
---
src/plugins/e-acsl/src/analyses/typing.ml | 17 +++++++++++------
src/plugins/e-acsl/src/analyses/typing.mli | 8 ++++++--
.../src/code_generator/logic_functions.ml | 5 ++++-
src/plugins/e-acsl/src/code_generator/loops.ml | 2 +-
4 files changed, 22 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index fa5d75b572d..9d2590f9bb4 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -262,16 +262,21 @@ 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_integer ik
- | TFloat(fk, _) -> C_float fk
- | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
- | TNamed _ -> assert false
+let number_ty_of_typ ~post ty =
+ (* Consider GMP types only in a post typing phase *)
+ if post && Gmp_types.Z.is_t ty then Gmpz
+ else if post && Gmp_types.Q.is_t ty then Rational
+ else
+ match Cil.unrollType ty with
+ | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_integer ik
+ | TFloat(fk, _) -> C_float fk
+ | 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
+ | Ctype ty -> number_ty_of_typ ~post:false ty
| Lreal -> Real
| Larrow _ -> Nan
| Ltype _ -> Error.not_yet "user-defined logic type"
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 8002d23e4a2..7a7fd0f80d5 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -79,8 +79,12 @@ val typ_of_number_ty: number_ty -> typ
for [Gmpz], [Real.t ()] for [Real] and [TInt(ik, [[]])] for [Ctype ik].
@raise Not_a_number in case of [Nan]. *)
-val number_ty_of_typ: typ -> number_ty
-(** Reverse of [typ_of_number_ty] *)
+val number_ty_of_typ: post:bool -> typ -> number_ty
+(** Reverse of [typ_of_number_ty]
+ [number_ty_of_typ ~post ty] return the {!number_ty} corresponding to a
+ C type. [post] indicates if the type is before or after the typing phase.
+ The GMP types will be recognized only in a post-typing phase.
+*)
val join: number_ty -> number_ty -> number_ty
(** {!number_ty} is a join-semi-lattice if you do not consider [Other]. If
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 1d552fd9949..3b346a01aff 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -88,7 +88,10 @@ let pred_to_block ~loc kf env ret_vi p =
(* Generate the function's body for terms. *)
let term_to_block ~loc kf env ret_ty ret_vi t =
- Typing.type_term ~use_gmp_opt:false ~ctx:(Typing.number_ty_of_typ ret_ty) t;
+ Typing.type_term
+ ~use_gmp_opt:false
+ ~ctx:(Typing.number_ty_of_typ ~post:false ret_ty)
+ t;
let e, env = !term_to_exp_ref kf env t in
if Cil.isVoidType ret_ty then
(* if the function's result is a GMP, it is the first parameter of the
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 4e605aad9d0..fe84f48fc29 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -117,7 +117,7 @@ let bounds_for_small_type ~loc (t1, lv, t2) =
let min, max = Misc.finite_min_and_max i in
let t1 = Logic_const.tint ~loc min in
let t2 = Logic_const.tint ~loc max in
- let ctx = Typing.number_ty_of_typ ty in
+ let ctx = Typing.number_ty_of_typ ~post:false ty in
(* we are assured that we will not have a GMP,
once again because we intersected with [ity] *)
Typing.type_term ~use_gmp_opt:false ~ctx t1;
--
GitLab