From c2e419f45a685a16d4f56aaa025045124608c45c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Mon, 22 Jul 2024 16:01:08 +0200 Subject: [PATCH] fix(BV): Do not lose explanations in bvmul (#1170) * fix(BV): Do not lose explanations in bvmul The implementation of bvmul from #1144 introduced a soundness bug: when we do not know anything about the result, the explanation is dropped. This is because the implementation was performing mixing bitlist computation and creation of raw bitlist values. This patch fixes the implementation by performing all computations in [Z] and only adding the explanation at the end. * Add a test --- src/lib/reasoners/bitlist.ml | 17 ++- tests/dune.inc | 249 +++++++++++++++++++++++++++++++++++ tests/issues/1170.expected | 2 + tests/issues/1170.smt2 | 6 + 4 files changed, 265 insertions(+), 9 deletions(-) create mode 100644 tests/issues/1170.expected create mode 100644 tests/issues/1170.smt2 diff --git a/src/lib/reasoners/bitlist.ml b/src/lib/reasoners/bitlist.ml index 0d346257c..a663b106f 100644 --- a/src/lib/reasoners/bitlist.ml +++ b/src/lib/reasoners/bitlist.ml @@ -321,20 +321,19 @@ let mul a b = let low_a_known = Z.trailing_zeros @@ a.bits_unk in let low_b_known = Z.trailing_zeros @@ b.bits_unk in let low_known = min low_a_known low_b_known in - let mid_bits = exact Z.(value a * value b) ex in + let mid_bits = Z.(value a * value b) in let mid_bits = if low_known = max_int then mid_bits - else extract mid_bits 0 low_known + else if low_known = 0 then Z.zero + else Z.extract mid_bits 0 low_known in if low_known = max_int then - mid_bits lsl zeroes + exact Z.(mid_bits lsl zeroes) ex else - let high_bits = - { bits_set = Z.zero - ; bits_unk = Z.minus_one - ; ex = Ex.empty } - in - ((high_bits lsl low_known) lor mid_bits) lsl zeroes + (* High bits are unknown *) + { bits_set = Z.(mid_bits lsl zeroes) + ; bits_unk = Z.(minus_one lsl Stdlib.(low_known + zeroes)) + ; ex } let bvshl ~size:sz a b = (* If the minimum value for [b] is larger than the bitwidth, the result is diff --git a/tests/dune.inc b/tests/dune.inc index fdb2e10f5..46f4bec79 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -180418,6 +180418,255 @@ (package alt-ergo) (action (diff 340.expected 340_fpa.output))) + (rule + (target 1170_ci_cdcl_no_minimal_bj.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps 1170_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_cdcl_no_minimal_bj.output))) + (rule + (target 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 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 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 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 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 1170_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 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 1170_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 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 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target 1170_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps 1170_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1170.expected 1170_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target 1170_cdcl.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps 1170_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_cdcl.output))) + (rule + (target 1170_tableaux_cdcl.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps 1170_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_tableaux_cdcl.output))) + (rule + (target 1170_tableaux.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps 1170_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_tableaux.output))) + (rule + (target 1170_dolmen.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps 1170_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_dolmen.output))) + (rule + (target 1170_fpa.output) + (deps (:input 1170.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (deps 1170_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1170.expected 1170_fpa.output))) (rule (target 1163.models_dolmen.output) (deps (:input 1163.models.smt2)) diff --git a/tests/issues/1170.expected b/tests/issues/1170.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/1170.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/issues/1170.smt2 b/tests/issues/1170.smt2 new file mode 100644 index 000000000..94ab438f8 --- /dev/null +++ b/tests/issues/1170.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_BV) +(declare-const A (_ BitVec 2)) +(declare-const B (_ BitVec 1)) +(declare-const C (_ BitVec 3)) +(assert (= (bvmul (_ bv3 4) (concat A (concat #b0 B))) (concat C #b1))) +(check-sat)