From 81a4ade0a3b43cbe1aa428cc7c944c5b45334ec8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 26 Feb 2024 16:27:50 +0100
Subject: [PATCH] [Eva] Removes the inclusion of garbled mix origins.
Origins should never impact the convergence of the analysis.
---
src/kernel_services/abstract_interp/map_lattice.ml | 3 +--
src/kernel_services/abstract_interp/origin.ml | 2 --
src/kernel_services/abstract_interp/origin.mli | 1 -
3 files changed, 1 insertion(+), 5 deletions(-)
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 204ad8aa11e..46c8138c810 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -392,8 +392,7 @@ module Make_MapSet_Lattice
let is_included t1 t2 =
match t1, t2 with
- | Top (s1, o1), Top (s2, o2) ->
- KSet.is_included s1 s2 && Origin.is_included o1 o2
+ | Top (s1, _), Top (s2, _) -> KSet.is_included s1 s2
| Map _, Top (KSet.Top, _) -> true
| Map m, Top (KSet.Set s, _) -> KVMap.for_all (fun k _ -> KSet.O.mem k s) m
| Top _, Map _ -> false
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 422fc364d37..357ebfd681a 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -119,8 +119,6 @@ let join t1 t2 =
| Well, _ | _, Well -> Well
| Origin o1, Origin o2 -> if o1.id <= o2.id then t1 else t2
-let is_included = equal
-
(* For each garbled mix origin, keep track of:
- the number of writes (according to [register_write] below), i.e. the number
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index a5d1ce6566c..bb8cdc57192 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -53,7 +53,6 @@ val pretty_as_reason: Format.formatter -> t -> unit
val descr: t -> string
val join: t -> t -> t
-val is_included: t -> t -> bool
(** Records the write of an imprecise value of the given bases,
with the given origin.
--
GitLab