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

Provides an implementation of abstract domains for bitvectors.
This abstract domain has essentially two modes: arithmetic
and bitvector modes. The arithmetic mode is a fairly straightforward
interval domain, albeit one that is carefully implemented to deal
properly with intervals that "cross zero", as is relatively common
when using 2's complement signed representations. The bitwise
mode tracks the values of individual bits independently in a
3-valued logic (true, false or unknown).  The abstract domain
transitions between the two modes when necessary, but attempts
to retain as much precision as possible.

The operations of these domains are formalized in the companion
Cryptol files found together in this package under the \"doc\"
directory, and their soundness properties stated and established.
-}

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

module What4.Utils.BVDomain
  ( -- * Bitvector abstract domains
    BVDomain(..)
  , proper
  , member
  , size
    -- ** Domain transfer functions
  , asArithDomain
  , asBitwiseDomain
  , asXorDomain
  , fromXorDomain
  , arithToXorDomain
  , bitwiseToXorDomain
  , xorToBitwiseDomain
    -- ** Projection functions
  , asSingleton
  , eq
  , slt
  , ult
  , testBit
  , domainsOverlap
  , ubounds
  , sbounds
  , A.arithDomainData
  , B.bitbounds
    -- * Operations
  , any
  , singleton
  , range
  , fromAscEltList
  , union
  , concat
  , select
  , zext
  , sext
    -- ** Shifts and rotates
  , shl
  , lshr
  , ashr
  , rol
  , ror
    -- ** Arithmetic
  , add
  , negate
  , scale
  , mul
  , udiv
  , urem
  , sdiv
  , srem
    -- ** Bitwise
  , What4.Utils.BVDomain.not
  , and
  , or
  , xor

    -- ** Misc
  , popcnt
  , clz
  , ctz

    -- * Useful bitvector computations
  , bitwiseRoundAbove
  , bitwiseRoundBetween

    -- * Correctness properties
  , genDomain
  , genElement
  , genPair

  , correct_arithToBitwise
  , correct_bitwiseToArith
  , correct_bitwiseToXorDomain
  , correct_arithToXorDomain
  , correct_xorToBitwiseDomain
  , correct_asXorDomain
  , correct_fromXorDomain

  , correct_bra1
  , correct_bra2
  , correct_brb1
  , correct_brb2

  , correct_any
  , correct_ubounds
  , correct_sbounds
  , correct_singleton
  , correct_overlap
  , precise_overlap
  , correct_union
  , correct_zero_ext
  , correct_sign_ext
  , correct_concat
  , correct_select
  , correct_add
  , correct_neg
  , correct_mul
  , correct_scale
  , correct_udiv
  , correct_urem
  , correct_sdiv
  , correct_srem
  , correct_shl
  , correct_lshr
  , correct_ashr
  , correct_rol
  , correct_ror
  , correct_eq
  , correct_ult
  , correct_slt
  , correct_and
  , correct_or
  , correct_not
  , correct_xor
  , correct_testBit
  , correct_popcnt
  , correct_clz
  , correct_ctz
  ) where

import qualified Data.Bits as Bits
import           Data.Bits hiding (testBit, xor)
import qualified Data.List as List
import           Data.Parameterized.NatRepr
import           Numeric.Natural
import           GHC.TypeNats
import           GHC.Stack

import qualified Prelude
import           Prelude hiding (any, concat, negate, and, or, not)

import qualified What4.Utils.Arithmetic as Arith

import qualified What4.Utils.BVDomain.Arith as A
import qualified What4.Utils.BVDomain.Bitwise as B
import qualified What4.Utils.BVDomain.XOR as X

import           Test.Verification ( Property, property, (==>), Gen, chooseBool )


arithToBitwiseDomain :: A.Domain w -> B.Domain w
arithToBitwiseDomain :: Domain w -> Domain w
arithToBitwiseDomain Domain w
a =
  let mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a in
  case Domain w -> Maybe (Integer, Integer)
forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
    Maybe (Integer, Integer)
Nothing -> Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
0 Integer
mask
    Just (Integer
alo,Integer
_) -> Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
lo Integer
hi
      where
        u :: Integer
u = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
A.unknowns Domain w
a
        hi :: Integer
hi = Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
u
        lo :: Integer
lo = Integer
hi Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
u

bitwiseToArithDomain :: B.Domain w -> A.Domain w
bitwiseToArithDomain :: Domain w -> Domain w
bitwiseToArithDomain Domain w
b = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
A.interval Integer
mask Integer
lo ((Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)
  where
  mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b
  (Integer
lo,Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b

bitwiseToXorDomain :: B.Domain w -> X.Domain w
bitwiseToXorDomain :: Domain w -> Domain w
bitwiseToXorDomain Domain w
b = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.interval Integer
mask Integer
lo Integer
hi
  where
  mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b
  (Integer
lo,Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b

arithToXorDomain :: A.Domain w -> X.Domain w
arithToXorDomain :: Domain w -> Domain w
arithToXorDomain Domain w
a =
  let mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a in
  case Domain w -> Maybe (Integer, Integer)
forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
    Maybe (Integer, Integer)
Nothing -> Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.BVDXor Integer
mask Integer
mask Integer
mask
    Just (Integer
alo,Integer
_) -> Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
X.BVDXor Integer
mask Integer
hi Integer
u
      where
        u :: Integer
u = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
A.unknowns Domain w
a
        hi :: Integer
hi = Integer
alo Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
u

xorToBitwiseDomain :: X.Domain w -> B.Domain w
xorToBitwiseDomain :: Domain w -> Domain w
xorToBitwiseDomain Domain w
x = Integer -> Integer -> Integer -> Domain w
forall (w :: Nat). Integer -> Integer -> Integer -> Domain w
B.interval Integer
mask Integer
lo Integer
hi
  where
  mask :: Integer
mask = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
X.bvdMask Domain w
x
  (Integer
lo, Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
X.bitbounds Domain w
x

asXorDomain :: BVDomain w -> X.Domain w
asXorDomain :: BVDomain w -> Domain w
asXorDomain (BVDArith Domain w
a) = Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
arithToXorDomain Domain w
a
asXorDomain (BVDBitwise Domain w
b) = Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
bitwiseToXorDomain Domain w
b

fromXorDomain :: X.Domain w -> BVDomain w
fromXorDomain :: Domain w -> BVDomain w
fromXorDomain Domain w
x = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
xorToBitwiseDomain Domain w
x)

asArithDomain :: BVDomain w -> A.Domain w
asArithDomain :: BVDomain w -> Domain w
asArithDomain (BVDArith Domain w
a)   = Domain w
a
asArithDomain (BVDBitwise Domain w
b) = Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain w
b

asBitwiseDomain :: BVDomain w -> B.Domain w
asBitwiseDomain :: BVDomain w -> Domain w
asBitwiseDomain (BVDArith Domain w
a)   = Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain w
a
asBitwiseDomain (BVDBitwise Domain w
b) = Domain w
b

--------------------------------------------------------------------------------
-- BVDomain definition

-- | A value of type @'BVDomain' w@ represents a set of bitvectors of
-- width @w@. A BVDomain represents either an arithmetic interval, or
-- a bitwise interval.

data BVDomain (w :: Nat)
  = BVDArith !(A.Domain w)
  | BVDBitwise !(B.Domain w)
  deriving Int -> BVDomain w -> ShowS
[BVDomain w] -> ShowS
BVDomain w -> String
(Int -> BVDomain w -> ShowS)
-> (BVDomain w -> String)
-> ([BVDomain w] -> ShowS)
-> Show (BVDomain w)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (w :: Nat). Int -> BVDomain w -> ShowS
forall (w :: Nat). [BVDomain w] -> ShowS
forall (w :: Nat). BVDomain w -> String
showList :: [BVDomain w] -> ShowS
$cshowList :: forall (w :: Nat). [BVDomain w] -> ShowS
show :: BVDomain w -> String
$cshow :: forall (w :: Nat). BVDomain w -> String
showsPrec :: Int -> BVDomain w -> ShowS
$cshowsPrec :: forall (w :: Nat). Int -> BVDomain w -> ShowS
Show

-- | Return the bitvector mask value from this domain
bvdMask :: BVDomain w -> Integer
bvdMask :: BVDomain w -> Integer
bvdMask BVDomain w
x =
  case BVDomain w
x of
    BVDArith Domain w
a   -> Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a
    BVDBitwise Domain w
b -> Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
B.bvdMask Domain w
b

-- | Test if the domain satisfies its invariants
proper :: NatRepr w -> BVDomain w -> Bool
proper :: NatRepr w -> BVDomain w -> Bool
proper NatRepr w
w (BVDArith Domain w
a) = NatRepr w -> Domain w -> Bool
forall (w :: Nat). NatRepr w -> Domain w -> Bool
A.proper NatRepr w
w Domain w
a
proper NatRepr w
w (BVDBitwise Domain w
b) = NatRepr w -> Domain w -> Bool
forall (w :: Nat). NatRepr w -> Domain w -> Bool
B.proper NatRepr w
w Domain w
b

-- | Test if the given integer value is a member of the abstract domain
member :: BVDomain w -> Integer -> Bool
member :: BVDomain w -> Integer -> Bool
member (BVDArith Domain w
a) Integer
x = Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain w
a Integer
x
member (BVDBitwise Domain w
a) Integer
x = Domain w -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain w
a Integer
x

-- | Compute how many concrete elements are in the abstract domain
size :: BVDomain w -> Integer
size :: BVDomain w -> Integer
size (BVDArith Domain w
a)   = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
A.size Domain w
a
size (BVDBitwise Domain w
b) = Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
B.size Domain w
b

-- | Generate a random nonempty domain
genDomain :: NatRepr w -> Gen (BVDomain w)
genDomain :: NatRepr w -> Gen (BVDomain w)
genDomain NatRepr w
w =
  do Bool
b <- Gen Bool
chooseBool
     if Bool
b then
       Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> BVDomain w) -> Gen (Domain w) -> Gen (BVDomain w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> Gen (Domain w)
forall (w :: Nat). NatRepr w -> Gen (Domain w)
A.genDomain NatRepr w
w
     else
       Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> BVDomain w) -> Gen (Domain w) -> Gen (BVDomain w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w -> Gen (Domain w)
forall (w :: Nat). NatRepr w -> Gen (Domain w)
B.genDomain NatRepr w
w

-- | Generate a random element from a domain, which
--   is assumed to be nonempty
genElement :: BVDomain w -> Gen Integer
genElement :: BVDomain w -> Gen Integer
genElement (BVDArith Domain w
a) = Domain w -> Gen Integer
forall (w :: Nat). Domain w -> Gen Integer
A.genElement Domain w
a
genElement (BVDBitwise Domain w
b) = Domain w -> Gen Integer
forall (w :: Nat). Domain w -> Gen Integer
B.genElement Domain w
b

-- | Generate a random nonempty domain and an element
--   contained in that domain.
genPair :: NatRepr w -> Gen (BVDomain w, Integer)
genPair :: NatRepr w -> Gen (BVDomain w, Integer)
genPair NatRepr w
w =
  do BVDomain w
a <- NatRepr w -> Gen (BVDomain w)
forall (w :: Nat). NatRepr w -> Gen (BVDomain w)
genDomain NatRepr w
w
     Integer
x <- BVDomain w -> Gen Integer
forall (w :: Nat). BVDomain w -> Gen Integer
genElement BVDomain w
a
     (BVDomain w, Integer) -> Gen (BVDomain w, Integer)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BVDomain w
a,Integer
x)

--------------------------------------------------------------------------------
-- Projection functions

-- | Return value if this is a singleton.
asSingleton :: BVDomain w -> Maybe Integer
asSingleton :: BVDomain w -> Maybe Integer
asSingleton (BVDArith Domain w
a)   = Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
A.asSingleton Domain w
a
asSingleton (BVDBitwise Domain w
b) = Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
B.asSingleton Domain w
b

{- |
 Precondition: @x <= lomask@.  Find the (arithmetically) smallest
 @z@ above @x@ which is bitwise above @lomask@.  In other words
 find the smallest @z@ such that @x <= z@ and @lomask .|. z == z@.
-}
bitwiseRoundAbove ::
  Integer {- ^ @bvmask@, based on the width of the bitvectors in question -} ->
  Integer {- ^ @x@ -} ->
  Integer {- ^ @lomask@ -} ->
  Integer
bitwiseRoundAbove :: Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove Integer
bvmask Integer
x Integer
lomask = Integer
upperbits Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
lowerbits
  where
  upperbits :: Integer
upperbits = Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (Integer
bvmask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
fillmask)
  lowerbits :: Integer
lowerbits = Integer
lomask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
fillmask
  fillmask :: Integer
fillmask = Integer -> Integer
A.fillright ((Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
lomask) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
x)

{- |
 Precondition: @lomask <= x <= himask@ and @lomask .|. himask == himask@.
 Find the (arithmetically) smallest @z@ above @x@ which is bitwise between
 @lomask@ and @himask@.  In other words, find the smallest @z@ such that
 @x <= z@ and @lomask .|. z = z@ and @z .|. himask == himask@.
-}
bitwiseRoundBetween ::
  Integer {- ^ @bvmask@, based on the width of the bitvectors in question -} ->
  Integer {- ^ @x@ -} ->
  Integer {- ^ @lomask@ -} ->
  Integer {- ^ @himask@ -} ->
  Integer
bitwiseRoundBetween :: Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween Integer
bvmask Integer
x Integer
lomask Integer
himask = Integer
final
  -- read these steps bottom up...
  where
  -- Finally mask out the low bits and only set those required by the lomask
  final :: Integer
final = (Integer
upper Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (Integer
lobits Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
bvmask)) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
lomask

  -- add the correcting bit and mask out any extraneous bits set in
  -- the previous step
  upper :: Integer
upper = (Integer
z Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
highbit) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
himask

  -- set ourselves up so that when we add the high bit to correct,
  -- the carry will ripple until it finds a bit position that we
  -- are allowed to set.
  z :: Integer
z = Integer
loup Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
himask'

  -- isolate just the highest incorrect bit
  highbit :: Integer
highbit = Integer
rmask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
lobits

  -- a mask for all the bits to the right of the highest incorrect bit
  lobits :: Integer
lobits = Integer
rmask Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
1

  -- set all the bits to the right of the highest incorrect bit
  rmask :: Integer
rmask = Integer -> Integer
A.fillright Integer
r

  -- now, compute all the bits that are set, but are not
  -- allowed to be set according to the himask
  r :: Integer
r = Integer
loup Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
himask'

  -- complement of the highmask
  himask' :: Integer
himask' = Integer
himask Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
bvmask

  -- first, round up to the lomask
  loup :: Integer
loup = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove Integer
bvmask Integer
x Integer
lomask


-- | Test if an arithmetic domain overlaps with a bitwise domain
mixedDomainsOverlap :: A.Domain a -> B.Domain b -> Bool
mixedDomainsOverlap :: Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain a
a Domain b
b =
   case Domain a -> Maybe (Integer, Integer)
forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain a
a of
     Maybe (Integer, Integer)
Nothing -> Domain b -> Bool
forall (w :: Nat). Domain w -> Bool
B.nonempty Domain b
b
     Just (Integer
alo,Integer
_) ->
       let (Integer
lomask,Integer
himask) = Domain b -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain b
b
           brb :: Integer
brb = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (Domain a -> Integer
forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain a
a) Integer
alo Integer
lomask Integer
himask
        in Domain b -> Bool
forall (w :: Nat). Domain w -> Bool
B.nonempty Domain b
b Bool -> Bool -> Bool
&& (Domain a -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
lomask Bool -> Bool -> Bool
|| Domain a -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
himask Bool -> Bool -> Bool
|| Domain a -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
A.member Domain a
a Integer
brb)


-- | Return true if domains contain a common element.
domainsOverlap :: BVDomain w -> BVDomain w -> Bool
domainsOverlap :: BVDomain w -> BVDomain w -> Bool
domainsOverlap (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = Domain w -> Domain w -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
B.domainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDArith Domain w
a)   (BVDArith Domain w
b)   = Domain w -> Domain w -> Bool
forall (w :: Nat). Domain w -> Domain w -> Bool
A.domainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDArith Domain w
a)   (BVDBitwise Domain w
b) = Domain w -> Domain w -> Bool
forall (a :: Nat) (b :: Nat). Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain w
a Domain w
b
domainsOverlap (BVDBitwise Domain w
b) (BVDArith Domain w
a)   = Domain w -> Domain w -> Bool
forall (a :: Nat) (b :: Nat). Domain a -> Domain b -> Bool
mixedDomainsOverlap Domain w
a Domain w
b

arithDomainLo :: A.Domain w -> Integer
arithDomainLo :: Domain w -> Integer
arithDomainLo Domain w
a =
  case Domain w -> Maybe (Integer, Integer)
forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
    Maybe (Integer, Integer)
Nothing -> Integer
0
    Just (Integer
lo,Integer
_) -> Integer
lo

mixedCandidates :: A.Domain w -> B.Domain w -> [Integer]
mixedCandidates :: Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b =
  case Domain w -> Maybe (Integer, Integer)
forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
A.arithDomainData Domain w
a of
    Maybe (Integer, Integer)
Nothing -> [ Integer
lomask ]
    Just (Integer
alo,Integer
_) -> [ Integer
lomask, Integer
himask, Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
A.bvdMask Domain w
a) Integer
alo Integer
lomask Integer
himask ]
 where
 (Integer
lomask,Integer
himask) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b

-- | Return a list of "candidate" overlap elements.  If two domains
--   overlap, then they will definitely share one of the given
--   values.
overlapCandidates :: BVDomain w -> BVDomain w -> [Integer]
overlapCandidates :: BVDomain w -> BVDomain w -> [Integer]
overlapCandidates (BVDArith Domain w
a)   (BVDBitwise Domain w
b) = Domain w -> Domain w -> [Integer]
forall (w :: Nat). Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b
overlapCandidates (BVDBitwise Domain w
b) (BVDArith Domain w
a)   = Domain w -> Domain w -> [Integer]
forall (w :: Nat). Domain w -> Domain w -> [Integer]
mixedCandidates Domain w
a Domain w
b
overlapCandidates (BVDArith Domain w
a)   (BVDArith Domain w
b)   = [ Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
arithDomainLo Domain w
a, Domain w -> Integer
forall (w :: Nat). Domain w -> Integer
arithDomainLo Domain w
b ]
overlapCandidates (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = [ Integer
loa Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
lob ]
  where
  (Integer
loa,Integer
_) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
a
  (Integer
lob,Integer
_) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b


eq :: BVDomain w -> BVDomain w -> Maybe Bool
eq :: BVDomain w -> BVDomain w -> Maybe Bool
eq BVDomain w
a BVDomain w
b
  | Just Integer
x <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a
  , Just Integer
y <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y)
  | BVDomain w -> BVDomain w -> Bool
forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap BVDomain w
a BVDomain w
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing

-- | Check if all elements in one domain are less than all elements in other.
slt :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt :: NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt NatRepr w
w BVDomain w
a BVDomain w
b = NatRepr w -> Domain w -> Domain w -> Maybe Bool
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Maybe Bool
A.slt NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b)

-- | Check if all elements in one domain are less than all elements in other.
ult :: (1 <= w) => BVDomain w -> BVDomain w -> Maybe Bool
ult :: BVDomain w -> BVDomain w -> Maybe Bool
ult BVDomain w
a BVDomain w
b = Domain w -> Domain w -> Maybe Bool
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Maybe Bool
A.ult (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b)

-- | Return @Just@ if every bitvector in the domain has the same bit
-- at the given index.
testBit ::
  NatRepr w ->
  BVDomain w ->
  Natural {- ^ Index of bit (least-significant bit has index 0) -} ->
  Maybe Bool
testBit :: NatRepr w -> BVDomain w -> Natural -> Maybe Bool
testBit NatRepr w
_w BVDomain w
a Natural
i = Domain w -> Natural -> Maybe Bool
forall (w :: Nat). Domain w -> Natural -> Maybe Bool
B.testBit (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) Natural
i

ubounds :: BVDomain w -> (Integer, Integer)
ubounds :: BVDomain w -> (Integer, Integer)
ubounds BVDomain w
a = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a)

sbounds :: (1 <= w) => NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds :: NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds NatRepr w
w BVDomain w
a = NatRepr w -> Domain w -> (Integer, Integer)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> (Integer, Integer)
A.sbounds NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a)

--------------------------------------------------------------------------------
-- Operations

-- | Represents all values
any :: (1 <= w) => NatRepr w -> BVDomain w
any :: NatRepr w -> BVDomain w
any NatRepr w
w = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (NatRepr w -> Domain w
forall (w :: Nat). NatRepr w -> Domain w
B.any NatRepr w
w)

-- | Create a bitvector domain representing the integer.
singleton :: (HasCallStack, 1 <= w) => NatRepr w -> Integer -> BVDomain w
singleton :: NatRepr w -> Integer -> BVDomain w
singleton NatRepr w
w Integer
x = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w Integer
x)

-- | @range w l u@ returns domain containing all bitvectors formed
-- from the @w@ low order bits of some @i@ in @[l,u]@.  Note that per
-- @testBit@, the least significant bit has index @0@.
range :: NatRepr w -> Integer -> Integer -> BVDomain w
range :: NatRepr w -> Integer -> Integer -> BVDomain w
range NatRepr w
w Integer
al Integer
ah = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
al Integer
ah)

-- | Create an abstract domain from an ascending list of elements.
-- The elements are assumed to be distinct.
fromAscEltList :: (1 <= w) => NatRepr w -> [Integer] -> BVDomain w
fromAscEltList :: NatRepr w -> [Integer] -> BVDomain w
fromAscEltList NatRepr w
w [Integer]
xs = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> [Integer] -> Domain w
forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> Domain w
A.fromAscEltList NatRepr w
w [Integer]
xs)

-- | Return union of two domains.
union :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
union :: BVDomain w -> BVDomain w -> BVDomain w
union (BVDBitwise Domain w
a) (BVDBitwise Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union Domain w
a Domain w
b)
union (BVDArith Domain w
a) (BVDArith Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.union Domain w
a Domain w
b)
union (BVDBitwise Domain w
a) (BVDArith Domain w
b) = Domain w -> Domain w -> BVDomain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
b Domain w
a
union (BVDArith Domain w
a) (BVDBitwise Domain w
b) = Domain w -> Domain w -> BVDomain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
a Domain w
b

mixedUnion :: (1 <= w) => A.Domain w -> B.Domain w  -> BVDomain w
mixedUnion :: Domain w -> Domain w -> BVDomain w
mixedUnion Domain w
a Domain w
b
  | Just Integer
_ <- Domain w -> Maybe Integer
forall (w :: Nat). Domain w -> Maybe Integer
A.asSingleton Domain w
a = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union (Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain w
a) Domain w
b)
  | Bool
otherwise = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.union Domain w
a (Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain w
b))

-- | @concat a y@ returns domain where each element in @a@ has been
-- concatenated with an element in @y@.  The most-significant bits
-- are @a@, and the least significant bits are @y@.
concat :: NatRepr u -> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat :: NatRepr u
-> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat NatRepr u
u (BVDArith Domain u
a) NatRepr v
v (BVDArith Domain v
b) = Domain (u + v) -> BVDomain (u + v)
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
A.concat NatRepr u
u Domain u
a NatRepr v
v Domain v
b)
concat NatRepr u
u (BVDomain u -> Domain u
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain u
a) NatRepr v
v (BVDomain v -> Domain v
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain v
b) = Domain (u + v) -> BVDomain (u + v)
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
forall (u :: Nat) (v :: Nat).
NatRepr u -> Domain u -> NatRepr v -> Domain v -> Domain (u + v)
B.concat NatRepr u
u Domain u
a NatRepr v
v Domain v
b)

-- | @select i n a@ selects @n@ bits starting from index @i@ from @a@.
select ::
  (1 <= n, i + n <= w) =>
  NatRepr i ->
  NatRepr n ->
  BVDomain w -> BVDomain n
select :: NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
select NatRepr i
i NatRepr n
n (BVDArith Domain w
a)   = Domain n -> BVDomain n
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr i -> NatRepr n -> Domain w -> Domain n
forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> Domain w -> Domain n
A.select NatRepr i
i NatRepr n
n Domain w
a)
select NatRepr i
i NatRepr n
n (BVDBitwise Domain w
b) = Domain n -> BVDomain n
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (NatRepr i -> NatRepr n -> Domain w -> Domain n
forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> Domain w -> Domain n
B.select NatRepr i
i NatRepr n
n Domain w
b)

zext :: (1 <= w, w+1 <= u) => BVDomain w -> NatRepr u -> BVDomain u
zext :: BVDomain w -> NatRepr u -> BVDomain u
zext (BVDArith Domain w
a) NatRepr u
u   = Domain u -> BVDomain u
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> NatRepr u -> Domain u
forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
A.zext Domain w
a NatRepr u
u)
zext (BVDBitwise Domain w
b) NatRepr u
u = Domain u -> BVDomain u
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> NatRepr u -> Domain u
forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
Domain w -> NatRepr u -> Domain u
B.zext Domain w
b NatRepr u
u)

sext ::
  forall w u. (1 <= w, w + 1 <= u) =>
  NatRepr w ->
  BVDomain w ->
  NatRepr u ->
  BVDomain u
sext :: NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u
sext NatRepr w
w (BVDArith Domain w
a) NatRepr u
u   = Domain u -> BVDomain u
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Domain w -> NatRepr u -> Domain u
forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
A.sext NatRepr w
w Domain w
a NatRepr u
u)
sext NatRepr w
w (BVDBitwise Domain w
b) NatRepr u
u = Domain u -> BVDomain u
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (NatRepr w -> Domain w -> NatRepr u -> Domain u
forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> Domain w -> NatRepr u -> Domain u
B.sext NatRepr w
w Domain w
b NatRepr u
u)

--------------------------------------------------------------------------------
-- Shifts

-- An arbitrary value; if we have to union together more than this many
-- bitwise shifts or rotates we'll fall back on some default instead
shiftBound :: Integer
shiftBound :: Integer
shiftBound = Integer
16

shl :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
shl :: NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
shl NatRepr w
w (BVDBitwise Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
  | Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
      Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> BVDomain w) -> Domain w -> BVDomain w
forall a b. (a -> b) -> a -> b
$ (Domain w -> Domain w -> Domain w) -> [Domain w] -> Domain w
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.shl NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
  where
  (Integer
lo, Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
  hi' :: Integer
hi' = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
hi (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)

shl NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.shl NatRepr w
w Domain w
a Domain w
b)


lshr :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
lshr :: NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
lshr NatRepr w
w (BVDBitwise Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
  | Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
      Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> BVDomain w) -> Domain w -> BVDomain w
forall a b. (a -> b) -> a -> b
$ (Domain w -> Domain w -> Domain w) -> [Domain w] -> Domain w
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.lshr NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
  where
  (Integer
lo, Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
  hi' :: Integer
hi' = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
hi (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)

lshr NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.lshr NatRepr w
w Domain w
a Domain w
b)



ashr :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ashr :: NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ashr NatRepr w
w (BVDBitwise Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b)
  | Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi' Bool -> Bool -> Bool
&& Integer
hi' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound =
      Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> BVDomain w) -> Domain w -> BVDomain w
forall a b. (a -> b) -> a -> b
$ (Domain w -> Domain w -> Domain w) -> [Domain w] -> Domain w
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Integer -> Domain w
B.ashr NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi'] ]
  where
  (Integer
lo, Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds Domain w
b
  hi' :: Integer
hi' = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
hi (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)

ashr NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.ashr NatRepr w
w Domain w
a Domain w
b)


rol :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

-- Special cases, rotating all 0 or all 1 bits makes no difference
rol :: NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
rol NatRepr w
_w a :: BVDomain w
a@(BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton -> Just Integer
x) BVDomain w
_
  | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = BVDomain w
a
  | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== BVDomain w -> Integer
forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a = BVDomain w
a

rol NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) =
    if (Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi Bool -> Bool -> Bool
&& Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound) then
      Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> BVDomain w) -> Domain w -> BVDomain w
forall a b. (a -> b) -> a -> b
$ (Domain w -> Domain w -> Domain w) -> [Domain w] -> Domain w
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.rol NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi] ]
    else
      NatRepr w -> BVDomain w
forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr w
w

  where
  (Integer
lo, Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
b (NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)))


ror :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w

-- Special cases, rotating all 0 or all 1 bits makes no difference
ror :: NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ror NatRepr w
_w a :: BVDomain w
a@(BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton -> Just Integer
x) BVDomain w
_
  | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = BVDomain w
a
  | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== BVDomain w -> Integer
forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a = BVDomain w
a

ror NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) =
    if (Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi Bool -> Bool -> Bool
&& Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
shiftBound) then
      Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> BVDomain w) -> Domain w -> BVDomain w
forall a b. (a -> b) -> a -> b
$ (Domain w -> Domain w -> Domain w) -> [Domain w] -> Domain w
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.union [ NatRepr w -> Domain w -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Domain w -> Integer -> Domain w
B.ror NatRepr w
w Domain w
a Integer
y | Integer
y <- [Integer
lo .. Integer
hi] ]
    else
      NatRepr w -> BVDomain w
forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr w
w

  where
  (Integer
lo, Integer
hi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
A.ubounds (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
b (NatRepr w -> Integer -> Domain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> Domain w
A.singleton NatRepr w
w (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w)))

--------------------------------------------------------------------------------
-- Arithmetic

add :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
add :: BVDomain w -> BVDomain w -> BVDomain w
add BVDomain w
a BVDomain w
b
  | Just Integer
0 <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
  | Just Integer
0 <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
  | Bool
otherwise = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.add (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b))

negate :: (1 <= w) => BVDomain w -> BVDomain w
negate :: BVDomain w -> BVDomain w
negate (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w
A.negate Domain w
a)

scale :: (1 <= w) => Integer -> BVDomain w -> BVDomain w
scale :: Integer -> BVDomain w -> BVDomain w
scale Integer
k BVDomain w
a
  | Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 = BVDomain w
a
  | Bool
otherwise = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Integer -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Integer -> Domain w -> Domain w
A.scale Integer
k (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a))

mul :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
mul :: BVDomain w -> BVDomain w -> BVDomain w
mul BVDomain w
a BVDomain w
b
  | Just Integer
1 <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
  | Just Integer
1 <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
  | Bool
otherwise = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.mul (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain BVDomain w
b))

udiv :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
udiv :: BVDomain w -> BVDomain w -> BVDomain w
udiv (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.udiv Domain w
a Domain w
b)

urem :: (1 <= w) => BVDomain w -> BVDomain w -> BVDomain w
urem :: BVDomain w -> BVDomain w -> BVDomain w
urem (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> Domain w -> Domain w
forall (w :: Nat). (1 <= w) => Domain w -> Domain w -> Domain w
A.urem Domain w
a Domain w
b)

sdiv :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv :: NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.sdiv NatRepr w
w Domain w
a Domain w
b)

srem :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem :: NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asArithDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Domain w -> Domain w -> Domain w
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Domain w -> Domain w -> Domain w
A.srem NatRepr w
w Domain w
a Domain w
b)

--------------------------------------------------------------------------------
-- Bitwise logical

-- | Complement bits in range.
not :: BVDomain w -> BVDomain w
not :: BVDomain w -> BVDomain w
not (BVDArith Domain w
a) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
A.not Domain w
a)
not (BVDBitwise Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w
B.not Domain w
b)

and :: BVDomain w -> BVDomain w -> BVDomain w
and :: BVDomain w -> BVDomain w -> BVDomain w
and BVDomain w
a BVDomain w
b
  | Just Integer
x <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a, Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mask = BVDomain w
b
  | Just Integer
x <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b, Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
mask = BVDomain w
a
  | Bool
otherwise = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.and (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))
 where
 mask :: Integer
mask = BVDomain w -> Integer
forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a

or :: BVDomain w -> BVDomain w -> BVDomain w
or :: BVDomain w -> BVDomain w -> BVDomain w
or BVDomain w
a BVDomain w
b
  | Just Integer
0 <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
  | Just Integer
0 <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
  | Bool
otherwise = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.or (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))

xor :: BVDomain w -> BVDomain w -> BVDomain w
xor :: BVDomain w -> BVDomain w -> BVDomain w
xor BVDomain w
a BVDomain w
b
  | Just Integer
0 <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
a = BVDomain w
b
  | Just Integer
0 <- BVDomain w -> Maybe Integer
forall (w :: Nat). BVDomain w -> Maybe Integer
asSingleton BVDomain w
b = BVDomain w
a
  | Bool
otherwise = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDBitwise (Domain w -> Domain w -> Domain w
forall (w :: Nat). Domain w -> Domain w -> Domain w
B.xor (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
a) (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain BVDomain w
b))

-------------------------------------------------------------------------------
-- Misc operations

popcnt :: NatRepr w -> BVDomain w -> BVDomain w
popcnt :: NatRepr w -> BVDomain w -> BVDomain w
popcnt NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
  where
  (Integer
bitlo, Integer
bithi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
  lo :: Integer
lo = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Integer -> Int
forall a. Bits a => a -> Int
Bits.popCount Integer
bitlo)
  hi :: Integer
hi = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Integer -> Int
forall a. Bits a => a -> Int
Bits.popCount Integer
bithi)

clz :: NatRepr w -> BVDomain w -> BVDomain w
clz :: NatRepr w -> BVDomain w -> BVDomain w
clz NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
  where
  (Integer
bitlo, Integer
bithi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
  lo :: Integer
lo = NatRepr w -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr w
w Integer
bithi
  hi :: Integer
hi = NatRepr w -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr w
w Integer
bitlo

ctz :: NatRepr w -> BVDomain w -> BVDomain w
ctz :: NatRepr w -> BVDomain w -> BVDomain w
ctz NatRepr w
w (BVDomain w -> Domain w
forall (w :: Nat). BVDomain w -> Domain w
asBitwiseDomain -> Domain w
b) = Domain w -> BVDomain w
forall (w :: Nat). Domain w -> BVDomain w
BVDArith (NatRepr w -> Integer -> Integer -> Domain w
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Domain w
A.range NatRepr w
w Integer
lo Integer
hi)
  where
  (Integer
bitlo, Integer
bithi) = Domain w -> (Integer, Integer)
forall (w :: Nat). Domain w -> (Integer, Integer)
B.bitbounds Domain w
b
  lo :: Integer
lo = NatRepr w -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr w
w Integer
bithi
  hi :: Integer
hi = NatRepr w -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr w
w Integer
bitlo


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

-- | Check that a domain is proper, and that
--   the given value is a member
pmember :: NatRepr n -> BVDomain n -> Integer -> Bool
pmember :: NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n BVDomain n
a Integer
x = NatRepr n -> BVDomain n -> Bool
forall (w :: Nat). NatRepr w -> BVDomain w -> Bool
proper NatRepr n
n BVDomain n
a Bool -> Bool -> Bool
&& BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x

correct_arithToBitwise :: NatRepr n -> (A.Domain n, Integer) -> Property
correct_arithToBitwise :: NatRepr n -> (Domain n, Integer) -> Property
correct_arithToBitwise NatRepr n
n (Domain n
a,Integer
x) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
A.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
B.pmember NatRepr n
n (Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w
arithToBitwiseDomain Domain n
a) Integer
x

correct_bitwiseToArith :: NatRepr n -> (B.Domain n, Integer) -> Property
correct_bitwiseToArith :: NatRepr n -> (Domain n, Integer) -> Property
correct_bitwiseToArith NatRepr n
n (Domain n
b,Integer
x) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain n
b 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
A.pmember NatRepr n
n (Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w
bitwiseToArithDomain Domain n
b) Integer
x

correct_bitwiseToXorDomain :: NatRepr n -> (B.Domain n, Integer) -> Property
correct_bitwiseToXorDomain :: NatRepr n -> (Domain n, Integer) -> Property
correct_bitwiseToXorDomain NatRepr n
n (Domain n
b,Integer
x) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
B.member Domain n
b 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
X.pmember NatRepr n
n (Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w
bitwiseToXorDomain Domain n
b) Integer
x

correct_arithToXorDomain :: NatRepr n -> (A.Domain n, Integer) -> Property
correct_arithToXorDomain :: NatRepr n -> (Domain n, Integer) -> Property
correct_arithToXorDomain NatRepr n
n (Domain n
a,Integer
x) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
A.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
X.pmember NatRepr n
n (Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w
arithToXorDomain Domain n
a) Integer
x

correct_xorToBitwiseDomain :: NatRepr n -> (X.Domain n, Integer) -> Property
correct_xorToBitwiseDomain :: NatRepr n -> (Domain n, Integer) -> Property
correct_xorToBitwiseDomain NatRepr n
n (Domain n
a,Integer
x) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
X.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
B.pmember NatRepr n
n (Domain n -> Domain n
forall (w :: Nat). Domain w -> Domain w
xorToBitwiseDomain Domain n
a) Integer
x

correct_asXorDomain :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_asXorDomain :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_asXorDomain NatRepr n
n (BVDomain n
a, Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain 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
X.pmember NatRepr n
n (BVDomain n -> Domain n
forall (w :: Nat). BVDomain w -> Domain w
asXorDomain BVDomain n
a) Integer
x

correct_fromXorDomain :: NatRepr n -> (X.Domain n, Integer) -> Property
correct_fromXorDomain :: NatRepr n -> (Domain n, Integer) -> Property
correct_fromXorDomain NatRepr n
n (Domain n
a, Integer
x) = Domain n -> Integer -> Bool
forall (w :: Nat). Domain w -> Integer -> Bool
X.member Domain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (Domain n -> BVDomain n
forall (w :: Nat). Domain w -> BVDomain w
fromXorDomain Domain n
a) Integer
x


correct_bra1 :: NatRepr n -> Integer -> Integer -> Property
correct_bra1 :: NatRepr n -> Integer -> Integer -> Property
correct_bra1 NatRepr n
n Integer
x Integer
lomask = Integer
lomask Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q)
 where
 q :: Integer
q = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove (NatRepr n -> Integer
forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask

correct_bra2 :: NatRepr n -> Integer -> Integer -> Integer -> Property
correct_bra2 :: NatRepr n -> Integer -> Integer -> Integer -> Property
correct_bra2 NatRepr n
n Integer
x Integer
lomask Integer
q' = (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q') Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
q Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
q'
 where
 q :: Integer
q = Integer -> Integer -> Integer -> Integer
bitwiseRoundAbove (NatRepr n -> Integer
forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask

correct_brb1 :: NatRepr n -> Integer -> Integer -> Integer -> Property
correct_brb1 :: NatRepr n -> Integer -> Integer -> Integer -> Property
correct_brb1 NatRepr n
n Integer
x Integer
lomask Integer
himask =
    (Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
himask Bool -> Bool -> Bool
&& Integer
lomask Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
himask) Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
    (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
q Integer
himask)
  where
  q :: Integer
q = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (NatRepr n -> Integer
forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask Integer
himask

correct_brb2 :: NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property
correct_brb2 :: NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property
correct_brb2 NatRepr n
n Integer
x Integer
lomask Integer
himask Integer
q' =
    (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
lomask Integer
q' Bool -> Bool -> Bool
&& Integer -> Integer -> Bool
B.bitle Integer
q' Integer
himask) Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
q Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
q'
  where
  q :: Integer
q = Integer -> Integer -> Integer -> Integer -> Integer
bitwiseRoundBetween (NatRepr n -> Integer
forall (n :: Nat). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer
x Integer
lomask Integer
himask

correct_any :: (1 <= n) => NatRepr n -> Integer -> Property
correct_any :: NatRepr n -> Integer -> Property
correct_any NatRepr n
n Integer
x = Bool -> Property
property (NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n
forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
any NatRepr n
n) Integer
x)

correct_ubounds :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_ubounds :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_ubounds NatRepr n
n (BVDomain n
a,Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x' Bool -> Bool -> Bool
&& Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x
  (Integer
lo,Integer
hi) = BVDomain n -> (Integer, Integer)
forall (w :: Nat). BVDomain w -> (Integer, Integer)
ubounds BVDomain n
a

correct_sbounds :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_sbounds :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_sbounds NatRepr n
n (BVDomain n
a,Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x' Bool -> Bool -> Bool
&& Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  (Integer
lo,Integer
hi) = NatRepr n -> BVDomain n -> (Integer, Integer)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> (Integer, Integer)
sbounds NatRepr n
n BVDomain n
a

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 (BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member (NatRepr n -> Integer -> BVDomain n
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> BVDomain 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_overlap :: BVDomain n -> BVDomain n -> Integer -> Property
correct_overlap :: BVDomain n -> BVDomain n -> Integer -> Property
correct_overlap BVDomain n
a BVDomain n
b Integer
x =
  BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
&& BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> BVDomain n -> Bool
forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap BVDomain n
a BVDomain n
b

precise_overlap :: BVDomain n -> BVDomain n -> Property
precise_overlap :: BVDomain n -> BVDomain n -> Property
precise_overlap BVDomain n
a BVDomain n
b =
  BVDomain n -> BVDomain n -> Bool
forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
domainsOverlap BVDomain n
a BVDomain n
b Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
List.or [ BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
&& BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x | Integer
x <- BVDomain n -> BVDomain n -> [Integer]
forall (w :: Nat). BVDomain w -> BVDomain w -> [Integer]
overlapCandidates BVDomain n
a BVDomain n
b ]

correct_union :: (1 <= n) => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property
correct_union :: NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property
correct_union NatRepr n
n BVDomain n
a BVDomain n
b Integer
x =
  (BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Bool
|| BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
x) Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
union BVDomain n
a BVDomain n
b) Integer
x

correct_zero_ext :: (1 <= w, w+1 <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_zero_ext :: NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_zero_ext NatRepr w
w BVDomain w
a NatRepr u
u Integer
x = BVDomain w -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr u -> BVDomain u -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr u
u (BVDomain w -> NatRepr u -> BVDomain u
forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
BVDomain w -> NatRepr u -> BVDomain u
zext BVDomain w
a NatRepr u
u) Integer
x'
  where
  x' :: Integer
x' = NatRepr w -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr w
w Integer
x

correct_sign_ext :: (1 <= w, w+1 <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_sign_ext :: NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
correct_sign_ext NatRepr w
w BVDomain w
a NatRepr u
u Integer
x = BVDomain w -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x' Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr u -> BVDomain u -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr u
u (NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u
forall (w :: Nat) (u :: Nat).
(1 <= w, (w + 1) <= u) =>
NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u
sext NatRepr w
w BVDomain w
a NatRepr u
u) Integer
x'
  where
  x' :: Integer
x' = NatRepr w -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
x

correct_concat :: NatRepr m -> (BVDomain m,Integer) -> NatRepr n -> (BVDomain n,Integer) -> Property
correct_concat :: NatRepr m
-> (BVDomain m, Integer)
-> NatRepr n
-> (BVDomain n, Integer)
-> Property
correct_concat NatRepr m
m (BVDomain m
a,Integer
x) NatRepr n
n (BVDomain n
b,Integer
y) =
    BVDomain m -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain m
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr (m + n) -> BVDomain (m + n) -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember (NatRepr m -> NatRepr n -> NatRepr (m + n)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr m
m NatRepr n
n) (NatRepr m
-> BVDomain m -> NatRepr n -> BVDomain n -> BVDomain (m + n)
forall (u :: Nat) (v :: Nat).
NatRepr u
-> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
concat NatRepr m
m BVDomain m
a NatRepr n
n BVDomain n
b) Integer
z
  where
  z :: Integer
z = (Integer
x Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (NatRepr n -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr n
n)) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
y

correct_select :: (1 <= n, i + n <= w) =>
  NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property
correct_select :: NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property
correct_select NatRepr i
i NatRepr n
n (BVDomain w
a, Integer
x) = BVDomain w -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain w
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
forall (n :: Nat) (i :: Nat) (w :: Nat).
(1 <= n, (i + n) <= w) =>
NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
select NatRepr i
i NatRepr n
n BVDomain w
a) Integer
y
  where
  y :: Integer
y = NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n ((Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. BVDomain w -> Integer
forall (w :: Nat). BVDomain w -> Integer
bvdMask BVDomain w
a) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (NatRepr i -> Int
forall (n :: Nat). NatRepr n -> Int
widthVal NatRepr i
i))

correct_add :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_add :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_add NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
add BVDomain n
a BVDomain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y)

correct_neg :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_neg :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_neg NatRepr n
n (BVDomain n
a,Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n
forall (w :: Nat). (1 <= w) => BVDomain w -> BVDomain w
negate BVDomain n
a) (Integer -> Integer
forall a. Num a => a -> a
Prelude.negate Integer
x)

correct_mul :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_mul :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_mul NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
mul BVDomain n
a BVDomain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y)

correct_scale :: (1 <= n) => NatRepr n -> Integer -> (BVDomain n, Integer) -> Property
correct_scale :: NatRepr n -> Integer -> (BVDomain n, Integer) -> Property
correct_scale NatRepr n
n Integer
k (BVDomain n
a,Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (Integer -> BVDomain n -> BVDomain n
forall (w :: Nat). (1 <= w) => Integer -> BVDomain w -> BVDomain w
scale Integer
k' BVDomain n
a) (Integer
k' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
x)
  where
  k' :: Integer
k' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
k

correct_udiv :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_udiv :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_udiv NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
udiv BVDomain n
a BVDomain n
b) (Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` 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_urem :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_urem :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_urem NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
urem BVDomain n
a BVDomain n
b) (Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` 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_sdiv :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_sdiv :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_sdiv NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
    BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
sdiv NatRepr n
n BVDomain n
a BVDomain n
b) (Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y')
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y

correct_srem :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_srem :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_srem NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
    BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y' Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> Integer
y' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
srem NatRepr n
n BVDomain n
a BVDomain n
b) (Integer
x' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y')
  where
  x' :: Integer
x' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x
  y' :: Integer
y' = NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y

correct_shl :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_shl :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_shl NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
shl NatRepr n
n BVDomain n
a BVDomain n
b) Integer
z
  where
  z :: Integer
z = (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (NatRepr n -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr n
n) Integer
y)

correct_lshr :: (1 <= n) => NatRepr n ->  (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_lshr :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_lshr NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
lshr NatRepr n
n BVDomain n
a BVDomain n
b) Integer
z
  where
  z :: Integer
z = (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (NatRepr n -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr n
n) Integer
y)

correct_ashr :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ashr :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ashr NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ashr NatRepr n
n BVDomain n
a BVDomain n
b) Integer
z
  where
  z :: Integer
z = (NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (NatRepr n -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr n
n) Integer
y)

correct_rol :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_rol :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_rol NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
rol NatRepr n
n BVDomain n
a BVDomain n
b) (NatRepr n -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateLeft NatRepr n
n Integer
x Integer
y)

correct_ror :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ror :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ror NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
ror NatRepr n
n BVDomain n
a BVDomain n
b) (NatRepr n -> Integer -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer -> Integer
Arith.rotateRight NatRepr n
n Integer
x Integer
y)

correct_eq :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_eq :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_eq NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
  BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
    case BVDomain n -> BVDomain n -> Maybe Bool
forall (w :: Nat). BVDomain w -> BVDomain w -> Maybe Bool
eq BVDomain n
a BVDomain n
b of
      Just Bool
True  -> NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
      Just Bool
False -> NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
      Maybe Bool
Nothing    -> Bool
True

correct_ult :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ult :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_ult NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
  BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
    case BVDomain n -> BVDomain n -> Maybe Bool
forall (w :: Nat).
(1 <= w) =>
BVDomain w -> BVDomain w -> Maybe Bool
ult BVDomain n
a BVDomain n
b of
      Just Bool
True  -> NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
      Just Bool
False -> NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
n Integer
y
      Maybe Bool
Nothing    -> Bool
True

correct_slt :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_slt :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_slt NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) =
  BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
    case NatRepr n -> BVDomain n -> BVDomain n -> Maybe Bool
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
slt NatRepr n
n BVDomain n
a BVDomain n
b of
      Just Bool
True  -> NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
      Just Bool
False -> NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Integer -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr n
n Integer
y
      Maybe Bool
Nothing    -> Bool
True

correct_not :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_not :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_not NatRepr n
n (BVDomain n
a,Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n
forall (w :: Nat). BVDomain w -> BVDomain w
not BVDomain n
a) (Integer -> Integer
forall a. Bits a => a -> a
complement Integer
x)

correct_and :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_and :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_and NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
and BVDomain n
a BVDomain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
y)

correct_or :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_or :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_or NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
or BVDomain n
a BVDomain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
y)

correct_xor :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_xor :: NatRepr n
-> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
correct_xor NatRepr n
n (BVDomain n
a,Integer
x) (BVDomain n
b,Integer
y) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Property -> Property
forall t. Verifiable t => Bool -> t -> Property
==> BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
b Integer
y Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (BVDomain n -> BVDomain n -> BVDomain n
forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
xor BVDomain n
a BVDomain n
b) (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`Bits.xor` Integer
y)

correct_testBit :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Natural -> Property
correct_testBit :: NatRepr n -> (BVDomain n, Integer) -> Natural -> Property
correct_testBit NatRepr n
n (BVDomain n
a,Integer
x) Natural
i =
  Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr n
n Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==>
    case NatRepr n -> BVDomain n -> Natural -> Maybe Bool
forall (w :: Nat). NatRepr w -> BVDomain w -> Natural -> Maybe Bool
testBit NatRepr n
n BVDomain n
a Natural
i of
      Just Bool
True  -> Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i)
      Just Bool
False -> Bool -> Bool
Prelude.not (Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
Bits.testBit Integer
x (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i))
      Maybe Bool
Nothing    -> Bool
True

correct_popcnt :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_popcnt :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_popcnt NatRepr n
n (BVDomain n
a,Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n
forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
popcnt NatRepr n
n BVDomain n
a) (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Integer -> Int
forall a. Bits a => a -> Int
Bits.popCount Integer
x))

correct_ctz :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_ctz :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_ctz NatRepr n
n (BVDomain n
a,Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n
forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
ctz NatRepr n
n BVDomain n
a) (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.ctz NatRepr n
n Integer
x)

correct_clz :: (1 <= n) => NatRepr n -> (BVDomain n, Integer) -> Property
correct_clz :: NatRepr n -> (BVDomain n, Integer) -> Property
correct_clz NatRepr n
n (BVDomain n
a,Integer
x) = BVDomain n -> Integer -> Bool
forall (w :: Nat). BVDomain w -> Integer -> Bool
member BVDomain n
a Integer
x Bool -> Bool -> Property
forall t. Verifiable t => Bool -> t -> Property
==> NatRepr n -> BVDomain n -> Integer -> Bool
forall (n :: Nat). NatRepr n -> BVDomain n -> Integer -> Bool
pmember NatRepr n
n (NatRepr n -> BVDomain n -> BVDomain n
forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
clz NatRepr n
n BVDomain n
a) (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
Arith.clz NatRepr n
n Integer
x)