From 6a2cbd4b639cd20cdead0669b9f3c8ef7d753b0e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 31 Mar 2020 09:50:03 +0200
Subject: [PATCH] [kernel] cast & coerce simpifications
---
src/kernel_services/ast_queries/cil.ml | 9 ++++-
src/kernel_services/ast_queries/cil.mli | 3 ++
.../ast_queries/logic_utils.ml | 34 ++++++++-----------
3 files changed, 26 insertions(+), 20 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d9330b5ab30..a3de91f6122 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3063,6 +3063,13 @@ let intKindForValue i (unsigned: bool) =
else if fitsInInt ILongLong i then ILongLong
else raise Not_representable
+(* True is an double constant is finite for a kind *)
+let isFiniteFloat fk v =
+ Floating_point.isfinite @@
+ match fk with
+ | FFloat -> Floating_point.round_to_single_precision_float v
+ | _ -> v
+
(* Construct an integer constant with possible truncation if the kind is not
specified *)
let kinteger64 ~loc ?repr ?kind i =
@@ -3631,7 +3638,7 @@ let typeOf_array_elem t =
let no_op_coerce typ t =
match typ with
- | Lreal -> true
+ | Lreal -> isLogicRealOrFloatType t.term_type
| Linteger -> isLogicIntegralType t.term_type
| Ltype _ when Logic_const.is_boolean_type typ ->
isLogicPureBooleanType t.term_type
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index c372bb6514c..9e47d0eedd8 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2136,6 +2136,9 @@ val max_unsigned_number: int -> Integer.t
(** True if the integer fits within the kind's range *)
val fitsInInt: ikind -> Integer.t -> bool
+(** True if the float is finite for the kind's range *)
+val isFiniteFloat: fkind -> float -> bool
+
exception Not_representable
(** raised by {!intKindForValue}. *)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 8a43475ab1c..c79a9d15400 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -307,29 +307,25 @@ let string_to_float_lconstant string =
LReal { r_nearest = f.f_nearest; r_upper = f.f_upper; r_lower = f.f_lower;
r_literal = string }
+let mk_coerce ltyp t =
+ Logic_const.term ~loc:t.term_loc (TLogic_coerce(ltyp, t)) ltyp
+
let numeric_coerce ltyp t =
- let coerce t =
- Logic_const.term ~loc:t.term_loc (TLogic_coerce(ltyp, t)) ltyp
- in
let oldt = unroll_type t.term_type in
if Cil_datatype.Logic_type.equal oldt ltyp then t
else match t.term_node with
- | TLogic_coerce(t,e) when Cil.no_op_coerce t e -> coerce e
- | TConst(Integer(i,_)) ->
- (match oldt, ltyp with
- | Ctype (TInt(ikind,_)), Linteger when Cil.fitsInInt ikind i ->
- { t with term_type = Linteger }
- | _ -> coerce t)
- | TCastE(typ, ({ term_node = TConst(Integer(i,_))} as t')) ->
- (match unrollType typ with
- | TInt (ikind,_) when Cil.fitsInInt ikind i ->
- (match unroll_type t'.term_type with
- | Linteger -> t'
- | Ctype (TInt (ikind,_)) when Cil.fitsInInt ikind i ->
- { t' with term_type = Linteger }
- | _ -> coerce t')
- | _ -> coerce t)
- | _ -> coerce t
+ | TLogic_coerce(lt,e) when Cil.no_op_coerce lt e -> mk_coerce ltyp e
+ | TConst(Integer _) when ltyp = Linteger -> { t with term_type = Linteger }
+ | TConst(LReal _ ) when ltyp = Lreal -> { t with term_type = Lreal }
+ | TCastE(ty,e) ->
+ begin match ltyp, Cil.unrollType ty, e.term_node with
+ | Linteger, TInt(ik,_), TConst(Integer(v,_))
+ when Cil.fitsInInt ik v -> { e with term_type = Linteger }
+ | Lreal, TFloat(fk,_), TConst(LReal r)
+ when Cil.isFiniteFloat fk r.r_nearest -> { e with term_type = Lreal }
+ | _ -> mk_coerce ltyp t
+ end
+ | _ -> mk_coerce ltyp t
(* Don't forget to keep is_zero_comparable
and scalar_term_to_predicate in sync. *)
--
GitLab