Skip to content

Commit

Permalink
Make first argument constant whenever possible when normalizing multi…
Browse files Browse the repository at this point in the history
…plication

This tends to play better with libraries such as What4, which use a similar
convention. See the Haddocks for `mul`.

This is part of an eventual fix for GaloisInc/saw-script#1828.
  • Loading branch information
RyanGlScott committed Mar 6, 2023
1 parent 5ecac4b commit ef84b3b
Showing 1 changed file with 15 additions and 9 deletions.
24 changes: 15 additions & 9 deletions src/Data/AIG/Operations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -627,25 +627,31 @@ subConst g x c = addConst g x (-c)
-- of the same size as the arguments.
-- Overflow is silently discarded.
--
-- Because it is beneficial to have the second argument be a constant whenever
-- Because it is beneficial to have the first argument be a constant whenever
-- possible (see the Haddocks for `mul'`), this will flip the order of
-- arguments if the first argument is a constant.
--
-- Because multiplication is commutative, we could just as well process the
-- arguments the other way around. We deliberately choose the convention of
-- making the first argument be a constant whenever possible due to the fact
-- that several downstream libraries (e.g., What4) already normalize
-- multiplication to have constants appear as the first argument.
mul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
mul g x y = assert (length x == length y) $
if isJust (asUnsigned g x)
then mul' g y x -- The first argument is constant, so swap the arguments
if isJust (asUnsigned g y)
then mul' g y x -- The second argument is a constant, so swap the arguments
else mul' g x y

-- | Multiply two bitvectors with the same size, with result
-- of the same size as the arguments.
-- Overflow is silently discarded.
--
-- This algorithm computes partial products by adding multiples of the first
-- This algorithm computes partial products by adding multiples of the second
-- 'BV' argument, where the coefficient is computed from different bits of the
-- second argument. Whenever the second 'BV' argument is a constant,
-- first argument. Whenever the first 'BV' argument is a constant,
-- bitblasting the resulting AIG will result in a network of full adders,
-- which is very amenable to verification. As a result, it is beneficial to
-- make the second 'BV' argument a constant whenever possible. (See
-- make the first 'BV' argument a constant whenever possible. (See
-- https://github.com/GaloisInc/saw-script/issues/1828 for a specific example
-- of where this can help.)
--
Expand All @@ -654,13 +660,13 @@ mul g x y = assert (length x == length y) $
mul' :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
mul' g x y = do
-- Create mutable array to store result.
let n = length y
let n = length x
-- Function to update bits.
let updateBits i z | i == n = return z
updateBits i z = do
z' <- iteM g (y ! i) (add g z (shlC g x i)) (return z)
z' <- iteM g (x ! i) (add g z (shlC g y i)) (return z)
updateBits (i+1) z'
updateBits 0 $ replicate (length x) (falseLit g)
updateBits 0 $ replicate (length y) (falseLit g)

-- | Unsigned multiply two bitvectors with size @m@ and size @n@,
-- resulting in a vector of size @m+n@.
Expand Down

0 comments on commit ef84b3b

Please sign in to comment.