Skip to content

Switch to widen which doesn't require leq on arguments #2081

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
sim642 wants to merge 16 commits into
base: master
Choose a base branch
from
Open

Switch to widen which doesn't require leq on arguments #2081

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
38f8476
Start converting widen to not require leq on arguments
sim642 Jul 24, 2026
113460e
Remove join from second argument of widen in solvers
sim642 Jul 24, 2026
40d1177
Remove join wrappers from widens used by Spec lifter domains
sim642 Jul 24, 2026
2eb844a
Remove join wrappers from interval domain widen
sim642 Jul 24, 2026
976c501
Remove join wrappers from more value domains
sim642 Jul 24, 2026
e92b7a3
Partially remove join wrappers from more domains
sim642 Aug 17, 2026
c4ea741
Remove join wrappers from DisjointDomain
sim642 Aug 18, 2026
1d01233
Remove join from second argument of widen in TD3
sim642 Aug 18, 2026
fca9686
Convert widen_with_fct to not require leq on arguments
sim642 Aug 18, 2026
aa34c89
Remove outdated widen comment in ArgConstraints
sim642 Aug 18, 2026
24eba8b
Update comments about int domain refinement on join
sim642 Aug 18, 2026
78acf49
Remove join from conservative widen check in TD3 update rule
sim642 Aug 18, 2026
b12972e
Fix widen documentation
sim642 Aug 18, 2026
70942f4
Remove now-unused Invalid_widen exception
sim642 Aug 18, 2026
b26b319
Merge branch 'master' into widen-no-leq
sim642 Aug 26, 2026
1172010
Remove join wrapper from Partitioned arrays non-smart widen
sim642 Aug 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions src/arg/argConstraints.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,6 @@ struct
module VI = Printable.Prod3 (Node) (CC) (I)
module VIE = Printable.Prod (VI) (MyARG.InlineEdgePrintable)
module VIES = SetDomain.Make (VIE)
(* even though R is just a set and in solver's [widen old (join old new)] would join the sets of predecessors
instead of keeping just the last, we are saved by set's narrow bringing that back down to the latest predecessors *)
module R =
struct
include VIES
Expand Down
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/addressDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -377,7 +377,7 @@ struct
| false, false -> cop x y

let meet x y = merge join meet x y
let narrow x y = merge (fun x y -> widen x (join x y)) narrow x y
let narrow x y = merge widen narrow x y

let meet x y =
if M.tracing then M.traceli "ad" "meet %a %a" pretty x pretty y;
Expand Down
18 changes: 16 additions & 2 deletions src/cdomain/value/cdomains/arrayDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -361,12 +361,26 @@ struct

let widen (x:t) (y:t) = normalize @@ match x,y with
| Joint x, Joint y -> Joint (Val.widen x y)
| Partitioned (e,(xl, xm, xr)), Joint y -> Partitioned (e,(Val.widen xl y, Val.widen xm y, Val.widen xr y))
| Partitioned (e,(xl, xm, xr)), Joint y -> Partitioned (e,(Val.widen xl y, Val.widen xm y, Val.widen xr y)) (* TODO: This case is strange, see below. *)
| Joint x, Partitioned (e,(yl, ym, yr)) -> Partitioned (e,(Val.widen x yl, Val.widen x ym, Val.widen x yr))
| Partitioned (e,(xl, xm, xr)), Partitioned (e',(yl, ym, yr)) ->
if CilType.Exp.equal e e' then Partitioned (e,(Val.widen xl yl, Val.widen xm ym, Val.widen xr yr))
else Joint (Val.widen (join_of_all_parts x) (join_of_all_parts y))

(** The non-smart {!widen} has some strange behavior, e.g. with
- [x = Partitioned (foo, 1, 2, 3)],
- [y = Partitioned (bar, 4, 5, 6)].

On the one hand:
- [join x y = Joint [1,6]],
- [widen x (join x y) = Partitioned (foo, widen 1 [1,6], widen 2 [1,6], widen 3 [1,6]) = Partitioned (foo, [1,inf], top, top)].

On the other hand:
- [widen x y = Joint (widen [1,3] [4,6]) = Joint [1,inf]].

So it's not the same. The first one widens from [Partitioned] to [Joint] goes back to [Partitioned].
{!smart_widen} below doesn't have this issue. *)

let show = function
| Joint x -> "Array (no part.): " ^ Val.show x
| Partitioned (e,(xl, xm, xr)) ->
Expand Down Expand Up @@ -660,7 +674,7 @@ struct
Partitioned (e1, (op xl1 xl2, op xm1 xm2, op xr1 xr2))
| Partitioned (e1, (xl1, xm1, xr1)), Partitioned (e2, (xl2, xm2, xr2)) ->
if get_string "ana.base.partition-arrays.keep-expr" = "last" || get_bool "ana.base.partition-arrays.smart-join" then
let op = Val.join in (* widen between different components isn't called validly *)
let op = Val.join in (* widen between different components isn't called validly *) (* TODO: can remove join now? overrides argument op *)
let over_all_x1 = op (op xl1 xm1) xr1 in
let over_all_x2 = op (op xl2 xm2) xr2 in
let e1_in_state_of_x2 = x2_eval_int e1 in
Expand Down
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/concDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ struct

let meet x y = merge join meet x y

let narrow x y = merge (fun x y -> widen x (join x y)) narrow x y
let narrow x y = merge widen narrow x y

let diff_mustset x (y: FiniteMustThreadSet.t) =
FiniteMustThreadSet.fold (fun t -> remove (ThreadIdDomain.Thread t)) y x
Expand Down
1 change: 0 additions & 1 deletion src/cdomain/value/cdomains/floatDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -291,7 +291,6 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
| PlusInfinity, PlusInfinity -> PlusInfinity
| _ -> Bot

(** [widen x y] assumes [leq x y]. Solvers guarantee this by calling [widen old (join old new)]. *)
let widen v1 v2 = (* TODO: support 'threshold_widening' option *)
match v1, v2 with
| Top, _ | _, Top -> Top
Expand Down
1 change: 1 addition & 0 deletions src/cdomain/value/cdomains/int/bitfieldDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
let nabla x y= if x =: (x |: y) then x else one_mask

let widen (z1,o1) (z2,o2) = (nabla z1 z2, nabla o1 o2)
let widen x y = widen x (join x y) (* TODO: inline? *)

let lognot (z,o) = (o,z)

Expand Down
2 changes: 2 additions & 0 deletions src/cdomain/value/cdomains/int/defExcDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -261,6 +261,8 @@ struct
else
join' ~range:(size ik) ik x y

let widen ik x y = widen ik x (join ik x y) (* TODO: inline? *)


let meet ik x y =
match (x,y) with
Expand Down
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/int/intDomTuple.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -414,7 +414,7 @@ module IntDomTupleImpl = struct

(* f2: binary ops *)
let join ik =
map2 ~norefine:true ik {f2= (fun (type a) (module I : SOverflow with type t = a) -> I.join ik)}
map2 ~norefine:true ik {f2= (fun (type a) (module I : SOverflow with type t = a) -> I.join ik)} (* TODO: could join refine now that it's now part of every widening? possibly not because some intermediate widens still do the join (e.g. struct domains) *)

let meet ik =
map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) -> I.meet ik)}
Expand Down
5 changes: 2 additions & 3 deletions src/cdomain/value/cdomains/int/intervalDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,20 +146,19 @@ struct
let (min_ik, max_ik) = range ik in
let threshold = get_interval_threshold_widening () in
let l2 =
if Ints_t.compare l0 l1 = 0 then l0
if Ints_t.compare l0 l1 <= 0 then l0
else if threshold then IArith.lower_threshold l1 min_ik
else min_ik
in
let u2 =
if Ints_t.compare u0 u1 = 0 then u0
if Ints_t.compare u0 u1 >= 0 then u0
else if threshold then IArith.upper_threshold u1 max_ik
else max_ik
in
norm ik @@ Some (l2,u2) |> fst
let widen ik x y =
let r = widen ik x y in
if M.tracing && not (equal x y) then M.tracel "int" "interval widen %a %a -> %a" pretty x pretty y pretty r;
assert (leq x y); (* TODO: remove for performance reasons? *)
r

let narrow ik x y =
Expand Down
2 changes: 2 additions & 0 deletions src/cdomain/value/cdomains/int/intervalSetDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -545,6 +545,8 @@ struct
in
interval_sets_to_partitions ik xs ys |> merge_list ik |> widen_left |> widen_right |> List.map snd

let widen ik x y = widen ik x (join ik x y) (* TODO: inline? *)

let starting ik n = norm_interval ik (n, snd (range ik))

let ending ik n = norm_interval ik (fst (range ik), n)
Expand Down
6 changes: 6 additions & 0 deletions src/cdomain/value/cdomains/structDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,9 @@ struct

let join = join_with_fct Val.join

let widen_with_fct f x y = widen_with_fct f x (join x y) (* TODO: inline *)
let widen x y = widen x (join x y) (* TODO: inline *)

(* let invariant = HS.invariant *)
let invariant ~value_invariant ~offset ~lval _ = Invariant.none (* TODO *)

Expand Down Expand Up @@ -439,6 +442,9 @@ struct

let join = join_with_fct Val.join

let widen_with_fct f x y = widen_with_fct f x (join x y) (* TODO: inline *)
let widen x y = widen x (join x y) (* TODO: inline *)

(* let invariant c (x,_) = HS.invariant c x *)
let invariant ~value_invariant ~offset ~lval _ = Invariant.none (* TODO *)

Expand Down
6 changes: 3 additions & 3 deletions src/cdomain/value/cdomains/valueDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -649,17 +649,17 @@ struct
| (Float x, Float y) -> Float (FD.widen x y)
(* TODO: symmetric widen, wtf? *)
| (Int x, Address y)
| (Address y, Int x) -> Address (AD.widen y (AD.join y (AD.of_int x)))
| (Address y, Int x) -> Address (AD.widen y (AD.of_int x))
| (Address x, Address y) -> Address (AD.widen x y)
| (Struct x, Struct y) -> Struct (Structs.widen x y)
| (Union x, Union y) -> Union (Unions.widen x y)
| (Array x, Array y) -> Array (CArrays.widen x y)
| (Blob x, Blob y) -> Blob (Blobs.widen x y) (* TODO: why no blob special cases like in join? *)
| (Thread x, Thread y) -> Thread (Threads.widen x y)
| (Int x, Thread y)
| (Thread y, Int x) -> Thread (Threads.widen y (Threads.join y (Threads.top ())))
| (Thread y, Int x) -> Thread (Threads.widen y (Threads.top ())) (* not just [Threads.top ()] because this keeps known IDs in y *)
| (Address x, Thread y)
| (Thread y, Address x) -> Thread (Threads.widen y (Threads.join y (Threads.top ())))
| (Thread y, Address x) -> Thread (Threads.widen y (Threads.top ())) (* not just [Threads.top ()] because this keeps known IDs in y *)
| (Mutex, Mutex) -> Mutex
| (JmpBuf x, JmpBuf y) -> JmpBuf (JmpBufs.widen x y)
| (MutexAttr x, MutexAttr y) -> MutexAttr (MutexAttr.widen x y)
Expand Down
2 changes: 2 additions & 0 deletions src/cdomains/apron/apronDomain.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -779,6 +779,8 @@ struct
if M.tracing then M.traceu "apron" "-> %a" pretty w;
w

let widen x y = widen x (join x y) (* TODO: inline? *)

let narrow x y =
let x_env = A.env x in
let y_env = A.env y in
Expand Down
2 changes: 1 addition & 1 deletion src/cdomains/c2poDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ module C2PODomain = struct
data_to_t filtered_join

let widen_eq_classes a b =
join_f a b widen_eq_no_automata
join_f a (join a b) widen_eq_no_automata (* TODO: join needed? *)

let widen a b =
if M.tracing then M.trace "c2po-widen" "WIDEN\n";
Expand Down
16 changes: 4 additions & 12 deletions src/domain/disjointDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,9 +117,7 @@ struct
add (f e) acc
) m (empty ()) (* no intermediate lists *)

let widen m1 m2 =
Lattice.assert_valid_widen ~leq ~pretty_diff m1 m2;
M.widen m1 m2
let widen = M.widen

let meet m1 m2 =
M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
Expand Down Expand Up @@ -358,7 +356,6 @@ struct
S.union s1' acc

let widen s1 s2 =
Lattice.assert_valid_widen ~leq ~pretty_diff s1 s2;
let f b2 (s1, acc) =
let e2 = B.choose b2 in
let (s1_match, s1_rest) = S.partition (fun e1 -> C.cong (B.choose e1) e2) s1 in
Expand All @@ -371,8 +368,7 @@ struct
(s1_rest, S.add b' acc)
in
let (s1', acc) = S.fold f s2 (s1, empty ()) in
assert (is_empty s1'); (* since [leq s1 s2], folding over s2 should remove all s1 *)
acc (* TODO: extra union s2 needed? *)
S.union s1' acc

let meet s1 s2 =
let f b2 (s1, acc) =
Expand Down Expand Up @@ -611,9 +607,7 @@ struct
Some b'
) m1 m2

let widen m1 m2 =
Lattice.assert_valid_widen ~leq ~pretty_diff m1 m2;
M.widen m1 m2
let widen = M.widen

let meet m1 m2 =
M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
Expand Down Expand Up @@ -841,7 +835,6 @@ struct
S.union s1' acc

let widen s1 s2 =
Lattice.assert_valid_widen ~leq ~pretty_diff s1 s2;
let f b2 (s1, acc) =
let e2 = fst (B.choose b2) in
let (s1_match, s1_rest) = S.partition (fun e1 -> C.cong (fst (B.choose e1)) e2) s1 in
Expand All @@ -854,8 +847,7 @@ struct
(s1_rest, S.add b' acc)
in
let (s1', acc) = S.fold f s2 (s1, empty ()) in
assert (is_empty s1'); (* since [leq s1 s2], folding over s2 should remove all s1 *)
acc (* TODO: extra union s2 needed? *)
S.union s1' acc

let meet s1 s2 =
let f b2 (s1, acc) =
Expand Down
14 changes: 10 additions & 4 deletions src/domain/hoareDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ struct
(* widen new(!) element e with old(!) bucket using op *)
let rec widen op e = function
| [] -> []
| x::xs -> try if E.leq x e then [op x e] else widen op e xs with Lattice.Uncomparable -> widen op e xs (* only widen if valid *)
| x::xs -> try if E.leq x e then [op x e] else widen op e xs with Lattice.Uncomparable -> widen op e xs (* only widen if valid *) (* TODO: still need leq? *)

(* meet element e with bucket using op *)
let rec meet op e = function
Expand Down Expand Up @@ -90,6 +90,7 @@ struct

let join x y = merge_join E.join x y
let widen x y = merge_widen E.widen x y
let widen x y = widen x (join x y) (* TODO: inline *)
let meet x y = merge_meet E.meet x y
let narrow x y = merge_meet E.narrow x y (* TODO: fix narrow like widen? see Set *)

Expand Down Expand Up @@ -203,7 +204,8 @@ struct
let product_widen op a b = (* assumes b to be bigger than a *)
let xs,ys = elements a, elements b in
GobList.cartesian_map op xs ys |> fun x -> reduce (union b (of_list x))
let widen = product_widen (fun x y -> if B.leq x y then B.widen x y else B.bot ())
let widen = product_widen (fun x y -> if B.leq x y then B.widen x y else B.bot ()) (* TODO: still need leq? *)
let widen x y = widen x (join x y) (* TODO: inline *)
let narrow = product_bot (fun x y -> if B.leq y x then B.narrow x y else x)

let add x a = if mem x a then a else add x a (* special mem! *)
Expand Down Expand Up @@ -321,7 +323,9 @@ struct
let narrow = product_bot2 (fun (x, xr) (y, yr) -> if SpecD.leq y x then (SpecD.narrow x y, yr) else (x, xr))
(* let widen = product_widen (fun x y -> if SpecD.leq x y then SpecD.widen x y else SpecD.bot ()) R.widen *)
(* TODO: move PathSensitive3-specific widen out of HoareMap *)
let widen = product_widen2 (fun (x, xr) (y, yr) -> if SpecD.leq x y then (SpecD.widen x y, yr) else (y, yr)) (* TODO: is this right now? *)
let widen = product_widen2 (fun (x, xr) (y, yr) -> if SpecD.leq x y then (SpecD.widen x y, yr) else (y, yr)) (* TODO: is this right now? *) (* TODO: still need leq? *)

let widen x y = widen x (join x y) (* TODO: inline *)

(* TODO: shouldn't this also reduce? *)
let apply_list f s = elements s |> f |> of_list
Expand Down Expand Up @@ -369,7 +373,7 @@ struct
let product_widen (op: elt -> elt -> elt option) a b = (* assumes b to be bigger than a *)
let xs,ys = elements a, elements b in
GobList.cartesian_filter_map op xs ys |> fun x -> join b (of_list x)
let widen = product_widen (fun x y -> if E.leq x y then Some (E.widen x y) else None)
let widen = product_widen (fun x y -> if E.leq x y then Some (E.widen x y) else None) (* TODO: still need leq? *)

(* above widen is actually extrapolation operator, so define connector-based widening instead *)

Expand Down Expand Up @@ -398,4 +402,6 @@ struct
join_em s1 s2
in
widen s1 s2'

let widen x y = widen x (join x y) (* TODO: inline *)
end
21 changes: 5 additions & 16 deletions src/domain/lattice.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ sig
val leq: t -> t -> bool
val join: t -> t -> t
val meet: t -> t -> t
val widen: t -> t -> t (** [widen x y] assumes [leq x y]. Solvers guarantee this by calling [widen old (join old new)]. *)
val widen: t -> t -> t (** [widen x y] {e cannot} assume [leq x y]. *)

val narrow: t -> t -> t

Expand Down Expand Up @@ -57,17 +57,6 @@ exception BotValue
(** Exception raised by a bottomless lattice in place of a bottom value.
Surrounding lattice functors may handle this on their own. *)

exception Invalid_widen of Pretty.doc

let () = Printexc.register_printer (function
| Invalid_widen doc ->
Some (GobPretty.sprintf "Lattice.Invalid_widen(%a)" Pretty.insert doc)
| _ -> None (* for other exceptions *)
)

let assert_valid_widen ~leq ~pretty_diff x y =
if not (leq x y) then
raise (Invalid_widen (pretty_diff () (x, y)))

module UnitConf (N: Printable.Name) =
struct
Expand Down Expand Up @@ -289,7 +278,7 @@ struct
try `Lifted (Base.widen x y)
with TopValue | Uncomparable -> `Top
end
| _ -> y
| _ -> join x y

let narrow x y =
match (x,y) with
Expand Down Expand Up @@ -367,7 +356,7 @@ struct
match (x,y) with
| (`Lifted1 x, `Lifted1 y) -> `Lifted1 (Base1.widen x y)
| (`Lifted2 x, `Lifted2 y) -> `Lifted2 (Base2.widen x y)
| _ -> y
| _ -> join x y

let narrow x y =
match (x,y) with
Expand Down Expand Up @@ -457,7 +446,7 @@ struct
let widen x y =
match (x,y) with
| (`Lifted x, `Lifted y) -> `Lifted (Base.widen x y)
| _ -> y
| _ -> join x y

let narrow x y =
match (x,y) with
Expand Down Expand Up @@ -509,7 +498,7 @@ struct
try `Lifted (Base.widen x y)
with TopValue -> `Top
end
| _ -> y
| _ -> join x y

let narrow x y =
match (x,y) with
Expand Down
4 changes: 2 additions & 2 deletions src/domain/mapDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -707,7 +707,7 @@ struct
let widen_with_fct f x y =
match (x,y) with
| (`Lifted x, `Lifted y) -> `Lifted (M.widen_with_fct f x y)
| _ -> y
| _ -> join x y

let cardinal = function
| `Top -> raise (Fn_over_All "cardinal")
Expand Down Expand Up @@ -852,7 +852,7 @@ struct
let widen_with_fct f x y =
match (x,y) with
| (`Lifted x, `Lifted y) -> `Lifted(M.widen_with_fct f x y)
| _ -> y
| _ -> join x y

let reflexive_subset_domain_for_all2 f x y =
match (x,y) with
Expand Down
2 changes: 1 addition & 1 deletion src/domain/setDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -381,7 +381,7 @@ struct
| `Top, _ -> `Top
| _, `Top -> `Top
| `Lifted x, `Lifted y -> `Lifted (S.join x y)
let widen x y = (* assumes y to be bigger than x *)
let widen x y =
match x, y with
| `Top, _
| _, `Top -> `Top
Expand Down
Loading
Loading