From 745a228a0676e74349ece274483f64c9a9daaf2c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Sat, 30 Mar 2024 17:08:19 +0100
Subject: [PATCH] [Eva] Avoids changing the origin of an existing garbled mix.
This has no impact as the join of origins now chooses the oldest known origin,
but it could be better if we ever change the implementation of the origin join.
---
src/kernel_services/abstract_interp/cvalue.ml | 18 ++++--------------
.../abstract_interp/locations.ml | 6 ++----
.../abstract_interp/offsetmap.ml | 2 +-
src/kernel_services/abstract_interp/origin.ml | 2 +-
.../eva/domains/cvalue/cvalue_domain.ml | 2 +-
src/plugins/eva/values/cvalue_forward.ml | 4 ++--
tests/builtins/oracle/memcpy.res.oracle | 2 +-
7 files changed, 12 insertions(+), 24 deletions(-)
diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index f401f1594ad..a37f6ce682a 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -504,11 +504,7 @@ module V = struct
with Not_based_on_null ->
if is_bottom e1 || is_bottom e2
then bottom
- else begin
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
- end
+ else topify_with_origin_kind topify (join e1 e2)
let arithmetic_function = import_function ~topify:Origin.Arith
@@ -540,9 +536,7 @@ module V = struct
try (* On the off chance that someone writes [i+(int)&p]... *)
Location_Bytes.shift (project_ival_bottom e1) e2
with Not_based_on_null ->
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ topify_with_origin_kind topify (join e1 e2)
end
with Not_found ->
(* we end up here if the only way left to make this
@@ -551,9 +545,7 @@ module V = struct
let right = Ival.scale_int_base factor (project_ival_bottom e2)
in Location_Bytes.shift right e1
with Not_based_on_null -> (* from [project_ival] *)
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ topify_with_origin_kind topify (join e1 e2)
(* Under-approximating variant of add_untyped. Takes two
under-approximation, and returns an under-approximation.*)
@@ -669,9 +661,7 @@ module V = struct
then
bottom
else
- join
- (topify_with_origin_kind topify acc)
- (topify_with_origin_kind topify value)
+ topify_with_origin_kind topify (join acc value)
end
else
add_untyped ~topify ~factor:Int_Base.one value acc
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index 768e9c12c42..b9e05407260 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -213,11 +213,9 @@ module Location_Bytes = struct
let topify_with_origin o v =
match v with
- | Top (s,a) ->
- Top (s, Origin.join a o)
- | v when is_zero v -> v
+ | Top _ -> v
| Map _ ->
- if equal v bottom then v
+ if is_zero v || equal v bottom then v
else
match get_keys v with
| Base.SetLattice.Top -> top_with_origin o
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 08fa4d98a93..3359a012d02 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1721,7 +1721,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let clip = clip_by_validity validity in
let r = fold
(fun (min, max as itv) (bound_v, _, _) acc ->
- let new_v = V.join (V.topify_with_origin o bound_v) v in
+ let new_v = V.topify_with_origin o (V.join bound_v v) in
let new_min, new_max = clip itv in
if new_min <=~ new_max then (* [min..max] and validity intersect *)
let acc =
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 99acf93c89c..fd87a5148a4 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -171,7 +171,7 @@ let clear () = History.clear ()
(* Keep the oldest known origin: it is probably the most relevant origin, as
subsequent ones may have been created because of the first. *)
let join t1 t2 =
- if t1 == t2 then t1 else
+ if equal t1 t2 then t1 else
match t1, t2 with
| Unknown, x | x, Unknown -> x
| Well, _ | _, Well -> Well
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 43b19bd4258..094e3c9124c 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -212,7 +212,7 @@ module State = struct
| Some location ->
let location = Precise_locs.imprecise_location location in
let v = Cvalue.Model.find ~conflate_bottom:false state location in
- Cvalue.V.join acc (Cvalue.V.topify_leaf_origin v)
+ Cvalue.V.topify_leaf_origin (Cvalue.V.join acc v)
else acc
in
List.fold_left one_from_contents Cvalue.V.top_int deps
diff --git a/src/plugins/eva/values/cvalue_forward.ml b/src/plugins/eva/values/cvalue_forward.ml
index 3f8b7a6bf34..b3482f725d2 100644
--- a/src/plugins/eva/values/cvalue_forward.ml
+++ b/src/plugins/eva/values/cvalue_forward.ml
@@ -364,7 +364,7 @@ let forward_minus_pp ~typ ev1 ev2 =
try
V.inject_ival (conv (Cvalue.V.project_ival minus_val))
with Cvalue.V.Not_based_on_null ->
- V.join (V.topify_arith_origin ev1) (V.topify_arith_origin ev2)
+ V.topify_arith_origin (V.join ev1 ev2)
else
(* Pointwise arithmetics.*)
let v = V.sub_pointer ev1 ev2 in
@@ -410,7 +410,7 @@ let forward_binop_int ~typ ev1 op ev2 =
let forward_binop_float fkind ev1 op ev2 =
match V.project_float ev1, V.project_float ev2 with
| exception V.Not_based_on_null ->
- V.join (V.topify_arith_origin ev1) (V.topify_arith_origin ev2)
+ V.topify_arith_origin (V.join ev1 ev2)
| f1, f2 ->
let binary_float_floats (_name: string) f =
V.inject_float (f fkind f1 f2)
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 6fe4eedb724..1559794a477 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -580,7 +580,7 @@
v4.x ∈ [--..--]
.y ∈ {{ (int)&t }}
{.p; .padding[0..23]} ∈ [--..--]
- v5 ∈ {{ garbled mix of &{t} (origin: Arithmetic {memcpy.c:91}) }}
+ v5 ∈ {{ garbled mix of &{t} (origin: Misaligned read {memcpy.c:91}) }}
t{[0]; [1]{.x; .y}} ∈ {0}
[1].p ∈ {{ &v1.y }}
{[1].padding[0..23]; [2]; [3]{.x; .y}} ∈ {0}
--
GitLab