From cbccc689b82d2bdc52240203db152f94b7cf2b2e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 28 Mar 2024 14:33:19 +0100
Subject: [PATCH] [Eva] Reduction by \valid and \valid_read always remove
indeterminate values.
---
src/plugins/eva/legacy/eval_op.ml | 26 ++++++++++++-------
tests/value/oracle/reduce_by_valid.res.oracle | 2 +-
tests/value/oracle/summary.4.res.oracle | 6 +----
3 files changed, 18 insertions(+), 16 deletions(-)
diff --git a/src/plugins/eva/legacy/eval_op.ml b/src/plugins/eva/legacy/eval_op.ml
index aa9227c4555..2aff52c9bf2 100644
--- a/src/plugins/eva/legacy/eval_op.ml
+++ b/src/plugins/eva/legacy/eval_op.ml
@@ -128,22 +128,28 @@ let reduce_by_initialized_defined f loc state =
state
let reduce_by_valid_loc ~positive access loc typ state =
- let value = Cvalue.Model.find state loc in
- let loc_bits = Locations.loc_bytes_to_loc_bits value in
+ let value = Cvalue.Model.find_indeterminate state loc in
+ let loc_bytes = Cvalue.V_Or_Uninitialized.get_v value in
+ let loc_bits = Locations.loc_bytes_to_loc_bits loc_bytes in
let size = Bit_utils.sizeof_pointed typ in
- let value_as_loc = Locations.make_loc loc_bits size in
+ let location = Locations.make_loc loc_bits size in
+ let reduced_location =
+ if positive
+ then Locations.valid_part access location
+ else Locations.invalid_part location
+ in
+ let reduced_loc_bytes = Locations.loc_to_loc_without_size reduced_location in
let reduced_value =
- Locations.loc_to_loc_without_size
- (if positive
- then Locations.valid_part access value_as_loc
- else Locations.invalid_part value_as_loc )
+ if positive
+ then Cvalue.V_Or_Uninitialized.initialized reduced_loc_bytes
+ else Cvalue.V_Or_Uninitialized.map (fun _ -> reduced_loc_bytes) value
in
- if V.equal value reduced_value
+ if Cvalue.V_Or_Uninitialized.equal value reduced_value
then state
else
- if V.equal V.bottom reduced_value
+ if Cvalue.V_Or_Uninitialized.(equal bottom reduced_value)
then Cvalue.Model.bottom
- else Cvalue.Model.reduce_previous_binding state loc reduced_value
+ else Cvalue.Model.reduce_indeterminate_binding state loc reduced_value
let make_loc_contiguous loc =
try
diff --git a/tests/value/oracle/reduce_by_valid.res.oracle b/tests/value/oracle/reduce_by_valid.res.oracle
index 1779ee8c716..a4bafca7fce 100644
--- a/tests/value/oracle/reduce_by_valid.res.oracle
+++ b/tests/value/oracle/reduce_by_valid.res.oracle
@@ -230,7 +230,7 @@
[eva:final-states] Values at end of function main5:
q ∈ {{ &y }}
p ∈ {0}
- r ∈ {{ &y }} or UNINITIALIZED
+ r ∈ {{ &y }}
[eva:final-states] Values at end of function main6:
S_f1_0_S_vs[0] ∈ {1}
[1] ∈ [--..--]
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 78f84b5adc2..022406b2a82 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -61,9 +61,6 @@
locals {z} escaping the scope of a block of alarms through p
[eva:alarm] summary.i:45: Warning:
assertion 'rte,mem_access' got status unknown.
-[eva:alarm] summary.i:45: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&p);
[eva] Recording results for alarms
[eva] Done for function alarms
[eva] computing for function logic <- main.
@@ -111,7 +108,7 @@
by the Eva analyzer: 0 errors 1 warning
by the Frama-C kernel: 0 errors 3 warnings
----------------------------------------------------------------------------
- 18 alarms generated by the analysis:
+ 17 alarms generated by the analysis:
3 invalid memory accesses
3 integer overflows
2 accesses out of bounds index
@@ -119,7 +116,6 @@
2 nan or infinite floating-point values
2 illegal conversions from floating-point to integer
1 division by zero
- 1 escaping address
2 others
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
--
GitLab