From 0e4c36e18cf210d062e888f4908efa72283cfc55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Mon, 20 Nov 2023 09:44:43 +0100 Subject: [PATCH] fix: Do not call [X.make] on non-subterms for bv2nat MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit It turns out that https://github.com/OCamlPro/alt-ergo/pull/881 revealed a latent issue with the implementation in https://github.com/OCamlPro/alt-ergo/pull/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 https://github.com/OCamlPro/alt-ergo/pull/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 https://github.com/OCamlPro/alt-ergo/pull/944 . This would avoid needing to go through terms for this. --- src/lib/reasoners/bitv.ml | 13 +- tests/bitv/testfile-bitv024.expected | 2 + tests/bitv/testfile-bitv024.smt2 | 4 + tests/dune.inc | 249 +++++++++++++++++++++++++++ 4 files changed, 265 insertions(+), 3 deletions(-) create mode 100644 tests/bitv/testfile-bitv024.expected create mode 100644 tests/bitv/testfile-bitv024.smt2 diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index c7c6ffdca..4d5e7234a 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -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 @@ -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 @@ -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 diff --git a/tests/bitv/testfile-bitv024.expected b/tests/bitv/testfile-bitv024.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/bitv/testfile-bitv024.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/bitv/testfile-bitv024.smt2 b/tests/bitv/testfile-bitv024.smt2 new file mode 100644 index 000000000..6315bca0c --- /dev/null +++ b/tests/bitv/testfile-bitv024.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(declare-const x (_ BitVec 4)) +(assert (= (bv2nat ((_ extract 3 2) x)) 0)) +(check-sat) diff --git a/tests/dune.inc b/tests/dune.inc index 62c2b6d2f..ef3858853 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -120886,6 +120886,255 @@ (package alt-ergo) (action (diff testfile-bv2nat-delayed.dolmen.expected testfile-bv2nat-delayed.dolmen_dolmen.output))) + (rule + (target testfile-bitv024_ci_cdcl_no_minimal_bj.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps testfile-bitv024_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_ci_cdcl_no_minimal_bj.output))) + (rule + (target testfile-bitv024_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-bitv024_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-bitv024_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-bitv024_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-bitv024_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-bitv024_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target testfile-bitv024_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (deps testfile-bitv024_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target testfile-bitv024_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps testfile-bitv024_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target testfile-bitv024_cdcl.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps testfile-bitv024_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_cdcl.output))) + (rule + (target testfile-bitv024_tableaux_cdcl.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps testfile-bitv024_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_tableaux_cdcl.output))) + (rule + (target testfile-bitv024_tableaux.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps testfile-bitv024_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_tableaux.output))) + (rule + (target testfile-bitv024_dolmen.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-bitv024_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_dolmen.output))) + (rule + (target testfile-bitv024_fpa.output) + (deps (:input testfile-bitv024.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (deps testfile-bitv024_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv024.expected testfile-bitv024_fpa.output))) (rule (target testfile-bitv023_ci_cdcl_no_minimal_bj.output) (deps (:input testfile-bitv023.ae))