{-|
Module      : What4.Utils.BVDomain.XOR
Copyright   : (c) Galois Inc, 2019-2020
License     : BSD3
Maintainer  : huffman@galois.com

Provides an implementation of bitvector abstract domains
optimized for performing XOR operations.
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module What4.Utils.BVDomain.XOR
  ( -- * XOR Domains
    Domain(..)
  , proper
  , bvdMask
  , member
  , pmember
  , range
  , interval
  , bitbounds
  , asSingleton
    -- ** Operations
  , singleton
  , xor
  , and
  , and_scalar

    -- * Correctness properties
  , 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 )

-- | A value of type @'BVDomain' w@ represents a set of bitvectors of
-- width @w@.  This is an alternate representation of the bitwise
-- domain values, optimized to compute XOR operations.
data Domain (w :: Nat) =
    BVDXor !Integer !Integer !Integer
    -- ^ @BVDXor mask hi unknown@ represents a set of values where
    --   @hi@ is a bitwise high bound, and @unknown@ represents
    --   the bits whose values are not known.  The value @mask@
    --   caches the value @2^w-1@.
  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)

-- | Test if the domain satisfies its invariants
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

-- | Test if the given integer value is a member of the abstract domain
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

-- | Return the bitvector mask value from this domain
bvdMask :: Domain w -> Integer
bvdMask :: forall (w :: Nat). Domain w -> Integer
bvdMask (BVDXor Integer
mask Integer
_ Integer
_) = Integer
mask

-- | Construct a domain from bitwise lower and upper bounds
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

-- | Unsafe constructor for internal use.
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)

-- | Bitwise lower and upper bounds
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)

-- | Test if this domain contains a single value, and return it if so
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

-- | Random generator for domain values.  We always generate
--   nonempty domain values.
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

-- This generator goes to some pains to try
-- to generate a good statistical distribution
-- of the values in the domain.  It only choses
-- random bits for the "unknown" values of
-- the domain, then stripes them out among
-- the unknown bit positions.
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)

-- | Generate a random nonempty domain and an element
--   contained in that domain.
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)

-- | Return a domain containing just the given value
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)

-----------------------------------------------------------------------
-- Correctness properties

-- | Check that a domain is proper, and that
--   the given value is a member
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