From ed964a09387b3321a9a385f5f5432188def339de Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Wed, 16 Oct 2024 14:37:00 +0200
Subject: [PATCH] [kernel] Unify is_intptr_t between RTE and Eva and define it
in Cil
---
src/kernel_services/ast_queries/cil.ml | 12 ++++++++++++
src/kernel_services/ast_queries/cil.mli | 10 ++++++++++
src/plugins/eva/engine/evaluation.ml | 11 +++++------
src/plugins/rte/rte.ml | 7 ++-----
4 files changed, 29 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 045236f5085..742b5c26528 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3304,6 +3304,18 @@ let isIntegralOrPointerType t =
| TInt _ | TEnum _ | TPtr _ -> true
| _ -> false
+(* Don't completely unroll here, as we do not want to identify
+ intptr_t with its supporting integer type. *)
+let rec is_intptr_t = function
+ | TNamed(t,_) ->
+ t.tname = "intptr_t" || is_intptr_t t.ttype
+ | _ -> false
+
+let rec is_uintptr_t = function
+ | TNamed (t,_) ->
+ t.tname = "uintptr_t" || is_uintptr_t t.ttype
+ | _ -> false
+
let rec isLogicBooleanType t =
match t with
| Ctype ty -> isIntegralType ty
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index dd36accd6a0..5f654d34907 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -416,6 +416,16 @@ val isIntegralType: typ -> bool
*)
val isBoolType: typ -> bool
+(** True if the argument is [intptr_t] (but _not_ its underlying integer type)
+ @since Frama-C+dev
+*)
+val is_intptr_t: typ -> bool
+
+(** True if the argument is [uintptr_t] (but _not_ its underlying integer type)
+ @since Frama-C+dev
+*)
+val is_uintptr_t: typ -> bool
+
(** True if the argument is [_Bool] or [boolean].
@since 19.0-Potassium
*)
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index e64f4ee5f0b..06c1daa44ce 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -169,11 +169,6 @@ let rec signed_counterpart typ =
| TPtr _ -> signed_counterpart ((Machine.uintptr_type ()))
| _ -> assert false
-let rec is_intptr_type = function
- | TNamed ({torig_name = name} as t, _) ->
- name = "intptr_t" || name = "uintptr_t" || is_intptr_type t.ttype
- | _ -> false
-
let return t = `Value t, Alarmset.none
(* Intersects [alarms] with the only possible alarms from the dereference of
@@ -797,7 +792,11 @@ module Make
let& value =
match src_type, dst_type with
| TSPtr src, TSInt dst ->
- let alarm = if is_intptr_type dst_typ then NoAlarm else PtrDowncast in
+ let alarm =
+ if Cil.is_intptr_t dst_typ || Cil.is_uintptr_t dst_typ
+ then NoAlarm
+ else PtrDowncast
+ in
cast_int_to_int context ~alarm ~src ~dst expr value
| TSInt src, (TSInt dst | TSPtr dst) ->
cast_int_to_int context ~alarm:IntDowncast ~src ~dst expr value
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index b4d94c63bb7..b5be2f5975c 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -330,10 +330,6 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
end
else overflow_alarm ()
-let rec is_intptr_t = function
- | Cil_types.TNamed(t,_) -> t.tname = "intptr_t" || is_intptr_t t.ttype
- | _ -> false
-
(* Assertion for downcasts. *)
let downcast_assertion ~remove_trivial ~on_alarm (dst_type, exp) =
let src_type = Cil.typeOf exp in
@@ -342,7 +338,8 @@ let downcast_assertion ~remove_trivial ~on_alarm (dst_type, exp) =
let src_size = Cil.bitsSizeOf src_type in
let dst_size = Cil.bitsSizeOfBitfield dst_type in
if (dst_size < src_size || dst_size == src_size && dst_signed <> src_signed)
- && not (Cil.isPointerType src_type && is_intptr_t dst_type)
+ && not (Cil.isPointerType src_type &&
+ (Cil.is_intptr_t dst_type || Cil.is_uintptr_t dst_type))
then
let dst_min, dst_max =
if dst_signed
--
GitLab