From bd9f133f1cf07d82380edd62aa26ea6c728b5c7d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Tue, 9 Jan 2024 17:47:33 +0100 Subject: [PATCH] refactor(BV): Track domains for uninterpreted leaves only (#1004) This patch changes the internal representation of domains in the bitvector relations. Without the patch, we are keeping track of domains for *all* bit-vector terms, which is correct but wasteful. With the patch, we only track the domains of (currently) uninterpreted class representatives, and rebuild the domain associated with other terms on-the-fly before propagation. This avoids carrying around huge domain maps with a potentially large amount of duplication, and allow to share propagations between terms that include identical sub-terms immediately without a round-trip through Uf (without the patch, if we learn that `0 @ x -> 01??`, it does not immediately propagate that `1 @ x -> 11??`; we first have to assert `x<2,2> = 1` which gets solved into the substitution `x |-> 1 @ x'` and we only learn `11 @ x' -> 11??` when performing the substitution). On the other hand, it means that `Domains.get` and `Domains.update` are a bit more expensive now. Since the `Congruence` is now only used for constraints, and not for domains, we only need to add the arguments of the constraints to the `Congruence` (which should also be a slight performance boost). Other changes to the use of the `Congruence` module are needed to fix the mismatch between what is stored in the `Domains` (whose keys are now uninterpreted terms) and the `Constraints` (the actual arguments of the constraints in the original problem). There is one exception: we now add the arguments of `Distinct` to the congruence, which is required for completeness because the terms that we generate during case splits are not guaranteed to already exist (in fact, in general they don't, since we create 1-bit extractions that have no reason to be in the original problem). Note that there is also a small bugfix in `Congruence`: when performing a substitution we need to remove the old terms, otherwise we will forget dependencies if we ever add it back later. --- src/lib/reasoners/bitv_rel.ml | 260 +++++++++++++++++++-------------- src/lib/reasoners/rel_utils.ml | 15 +- 2 files changed, 167 insertions(+), 108 deletions(-) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index e05dd1131..15761cc24 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -111,9 +111,6 @@ module Domains : sig Use this to ensure that the representation is always normalized. - [v] must have an existing associated domain (possibly unconstrained) - before calling [subst]. Call [update] beforehand. - The explanation [ex] justifies the equality [p = v]. @raise Bitlist.Inconsistent if this causes any domain in [d] to become @@ -131,7 +128,12 @@ module Domains : sig end = struct type t = { bitlists : Bitlist.t MX.t - (** Mapping from semantic values to their bitlist domain. *) + (** Mapping from semantic values to their bitlist domain. + + Note: this mapping only contains domain for leaves (i.e. uninterpreted + terms or AC symbols); domains associated with more complex semantic + values are rebuilt on-the-fly using the structure of said semantic + values. *) ; changed : SX.t (** Elements whose domain has changed since last propagation. *) } @@ -144,7 +146,7 @@ end = struct ppf t.bitlists let empty = { bitlists = MX.empty ; changed = SX.empty } - let update ex r t bl = + let update_leaf ex r t bl = let changed = ref false in let bitlists = MX.update r (function @@ -171,45 +173,67 @@ end = struct let changed = if !changed then SX.add r t.changed else t.changed in { changed; bitlists } - let get r t = + let update_signed ex { Bitv.value; negated } t bl = + let bl = if negated then Bitlist.lognot bl else bl in + update_leaf ex value t bl + + let update ex r t bl = + fst @@ List.fold_left (fun (t, bl) { Bitv.bv; sz } -> + (* Extract the bitlist associated with the current component *) + let mid = Bitlist.width bl - sz in + let bl_tail = + if mid = 0 then Bitlist.empty else + Bitlist.extract bl 0 (mid - 1) + in + let bl = Bitlist.extract bl mid (Bitlist.width bl - 1) in + + match bv with + | Bitv.Cte z -> + (* Nothing to update, but still check for consistency! *) + ignore @@ Bitlist.intersect bl (Bitlist.exact sz z Ex.empty) ex; + t, bl_tail + | Other r -> update_signed ex r t bl, bl_tail + | Ext (r, r_size, i, j) -> + (* r = bl -> r = ?^(r_size - j - 1) @ bl @ ?^i *) + assert (i + r_size - j - 1 + Bitlist.width bl = r_size); + let hi = Bitlist.unknown (r_size - j - 1) Ex.empty in + let lo = Bitlist.unknown i Ex.empty in + update_signed ex r t Bitlist.(hi @ bl @ lo), bl_tail + ) (t, bl) (Shostak.Bitv.embed r) + + let get_leaf r t = try MX.find r t.bitlists with | Not_found -> match X.type_info r with | Tbitv n -> Bitlist.unknown n Explanation.empty | _ -> assert false + let get_signed { Bitv.value; negated } t = + let bl = get_leaf value t in + if negated then Bitlist.lognot bl else bl + + let get r t = + List.fold_left (fun bl { Bitv.bv; sz } -> + Bitlist.concat bl @@ + match bv with + | Bitv.Cte z -> Bitlist.exact sz z Ex.empty + | Other r -> get_signed r t + | Ext (r, _r_size, i, j) -> Bitlist.extract (get_signed r t) i j + ) Bitlist.empty (Shostak.Bitv.embed r) + let subst ex rr nrr t = match MX.find rr t.bitlists with | bl -> - let has_changed = ref (SX.mem rr t.changed) in - let bitlists = - MX.update nrr (function - | Some bl' as o -> - let bl'' = Bitlist.intersect bl bl' ex in - (* Keep simpler explanations, and don't loop adding the domain to - the changed set infinitely. *) - if Bitlist.equal bl' bl'' then - o - else ( - has_changed := true; - if Options.get_debug_bitv () then - Printer.print_dbg - ~module_name:"Bitv_rel" ~function_name:"Domain.subst" - "domain shrunk for %a: %a -> %a" - X.print nrr Bitlist.pp bl' Bitlist.pp bl''; - Some (Bitlist.intersect bl bl' ex) - ) - | None -> - (* We require that [nrr] has a domain before calling [subst]. *) - Printer.print_err - "Bitv_rel: substituting %a -> %a without domain" - X.print rr X.print nrr; - assert false - ) @@ MX.remove rr t.bitlists + (* Note: even if [rr] had changed its domain, we don't need to keep that + information because if the constraints that used to apply to [rr] were + not already valid, they will be marked as fresh in the [Constraints.t] + after substitution there and propagated already. *) + let t = + { changed = SX.remove rr t.changed + ; bitlists = MX.remove rr t.bitlists + } in - let changed = SX.remove rr t.changed in - let changed = if !has_changed then SX.add nrr changed else changed in - { changed ; bitlists } + update ex nrr t bl | exception Not_found -> t let choose_changed t = @@ -481,6 +505,11 @@ module Constraints : sig Fresh constraints are constraints that were never propagated yet. *) + val fold_r : (X.r -> 'a -> 'a) -> t -> 'a -> 'a + (** [fold_r f cs acc] folds [f] over any representative [r] that is currently + associated with a constraint (i.e. at least one constraint currently + applies to [r]). *) + val propagate : t -> X.r -> Domains.t -> Domains.t (** [propagate cs r dom] propagates the constraints associated with [r] in the constraint set [cs] and returns the new domain map after propagation. *) @@ -568,29 +597,38 @@ end = struct let acc = CS.fold f bcs.fresh acc in { bcs with fresh = CS.empty }, acc + let fold_r f bcs acc = + MX.fold (fun r _ acc -> f r acc) bcs.cs_map acc + let propagate bcs r dom = match MX.find r bcs.cs_map with | cs -> CS.fold Constraint.propagate cs dom | exception Not_found -> dom end -let extract_constraints bcs uf r t = +(* Add one constraint and register its arguments as relevant for congruence *) +let add_constraint (bcs, cgr) c = + let bcs = Constraints.add bcs c in + let cgr = Constraint.fold_deps Congruence.add c cgr in + (bcs, cgr) + +let extract_constraints (bcs, cgr) uf r t = match E.term_view t with (* BVnot is already internalized in the Shostak but we want to know about it without needing a round-trip through Uf *) | { f = Op BVnot; xs = [ x ] ; _ } -> let rx, exx = Uf.find uf x in - Constraints.add bcs @@ + add_constraint (bcs, cgr) @@ { repr = Constraint.hcons @@ Bnot (r, rx) ; ex = exx } | { f = Op BVand; xs = [ x; y ]; _ } -> let rx, exx = Uf.find uf x and ry, exy = Uf.find uf y in - Constraints.add bcs @@ + add_constraint (bcs, cgr) @@ { repr = Constraint.hcons @@ Band (r, rx, ry) ; ex = Ex.union exx exy } | { f = Op BVor; xs = [ x; y ]; _ } -> let rx, exx = Uf.find uf x and ry, exy = Uf.find uf y in - Constraints.add bcs @@ + add_constraint (bcs, cgr) @@ { repr = Constraint.hcons @@ Bor (r, rx, ry) ; ex = Ex.union exx exy } | { f = Op BVxor; xs = [ x; y ]; _ } -> let rx, exx = Uf.find uf x @@ -598,20 +636,9 @@ let extract_constraints bcs uf r t = let xs = SX.singleton r in let xs = if SX.mem rx xs then SX.remove rx xs else SX.add rx xs in let xs = if SX.mem ry xs then SX.remove ry xs else SX.add ry xs in - Constraints.add bcs @@ + add_constraint (bcs, cgr) @@ { repr = Constraint.hcons @@ Bxor xs ; ex = Ex.union exx exy } - | _ -> bcs - -(** [abstract_bitlist r ex] builds a bitlist representation of the semantic - bit-vector value [r] *) -let abstract_bitlist = - let rec aux = function - | [] -> Bitlist.empty - | { Bitv.bv = Bitv.Cte n; sz } :: bs -> - Bitlist.(exact sz n Ex.empty @ aux bs) - | { sz; bv = (Other _ | Ext _) } :: bs -> - Bitlist.(unknown sz Ex.empty @ aux bs) - in fun bs -> Bitlist.add_explanation (aux bs) + | _ -> (bcs, cgr) let rec mk_eq ex lhs w z = match lhs with @@ -666,12 +693,12 @@ let add_eqs = includes constraints that changed due to substitutions) - The constraints involving variables whose domain changed since the last propagation *) -let propagate = +let propagate cgr = let rec propagate changed bcs dom = match Domains.choose_changed dom with | r, dom -> ( propagate (SX.add r changed) bcs @@ - Constraints.propagate bcs r dom + Congruence.fold_parents (Constraints.propagate bcs) cgr r dom ) | exception Not_found -> changed, dom in @@ -709,31 +736,32 @@ let assume env uf la = | Th_util.CS (Th_bitv, n) -> Q.(ss * n) | _ -> ss in + let is_1bit r = + match X.type_info r with + | Tbitv 1 -> true + | _ -> false + in match a, orig with | L.Eq (rr, nrr), Subst when is_bv_r rr -> - let cc, acc = - Congruence.subst rr nrr cgr (fun rr nrr (bcs, dom) -> - let bl = - abstract_bitlist (Shostak.Bitv.embed nrr) Ex.empty - in - let dom = Domains.update Ex.empty nrr dom bl in - ( Constraints.subst ex rr nrr bcs - , Domains.subst ex rr nrr dom ) - ) (bcs, dom) - in (cc, acc, ss) - | L.Distinct (false, [rr; nrr]), NCS (Th_bitv, _) -> - (* We don't support [distinct] in general yet, but we must + let dom = Domains.subst ex rr nrr dom in + let cgr, bcs = + Congruence.subst rr nrr cgr (Constraints.subst ex) bcs + in + (cgr, (bcs, dom), ss) + | L.Distinct (false, [rr; nrr]), _ when is_1bit rr -> + (* We don't (yet) support [distinct] in general, but we must support it for case splits to avoid looping. - Note that for 1-bit vectors (i.e. booleans), we have `x <> y` - iff `x = not y`. *) - assert Stdlib.(X.type_info rr = Ty.Tbitv 1); - let drr = abstract_bitlist (Shostak.Bitv.embed rr) Ex.empty in - let dnrr = abstract_bitlist (Shostak.Bitv.embed nrr) Ex.empty in - let dom = Domains.update Ex.empty rr dom drr in - let dom = Domains.update Ex.empty nrr dom dnrr in - let bcs = - Constraints.add bcs @@ + We are a bit more general and support it for 1-bit vectors, for + which `distinct` can be expressed using `bvnot`. + + Note that we are not guaranteed that the arguments are already + in normal form! *) + let rr, exrr = Uf.find_r uf rr in + let nrr, exnrr = Uf.find_r uf nrr in + let ex = Ex.union ex (Ex.union exrr exnrr) in + let bcs, cgr = + add_constraint (bcs, cgr) @@ { repr = Constraint.hcons @@ Bnot (rr, nrr) ; ex } in (cgr, (bcs, dom), ss) @@ -742,7 +770,7 @@ let assume env uf la = (env.congruence, (env.constraints, env.domain), env.size_splits) la in - let eqs, constraints, domain = propagate constraints domain in + let eqs, constraints, domain = propagate congruence constraints domain in if Options.get_debug_bitv () && not (Lists.is_empty eqs) then ( Printer.print_dbg ~module_name:"Bitv_rel" ~function_name:"assume" @@ -770,35 +798,51 @@ let case_split env _uf ~for_model = [] else (* Look for representatives with minimal, non-fully known, domain size. + + We first look among the constrained variables, then if there are no + constrained variables, all the remaining variables. + [nunk] is the number of unknown bits. *) + let f_acc r bl acc = + let nunk = Bitlist.num_unknown bl in + if nunk = 0 then + acc + else + match acc with + | Some (nunk', _) when nunk > nunk' -> acc + | Some (nunk', xs) when nunk = nunk' -> + Some (nunk', SX.add r xs) + | _ -> Some (nunk, SX.singleton r) + in let _, candidates = match - Domains.fold (fun r bl acc -> - let nunk = Bitlist.num_unknown bl in - if nunk = 0 then - acc - else - match acc with - | Some (nunk', _) when nunk > nunk' -> acc - | Some (nunk', xs) when nunk = nunk' -> - Some (nunk', SX.add r xs) - | _ -> Some (nunk, SX.singleton r) - ) env.domain None + Constraints.fold_r (fun r acc -> + List.fold_left (fun acc { Bitv.bv; _ } -> + match bv with + | Bitv.Cte _ -> acc + | Other r | Ext (r, _, _, _) -> + let bl = Domains.get r.value env.domain in + f_acc r.value bl acc + ) acc (Shostak.Bitv.embed r) + ) env.constraints None with | Some (nunk, xs) -> nunk, xs - | None -> 0, SX.empty + | None -> + match Domains.fold f_acc env.domain None with + | Some (nunk, xs) -> nunk, xs + | None -> 0, SX.empty in (* For now, just pick a value for the most significant bit. *) match SX.choose candidates with | r -> - let biv = Shostak.Bitv.embed r in - let rec aux = function - | [] -> assert false - | { Bitv.bv = Bitv.Cte _; _ } :: biv -> aux biv - | part :: _ -> - Bitv.extract part.sz (part.sz - 1) (part.sz - 1) [ part ] + let bl = Domains.get r env.domain in + let w = Bitlist.width bl in + let unknown = Z.extract (Z.lognot @@ Bitlist.bits_known bl) 0 w in + let bitidx = Z.numbits unknown - 1 in + let lhs = + Shostak.Bitv.is_mine @@ + Bitv.extract w bitidx bitidx (Shostak.Bitv.embed r) in - let lhs = Shostak.Bitv.is_mine @@ aux biv in (* Just always pick zero for now. *) let zero = Shostak.Bitv.is_mine Bitv.[ { bv = Cte Z.zero ; sz = 1 } ] in if Options.get_debug_bitv () then @@ -811,19 +855,21 @@ let case_split env _uf ~for_model = let add env uf r t = let delayed, eqs = Rel_utils.Delayed.add env.delayed uf r t in let env, eqs = - if is_bv_r r then - try - let bcs = extract_constraints env.constraints uf r t in - let dr = abstract_bitlist (Shostak.Bitv.embed r) Ex.empty in - let dom = Domains.update Ex.empty r env.domain dr in - let congruence = Congruence.add r env.congruence in - let eqs', bcs, dom = propagate bcs dom in - { env with congruence ; constraints = bcs ; domain = dom }, - List.rev_append eqs' eqs - with Bitlist.Inconsistent ex -> - raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf) - else - env, eqs + match X.type_info r with + | Tbitv n -> ( + try + let dr = Bitlist.unknown n Ex.empty in + let dom = Domains.update Ex.empty r env.domain dr in + let (bcs, congruence) = + extract_constraints (env.constraints, env.congruence) uf r t + in + let eqs', bcs, dom = propagate congruence bcs dom in + { env with congruence ; constraints = bcs ; domain = dom }, + List.rev_append eqs' eqs + with Bitlist.Inconsistent ex -> + raise @@ Ex.Inconsistent (ex, Uf.cl_extract uf) + ) + | _ -> env, eqs in { env with delayed }, eqs diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml index 4691941a4..370568371 100644 --- a/src/lib/reasoners/rel_utils.ml +++ b/src/lib/reasoners/rel_utils.ml @@ -235,6 +235,10 @@ module Congruence : sig [f] is intended to perform a substitution operation on the type ['a], merging the values associated with [rr] into the values associated with [nrr]. *) + + val fold_parents : (X.r -> 'a -> 'a) -> t -> X.r -> 'a -> 'a + (** [fold_parents f t r acc] folds function [f] over all the registered terms + whose current representative contains [r] as a leaf. *) end = struct module SX = Shostak.SXH module MX = Shostak.MXH @@ -251,6 +255,11 @@ end = struct let empty = { parents = MX.empty ; registered = SX.empty } + let fold_parents f { parents; _ } r acc = + match MX.find r parents with + | deps -> SX.fold f deps acc + | exception Not_found -> acc + let add r t = if SX.mem r t.registered then t @@ -308,8 +317,12 @@ end = struct ) cgr.parents (X.leaves r) in + (* It is no longer here, but it could be added back later -- let's not + skip it! *) + let registered = SX.remove r cgr.registered in + (* Add the new representative to the congruence if needed *) - let cgr = add r' { cgr with parents } in + let cgr = add r' { parents ; registered } in (* Propagate the substitution *) cgr, f r r' t