{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.BitVector.Base
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.BitVector.Base
  (
  -- * BitVector values
    BV
  , bv2nat
  , nat2bv
  , fromAscBits
  , fromDescBits
  , toAscBits
  , toDescBits
  , IsBV (..)

  -- * BitVector language
  , 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
  extract :: 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 = a -> a
forall a. IsBV a => a -> a
bvnot (a -> a -> a
forall a. IsBV a => a -> a -> a
bvand a
s a
t)
  bvnor a
s a
t  = a -> a
forall a. IsBV a => a -> a
bvnot (a -> a -> a
forall a. IsBV a => a -> a -> a
bvor a
s a
t)
  bvxnor a
s a
t = a -> a
forall a. IsBV a => a -> a
bvnot (a -> a -> a
forall a. IsBV a => a -> a -> a
bvxor a
s a
t)

  bvsub a
s a
t = a -> a -> a
forall a. IsBV a => a -> a -> a
bvadd a
s (a -> a
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 = [m] -> m
forall a. Monoid a => [a] -> a
mconcat (Int -> m -> [m]
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 = [Bool] -> a
forall a. IsBV a => [Bool] -> a
fromAscBits (Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate Int
i Bool
False) a -> a -> a
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = [Bool] -> a
forall a. IsBV a => [Bool] -> a
fromAscBits (Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate Int
i Bool
False)
  | Bool
otherwise = Int -> a -> a
forall m. Monoid m => Int -> m -> m
repeat Int
i (Int -> Int -> a -> a
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) a
s) a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
s
  where
    w :: Int
w = a -> Int
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 = ComparisonResult a -> ComparisonResult a
forall a. Complement a => a -> a
notB (a -> a -> ComparisonResult a
forall a. BVComparison a => a -> a -> ComparisonResult a
bvult a
b a
a)
  bvult a
a a
b = ComparisonResult a -> ComparisonResult a
forall a. Complement a => a -> a
notB (a -> a -> ComparisonResult a
forall a. BVComparison a => a -> a -> ComparisonResult a
bvule a
b a
a)
  bvuge a
a a
b = a -> a -> ComparisonResult a
forall a. BVComparison a => a -> a -> ComparisonResult a
bvule a
b a
a
  bvugt a
a a
b = a -> a -> ComparisonResult a
forall a. BVComparison a => a -> a -> ComparisonResult a
bvult a
b a
a

  bvsle a
a a
b = ComparisonResult a -> ComparisonResult a
forall a. Complement a => a -> a
notB (a -> a -> ComparisonResult a
forall a. BVComparison a => a -> a -> ComparisonResult a
bvslt a
b a
a)
  bvslt a
a a
b = ComparisonResult a -> ComparisonResult a
forall a. Complement a => a -> a
notB (a -> a -> ComparisonResult a
forall a. BVComparison a => a -> a -> ComparisonResult a
bvsle a
b a
a)
  bvsge a
a a
b = a -> a -> ComparisonResult a
forall a. BVComparison a => a -> a -> ComparisonResult a
bvsle a
b a
a
  bvsgt a
a a
b = a -> a -> ComparisonResult a
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
(BV -> BV -> Bool) -> (BV -> BV -> Bool) -> Eq BV
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BV -> BV -> Bool
== :: BV -> BV -> Bool
$c/= :: BV -> BV -> Bool
/= :: BV -> BV -> Bool
Eq)

instance Ord BV where
  compare :: BV -> BV -> Ordering
compare (BV Vector Bool
bs1) (BV Vector Bool
bs2) =
    ((Vector Bool -> Int) -> Vector Bool -> Vector Bool -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Vector Bool -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length (Vector Bool -> Vector Bool -> Ordering)
-> (Vector Bool -> Vector Bool -> Ordering)
-> Vector Bool
-> Vector Bool
-> Ordering
forall a. Semigroup a => a -> a -> a
<> (Vector Bool -> Vector Bool)
-> Vector Bool -> Vector Bool -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Vector Bool -> Vector Bool
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 Vector Bool -> Vector Bool -> Vector Bool
forall a. Semigroup a => a -> a -> a
<> Vector Bool
hi)

instance Monoid BV where
  mempty :: BV
mempty = Vector Bool -> BV
BV Vector Bool
forall (v :: * -> *) a. Vector v a => v a
VG.empty

instance Show BV where
  show :: BV -> String
show BV
bv = String
"0b" String -> ShowS
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
(.&.) = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvand
  .|. :: BV -> BV -> BV
(.|.) = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvor
  xor :: BV -> BV -> BV
xor = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvxor
  complement :: BV -> BV
complement = BV -> BV
forall a. IsBV a => a -> a
bvnot

  shiftL :: BV -> Int -> BV
shiftL BV
x Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Int -> Int -> BV -> BV
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i) Int
0 BV
x BV -> BV -> BV
forall a. Semigroup a => a -> a -> a
<> Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
i Integer
0
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
w Integer
0
    where
      w :: Int
w = BV -> Int
forall a. IsBV a => a -> Int
width BV
x
  shiftR :: BV -> Int -> BV
shiftR BV
x Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
i Integer
0 BV -> BV -> BV
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> BV -> BV
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
i BV
x
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
w Integer
0
    where
      w :: Int
w = BV -> Int
forall a. IsBV a => a -> Int
width BV
x
  rotateL :: BV -> Int -> BV
rotateL BV
x Int
i
    | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = BV
x
    | Bool
otherwise = Int -> Int -> BV -> BV
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
j) Int
0 BV
x BV -> BV -> BV
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> BV -> BV
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
j) BV
x
    where
      w :: Int
w = BV -> Int
forall a. IsBV a => a -> Int
width BV
x
      j :: Int
j = Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
w
  rotateR :: BV -> Int -> BV
rotateR BV
x Int
i
    | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = BV
x
    | Bool
otherwise = Int -> Int -> BV -> BV
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
0 BV
x BV -> BV -> BV
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> BV -> BV
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
j BV
x
    where
      w :: Int
w = BV -> Int
forall a. IsBV a => a -> Int
width BV
x
      j :: Int
j = Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
w

  zeroBits :: BV
zeroBits = String -> BV
forall a. HasCallStack => String -> a
error String
"zeroBits is not implemented"

  bit :: Int -> BV
bit = String -> Int -> BV
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Vector Bool -> BV
BV (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ Vector Bool
bs Vector Bool -> [(Int, Bool)] -> Vector Bool
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 = BV -> Int
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Vector Bool -> BV
BV (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ Vector Bool
bs Vector Bool -> [(Int, Bool)] -> Vector Bool
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 = BV -> Int
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Vector Bool -> BV
BV (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ Vector Bool
bs Vector Bool -> [(Int, Bool)] -> Vector Bool
forall (v :: * -> *) a. Vector v a => v a -> [(Int, a)] -> v a
VG.// [(Int
i, Bool -> Bool
not (BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
x Int
i))]
    | Bool
otherwise = BV
x
    where
      w :: Int
w = BV -> Int
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Vector Bool
bs Vector Bool -> Int -> Bool
forall (v :: * -> *) a.
(HasCallStack, Vector v a) =>
v a -> Int -> a
VG.! Int
i
    | Bool
otherwise = Bool
False
    where
      w :: Int
w = BV -> Int
forall a. IsBV a => a -> Int
width BV
x

  popCount :: BV -> Int
popCount BV
x = [Int] -> Int
forall a. Num a => [a] -> a
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
_ = Maybe Int
forall a. Maybe a
Nothing
  bitSize :: BV -> Int
bitSize BV
_ = String -> Int
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) = Vector Bool -> Int
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 (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Bool -> Vector Bool
forall (v :: * -> *) a.
(HasCallStack, Vector v a) =>
Int -> Int -> v a -> v a
VG.slice Int
j (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Vector Bool
bs
  fromBV :: BV -> BV
fromBV = BV -> BV
forall a. a -> a
id

  bvnot :: BV -> BV
bvnot (BV Vector Bool
bs) = Vector Bool -> BV
BV (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool) -> Vector Bool -> Vector Bool
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)
    | Vector Bool -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Bool -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs2 = String -> BV
forall a. HasCallStack => String -> a
error String
"width mismatch"
    | Bool
otherwise = Vector Bool -> BV
BV (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool -> Bool) -> Vector Bool -> Vector Bool -> Vector Bool
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)
    | Vector Bool -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Bool -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs2 = String -> BV
forall a. HasCallStack => String -> a
error String
"width mismatch"
    | Bool
otherwise = Vector Bool -> BV
BV (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool -> Bool) -> Vector Bool -> Vector Bool -> Vector Bool
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)
    | Vector Bool -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Bool -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Bool
bs2 = String -> BV
forall a. HasCallStack => String -> a
error String
"width mismatch"
    | Bool
otherwise = Vector Bool -> BV
BV (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool -> Bool) -> Vector Bool -> Vector Bool -> Vector Bool
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
forall a. Eq a => a -> a -> Bool
(/=) Vector Bool
bs1 Vector Bool
bs2

  bvneg :: BV -> BV
bvneg BV
x = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ BV -> Int
forall a. IsBV a => a -> Int
width BV
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
x

  bvadd :: BV -> BV -> BV
bvadd BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) (BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
y)

  bvmul :: BV -> BV -> BV
bvmul BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) (BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
y)

  bvudiv :: BV -> BV -> BV
bvudiv BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = String -> BV
forall a. HasCallStack => String -> a
error String
"division by zero"
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) (BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
y')
    where
      y' :: Integer
      y' :: Integer
y' = BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
y

  bvurem :: BV -> BV -> BV
bvurem BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = String -> BV
forall a. HasCallStack => String -> a
error String
"division by zero"
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) (BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
y')
    where
      y' :: Integer
      y' :: Integer
y' = BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
y

  bvsdiv :: BV -> BV -> BV
bvsdiv BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvudiv BV
x BV
y
    | Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvudiv (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x) BV
y
    | Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvudiv BV
x (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y)
    | Bool
otherwise = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvudiv (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x) (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y)
    where
      msb_x :: Bool
msb_x = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
x (BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      msb_y :: Bool
msb_y = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
y (BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

  bvsrem :: BV -> BV -> BV
bvsrem BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvurem BV
x BV
y
    | Bool
msb_x Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
msb_y = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvurem (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x) BV
y
    | Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvurem BV
x (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y)
    | Bool
otherwise = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvurem (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x) (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y)
    where
      msb_x :: Bool
msb_x = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
x (BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      msb_y :: Bool
msb_y = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
y (BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

  bvsmod :: BV -> BV -> BV
bvsmod BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
u Integer -> Integer -> Bool
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 = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvadd (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
u) BV
y
    | Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvadd BV
u BV
y
    | Bool
otherwise = BV -> BV
forall a. IsBV a => a -> a
bvneg BV
u
    where
      msb_x :: Bool
msb_x = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
x (BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      msb_y :: Bool
msb_y = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
y (BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      abs_x :: BV
abs_x = if Bool
msb_x then BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x else BV
x
      abs_y :: BV
abs_y = if Bool
msb_y then BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y else BV
y
      u :: BV
u = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvurem BV
abs_x BV
abs_y

  bvshl :: BV -> BV -> BV
bvshl  BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) (BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` BV -> Int
forall a. Integral a => BV -> a
bv2nat BV
y)

  bvlshr :: BV -> BV -> BV
bvlshr BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) (BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` BV -> Int
forall a. Integral a => BV -> a
bv2nat BV
y)

  bvashr :: BV -> BV -> BV
bvashr BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Bool -> Bool
not Bool
msb_x = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvlshr BV
x BV
y
    | Bool
otherwise = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvlshr (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x) BV
y
    where
      msb_x :: Bool
msb_x = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
x (BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

  bvcomp :: BV -> BV -> BV
bvcomp BV
x BV
y
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
    | Bool
otherwise = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
1 (if BV
xBV -> BV -> Bool
forall a. Eq a => a -> a -> Bool
==BV
y then Integer
1 else Integer
0)

instance IsEqRel BV Bool where
  .==. :: BV -> BV -> Bool
(.==.) = BV -> BV -> Bool
forall a. Eq a => a -> a -> Bool
(==)
  ./=. :: BV -> BV -> 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 = BV -> BV -> Bool
BV -> BV -> ComparisonResult BV
forall a. Ord a => a -> a -> Bool
(<=)

  bvsle :: BV -> BV -> ComparisonResult BV
bvsle BV
bs1 BV
bs2
    | BV -> Int
forall a. IsBV a => a -> Int
width BV
bs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
bs2 = String -> Bool
forall a. HasCallStack => String -> a
error (String
"length mismatch: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (BV -> Int
forall a. IsBV a => a -> Int
width BV
bs1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (BV -> Int
forall a. IsBV a => a -> Int
width BV
bs2))
    | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Bool
ComparisonResult BV
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 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
bs2_msb) Bool -> Bool -> Bool
&& BV
bs1 BV -> BV -> Bool
forall a. Ord a => a -> a -> Bool
<= BV
bs2
    where
      w :: Int
w = BV -> Int
forall a. IsBV a => a -> Int
width BV
bs1
      bs1_msb :: Bool
bs1_msb = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
bs1 (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
      bs2_msb :: Bool
bs2_msb = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
bs2 (Int
wInt -> Int -> Int
forall 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) = (a -> Int -> Bool -> a) -> a -> Vector Bool -> a
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
ra -> a -> a
forall a. Num a => a -> a -> a
+a
2a -> Int -> a
forall 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 = BV -> a
forall a. IsBV a => BV -> a
fromBV (BV -> a) -> BV -> a
forall a b. (a -> b) -> a -> b
$ Vector Bool -> BV
BV (Vector Bool -> BV) -> Vector Bool -> BV
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Bool) -> Vector Bool
forall (v :: * -> *) a. Vector v a => Int -> (Int -> a) -> v a
VG.generate Int
m (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
x)

fromAscBits :: IsBV a => [Bool] -> a
fromAscBits :: forall a. IsBV a => [Bool] -> a
fromAscBits = BV -> a
forall a. IsBV a => BV -> a
fromBV (BV -> a) -> ([Bool] -> BV) -> [Bool] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Bool -> BV
BV (Vector Bool -> BV) -> ([Bool] -> Vector Bool) -> [Bool] -> BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> Vector Bool
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList

fromDescBits :: IsBV a => [Bool] -> a
fromDescBits :: forall a. IsBV a => [Bool] -> a
fromDescBits = BV -> a
forall a. IsBV a => BV -> a
fromBV (BV -> a) -> ([Bool] -> BV) -> [Bool] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> BV
forall a. IsBV a => [Bool] -> a
fromAscBits ([Bool] -> BV) -> ([Bool] -> [Bool]) -> [Bool] -> BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> [Bool]
forall a. [a] -> [a]
reverse

toAscBits :: BV -> [Bool]
toAscBits :: BV -> [Bool]
toAscBits (BV Vector Bool
bs) = Vector Bool -> [Bool]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Bool
bs

toDescBits :: BV -> [Bool]
toDescBits :: BV -> [Bool]
toDescBits = [Bool] -> [Bool]
forall a. [a] -> [a]
reverse ([Bool] -> [Bool]) -> (BV -> [Bool]) -> BV -> [Bool]
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
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
/= :: Var -> Var -> Bool
Eq, Eq Var
Eq Var =>
(Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord 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
$ccompare :: Var -> Var -> Ordering
compare :: Var -> Var -> Ordering
$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
>= :: Var -> Var -> Bool
$cmax :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
min :: Var -> Var -> Var
Ord, Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Var -> ShowS
showsPrec :: Int -> Var -> ShowS
$cshow :: Var -> String
show :: Var -> String
$cshowList :: [Var] -> ShowS
showList :: [Var] -> ShowS
Show)

data Expr
  = EConst BV
  | EVar Var
  | EOp1 Op1 Expr
  | EOp2 Op2 Expr Expr
  deriving (Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
/= :: Expr -> Expr -> Bool
Eq, Eq Expr
Eq Expr =>
(Expr -> Expr -> Ordering)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Expr)
-> (Expr -> Expr -> Expr)
-> Ord 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
$ccompare :: Expr -> Expr -> Ordering
compare :: Expr -> Expr -> Ordering
$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
>= :: Expr -> Expr -> Bool
$cmax :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
min :: Expr -> Expr -> Expr
Ord, Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Expr -> ShowS
showsPrec :: Int -> Expr -> ShowS
$cshow :: Expr -> String
show :: Expr -> String
$cshowList :: [Expr] -> ShowS
showList :: [Expr] -> ShowS
Show)

data Op1
  = OpExtract !Int !Int
  | OpNot
  | OpNeg
  deriving (Op1 -> Op1 -> Bool
(Op1 -> Op1 -> Bool) -> (Op1 -> Op1 -> Bool) -> Eq Op1
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Op1 -> Op1 -> Bool
== :: Op1 -> Op1 -> Bool
$c/= :: Op1 -> Op1 -> Bool
/= :: Op1 -> Op1 -> Bool
Eq, Eq Op1
Eq Op1 =>
(Op1 -> Op1 -> Ordering)
-> (Op1 -> Op1 -> Bool)
-> (Op1 -> Op1 -> Bool)
-> (Op1 -> Op1 -> Bool)
-> (Op1 -> Op1 -> Bool)
-> (Op1 -> Op1 -> Op1)
-> (Op1 -> Op1 -> Op1)
-> Ord 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
$ccompare :: Op1 -> Op1 -> Ordering
compare :: Op1 -> Op1 -> Ordering
$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
>= :: Op1 -> Op1 -> Bool
$cmax :: Op1 -> Op1 -> Op1
max :: Op1 -> Op1 -> Op1
$cmin :: Op1 -> Op1 -> Op1
min :: Op1 -> Op1 -> Op1
Ord, Int -> Op1 -> ShowS
[Op1] -> ShowS
Op1 -> String
(Int -> Op1 -> ShowS)
-> (Op1 -> String) -> ([Op1] -> ShowS) -> Show Op1
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Op1 -> ShowS
showsPrec :: Int -> Op1 -> ShowS
$cshow :: Op1 -> String
show :: Op1 -> String
$cshowList :: [Op1] -> ShowS
showList :: [Op1] -> ShowS
Show)

data Op2
  = OpConcat
  | OpAnd
  | OpOr
  | OpXOr
  | OpComp
  | OpAdd
  | OpMul
  | OpUDiv
  | OpURem
  | OpSDiv
  | OpSRem
  | OpSMod
  | OpShl
  | OpLShr
  | OpAShr
  deriving (Op2 -> Op2 -> Bool
(Op2 -> Op2 -> Bool) -> (Op2 -> Op2 -> Bool) -> Eq Op2
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Op2 -> Op2 -> Bool
== :: Op2 -> Op2 -> Bool
$c/= :: Op2 -> Op2 -> Bool
/= :: Op2 -> Op2 -> Bool
Eq, Eq Op2
Eq Op2 =>
(Op2 -> Op2 -> Ordering)
-> (Op2 -> Op2 -> Bool)
-> (Op2 -> Op2 -> Bool)
-> (Op2 -> Op2 -> Bool)
-> (Op2 -> Op2 -> Bool)
-> (Op2 -> Op2 -> Op2)
-> (Op2 -> Op2 -> Op2)
-> Ord 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
$ccompare :: Op2 -> Op2 -> Ordering
compare :: Op2 -> Op2 -> Ordering
$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
>= :: Op2 -> Op2 -> Bool
$cmax :: Op2 -> Op2 -> Op2
max :: Op2 -> Op2 -> Op2
$cmin :: Op2 -> Op2 -> Op2
min :: Op2 -> Op2 -> Op2
Ord, Int -> Op2
Op2 -> Int
Op2 -> [Op2]
Op2 -> Op2
Op2 -> Op2 -> [Op2]
Op2 -> Op2 -> Op2 -> [Op2]
(Op2 -> Op2)
-> (Op2 -> Op2)
-> (Int -> Op2)
-> (Op2 -> Int)
-> (Op2 -> [Op2])
-> (Op2 -> Op2 -> [Op2])
-> (Op2 -> Op2 -> [Op2])
-> (Op2 -> Op2 -> Op2 -> [Op2])
-> Enum 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
$csucc :: Op2 -> Op2
succ :: Op2 -> Op2
$cpred :: Op2 -> Op2
pred :: Op2 -> Op2
$ctoEnum :: Int -> Op2
toEnum :: Int -> Op2
$cfromEnum :: Op2 -> Int
fromEnum :: Op2 -> Int
$cenumFrom :: Op2 -> [Op2]
enumFrom :: Op2 -> [Op2]
$cenumFromThen :: Op2 -> Op2 -> [Op2]
enumFromThen :: Op2 -> Op2 -> [Op2]
$cenumFromTo :: Op2 -> Op2 -> [Op2]
enumFromTo :: Op2 -> Op2 -> [Op2]
$cenumFromThenTo :: Op2 -> Op2 -> Op2 -> [Op2]
enumFromThenTo :: Op2 -> Op2 -> Op2 -> [Op2]
Enum, Op2
Op2 -> Op2 -> Bounded Op2
forall a. a -> a -> Bounded a
$cminBound :: Op2
minBound :: Op2
$cmaxBound :: Op2
maxBound :: Op2
Bounded, Int -> Op2 -> ShowS
[Op2] -> ShowS
Op2 -> String
(Int -> Op2 -> ShowS)
-> (Op2 -> String) -> ([Op2] -> ShowS) -> Show Op2
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Op2 -> ShowS
showsPrec :: Int -> Op2 -> ShowS
$cshow :: Op2 -> String
show :: Op2 -> String
$cshowList :: [Op2] -> ShowS
showList :: [Op2] -> ShowS
Show)

instance IsBV Expr where
  width :: Expr -> Int
width (EConst BV
x) = BV -> Int
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
      Op1
_ -> Expr -> Int
forall a. IsBV a => a -> Int
width Expr
arg
  width (EOp2 Op2
op Expr
arg1 Expr
arg2) =
    case Op2
op of
      Op2
OpConcat -> Expr -> Int
forall a. IsBV a => a -> Int
width Expr
arg1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Expr -> Int
forall a. IsBV a => a -> Int
width Expr
arg2
      Op2
OpComp -> Int
1
      Op2
_ -> Expr -> Int
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 BV
forall a. Monoid a => a
mempty

instance Bits Expr where
  .&. :: Expr -> Expr -> Expr
(.&.) = Expr -> Expr -> Expr
forall a. IsBV a => a -> a -> a
bvand
  .|. :: Expr -> Expr -> Expr
(.|.) = Expr -> Expr -> Expr
forall a. IsBV a => a -> a -> a
bvor
  xor :: Expr -> Expr -> Expr
xor = Expr -> Expr -> Expr
forall a. IsBV a => a -> a -> a
bvxor
  complement :: Expr -> Expr
complement = Expr -> Expr
forall a. IsBV a => a -> a
bvnot
  shiftL :: Expr -> Int -> Expr
shiftL Expr
x Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i) Int
0 Expr
x Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> Int -> Integer -> Expr
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
i Integer
0
    | Bool
otherwise = Int -> Integer -> Expr
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
w Integer
0
    where
      w :: Int
w = Expr -> Int
forall a. IsBV a => a -> Int
width Expr
x
  shiftR :: Expr -> Int -> Expr
shiftR Expr
x Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Int -> Integer -> Expr
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
i Integer
0 Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
i Expr
x
    | Bool
otherwise = Int -> Integer -> Expr
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
w Integer
0
    where
      w :: Int
w = Expr -> Int
forall a. IsBV a => a -> Int
width Expr
x
  rotateL :: Expr -> Int -> Expr
rotateL Expr
x Int
i
    | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Expr
x
    | Bool
otherwise = Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
j) Int
0 Expr
x Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
j) Expr
x
    where
      w :: Int
w = Expr -> Int
forall a. IsBV a => a -> Int
width Expr
x
      j :: Int
j = Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
w
  rotateR :: Expr -> Int -> Expr
rotateR Expr
x Int
i
    | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Expr
x
    | Bool
otherwise = Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
0 Expr
x Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
j Expr
x
    where
      w :: Int
w = Expr -> Int
forall a. IsBV a => a -> Int
width Expr
x
      j :: Int
j = Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
w

  zeroBits :: Expr
zeroBits = String -> Expr
forall a. HasCallStack => String -> a
error String
"zeroBits is not implemented"

  bit :: Int -> Expr
bit = String -> Int -> Expr
forall a. HasCallStack => String -> a
error String
"bit is not implemented"

  setBit :: Expr -> Int -> Expr
setBit Expr
x Int
i
    | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Expr
x Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> [Bool] -> Expr
forall a. IsBV a => [Bool] -> a
fromDescBits [Bool
True] Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
0 Expr
x
    | Bool
otherwise = Expr
x
    where
      w :: Int
w = Expr -> Int
forall a. IsBV a => a -> Int
width Expr
x

  clearBit :: Expr -> Int -> Expr
clearBit Expr
x Int
i
    | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Expr
x Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> [Bool] -> Expr
forall a. IsBV a => [Bool] -> a
fromDescBits [Bool
False] Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
0 Expr
x
    | Bool
otherwise = Expr
x
    where
      w :: Int
w = Expr -> Int
forall a. IsBV a => a -> Int
width Expr
x

  complementBit :: Expr -> Int -> Expr
complementBit Expr
x Int
i
    | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
w = Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Expr
x Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> Expr -> Expr
forall a. IsBV a => a -> a
bvnot (Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract Int
i Int
i Expr
x) Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
<> Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
extract (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
0 Expr
x
    | Bool
otherwise = Expr
x
    where
      w :: Int
w = Expr -> Int
forall a. IsBV a => a -> Int
width Expr
x

  testBit :: Expr -> Int -> Bool
testBit = String -> Expr -> Int -> Bool
forall a. HasCallStack => String -> a
error String
"testBit is not implemented"

  popCount :: Expr -> Int
popCount = String -> Expr -> Int
forall a. HasCallStack => String -> a
error String
"popCount is not implemented"

  bitSizeMaybe :: Expr -> Maybe Int
bitSizeMaybe Expr
_ = Maybe Int
forall a. Maybe a
Nothing
  bitSize :: Expr -> Int
bitSize Expr
_ = String -> Int
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
(Atom -> Atom -> Bool) -> (Atom -> Atom -> Bool) -> Eq Atom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
/= :: Atom -> Atom -> Bool
Eq, Eq Atom
Eq Atom =>
(Atom -> Atom -> Ordering)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Atom)
-> (Atom -> Atom -> Atom)
-> Ord 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
$ccompare :: Atom -> Atom -> Ordering
compare :: Atom -> Atom -> Ordering
$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
>= :: Atom -> Atom -> Bool
$cmax :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
min :: Atom -> Atom -> Atom
Ord, Int -> Atom -> ShowS
[Atom] -> ShowS
Atom -> String
(Int -> Atom -> ShowS)
-> (Atom -> String) -> ([Atom] -> ShowS) -> Show Atom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Atom -> ShowS
showsPrec :: Int -> Atom -> ShowS
$cshow :: Atom -> String
show :: Atom -> String
$cshowList :: [Atom] -> ShowS
showList :: [Atom] -> ShowS
Show)

instance Complement Atom where
  notB :: Atom -> Atom
notB (Rel OrdRel Expr
rel Bool
signed) = OrdRel Expr -> Bool -> Atom
Rel (OrdRel Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Expr -> Expr -> OrdRel Expr
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 Vector BV -> Int -> BV
forall (v :: * -> *) a.
(HasCallStack, Vector v a) =>
v a -> Int -> a
VG.! Var -> Int
varId Var
v
    f (EOp1 Op1
op Expr
x) = Op1 -> BV -> BV
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) = Int -> Int -> a -> a
forall a. IsBV a => Int -> Int -> a -> a
extract Int
i Int
j
    evalOp1 Op1
OpNot = a -> a
forall a. IsBV a => a -> a
bvnot
    evalOp1 Op1
OpNeg = a -> a
forall a. IsBV a => a -> a
bvneg

    evalOp2 :: Op2 -> BV -> BV -> BV
evalOp2 Op2
OpConcat BV
a BV
b = BV
a BV -> BV -> BV
forall a. Semigroup a => a -> a -> a
<> BV
b
    evalOp2 Op2
OpAnd BV
x BV
y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvand BV
x BV
y
    evalOp2 Op2
OpOr BV
x BV
y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvor BV
x BV
y
    evalOp2 Op2
OpXOr BV
x BV
y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvxor BV
x BV
y
    evalOp2 Op2
OpAdd BV
x BV
y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvadd BV
x BV
y
    evalOp2 Op2
OpMul BV
x BV
y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvmul BV
x BV
y
    evalOp2 Op2
OpUDiv BV
x BV
y
      | Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvudiv BV
x BV
y
      | Bool
otherwise =
          case BV -> Map BV BV -> Maybe BV
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 -> Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) Integer
0
      where
        y' :: Integer
        y' :: Integer
y' = BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
y
    evalOp2 Op2
OpURem BV
x BV
y
      | Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvurem BV
x BV
y
      | Bool
otherwise =
          case BV -> Map BV BV -> Maybe BV
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 -> Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv (BV -> Int
forall a. IsBV a => a -> Int
width BV
x) Integer
0
      where
        y' :: Integer
        y' :: Integer
y' = BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
y
    evalOp2 Op2
OpSDiv BV
x BV
y
      | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
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 = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ Op2 -> BV -> BV -> BV
evalOp2 Op2
OpUDiv (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x) BV
y
      | Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ Op2 -> BV -> BV -> BV
evalOp2 Op2
OpUDiv BV
x (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y)
      | Bool
otherwise = Op2 -> BV -> BV -> BV
evalOp2 Op2
OpUDiv (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x) (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y)
      where
        msb_x :: Bool
msb_x = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
x (BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        msb_y :: Bool
msb_y = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
y (BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
    evalOp2 Op2
OpSRem BV
x BV
y
      | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
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 = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ Op2 -> BV -> BV -> BV
evalOp2 Op2
OpURem (BV -> BV
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 (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y)
      | Bool
otherwise = BV -> BV
forall a. IsBV a => a -> a
bvneg (BV -> BV) -> BV -> BV
forall a b. (a -> b) -> a -> b
$ Op2 -> BV -> BV -> BV
evalOp2 Op2
OpURem (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x) (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
y)
      where
        msb_x :: Bool
msb_x = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
x (BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        msb_y :: Bool
msb_y = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
y (BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
    evalOp2 Op2
OpSMod BV
x BV
y
      | BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= BV -> Int
forall a. IsBV a => a -> Int
width BV
y = String -> BV
forall a. HasCallStack => String -> a
error String
"invalid width"
      | BV -> Integer
forall a. Integral a => BV -> a
bv2nat BV
u Integer -> Integer -> Bool
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 = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvadd (BV -> BV
forall a. IsBV a => a -> a
bvneg BV
u) BV
y
      | Bool -> Bool
not Bool
msb_x Bool -> Bool -> Bool
&& Bool
msb_y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvadd BV
u BV
y
      | Bool
otherwise = BV -> BV
forall a. IsBV a => a -> a
bvneg BV
u
      where
        msb_x :: Bool
msb_x = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
x (BV -> Int
forall a. IsBV a => a -> Int
width BV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        msb_y :: Bool
msb_y = BV -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit BV
y (BV -> Int
forall a. IsBV a => a -> Int
width BV
y Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        abs_x :: BV
abs_x = if Bool
msb_x then BV -> BV
forall a. IsBV a => a -> a
bvneg BV
x else BV
x
        abs_y :: BV
abs_y = if Bool
msb_y then BV -> BV
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 = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvshl BV
x BV
y
    evalOp2 Op2
OpLShr BV
x BV
y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvlshr BV
x BV
y
    evalOp2 Op2
OpAShr BV
x BV
y = BV -> BV -> BV
forall a. IsBV a => a -> a -> a
bvashr BV
x BV
y
    evalOp2 Op2
OpComp BV
x BV
y = Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
1 (if BV
xBV -> BV -> Bool
forall 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) = RelOp -> BV -> BV -> Bool
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 -> BV -> BV -> ComparisonResult BV
forall a. BVComparison a => a -> a -> ComparisonResult a
bvslt BV
lhs' BV
rhs'
    RelOp
Gt -> BV -> BV -> ComparisonResult BV
forall a. BVComparison a => a -> a -> ComparisonResult a
bvslt BV
rhs' BV
lhs'
    RelOp
Le -> BV -> BV -> ComparisonResult BV
forall a. BVComparison a => a -> a -> ComparisonResult a
bvsle BV
lhs' BV
rhs'
    RelOp
Ge -> BV -> BV -> ComparisonResult BV
forall a. BVComparison a => a -> a -> ComparisonResult a
bvsle BV
rhs' BV
lhs'
    RelOp
Eql -> BV
lhs' BV -> BV -> Bool
forall a. Eq a => a -> a -> Bool
== BV
rhs'
    RelOp
NEq -> BV
lhs' BV -> BV -> Bool
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