    {-|
    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 (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
    $cshowsPrec :: forall (w :: Nat). Int -> Domain w -> ShowS
    showsPrec :: Int -> Domain w -> ShowS
    $cshow :: forall (w :: Nat). Domain w -> String
    show :: Domain w -> String
    $cshowList :: forall (w :: Nat). [Domain w] -> ShowS
    showList :: [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 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 :: forall (w :: Nat). 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 :: 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 = 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 a. a -> Gen a
    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 :: 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, 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 a. a -> Gen a
    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 :: forall (w :: Nat). 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 a. a -> Gen 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 = 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 :: forall (n :: Nat). 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 :: forall (n :: Nat).
    (1 <= n) =>
    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 :: 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) = 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 :: 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) = 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 :: 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) = 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 :: forall (n :: Nat). 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