diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index c003f9f35bf77362155c81dbd52b77242f5abf7d..788b50d806d9634321b1df5cf8e6b7daa6f847d0 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -29,6 +29,12 @@ open Eval
for a minimal drop in efficiency. *)
let infer_intervals = true
+(* Whether the domain saturates the octagons: from a relation between (x, y)
+ and a relation between (y, z), infers the relation between (x, z).
+ The saturation is currently partial. Improves the domain accuracy for a
+ minimal drop in efficiency. *)
+let saturate_octagons = true
+
(* -------------------------------------------------------------------------- *)
(* Basic types: pair of variables and Ival.t *)
(* -------------------------------------------------------------------------- *)
@@ -395,8 +401,10 @@ module Diamond = struct
Arith.narrow x.add y.add >>- fun add ->
Arith.narrow x.sub y.sub >>-: fun sub -> {add; sub}
- (* Makes a diamond about (X, Y) from a diamond about (Y, X). *)
- let reverse_variables t = { t with sub = Arith.neg t.sub }
+ (* If [swap] is true, makes a diamond about (X, Y) from a diamond
+ about (Y, X). *)
+ let reverse_variables swap t =
+ if swap then { t with sub = Arith.neg t.sub } else t
end
@@ -643,7 +651,7 @@ module State = struct
type t = state
include Datatype.Serializable_undefined
- let name = "Octagons.Octagons"
+ let name = "Octagons.State"
let structural_descr =
Structural_descr.t_record
[| Octagons.packed_descr;
@@ -676,6 +684,8 @@ module State = struct
Octagons.pretty octagons Intervals.pretty intervals
end)
+ (* ------------------------------ Lattice --------------------------------- *)
+
let top =
{ octagons = Octagons.top;
intervals = Intervals.top;
@@ -762,7 +772,67 @@ module State = struct
let modified = Zone.narrow t1.modified t2.modified in
`Value { octagons; intervals; relations; modified; }
- let add_octagon state octagon =
+ (* -------------- Transitive closure when adding an octagon --------------- *)
+
+ type relation =
+ { vars: varinfo * varinfo;
+ diamond: diamond; }
+
+ let add_relation state rel =
+ let x, z = rel.vars in
+ let pair, swap = Pair.make x z in
+ let diamond = Diamond.reverse_variables swap rel.diamond in
+ Octagons.add pair diamond state.octagons >>-: fun octagons ->
+ let relations = Relations.relate pair state.relations in
+ { state with octagons; relations }
+
+ let inverse { vars; diamond } =
+ let var1, var2 = vars in
+ { vars = var2, var1; diamond = Diamond.reverse_variables true diamond }
+
+ let transitive_relation y rel1 rel2 =
+ let rel1 =
+ if Variable.equal y (snd rel1.vars) then rel1 else inverse rel1
+ and rel2 =
+ if Variable.equal y (fst rel2.vars) then rel2 else inverse rel2
+ in
+ (* rel1 is about X±Y, rel2 is about Y±Z. *)
+ let typ = y.vtype in
+ (* X+Z = (X+Y) - (Y-Z) and X+Y = (X-Y) + (Y+Z) *)
+ let add =
+ Ival.narrow
+ (Arith.sub typ rel1.diamond.add rel2.diamond.sub)
+ (Arith.add typ rel1.diamond.sub rel2.diamond.add)
+ (* X-Z = (X+Y) - (Y+Z) and X-Z = (X-Y) + (Y-Z) *)
+ and sub =
+ Ival.narrow
+ (Arith.sub typ rel1.diamond.add rel2.diamond.add)
+ (Arith.add typ rel1.diamond.sub rel2.diamond.sub)
+ in
+ let diamond = {add; sub} in
+ if Diamond.is_top diamond then raise Not_found else
+ let vars = fst rel1.vars, snd rel2.vars in
+ { vars; diamond }
+
+ let saturate state x y rel1 =
+ try
+ let y_related = Relations.find y state.relations in
+ let y_related = VariableSet.remove x y_related in
+ let aux z state =
+ state >>- fun state ->
+ try
+ let pair, _ = Pair.make y z in
+ let diamond = Octagons.find pair state.octagons in
+ let vars = Pair.get pair in
+ let rel2 = { vars; diamond } in
+ let new_relation = transitive_relation y rel1 rel2 in
+ add_relation state new_relation
+ with Not_found -> `Value state
+ in
+ VariableSet.fold aux y_related (`Value state)
+ with Not_found -> `Value state
+
+ let add_octagon_aux state octagon =
if Ival.(equal top octagon.value)
then `Value state
else
@@ -770,6 +840,22 @@ module State = struct
let relations = Relations.relate octagon.variables state.relations in
{ state with octagons; relations }
+ let add_octagon state octagon =
+ let state =
+ if saturate_octagons
+ then
+ let x, y = Pair.get octagon.variables in
+ let diamond = match octagon.operation with
+ | Add -> { add = octagon.value; sub = Ival.top }
+ | Sub -> { add = Ival.top; sub = octagon.value }
+ in
+ let relation = { vars = x, y; diamond } in
+ saturate state y x relation >>- fun state ->
+ saturate state x y relation
+ else `Value state
+ in
+ state >>- fun state -> add_octagon_aux state octagon
+
let remove state x =
let intervals = Intervals.remove x state.intervals in
let state = { state with intervals } in
@@ -797,11 +883,7 @@ module State = struct
let pair, swap = Pair.make x y in
try
let diamond = Octagons.find pair state.octagons in
- let diamond =
- if swap
- then Diamond.reverse_variables diamond
- else diamond
- in
+ let diamond = Diamond.reverse_variables swap diamond in
(y, diamond) :: acc
with Not_found -> acc
in
@@ -814,19 +896,19 @@ module State = struct
let state = { state with intervals } in
let x_related = Relations.find x state.relations in
let aux y state =
- let pair, order = Pair.make x y in
+ let pair, swap = Pair.make x y in
try
let diamond = Octagons.find pair state.octagons in
let diamond =
if inverse
then
- let op = if order then Arith.neg else fun x -> x in
+ let op = if swap then fun x -> x else Arith.neg in
{ add = op diamond.sub;
sub = op diamond.add }
else diamond
in
let typ = x.vtype in
- let op = if order then Arith.sub else Arith.add in
+ let op = if swap then Arith.add else Arith.sub in
let add =
if Ival.(equal top diamond.add)
then diamond.add