{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module ToySolver.BitVector.Base
(
BV
, bv2nat
, nat2bv
, fromAscBits
, fromDescBits
, toAscBits
, toDescBits
, IsBV (..)
, Var (..)
, Expr (..)
, Op1 (..)
, Op2 (..)
, repeat
, zeroExtend
, signExtend
, Atom (..)
, BVComparison (..)
, module ToySolver.Data.OrdRel
, Model
, evalExpr
, evalAtom
) where
import Prelude hiding (repeat)
import Data.Bits
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Ord
import qualified Data.Semigroup as Semigroup
import qualified Data.Vector as V
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Unboxed as VU
import ToySolver.Data.Boolean
import ToySolver.Data.OrdRel
class Monoid a => IsBV a where
width :: a -> Int
:: Int -> Int -> a -> a
fromBV :: BV -> a
bvnot :: a -> a
bvand :: a -> a -> a
bvor :: a -> a -> a
bvxor :: a -> a -> a
bvnand :: a -> a -> a
bvnor :: a -> a -> a
bvxnor :: a -> a -> a
bvneg :: a -> a
bvadd :: a -> a -> a
bvsub :: a -> a -> a
bvmul :: a -> a -> a
bvudiv :: a -> a -> a
bvurem :: a -> a -> a
bvsdiv :: a -> a -> a
bvsrem :: a -> a -> a
bvsmod :: a -> a -> a
bvshl :: a -> a -> a
bvlshr :: a -> a -> a
bvashr :: a -> a -> a
bvcomp :: a -> a -> a
bvnand a
s a
t = forall a. IsBV a => a -> a
bvnot (forall a. IsBV a => a -> a -> a
bvand a
s a
t)
bvnor a
s a
t = forall a. IsBV a => a -> a
bvnot (forall a. IsBV a => a -> a -> a
bvor a
s a
t)
bvxnor a
s a
t = forall a. IsBV a => a -> a
bvnot (forall a. IsBV a => a -> a -> a
bvxor a
s a
t)
bvsub a
s a
t = forall a. IsBV a => a -> a -> a
bvadd a
s (forall a. IsBV a => a -> a
bvneg a
t)
repeat :: Monoid m => Int -> m -> m
repeat :: forall m. Monoid m => Int -> m -> m
repeat Int
i m
x = forall a. Monoid a => [a] -> a
mconcat (forall a. Int -> a -> [a]
replicate Int
i m
x)
zeroExtend :: IsBV a => Int -> a -> a
zeroExtend :: forall a. IsBV a => Int -> a -> a
zeroExtend Int
i a
s = forall a. IsBV a => [Bool] -> a
fromAscBits (forall a. Int -> a -> [a]
replicate Int
i Bool
False) forall a. Semigroup a => a -> a -> a
<> a
s
signExtend :: IsBV a => Int -> a -> a
signExtend :: forall a. IsBV a => Int -> a -> a
signExtend Int
i a
s
| Int
w forall a. Eq a => a -> a -> Bool
== Int
0 = forall a. IsBV a => [Bool] -> a
fromAscBits (forall a. Int -> a -> [a]
replicate Int
i Bool
False)
| Bool
otherwise = forall m. Monoid m => Int -> m -> m
repeat Int
i (forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) (Int
wforall a. Num a => a -> a -> a
-Int
1) a
s) forall a. Semigroup a => a -> a -> a
<> a
s
where
w :: Int
w = forall a. IsBV a => a -> Int
width a
s
class (IsBV a, IsEqRel a (ComparisonResult a), Complement (ComparisonResult a)) => BVComparison a where
type ComparisonResult a
bvule, bvult, bvuge, bvugt, bvsle, bvslt, bvsge, bvsgt :: a -> a -> ComparisonResult a
bvule a
a a
b = forall a. Complement a => a -> a
notB (forall a. BVComparison a => a -> a -> ComparisonResult a
bvult a
b a
a)
bvult a
a a
b = forall a. Complement a => a -> a
notB (forall a. BVComparison a => a -> a -> ComparisonResult a
bvule a
b a
a)
bvuge a
a a
b = forall a. BVComparison a => a -> a -> ComparisonResult a
bvule a
b a
a
bvugt a
a a
b = forall a. BVComparison a => a -> a -> ComparisonResult a
bvult a
b a
a
bvsle a
a a
b = forall a. Complement a => a -> a
notB (forall a. BVComparison a => a -> a -> ComparisonResult a
bvslt a
b a
a)
bvslt a
a a
b = forall a. Complement a => a -> a
notB (forall a. BVComparison a => a -> a -> ComparisonResult a
bvsle a
b a
a)
bvsge a
a a
b = forall a. BVComparison a => a -> a -> ComparisonResult a
bvsle a
b a
a
bvsgt a
a a
b = forall a. BVComparison a => a -> a -> ComparisonResult a
bvslt a
b a
a
{-# MINIMAL (bvule | bvult), (bvsle | bvslt) #-}
newtype BV = BV (VU.Vector Bool)
deriving (BV -> BV -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BV -> BV -> Bool
$c/= :: BV -> BV -> Bool
== :: BV -> BV -> Bool
$c== :: BV -> BV -> Bool
Eq)
instance Ord BV where
compare :: BV -> BV -> Ordering
compare (BV Vector Bool
bs1) (BV Vector Bool
bs2) =
(forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length forall a. Semigroup a => a -> a -> a
<> forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall (v :: * -> *) a. Vector v a => v a -> v a
VG.reverse) Vector Bool
bs1 Vector Bool
bs2
instance Semigroup.Semigroup BV where
BV Vector Bool
hi <> :: BV -> BV -> BV
<> BV Vector Bool
lo = Vector Bool -> BV
BV (Vector Bool
lo forall a. Semigroup a => a -> a -> a
<> Vector Bool
hi)
instance Monoid BV where
mempty :: BV
mempty = Vector Bool -> BV
BV forall (v :: * -> *) a. Vector v a => v a
VG.empty
instance Show BV where
show :: BV -> String
show BV
bv = String
"0b" forall a. [a] -> [a] -> [a]
++ [if Bool
b then Char
'1' else Char
'0' | Bool
b <- BV -> [Bool]
toDescBits BV
bv]
instance Bits BV where
.&. :: BV -> BV -> BV
(.&.) = forall a. IsBV a => a -> a -> a
bvand
.|. :: BV -> BV -> BV
(.|.) = forall a. IsBV a => a -> a -> a
bvor
xor :: BV -> BV -> BV
xor = forall a. IsBV a => a -> a -> a
bvxor
complement :: BV -> BV
complement = forall a. IsBV a => a -> a
bvnot
shiftL :: BV -> Int -> BV
shiftL BV
x Int
i
| Int
i forall a. Ord a => a -> a -> Bool
< Int
w = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
i) Int
0 BV
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Integer -> a
nat2bv Int
i Integer
0
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv Int
w Integer
0
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
x
shiftR :: BV -> Int -> BV
shiftR BV
x Int
i
| Int
i forall a. Ord a => a -> a -> Bool
< Int
w = forall a. IsBV a => Int -> Integer -> a
nat2bv Int
i Integer
0 forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) Int
i BV
x
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv Int
w Integer
0
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
x
rotateL :: BV -> Int -> BV
rotateL BV
x Int
i
| Int
w forall a. Eq a => a -> a -> Bool
== Int
0 = BV
x
| Bool
otherwise = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
j) Int
0 BV
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) (Int
wforall a. Num a => a -> a -> a
-Int
j) BV
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
x
j :: Int
j = Int
i forall a. Integral a => a -> a -> a
`mod` Int
w
rotateR :: BV -> Int -> BV
rotateR BV
x Int
i
| Int
w forall a. Eq a => a -> a -> Bool
== Int
0 = BV
x
| Bool
otherwise = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
jforall a. Num a => a -> a -> a
-Int
1) Int
0 BV
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) Int
j BV
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
x
j :: Int
j = Int
i forall a. Integral a => a -> a -> a
`mod` Int
w
zeroBits :: BV
zeroBits = forall a. HasCallStack => String -> a
error String
"zeroBits is not implemented"
bit :: Int -> BV
bit = forall a. HasCallStack => String -> a
error String
"bit is not implemented"
setBit :: BV -> Int -> BV
setBit x :: BV
x@(BV Vector Bool
bs) Int
i
| Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< Int
w = Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ Vector Bool
bs forall (v :: * -> *) a. Vector v a => v a -> [(Int, a)] -> v a
VG.// [(Int
i,Bool
True)]
| Bool
otherwise = BV
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
x
clearBit :: BV -> Int -> BV
clearBit x :: BV
x@(BV Vector Bool
bs) Int
i
| Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< Int
w = Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ Vector Bool
bs forall (v :: * -> *) a. Vector v a => v a -> [(Int, a)] -> v a
VG.// [(Int
i,Bool
False)]
| Bool
otherwise = BV
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
x
complementBit :: BV -> Int -> BV
complementBit x :: BV
x@(BV Vector Bool
bs) Int
i
| Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< Int
w = Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ Vector Bool
bs forall (v :: * -> *) a. Vector v a => v a -> [(Int, a)] -> v a
VG.// [(Int
i, Bool -> Bool
not (forall a. Bits a => a -> Int -> Bool
testBit BV
x Int
i))]
| Bool
otherwise = BV
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
x
testBit :: BV -> Int -> Bool
testBit x :: BV
x@(BV Vector Bool
bs) Int
i
| Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< Int
w = Vector Bool
bs forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! Int
i
| Bool
otherwise = Bool
False
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
x
popCount :: BV -> Int
popCount BV
x = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int
1 | Bool
b <- BV -> [Bool]
toAscBits BV
x, Bool
b]
bitSizeMaybe :: BV -> Maybe Int
bitSizeMaybe BV
_ = forall a. Maybe a
Nothing
bitSize :: BV -> Int
bitSize BV
_ = forall a. HasCallStack => String -> a
error String
"bitSize is not implemented"
isSigned :: BV -> Bool
isSigned BV
_ = Bool
False
instance IsBV BV where
width :: BV -> Int
width (BV Vector Bool
bs) = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs
extract :: Int -> Int -> BV -> BV
extract Int
i Int
j (BV Vector Bool
bs) = Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a. Vector v a => Int -> Int -> v a -> v a
VG.slice Int
j (Int
i forall a. Num a => a -> a -> a
- Int
j forall a. Num a => a -> a -> a
+ Int
1) Vector Bool
bs
fromBV :: BV -> BV
fromBV = forall a. a -> a
id
bvnot :: BV -> BV
bvnot (BV Vector Bool
bs) = Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map Bool -> Bool
not Vector Bool
bs
bvand :: BV -> BV -> BV
bvand (BV Vector Bool
bs1) (BV Vector Bool
bs2)
| forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs1 forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs2 = forall a. HasCallStack => String -> a
error String
"width mismatch"
| Bool
otherwise = Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a b c.
(Vector v a, Vector v b, Vector v c) =>
(a -> b -> c) -> v a -> v b -> v c
VG.zipWith Bool -> Bool -> Bool
(&&) Vector Bool
bs1 Vector Bool
bs2
bvor :: BV -> BV -> BV
bvor (BV Vector Bool
bs1) (BV Vector Bool
bs2)
| forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs1 forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs2 = forall a. HasCallStack => String -> a
error String
"width mismatch"
| Bool
otherwise = Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a b c.
(Vector v a, Vector v b, Vector v c) =>
(a -> b -> c) -> v a -> v b -> v c
VG.zipWith Bool -> Bool -> Bool
(||) Vector Bool
bs1 Vector Bool
bs2
bvxor :: BV -> BV -> BV
bvxor (BV Vector Bool
bs1) (BV Vector Bool
bs2)
| forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs1 forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs2 = forall a. HasCallStack => String -> a
error String
"width mismatch"
| Bool
otherwise = Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a b c.
(Vector v a, Vector v b, Vector v c) =>
(a -> b -> c) -> v a -> v b -> v c
VG.zipWith forall a. Eq a => a -> a -> Bool
(/=) Vector Bool
bs1 Vector Bool
bs2
bvneg :: BV -> BV
bvneg BV
x = forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) forall a b. (a -> b) -> a -> b
$ Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ forall a. IsBV a => a -> Int
width BV
x forall a. Num a => a -> a -> a
- forall a. Integral a => BV -> a
bv2nat BV
x
bvadd :: BV -> BV -> BV
bvadd BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) (forall a. Integral a => BV -> a
bv2nat BV
x forall a. Num a => a -> a -> a
+ forall a. Integral a => BV -> a
bv2nat BV
y)
bvmul :: BV -> BV -> BV
bvmul BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) (forall a. Integral a => BV -> a
bv2nat BV
x forall a. Num a => a -> a -> a
* forall a. Integral a => BV -> a
bv2nat BV
y)
bvudiv :: BV -> BV -> BV
bvudiv BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Integer
y' forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a. HasCallStack => String -> a
error String
"division by zero"
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) (forall a. Integral a => BV -> a
bv2nat BV
x forall a. Integral a => a -> a -> a
`div` Integer
y')
where
y' :: Integer
y' :: Integer
y' = forall a. Integral a => BV -> a
bv2nat BV
y
bvurem :: BV -> BV -> BV
bvurem BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Integer
y' forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a. HasCallStack => String -> a
error String
"division by zero"
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) (forall a. Integral a => BV -> a
bv2nat BV
x forall a. Integral a => a -> a -> a
`mod` Integer
y')
where
y' :: Integer
y' :: Integer
y' = forall a. Integral a => BV -> a
bv2nat BV
y
bvsdiv :: BV -> BV -> BV
bvsdiv BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
y forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = forall a. IsBV a => a -> a -> a
bvudiv BV
x BV
y
| Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => a -> a -> a
bvudiv (forall a. IsBV a => a -> a
bvneg BV
x) BV
y
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => a -> a -> a
bvudiv BV
x (forall a. IsBV a => a -> a
bvneg BV
y)
| Bool
otherwise = forall a. IsBV a => a -> a -> a
bvudiv (forall a. IsBV a => a -> a
bvneg BV
x) (forall a. IsBV a => a -> a
bvneg BV
y)
where
msb_x :: Bool
msb_x = forall a. Bits a => a -> Int -> Bool
testBit BV
x (forall a. IsBV a => a -> Int
width BV
x forall a. Num a => a -> a -> a
- Int
1)
msb_y :: Bool
msb_y = forall a. Bits a => a -> Int -> Bool
testBit BV
y (forall a. IsBV a => a -> Int
width BV
y forall a. Num a => a -> a -> a
- Int
1)
bvsrem :: BV -> BV -> BV
bvsrem BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
y forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = forall a. IsBV a => a -> a -> a
bvurem BV
x BV
y
| Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => a -> a -> a
bvurem (forall a. IsBV a => a -> a
bvneg BV
x) BV
y
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = forall a. IsBV a => a -> a -> a
bvurem BV
x (forall a. IsBV a => a -> a
bvneg BV
y)
| Bool
otherwise = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => a -> a -> a
bvurem (forall a. IsBV a => a -> a
bvneg BV
x) (forall a. IsBV a => a -> a
bvneg BV
y)
where
msb_x :: Bool
msb_x = forall a. Bits a => a -> Int -> Bool
testBit BV
x (forall a. IsBV a => a -> Int
width BV
x forall a. Num a => a -> a -> a
- Int
1)
msb_y :: Bool
msb_y = forall a. Bits a => a -> Int -> Bool
testBit BV
y (forall a. IsBV a => a -> Int
width BV
y forall a. Num a => a -> a -> a
- Int
1)
bvsmod :: BV -> BV -> BV
bvsmod BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
y forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| forall a. Integral a => BV -> a
bv2nat BV
u forall a. Eq a => a -> a -> Bool
== (Integer
0::Integer) = BV
u
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = BV
u
| Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = forall a. IsBV a => a -> a -> a
bvadd (forall a. IsBV a => a -> a
bvneg BV
u) BV
y
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = forall a. IsBV a => a -> a -> a
bvadd BV
u BV
y
| Bool
otherwise = forall a. IsBV a => a -> a
bvneg BV
u
where
msb_x :: Bool
msb_x = forall a. Bits a => a -> Int -> Bool
testBit BV
x (forall a. IsBV a => a -> Int
width BV
x forall a. Num a => a -> a -> a
- Int
1)
msb_y :: Bool
msb_y = forall a. Bits a => a -> Int -> Bool
testBit BV
y (forall a. IsBV a => a -> Int
width BV
y forall a. Num a => a -> a -> a
- Int
1)
abs_x :: BV
abs_x = if Bool
msb_x then forall a. IsBV a => a -> a
bvneg BV
x else BV
x
abs_y :: BV
abs_y = if Bool
msb_y then forall a. IsBV a => a -> a
bvneg BV
y else BV
y
u :: BV
u = forall a. IsBV a => a -> a -> a
bvurem BV
abs_x BV
abs_y
bvshl :: BV -> BV -> BV
bvshl BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) (forall a. Integral a => BV -> a
bv2nat BV
x forall a. Bits a => a -> Int -> a
`shiftL` forall a. Integral a => BV -> a
bv2nat BV
y)
bvlshr :: BV -> BV -> BV
bvlshr BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) (forall a. Integral a => BV -> a
bv2nat BV
x forall a. Bits a => a -> Int -> a
`shiftR` forall a. Integral a => BV -> a
bv2nat BV
y)
bvashr :: BV -> BV -> BV
bvashr BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool -> Bool
not Bool
msb_x = forall a. IsBV a => a -> a -> a
bvlshr BV
x BV
y
| Bool
otherwise = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => a -> a -> a
bvlshr (forall a. IsBV a => a -> a
bvneg BV
x) BV
y
where
msb_x :: Bool
msb_x = forall a. Bits a => a -> Int -> Bool
testBit BV
x (forall a. IsBV a => a -> Int
width BV
x forall a. Num a => a -> a -> a
- Int
1)
bvcomp :: BV -> BV -> BV
bvcomp BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv Int
1 (if BV
xforall a. Eq a => a -> a -> Bool
==BV
y then Integer
1 else Integer
0)
instance IsEqRel BV Bool where
.==. :: BV -> BV -> Bool
(.==.) = forall a. Eq a => a -> a -> Bool
(==)
./=. :: BV -> BV -> Bool
(./=.) = forall a. Eq a => a -> a -> Bool
(/=)
instance BVComparison BV where
type ComparisonResult BV = Bool
bvule :: BV -> BV -> ComparisonResult BV
bvule = forall a. Ord a => a -> a -> Bool
(<=)
bvsle :: BV -> BV -> ComparisonResult BV
bvsle BV
bs1 BV
bs2
| forall a. IsBV a => a -> Int
width BV
bs1 forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
bs2 = forall a. HasCallStack => String -> a
error (String
"length mismatch: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. IsBV a => a -> Int
width BV
bs1) forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. IsBV a => a -> Int
width BV
bs2))
| Int
w forall a. Eq a => a -> a -> Bool
== Int
0 = forall a. MonotoneBoolean a => a
true
| Bool
otherwise = Bool
bs1_msb Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
bs2_msb Bool -> Bool -> Bool
|| (Bool
bs1_msb forall a. Eq a => a -> a -> Bool
== Bool
bs2_msb) Bool -> Bool -> Bool
&& BV
bs1 forall a. Ord a => a -> a -> Bool
<= BV
bs2
where
w :: Int
w = forall a. IsBV a => a -> Int
width BV
bs1
bs1_msb :: Bool
bs1_msb = forall a. Bits a => a -> Int -> Bool
testBit BV
bs1 (Int
wforall a. Num a => a -> a -> a
-Int
1)
bs2_msb :: Bool
bs2_msb = forall a. Bits a => a -> Int -> Bool
testBit BV
bs2 (Int
wforall a. Num a => a -> a -> a
-Int
1)
bv2nat :: Integral a => BV -> a
bv2nat :: forall a. Integral a => BV -> a
bv2nat (BV Vector Bool
bv) = forall (v :: * -> *) b a.
Vector v b =>
(a -> Int -> b -> a) -> a -> v b -> a
VG.ifoldl' (\a
r Int
i Bool
x -> if Bool
x then a
rforall a. Num a => a -> a -> a
+a
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
i else a
r) a
0 Vector Bool
bv
nat2bv :: IsBV a => Int -> Integer -> a
nat2bv :: forall a. IsBV a => Int -> Integer -> a
nat2bv Int
m Integer
x = forall a. IsBV a => BV -> a
fromBV forall a b. (a -> b) -> a -> b
$ Vector Bool -> BV
BV forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a. Vector v a => Int -> (Int -> a) -> v a
VG.generate Int
m (forall a. Bits a => a -> Int -> Bool
testBit Integer
x)
fromAscBits :: IsBV a => [Bool] -> a
fromAscBits :: forall a. IsBV a => [Bool] -> a
fromAscBits = forall a. IsBV a => BV -> a
fromBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Bool -> BV
BV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList
fromDescBits :: IsBV a => [Bool] -> a
fromDescBits :: forall a. IsBV a => [Bool] -> a
fromDescBits = forall a. IsBV a => BV -> a
fromBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsBV a => [Bool] -> a
fromAscBits forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse
toAscBits :: BV -> [Bool]
toAscBits :: BV -> [Bool]
toAscBits (BV Vector Bool
bs) = forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Bool
bs
toDescBits :: BV -> [Bool]
toDescBits :: BV -> [Bool]
toDescBits = forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> [Bool]
toAscBits
data Var
= Var
{ Var -> Int
varWidth :: {-# UNPACK #-} !Int
, Var -> Int
varId :: {-# UNPACK #-} !Int
}
deriving (Var -> Var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord, Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show)
data Expr
= EConst BV
| EVar Var
| EOp1 Op1 Expr
| EOp2 Op2 Expr Expr
deriving (Expr -> Expr -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: Expr -> Expr -> Bool
Eq, Eq Expr
Expr -> Expr -> Bool
Expr -> Expr -> Ordering
Expr -> Expr -> Expr
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmax :: Expr -> Expr -> Expr
>= :: Expr -> Expr -> Bool
$c>= :: Expr -> Expr -> Bool
> :: Expr -> Expr -> Bool
$c> :: Expr -> Expr -> Bool
<= :: Expr -> Expr -> Bool
$c<= :: Expr -> Expr -> Bool
< :: Expr -> Expr -> Bool
$c< :: Expr -> Expr -> Bool
compare :: Expr -> Expr -> Ordering
$ccompare :: Expr -> Expr -> Ordering
Ord, Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show)
data Op1
= !Int !Int
| OpNot
| OpNeg
deriving (Op1 -> Op1 -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Op1 -> Op1 -> Bool
$c/= :: Op1 -> Op1 -> Bool
== :: Op1 -> Op1 -> Bool
$c== :: Op1 -> Op1 -> Bool
Eq, Eq Op1
Op1 -> Op1 -> Bool
Op1 -> Op1 -> Ordering
Op1 -> Op1 -> Op1
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Op1 -> Op1 -> Op1
$cmin :: Op1 -> Op1 -> Op1
max :: Op1 -> Op1 -> Op1
$cmax :: Op1 -> Op1 -> Op1
>= :: Op1 -> Op1 -> Bool
$c>= :: Op1 -> Op1 -> Bool
> :: Op1 -> Op1 -> Bool
$c> :: Op1 -> Op1 -> Bool
<= :: Op1 -> Op1 -> Bool
$c<= :: Op1 -> Op1 -> Bool
< :: Op1 -> Op1 -> Bool
$c< :: Op1 -> Op1 -> Bool
compare :: Op1 -> Op1 -> Ordering
$ccompare :: Op1 -> Op1 -> Ordering
Ord, Int -> Op1 -> ShowS
[Op1] -> ShowS
Op1 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Op1] -> ShowS
$cshowList :: [Op1] -> ShowS
show :: Op1 -> String
$cshow :: Op1 -> String
showsPrec :: Int -> Op1 -> ShowS
$cshowsPrec :: Int -> Op1 -> ShowS
Show)
data Op2
= OpConcat
| OpAnd
| OpOr
| OpXOr
| OpComp
| OpAdd
| OpMul
| OpUDiv
| OpURem
| OpSDiv
| OpSRem
| OpSMod
| OpShl
| OpLShr
| OpAShr
deriving (Op2 -> Op2 -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Op2 -> Op2 -> Bool
$c/= :: Op2 -> Op2 -> Bool
== :: Op2 -> Op2 -> Bool
$c== :: Op2 -> Op2 -> Bool
Eq, Eq Op2
Op2 -> Op2 -> Bool
Op2 -> Op2 -> Ordering
Op2 -> Op2 -> Op2
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Op2 -> Op2 -> Op2
$cmin :: Op2 -> Op2 -> Op2
max :: Op2 -> Op2 -> Op2
$cmax :: Op2 -> Op2 -> Op2
>= :: Op2 -> Op2 -> Bool
$c>= :: Op2 -> Op2 -> Bool
> :: Op2 -> Op2 -> Bool
$c> :: Op2 -> Op2 -> Bool
<= :: Op2 -> Op2 -> Bool
$c<= :: Op2 -> Op2 -> Bool
< :: Op2 -> Op2 -> Bool
$c< :: Op2 -> Op2 -> Bool
compare :: Op2 -> Op2 -> Ordering
$ccompare :: Op2 -> Op2 -> Ordering
Ord, Int -> Op2
Op2 -> Int
Op2 -> [Op2]
Op2 -> Op2
Op2 -> Op2 -> [Op2]
Op2 -> Op2 -> Op2 -> [Op2]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Op2 -> Op2 -> Op2 -> [Op2]
$cenumFromThenTo :: Op2 -> Op2 -> Op2 -> [Op2]
enumFromTo :: Op2 -> Op2 -> [Op2]
$cenumFromTo :: Op2 -> Op2 -> [Op2]
enumFromThen :: Op2 -> Op2 -> [Op2]
$cenumFromThen :: Op2 -> Op2 -> [Op2]
enumFrom :: Op2 -> [Op2]
$cenumFrom :: Op2 -> [Op2]
fromEnum :: Op2 -> Int
$cfromEnum :: Op2 -> Int
toEnum :: Int -> Op2
$ctoEnum :: Int -> Op2
pred :: Op2 -> Op2
$cpred :: Op2 -> Op2
succ :: Op2 -> Op2
$csucc :: Op2 -> Op2
Enum, Op2
forall a. a -> a -> Bounded a
maxBound :: Op2
$cmaxBound :: Op2
minBound :: Op2
$cminBound :: Op2
Bounded, Int -> Op2 -> ShowS
[Op2] -> ShowS
Op2 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Op2] -> ShowS
$cshowList :: [Op2] -> ShowS
show :: Op2 -> String
$cshow :: Op2 -> String
showsPrec :: Int -> Op2 -> ShowS
$cshowsPrec :: Int -> Op2 -> ShowS
Show)
instance IsBV Expr where
width :: Expr -> Int
width (EConst BV
x) = forall a. IsBV a => a -> Int
width BV
x
width (EVar Var
v) = Var -> Int
varWidth Var
v
width (EOp1 Op1
op Expr
arg) =
case Op1
op of
OpExtract Int
i Int
j -> Int
i forall a. Num a => a -> a -> a
- Int
j forall a. Num a => a -> a -> a
+ Int
1
Op1
_ -> forall a. IsBV a => a -> Int
width Expr
arg
width (EOp2 Op2
op Expr
arg1 Expr
arg2) =
case Op2
op of
Op2
OpConcat -> forall a. IsBV a => a -> Int
width Expr
arg1 forall a. Num a => a -> a -> a
+ forall a. IsBV a => a -> Int
width Expr
arg2
Op2
OpComp -> Int
1
Op2
_ -> forall a. IsBV a => a -> Int
width Expr
arg1
extract :: Int -> Int -> Expr -> Expr
extract Int
i Int
j = Op1 -> Expr -> Expr
EOp1 (Int -> Int -> Op1
OpExtract Int
i Int
j)
fromBV :: BV -> Expr
fromBV = BV -> Expr
EConst
bvnot :: Expr -> Expr
bvnot = Op1 -> Expr -> Expr
EOp1 Op1
OpNot
bvand :: Expr -> Expr -> Expr
bvand = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpAnd
bvor :: Expr -> Expr -> Expr
bvor = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpOr
bvxor :: Expr -> Expr -> Expr
bvxor = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpXOr
bvneg :: Expr -> Expr
bvneg = Op1 -> Expr -> Expr
EOp1 Op1
OpNeg
bvadd :: Expr -> Expr -> Expr
bvadd = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpAdd
bvmul :: Expr -> Expr -> Expr
bvmul = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpMul
bvudiv :: Expr -> Expr -> Expr
bvudiv = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpUDiv
bvurem :: Expr -> Expr -> Expr
bvurem = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpURem
bvsdiv :: Expr -> Expr -> Expr
bvsdiv = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpSDiv
bvsrem :: Expr -> Expr -> Expr
bvsrem = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpSRem
bvsmod :: Expr -> Expr -> Expr
bvsmod = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpSMod
bvshl :: Expr -> Expr -> Expr
bvshl = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpShl
bvlshr :: Expr -> Expr -> Expr
bvlshr = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpLShr
bvashr :: Expr -> Expr -> Expr
bvashr = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpAShr
bvcomp :: Expr -> Expr -> Expr
bvcomp = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpComp
instance Semigroup.Semigroup Expr where
<> :: Expr -> Expr -> Expr
(<>) = Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpConcat
instance Monoid Expr where
mempty :: Expr
mempty = BV -> Expr
EConst forall a. Monoid a => a
mempty
instance Bits Expr where
.&. :: Expr -> Expr -> Expr
(.&.) = forall a. IsBV a => a -> a -> a
bvand
.|. :: Expr -> Expr -> Expr
(.|.) = forall a. IsBV a => a -> a -> a
bvor
xor :: Expr -> Expr -> Expr
xor = forall a. IsBV a => a -> a -> a
bvxor
complement :: Expr -> Expr
complement = forall a. IsBV a => a -> a
bvnot
shiftL :: Expr -> Int -> Expr
shiftL Expr
x Int
i
| Int
i forall a. Ord a => a -> a -> Bool
< Int
w = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
i) Int
0 Expr
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Integer -> a
nat2bv Int
i Integer
0
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv Int
w Integer
0
where
w :: Int
w = forall a. IsBV a => a -> Int
width Expr
x
shiftR :: Expr -> Int -> Expr
shiftR Expr
x Int
i
| Int
i forall a. Ord a => a -> a -> Bool
< Int
w = forall a. IsBV a => Int -> Integer -> a
nat2bv Int
i Integer
0 forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) Int
i Expr
x
| Bool
otherwise = forall a. IsBV a => Int -> Integer -> a
nat2bv Int
w Integer
0
where
w :: Int
w = forall a. IsBV a => a -> Int
width Expr
x
rotateL :: Expr -> Int -> Expr
rotateL Expr
x Int
i
| Int
w forall a. Eq a => a -> a -> Bool
== Int
0 = Expr
x
| Bool
otherwise = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
j) Int
0 Expr
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) (Int
wforall a. Num a => a -> a -> a
-Int
j) Expr
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width Expr
x
j :: Int
j = Int
i forall a. Integral a => a -> a -> a
`mod` Int
w
rotateR :: Expr -> Int -> Expr
rotateR Expr
x Int
i
| Int
w forall a. Eq a => a -> a -> Bool
== Int
0 = Expr
x
| Bool
otherwise = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
jforall a. Num a => a -> a -> a
-Int
1) Int
0 Expr
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) Int
j Expr
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width Expr
x
j :: Int
j = Int
i forall a. Integral a => a -> a -> a
`mod` Int
w
zeroBits :: Expr
zeroBits = forall a. HasCallStack => String -> a
error String
"zeroBits is not implemented"
bit :: Int -> Expr
bit = forall a. HasCallStack => String -> a
error String
"bit is not implemented"
setBit :: Expr -> Int -> Expr
setBit Expr
x Int
i
| Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< Int
w = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) (Int
iforall a. Num a => a -> a -> a
+Int
1) Expr
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => [Bool] -> a
fromDescBits [Bool
True] forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
iforall a. Num a => a -> a -> a
-Int
1) Int
0 Expr
x
| Bool
otherwise = Expr
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width Expr
x
clearBit :: Expr -> Int -> Expr
clearBit Expr
x Int
i
| Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< Int
w = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) (Int
iforall a. Num a => a -> a -> a
+Int
1) Expr
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => [Bool] -> a
fromDescBits [Bool
False] forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
iforall a. Num a => a -> a -> a
-Int
1) Int
0 Expr
x
| Bool
otherwise = Expr
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width Expr
x
complementBit :: Expr -> Int -> Expr
complementBit Expr
x Int
i
| Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< Int
w = forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wforall a. Num a => a -> a -> a
-Int
1) (Int
iforall a. Num a => a -> a -> a
+Int
1) Expr
x forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => a -> a
bvnot (forall a. IsBV a => Int -> Int -> a -> a
extract Int
i Int
i Expr
x) forall a. Semigroup a => a -> a -> a
<> forall a. IsBV a => Int -> Int -> a -> a
extract (Int
iforall a. Num a => a -> a -> a
-Int
1) Int
0 Expr
x
| Bool
otherwise = Expr
x
where
w :: Int
w = forall a. IsBV a => a -> Int
width Expr
x
testBit :: Expr -> Int -> Bool
testBit = forall a. HasCallStack => String -> a
error String
"testBit is not implemented"
popCount :: Expr -> Int
popCount = forall a. HasCallStack => String -> a
error String
"popCount is not implemented"
bitSizeMaybe :: Expr -> Maybe Int
bitSizeMaybe Expr
_ = forall a. Maybe a
Nothing
bitSize :: Expr -> Int
bitSize Expr
_ = forall a. HasCallStack => String -> a
error String
"bitSize is not implemented"
isSigned :: Expr -> Bool
isSigned Expr
_ = Bool
False
data Atom = Rel (OrdRel Expr) Bool
deriving (Atom -> Atom -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c== :: Atom -> Atom -> Bool
Eq, Eq Atom
Atom -> Atom -> Bool
Atom -> Atom -> Ordering
Atom -> Atom -> Atom
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmax :: Atom -> Atom -> Atom
>= :: Atom -> Atom -> Bool
$c>= :: Atom -> Atom -> Bool
> :: Atom -> Atom -> Bool
$c> :: Atom -> Atom -> Bool
<= :: Atom -> Atom -> Bool
$c<= :: Atom -> Atom -> Bool
< :: Atom -> Atom -> Bool
$c< :: Atom -> Atom -> Bool
compare :: Atom -> Atom -> Ordering
$ccompare :: Atom -> Atom -> Ordering
Ord, Int -> Atom -> ShowS
[Atom] -> ShowS
Atom -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Atom] -> ShowS
$cshowList :: [Atom] -> ShowS
show :: Atom -> String
$cshow :: Atom -> String
showsPrec :: Int -> Atom -> ShowS
$cshowsPrec :: Int -> Atom -> ShowS
Show)
instance Complement Atom where
notB :: Atom -> Atom
notB (Rel OrdRel Expr
rel Bool
signed) = OrdRel Expr -> Bool -> Atom
Rel (forall a. Complement a => a -> a
notB OrdRel Expr
rel) Bool
signed
instance IsEqRel Expr Atom where
Expr
a .==. :: Expr -> Expr -> Atom
.==. Expr
b = OrdRel Expr -> Bool -> Atom
Rel (Expr
a forall e r. IsEqRel e r => e -> e -> r
.==. Expr
b) Bool
False
Expr
a ./=. :: Expr -> Expr -> Atom
./=. Expr
b = OrdRel Expr -> Bool -> Atom
Rel (Expr
a forall e r. IsEqRel e r => e -> e -> r
./=. Expr
b) Bool
False
instance BVComparison Expr where
type ComparisonResult Expr = Atom
bvule :: Expr -> Expr -> ComparisonResult Expr
bvule Expr
s Expr
t = OrdRel Expr -> Bool -> Atom
Rel (Expr
s forall e r. IsOrdRel e r => e -> e -> r
.<=. Expr
t) Bool
False
bvult :: Expr -> Expr -> ComparisonResult Expr
bvult Expr
s Expr
t = OrdRel Expr -> Bool -> Atom
Rel (Expr
s forall e r. IsOrdRel e r => e -> e -> r
.<. Expr
t) Bool
False
bvuge :: Expr -> Expr -> ComparisonResult Expr
bvuge Expr
s Expr
t = OrdRel Expr -> Bool -> Atom
Rel (Expr
s forall e r. IsOrdRel e r => e -> e -> r
.>=. Expr
t) Bool
False
bvugt :: Expr -> Expr -> ComparisonResult Expr
bvugt Expr
s Expr
t = OrdRel Expr -> Bool -> Atom
Rel (Expr
s forall e r. IsOrdRel e r => e -> e -> r
.>. Expr
t) Bool
False
bvsle :: Expr -> Expr -> ComparisonResult Expr
bvsle Expr
s Expr
t = OrdRel Expr -> Bool -> Atom
Rel (Expr
s forall e r. IsOrdRel e r => e -> e -> r
.<=. Expr
t) Bool
True
bvslt :: Expr -> Expr -> ComparisonResult Expr
bvslt Expr
s Expr
t = OrdRel Expr -> Bool -> Atom
Rel (Expr
s forall e r. IsOrdRel e r => e -> e -> r
.<. Expr
t) Bool
True
bvsge :: Expr -> Expr -> ComparisonResult Expr
bvsge Expr
s Expr
t = OrdRel Expr -> Bool -> Atom
Rel (Expr
s forall e r. IsOrdRel e r => e -> e -> r
.>=. Expr
t) Bool
True
bvsgt :: Expr -> Expr -> ComparisonResult Expr
bvsgt Expr
s Expr
t = OrdRel Expr -> Bool -> Atom
Rel (Expr
s forall e r. IsOrdRel e r => e -> e -> r
.>. Expr
t) Bool
True
type Model = (V.Vector BV, Map BV BV, Map BV BV)
evalExpr :: Model -> Expr -> BV
evalExpr :: Model -> Expr -> BV
evalExpr (Vector BV
env, Map BV BV
divTable, Map BV BV
remTable) = Expr -> BV
f
where
f :: Expr -> BV
f (EConst BV
bv) = BV
bv
f (EVar Var
v) = Vector BV
env forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! Var -> Int
varId Var
v
f (EOp1 Op1
op Expr
x) = forall {a}. IsBV a => Op1 -> a -> a
evalOp1 Op1
op (Expr -> BV
f Expr
x)
f (EOp2 Op2
op Expr
x Expr
y) = Op2 -> BV -> BV -> BV
evalOp2 Op2
op (Expr -> BV
f Expr
x) (Expr -> BV
f Expr
y)
evalOp1 :: Op1 -> a -> a
evalOp1 (OpExtract Int
i Int
j) = forall a. IsBV a => Int -> Int -> a -> a
extract Int
i Int
j
evalOp1 Op1
OpNot = forall a. IsBV a => a -> a
bvnot
evalOp1 Op1
OpNeg = forall a. IsBV a => a -> a
bvneg
evalOp2 :: Op2 -> BV -> BV -> BV
evalOp2 Op2
OpConcat BV
a BV
b = BV
a forall a. Semigroup a => a -> a -> a
<> BV
b
evalOp2 Op2
OpAnd BV
x BV
y = forall a. IsBV a => a -> a -> a
bvand BV
x BV
y
evalOp2 Op2
OpOr BV
x BV
y = forall a. IsBV a => a -> a -> a
bvor BV
x BV
y
evalOp2 Op2
OpXOr BV
x BV
y = forall a. IsBV a => a -> a -> a
bvxor BV
x BV
y
evalOp2 Op2
OpAdd BV
x BV
y = forall a. IsBV a => a -> a -> a
bvadd BV
x BV
y
evalOp2 Op2
OpMul BV
x BV
y = forall a. IsBV a => a -> a -> a
bvmul BV
x BV
y
evalOp2 Op2
OpUDiv BV
x BV
y
| Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 = forall a. IsBV a => a -> a -> a
bvudiv BV
x BV
y
| Bool
otherwise =
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BV
x Map BV BV
divTable of
Just BV
d -> BV
d
Maybe BV
Nothing -> forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) Integer
0
where
y' :: Integer
y' :: Integer
y' = forall a. Integral a => BV -> a
bv2nat BV
y
evalOp2 Op2
OpURem BV
x BV
y
| Integer
y' forall a. Eq a => a -> a -> Bool
/= Integer
0 = forall a. IsBV a => a -> a -> a
bvurem BV
x BV
y
| Bool
otherwise =
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BV
x Map BV BV
remTable of
Just BV
r -> BV
r
Maybe BV
Nothing -> forall a. IsBV a => Int -> Integer -> a
nat2bv (forall a. IsBV a => a -> Int
width BV
x) Integer
0
where
y' :: Integer
y' :: Integer
y' = forall a. Integral a => BV -> a
bv2nat BV
y
evalOp2 Op2
OpSDiv BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
y forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = Op2 -> BV -> BV -> BV
evalOp2 Op2
OpUDiv BV
x BV
y
| Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ Op2 -> BV -> BV -> BV
evalOp2 Op2
OpUDiv (forall a. IsBV a => a -> a
bvneg BV
x) BV
y
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ Op2 -> BV -> BV -> BV
evalOp2 Op2
OpUDiv BV
x (forall a. IsBV a => a -> a
bvneg BV
y)
| Bool
otherwise = Op2 -> BV -> BV -> BV
evalOp2 Op2
OpUDiv (forall a. IsBV a => a -> a
bvneg BV
x) (forall a. IsBV a => a -> a
bvneg BV
y)
where
msb_x :: Bool
msb_x = forall a. Bits a => a -> Int -> Bool
testBit BV
x (forall a. IsBV a => a -> Int
width BV
x forall a. Num a => a -> a -> a
- Int
1)
msb_y :: Bool
msb_y = forall a. Bits a => a -> Int -> Bool
testBit BV
y (forall a. IsBV a => a -> Int
width BV
y forall a. Num a => a -> a -> a
- Int
1)
evalOp2 Op2
OpSRem BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
y forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = Op2 -> BV -> BV -> BV
evalOp2 Op2
OpURem BV
x BV
y
| Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ Op2 -> BV -> BV -> BV
evalOp2 Op2
OpURem (forall a. IsBV a => a -> a
bvneg BV
x) BV
y
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = Op2 -> BV -> BV -> BV
evalOp2 Op2
OpURem BV
x (forall a. IsBV a => a -> a
bvneg BV
y)
| Bool
otherwise = forall a. IsBV a => a -> a
bvneg forall a b. (a -> b) -> a -> b
$ Op2 -> BV -> BV -> BV
evalOp2 Op2
OpURem (forall a. IsBV a => a -> a
bvneg BV
x) (forall a. IsBV a => a -> a
bvneg BV
y)
where
msb_x :: Bool
msb_x = forall a. Bits a => a -> Int -> Bool
testBit BV
x (forall a. IsBV a => a -> Int
width BV
x forall a. Num a => a -> a -> a
- Int
1)
msb_y :: Bool
msb_y = forall a. Bits a => a -> Int -> Bool
testBit BV
y (forall a. IsBV a => a -> Int
width BV
y forall a. Num a => a -> a -> a
- Int
1)
evalOp2 Op2
OpSMod BV
x BV
y
| forall a. IsBV a => a -> Int
width BV
x forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
y forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| forall a. IsBV a => a -> Int
width BV
x forall a. Eq a => a -> a -> Bool
/= forall a. IsBV a => a -> Int
width BV
y = forall a. HasCallStack => String -> a
error String
"invalid width"
| forall a. Integral a => BV -> a
bv2nat BV
u forall a. Eq a => a -> a -> Bool
== (Integer
0::Integer) = BV
u
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = BV
u
| Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = forall a. IsBV a => a -> a -> a
bvadd (forall a. IsBV a => a -> a
bvneg BV
u) BV
y
| Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = forall a. IsBV a => a -> a -> a
bvadd BV
u BV
y
| Bool
otherwise = forall a. IsBV a => a -> a
bvneg BV
u
where
msb_x :: Bool
msb_x = forall a. Bits a => a -> Int -> Bool
testBit BV
x (forall a. IsBV a => a -> Int
width BV
x forall a. Num a => a -> a -> a
- Int
1)
msb_y :: Bool
msb_y = forall a. Bits a => a -> Int -> Bool
testBit BV
y (forall a. IsBV a => a -> Int
width BV
y forall a. Num a => a -> a -> a
- Int
1)
abs_x :: BV
abs_x = if Bool
msb_x then forall a. IsBV a => a -> a
bvneg BV
x else BV
x
abs_y :: BV
abs_y = if Bool
msb_y then forall a. IsBV a => a -> a
bvneg BV
y else BV
y
u :: BV
u = Op2 -> BV -> BV -> BV
evalOp2 Op2
OpURem BV
abs_x BV
abs_y
evalOp2 Op2
OpShl BV
x BV
y = forall a. IsBV a => a -> a -> a
bvshl BV
x BV
y
evalOp2 Op2
OpLShr BV
x BV
y = forall a. IsBV a => a -> a -> a
bvlshr BV
x BV
y
evalOp2 Op2
OpAShr BV
x BV
y = forall a. IsBV a => a -> a -> a
bvashr BV
x BV
y
evalOp2 Op2
OpComp BV
x BV
y = forall a. IsBV a => Int -> Integer -> a
nat2bv Int
1 (if BV
xforall a. Eq a => a -> a -> Bool
==BV
y then Integer
1 else Integer
0)
evalAtom :: Model -> Atom -> Bool
evalAtom :: Model -> Atom -> Bool
evalAtom Model
m (Rel (OrdRel Expr
lhs RelOp
op Expr
rhs) Bool
False) = forall a. Ord a => RelOp -> a -> a -> Bool
evalOp RelOp
op (Model -> Expr -> BV
evalExpr Model
m Expr
lhs) (Model -> Expr -> BV
evalExpr Model
m Expr
rhs)
evalAtom Model
m (Rel (OrdRel Expr
lhs RelOp
op Expr
rhs) Bool
True) =
case RelOp
op of
RelOp
Lt -> forall a. BVComparison a => a -> a -> ComparisonResult a
bvslt BV
lhs' BV
rhs'
RelOp
Gt -> forall a. BVComparison a => a -> a -> ComparisonResult a
bvslt BV
rhs' BV
lhs'
RelOp
Le -> forall a. BVComparison a => a -> a -> ComparisonResult a
bvsle BV
lhs' BV
rhs'
RelOp
Ge -> forall a. BVComparison a => a -> a -> ComparisonResult a
bvsle BV
rhs' BV
lhs'
RelOp
Eql -> BV
lhs' forall a. Eq a => a -> a -> Bool
== BV
rhs'
RelOp
NEq -> BV
lhs' forall a. Eq a => a -> a -> Bool
/= BV
rhs'
where
lhs' :: BV
lhs' = Model -> Expr -> BV
evalExpr Model
m Expr
lhs
rhs' :: BV
rhs' = Model -> Expr -> BV
evalExpr Model
m Expr
rhs