{-|
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
[Domain w] -> ShowS
Domain w -> String
(Int -> Domain w -> ShowS)
-> (Domain w -> String) -> ([Domain w] -> ShowS) -> Show (Domain w)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (w :: Nat). Int -> Domain w -> ShowS
forall (w :: Nat). [Domain w] -> ShowS
forall (w :: Nat). Domain w -> String
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 :: NatRepr w -> Domain w -> Bool
proper NatRepr w
w (BVDXor Integer
mask Integer
val Integer
u) =
  Integer
mask Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> Integer
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 :: Domain w -> Integer -> Bool
member (BVDXor Integer
mask Integer
hi Integer
unknown) Integer
x = Integer
hi Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
unknown

-- | Return the bitvector mask value from this domain
bvdMask :: Domain w -> Integer
bvdMask :: 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 :: NatRepr w -> Integer -> Integer -> Domain w
range NatRepr w
w Integer
lo Integer
hi = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo' Integer
hi'
  where
  lo' :: Integer
lo'  = Integer
lo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
  hi' :: Integer
hi'  = Integer
hi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask
  mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w

-- | Unsafe constructor for internal use.
interval :: Integer -> Integer -> Integer -> Domain w
interval :: Integer -> Integer -> Integer -> Domain w
interval Integer
mask Integer
lo Integer
hi = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask Integer
hi (Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
Bits.xor Integer
lo Integer
hi)

-- | Bitwise lower and upper bounds
bitbounds :: Domain w -> (Integer, Integer)
bitbounds :: Domain w -> (Integer, Integer)
bitbounds (BVDXor Integer
_ Integer
hi Integer
u) = (Integer -> Integer -> Integer
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 :: Domain w -> Maybe Integer
asSingleton (BVDXor Integer
_ Integer
hi Integer
u) = if Integer
u Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
hi else Maybe Integer
forall a. Maybe a
Nothing

-- | Random generator for domain values.  We always generate
--   nonempty domain values.
genDomain :: NatRepr w -> Gen (Domain w)
genDomain :: NatRepr w -> Gen (Domain w)
genDomain NatRepr w
w =
  do let mask :: Integer
mask = NatRepr w -> Integer
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)
     Domain w -> Gen (Domain w)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Domain w -> Gen (Domain w)) -> Domain w -> Gen (Domain w)
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask (Integer
val Integer -> Integer -> Integer
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 :: Domain w -> Gen Integer
genElement (BVDXor Integer
_mask Integer
v Integer
u) =
   do Integer
x <- (Integer, Integer) -> Gen Integer
chooseInteger (Integer
0, Int -> Integer
forall a. Bits a => Int -> a
bit Int
bs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
      Integer -> Gen Integer
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer -> Gen Integer) -> Integer -> Gen Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Int -> Integer
stripe Integer
lo Integer
x Int
0

  where
  lo :: Integer
lo = Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
u
  bs :: Int
bs = Integer -> Int
forall a. Bits a => a -> Int
Bits.popCount Integer
u
  stripe :: Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x Int
i
   | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer
val
   | Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
u Int
i =
       let val' :: Integer
val' = if Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x Int
0 then Integer -> Int -> Integer
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 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
   | Bool
otherwise = Integer -> Integer -> Int -> Integer
stripe Integer
val Integer
x (Int
iInt -> Int -> Int
forall 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 :: NatRepr w -> Gen (Domain w, Integer)
genPair NatRepr w
w =
  do Domain w
a <- NatRepr w -> Gen (Domain w)
forall (w :: Nat). NatRepr w -> Gen (Domain w)
genDomain NatRepr w
w
     Integer
x <- Domain w -> Gen Integer
forall (w :: Nat). Domain w -> Gen Integer
genElement Domain w
a
     (Domain w, Integer) -> Gen (Domain w, Integer)
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 :: NatRepr w -> Integer -> Domain w
singleton NatRepr w
w Integer
x = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask) Integer
0
  where
  mask :: Integer
mask = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w

xor :: Domain w -> Domain w -> Domain w
xor :: Domain w -> Domain w -> Domain w
xor (BVDXor Integer
mask Integer
va Integer
ua) (BVDXor Integer
_ Integer
vb Integer
ub) = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
u) Integer
u
  where
  v :: Integer
v = Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
Bits.xor Integer
va Integer
vb
  u :: Integer
u = Integer
ua Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
ub

and :: Domain w -> Domain w -> Domain w
and :: Domain w -> Domain w -> Domain w
and (BVDXor Integer
mask Integer
va Integer
ua) (BVDXor Integer
_ Integer
vb Integer
ub) = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask Integer
v (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
u)
  where
  v :: Integer
v = Integer
va Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
vb
  u :: Integer
u = Integer
ua Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
ub

and_scalar :: Integer -> Domain w -> Domain w
and_scalar :: Integer -> Domain w -> Domain w
and_scalar Integer
x (BVDXor Integer
mask Integer
va Integer
ua) = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
BVDXor Integer
mask (Integer
va Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
x) (Integer
ua Integer -> Integer -> Integer
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 :: NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n Domain n
a Integer
x = NatRepr n -> Domain n -> Bool
forall (w :: Nat). NatRepr w -> Domain w -> Bool
proper NatRepr n
n Domain n
a Bool -> Bool -> Bool
&& Domain n -> Integer -> 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 :: NatRepr n -> Integer -> Integer -> Property
correct_singleton NatRepr n
n Integer
x Integer
y = Bool -> Property
property (NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> Integer -> Domain n
forall (w :: Nat). NatRepr w -> Integer -> Domain w
singleton NatRepr n
n Integer
x') Integer
y' Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
x' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y'))
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
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 :: NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_xor NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
xor Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
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 :: NatRepr n -> (Domain n, Integer) -> (Domain n, Integer) -> Property
correct_and NatRepr n
n (Domain n
a,Integer
x) (Domain n
b,Integer
y) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (Domain n -> Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w -> Domain w
and Domain n
a Domain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
y)

correct_and_scalar :: (1 <= n) => NatRepr n -> Integer -> (Domain n, Integer) -> Property
correct_and_scalar :: NatRepr n -> Integer -> (Domain n, Integer) -> Property
correct_and_scalar NatRepr n
n Integer
y (Domain n
a,Integer
x) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> Domain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> Domain n -> Integer -> Bool
pmember NatRepr n
n (Integer -> Domain n -> Domain n
forall (w :: Nat). Integer -> Domain w -> Domain w
and_scalar Integer
y Domain n
a) (Integer
y Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
x)

bitle :: Integer -> Integer -> Bool
bitle :: Integer -> Integer -> Bool
bitle Integer
x Integer
y = (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
y) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y

correct_bitbounds :: Domain n -> Integer -> Property
correct_bitbounds :: Domain n -> Integer -> Property
correct_bitbounds Domain n
a Integer
x = Bool -> Property
property (Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
member Domain n
a Integer
x Bool -> Bool -> Bool
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) = Domain n -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
bitbounds Domain n
a