Skip to content

Commit

Permalink
fix: Do not call [X.make] on non-subterms for bv2nat
Browse files Browse the repository at this point in the history
It turns out that OCamlPro#881 revealed
a latent issue with the implementation in
OCamlPro#733

When we encounter a [bv2nat] term, we create a *term* that represents
the [bv2nat] computation, then call [X.make] on the result. This has the
unfortunate effect that the sub-terms of that new term are not added to
the Union-Find (or at least not before the term itself). This is bad,
but was harmless at the time.

However, the resulting term from a call of [bv2nat] includes divisions.
And since OCamlPro#881 divisions are
represented by an uninterpreted term rather than an existential variable
— and [IntervalCalculus.add] inspects that term, rightfully expecting
that its sub-terms have been added to the Union-Find, which in this case
they are not, and so we crash.

This patch fixes the issue by introducing an uninterpreted term for the
result of [bv2nat] and adding the equality between that uninterpreted
term and the [bv2nat] computation. This equality is then processed as a
term on its own, ensuring that subterms are added to the Union-Find
before the terms that contain them.

Note that long-term, we probably want to get rid of the construction of
[bv2nat] terms directly in [X.make] in favor of propagators in a
follow-up to OCamlPro#944 . This would
avoid needing to go through terms for this.
  • Loading branch information
bclement-ocp committed Nov 20, 2023
1 parent fb98e82 commit 0e4c36e
Show file tree
Hide file tree
Showing 4 changed files with 265 additions and 3 deletions.
13 changes: 10 additions & 3 deletions src/lib/reasoners/bitv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1317,7 +1317,7 @@ module Shostak(X : ALIEN) = struct
we do so, we may end up in a loop where we repeatedly call [X.make] on a
[BV2Nat] term -- so instead if we are a single [Other] term, we become
uninterpreted. *)
let bv2nat bv =
let bv2nat ot bv =
match bv with
| [{ bv = Other { value = r; negated }; sz }] ->
let t = term_extract r in
Expand All @@ -1342,7 +1342,14 @@ module Shostak(X : ALIEN) = struct
| { ty; _ } ->
Util.internal_error "expected bitv, got %a" Ty.print ty
end
| _ -> abstract_to_nat bv |> X.make
| _ ->
(* Note: we can't just call [X.make] on the result of [abstract_to_nat]
because [X.make] should only be called on subterms. If we do it, it
causes crashes when `IntervalCalculus.add` assumes that the arguments
of division operators have been added to the `Uf` prior to the
division itself. *)
let t' = abstract_to_nat bv in
X.term_embed ot, [ E.Core.eq ot t' ]

let make t =
let { E.f; xs; _ } = E.term_view t in
Expand All @@ -1357,7 +1364,7 @@ module Shostak(X : ALIEN) = struct
[int2bv] terms, we convert the composition [(bv2nat ((_ int2bv n) x))]
into [(mod x (pow 2 n))]. *)
let r, ctx = Canon.make x in
let r, ctx' = bv2nat r in
let r, ctx' = bv2nat t r in
r, List.rev_append ctx' ctx
| _ ->
let r, ctx = Canon.make t in
Expand Down
2 changes: 2 additions & 0 deletions tests/bitv/testfile-bitv024.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

unknown
4 changes: 4 additions & 0 deletions tests/bitv/testfile-bitv024.smt2
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
(set-logic ALL)
(declare-const x (_ BitVec 4))
(assert (= (bv2nat ((_ extract 3 2) x)) 0))
(check-sat)
249 changes: 249 additions & 0 deletions tests/dune.inc

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

0 comments on commit 0e4c36e

Please sign in to comment.