From 1d3327de398e44eab0fc7e6bee535a66dbe944d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 28 Apr 2023 11:05:37 +0200
Subject: [PATCH] [Eva] Octagons: uses Hptset for sets of variables.
---
src/plugins/eva/domains/octagons.ml | 48 +++++++++++--------
.../value/oracle/octagons-pointers.res.oracle | 10 ++--
2 files changed, 32 insertions(+), 26 deletions(-)
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index 0b2938d68ce..978434c0097 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -160,6 +160,12 @@ module Variable : Variable = struct
Eva_utils.deps_of_lval eval_loc (Option.get (HCE.to_lval lval))
end
+module VarSet =
+ Hptset.Make
+ (Variable)
+ (struct let v = [ [ ] ] end)
+ (struct let l = [ Ast.self ] end)
+
(* Pairs of related variables in an octagon.
This module imposes an order between the two variables X and Y in a pair
to avoid creating octagons about X±Y *and* about Y±X. *)
@@ -742,29 +748,29 @@ module Relations = struct
module Dependencies = struct let l = [ Ast.self ] end
include Hptmap.Make (Variable)
- (struct include Variable.Set let pretty_debug = pretty end)
+ (struct include VarSet let pretty_debug = pretty end)
(Hptmap.Comp_unused) (Initial_Values) (Dependencies)
let inter =
let cache = Hptmap_sig.PersistentCache "Octagons.Relations.inter" in
let decide _pair x y =
- let r = Variable.Set.inter x y in
- if Variable.Set.is_empty r then None else Some r
+ let r = VarSet.inter x y in
+ if VarSet.is_empty r then None else Some r
in
inter ~cache ~symmetric:true ~idempotent:true ~decide
let union =
let cache = Hptmap_sig.PersistentCache "Octagons.Relations.union" in
- let decide _pair x y = Variable.Set.union x y in
+ let decide _pair x y = VarSet.union x y in
join ~cache ~symmetric:true ~idempotent:true ~decide
(* Marks y as related to x. *)
let relate_aux x y t =
let related =
try find x t
- with Not_found -> Variable.Set.empty
+ with Not_found -> VarSet.empty
in
- let updated = Variable.Set.add y related in
+ let updated = VarSet.add y related in
add x updated t
(* Marks x and y as mutually related. *)
@@ -773,7 +779,7 @@ module Relations = struct
relate_aux y x (relate_aux x y t)
let add variable set t =
- if Variable.Set.is_empty set
+ if VarSet.is_empty set
then remove variable t
else add variable set t
end
@@ -898,7 +904,7 @@ struct
end
module BaseToVariables = struct
- module VSet = Variable.Set
+ module VSet = VarSet
(* [BaseToVariables] represents a map from bases to each symbolic variable
used in the domain state that depends on this base.
@@ -985,7 +991,7 @@ module BaseToVariables = struct
end
module Deps = struct
- module VSet = Variable.Set
+ module VSet = VarSet
include Datatype.Pair (VariableToDeps) (BaseToVariables)
@@ -1196,8 +1202,8 @@ module State = struct
variables can be related in [t.relations] without an actual octagon
between them. *)
let check_relation x y =
- try Variable.Set.mem x (Relations.find y t.relations)
- && Variable.Set.mem y (Relations.find x t.relations)
+ try VarSet.mem x (Relations.find y t.relations)
+ && VarSet.mem y (Relations.find x t.relations)
with Not_found -> false
in
let check_relation x y =
@@ -1444,7 +1450,7 @@ module State = struct
let saturate state x y rel1 =
try
let y_related = Relations.find y state.relations in
- let y_related = Variable.Set.remove x y_related in
+ let y_related = VarSet.remove x y_related in
let aux z state =
state >>- fun state ->
try
@@ -1456,7 +1462,7 @@ module State = struct
add_diamond state pair diamond
with Not_found -> `Value state
in
- Variable.Set.fold aux y_related (`Value state)
+ VarSet.fold aux y_related (`Value state)
with Not_found -> `Value state
(* Adds dependencies to the state only if [eval_deps] is not None. *)
@@ -1505,14 +1511,14 @@ module State = struct
let remove_one y state =
try
let yrelations = Relations.find y state.relations in
- let yrelations = Variable.Set.remove x yrelations in
+ let yrelations = VarSet.remove x yrelations in
let relations = Relations.add y yrelations state.relations in
let pair, _ = Pair.make x y in
let octagons = Octagons.remove pair state.octagons in
{ state with octagons; relations }
with Not_found -> state
in
- let state = Variable.Set.fold remove_one relations state in
+ let state = VarSet.fold remove_one relations state in
let relations = Relations.remove x state.relations in
let deps = Deps.remove x state.deps in
{ state with relations; deps }
@@ -1529,7 +1535,7 @@ module State = struct
(y, diamond) :: acc
with Not_found -> acc
in
- Variable.Set.fold aux related []
+ VarSet.fold aux related []
with Not_found -> []
(* x' = ±x - delta *)
@@ -1565,7 +1571,7 @@ module State = struct
{ state with octagons }
with Not_found -> state
in
- Variable.Set.fold aux x_related state
+ VarSet.fold aux x_related state
end
@@ -1842,9 +1848,9 @@ module Domain = struct
let add_related_bases acc var =
try
let related = Relations.find var state.relations in
- Variable.Set.to_seq related |>
- Seq.map (Deps.get_var_bases state.deps) |>
- Seq.fold_left Base.SetLattice.join acc
+ VarSet.elements related |>
+ List.map (Deps.get_var_bases state.deps) |>
+ List.fold_left Base.SetLattice.join acc
with Not_found -> acc
in
let aux base acc =
@@ -1858,7 +1864,7 @@ module Domain = struct
then state
else
let removed_vars, deps = Deps.filter bases state.deps in
- let mem_var v = not (Variable.Set.mem v removed_vars) in
+ let mem_var v = not (VarSet.mem v removed_vars) in
let mem_pair pair =
let x, y = Pair.get pair in
mem_var x && mem_var y
diff --git a/tests/value/oracle/octagons-pointers.res.oracle b/tests/value/oracle/octagons-pointers.res.oracle
index 301a6c28d20..d3863b4a43e 100644
--- a/tests/value/oracle/octagons-pointers.res.oracle
+++ b/tests/value/oracle/octagons-pointers.res.oracle
@@ -46,30 +46,30 @@
cmd - cmd ∈ [-430..427]
cmd->cmdLen + index ∈ [--..434]
cmd - len ∈ {0}
- len - cmd ∈ [-430..427]
buffer - len ∈ [-433..-6]
+ len - cmd ∈ [-430..427]
len - code ∈ {-2}
+ buffer - code ∈ [-435..-8]
cmd - code ∈ {-2}
code - cmd ∈ [-428..429]
- buffer - code ∈ [-435..-8]
code - elt1 ∈ {-1}
+ buffer - elt1 ∈ [-436..-9]
cmd - elt1 ∈ {-3}
len - elt1 ∈ {-3}
elt1 - cmd ∈ [-427..430]
- buffer - elt1 ∈ [-436..-9]
elt1 - elt2 ∈ {-4}
+ buffer - elt2 ∈ [-440..-13]
cmd - elt2 ∈ {-7}
len - elt2 ∈ {-7}
code - elt2 ∈ {-5}
elt2 - cmd ∈ [-423..434]
- buffer - elt2 ∈ [-440..-13]
elt2 - elt3 ∈ {-2}
+ buffer - elt3 ∈ [-442..-15]
cmd - elt3 ∈ {-9}
len - elt3 ∈ {-9}
code - elt3 ∈ {-7}
elt1 - elt3 ∈ {-6}
elt3 - cmd ∈ [-421..436]
- buffer - elt3 ∈ [-442..-15]
]}
==END OF DUMP==
[eva:alarm] octagons-pointers.c:33: Warning:
--
GitLab