{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module What4.Utils.BVDomain.XOR
(
Domain(..)
, proper
, bvdMask
, member
, pmember
, range
, interval
, bitbounds
, asSingleton
, singleton
, xor
, and
, and_scalar
, genDomain
, genElement
, genPair
, correct_singleton
, correct_xor
, correct_and
, correct_and_scalar
, correct_bitbounds
) where
import qualified Data.Bits as Bits
import Data.Bits hiding (testBit, xor)
import Data.Parameterized.NatRepr
import GHC.TypeNats
import Prelude hiding (any, concat, negate, and, or, not)
import Test.Verification ( Property, property, (==>), Gen, chooseInteger )
data Domain (w :: Nat) =
BVDXor !Integer !Integer !Integer
deriving (Int -> Domain w -> ShowS
forall (w :: Nat). Int -> Domain w -> ShowS
forall (w :: Nat). [Domain w] -> ShowS
forall (w :: Nat). Domain w -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Domain w] -> ShowS
$cshowList :: forall (w :: Nat). [Domain w] -> ShowS
show :: Domain w -> String
$cshow :: forall (w :: Nat). Domain w -> String
showsPrec :: Int -> Domain w -> ShowS
$cshowsPrec :: forall (w :: Nat). Int -> Domain w -> ShowS
Show)
proper :: NatRepr w -> Domain w -> Bool
proper :: forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr w
w (BVDXor Integer
mask Integer
val Integer
u) =
Integer
mask forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w Bool -> Bool -> Bool
&&
Integer -> Integer -> Bool
bitle Integer
val Integer
mask Bool -> Bool -> Bool
&&
Integer -> Integer -> Bool
bitle Integer
u Integer
mask Bool -> Bool -> Bool
&&
Integer -> Integer -> Bool
bitle Integer
u Integer
val
member :: Domain w -> Integer -> Bool
member :: forall (w :: Nat). Domain w -> Integer -> Bool
member (BVDXor Integer
mask Integer
hi Integer
unknown) Integer
x = Integer
hi forall a. Eq a => a -> a -> Bool
== (Integer
x forall a. Bits a => a -> a -> a
.&. Integer
mask) forall a. Bits a => a -> a -> a
.|. Integer
unknown
bvdMask :: Domain w -> Integer
bvdMask :: forall (w :: Nat). Domain w -> Integer
bvdMask (BVDXor Integer
mask Integer
_ Integer
_) = Integer
mask
range :: NatRepr w -> Integer -> Integer -> Domain w
range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
lo Integer
hi = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo' Integer
hi'
where
lo' :: Integer
lo' = Integer
lo forall a. Bits a => a -> a -> a
.&. Integer
mask
hi' :: Integer
hi' = Integer
hi forall a. Bits a => a -> a -> a
.&. Integer
mask
mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
interval :: Integer -> Integer -> Integer -> Domain w
interval :: forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo Integer
hi = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask Integer
hi (forall a. Bits a => a -> a -> a
Bits.xor Integer
lo Integer
hi)
bitbounds :: Domain w -> (Integer, Integer)
bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds (BVDXor Integer
_ Integer
hi Integer
u) = (forall a. Bits a => a -> a -> a
Bits.xor Integer
u Integer
hi, Integer
hi)
asSingleton :: Domain w -> Maybe Integer
asSingleton :: forall (w :: Nat). Domain w -> Maybe Integer
asSingleton (BVDXor Integer
_ Integer
hi Integer
u) = if Integer
u forall a. Eq a => a -> a -> Bool
== Integer
0 then forall a. a -> Maybe a
Just Integer
hi else forall a. Maybe a
Nothing
genDomain :: NatRepr w -> Gen (Domain w)
genDomain :: forall (w :: Nat). NatRepr w -> Gen (Domain w)
genDomain NatRepr w
w =
do let mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
Integer
val <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
mask)
Integer
u <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Integer
mask)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask (Integer
val forall a. Bits a => a -> a -> a
.|. Integer
u) Integer
u
genElement :: Domain w -> Gen Integer
genElement :: forall (w :: Nat). Domain w -> Gen Integer
genElement (BVDXor Integer
_mask Integer
v Integer
u) =
do Integer
x <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, forall a. Bits a => Int -> a
bit Int
bs forall a. Num a => a -> a -> a
- Integer
1)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Int -> Integer
stripe Integer
lo Integer
x Int
0
where
lo :: Integer
lo = Integer
v forall a. Bits a => a -> a -> a
`Bits.xor` Integer
u
bs :: Int
bs = forall a. Bits a => a -> Int
Bits.popCount Integer
u
stripe :: Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x Int
i
| Integer
x forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer
val
| forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
u Int
i =
let val' :: Integer
val' = if forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x Int
0 then forall a. Bits a => a -> Int -> a
setBit Integer
val Int
i else Integer
val in
Integer -> Integer -> Int -> Integer
stripe Integer
val' (Integer
x forall a. Bits a => a -> Int -> a
`shiftR` Int
1) (Int
iforall a. Num a => a -> a -> a
+Int
1)
| Bool
otherwise = Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x (Int
iforall a. Num a => a -> a -> a
+Int
1)
genPair :: NatRepr w -> Gen (Domain w, Integer)
genPair :: forall (w :: Nat). NatRepr w -> Gen (Domain w, Integer)
genPair NatRepr w
w =
do Domain w
a <- forall (w :: Nat). NatRepr w -> Gen (Domain w)
genDomain NatRepr w
w
Integer
x <- forall (w :: Nat). Domain w -> Gen Integer
genElement Domain w
a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Domain w
a,Integer
x)
singleton :: NatRepr w -> Integer -> Domain w
singleton :: forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
x = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask (Integer
x forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
0
where
mask :: Integer
mask = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
xor :: Domain w -> Domain w -> Domain w
xor :: forall (w :: Nat). Domain w -> Domain w -> Domain w
xor (BVDXor Integer
mask Integer
va Integer
ua) (BVDXor Integer
_ Integer
vb Integer
ub) = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask (Integer
v forall a. Bits a => a -> a -> a
.|. Integer
u) Integer
u
where
v :: Integer
v = forall a. Bits a => a -> a -> a
Bits.xor Integer
va Integer
vb
u :: Integer
u = Integer
ua forall a. Bits a => a -> a -> a
.|. Integer
ub
and :: Domain w -> Domain w -> Domain w
and :: forall (w :: Nat). Domain w -> Domain w -> Domain w
and (BVDXor Integer
mask Integer
va Integer
ua) (BVDXor Integer
_ Integer
vb Integer
ub) = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask Integer
v (Integer
v forall a. Bits a => a -> a -> a
.&. Integer
u)
where
v :: Integer
v = Integer
va forall a. Bits a => a -> a -> a
.&. Integer
vb
u :: Integer
u = Integer
ua forall a. Bits a => a -> a -> a
.|. Integer
ub
and_scalar :: Integer -> Domain w -> Domain w
and_scalar :: forall (w :: Nat). Integer -> Domain w -> Domain w
and_scalar Integer
x (BVDXor Integer
mask Integer
va Integer
ua) = forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask (Integer
va forall a. Bits a => a -> a -> a
.&. Integer
x) (Integer
ua forall a. Bits a => a -> a -> a
.&. Integer
x)
pmember :: NatRepr n -> Domain n -> Integer -> Bool
pmember :: forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n Domain n
a Integer
x = forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr n
n Domain n
a Bool -> Bool -> Bool
&& forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x
correct_singleton :: (1 <= n) => NatRepr n -> Integer -> Integer -> Property
correct_singleton :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Integer -> Integer -> Property
correct_singleton NatRepr n
n Integer
x Integer
y = Bool -> Property
property (forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr n
n Integer
x') Integer
y' forall a. Eq a => a -> a -> Bool
== (Integer
x' forall a. Eq a => a -> a -> Bool
== Integer
y'))
where
x' :: Integer
x' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
y' :: Integer
y' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
correct_xor :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_xor :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_xor NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w -> Domain w
xor Domain n
a Domain n
b) (Integer
x forall a. Bits a => a -> a -> a
`Bits.xor` Integer
y)
correct_and :: (1 <= n) => NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Domain w -> Domain w -> Domain w
and Domain n
a Domain n
b) (Integer
x forall a. Bits a => a -> a -> a
.&. Integer
y)
correct_and_scalar :: (1 <= n) => NatRepr n -> Integer -> (Domain n, Integer) -> Property
correct_and_scalar :: forall (n :: Nat).
(1 <= n) =>
NatRepr n -> Integer -> (Domain n, Integer) -> Property
correct_and_scalar NatRepr n
n Integer
y (Domain n
a,Integer
x) = forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall t. Verifiable t => Bool -> t -> Property
==> forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (forall (w :: Nat). Integer -> Domain w -> Domain w
and_scalar Integer
y Domain n
a) (Integer
y forall a. Bits a => a -> a -> a
.&. Integer
x)
bitle :: Integer -> Integer -> Bool
bitle :: Integer -> Integer -> Bool
bitle Integer
x Integer
y = (Integer
x forall a. Bits a => a -> a -> a
.|. Integer
y) forall a. Eq a => a -> a -> Bool
== Integer
y
correct_bitbounds :: Domain n -> Integer -> Property
correct_bitbounds :: forall (n :: Nat). Domain n -> Integer -> Property
correct_bitbounds Domain n
a Integer
x = Bool -> Property
property (forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x forall a. Eq a => a -> a -> Bool
== (Integer -> Integer -> Bool
bitle Integer
lo Integer
x Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
bitle Integer
x Integer
hi))
where
(Integer
lo,Integer
hi) = forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain n
a