From 8bb63bdbb3652b54325cf90a4547502d381497c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Sat, 30 Mar 2024 10:31:01 +0100
Subject: [PATCH] [Eva] Rewraps absolute addresses of pointer values, seeen as
unsigned integers.
---
src/plugins/eva/engine/evaluation.ml | 18 ++++++++++++------
src/plugins/eva/utils/eval_typ.ml | 11 +++++------
src/plugins/eva/utils/eval_typ.mli | 3 +++
src/plugins/eva/values/abstract_value.ml | 3 ++-
.../value/oracle/absolute_pointer.1.res.oracle | 9 ++-------
.../oracle_multidim/strings_logic.res.oracle | 8 --------
6 files changed, 24 insertions(+), 28 deletions(-)
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index 7a58005d92b..84e733c6df4 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -451,12 +451,18 @@ module Make
| _ -> assert false
let assume_pointer expr value =
- if Kernel.InvalidPointer.get ()
- then
- let truth = Value.assume_pointer value in
- let alarm () = Alarms.Invalid_pointer expr in
- interpret_truth ~alarm value truth
- else return value
+ let value, alarms =
+ if Kernel.InvalidPointer.get ()
+ then
+ let truth = Value.assume_pointer value in
+ let alarm () = Alarms.Invalid_pointer expr in
+ interpret_truth ~alarm value truth
+ else return value
+ in
+ (* Rewrap absolute addresses of pointer values, seen as unsigned
+ integers, to ensure a consistent representation of pointers. *)
+ let range = Eval_typ.pointer_range () in
+ value >>-: Value.rewrap_integer range, alarms
let handle_overflow ~may_overflow expr typ value =
match Eval_typ.classify_as_scalar typ with
diff --git a/src/plugins/eva/utils/eval_typ.ml b/src/plugins/eva/utils/eval_typ.ml
index 129d1db7b56..96f0c767a46 100644
--- a/src/plugins/eva/utils/eval_typ.ml
+++ b/src/plugins/eva/utils/eval_typ.ml
@@ -211,16 +211,15 @@ type scalar_typ =
| TSPtr of integer_range
| TSFloat of fkind
+let pointer_range () =
+ { i_bits = Cil.bitsSizeOfInt Cil.theMachine.Cil.upointKind;
+ i_signed = Cil.isSigned Cil.theMachine.Cil.upointKind }
+
let classify_as_scalar typ =
match Cil.unrollType typ with
| TInt (ik, attrs) | TEnum ({ekind=ik}, attrs) ->
Some (TSInt (ik_attrs_range ik attrs))
- | TPtr _ ->
- let range =
- { i_bits = Cil.bitsSizeOfInt Cil.theMachine.Cil.upointKind;
- i_signed = Cil.isSigned Cil.theMachine.Cil.upointKind }
- in
- Some (TSPtr range)
+ | TPtr _ -> Some (TSPtr (pointer_range ()))
| TFloat (fk, _) -> Some (TSFloat fk)
| _ -> None
diff --git a/src/plugins/eva/utils/eval_typ.mli b/src/plugins/eva/utils/eval_typ.mli
index f6ce26872bc..18e94b718af 100644
--- a/src/plugins/eva/utils/eval_typ.mli
+++ b/src/plugins/eva/utils/eval_typ.mli
@@ -75,6 +75,9 @@ val ik_attrs_range: ikind -> attributes -> integer_range
(** Range for an integer type with some attributes. The attribute
{!Cil.bitfield_attribute_name} influences the width of the type. *)
+val pointer_range: unit -> integer_range
+(** Range for a pointer type. *)
+
val range_inclusion: integer_range -> integer_range -> bool
(** Checks inclusion of two integer ranges. *)
diff --git a/src/plugins/eva/values/abstract_value.ml b/src/plugins/eva/values/abstract_value.ml
index e63cc2c575d..353773dc05f 100644
--- a/src/plugins/eva/values/abstract_value.ml
+++ b/src/plugins/eva/values/abstract_value.ml
@@ -133,7 +133,8 @@ module type S = sig
val forward_binop : typ -> binop -> t -> t -> t or_bottom
(** [rewrap_integer irange t] wraps around the abstract value [t] to fit the
- integer range [irange], assuming 2's complement. *)
+ integer range [irange], assuming 2's complement. Also used on absolute
+ addresses for pointer values, seen as unsigned integers. *)
val rewrap_integer: Eval_typ.integer_range -> t -> t
(** Abstract evaluation of casts operators from [src_type] to [dst_type]. *)
diff --git a/tests/value/oracle/absolute_pointer.1.res.oracle b/tests/value/oracle/absolute_pointer.1.res.oracle
index 1a7896cbbe0..0aca61ab004 100644
--- a/tests/value/oracle/absolute_pointer.1.res.oracle
+++ b/tests/value/oracle/absolute_pointer.1.res.oracle
@@ -6,21 +6,16 @@
NULL[rbits 0 to 147573952589676412935] ∈ [--..--]
R ∈ {0}
nondet ∈ [--..--]
-[eva:alarm] absolute_pointer.c:43: Warning:
- out of bounds write. assert \valid(p - 100);
-[kernel] absolute_pointer.c:43: Warning:
- all target addresses were invalid. This path is assumed to be dead.
+[eva] absolute_pointer.c:44: Frama_C_show_each: {4294967196}
[eva] absolute_pointer.c:47: Frama_C_show_each: {4294967196}
[eva] absolute_pointer.c:52: Frama_C_show_each: {4294967197}
[eva] absolute_pointer.c:56: Frama_C_show_each: {4294967197}
[eva] Recording results for negative_absolute_address
[eva] Done for function negative_absolute_address
-[eva] absolute_pointer.c:43:
- assertion 'Eva,mem_access' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function negative_absolute_address:
NULL[rbits 0 to 34359737567] ∈ [--..--]
- [rbits 34359737568 to 34359737575] ∈ {1}
+ [rbits 34359737568 to 34359737575] ∈ {1; 25}
[rbits 34359737576 to 34359737583] ∈ {2; 42}
[rbits 34359737584 to 147573952589676412935] ∈ [--..--]
uptr ∈ {0}
diff --git a/tests/value/oracle_multidim/strings_logic.res.oracle b/tests/value/oracle_multidim/strings_logic.res.oracle
index ed8b014f3c9..e69de29bb2d 100644
--- a/tests/value/oracle_multidim/strings_logic.res.oracle
+++ b/tests/value/oracle_multidim/strings_logic.res.oracle
@@ -1,8 +0,0 @@
-83c83
-< {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
----
-> {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
-92c92
-< {{ NULL + [0..4294967295] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
----
-> {{ NULL + [0..147] ; &s1 + [-123..147] ; &s2 + [-123..147] ;
--
GitLab