From 4d552b291d8cf2e80f6cf07070f66763690f5a1c Mon Sep 17 00:00:00 2001
From: Nicolas Bellec <nicolas.bellec@cea.fr>
Date: Wed, 24 Jan 2024 16:49:00 +0100
Subject: [PATCH] Merged TCastE and TLogic_coerce with a boolean
---
src/kernel_internals/typing/asm_contracts.ml | 2 +-
src/kernel_services/ast_data/alarms.ml | 2 +-
src/kernel_services/ast_data/cil_types.ml | 14 ++--
.../ast_printing/cil_printer.ml | 14 ++--
.../ast_printing/cil_types_debug.ml | 4 +-
src/kernel_services/ast_queries/ast_diff.ml | 10 +--
src/kernel_services/ast_queries/ast_info.ml | 2 +-
src/kernel_services/ast_queries/cil.ml | 22 ++---
.../ast_queries/cil_datatype.ml | 27 +++----
.../ast_queries/logic_const.ml | 4 +-
src/kernel_services/ast_queries/logic_to_c.ml | 21 +++--
.../ast_queries/logic_typing.ml | 51 ++++++------
.../ast_queries/logic_utils.ml | 67 ++++++++-------
src/plugins/aorai/aorai_utils.ml | 20 ++---
.../e-acsl/src/analyses/bound_variables.ml | 4 +-
src/plugins/e-acsl/src/analyses/interval.ml | 5 +-
src/plugins/e-acsl/src/analyses/labels.ml | 4 +-
.../e-acsl/src/analyses/memory_tracking.ml | 7 +-
src/plugins/e-acsl/src/analyses/typing.ml | 21 ++---
.../src/code_generator/translate_terms.ml | 8 +-
src/plugins/eva/legacy/eval_terms.ml | 81 ++++++++++---------
src/plugins/wp/LogicSemantics.ml | 6 +-
src/plugins/wp/MemoryContext.ml | 4 +-
src/plugins/wp/RefUsage.ml | 5 +-
src/plugins/wp/RegionAccess.ml | 6 +-
src/plugins/wp/wpPropId.ml | 2 +-
tests/libc/check_const.ml | 2 +-
27 files changed, 206 insertions(+), 209 deletions(-)
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 836d52abf98..5a117f92751 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -82,7 +82,7 @@ let access_ptr_elts ~loc tlv =
let base, basetype =
if Logic_utils.isLogicVoidPointerType basetype then begin
let typ = Ctype Cil.charPtrType in
- Logic_const.term ~loc (TCastE(Cil.charPtrType,base)) typ, typ
+ Logic_const.term ~loc (TCast(false, Ctype Cil.charPtrType,base)) typ, typ
end else base, basetype
in
let offset = Logic_const.term ~loc (TBinOp (PlusPI, base, range)) basetype in
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 16ab1a0a5cb..1fbd95cf544 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -519,7 +519,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
| _ -> Cil.voidPtrType
in
let zero = Cil.lzero () in
- Logic_const.term (TCastE (typ, zero)) (Ctype typ)
+ Logic_const.term (TCast (false, Ctype typ, zero)) (Ctype typ)
end
| Some e -> Logic_utils.expr_to_term e
in
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 55ea8321125..9fb991e9ecc 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1362,7 +1362,13 @@ and term_node =
| TAlignOfE of term (** alignment of the type of an expression. *)
| TUnOp of unop * term (** unary operator. *)
| TBinOp of binop * term * term (** binary operators. *)
- | TCastE of typ * term (** cast to a C type. *)
+ | TCast of bool * logic_type * term
+ (** cast to a C type (if bool is false)
+ or an implicit conversion from C type to a logic type (if bool is true).
+ In the second case:
+ The logic type must not be a Ctype.
+ In particular, used to denote lifting to Linteger and Lreal.
+ *)
| TAddrOf of term_lval (** address of a term. *)
| TStartOf of term_lval (** beginning of an array. *)
@@ -1380,11 +1386,7 @@ and term_node =
| Toffset of logic_label * term (** offset from the base address of a pointer. *)
| Tblock_length of logic_label * term (** length of the block pointed to by the term. *)
| Tnull (** the null pointer. *)
- | TLogic_coerce of logic_type * term
- (** implicit conversion from a C type to a logic type.
- The logic type must not be a Ctype. In particular, used to denote
- lifting to Linteger and Lreal.
- *)
+
| TUpdate of term * term_offset * term
(** functional update of a field. *)
| Ttypeof of term (** type tag for a term. *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index b8d83736750..a9d7c981037 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -360,7 +360,7 @@ module Precedence = struct
| Tapp({ l_var_info },[],[_;_])
when l_var_info.lv_name = "\\repeat" -> bitwiseLevel
(* Unary *)
- | TCastE(_,_)
+ | TCast(false,_,_)
| TAddrOf(_)
| TStartOf(_)
| TUnOp((Neg|BNot|LNot),_) -> unaryLevel
@@ -382,7 +382,7 @@ module Precedence = struct
| TConst _
| Tnull | TLval (TResult _,TNoOffset) | Tcomprehension _ | Tempty_set -> 0
| Tif (_, _, _) -> questionLevel
- | TLogic_coerce(_,e) -> (getParenthLevelLogic e.term_node) + 1
+ | TCast (true,_,e) -> (getParenthLevelLogic e.term_node) + 1
(* Create an expression of the same shape, and use {!getParenthLevel} *)
let getParenthLevelAttrParam = function
@@ -468,12 +468,12 @@ let is_same_direction_rel dir op =
let remove_no_op_coerce t =
match t.term_node with
- | TLogic_coerce (ty,t) when Cil.no_op_coerce ty t -> t
+ | TCast (true, ty,t) when Cil.no_op_coerce ty t -> t
| _ -> t
let rec is_singleton t =
match t.term_node with
- | TLogic_coerce(Ltype ({ lt_name = "set"},_), t') -> is_singleton t'
+ | TCast (true, Ltype ({ lt_name = "set"},_), t') -> is_singleton t'
| _ -> not (Logic_const.is_set_type t.term_type)
(* when pretty-printing relation chains, a < b && b' < c, it can happen that
@@ -2547,7 +2547,7 @@ class cil_printer () = object (self)
fprintf fmt "@[%a@]" self#tand_list (get_tand_list l [r])
| TBinOp (op,l,r) ->
fprintf fmt "@[%a@ %a@ %a@]" term l self#term_binop op term r
- | TCastE (ty,t) ->
+ | TCast (false, Ctype ty,t) ->
begin match ty, t.term_node with
| TFloat(fk,_) , TConst(LReal r as cst) when
not Kernel.(is_debug_key_enabled dkey_print_logic_coercions) &&
@@ -2556,6 +2556,8 @@ class cil_printer () = object (self)
| _ ->
fprintf fmt "(%a)%a" (self#typ None) ty term t
end
+ | TCast(false,_,_) ->
+ Kernel.fatal "Found a TCast to ctype without a Ctype associated"
| TAddrOf lv ->
fprintf fmt "&%a" (self#term_lval_prec Precedence.addrOfLevel) lv
| TStartOf lv ->
@@ -2659,7 +2661,7 @@ class cil_printer () = object (self)
self#quantifiers args)
pp_defn
term body
- | TLogic_coerce(ty,t) ->
+ | TCast (true, ty,t) ->
if (not (Cil.no_op_coerce ty t)) ||
Kernel.is_debug_key_enabled Kernel.dkey_print_logic_coercions
then
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 97cbc21081f..bdd64597f86 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -660,7 +660,7 @@ and pp_term_node fmt = function
| TUnOp(unop,term) -> Format.fprintf fmt "TUnOp(%a,%a)" pp_unop unop pp_term term
| TBinOp(binop,term1,term2) ->
Format.fprintf fmt "TBinOp(%a,%a,%a)" pp_binop binop pp_term term1 pp_term term2
- | TCastE(typ,term) -> Format.fprintf fmt "TCastE(%a,%a)" pp_typ typ pp_term term
+ | TCast(logic,typ,term) -> Format.fprintf fmt "TCast(%a,%a,%a)" pp_bool logic pp_logic_type typ pp_term term
| TAddrOf(term_lval) -> Format.fprintf fmt "TAddrOf(%a)" pp_term_lval term_lval
| TStartOf(term_lval) -> Format.fprintf fmt "TStartOf(%a)" pp_term_lval term_lval
| Tapp(logic_info,logic_label_list,term_list) ->
@@ -681,8 +681,6 @@ and pp_term_node fmt = function
| Tblock_length(logic_label,term) ->
Format.fprintf fmt "Tblock_length(%a,%a)" pp_logic_label logic_label pp_term term
| Tnull -> Format.fprintf fmt "Tnull"
- | TLogic_coerce(logic_type,term) ->
- Format.fprintf fmt "TLogic_coerce(%a,%a)" pp_logic_type logic_type pp_term term
| TUpdate(term1,term_offset,term2) ->
Format.fprintf fmt "TUpdate(%a,%a,%a)" pp_term term1 pp_term_offset term_offset pp_term term2
| Ttypeof(term) -> Format.fprintf fmt "Ttypeof(%a)" pp_term term
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 222d4c77a26..3b73ea2acc6 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -582,8 +582,8 @@ and is_same_term_node t t' env =
| TUnOp(op,t), TUnOp(op',t') -> Unop.equal op op' && is_same_term t t' env
| TBinOp(op,t1,t2), TBinOp(op',t1',t2') ->
Binop.equal op op' && is_same_term t1 t1' env && is_same_term t2 t2' env
- | TCastE(typ,term), TCastE(typ',term') ->
- is_same_type typ typ' env && is_same_term term term' env
+ | TCast(is_logic, typ, term), TCast(is_logic', typ', term') ->
+ is_logic = is_logic' && is_same_logic_type typ typ' env && is_same_term term term' env
| TAddrOf lv, TAddrOf lv'
| TStartOf lv, TStartOf lv' -> is_same_term_lval lv lv' env
| Tapp(f,labs,args), Tapp(f',labs',args') ->
@@ -609,8 +609,6 @@ and is_same_term_node t t' env =
| Tblock_length(l,t), Tblock_length(l',t') ->
is_same_logic_label l l' env && is_same_term t t' env
| Tnull, Tnull -> true
- | TLogic_coerce(typ,t), TLogic_coerce(typ',t') ->
- is_same_logic_type typ typ' env && is_same_term t t' env
| TUpdate(a,o,v), TUpdate(a',o',v') ->
is_same_term a a' env &&
is_same_term_offset o o' env &&
@@ -634,9 +632,9 @@ and is_same_term_node t t' env =
is_same_term t t' env
end else false
| (TConst _ | TLval _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
- | TAlignOfE _ | TUnOp _ | TBinOp _ | TCastE _ | TAddrOf _ | TStartOf _
+ | TAlignOfE _ | TUnOp _ | TBinOp _ | TCast _ | TAddrOf _ | TStartOf _
| Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _ | Tbase_addr _
- | Toffset _ | Tblock_length _ | Tnull | TLogic_coerce _ | TUpdate _
+ | Toffset _ | Tblock_length _ | Tnull | TUpdate _
| Ttypeof _ | Ttype _ | Tempty_set | Tunion _ | Tinter _ | Tcomprehension _
| Tlet _ | Trange _), _ -> false
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index e1c019546c4..5030a6d76bd 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -307,7 +307,7 @@ let constant_term loc i =
let rec is_null_term t = match t.term_node with
| TConst c when is_integral_logic_const c ->
Integer.equal (value_of_integral_logic_const c) Integer.zero
- | TCastE(_,t) -> is_null_term t
+ | TCast(false, _,t) -> is_null_term t
| _ -> false
(* ************************************************************************** *)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 6a38cc02b36..4a40c63ae67 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1467,10 +1467,15 @@ and childrenTermNode vis tn =
let t1' = vTerm t1 in
let t2' = vTerm t2 in
if t1' != t1 || t2' != t2 then TBinOp(op,t1',t2') else tn
- | TCastE(ty,te) ->
+ | TCast(false, Ctype ty,te) ->
let ty' = vTyp ty in
let te' = vTerm te in
- if ty' != ty || te' != te then TCastE(ty',te') else tn
+ if ty' != ty || te' != te then TCast(false, Ctype ty',te') else tn
+ | TCast (true, ty,t) ->
+ let ty' = visitCilLogicType vis ty in
+ let t' = visitCilTerm vis t in
+ if ty' != ty || t' != t then TCast (true, ty',t') else tn
+ | TCast(false,_,_) -> Kernel.fatal "TCast to ctype without Ctype"
| TAddrOf tl ->
let tl' = vTermLval tl in
if tl' != tl then TAddrOf tl' else tn
@@ -1552,10 +1557,6 @@ and childrenTermNode vis tn =
let def'= visitCilLogicInfo vis def in
let body' = visitCilTerm vis body in
if def != def' || body != body' then Tlet(def',body') else tn
- | TLogic_coerce(ty,t) ->
- let ty' = visitCilLogicType vis ty in
- let t' = visitCilTerm vis t in
- if ty' != ty || t' != t then TLogic_coerce(ty',t') else tn
and visitCilLogicLabel vis l =
doVisitCil vis
@@ -3186,14 +3187,14 @@ let isZero (e: exp) : bool =
let rec isLogicZero t = match t.term_node with
| TConst (Integer (n,_)) -> Integer.equal n Integer.zero
| TConst (LChr c) -> Char.code c = 0
- | TCastE(_, t) -> isLogicZero t
+ | TCast(false, _, t) -> isLogicZero t
| _ -> false
let isLogicNull t =
isLogicZero t ||
(let rec aux t = match t.term_node with
| Tnull -> true
- | TCastE(_, t) -> aux t
+ | TCast(false,_, t) -> aux t
| _ -> false
in aux t)
@@ -3461,7 +3462,7 @@ let rec stripCasts (e: exp) =
match e.enode with CastE(_, e') -> stripCasts e' | _ -> e
let rec stripTermCasts (t: term) =
- match t.term_node with TCastE(_, t') -> stripTermCasts t' | _ -> t
+ match t.term_node with TCast(false,_, t') -> stripTermCasts t' | _ -> t
(* Separate out the storage-modifier name attributes *)
let separateStorageModifiers (al: attribute list) =
@@ -7356,7 +7357,7 @@ let rec free_vars_term bound_vars t = match t.term_node with
| TSizeOfE t
| TAlignOfE t
| TUnOp (_,t)
- | TCastE (_,t)
+ | TCast (_,_,t)
| Tat (t,_)
| Toffset (_,t)
| Tbase_addr (_,t)
@@ -7429,7 +7430,6 @@ let rec free_vars_term bound_vars t = match t.term_node with
free_vars_term (Logic_var.Set.add d.l_var_info bound_vars) b
in
Logic_var.Set.union fvd fvb
- | TLogic_coerce(_,t) -> free_vars_term bound_vars t
and free_vars_lval bv (h,o) =
Logic_var.Set.union
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 0e02f014f61..ef018a9add1 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -93,7 +93,7 @@ let rank_term = function
| TAlignOfE _ -> 6
| TUnOp _ -> 7
| TBinOp _ -> 8
- | TCastE _ -> 9
+ | TCast (false,_,_) -> 9
| TAddrOf _ -> 10
| TStartOf _ -> 11
| Tapp _ -> 12
@@ -114,7 +114,7 @@ let rank_term = function
| Tlet _ -> 29
| Tcomprehension _ -> 30
| Toffset _ -> 31
- | TLogic_coerce _ -> 32
+ | TCast (true, _,_) -> 32
let rank_predicate = function
| Pfalse -> 0
@@ -1638,9 +1638,11 @@ let rec compare_term t1 t2 =
if c <> 0 then c else
let cx = compare_term x1 x2 in
if cx <> 0 then cx else compare_term y1 y2
- | TCastE(ty1,t1) , TCastE(ty2,t2) ->
- let c = Typ.compare ty1 ty2 in
- if c <> 0 then c else compare_term t1 t2
+ | TCast (false, ty1,e1), TCast (false, ty2,e2)
+ | TCast (true, ty1,e1) , TCast (true, ty2,e2) ->
+ let ct = Logic_type.compare ty1 ty2 in
+ if ct <> 0 then ct
+ else compare_term e1 e2
| Tapp(f1,labs1,ts1) , Tapp(f2,labs2,ts2) ->
let cf = Logic_info.compare f1 f2 in
if cf <> 0 then cf else
@@ -1683,18 +1685,13 @@ let rec compare_term t1 t2 =
else
let cq = compare_list Logic_var.compare q1 q2 in
if cq <> 0 then cq else Option.compare compare_predicate p1 p2
- | TLogic_coerce(ty1,e1), TLogic_coerce(ty2,e2) ->
- let ct = Logic_type.compare ty1 ty2 in
- if ct <> 0 then ct
- else compare_term e1 e2
| (TConst _ | TLval _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
- | TAlignOfE _ | TUnOp _ | TBinOp _ | TCastE _ | TAddrOf _ | TStartOf _
+ | TAlignOfE _ | TUnOp _ | TBinOp _ | TCast _ | TAddrOf _ | TStartOf _
| Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
| Tbase_addr _ | Tblock_length _ | Toffset _
| Tnull | TUpdate _ | Ttypeof _
| Ttype _ | Tempty_set | Tunion _ | Tinter _ | Tcomprehension _
- | Trange _ | Tlet _
- | TLogic_coerce _), _ -> assert false
+ | Trange _ | Tlet _ ), _ -> assert false
and compare_tlval (h1,off1) (h2,off2) =
let ch = compare_tlhost h1 h2 in
@@ -1854,9 +1851,12 @@ let rec hash_term (acc,depth,tot) t =
hash_term (acc+19+Hashtbl.hash bop,depth-1,tot-2) t1
in
hash_term (hash1,depth-1,tot1) t2
- | TCastE(ty,t) ->
+ | TCast(false, Ctype ty,t) ->
let hash1 = Typ.hash ty in
hash_term (acc+23+hash1,depth-1,tot-2) t
+ | TCast(true,_,e) -> hash_term (acc + 113, depth - 1, tot - 1) e
+ (* TODO (NB) : Check the magic values here (see if it can't be merged) *)
+ | TCast(false,_,_) -> assert false
| TAddrOf lv -> hash_tlval (acc+29,depth-1,tot-1) lv
| TStartOf lv -> hash_tlval (acc+31,depth-1,tot-1) lv
| Tapp (li,labs,apps) ->
@@ -1935,7 +1935,6 @@ let rec hash_term (acc,depth,tot) t =
hash_term
(acc + 109 + Hashtbl.hash li.l_var_info.lv_name, depth-1, tot-1)
t
- | TLogic_coerce(_,e) -> hash_term (acc + 113, depth - 1, tot - 1) e
end
and hash_tlval (acc,depth,tot) (h,o) =
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index ccea4480273..34d0e0a7f32 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -309,10 +309,10 @@ let tat ?(loc=Cil_datatype.Location.unknown) (t,label) =
let told ?(loc=Cil_datatype.Location.unknown) t = tat ~loc (t,old_label)
let tcast ?(loc=Cil_datatype.Location.unknown) t ct =
- term ~loc (TCastE (ct, t)) (Ctype ct)
+ term ~loc (TCast(false, Ctype ct, t)) (Ctype ct)
let tlogic_coerce ?(loc=Cil_datatype.Location.unknown) t lt =
- term ~loc (TLogic_coerce (lt, t)) lt
+ term ~loc (TCast (true, lt, t)) lt
let tvar ?(loc=Cil_datatype.Location.unknown) lv =
term ~loc (TLval(TVar lv,TNoOffset)) lv.lv_type
diff --git a/src/kernel_services/ast_queries/logic_to_c.ml b/src/kernel_services/ast_queries/logic_to_c.ml
index 2b0ab82e024..971013e5757 100644
--- a/src/kernel_services/ast_queries/logic_to_c.ml
+++ b/src/kernel_services/ast_queries/logic_to_c.ml
@@ -115,7 +115,7 @@ and loc_to_exp ?result {term_node = lnode ; term_type = ltype; term_loc = loc} =
(* TODO: Very likely to fail on large integer and incorrect on reals not
representable as floats *)
[new_exp ~loc (Const (Logic_utils.lconstant_to_constant constant))]
- | TCastE (typ, lexp) ->
+ | TCast (false, Ctype typ, lexp) ->
List.map
(fun x -> new_exp ~loc (CastE (typ, x))) (loc_to_exp ?result lexp)
| TAlignOf typ -> [new_exp ~loc (AlignOf typ)]
@@ -129,15 +129,15 @@ and loc_to_exp ?result {term_node = lnode ; term_type = ltype; term_loc = loc} =
| Tinter _ | Tcomprehension _ -> error_lval()
| Tat ({term_node = TAddrOf (TVar _, TNoOffset)} as taddroflval, _) ->
loc_to_exp ?result taddroflval
- | TLogic_coerce(Linteger, t) when Logic_typing.is_integral_type t.term_type ->
+ | TCast (true, Linteger, t) when Logic_typing.is_integral_type t.term_type ->
loc_to_exp ?result t
- | TLogic_coerce(Lreal, t) when Logic_typing.is_integral_type t.term_type ->
+ | TCast (true, Lreal, t) when Logic_typing.is_integral_type t.term_type ->
List.map
(fun x -> new_exp ~loc (CastE (logic_type_to_typ Lreal, x)))
(loc_to_exp ?result t)
- | TLogic_coerce(Lreal, t) when Logic_typing.is_arithmetic_type t.term_type ->
+ | TCast (true, Lreal, t) when Logic_typing.is_arithmetic_type t.term_type ->
loc_to_exp ?result t
- | TLogic_coerce (set, t)
+ | TCast (true, set, t)
when
Logic_const.is_set_type set &&
Logic_utils.is_same_type
@@ -154,7 +154,7 @@ and loc_to_exp ?result {term_node = lnode ; term_type = ltype; term_loc = loc} =
| Toffset _
| Tblock_length _
| TUpdate _ | Ttypeof _ | Ttype _
- | TLogic_coerce _
+ | TCast _
-> error_lval ()
let rec loc_to_lval ?result t =
@@ -167,7 +167,7 @@ let rec loc_to_lval ?result t =
(* coercions to arithmetic types cannot be lval. We only have to consider
a coercion to set here.
*)
- | TLogic_coerce(set, t) when
+ | TCast (true, set, t) when
Logic_typing.is_set_type set &&
Logic_utils.is_same_type
(Logic_typing.type_of_set_elem set) t.term_type ->
@@ -175,10 +175,10 @@ let rec loc_to_lval ?result t =
| Tinter _ -> error_lval() (* TODO *)
| Tcomprehension _ -> error_lval()
| TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
- | TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
+ | TConst _ | TCast _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
| Tat _ | Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull | Trange _
| TDataCons _ | TUpdate _ | Tlambda _
- | Ttypeof _ | Ttype _ | Tlet _ | TLogic_coerce _ ->
+ | Ttypeof _ | Ttype _ | Tlet _ ->
error_lval ()
let loc_to_offset ?result loc =
@@ -198,11 +198,10 @@ let loc_to_offset ?result loc =
| Tempty_set -> h,[]
| Trange _ | TAddrOf _ | Tat _
| TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
- | TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
+ | TConst _ | TCast _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
| Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull
| TDataCons _ | TUpdate _ | Tlambda _
| Ttypeof _ | Ttype _ | Tcomprehension _ | Tinter _ | Tlet _
- | TLogic_coerce _
-> error_lval ()
in snd (aux None loc.term_node)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 4cfddc62f89..1eac2474cd7 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -192,10 +192,10 @@ let optimize_comprehension term =
let lv = Logic_const.addTermOffsetLval o lv in
let ty = Cil.typeOfTermLval lv in
Logic_utils.mk_logic_StartOf (Logic_const.term ~loc (TLval lv) ty))
- | TLogic_coerce(lt,{ term_node = TLval(TVar y,TNoOffset)}) when is_x y ->
+ | TCast (true, lt,{ term_node = TLval(TVar y,TNoOffset)}) when is_x y ->
(* { (lt)x | \subset(x, set) } -> (lt set)set *)
{ t with
- term_node = TLogic_coerce(Logic_const.make_set_type lt,set);
+ term_node = TCast (true, Logic_const.make_set_type lt,set);
term_type = Logic_const.make_set_type lt }
| _ -> term
in
@@ -206,8 +206,8 @@ let optimize_comprehension term =
{ pred_content =
Papp({l_var_info = {lv_name="\\subset"}},[],[elt;set]) }) ->
(match elt.term_node with
- | TLogic_coerce
- (_,
+ | TCast
+ (true,_,
{ term_node =
TLval(TVar y, TNoOffset) })
when Cil_datatype.Logic_var.equal x y ->
@@ -228,22 +228,22 @@ let lift_set f loc =
| Tempty_set -> loc
(* coercion from a set to another set: keep the current coercion
over the result of the transformation. *)
- | TLogic_coerce(set,t1)
+ | TCast (true, set,t1)
when is_set_type set && is_set_type t1.term_type ->
let res = aux t1 in
- { loc with term_node = TLogic_coerce(set, res) }
+ { loc with term_node = TCast (true, set, res) }
(* coercion from a singleton to a set: performs the transformation.
*)
- | TLogic_coerce(oset, t1) when is_set_type oset ->
+ | TCast (true, oset, t1) when is_set_type oset ->
let t = f t1 in
let nset = make_set_type t.term_type in
(* performs the coercion into a set. *)
let singleton_coerce =
- { t with term_node = TLogic_coerce(nset, t); term_type = nset }
+ { t with term_node = TCast (true, nset, t); term_type = nset }
in
(* see whether we have to coerce the set type itself. *)
if is_same_type oset nset then singleton_coerce
- else { loc with term_node = TLogic_coerce(oset, singleton_coerce) }
+ else { loc with term_node = TCast (true, oset, singleton_coerce) }
(* if we a term of type set, try to apply f to each
element of x by using a comprehension, and see whether we can get
rid of said comprehension afterwards. *)
@@ -257,7 +257,7 @@ let lift_set f loc =
let t2 = Logic_const.tvar ~loc:loc.term_loc x in
let t2 =
Logic_const.term
- ~loc:loc.term_loc (TLogic_coerce (loc.term_type,t2)) loc.term_type
+ ~loc:loc.term_loc (TCast (true, loc.term_type,t2)) loc.term_type
in
let p = Logic_const.papp ~loc:loc.term_loc (sub, [], [t2;loc]) in
let c = { loc with term_node = Tcomprehension(t,[x],Some p) } in
@@ -1057,7 +1057,7 @@ struct
| TLval _ -> true
| TUnOp(_,t) -> needs_at t
| TBinOp(_,t1,t2) -> needs_at t1 || needs_at t2
- | TCastE(_,t) -> needs_at t
+ | TCast(_,_,t) -> needs_at t
| TAddrOf (_,o) -> needs_at_offset o
| TStartOf (_,o) -> needs_at_offset o
| Tapp(_,_,l) | TDataCons(_,l) -> List.exists needs_at l
@@ -1071,7 +1071,6 @@ struct
| Trange (Some t1, Some t2) -> needs_at t1 || needs_at t2
| Tlet(_,t) -> needs_at t
| Tif(t1,t2,t3) -> needs_at t1 || needs_at t2 || needs_at t3
- | TLogic_coerce(_,t) -> needs_at t
and needs_at_offset = function
| TNoOffset -> false
| TIndex (t,o) -> needs_at t || needs_at_offset o
@@ -1124,7 +1123,7 @@ struct
if isPointerType newt && isLogicNull e && not (isLogicZero e) then
(* \null can have any pointer type, see ACSL manual. *)
(if force then
- Logic_const.term ~loc (TCastE (newt, e)) (Ctype newt)
+ Logic_const.term ~loc (TCast (false, Ctype newt, e)) (Ctype newt)
else
{ e with term_type = Ctype newt })
else if isPointerType newt && isArrayType oldt then begin
@@ -1225,13 +1224,13 @@ struct
| Tinter l ->
{ e with term_type = real_type; term_node = Tinter (List.map aux l) }
| Tempty_set -> { e with term_type = real_type }
- | TLogic_coerce(t2,e) when Cil.no_op_coerce t2 e ->
+ | TCast (true,t2,e) when Cil.no_op_coerce t2 e ->
let e = aux e in
- { e with term_type = real_type; term_node = TLogic_coerce(real_type,e) }
+ { e with term_type = real_type; term_node = TCast (true, real_type,e) }
| _ when Cil.isLogicArithmeticType real_type ->
Logic_utils.numeric_coerce real_type e
| _ ->
- { e with term_type = real_type; term_node = TLogic_coerce(real_type,e) }
+ { e with term_type = real_type; term_node = TCast (true, real_type,e) }
in
if is_same_type e.term_type t then e else aux e
@@ -1248,7 +1247,7 @@ struct
let range = trange ~loc (Some (lzero ~loc ()), Some sizeof) in
let converted_type = set_conversion (Ctype Cil.charPtrType) t.term_type
in
- let cast = term ~loc (TCastE(Cil.charPtrType, t)) converted_type in
+ let cast = term ~loc (TCast(false, Ctype Cil.charPtrType, t)) converted_type in
term ~loc (TBinOp(PlusPI,cast,range)) (make_set_type converted_type)
in
lift_set convert_one_location t
@@ -1263,7 +1262,7 @@ struct
if explicit then begin
match Logic_const.unroll_ltdef newt with
| Ctype cnewt ->
- { e with term_node = TCastE(cnewt,e); term_type = newt }
+ { e with term_node = TCast(false, Ctype cnewt,e); term_type = newt }
| _ -> e
end else e
end else if is_enum_cst e newt then { e with term_type = newt }
@@ -1284,7 +1283,7 @@ struct
logic_coerce Linteger e
| t1, Ctype t2 when Logic_const.is_boolean_type t1
&& is_integral_type newt && explicit ->
- Logic_const.term ~loc (TCastE (t2,e)) newt
+ Logic_const.term ~loc (TCast (false, Ctype t2,e)) newt
| ty1, Ltype({lt_name="set"},[ty2])
when is_pointer_type ty1 &&
is_plain_pointer_type ty2 &&
@@ -1429,7 +1428,7 @@ struct
(* Integer 0 is also a valid pointer. *)
| Linteger, Ctype ty when Cil.isPointerType ty && isLogicNull oterm ->
nt, { oterm with
- term_node = TCastE(ty,oterm);
+ term_node = TCast(false, Ctype ty,oterm);
term_type = nt }
| Linteger, Ctype ty when Cil.isIntegralType ty ->
(try
@@ -2058,7 +2057,7 @@ struct
known_vars, kont (eta_expand term.term_loc term.term_name env v)
| TConst _ | TLval _ | TSizeOf _ | TSizeOfE _
| TSizeOfStr _ | TAlignOf _ | TAlignOfE _
- | TUnOp _ | TBinOp _ | TCastE _ | TAddrOf _ | TStartOf _
+ | TUnOp _ | TBinOp _ | TCast _ | TAddrOf _ | TStartOf _
| Tapp _ | TDataCons _ | Tbase_addr _ | Toffset _
| Tblock_length _ | Tnull
| TUpdate _ | Ttypeof _ | Ttype _ | Tempty_set
@@ -2068,7 +2067,7 @@ struct
idea that you can always replace a term by a set of terms
*)
| Tunion _ | Tinter _ | Tcomprehension _
- | Trange _ | TLogic_coerce _
+ | Trange _
-> known_vars, kont term
| Tlambda (quants,term) ->
@@ -2366,11 +2365,11 @@ struct
| Tunion l | Tinter l -> List.for_all aux l
- | TLogic_coerce (_,t) | Tat (t, _) | Tcomprehension (t,_,_) | Tlet (_, t)
+ | TCast (true,_,t) | Tat (t, _) | Tcomprehension (t,_,_) | Tlet (_, t)
-> aux t
| Trange _ | TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
- | TAlignOfE _ | TUnOp (_,_) | TBinOp (_,_,_) | TCastE (_,_)
+ | TAlignOfE _ | TUnOp (_,_) | TBinOp (_,_,_) | TCast (false,_,_)
| Tlambda (_,_) | TDataCons (_,_) | Tbase_addr (_,_)
| Toffset (_,_) | Tblock_length (_,_) | Tnull | Tapp _
| TUpdate (_,_,_) | Ttypeof _ | Ttype _ ->
@@ -3159,7 +3158,7 @@ struct
let check_lval t =
match t.term_node with
TLval lv
- | TLogic_coerce(_,{term_node = TLval lv })
+ | TCast (true, _,{term_node = TLval lv })
| Tat({term_node = TLval lv},_) -> f lv t
| TStartOf lv
| Tat ({term_node = TStartOf lv}, _) ->
@@ -3183,7 +3182,7 @@ struct
term_type = type_of_pointed t.term_type;
term_node = TLval lv }
| TLval lv
- | TLogic_coerce(_,{term_node = TLval lv })
+ | TCast (true, _,{term_node = TLval lv })
| Tat({term_node = TLval lv},_) -> f lv t
| TStartOf lv
| Tat ({term_node = TStartOf lv}, _)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 7a2b471b5d8..3dcd4013e17 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -236,16 +236,16 @@ let mk_cast ?loc ?(force=false) newt t =
let newt' = Cil.type_remove_attributes_for_logic_type newt in
if equal_ltype (Ctype newt') t.term_type then t else
let rec unroll_cast e = match e.term_node with
- | TCastE(oldt,e)
+ | TCast(false, Ctype oldt,e)
when (Cil.isPointerType newt' && Cil.isPointerType oldt)
|| equal_ltype
(Ctype (Cil.type_remove_attributes_for_logic_type oldt))
(Ctype newt')
-> unroll_cast e
- | TLogic_coerce(Linteger,e)
+ | TCast(true,Linteger,e)
when Cil.isArithmeticOrPointerType newt'
-> unroll_cast e
- | TLogic_coerce(Lreal,e)
+ | TCast(true,Lreal,e)
when Cil.isFloatingType newt'
-> unroll_cast e
| _ -> e
@@ -254,7 +254,7 @@ let mk_cast ?loc ?(force=false) newt t =
let loc = match loc with None -> t.term_loc | Some loc -> loc in
(* we keep newt as the cast target, as newt' might have unrolled typedefs
in order to remove attributes, resulting in a less user-friendly type *)
- Logic_const.term ~loc (TCastE (newt, tres)) (Ctype newt')
+ Logic_const.term ~loc (TCast (false, Ctype newt, tres)) (Ctype newt')
(* -------------------------------------------------------------------------- *)
@@ -319,23 +319,23 @@ let parse_float ?loc literal =
let vreal = Logic_const.term ?loc (TConst(LReal creal)) Lreal in
if is_flt then
let ty = TFloat(fk,[]) in
- Logic_const.term ?loc (TCastE(ty,vreal)) (Ctype ty)
+ Logic_const.term ?loc (TCast(false, Ctype ty,vreal)) (Ctype ty)
else vreal
let mk_coerce ltyp t =
- Logic_const.term ~loc:t.term_loc (TLogic_coerce(ltyp, t)) ltyp
+ Logic_const.term ~loc:t.term_loc (TCast (true, ltyp, t)) ltyp
let rec numeric_coerce ltyp t =
let oldt = unroll_type t.term_type in
match t.term_node with
- | TLogic_coerce(lt,e) when Cil.no_op_coerce lt e ->
+ | TCast (true, 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) ->
+ | TCast (false, Ctype 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 }
@@ -658,7 +658,7 @@ let array_with_range arr size =
let remove_logic_coerce t =
match t.term_node with
- | TLogic_coerce(_,t) -> t
+ | TCast (true, _,t) -> t
| _ -> t
let rec remove_term_offset o =
@@ -954,8 +954,8 @@ let rec is_same_term t1 t2 =
| TUnOp (o1,t1), TUnOp(o2,t2) -> o1 = o2 && is_same_term t1 t2
| TBinOp(o1,l1,r1), TBinOp(o2,l2,r2) ->
is_same_binop o1 o2 && is_same_term l1 l2 && is_same_term r1 r2
- | TCastE(typ1,t1), TCastE(typ2,t2) ->
- Cil_datatype.TypByName.equal typ1 typ2 && is_same_term t1 t2
+ | TCast (b1, ty1,t1), TCast (b2, ty2,t2) ->
+ b1 = b2 && is_same_type ty1 ty2 && is_same_term t1 t2
| TAddrOf l1, TAddrOf l2 -> is_same_tlval l1 l2
| TStartOf l1, TStartOf l2 -> is_same_tlval l1 l2
| Tapp(f1,labels1, args1), Tapp(f2, labels2, args2) ->
@@ -993,15 +993,13 @@ let rec is_same_term t1 t2 =
is_same_opt is_same_term l1 l2 && is_same_opt is_same_term h1 h2
| Tlet(d1,b1), Tlet(d2,b2) ->
is_same_logic_info d1 d2 && is_same_term b1 b2
- | TLogic_coerce(ty1,t1), TLogic_coerce(ty2,t2) ->
- is_same_type ty1 ty2 && is_same_term t1 t2
| (TConst _ | TLval _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _
- | TAlignOf _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TCastE _
+ | TAlignOf _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TCast _
| TAddrOf _ | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _
| Tif _ | Tat _ | Tbase_addr _ | Tblock_length _ | Toffset _ | Tnull
| TUpdate _ | Ttypeof _ | Ttype _
| Tcomprehension _ | Tempty_set | Tunion _ | Tinter _ | Trange _
- | Tlet _ | TLogic_coerce _
+ | Tlet _
),_ -> false
and is_same_logic_info l1 l2 =
@@ -1508,9 +1506,14 @@ let rec hash_term (acc,depth,tot) t =
hash_term (acc+152+Hashtbl.hash bop,depth-1,tot-2) t1
in
hash_term (hash1,depth-1,tot1) t2
- | TCastE(ty,t) ->
+ | TCast (false, Ctype ty,t) ->
let hash1 = Cil_datatype.TypByName.hash ty in
hash_term (acc+171+hash1,depth-1,tot-2) t
+ | TCast (true, _,t) ->
+ hash_term (acc + 587, depth - 1, tot - 1) t
+ | TCast (false, _,_) -> assert false
+ (* TODO (NB) : Should check the magic values here to see if we can merge
+ them *)
| TAddrOf lv -> hash_term_lval (acc+190,depth-1,tot-1) lv
| TStartOf lv -> hash_term_lval (acc+209,depth-1,tot-1) lv
| Tapp (li,labs,apps) -> hash_app (acc,depth,tot) li labs apps
@@ -1583,8 +1586,6 @@ let rec hash_term (acc,depth,tot) t =
hash_term
(acc + 570 + Hashtbl.hash li.l_var_info.lv_name, depth-1, tot-1)
t
- | TLogic_coerce(_,t) ->
- hash_term (acc + 587, depth - 1, tot - 1) t
end
and hash_app (acc,depth,tot) li labs apps =
@@ -1740,11 +1741,12 @@ let rec compare_term t1 t2 =
else res
| TBinOp _, _ -> 1
| _, TBinOp _ -> -1
- | TCastE(typ1,t1), TCastE(typ2,t2) ->
- let res = Cil_datatype.TypByName.compare typ1 typ2 in
+ | TCast (false, ty1,t1), TCast (false, ty2,t2)
+ | TCast (true, ty1,t1), TCast (true, ty2,t2) ->
+ let res = Cil_datatype.Logic_type_ByName.compare ty1 ty2 in
if res = 0 then compare_term t1 t2 else res
- | TCastE _, _ -> 1
- | _, TCastE _ -> -1
+ | TCast (false,_,_), _ -> 1
+ | _, TCast (false,_,_) -> -1
| TAddrOf l1, TAddrOf l2 -> compare_tlval l1 l2
| TAddrOf _, _ -> 1
| _, TAddrOf _ -> -1
@@ -1835,9 +1837,6 @@ let rec compare_term t1 t2 =
if res = 0 then compare_term b1 b2 else res
| Tlet _, _ -> 1
| _, Tlet _ -> -1
- | TLogic_coerce(ty1,t1), TLogic_coerce(ty2,t2) ->
- let res = Cil_datatype.Logic_type_ByName.compare ty1 ty2 in
- if res = 0 then compare_term t1 t2 else res
and compare_logic_info l1 l2 =
let res = compare_logic_signature l1 l2 in
@@ -2446,30 +2445,28 @@ let rec constFoldTermToInt ?(machdep=true) (e: term) : Integer.t option =
with Cil.SizeOfError _ -> None
end
| TAlignOfE _ -> None (* exp case is very complex, and possibly incorrect *)
- | TCastE (typ, e) -> constFoldCastToInt ~machdep typ e
+ | TCast (false, Ctype typ, e) -> constFoldCastToInt ~machdep typ e
+ | TCast (true, Linteger, e) -> constFoldTermToInt ~machdep e
| Toffset (_, t) -> if machdep then constFoldToffset t else None
| Tif (c, e1, e2) -> begin
- match constFoldTermToInt ~machdep c with
- | None -> None
- | Some i ->
- constFoldTermToInt ~machdep (if Integer.is_zero i then e2 else e1)
+ Option.bind (constFoldTermToInt ~machdep c)
+ (fun i -> constFoldTermToInt ~machdep (if Integer.is_zero i then e2 else e1))
end
- | TLogic_coerce (lt, e) ->
- if lt = Linteger then constFoldTermToInt ~machdep e else None
| Tnull -> Some Integer.zero
| Tapp (li, _, [{term_node = (Tunion args |
- TLogic_coerce (_, {term_node = Tunion args}))}])
+ TCast (true, _, {term_node = Tunion args}))}])
when is_max_function li ->
constFoldMinMax ~machdep Integer.max args
| Tapp (li, _, [{term_node = (Tunion args |
- TLogic_coerce (_, {term_node = Tunion args}))}])
+ TCast (true, _, {term_node = Tunion args}))}])
when is_min_function li ->
constFoldMinMax ~machdep Integer.min args
| TLval _ | TAddrOf _ | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _
| Tat _ | Tbase_addr _ | Tblock_length _
| TUpdate _ | Ttypeof _ | Ttype _ | Tempty_set | Tunion _ | Tinter _
- | Tcomprehension _ | Trange _ | Tlet _ ->
+ | Tcomprehension _ | Trange _ | Tlet _
+ | TCast _ ->
None
and constFoldCastToInt ~machdep typ e =
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 23685c5dde7..395295a3904 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -165,13 +165,12 @@ let isCrossableAtInit tr func =
bool_res (comp (Char.compare c1 c2))
| TConst(LReal r1), TConst (LReal r2) ->
bool_res (comp (compare r1.r_nearest r2.r_nearest))
- | TCastE(ty1,t1), TCastE(ty2,t2)
+ | TCast (false, Ctype ty1,t1), TCast (false, Ctype ty2,t2)
when Cil_datatype.Typ.equal ty1 ty2 ->
comparison comp t1 t2
| _ -> t
in
(match op, t1.term_node, t2.term_node with
-
| PlusA, TConst(Integer(i1,_)), TConst(Integer(i2,_)) ->
{ t with term_node =
TConst(Integer(Integer.add i1 i2,None))}
@@ -208,11 +207,11 @@ let isCrossableAtInit tr func =
| LOr, t1, t2 ->
bool3_res t (Bool3.bool3or (is_true t1) (is_true t2))
| _ -> t)
- | TCastE(ty,t1) ->
+ | TCast (false, Ctype ty,t1) ->
let t1 = aux t1 in
(match t1.term_type with
- Ctype ty1 when Cil_datatype.Typ.equal ty ty1 -> t1
- | _ -> { t with term_node = TCastE(ty,t1) })
+ | Ctype ty1 when Cil_datatype.Typ.equal ty ty1 -> t1
+ | _ -> { t with term_node = TCast (false, Ctype ty,t1) })
| _ -> t
and aux_lv (base,off) =
match base with
@@ -283,7 +282,8 @@ let isCrossableAtInit tr func =
Bool3.bool3_of_bool (comp (Char.compare c1 c2))
| TConst(LReal r1), TConst (LReal r2) ->
Bool3.bool3_of_bool (comp (compare r1.r_nearest r2.r_nearest))
- | TCastE(ty1,t1), TCastE(ty2,t2) when Cil_datatype.Typ.equal ty1 ty2 ->
+ | TCast (false, Ctype ty1,t1), TCast (false, Ctype ty2,t2)
+ when Cil_datatype.Typ.equal ty1 ty2 ->
comparison t1 t2
| _ -> Bool3.Undefined
in
@@ -419,7 +419,7 @@ let rec term_to_exp t res =
| TBinOp (binop, t1, t2)->
new_exp ~loc
(BinOp(binop, term_to_exp t1 res, term_to_exp t2 res, Cil.intType))
- | TCastE(ty, {term_node = TConst(LReal lreal)}) when Cil.isFloatingType ty ->
+ | TCast (false, Ctype ty, {term_node = TConst(LReal lreal)}) when Cil.isFloatingType ty ->
(match Cil.unrollType ty with
| TFloat(fk,_) ->
new_exp ~loc
@@ -427,10 +427,10 @@ let rec term_to_exp t res =
| _ ->
Aorai_option.fatal
"A floating-point type was expected, got %a." Printer.pp_typ ty)
- | TCastE (ty, t) -> new_exp ~loc (CastE (ty, term_to_exp t res))
+ | TCast (false, Ctype ty, t) -> new_exp ~loc (CastE (ty, term_to_exp t res))
| TAddrOf tlval -> new_exp ~loc (AddrOf (tlval_to_lval tlval res))
| TStartOf tlval -> new_exp ~loc (StartOf (tlval_to_lval tlval res))
- | TLogic_coerce (_,t) -> term_to_exp t res
+ | TCast (true, _,t) -> term_to_exp t res
| _ ->
Aorai_option.fatal
"Term %a cannot be transformed into exp."
@@ -510,7 +510,7 @@ let get_bhv_aux_fct kf bhv =
[Normal,
Logic_const.(
new_predicate
- (prel (Req,tlogic_coerce (tresult ret_typ) Linteger,lone())))]
+ (prel (Req, tlogic_coerce (tresult ret_typ) Linteger,lone())))]
in
let bhv_in =
Cil.mk_behavior ~name:bhv.b_name ~assumes ~assigns ~post_cond ()
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 7764bd1d100..7bf460e21c6 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -247,7 +247,7 @@ end = struct
let get_bounded_var t ctxt =
let rec aux t =
match t.term_node with
- | TLogic_coerce(_, t) -> aux t
+ | TCast (true, _, t) -> aux t
| TLval(TVar lv, TNoOffset) when Logic_var.Set.mem lv ctxt.bounded_vars ->
Some lv
| _ -> None
@@ -524,7 +524,7 @@ let extract_constraint ctxt t1 r t2 =
is not a variable ([TLval(TVar _, TNoOffset)]). *)
let rec _get_logic_var_opt t =
match t.term_node with
- | TLogic_coerce(_, t) -> _get_logic_var_opt t
+ | TCast (true, _, t) -> _get_logic_var_opt t
| TLval(TVar x, TNoOffset) -> Some x
| _ -> None
in
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 79f27b6ae31..679f8530323 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -392,10 +392,12 @@ let rec infer ~force ~logic_env t =
let i2 = infer ~force ~logic_env t2 in
Error.map2 (lift_arith_binop (ival_arith_binop op)) i1 i2
- | TCastE (ty, t) ->
+ | TCast (false, Ctype ty, t) ->
let src = infer ~force ~logic_env t in
let dst = interv_of_typ ty in
Error.map (fun src -> cast ~src ~dst) src
+ | TCast (true, _, t) -> get_res (infer ~force ~logic_env t)
+ | TCast (false, _,_) -> assert false
| Tif (t1, t2, t3) ->
ignore (infer ~force ~logic_env t1);
let logic_env_tbranch, logic_env_fbranch =
@@ -440,7 +442,6 @@ let rec infer ~force ~logic_env t =
| TPtr _ -> Lazy.force interv_of_unknown_block
| _ -> assert false)
| Tnull -> singleton_of_int 0
- | TLogic_coerce (_, t) -> get_res (infer ~force ~logic_env t)
| Tapp (li,_,args) ->
(match li.l_body with
| LBpred _ | LBterm _ ->
diff --git a/src/plugins/e-acsl/src/analyses/labels.ml b/src/plugins/e-acsl/src/analyses/labels.ml
index 36325279ded..29fe58ee990 100644
--- a/src/plugins/e-acsl/src/analyses/labels.ml
+++ b/src/plugins/e-acsl/src/analyses/labels.ml
@@ -324,8 +324,8 @@ end = struct
do_term ?error env t
| TLval lv | TAddrOf lv | TStartOf lv ->
do_term_lval ?error env lv
- | TSizeOfE t | TAlignOfE t | TUnOp (_, t) | TCastE (_, t) | Tlambda (_, t)
- | TLogic_coerce (_, t) ->
+ | TSizeOfE t | TAlignOfE t | TUnOp (_, t)
+ | TCast (_, _, t) | Tlambda (_, t) ->
do_term ?error env t
| TBinOp (_, t1, t2) ->
let error = do_term ?error env t1 in
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index e0aacb1c1fe..ccaa156f127 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -303,7 +303,7 @@ module rec Transfer
and register_term kf varinfos term = match term.term_node with
| TLval tlv | TAddrOf tlv | TStartOf tlv ->
register_term_lval kf varinfos tlv
- | TCastE(_, t) | Tat(t, _) ->
+ | TCast (_, _, t) | Tat(t, _) ->
register_term kf varinfos t
| Tlet(li, t) ->
if may_alias li then Error.not_yet "let-binding on array or pointer"
@@ -339,7 +339,6 @@ module rec Transfer
| Tbase_addr _ -> Error.not_yet "\\base_addr"
| Toffset _ -> Error.not_yet "\\offset"
| Tblock_length _ -> Error.not_yet "\\block_length"
- | TLogic_coerce(_, t) -> register_term kf varinfos t
| TUpdate _ -> Error.not_yet "functional update"
| Ttypeof _ -> Error.not_yet "typeof"
| Tempty_set -> Error.not_yet "empty set"
@@ -396,10 +395,10 @@ module rec Transfer
(* no left-value inside inside: skip for efficiency *)
Cil.SkipChildren
| TUnOp _ | TBinOp _ | Ttypeof _ | TSizeOfE _
- | TLval _ | TAlignOfE _ | TCastE _ | TAddrOf _
+ | TLval _ | TAlignOfE _ | TCast _ | TAddrOf _
| TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
| TUpdate _ | Tunion _ | Tinter _
- | Tcomprehension _ | Trange _ | TLogic_coerce _ ->
+ | Tcomprehension _ | Trange _ ->
(* potential sub-term inside *)
Cil.DoChildren
method !vlogic_label _ = Cil.SkipChildren
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 00650b57443..3dbec883bfe 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -428,7 +428,7 @@ let rec type_term
order to lower the number of explicit casts *)
let rec cast_first t1 t2 = match t1.term_node with
| TLval _ -> false
- | TLogic_coerce(_, t) -> cast_first t t2
+ | TCast (true, _, t) -> cast_first t t2
| _ -> true
in
let cast_first = cast_first t1 t2 in
@@ -457,7 +457,7 @@ let rec type_term
ignore (type_term ~use_gmp_opt:true ~ctx:c_int ~profile t2);
ty
- | TCastE(_, t') ->
+ | TCast (false, Ctype _, t') ->
(* compute the smallest interval from the whole term [t] *)
let i = Interval.get_from_profile ~profile t in
(* nothing more to do: [i] is already more precise than what we could
@@ -466,6 +466,14 @@ let rec type_term
ignore (type_term ~use_gmp_opt:true ~ctx ~profile t');
ctx
+ | TCast (true, _, t') ->
+ let i = Interval.get_from_profile ~profile t in
+ ignore (type_term ~use_gmp_opt ~arith_operand ?ctx ~profile t');
+ ty_of_interv ~use_gmp_opt i
+ (* TODO (NB) : Maybe can be merged ? *)
+
+ | TCast (false, _,_) -> assert false
+
| Tif (t1, t2, t3) ->
let ctx1 =
mk_ctx ~use_gmp_opt:false c_int (* an int must be generated *)
@@ -479,11 +487,6 @@ let rec type_term
ignore (type_term ~use_gmp_opt:true ~ctx ~profile t3);
ctx
- | TLogic_coerce (_, t') ->
- let i = Interval.get_from_profile ~profile t in
- ignore (type_term ~use_gmp_opt ~arith_operand ?ctx ~profile t');
- ty_of_interv ~use_gmp_opt i
-
| Tat (t, _) ->
(type_term ~use_gmp_opt ~arith_operand ?ctx ~profile t).ty
@@ -534,7 +537,7 @@ let rec type_term
the kernel introduces a coercion to integer, so we will
always see integer here.*)
begin match x.term_node with
- |TLogic_coerce _ -> None
+ | TCast (true,_,_) -> None
|_ -> if Options.Gmp_only.get() then Some Gmpz else None
end
| Lreal -> Some Real
@@ -567,7 +570,7 @@ let rec type_term
the kernel introduces a coercion to integer, so we will
always see integer here.*)
begin match x.term_node with
- | TLogic_coerce _ -> None
+ | TCast (true,_,_) -> None
|_ -> if Options.Gmp_only.get() then Some Gmpz else None
end
| Lreal -> Some Real
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index c025a21d251..c8d95953029 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -473,8 +473,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
match t.term_node with
| TConst _ -> "cst_"
| TLval (TVar { lv_name }, _) -> lv_name ^ "_"
- | TCastE (_, t) -> term_to_name t
- | TLogic_coerce (_, t) -> term_to_name t
+ | TCast (_,_, t) -> term_to_name t
| _ -> ""
in
let ctx = Typing.get_number_ty ~logic_env t in
@@ -724,7 +723,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
| C_float _ | Rational | Real | Nan ->
assert false
end
- | TCastE(ty, t') ->
+ | TCast (false, Ctype ty, t') ->
let e, adata, env = to_exp ~adata kf env t' in
let e, env =
Typed_number.add_cast
@@ -738,7 +737,8 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
e
in
e, adata, env, Analyses_types.C_number, ""
- | TLogic_coerce (_, t) -> context_insensitive_term_to_exp ~adata kf env t
+ | TCast (true, _, t) -> context_insensitive_term_to_exp ~adata kf env t
+ | TCast (false, _,_) -> assert false
| TAddrOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
let e = Cil.mkAddrOf ~loc lv in
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 6f7b8fe7f10..709c0be2138 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -604,9 +604,9 @@ let pass_logic_cast exn typ trm =
let is_same_term_coerce t1 t2 =
match t1.term_node, t2.term_node with
- | TLogic_coerce _, TLogic_coerce _ -> Logic_utils.is_same_term t1 t2
- | TLogic_coerce (_,t1), _ -> Logic_utils.is_same_term t1 t2
- | _, TLogic_coerce(_,t2) -> Logic_utils.is_same_term t1 t2
+ | TCast (true,_,_), TCast (true,_,_) -> Logic_utils.is_same_term t1 t2
+ | TCast (true, _,t1), _ -> Logic_utils.is_same_term t1 t2
+ | _, TCast (true, _,t2) -> Logic_utils.is_same_term t1 t2
| _ -> Logic_utils.is_same_term t1 t2
(* Constrain the ACSL range [idx] when it is used to access an array of
@@ -1142,7 +1142,7 @@ let rec eval_term ~alarm_mode env t =
etype = Cil.intType;
eunder; eover; empty; }
- | TCastE (typ, t) ->
+ | TCast (false, Ctype typ, t) ->
let r = eval_term ~alarm_mode env t in
(* See if the cast does something. If not, we can keep eunder as is.*)
if is_noop_cast ~src_typ:t.term_type ~dst_typ:typ
@@ -1153,6 +1153,36 @@ let rec eval_term ~alarm_mode env t =
let eover = cast ~src_typ:r.etype ~dst_typ:typ r.eover in
{ etype = typ; ldeps = r.ldeps; eunder = under_from_over eover; eover;
empty = r.empty; }
+ | TCast (false, _,_) -> assert false
+
+ | TCast (true, ltyp, t) ->
+ let r = eval_term ~alarm_mode env t in
+ (* we must handle coercion from singleton to set, for which there is
+ nothing to do, AND coercion from an integer type to a floating-point
+ type, that require a conversion. *)
+ (match Logic_const.plain_or_set Fun.id ltyp with
+ | Linteger when Logic_typing.is_integral_type t.term_type
+ || Logic_const.is_boolean_type t.term_type -> r
+ | Ctype typ when Cil.isIntegralOrPointerType typ -> r
+ | Lreal ->
+ let eover =
+ if Logic_typing.is_integral_type t.term_type
+ then V.cast_int_to_float Fval.Real r.eover
+ else V.cast_float_to_float Fval.Real r.eover
+ in
+ { etype = Cil.longDoubleType; (* hack until logic type *)
+ ldeps = r.ldeps;
+ eover; eunder = under_from_over eover;
+ empty = r.empty }
+ | _ ->
+ if Logic_const.is_boolean_type ltyp
+ && Logic_typing.is_integral_type t.term_type
+ then cast_to_bool r
+ else
+ unsupported
+ (Format.asprintf "logic coercion %a -> %a@."
+ Printer.pp_logic_type t.term_type Printer.pp_logic_type ltyp)
+ )
| Tif (tcond, ttrue, tfalse) ->
eval_tif eval_term Cvalue.V.join Cvalue.V.meet ~alarm_mode env
@@ -1193,35 +1223,6 @@ let rec eval_term ~alarm_mode env t =
eover = Cvalue.V.singleton_zero;
empty = false; }
- | TLogic_coerce(ltyp, t) ->
- let r = eval_term ~alarm_mode env t in
- (* we must handle coercion from singleton to set, for which there is
- nothing to do, AND coercion from an integer type to a floating-point
- type, that require a conversion. *)
- (match Logic_const.plain_or_set Fun.id ltyp with
- | Linteger when Logic_typing.is_integral_type t.term_type
- || Logic_const.is_boolean_type t.term_type -> r
- | Ctype typ when Cil.isIntegralOrPointerType typ -> r
- | Lreal ->
- let eover =
- if Logic_typing.is_integral_type t.term_type
- then V.cast_int_to_float Fval.Real r.eover
- else V.cast_float_to_float Fval.Real r.eover
- in
- { etype = Cil.longDoubleType; (* hack until logic type *)
- ldeps = r.ldeps;
- eover; eunder = under_from_over eover;
- empty = r.empty }
- | _ ->
- if Logic_const.is_boolean_type ltyp
- && Logic_typing.is_integral_type t.term_type
- then cast_to_bool r
- else
- unsupported
- (Format.asprintf "logic coercion %a -> %a@."
- Printer.pp_logic_type t.term_type Printer.pp_logic_type ltyp)
- )
-
(* TODO: the meaning of the label in \offset and \base_addr is not obvious
at all *)
| Toffset (_lbl, t) ->
@@ -1781,7 +1782,7 @@ and eval_term_as_lval ~alarm_mode env t =
| Tat (t, lab) ->
ignore (env_state env lab);
eval_term_as_lval ~alarm_mode { env with e_cur = lab } t
- | TLogic_coerce (_lt, t) ->
+ | TCast (true, _lt, t) ->
(* Logic coerce on locations (that are pointers) can only introduce
sets, that do not change the abstract value. *)
eval_term_as_lval ~alarm_mode env t
@@ -1816,7 +1817,7 @@ and eval_term_as_exact_locs ~alarm_mode env t =
if Locations.is_bottom_loc loc then raise Not_an_exact_loc;
Location (typ, loc)
- | TLogic_coerce (Lreal, t) -> begin
+ | TCast (true, Lreal, t) -> begin
match eval_term_as_exact_locs ~alarm_mode env t with
| Logic_var _ as x -> x
| Location (_, locs) as r ->
@@ -1841,13 +1842,13 @@ and eval_term_as_exact_locs ~alarm_mode env t =
r
end
- | TLogic_coerce (_, t) ->
- (* Otherwise it is always ok to pass through a TLogic_coerce, as the destination
+ | TCast (true, _, t) ->
+ (* Otherwise it is always ok to pass through a TCast (true,_,_), as the destination
type is always a supertype *)
eval_term_as_exact_locs ~alarm_mode env t
- | TCastE (ctype, t') ->
- pass_logic_cast Not_an_exact_loc (Ctype ctype) t';
+ | TCast (false, ctype, t') ->
+ pass_logic_cast Not_an_exact_loc ctype t';
eval_term_as_exact_locs ~alarm_mode env t'
| Tunion [t] ->
@@ -1947,7 +1948,7 @@ and reduce_by_valid env positive access (tset: term) =
| TLval tlval -> aux_lval tlval env
- | TCastE (typ, {term_node = TLval tlval}) -> aux_lval ~typ tlval env
+ | TCast (false, Ctype typ, {term_node = TLval tlval}) -> aux_lval ~typ tlval env
| TAddrOf (TMem {term_node = TLval tlval}, offs) ->
(try
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 96baad2451d..cad0d5b3b93 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -672,8 +672,7 @@ struct
| TUnOp(unop,t) -> term_unop unop (C.logic env t)
| TBinOp(binop,a,b) -> term_binop env binop a b
- | TCastE(ty,t) -> term_cast_to_ctype env ty t
- | TLogic_coerce(typ,t) -> term_cast_to_ltype env typ t
+ | TCast (_, typ,t) -> term_cast_to_ltype env typ t
| Tapp(f,ls,ts) ->
let vs = List.map (val_of_term env) ts in
@@ -941,8 +940,7 @@ struct
Warning.error "Complex let-binding not implemented yet (%a)"
Printer.pp_term t
- | TCastE (_,t)
- | TLogic_coerce(_,t) -> C.region env t
+ | TCast (_,_,t) -> C.region env t
| TBinOp _ | TUnOp _ | Trange _ | TUpdate _ | Tapp _ | Tif _
| TConst _ | Tnull | TDataCons _ | Tlambda _
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 3412bfc6824..5840be85cb8 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -122,7 +122,7 @@ let rec addr_of_lval ?loc term =
match term.term_node with
| TLval lv ->
Logic_utils.mk_logic_AddrOf ?loc lv typ
- | TCastE (_, t) | TLogic_coerce (_, t) ->
+ | TCast (_,_, t) ->
addr_of_lval ?loc t
| Tif(c, t, e) ->
let t = addr_of_lval ?loc t in
@@ -320,7 +320,7 @@ let assigned_via_pointers kf =
match t.term_node with
| TLval (TMem _, _) ->
true
- | TCastE (_, t) | TLogic_coerce (_, t)
+ | TCast (_,_, t)
| Tcomprehension(t, _, _) | Tat (t, _) ->
assigned_via_pointer t
| Tunion l | Tinter l ->
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 958a36bfde7..13e0908d44a 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -419,8 +419,9 @@ and term (env:ctx) (t:term) : model = match t.term_node with
| TBinOp((PlusPI|MinusPI),a,b) -> shift (term env a) (vterm env b)
(* Casts *)
- | TCastE(ty_tgt,t) -> cast (cast_ltyp ty_tgt t.term_type) (term env t)
- | TLogic_coerce (_lt,t) -> term env t
+ | TCast (false, Ctype ty_tgt,t) -> cast (cast_ltyp ty_tgt t.term_type) (term env t)
+ | TCast (true, _lt,t) -> term env t
+ | TCast (false, _, _) -> assert false
(* Term L-Values *)
diff --git a/src/plugins/wp/RegionAccess.ml b/src/plugins/wp/RegionAccess.ml
index f96af2972fd..4d1da962951 100644
--- a/src/plugins/wp/RegionAccess.ml
+++ b/src/plugins/wp/RegionAccess.ml
@@ -270,9 +270,9 @@ and cc_term_value (map:map) (term:term) =
| Tat(t,_) -> cc_term_value map t
- | TCastE(ty,t) -> cast ty @@ cc_term_value map t
- | TLogic_coerce (Ctype ty,t) -> cast ty @@ cc_term_value map t
- | TLogic_coerce (_,t) -> cc_term_value map t
+ | TCast (_, Ctype ty,t) -> cast ty @@ cc_term_value map t
+ | TCast (true, _,t) -> cc_term_value map t
+ | TCast (false, _,_) -> assert false
| TConst _
| TSizeOf _ | TSizeOfE _ | TSizeOfStr _
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index c025c2b8279..2cce251f7c3 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -622,7 +622,7 @@ let rec term_hints hs t =
match t.term_node with
| TLval(lv,_) -> lval_hints hs lv
| TAddrOf(lv,_) -> lval_hints hs lv
- | TCastE(_,t) -> term_hints hs t
+ | TCast (false, Ctype _,t) -> term_hints hs t
| TBinOp((PlusPI|MinusPI),a,_) -> term_hints hs a
| Tlet(_,t) -> term_hints hs t
| _ -> ()
diff --git a/tests/libc/check_const.ml b/tests/libc/check_const.ml
index 6996d5ed032..8a38a17b5c1 100644
--- a/tests/libc/check_const.ml
+++ b/tests/libc/check_const.ml
@@ -48,7 +48,7 @@ let check_annot kf _ (a: identified_predicate) =
end
| TBinOp ((PlusPI | MinusPI),
({term_node = TLval (TVar lvi, _)} |
- {term_node = TCastE (_, {term_node = TLval (TVar lvi, _)})}),
+ {term_node = TCast (false,_, {term_node = TLval (TVar lvi, _)})}),
_)
| TLval (TVar lvi, _) -> begin
match lvi.lv_origin with
--
GitLab