From 7ce7868682c4c6c07586ef83dce5a03c9783510c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 19 Jul 2024 13:59:20 +0200 Subject: [PATCH] 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. --- src/lib/reasoners/bitlist.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/lib/reasoners/bitlist.ml b/src/lib/reasoners/bitlist.ml index 4cc322e22..ec0c1029c 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