From ddd9af48f6348902b4e8ae5cf4603ee72936d044 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 2 Apr 2020 11:47:26 +0200
Subject: [PATCH] [kernel] recursively coerce t-sets
Visible impact on Genassigns plug-in
---
.../ast_queries/logic_utils.ml | 65 ++++++++++++-------
.../ast_queries/logic_utils.mli | 13 ++--
2 files changed, 51 insertions(+), 27 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index d1bcc167969..242feb6c6a0 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -305,30 +305,49 @@ let parse_float ?loc literal =
let mk_coerce ltyp t =
Logic_const.term ~loc:t.term_loc (TLogic_coerce(ltyp, t)) ltyp
-let numeric_coerce ltyp t =
+let rec numeric_coerce ltyp t =
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(lt,e) when Cil.no_op_coerce lt e ->
- (* coercion hidden by the printer, but still present *)
- mk_coerce ltyp e
- | TConst(LEnum _) | 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.isExactFloat fk r -> { e with term_type = Lreal }
- | Linteger, TInt(ik,_), TConst(LEnum { eival }) ->
- ( match Cil.constFoldToInt eival with
- | Some i when Cil.fitsInInt ik i -> { e with term_type = Linteger }
- | _ -> mk_coerce ltyp t )
- | _ -> mk_coerce ltyp t
- end
- | _ -> mk_coerce ltyp t
+ match t.term_node with
+ | TLogic_coerce(lt,e) when Cil.no_op_coerce lt e ->
+ (* coercion hidden by the printer, but still present *)
+ numeric_coerce ltyp e
+ | TConst(LEnum _) | 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.isExactFloat fk r -> { e with term_type = Lreal }
+ | Linteger, TInt(ik,_), TConst(LEnum { eival }) ->
+ ( match Cil.constFoldToInt eival with
+ | Some i when Cil.fitsInInt ik i -> { e with term_type = Linteger }
+ | _ -> mk_coerce ltyp t )
+ | _ -> mk_coerce ltyp t
+ end
+ | Trange(a,b) ->
+ let ra = numeric_bound ltyp a in
+ let rb = numeric_bound ltyp b in
+ { t with term_node = Trange(ra,rb) ;
+ term_type = Logic_const.make_set_type ltyp }
+ | Tunion ts ->
+ { t with term_node = Tunion (List.map (numeric_coerce ltyp) ts) ;
+ term_type = Logic_const.make_set_type ltyp }
+ | Tinter ts ->
+ { t with term_node = Tinter (List.map (numeric_coerce ltyp) ts) ;
+ term_type = Logic_const.make_set_type ltyp }
+ | Tcomprehension(t,qs,cond) ->
+ { t with term_node = Tcomprehension (numeric_coerce ltyp t,qs,cond) ;
+ term_type = Logic_const.make_set_type ltyp }
+ | _ ->
+ if Cil_datatype.Logic_type.equal oldt ltyp then t
+ else mk_coerce ltyp t
+
+and numeric_bound ltyp = function
+ | None -> None
+ | Some a -> Some (numeric_coerce ltyp a)
(* Don't forget to keep is_zero_comparable
and scalar_term_to_predicate in sync. *)
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 81a7c454d54..6817dfd9371 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -85,7 +85,9 @@ val logicCType : logic_type -> typ
(** transforms an array into pointer. *)
val array_to_ptr : logic_type -> logic_type
-(** C type to logic type, with implicit conversion for arithmetic types. *)
+(** C type to logic type, with implicit conversion for arithmetic types.
+ @since Frama-C+dev
+*)
val coerce_type : typ -> logic_type
(** {2 Predicates} *)
@@ -122,9 +124,7 @@ val mk_logic_pointer_or_StartOf : term -> term
be inserted. Otherwise (which is the default), [mk_cast typ t] will return
[t] if it is already of type [typ]
- @modify Aluminium-20160501 added [force] optional argument
-
-*)
+ @modify Aluminium-20160501 added [force] optional argument *)
val mk_cast: ?loc:location -> ?force:bool -> typ -> term -> term
@@ -141,7 +141,12 @@ val remove_logic_coerce: term -> term
in [t]. In particular, [numeric_coerce (int)cst Linteger], where [cst]
fits in int will be directly [cst], without any coercion.
+ Also coerce recursively the sub-terms of t-set expressions
+ (range, union, inter and comprehension) and lift the associated
+ set type.
+
@since Magnesium-20151001
+ @modify Frama-C+dev
*)
val numeric_coerce: logic_type -> term -> term
--
GitLab