{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.BitPrecise.PEXT_PDEP where
import Data.SBV
import GHC.TypeLits (KnownNat)
pext :: forall n. (KnownNat n, BVIsNonZero n) => SWord n -> SWord n -> SWord n
pext :: forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
SWord n -> SWord n -> SWord n
pext SBV (WordN n)
src SBV (WordN n)
mask = SBV (WordN n)
-> SBV (WordN n) -> SBV (WordN n) -> [SBool] -> SBV (WordN n)
forall {a} {a}.
(Integral a, SFiniteBits a, SFiniteBits a) =>
SBV a -> SBV a -> SBV a -> [SBool] -> SBV a
walk SBV (WordN n)
0 SBV (WordN n)
src SBV (WordN n)
0 (SBV (WordN n) -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV (WordN n)
mask)
where walk :: SBV a -> SBV a -> SBV a -> [SBool] -> SBV a
walk SBV a
dest SBV a
_ SBV a
_ [] = SBV a
dest
walk SBV a
dest SBV a
x SBV a
idx (SBool
m:[SBool]
ms) = SBV a -> SBV a -> SBV a -> [SBool] -> SBV a
walk (SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
m (SBV a -> SBV a -> SBool -> SBV a
forall a.
(SFiniteBits a, Integral a) =>
SBV a -> SBV a -> SBool -> SBV a
sSetBitTo SBV a
dest SBV a
idx (SBV a -> SBool
forall a. SFiniteBits a => SBV a -> SBool
lsb SBV a
x)) SBV a
dest)
(SBV a
x SBV a -> Int -> SBV a
forall a. Bits a => a -> Int -> a
`shiftR` Int
1)
(SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
m (SBV a
idx SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SBV a
1) SBV a
idx)
[SBool]
ms
pdep :: forall n. (KnownNat n, BVIsNonZero n) => SWord n -> SWord n -> SWord n
pdep :: forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
SWord n -> SWord n -> SWord n
pdep SBV (WordN n)
src SBV (WordN n)
mask = SBV (WordN n)
-> SBV (WordN n) -> SBV (WordN n) -> [SBool] -> SBV (WordN n)
forall {a} {a}.
(Integral a, SFiniteBits a, SFiniteBits a) =>
SBV a -> SBV a -> SBV a -> [SBool] -> SBV a
walk SBV (WordN n)
0 SBV (WordN n)
src SBV (WordN n)
0 (SBV (WordN n) -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV (WordN n)
mask)
where walk :: SBV a -> SBV a -> SBV a -> [SBool] -> SBV a
walk SBV a
dest SBV a
_ SBV a
_ [] = SBV a
dest
walk SBV a
dest SBV a
x SBV a
idx (SBool
m:[SBool]
ms) = SBV a -> SBV a -> SBV a -> [SBool] -> SBV a
walk (SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
m (SBV a -> SBV a -> SBool -> SBV a
forall a.
(SFiniteBits a, Integral a) =>
SBV a -> SBV a -> SBool -> SBV a
sSetBitTo SBV a
dest SBV a
idx (SBV a -> SBool
forall a. SFiniteBits a => SBV a -> SBool
lsb SBV a
x)) SBV a
dest)
(SBool -> SBV a -> SBV a -> SBV a
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
m (SBV a
x SBV a -> Int -> SBV a
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) SBV a
x)
(SBV a
idx SBV a -> SBV a -> SBV a
forall a. Num a => a -> a -> a
+ SBV a
1)
[SBool]
ms
extractThenDeposit :: IO ThmResult
= SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do SWord 8
x :: SWord 8 <- String -> Symbolic (SWord 8)
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord String
"x"
SWord 8
m :: SWord 8 <- String -> Symbolic (SWord 8)
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord String
"m"
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ (SWord 8
x SWord 8 -> SWord 8 -> SWord 8
forall a. Bits a => a -> a -> a
.&. SWord 8
m) SWord 8 -> SWord 8 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 8 -> SWord 8 -> SWord 8
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
SWord n -> SWord n -> SWord n
pdep (SWord 8 -> SWord 8 -> SWord 8
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
SWord n -> SWord n -> SWord n
pext SWord 8
x SWord 8
m) SWord 8
m
depositThenExtract :: IO ThmResult
= SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do SWord 8
x :: SWord 8 <- String -> Symbolic (SWord 8)
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord String
"x"
SWord 8
m :: SWord 8 <- String -> Symbolic (SWord 8)
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
String -> Symbolic (SWord n)
sWord String
"m"
let preserved :: SWord 8
preserved = SWord 8
2 SWord 8 -> SBV Word8 -> SWord 8
forall b e. (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
.^ SWord 8 -> SBV Word8
forall a. SFiniteBits a => SBV a -> SBV Word8
sPopCount SWord 8
m SWord 8 -> SWord 8 -> SWord 8
forall a. Num a => a -> a -> a
- SWord 8
1
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ (SWord 8
x SWord 8 -> SWord 8 -> SWord 8
forall a. Bits a => a -> a -> a
.&. SWord 8
preserved) SWord 8 -> SWord 8 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord 8 -> SWord 8 -> SWord 8
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
SWord n -> SWord n -> SWord n
pext (SWord 8 -> SWord 8 -> SWord 8
forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
SWord n -> SWord n -> SWord n
pdep SWord 8
x SWord 8
m) SWord 8
m
pext_2 :: SWord 2 -> SWord 2 -> SWord 2
pext_2 :: SWord 2 -> SWord 2 -> SWord 2
pext_2 = String
-> (SWord 2 -> SWord 2 -> SWord 2) -> SWord 2 -> SWord 2 -> SWord 2
forall a.
(SMTDefinable a, Lambda (SymbolicT IO) a) =>
String -> a -> a
smtFunction String
"pext_2" (forall (n :: Nat).
(KnownNat n, BVIsNonZero n) =>
SWord n -> SWord n -> SWord n
pext @2)