{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
module EVM.Expr where
import Prelude hiding (LT, GT)
import Control.Monad.ST
import Data.Bits hiding (And, Xor)
import Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128))
import Data.List
import Data.Map.Strict qualified as Map
import Data.Maybe (mapMaybe, isJust, fromMaybe)
import Data.Semigroup (Any, Any(..), getAny)
import Data.Vector qualified as V
import Data.Vector (Vector)
import Data.Vector.Mutable qualified as MV
import Data.Vector.Mutable (MVector)
import Data.Vector.Storable qualified as VS
import Data.Vector.Storable.ByteString
import Data.Word (Word8, Word32)
import Witch (unsafeInto, into, tryFrom)
import Data.Containers.ListUtils (nubOrd)
import Control.Monad.State
import Optics.Core
import EVM.Traversals
import EVM.Types
maxLit :: W256
maxLit :: W256
maxLit = W256
0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
op1 :: (Expr EWord -> Expr EWord)
-> (W256 -> W256)
-> Expr EWord -> Expr EWord
op1 :: (Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256) -> Expr 'EWord -> Expr 'EWord
op1 Expr 'EWord -> Expr 'EWord
_ W256 -> W256
concrete (Lit W256
x) = W256 -> Expr 'EWord
Lit (W256 -> W256
concrete W256
x)
op1 Expr 'EWord -> Expr 'EWord
symbolic W256 -> W256
_ Expr 'EWord
x = Expr 'EWord -> Expr 'EWord
symbolic Expr 'EWord
x
op2 :: (Expr EWord -> Expr EWord -> Expr EWord)
-> (W256 -> W256 -> W256)
-> Expr EWord -> Expr EWord -> Expr EWord
op2 :: (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
_ W256 -> W256 -> W256
concrete (Lit W256
x) (Lit W256
y) = W256 -> Expr 'EWord
Lit (W256 -> W256 -> W256
concrete W256
x W256
y)
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
symbolic W256 -> W256 -> W256
_ Expr 'EWord
x Expr 'EWord
y = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
symbolic Expr 'EWord
x Expr 'EWord
y
op3 :: (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord)
-> (W256 -> W256 -> W256 -> W256)
-> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
op3 :: (Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op3 Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
_ W256 -> W256 -> W256 -> W256
concrete (Lit W256
x) (Lit W256
y) (Lit W256
z) = W256 -> Expr 'EWord
Lit (W256 -> W256 -> W256 -> W256
concrete W256
x W256
y W256
z)
op3 Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
symbolic W256 -> W256 -> W256 -> W256
_ Expr 'EWord
x Expr 'EWord
y Expr 'EWord
z = Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
symbolic Expr 'EWord
x Expr 'EWord
y Expr 'EWord
z
normArgs :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord
normArgs :: (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sym W256 -> W256 -> W256
conc Expr 'EWord
l Expr 'EWord
r = case (Expr 'EWord
l, Expr 'EWord
r) of
(Lit W256
_, Expr 'EWord
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
doOp Expr 'EWord
l Expr 'EWord
r
(Expr 'EWord
_, Lit W256
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
doOp Expr 'EWord
r Expr 'EWord
l
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
doOp Expr 'EWord
l Expr 'EWord
r
where
doOp :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
doOp = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sym W256 -> W256 -> W256
conc
add :: Expr EWord -> Expr EWord -> Expr EWord
add :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Add W256 -> W256 -> W256
forall a. Num a => a -> a -> a
(+)
sub :: Expr EWord -> Expr EWord -> Expr EWord
sub :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Sub (-)
mul :: Expr EWord -> Expr EWord -> Expr EWord
mul :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Mul W256 -> W256 -> W256
forall a. Num a => a -> a -> a
(*)
div :: Expr EWord -> Expr EWord -> Expr EWord
div :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
div = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Div (\W256
x W256
y -> if W256
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else W256 -> W256 -> W256
forall a. Integral a => a -> a -> a
Prelude.div W256
x W256
y)
sdiv :: Expr EWord -> Expr EWord -> Expr EWord
sdiv :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sdiv = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SDiv (\W256
x W256
y -> let sx, sy :: Int256
sx :: Int256
sx = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
sy :: Int256
sy = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
in if W256
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else Int256 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int256
sx Int256 -> Int256 -> Int256
forall a. Integral a => a -> a -> a
`quot` Int256
sy))
mod :: Expr EWord -> Expr EWord -> Expr EWord
mod :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mod = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Mod (\W256
x W256
y -> if W256
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else W256
x W256 -> W256 -> W256
forall a. Integral a => a -> a -> a
`Prelude.mod` W256
y)
smod :: Expr EWord -> Expr EWord -> Expr EWord
smod :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
smod = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SMod (\W256
x W256
y ->
let sx, sy :: Int256
sx :: Int256
sx = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
sy :: Int256
sy = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
in if W256
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0
then W256
0
else Int256 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int256
sx Int256 -> Int256 -> Int256
forall a. Integral a => a -> a -> a
`rem` Int256
sy))
addmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
addmod :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
addmod = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op3 Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
AddMod (\W256
x W256
y W256
z ->
if W256
z W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0
then W256
0
else Word512 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word512 -> W256) -> Word512 -> W256
forall a b. (a -> b) -> a -> b
$ (W256 -> Word512
to512 W256
x Word512 -> Word512 -> Word512
forall a. Num a => a -> a -> a
+ W256 -> Word512
to512 W256
y) Word512 -> Word512 -> Word512
forall a. Integral a => a -> a -> a
`Prelude.mod` W256 -> Word512
to512 W256
z)
mulmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
mulmod :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mulmod = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op3 Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
MulMod (\W256
x W256
y W256
z ->
if W256
z W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0
then W256
0
else Word512 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word512 -> W256) -> Word512 -> W256
forall a b. (a -> b) -> a -> b
$ (W256 -> Word512
to512 W256
x Word512 -> Word512 -> Word512
forall a. Num a => a -> a -> a
* W256 -> Word512
to512 W256
y) Word512 -> Word512 -> Word512
forall a. Integral a => a -> a -> a
`Prelude.mod` W256 -> Word512
to512 W256
z)
exp :: Expr EWord -> Expr EWord -> Expr EWord
exp :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
exp = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Exp W256 -> W256 -> W256
forall a b. (Num a, Integral b) => a -> b -> a
(^)
sex :: Expr EWord -> Expr EWord -> Expr EWord
sex :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sex = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SEx (\W256
bytes W256
x ->
if W256
bytes W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
32 then W256
x
else let n :: Int
n = W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
bytes Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
7 in
if W256 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit W256
x Int
n
then W256
x W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
.|. W256 -> W256
forall a. Bits a => a -> a
complement (Int -> W256
forall a. Bits a => Int -> a
bit Int
n W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1)
else W256
x W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
.&. (Int -> W256
forall a. Bits a => Int -> a
bit Int
n W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1))
lt :: Expr EWord -> Expr EWord -> Expr EWord
lt :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
lt = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
LT (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
y then W256
1 else W256
0)
gt :: Expr EWord -> Expr EWord -> Expr EWord
gt :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
gt = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
GT (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
y then W256
1 else W256
0)
leq :: Expr EWord -> Expr EWord -> Expr EWord
leq :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
leq = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
LEq (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
y then W256
1 else W256
0)
geq :: Expr EWord -> Expr EWord -> Expr EWord
geq :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
geq = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
GEq (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
y then W256
1 else W256
0)
slt :: Expr EWord -> Expr EWord -> Expr EWord
slt :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
slt = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SLT (\W256
x W256
y ->
let sx, sy :: Int256
sx :: Int256
sx = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
sy :: Int256
sy = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
in if Int256
sx Int256 -> Int256 -> Bool
forall a. Ord a => a -> a -> Bool
< Int256
sy then W256
1 else W256
0)
sgt :: Expr EWord -> Expr EWord -> Expr EWord
sgt :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sgt = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SGT (\W256
x W256
y ->
let sx, sy :: Int256
sx :: Int256
sx = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
sy :: Int256
sy = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
in if Int256
sx Int256 -> Int256 -> Bool
forall a. Ord a => a -> a -> Bool
> Int256
sy then W256
1 else W256
0)
eq :: Expr EWord -> Expr EWord -> Expr EWord
eq :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
eq = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Eq (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
y then W256
1 else W256
0)
iszero :: Expr EWord -> Expr EWord
iszero :: Expr 'EWord -> Expr 'EWord
iszero = (Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256) -> Expr 'EWord -> Expr 'EWord
op1 Expr 'EWord -> Expr 'EWord
IsZero (\W256
x -> if W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
1 else W256
0)
and :: Expr EWord -> Expr EWord -> Expr EWord
and :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
and = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
And W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
(.&.)
or :: Expr EWord -> Expr EWord -> Expr EWord
or :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
or = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Or W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
(.|.)
xor :: Expr EWord -> Expr EWord -> Expr EWord
xor :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
xor = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Xor W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
Data.Bits.xor
not :: Expr EWord -> Expr EWord
not :: Expr 'EWord -> Expr 'EWord
not = (Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256) -> Expr 'EWord -> Expr 'EWord
op1 Expr 'EWord -> Expr 'EWord
Not W256 -> W256
forall a. Bits a => a -> a
complement
shl :: Expr EWord -> Expr EWord -> Expr EWord
shl :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
shl = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SHL (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
256 then W256
0 else W256 -> Int -> W256
forall a. Bits a => a -> Int -> a
shiftL W256
y (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x))
shr :: Expr EWord -> Expr EWord -> Expr EWord
shr :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
shr = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2
(\Expr 'EWord
x Expr 'EWord
y -> case (Expr 'EWord
x, Expr 'EWord
y) of
(Lit W256
0xe0, ReadWord (Lit W256
idx) Expr 'Buf
buf)
-> [Expr 'Byte] -> Expr 'EWord
joinBytes (
Int -> Expr 'Byte -> [Expr 'Byte]
forall a. Int -> a -> [a]
replicate Int
28 (Word8 -> Expr 'Byte
LitByte Word8
0) [Expr 'Byte] -> [Expr 'Byte] -> [Expr 'Byte]
forall a. Semigroup a => a -> a -> a
<>
[ Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit W256
idx) Expr 'Buf
buf
, Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1) Expr 'Buf
buf
, Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
2) Expr 'Buf
buf
, Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
3) Expr 'Buf
buf])
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SHR Expr 'EWord
x Expr 'EWord
y)
(\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
256 then W256
0 else W256 -> Int -> W256
forall a. Bits a => a -> Int -> a
shiftR W256
y (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x))
sar :: Expr EWord -> Expr EWord -> Expr EWord
sar :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sar = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SAR (\W256
x W256
y ->
let msb :: Bool
msb = W256 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit W256
y Int
255
asSigned :: Int256
asSigned = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y :: Int256
in if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
256 then
if Bool
msb then W256
forall a. Bounded a => a
maxBound else W256
0
else
Int256 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int256 -> W256) -> Int256 -> W256
forall a b. (a -> b) -> a -> b
$ Int256 -> Int -> Int256
forall a. Bits a => a -> Int -> a
shiftR Int256
asSigned (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x))
readByte :: Expr EWord -> Expr Buf -> Expr Byte
readByte :: Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (Lit W256
x) (ConcreteBuf ByteString
b)
= if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (Int
forall a. Bounded a => a
maxBound :: Int) Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ByteString -> Int
BS.length ByteString
b
then Word8 -> Expr 'Byte
LitByte (HasCallStack => ByteString -> Int -> Word8
ByteString -> Int -> Word8
BS.index ByteString
b Int
i)
else Word8 -> Expr 'Byte
LitByte Word8
0x0
where
i :: Int
i :: Int
i = case W256
x of
(W256 (Word256 Word128
_ (Word128 Word64
_ Word64
x'))) -> Word64 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto Word64
x'
readByte i :: Expr 'EWord
i@(Lit W256
x) (WriteByte (Lit W256
idx) Expr 'Byte
val Expr 'Buf
src)
= if W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
idx
then Expr 'Byte
val
else Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
i Expr 'Buf
src
readByte i :: Expr 'EWord
i@(Lit W256
x) (WriteWord (Lit W256
idx) Expr 'EWord
val Expr 'Buf
src)
= if W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
32
then case Expr 'EWord
val of
(Lit W256
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
idx) Expr 'EWord
val
Expr 'EWord
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'Byte
IndexWord (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
idx) Expr 'EWord
val
else Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
i Expr 'Buf
src
readByte i :: Expr 'EWord
i@(Lit W256
x) (CopySlice (Lit W256
srcOffset) (Lit W256
dstOffset) (Lit W256
size) Expr 'Buf
src Expr 'Buf
dst)
= if W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
size
then Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- (W256
dstOffset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
srcOffset)) Expr 'Buf
src
else Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
i Expr 'Buf
dst
readByte i :: Expr 'EWord
i@(Lit W256
x) buf :: Expr 'Buf
buf@(CopySlice Expr 'EWord
_ (Lit W256
dstOffset) (Lit W256
size) Expr 'Buf
_ Expr 'Buf
dst)
= if W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size
then Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
i Expr 'Buf
dst
else Expr 'EWord -> Expr 'Buf -> Expr 'Byte
ReadByte (W256 -> Expr 'EWord
Lit W256
x) Expr 'Buf
buf
readByte Expr 'EWord
i Expr 'Buf
buf = Expr 'EWord -> Expr 'Buf -> Expr 'Byte
ReadByte Expr 'EWord
i Expr 'Buf
buf
readBytes :: Int -> Expr EWord -> Expr Buf -> Expr EWord
readBytes :: Int -> Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readBytes (Int -> Int -> Int
forall a. Ord a => a -> a -> a
Prelude.min Int
32 -> Int
n) Expr 'EWord
idx Expr 'Buf
buf
= [Expr 'Byte] -> Expr 'EWord
joinBytes [Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
idx (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Int -> W256) -> Int -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (Int -> Expr 'EWord) -> Int -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Int
i)) Expr 'Buf
buf | Int
i <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
readWord :: Expr EWord -> Expr Buf -> Expr EWord
readWord :: Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord Expr 'EWord
idx b :: Expr 'Buf
b@(WriteWord Expr 'EWord
idx' Expr 'EWord
val Expr 'Buf
buf)
| Expr 'EWord
idx Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
idx' = Expr 'EWord
val
| Bool
otherwise = case (Expr 'EWord
idx, Expr 'EWord
idx') of
(Lit W256
i, Lit W256
i') ->
if W256
i' W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
i W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
32 Bool -> Bool -> Bool
&& W256
i' W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
i W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= (W256
forall a. Bounded a => a
maxBound :: W256) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
31
then Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord Expr 'EWord
idx Expr 'Buf
buf
else Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWordFromBytes Expr 'EWord
idx Expr 'Buf
b
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWordFromBytes Expr 'EWord
idx Expr 'Buf
b
readWord (Lit W256
idx) b :: Expr 'Buf
b@(CopySlice (Lit W256
srcOff) (Lit W256
dstOff) (Lit W256
size) Expr 'Buf
src Expr 'Buf
dst)
| (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
size Bool -> Bool -> Bool
&& W256
32 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
size W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
srcOff W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff)) Expr 'Buf
src
| (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= (W256
forall a. Bounded a => a
maxBound :: W256) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
31 = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'Buf
dst
| Bool
otherwise = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWordFromBytes (W256 -> Expr 'EWord
Lit W256
idx) Expr 'Buf
b
readWord Expr 'EWord
i Expr 'Buf
b = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWordFromBytes Expr 'EWord
i Expr 'Buf
b
readWordFromBytes :: Expr EWord -> Expr Buf -> Expr EWord
readWordFromBytes :: Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWordFromBytes (Lit W256
idx) (ConcreteBuf ByteString
bs) =
case W256 -> Maybe Int
toInt W256
idx of
Maybe Int
Nothing -> W256 -> Expr 'EWord
Lit W256
0
Just Int
i -> W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
word (ByteString -> W256) -> ByteString -> W256
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
padRight Int
32 (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take Int
32 (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.drop Int
i ByteString
bs
readWordFromBytes i :: Expr 'EWord
i@(Lit W256
idx) Expr 'Buf
buf = let
bytes :: [Expr 'Byte]
bytes = [Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit W256
i') Expr 'Buf
buf | W256
i' <- [W256
idx .. W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
31]]
in if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and ([Bool] -> Bool)
-> ([Expr 'Byte] -> [Bool]) -> [Expr 'Byte] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Bool) -> [Expr 'Byte] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) ([Expr 'Byte] -> Bool) -> [Expr 'Byte] -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bytes
then W256 -> Expr 'EWord
Lit ([Word8] -> W256
bytesToW256 ([Word8] -> W256)
-> ([Expr 'Byte] -> [Word8]) -> [Expr 'Byte] -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'Byte -> Maybe Word8) -> [Expr 'Byte] -> [Word8]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
maybeLitByte ([Expr 'Byte] -> W256) -> [Expr 'Byte] -> W256
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bytes)
else Expr 'EWord -> Expr 'Buf -> Expr 'EWord
ReadWord Expr 'EWord
i Expr 'Buf
buf
readWordFromBytes Expr 'EWord
idx Expr 'Buf
buf = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
ReadWord Expr 'EWord
idx Expr 'Buf
buf
maxBytes :: W256
maxBytes :: W256
maxBytes = Word32 -> W256
forall target source. From source target => source -> target
into (Word32
forall a. Bounded a => a
maxBound :: Word32) W256 -> W256 -> W256
forall a. Integral a => a -> a -> a
`Prelude.div` W256
8
copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf
copySlice :: Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice Expr 'EWord
_ Expr 'EWord
_ (Lit W256
0) (ConcreteBuf ByteString
"") Expr 'Buf
dst = Expr 'Buf
dst
copySlice Expr 'EWord
a Expr 'EWord
b c :: Expr 'EWord
c@(Lit W256
size) d :: Expr 'Buf
d@(ConcreteBuf ByteString
"") e :: Expr 'Buf
e@(ConcreteBuf ByteString
"")
| W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) Word8
0
| Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
e
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset sz :: Expr 'EWord
sz@(Lit W256
size) src :: Expr 'Buf
src@(ConcreteBuf ByteString
"") Expr 'Buf
dst
| W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset (W256 -> Expr 'EWord
Lit W256
size) (ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) Word8
0) Expr 'Buf
dst
| Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset Expr 'EWord
sz Expr 'Buf
src Expr 'Buf
dst
copySlice a :: Expr 'EWord
a@(Lit W256
srcOffset) b :: Expr 'EWord
b@(Lit W256
dstOffset) c :: Expr 'EWord
c@(Lit W256
size) d :: Expr 'Buf
d@(ConcreteBuf ByteString
src) e :: Expr 'Buf
e@(ConcreteBuf ByteString
"")
| W256
srcOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (ByteString -> Int
BS.length ByteString
src), W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) Word8
0
| W256
srcOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (ByteString -> Int
BS.length ByteString
src), W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes, W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes = let
hd :: ByteString
hd = Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
dstOffset) Word8
0
sl :: ByteString
sl = Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) (Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
srcOffset) ByteString
src)
in ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ ByteString
hd ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
sl
| Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
e
copySlice a :: Expr 'EWord
a@(Lit W256
srcOffset) b :: Expr 'EWord
b@(Lit W256
dstOffset) c :: Expr 'EWord
c@(Lit W256
size) d :: Expr 'Buf
d@(ConcreteBuf ByteString
src) e :: Expr 'Buf
e@(ConcreteBuf ByteString
dst)
| W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
, W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes =
let hd :: ByteString
hd = Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
dstOffset) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
dstOffset) ByteString
dst
sl :: ByteString
sl = if W256
srcOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (ByteString -> Int
BS.length ByteString
src)
then Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) Word8
0
else Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) (Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
srcOffset) ByteString
src)
tl :: ByteString
tl = Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
dstOffset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) ByteString
dst
in ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ ByteString
hd ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
sl ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
tl
| Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
e
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset (Lit W256
32) Expr 'Buf
src Expr 'Buf
dst = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord Expr 'EWord
dstOffset (Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord Expr 'EWord
srcOffset Expr 'Buf
src) Expr 'Buf
dst
copySlice s :: Expr 'EWord
s@(Lit W256
srcOffset) d :: Expr 'EWord
d@(Lit W256
dstOffset) sz :: Expr 'EWord
sz@(Lit W256
size) Expr 'Buf
src ds :: Expr 'Buf
ds@(ConcreteBuf ByteString
dst)
| W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes, W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes, W256
srcOffset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ (W256
sizeW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
1) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
srcOffset = let
hd :: ByteString
hd = Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
dstOffset) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
dstOffset) ByteString
dst
sl :: [Expr 'Byte]
sl = [Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit W256
i) Expr 'Buf
src | W256
i <- [W256
srcOffset .. W256
srcOffset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ (W256
size W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1)]]
tl :: ByteString
tl = Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
dstOffset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
size) ByteString
dst
in if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and ([Bool] -> Bool)
-> ([Expr 'Byte] -> [Bool]) -> [Expr 'Byte] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Bool) -> [Expr 'Byte] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) ([Expr 'Byte] -> Bool) -> [Expr 'Byte] -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
sl
then ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ ByteString
hd ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ([Word8] -> ByteString
BS.pack ([Word8] -> ByteString)
-> ([Expr 'Byte] -> [Word8]) -> [Expr 'Byte] -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Maybe Word8) -> [Expr 'Byte] -> [Word8]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
maybeLitByte) ([Expr 'Byte] -> ByteString) -> [Expr 'Byte] -> ByteString
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
sl) ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
tl
else Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
s Expr 'EWord
d Expr 'EWord
sz Expr 'Buf
src Expr 'Buf
ds
| Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
s Expr 'EWord
d Expr 'EWord
sz Expr 'Buf
src Expr 'Buf
ds
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset Expr 'EWord
size Expr 'Buf
src Expr 'Buf
dst = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset Expr 'EWord
size Expr 'Buf
src Expr 'Buf
dst
writeByte :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf
writeByte :: Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
writeByte (Lit W256
offset) (LitByte Word8
val) (ConcreteBuf ByteString
"")
| W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
offset) Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Word8 -> ByteString
BS.singleton Word8
val
writeByte o :: Expr 'EWord
o@(Lit W256
offset) b :: Expr 'Byte
b@(LitByte Word8
byte) buf :: Expr 'Buf
buf@(ConcreteBuf ByteString
src)
| W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ (Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
offset) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
offset) ByteString
src)
ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> [Word8] -> ByteString
BS.pack [Word8
byte]
ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ByteString
src
| Bool
otherwise = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte Expr 'EWord
o Expr 'Byte
b Expr 'Buf
buf
writeByte Expr 'EWord
offset Expr 'Byte
byte Expr 'Buf
src = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte Expr 'EWord
offset Expr 'Byte
byte Expr 'Buf
src
writeWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
writeWord :: Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord o :: Expr 'EWord
o@(Lit W256
offset) (WAddr (LitAddr Addr
val)) b :: Expr 'Buf
b@(ConcreteBuf ByteString
_)
| W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes Bool -> Bool -> Bool
&& W256
offset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord Expr 'EWord
o (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Addr -> W256
forall target source. From source target => source -> target
into Addr
val) Expr 'Buf
b
writeWord (Lit W256
offset) (Lit W256
val) (ConcreteBuf ByteString
"")
| W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes Bool -> Bool -> Bool
&& W256
offset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
offset) Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> W256 -> ByteString
word256Bytes W256
val
writeWord o :: Expr 'EWord
o@(Lit W256
offset) v :: Expr 'EWord
v@(Lit W256
val) buf :: Expr 'Buf
buf@(ConcreteBuf ByteString
src)
| W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes Bool -> Bool -> Bool
&& W256
offset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ (Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
offset) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
offset) ByteString
src)
ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> W256 -> ByteString
word256Bytes W256
val
ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Int -> ByteString -> ByteString
BS.drop ((W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
offset) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
32) ByteString
src
| Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
o Expr 'EWord
v Expr 'Buf
buf
writeWord Expr 'EWord
idx Expr 'EWord
val b :: Expr 'Buf
b@(WriteWord Expr 'EWord
idx' Expr 'EWord
val' Expr 'Buf
buf)
| Expr 'EWord
idx Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
idx' = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
buf
| Bool
otherwise
= case (Expr 'EWord
idx, Expr 'EWord
idx') of
(Lit W256
i, Lit W256
i') -> if W256
i W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
i' W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32
then Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
idx' Expr 'EWord
val' (Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
buf)
else Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
b
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
b
writeWord Expr 'EWord
offset Expr 'EWord
val Expr 'Buf
src = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
offset Expr 'EWord
val Expr 'Buf
src
bufLength :: Expr Buf -> Expr EWord
bufLength :: Expr 'Buf -> Expr 'EWord
bufLength = Map Int (Expr 'Buf) -> Bool -> Expr 'Buf -> Expr 'EWord
bufLengthEnv Map Int (Expr 'Buf)
forall a. Monoid a => a
mempty Bool
False
bufLengthEnv :: Map.Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord
bufLengthEnv :: Map Int (Expr 'Buf) -> Bool -> Expr 'Buf -> Expr 'EWord
bufLengthEnv Map Int (Expr 'Buf)
env Bool
useEnv Expr 'Buf
buf = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go (W256 -> Expr 'EWord
Lit W256
0) Expr 'Buf
buf
where
go :: Expr EWord -> Expr Buf -> Expr EWord
go :: Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go Expr 'EWord
l (ConcreteBuf ByteString
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (W256 -> Expr 'EWord
Lit (Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (Int -> W256) -> (ByteString -> Int) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length (ByteString -> W256) -> ByteString -> W256
forall a b. (a -> b) -> a -> b
$ ByteString
b))
go Expr 'EWord
l (AbstractBuf Text
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'Buf -> Expr 'EWord
BufLength (Text -> Expr 'Buf
AbstractBuf Text
b))
go Expr 'EWord
l (WriteWord Expr 'EWord
idx Expr 'EWord
_ Expr 'Buf
b) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
idx (W256 -> Expr 'EWord
Lit W256
32))) Expr 'Buf
b
go Expr 'EWord
l (WriteByte Expr 'EWord
idx Expr 'Byte
_ Expr 'Buf
b) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
idx (W256 -> Expr 'EWord
Lit W256
1))) Expr 'Buf
b
go Expr 'EWord
l (CopySlice Expr 'EWord
_ Expr 'EWord
dstOffset Expr 'EWord
size Expr 'Buf
_ Expr 'Buf
dst) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
dstOffset Expr 'EWord
size)) Expr 'Buf
dst
go Expr 'EWord
l (GVar (BufVar Int
a)) | Bool
useEnv =
case Int -> Map Int (Expr 'Buf) -> Maybe (Expr 'Buf)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
a Map Int (Expr 'Buf)
env of
Just Expr 'Buf
b -> Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go Expr 'EWord
l Expr 'Buf
b
Maybe (Expr 'Buf)
Nothing -> [Char] -> Expr 'EWord
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot compute length of open expression"
go Expr 'EWord
l (GVar (BufVar Int
a)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'Buf -> Expr 'EWord
BufLength (GVar 'Buf -> Expr 'Buf
forall (a :: EType). GVar a -> Expr a
GVar (Int -> GVar 'Buf
BufVar Int
a)))
minLength :: Map.Map Int (Expr Buf) -> Expr Buf -> Maybe Integer
minLength :: Map Int (Expr 'Buf) -> Expr 'Buf -> Maybe Integer
minLength Map Int (Expr 'Buf)
bufEnv = W256 -> Expr 'Buf -> Maybe Integer
go W256
0
where
go :: W256 -> Expr Buf -> Maybe Integer
go :: W256 -> Expr 'Buf -> Maybe Integer
go W256
l (AbstractBuf Text
_) = if W256
l W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then Maybe Integer
forall a. Maybe a
Nothing else Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ W256 -> Integer
forall target source. From source target => source -> target
into W256
l
go W256
l (ConcreteBuf ByteString
b) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (W256 -> Integer) -> W256 -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Integer
forall target source. From source target => source -> target
into (W256 -> Maybe Integer) -> W256 -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max (Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (Int -> W256) -> (ByteString -> Int) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length (ByteString -> W256) -> ByteString -> W256
forall a b. (a -> b) -> a -> b
$ ByteString
b) W256
l
go W256
l (WriteWord (Lit W256
idx) Expr 'EWord
_ Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go (W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max W256
l (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32)) Expr 'Buf
b
go W256
l (WriteByte (Lit W256
idx) Expr 'Byte
_ Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go (W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max W256
l (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1)) Expr 'Buf
b
go W256
l (CopySlice Expr 'EWord
_ (Lit W256
dstOffset) (Lit W256
size) Expr 'Buf
_ Expr 'Buf
dst) = W256 -> Expr 'Buf -> Maybe Integer
go (W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max (W256
dstOffset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
size) W256
l) Expr 'Buf
dst
go W256
l (WriteWord Expr 'EWord
_ Expr 'EWord
_ Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go W256
l Expr 'Buf
b
go W256
l (WriteByte Expr 'EWord
_ Expr 'Byte
_ Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go W256
l Expr 'Buf
b
go W256
l (CopySlice Expr 'EWord
_ Expr 'EWord
_ Expr 'EWord
_ Expr 'Buf
_ Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go W256
l Expr 'Buf
b
go W256
l (GVar (BufVar Int
a)) = do
Expr 'Buf
b <- Int -> Map Int (Expr 'Buf) -> Maybe (Expr 'Buf)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
a Map Int (Expr 'Buf)
bufEnv
W256 -> Expr 'Buf -> Maybe Integer
go W256
l Expr 'Buf
b
concretePrefix :: Expr Buf -> Vector Word8
concretePrefix :: Expr 'Buf -> Vector Word8
concretePrefix Expr 'Buf
b = (forall s. ST s (MVector s Word8)) -> Vector Word8
forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create ((forall s. ST s (MVector s Word8)) -> Vector Word8)
-> (forall s. ST s (MVector s Word8)) -> Vector Word8
forall a b. (a -> b) -> a -> b
$ do
MVector s Word8
v <- Int -> ST s (MVector (PrimState (ST s)) Word8)
forall (m :: * -> *) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MV.new (Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
1024 Maybe Int
inputLen)
(Int
filled, MVector s Word8
v') <- Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
forall s. Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go Int
0 MVector s Word8
v
MVector s Word8 -> ST s (MVector s Word8)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MVector s Word8 -> ST s (MVector s Word8))
-> MVector s Word8 -> ST s (MVector s Word8)
forall a b. (a -> b) -> a -> b
$ Int -> MVector s Word8 -> MVector s Word8
forall s a. Int -> MVector s a -> MVector s a
MV.take Int
filled MVector s Word8
v'
where
maxIdx :: Num i => i
maxIdx :: forall i. Num i => i
maxIdx = i
500 i -> i -> i
forall a. Num a => a -> a -> a
* (i
10 i -> Int -> i
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
6 :: Int))
inputLen :: Maybe Int
inputLen :: Maybe Int
inputLen = case Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
b of
Lit W256
s -> if W256
s W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
forall i. Num i => i
maxIdx
then [Char] -> Maybe Int
forall a. HasCallStack => [Char] -> a
internalError [Char]
"concretePrefix: input buffer size exceeds 500mb"
else Int -> Maybe Int
forall a. a -> Maybe a
Just (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
s)
Expr 'EWord
_ -> Maybe Int
forall a. Maybe a
Nothing
go :: forall s . Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go :: forall s. Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go Int
i MVector s Word8
v
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
forall i. Num i => i
maxIdx = [Char] -> ST s (Int, MVector s Word8)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"concretePrefix: prefix size exceeds 500mb"
| Just Int
mr <- Maybe Int
inputLen, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
mr = (Int, MVector s Word8) -> ST s (Int, MVector s Word8)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
i, MVector s Word8
v)
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= MVector s Word8 -> Int
forall s a. MVector s a -> Int
MV.length MVector s Word8
v = do
MVector s Word8
v' <- MVector (PrimState (ST s)) Word8
-> Int -> ST s (MVector (PrimState (ST s)) Word8)
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m (MVector (PrimState m) a)
MV.grow MVector s Word8
MVector (PrimState (ST s)) Word8
v (MVector s Word8 -> Int
forall s a. MVector s a -> Int
MV.length MVector s Word8
v)
Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
forall s. Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go Int
i MVector s Word8
v'
| Bool
otherwise = case Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Int -> W256) -> Int -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (Int -> Expr 'EWord) -> Int -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Int
i) Expr 'Buf
b of
LitByte Word8
byte -> do
MVector (PrimState (ST s)) Word8 -> Int -> Word8 -> ST s ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s Word8
MVector (PrimState (ST s)) Word8
v Int
i Word8
byte
Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
forall s. Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) MVector s Word8
v
Expr 'Byte
_ -> (Int, MVector s Word8) -> ST s (Int, MVector s Word8)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
i, MVector s Word8
v)
word256At :: Expr EWord -> Lens (Expr Buf) (Expr Buf) (Expr EWord) (Expr EWord)
word256At :: Expr 'EWord
-> Lens (Expr 'Buf) (Expr 'Buf) (Expr 'EWord) (Expr 'EWord)
word256At Expr 'EWord
i = (Expr 'Buf -> Expr 'EWord)
-> (Expr 'Buf -> Expr 'EWord -> Expr 'Buf)
-> Lens (Expr 'Buf) (Expr 'Buf) (Expr 'EWord) (Expr 'EWord)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens Expr 'Buf -> Expr 'EWord
getter Expr 'Buf -> Expr 'EWord -> Expr 'Buf
setter where
getter :: Expr 'Buf -> Expr 'EWord
getter = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord Expr 'EWord
i
setter :: Expr 'Buf -> Expr 'EWord -> Expr 'Buf
setter Expr 'Buf
m Expr 'EWord
x = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord Expr 'EWord
i Expr 'EWord
x Expr 'Buf
m
take :: W256 -> Expr Buf -> Expr Buf
take :: W256 -> Expr 'Buf -> Expr 'Buf
take W256
n = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
slice (W256 -> Expr 'EWord
Lit W256
0) (W256 -> Expr 'EWord
Lit W256
n)
drop :: W256 -> Expr Buf -> Expr Buf
drop :: W256 -> Expr 'Buf -> Expr 'Buf
drop W256
n Expr 'Buf
buf = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
slice (W256 -> Expr 'EWord
Lit W256
n) (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
buf) (W256 -> Expr 'EWord
Lit W256
n)) Expr 'Buf
buf
slice :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
slice :: Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
slice Expr 'EWord
offset Expr 'EWord
size Expr 'Buf
src = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice Expr 'EWord
offset (W256 -> Expr 'EWord
Lit W256
0) Expr 'EWord
size Expr 'Buf
src Expr 'Buf
forall a. Monoid a => a
mempty
toList :: Expr Buf -> Maybe (V.Vector (Expr Byte))
toList :: Expr 'Buf -> Maybe (Vector (Expr 'Byte))
toList (AbstractBuf Text
_) = Maybe (Vector (Expr 'Byte))
forall a. Maybe a
Nothing
toList (ConcreteBuf ByteString
bs) = Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte))
forall a. a -> Maybe a
Just (Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte)))
-> Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte))
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte] -> Vector (Expr 'Byte)
forall a. [a] -> Vector a
V.fromList ([Expr 'Byte] -> Vector (Expr 'Byte))
-> [Expr 'Byte] -> Vector (Expr 'Byte)
forall a b. (a -> b) -> a -> b
$ Word8 -> Expr 'Byte
LitByte (Word8 -> Expr 'Byte) -> [Word8] -> [Expr 'Byte]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ByteString -> [Word8]
BS.unpack ByteString
bs
toList Expr 'Buf
buf = case Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
buf of
Lit W256
l -> if W256
l W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (Int
forall a. Bounded a => a
maxBound :: Int)
then Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte))
forall a. a -> Maybe a
Just (Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte)))
-> Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte))
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Expr 'Byte) -> Vector (Expr 'Byte)
forall a. Int -> (Int -> a) -> Vector a
V.generate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
l) (\Int
i -> Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto Int
i) Expr 'Buf
buf)
else [Char] -> Maybe (Vector (Expr 'Byte))
forall a. HasCallStack => [Char] -> a
internalError [Char]
"overflow when converting buffer to list"
Expr 'EWord
_ -> Maybe (Vector (Expr 'Byte))
forall a. Maybe a
Nothing
fromList :: V.Vector (Expr Byte) -> Expr Buf
fromList :: Vector (Expr 'Byte) -> Expr 'Buf
fromList Vector (Expr 'Byte)
bs = case Vector Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and ((Expr 'Byte -> Bool) -> Vector (Expr 'Byte) -> Vector Bool
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte Vector (Expr 'Byte)
bs) of
Bool
True -> ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf)
-> (Vector (Expr 'Byte) -> ByteString)
-> Vector (Expr 'Byte)
-> Expr 'Buf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack ([Word8] -> ByteString)
-> (Vector (Expr 'Byte) -> [Word8])
-> Vector (Expr 'Byte)
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Word8 -> [Word8]
forall a. Vector a -> [a]
V.toList (Vector Word8 -> [Word8])
-> (Vector (Expr 'Byte) -> Vector Word8)
-> Vector (Expr 'Byte)
-> [Word8]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'Byte -> Maybe Word8) -> Vector (Expr 'Byte) -> Vector Word8
forall a b. (a -> Maybe b) -> Vector a -> Vector b
V.mapMaybe Expr 'Byte -> Maybe Word8
maybeLitByte (Vector (Expr 'Byte) -> Expr 'Buf)
-> Vector (Expr 'Byte) -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Vector (Expr 'Byte)
bs
Bool
False -> (Expr 'Buf -> Int -> Expr 'Byte -> Expr 'Buf)
-> Expr 'Buf -> Vector (Expr 'Byte) -> Expr 'Buf
forall a b. (a -> Int -> b -> a) -> a -> Vector b -> a
V.ifoldl' Expr 'Buf -> Int -> Expr 'Byte -> Expr 'Buf
applySymWrites (ByteString -> Expr 'Buf
ConcreteBuf ByteString
concreteBytes) Vector (Expr 'Byte)
bs
where
concreteBytes :: ByteString
concreteBytes :: ByteString
concreteBytes = Vector Word8 -> ByteString
forall a. Storable a => Vector a -> ByteString
vectorToByteString (Vector Word8 -> ByteString) -> Vector Word8 -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Word8) -> Vector Word8
forall a. Storable a => Int -> (Int -> a) -> Vector a
VS.generate (Vector (Expr 'Byte) -> Int
forall a. Vector a -> Int
V.length Vector (Expr 'Byte)
bs) (\Int
idx ->
case Vector (Expr 'Byte)
bs Vector (Expr 'Byte) -> Int -> Expr 'Byte
forall a. Vector a -> Int -> a
V.! Int
idx of
LitByte Word8
b -> Word8
b
Expr 'Byte
_ -> Word8
0)
applySymWrites :: Expr Buf -> Int -> Expr Byte -> Expr Buf
applySymWrites :: Expr 'Buf -> Int -> Expr 'Byte -> Expr 'Buf
applySymWrites Expr 'Buf
buf Int
_ (LitByte Word8
_) = Expr 'Buf
buf
applySymWrites Expr 'Buf
buf Int
idx Expr 'Byte
by = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto Int
idx) Expr 'Byte
by Expr 'Buf
buf
instance Semigroup (Expr Buf) where
(ConcreteBuf ByteString
a) <> :: Expr 'Buf -> Expr 'Buf -> Expr 'Buf
<> (ConcreteBuf ByteString
b) = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ ByteString
a ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
b
Expr 'Buf
a <> Expr 'Buf
b = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice (W256 -> Expr 'EWord
Lit W256
0) (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
a) (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
b) Expr 'Buf
b Expr 'Buf
a
instance Monoid (Expr Buf) where
mempty :: Expr 'Buf
mempty = ByteString -> Expr 'Buf
ConcreteBuf ByteString
""
simplifyReads :: Expr a -> Expr a
simplifyReads :: forall (a :: EType). Expr a -> Expr a
simplifyReads = \case
ReadWord (Lit W256
idx) Expr 'Buf
b -> Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord (W256 -> Expr 'EWord
Lit W256
idx) (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
idx W256
32 Expr 'Buf
b)
ReadByte (Lit W256
idx) Expr 'Buf
b -> Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit W256
idx) (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
idx W256
1 Expr 'Buf
b)
Expr a
a -> Expr a
a
stripWrites :: W256 -> W256 -> Expr Buf -> Expr Buf
stripWrites :: W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size = \case
AbstractBuf Text
s -> Text -> Expr 'Buf
AbstractBuf Text
s
ConcreteBuf ByteString
b -> ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ case W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
off W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
size of
Bool
True -> case forall source target.
TryFrom source target =>
source -> Either (TryFromException source target) target
tryFrom @W256 (W256
off W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
size) of
Right Int
n -> Int -> ByteString -> ByteString
BS.take Int
n ByteString
b
Left TryFromException W256 Int
_ -> ByteString
b
Bool
False -> ByteString
b
WriteByte (Lit W256
idx) Expr 'Byte
v Expr 'Buf
prev
-> if W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size
then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev
else Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte (W256 -> Expr 'EWord
Lit W256
idx) Expr 'Byte
v (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev)
WriteWord (Lit W256
idx) Expr 'EWord
v Expr 'Buf
prev
-> if W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= (W256
forall a. Bounded a => a
maxBound :: W256) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
31
then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev
else Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'EWord
v (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev)
CopySlice (Lit W256
srcOff) (Lit W256
dstOff) (Lit W256
size') Expr 'Buf
src Expr 'Buf
dst
-> if W256
dstOff W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& W256
dstOff W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= (W256
forall a. Bounded a => a
maxBound :: W256) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
size' W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1
then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
dst
else Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice (W256 -> Expr 'EWord
Lit W256
srcOff) (W256 -> Expr 'EWord
Lit W256
dstOff) (W256 -> Expr 'EWord
Lit W256
size')
(W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
srcOff W256
size' Expr 'Buf
src)
(W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
dst)
WriteByte Expr 'EWord
i Expr 'Byte
v Expr 'Buf
prev -> Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte Expr 'EWord
i Expr 'Byte
v (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev)
WriteWord Expr 'EWord
i Expr 'EWord
v Expr 'Buf
prev -> Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
i Expr 'EWord
v (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev)
CopySlice Expr 'EWord
srcOff Expr 'EWord
dstOff Expr 'EWord
size' Expr 'Buf
src Expr 'Buf
dst -> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
srcOff Expr 'EWord
dstOff Expr 'EWord
size' Expr 'Buf
src Expr 'Buf
dst
GVar GVar 'Buf
_ -> [Char] -> Expr 'Buf
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Unexpected GVar in stripWrites"
readStorage' :: Expr EWord -> Expr Storage -> Expr EWord
readStorage' :: Expr 'EWord -> Expr 'Storage -> Expr 'EWord
readStorage' Expr 'EWord
loc Expr 'Storage
store = case Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
loc Expr 'Storage
store of
Just Expr 'EWord
v -> Expr 'EWord
v
Maybe (Expr 'EWord)
Nothing -> W256 -> Expr 'EWord
Lit W256
0
readStorage :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
readStorage :: Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
w Expr 'Storage
st = Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
w) Expr 'Storage
st
where
go :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
go :: Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
_ (GVar GVar 'Storage
_) = [Char] -> Maybe (Expr 'EWord)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Can't read from a GVar"
go Expr 'EWord
slot s :: Expr 'Storage
s@(AbstractStore Expr 'EAddr
_ Maybe W256
_) = Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
Just (Expr 'EWord -> Maybe (Expr 'EWord))
-> Expr 'EWord -> Maybe (Expr 'EWord)
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
slot Expr 'Storage
s
go (Lit W256
l) (ConcreteStore Map W256 W256
s) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> Maybe W256 -> Maybe (Expr 'EWord)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> W256 -> Map W256 W256 -> Maybe W256
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup W256
l Map W256 W256
s
go Expr 'EWord
slot store :: Expr 'Storage
store@(ConcreteStore Map W256 W256
_) = Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
Just (Expr 'EWord -> Maybe (Expr 'EWord))
-> Expr 'EWord -> Maybe (Expr 'EWord)
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
slot Expr 'Storage
store
go Expr 'EWord
slot s :: Expr 'Storage
s@(SStore Expr 'EWord
prevSlot Expr 'EWord
val Expr 'Storage
prev) = case (Expr 'EWord
prevSlot, Expr 'EWord
slot) of
(Expr 'EWord, Expr 'EWord)
_ | Expr 'EWord
prevSlot Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
slot -> Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
Just Expr 'EWord
val
(Lit W256
_, Lit W256
_) -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(MappingSlot ByteString
idA Expr 'EWord
_, MappingSlot ByteString
idB Expr 'EWord
_) | ByteString -> ByteString -> Bool
idsDontMatch ByteString
idA ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(MappingSlot ByteString
_ Expr 'EWord
keyA, MappingSlot ByteString
_ Expr 'EWord
keyB) | Expr 'EWord -> Expr 'EWord -> Bool
forall (a :: EType). Expr a -> Expr a -> Bool
surelyNotEq Expr 'EWord
keyA Expr 'EWord
keyB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotWithOffset ByteString
idA Expr 'EWord
_, Expr 'EWord
Keccak64Bytes) | ByteString -> Int
BS.length ByteString
idA Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotZero ByteString
idA, Expr 'EWord
Keccak64Bytes) | ByteString -> Int
BS.length ByteString
idA Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Expr 'EWord
Keccak64Bytes, ArraySlotWithOffset ByteString
idA Expr 'EWord
_) | ByteString -> Int
BS.length ByteString
idA Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Expr 'EWord
Keccak64Bytes, ArraySlotZero ByteString
idA) | ByteString -> Int
BS.length ByteString
idA Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Lit W256
a, Keccak Expr 'Buf
_) | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Keccak Expr 'Buf
_, Lit W256
a) | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Lit W256
a, Add (Lit W256
b) (Keccak Expr 'Buf
_) ) | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256, W256
b W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxW32 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Add (Lit W256
a) (Keccak Expr 'Buf
_) , Lit W256
b) | W256
b W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256, W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxW32 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Add (Lit W256
a2) (Keccak Expr 'Buf
_), Add (Lit W256
b2) (Keccak Expr 'Buf
_)) | W256
a2 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
b2, W256 -> W256
forall a. Num a => a -> a
abs(W256
a2W256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
b2) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Add (Lit W256
a2) (Keccak Expr 'Buf
_), (Keccak Expr 'Buf
_)) | W256
a2 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
0, W256
a2 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
((Keccak Expr 'Buf
_), Add (Lit W256
b2) (Keccak Expr 'Buf
_)) | W256
b2 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
0, W256
b2 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotZero ByteString
idA, ArraySlotZero ByteString
idB) | ByteString
idA ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotZero ByteString
idA, ArraySlotWithOffset ByteString
idB Expr 'EWord
_) | ByteString
idA ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotZero ByteString
_, ArraySlotWithOffset ByteString
_ (Lit W256
offB)) | W256
offB W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
0 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotWithOffset ByteString
idA Expr 'EWord
_, ArraySlotZero ByteString
idB) | ByteString
idA ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotWithOffset ByteString
_ (Lit W256
offA), ArraySlotZero ByteString
_) | W256
offA W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
0 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotWithOffset ByteString
idA Expr 'EWord
_, ArraySlotWithOffset ByteString
idB Expr 'EWord
_) | ByteString
idA ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(ArraySlotWithOffset ByteString
_ Expr 'EWord
offA, ArraySlotWithOffset ByteString
_ Expr 'EWord
offB) | Expr 'EWord -> Expr 'EWord -> Bool
forall (a :: EType). Expr a -> Expr a -> Bool
surelyNotEq Expr 'EWord
offA Expr 'EWord
offB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
Just (Expr 'EWord -> Maybe (Expr 'EWord))
-> Expr 'EWord -> Maybe (Expr 'EWord)
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
slot Expr 'Storage
s
surelyNotEq :: Expr a -> Expr a -> Bool
surelyNotEq :: forall (a :: EType). Expr a -> Expr a -> Bool
surelyNotEq (Lit W256
a) (Lit W256
b) = W256
a W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
b
surelyNotEq (Add (Lit W256
l1) Expr 'EWord
v1) (Add (Lit W256
l2) Expr 'EWord
v2) = W256
l1 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
l2 Bool -> Bool -> Bool
&& Expr 'EWord
v1 Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
v2
surelyNotEq Expr a
v1 (Add (Lit W256
l2) Expr 'EWord
v2) = W256
l2 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
0 Bool -> Bool -> Bool
&& Expr a
v1 Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
Expr 'EWord
v2
surelyNotEq (Add (Lit W256
l1) Expr 'EWord
v1) Expr a
v2 = W256
l1 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
0 Bool -> Bool -> Bool
&& Expr 'EWord
v1 Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
Expr 'EWord
v2
surelyNotEq Expr a
_ Expr a
_ = Bool
False
maxW32 :: W256
maxW32 :: W256
maxW32 = Word32 -> W256
forall target source. From source target => source -> target
into (Word32
forall a. Bounded a => a
maxBound :: Word32)
pattern MappingSlot :: ByteString -> Expr EWord -> Expr EWord
pattern $mMappingSlot :: forall {r}.
Expr 'EWord
-> (ByteString -> Expr 'EWord -> r) -> ((# #) -> r) -> r
$bMappingSlot :: ByteString -> Expr 'EWord -> Expr 'EWord
MappingSlot id key = Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) (WriteWord (Lit 0) key (ConcreteBuf id)) (ConcreteBuf ""))
pattern Keccak64Bytes :: Expr EWord
pattern $mKeccak64Bytes :: forall {r}. Expr 'EWord -> ((# #) -> r) -> ((# #) -> r) -> r
Keccak64Bytes <- Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) _ (ConcreteBuf ""))
pattern ArraySlotWithOffset :: ByteString -> Expr EWord -> Expr EWord
pattern $mArraySlotWithOffset :: forall {r}.
Expr 'EWord
-> (ByteString -> Expr 'EWord -> r) -> ((# #) -> r) -> r
$bArraySlotWithOffset :: ByteString -> Expr 'EWord -> Expr 'EWord
ArraySlotWithOffset id offset = Add (Keccak (ConcreteBuf id)) offset
pattern ArraySlotZero :: ByteString -> Expr EWord
pattern $mArraySlotZero :: forall {r}. Expr 'EWord -> (ByteString -> r) -> ((# #) -> r) -> r
$bArraySlotZero :: ByteString -> Expr 'EWord
ArraySlotZero id = Keccak (ConcreteBuf id)
idsDontMatch :: ByteString -> ByteString -> Bool
idsDontMatch :: ByteString -> ByteString -> Bool
idsDontMatch ByteString
a ByteString
b = ByteString -> Int
BS.length ByteString
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
64 Bool -> Bool -> Bool
&& ByteString -> Int
BS.length ByteString
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
64 Bool -> Bool -> Bool
&& ByteString -> ByteString -> Bool
diff32to64Byte ByteString
a ByteString
b
where
diff32to64Byte :: ByteString -> ByteString -> Bool
diff32to64Byte :: ByteString -> ByteString -> Bool
diff32to64Byte ByteString
x ByteString
y = ByteString
x32 ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
y32
where
x32 :: ByteString
x32 = Int -> ByteString -> ByteString
BS.take Int
32 (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.drop Int
32 ByteString
x
y32 :: ByteString
y32 = Int -> ByteString -> ByteString
BS.take Int
32 (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.drop Int
32 ByteString
y
slotPos :: Word8 -> ByteString
slotPos :: Word8 -> ByteString
slotPos Word8
pos = [Word8] -> ByteString
BS.pack ((Int -> Word8 -> [Word8]
forall a. Int -> a -> [a]
replicate Int
31 (Word8
0::Word8))[Word8] -> [Word8] -> [Word8]
forall a. [a] -> [a] -> [a]
++[Word8
pos])
structureArraySlots :: Expr a -> Expr a
structureArraySlots :: forall (a :: EType). Expr a -> Expr a
structureArraySlots Expr a
e = (forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go Expr a
e
where
go :: Expr a -> Expr a
go :: forall (a :: EType). Expr a -> Expr a
go orig :: Expr a
orig@(Lit W256
key) = case W256 -> Maybe (Word8, W256)
litToArrayPreimage W256
key of
Just (Word8
array, W256
offset) -> ByteString -> Expr 'EWord -> Expr 'EWord
ArraySlotWithOffset (Word8 -> ByteString
slotPos Word8
array) (W256 -> Expr 'EWord
Lit W256
offset)
Maybe (Word8, W256)
_ -> Expr a
orig
go Expr a
a = Expr a
a
litToArrayPreimage :: W256 -> Maybe (Word8, W256)
litToArrayPreimage :: W256 -> Maybe (Word8, W256)
litToArrayPreimage W256
val = [(W256, Word8)] -> Maybe (Word8, W256)
go [(W256, Word8)]
preImages
where
go :: [(W256, Word8)] -> Maybe (Word8, W256)
go :: [(W256, Word8)] -> Maybe (Word8, W256)
go ((W256
image, Word8
preimage):[(W256, Word8)]
ax) = if W256
val W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
image Bool -> Bool -> Bool
&& W256
valW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
image W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
255 then (Word8, W256) -> Maybe (Word8, W256)
forall a. a -> Maybe a
Just (Word8
preimage, W256
valW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
image)
else [(W256, Word8)] -> Maybe (Word8, W256)
go [(W256, Word8)]
ax
go [] = Maybe (Word8, W256)
forall a. Maybe a
Nothing
writeStorage :: Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage
writeStorage :: Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage k :: Expr 'EWord
k@(Lit W256
key) v :: Expr 'EWord
v@(Lit W256
val) Expr 'Storage
store = case Expr 'Storage
store of
ConcreteStore Map W256 W256
s -> Map W256 W256 -> Expr 'Storage
ConcreteStore (W256 -> W256 -> Map W256 W256 -> Map W256 W256
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert W256
key W256
val Map W256 W256
s)
Expr 'Storage
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
k Expr 'EWord
v Expr 'Storage
store
writeStorage Expr 'EWord
key Expr 'EWord
val store :: Expr 'Storage
store@(SStore Expr 'EWord
key' Expr 'EWord
val' Expr 'Storage
prev)
= if Expr 'EWord
key Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
key'
then Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key Expr 'EWord
val Expr 'Storage
prev
else case (Expr 'EWord
key, Expr 'EWord
key') of
(Lit W256
k, Lit W256
k') -> if W256
k W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
k'
then Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key' Expr 'EWord
val' (Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage Expr 'EWord
key Expr 'EWord
val Expr 'Storage
prev)
else Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
writeStorage Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store = Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
getAddr :: Expr Storage -> Maybe (Expr EAddr)
getAddr :: Expr 'Storage -> Maybe (Expr 'EAddr)
getAddr (SStore Expr 'EWord
_ Expr 'EWord
_ Expr 'Storage
p) = Expr 'Storage -> Maybe (Expr 'EAddr)
getAddr Expr 'Storage
p
getAddr (AbstractStore Expr 'EAddr
a Maybe W256
_) = Expr 'EAddr -> Maybe (Expr 'EAddr)
forall a. a -> Maybe a
Just Expr 'EAddr
a
getAddr (ConcreteStore Map W256 W256
_) = Maybe (Expr 'EAddr)
forall a. Maybe a
Nothing
getAddr (GVar GVar 'Storage
_) = [Char] -> Maybe (Expr 'EAddr)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot determine addr of a GVar"
getLogicalIdx :: Expr Storage -> Maybe W256
getLogicalIdx :: Expr 'Storage -> Maybe W256
getLogicalIdx (SStore Expr 'EWord
_ Expr 'EWord
_ Expr 'Storage
p) = Expr 'Storage -> Maybe W256
getLogicalIdx Expr 'Storage
p
getLogicalIdx (AbstractStore Expr 'EAddr
_ Maybe W256
idx) = Maybe W256
idx
getLogicalIdx (ConcreteStore Map W256 W256
_) = Maybe W256
forall a. Maybe a
Nothing
getLogicalIdx (GVar GVar 'Storage
_) = [Char] -> Maybe W256
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot determine addr of a GVar"
data StorageType = SmallSlot | Array | Map | Mixed | UNK
deriving (Int -> StorageType -> ShowS
[StorageType] -> ShowS
StorageType -> [Char]
(Int -> StorageType -> ShowS)
-> (StorageType -> [Char])
-> ([StorageType] -> ShowS)
-> Show StorageType
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StorageType -> ShowS
showsPrec :: Int -> StorageType -> ShowS
$cshow :: StorageType -> [Char]
show :: StorageType -> [Char]
$cshowList :: [StorageType] -> ShowS
showList :: [StorageType] -> ShowS
Show, StorageType -> StorageType -> Bool
(StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool) -> Eq StorageType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StorageType -> StorageType -> Bool
== :: StorageType -> StorageType -> Bool
$c/= :: StorageType -> StorageType -> Bool
/= :: StorageType -> StorageType -> Bool
Eq)
safeToDecompose :: Expr a -> Bool
safeToDecompose :: forall (a :: EType). Expr a -> Bool
safeToDecompose Expr a
inp = StorageType
result StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
/= StorageType
Mixed
where
result :: StorageType
result = State StorageType () -> StorageType -> StorageType
forall s a. State s a -> s -> s
execState (Expr a -> State StorageType ()
forall (a :: EType). Expr a -> State StorageType ()
safeToDecomposeRunner Expr a
inp) StorageType
UNK
safeToDecomposeRunner :: forall a. Expr a -> State StorageType ()
safeToDecomposeRunner :: forall (a :: EType). Expr a -> State StorageType ()
safeToDecomposeRunner Expr a
a = Expr a -> State StorageType ()
forall (a :: EType). Expr a -> State StorageType ()
go Expr a
a
go :: forall b. Expr b -> State StorageType ()
go :: forall (a :: EType). Expr a -> State StorageType ()
go e :: Expr b
e@(SLoad (MappingSlot {}) Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setMap Expr b
e
go e :: Expr b
e@(SLoad (ArraySlotZero {}) Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setArray Expr b
e
go e :: Expr b
e@(SLoad (ArraySlotWithOffset {}) Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setArray Expr b
e
go e :: Expr b
e@(SLoad (Lit W256
x) Expr 'Storage
_) | W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setSmall Expr b
e
go e :: Expr b
e@(SLoad Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setMixed Expr b
e
go e :: Expr b
e@(SStore (MappingSlot {}) Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setMap Expr b
e
go e :: Expr b
e@(SStore (ArraySlotZero {}) Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setArray Expr b
e
go e :: Expr b
e@(SStore (ArraySlotWithOffset {}) Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setArray Expr b
e
go e :: Expr b
e@(SStore (Lit W256
x) Expr 'EWord
_ Expr 'Storage
_) | W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setSmall Expr b
e
go e :: Expr b
e@(SStore Expr 'EWord
_ Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setMixed Expr b
e
go Expr b
_ = () -> State StorageType ()
forall a. a -> StateT StorageType Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
setMixed :: p -> m ()
setMixed p
_ = do
StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
setMap :: p -> m ()
setMap p
_ = do
StorageType
s <- m StorageType
forall s (m :: * -> *). MonadState s m => m s
get
case StorageType
s of
StorageType
Array -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
StorageType
SmallSlot -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
StorageType
UNK -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Map
StorageType
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
setArray :: p -> m ()
setArray p
_ = do
StorageType
s <- m StorageType
forall s (m :: * -> *). MonadState s m => m s
get
case StorageType
s of
StorageType
Map -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
StorageType
SmallSlot -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
StorageType
UNK -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Array
StorageType
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
setSmall :: p -> m ()
setSmall p
_ = do
StorageType
s <- m StorageType
forall s (m :: * -> *). MonadState s m => m s
get
case StorageType
s of
StorageType
Map -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
StorageType
Array -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
StorageType
UNK -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
SmallSlot
StorageType
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
decomposeStorage :: Expr a -> Maybe (Expr a)
decomposeStorage :: forall (a :: EType). Expr a -> Maybe (Expr a)
decomposeStorage = Expr a -> Maybe (Expr a)
forall (a :: EType). Expr a -> Maybe (Expr a)
go
where
go :: Expr a -> Maybe (Expr a)
go :: forall (a :: EType). Expr a -> Maybe (Expr a)
go e :: Expr a
e@(SLoad Expr 'EWord
origKey Expr 'Storage
store) = if Bool -> Bool
Prelude.not (Expr a -> Bool
forall (a :: EType). Expr a -> Bool
safeToDecompose Expr a
e) then Maybe (Expr a)
forall a. Maybe a
Nothing else Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
tryRewrite Expr 'EWord
origKey Expr 'Storage
store
go Expr a
e = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
e
tryRewrite :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
tryRewrite :: Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
tryRewrite Expr 'EWord
origKey Expr 'Storage
store = case Expr 'EWord -> Maybe (Maybe W256, Expr 'EWord)
inferLogicalIdx Expr 'EWord
origKey of
Just (Maybe W256
idx, Expr 'EWord
key) -> do
Expr 'Storage
base <- Maybe W256 -> Expr 'Storage -> Maybe (Expr 'Storage)
setLogicalBase Maybe W256
idx Expr 'Storage
store
Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
key Expr 'Storage
base)
Maybe (Maybe W256, Expr 'EWord)
_ -> Maybe (Expr 'EWord)
forall a. Maybe a
Nothing
inferLogicalIdx :: Expr EWord -> Maybe (Maybe W256, Expr EWord)
inferLogicalIdx :: Expr 'EWord -> Maybe (Maybe W256, Expr 'EWord)
inferLogicalIdx = \case
Lit W256
a | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
256 -> Maybe (Maybe W256, Expr 'EWord)
forall a. Maybe a
Nothing
Lit W256
a -> (Maybe W256, Expr 'EWord) -> Maybe (Maybe W256, Expr 'EWord)
forall a. a -> Maybe a
Just (Maybe W256
forall a. Maybe a
Nothing, W256 -> Expr 'EWord
Lit W256
a)
(MappingSlot ByteString
idx Expr 'EWord
key) | ByteString -> Int
BS.length ByteString
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
64 -> (Maybe W256, Expr 'EWord) -> Maybe (Maybe W256, Expr 'EWord)
forall a. a -> Maybe a
Just (W256 -> Maybe W256
forall a. a -> Maybe a
Just (W256 -> Maybe W256) -> W256 -> Maybe W256
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
idxToWord ByteString
idx, Expr 'EWord
key)
(ArraySlotWithOffset ByteString
idx Expr 'EWord
offset) | ByteString -> Int
BS.length ByteString
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
32 -> (Maybe W256, Expr 'EWord) -> Maybe (Maybe W256, Expr 'EWord)
forall a. a -> Maybe a
Just (W256 -> Maybe W256
forall a. a -> Maybe a
Just (W256 -> Maybe W256) -> W256 -> Maybe W256
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
idxToWord64 ByteString
idx, Expr 'EWord
offset)
(ArraySlotZero ByteString
idx) | ByteString -> Int
BS.length ByteString
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
32 -> (Maybe W256, Expr 'EWord) -> Maybe (Maybe W256, Expr 'EWord)
forall a. a -> Maybe a
Just (W256 -> Maybe W256
forall a. a -> Maybe a
Just (W256 -> Maybe W256) -> W256 -> Maybe W256
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
idxToWord64 ByteString
idx, W256 -> Expr 'EWord
Lit W256
0)
Expr 'EWord
_ -> Maybe (Maybe W256, Expr 'EWord)
forall a. Maybe a
Nothing
idxToWord :: ByteString -> W256
idxToWord :: ByteString -> W256
idxToWord = Word256 -> W256
W256 (Word256 -> W256) -> (ByteString -> Word256) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Word256
word256 (ByteString -> Word256)
-> (ByteString -> ByteString) -> ByteString -> Word256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> ByteString -> ByteString
BS.takeEnd Int
32)
idxToWord64 :: ByteString -> W256
idxToWord64 :: ByteString -> W256
idxToWord64 = Word256 -> W256
W256 (Word256 -> W256) -> (ByteString -> Word256) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Word256
word256 (ByteString -> Word256)
-> (ByteString -> ByteString) -> ByteString -> Word256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> ByteString -> ByteString
BS.takeEnd Int
64)
setLogicalBase :: Maybe W256 -> Expr Storage -> Maybe (Expr Storage)
setLogicalBase :: Maybe W256 -> Expr 'Storage -> Maybe (Expr 'Storage)
setLogicalBase Maybe W256
idx (AbstractStore Expr 'EAddr
addr Maybe W256
_) = Expr 'Storage -> Maybe (Expr 'Storage)
forall a. a -> Maybe a
Just (Expr 'Storage -> Maybe (Expr 'Storage))
-> Expr 'Storage -> Maybe (Expr 'Storage)
forall a b. (a -> b) -> a -> b
$ Expr 'EAddr -> Maybe W256 -> Expr 'Storage
AbstractStore Expr 'EAddr
addr Maybe W256
idx
setLogicalBase Maybe W256
idx (SStore Expr 'EWord
i Expr 'EWord
v Expr 'Storage
s) = do
Expr 'Storage
b <- Maybe W256 -> Expr 'Storage -> Maybe (Expr 'Storage)
setLogicalBase Maybe W256
idx Expr 'Storage
s
(Maybe W256
idx2, Expr 'EWord
key2) <- Expr 'EWord -> Maybe (Maybe W256, Expr 'EWord)
inferLogicalIdx Expr 'EWord
i
if Maybe W256
idx Maybe W256 -> Maybe W256 -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe W256
idx2 then Expr 'Storage -> Maybe (Expr 'Storage)
forall a. a -> Maybe a
Just (Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key2 Expr 'EWord
v Expr 'Storage
b) else Maybe (Expr 'Storage)
forall a. Maybe a
Nothing
setLogicalBase Maybe W256
_ s :: Expr 'Storage
s@(ConcreteStore Map W256 W256
m) | Map W256 W256 -> Bool
forall k a. Map k a -> Bool
Map.null Map W256 W256
m = Expr 'Storage -> Maybe (Expr 'Storage)
forall a. a -> Maybe a
Just Expr 'Storage
s
setLogicalBase Maybe W256
_ (ConcreteStore Map W256 W256
store) =
if (W256 -> Bool) -> [W256] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256) (Map W256 W256 -> [W256]
forall k a. Map k a -> [k]
Map.keys Map W256 W256
store)
then Expr 'Storage -> Maybe (Expr 'Storage)
forall a. a -> Maybe a
Just (Map W256 W256 -> Expr 'Storage
ConcreteStore Map W256 W256
forall a. Monoid a => a
mempty)
else Maybe (Expr 'Storage)
forall a. Maybe a
Nothing
setLogicalBase Maybe W256
_ (GVar GVar 'Storage
_) = [Char] -> Maybe (Expr 'Storage)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Unexpected GVar"
simplify :: Expr a -> Expr a
simplify :: forall (a :: EType). Expr a -> Expr a
simplify Expr a
e = if ((forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go Expr a
e Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
e)
then Expr a
e
else Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplify ((forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go (Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
structureArraySlots Expr a
e))
where
go :: Expr a -> Expr a
go :: forall (a :: EType). Expr a -> Expr a
go (Failure [Prop]
a Traces
b EvmError
c) = [Prop] -> Traces -> EvmError -> Expr 'End
Failure ([Prop] -> [Prop]
simplifyProps [Prop]
a) Traces
b EvmError
c
go (Partial [Prop]
a Traces
b PartialExec
c) = [Prop] -> Traces -> PartialExec -> Expr 'End
Partial ([Prop] -> [Prop]
simplifyProps [Prop]
a) Traces
b PartialExec
c
go (Success [Prop]
a Traces
b Expr 'Buf
c Map (Expr 'EAddr) (Expr 'EContract)
d) = [Prop]
-> Traces
-> Expr 'Buf
-> Map (Expr 'EAddr) (Expr 'EContract)
-> Expr 'End
Success ([Prop] -> [Prop]
simplifyProps [Prop]
a) Traces
b Expr 'Buf
c Map (Expr 'EAddr) (Expr 'EContract)
d
go (CopySlice (Lit W256
0x0) (Lit W256
0x0) (Lit W256
0x0) Expr 'Buf
_ Expr 'Buf
dst) = Expr a
Expr 'Buf
dst
go (Keccak (ConcreteBuf ByteString
bs)) = case ByteString -> Int
BS.length ByteString
bs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
64 of
Bool
True -> ByteString -> Expr 'EWord -> Expr 'EWord
MappingSlot ByteString
bs (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
word ByteString
bs)
Bool
False -> Expr 'Buf -> Expr 'EWord
Keccak (ByteString -> Expr 'Buf
ConcreteBuf ByteString
bs)
go (SLoad Expr 'EWord
slot Expr 'Storage
store) = Expr 'EWord -> Expr 'Storage -> Expr 'EWord
readStorage' Expr 'EWord
slot Expr 'Storage
store
go (SStore Expr 'EWord
slot Expr 'EWord
val Expr 'Storage
store) = Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage Expr 'EWord
slot Expr 'EWord
val Expr 'Storage
store
go o :: Expr a
o@(ReadWord (Lit W256
_) Expr 'Buf
_) = Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplifyReads Expr a
o
go (ReadWord Expr 'EWord
idx Expr 'Buf
buf) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord Expr 'EWord
idx Expr 'Buf
buf
go o :: Expr a
o@(ReadByte (Lit W256
_) Expr 'Buf
_) = Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplifyReads Expr a
o
go (ReadByte Expr 'EWord
idx Expr 'Buf
buf) = Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
idx Expr 'Buf
buf
go (BufLength Expr 'Buf
buf) = Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
buf
go o :: Expr a
o@(WriteWord (Lit W256
idx) Expr 'EWord
val (ConcreteBuf ByteString
b))
| W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= (Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'EWord
val (
ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$
(Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
idx) (Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
idx) ByteString
b))
ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> (Int -> Word8 -> ByteString
BS.replicate Int
32 Word8
0)
ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> (Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
32) ByteString
b)))
| Bool
otherwise = Expr a
o
go (WriteWord Expr 'EWord
a Expr 'EWord
b Expr 'Buf
c) = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord Expr 'EWord
a Expr 'EWord
b Expr 'Buf
c
go (WriteByte Expr 'EWord
a Expr 'Byte
b Expr 'Buf
c) = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
writeByte Expr 'EWord
a Expr 'Byte
b Expr 'Buf
c
go orig :: Expr a
orig@(CopySlice srcOff :: Expr 'EWord
srcOff@(Lit W256
n) Expr 'EWord
dstOff size :: Expr 'EWord
size@(Lit W256
sz)
(WriteWord Expr 'EWord
wOff Expr 'EWord
value (ConcreteBuf ByteString
buf)) Expr 'Buf
dst)
| W256
nW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
sz W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
n
, W256
nW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
sz W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
sz
, W256
nW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
sz W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
maxBytes
= (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
srcOff Expr 'EWord
dstOff Expr 'EWord
size
(Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
wOff Expr 'EWord
value (ByteString -> Expr 'Buf
ConcreteBuf ByteString
simplifiedBuf)) Expr 'Buf
dst)
| Bool
otherwise = Expr a
orig
where simplifiedBuf :: ByteString
simplifiedBuf = Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto (W256
nW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
sz)) ByteString
buf
go (CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
f) = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
f
go (IndexWord Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord Expr 'EWord
a Expr 'EWord
b
go (EVM.Types.LT (Lit W256
a) (Lit W256
b))
| W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
b = W256 -> Expr 'EWord
Lit W256
1
| Bool
otherwise = W256 -> Expr 'EWord
Lit W256
0
go (EVM.Types.LT Expr 'EWord
_ (Lit W256
0)) = W256 -> Expr 'EWord
Lit W256
0
go (EVM.Types.GT Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
lt Expr 'EWord
b Expr 'EWord
a
go (EVM.Types.GEq Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
leq Expr 'EWord
b Expr 'EWord
a
go (EVM.Types.LEq Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord
EVM.Types.IsZero (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
gt Expr 'EWord
a Expr 'EWord
b)
go (IsZero Expr 'EWord
a) = Expr 'EWord -> Expr 'EWord
iszero Expr 'EWord
a
go (SLT a :: Expr 'EWord
a@(Lit W256
_) b :: Expr 'EWord
b@(Lit W256
_)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
slt Expr 'EWord
a Expr 'EWord
b
go (SGT Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SLT Expr 'EWord
b Expr 'EWord
a
go (Eq (Lit W256
a) (Lit W256
b))
| W256
a W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
b = W256 -> Expr 'EWord
Lit W256
1
| Bool
otherwise = W256 -> Expr 'EWord
Lit W256
0
go (Eq (Lit W256
0) (Sub Expr 'EWord
a Expr 'EWord
b)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
eq Expr 'EWord
a Expr 'EWord
b
go (Eq Expr 'EWord
a Expr 'EWord
b)
| Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = W256 -> Expr 'EWord
Lit W256
1
| Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
eq Expr 'EWord
a Expr 'EWord
b
go (ITE (Lit W256
x) Expr 'End
a Expr 'End
b)
| W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr a
Expr 'End
b
| Bool
otherwise = Expr a
Expr 'End
a
go (And (Lit W256
0xffffffffffffffffffffffffffffffffffffffff) a :: Expr 'EWord
a@(WAddr Expr 'EAddr
_)) = Expr a
Expr 'EWord
a
go (WAddr (LitAddr Addr
a)) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Addr -> W256
forall target source. From source target => source -> target
into Addr
a
go (Div o1 :: Expr 'EWord
o1@(Lit W256
_) o2 :: Expr 'EWord
o2@(Lit W256
_)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.div Expr 'EWord
o1 Expr 'EWord
o2
go (SDiv o1 :: Expr 'EWord
o1@(Lit W256
_) o2 :: Expr 'EWord
o2@(Lit W256
_)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.sdiv Expr 'EWord
o1 Expr 'EWord
o2
go (Mod o1 :: Expr 'EWord
o1@(Lit W256
_) o2 :: Expr 'EWord
o2@(Lit W256
_)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.mod Expr 'EWord
o1 Expr 'EWord
o2
go (SMod o1 :: Expr 'EWord
o1@(Lit W256
_) o2 :: Expr 'EWord
o2@(Lit W256
_)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.smod Expr 'EWord
o1 Expr 'EWord
o2
go (Add o1 :: Expr 'EWord
o1@(Lit W256
_) o2 :: Expr 'EWord
o2@(Lit W256
_)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.add Expr 'EWord
o1 Expr 'EWord
o2
go (Sub o1 :: Expr 'EWord
o1@(Lit W256
_) o2 :: Expr 'EWord
o2@(Lit W256
_)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.sub Expr 'EWord
o1 Expr 'EWord
o2
go (Add (Lit W256
x) (Add (Lit W256
y) Expr 'EWord
orig)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
y)) Expr 'EWord
orig
go (Add (Lit W256
x) (Sub (Lit W256
y) Expr 'EWord
orig)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
y)) Expr 'EWord
orig
go (Add (Lit W256
x) (Sub Expr 'EWord
orig (Lit W256
y))) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
go (Sub (Lit W256
x) (Sub (Lit W256
y) Expr 'EWord
orig)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
go (Sub (Lit W256
x) (Sub Expr 'EWord
orig (Lit W256
y))) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
y)) Expr 'EWord
orig
go (Sub (Sub (Lit W256
x) Expr 'EWord
orig) (Lit W256
y)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
go (Sub (Sub Expr 'EWord
orig (Lit W256
x)) (Lit W256
y)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub Expr 'EWord
orig (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
y))
go (Sub (Lit W256
x) (Add (Lit W256
y) Expr 'EWord
orig)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
go (Sub (Add (Lit W256
x) Expr 'EWord
orig) (Lit W256
y) ) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
go (Sub (Add Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c)
| Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c = Expr a
Expr 'EWord
b
| Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c = Expr a
Expr 'EWord
a
| Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c
go (Add Expr 'EWord
a (Add Expr 'EWord
b Expr 'EWord
c)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c
go (Add (Add (Lit W256
a) Expr 'EWord
x) (Lit W256
b)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
aW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
b)) Expr 'EWord
x
go (Add Expr 'EWord
a Expr 'EWord
b)
| Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
a
| Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
b
| Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
a Expr 'EWord
b
go (Sub Expr 'EWord
a Expr 'EWord
b)
| Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = W256 -> Expr 'EWord
Lit W256
0
| Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
a
| Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub Expr 'EWord
a Expr 'EWord
b
go (SHL Expr 'EWord
a Expr 'EWord
v)
| Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
v
| Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
shl Expr 'EWord
a Expr 'EWord
v
go (SHR Expr 'EWord
a Expr 'EWord
v)
| Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
v
| Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
shr Expr 'EWord
a Expr 'EWord
v
go o :: Expr a
o@(And Expr 'EWord
a (And Expr 'EWord
b Expr 'EWord
c))
| Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
And Expr 'EWord
a Expr 'EWord
b)
| Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
And Expr 'EWord
b Expr 'EWord
c)
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(And (Lit W256
x) Expr 'EWord
_)
| W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = W256 -> Expr 'EWord
Lit W256
0
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(And Expr 'EWord
v (Lit W256
x))
| W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = W256 -> Expr 'EWord
Lit W256
0
| W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
maxLit = Expr a
Expr 'EWord
v
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(Or (Lit W256
x) Expr 'EWord
b)
| W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr a
Expr 'EWord
b
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(Or Expr 'EWord
a (Lit W256
x))
| W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr a
Expr 'EWord
a
| Bool
otherwise = Expr a
o
go (ITE (Or (Lit W256
x) Expr 'EWord
a) Expr 'End
t Expr 'End
f)
| W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE Expr 'EWord
a Expr 'End
t Expr 'End
f
| Bool
otherwise = Expr a
Expr 'End
t
go (ITE (Or Expr 'EWord
a b :: Expr 'EWord
b@(Lit W256
_)) Expr 'End
t Expr 'End
f) = Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Or Expr 'EWord
b Expr 'EWord
a) Expr 'End
t Expr 'End
f
go o :: Expr a
o@(EVM.Types.LT (BufLength (WriteWord {})) (Lit W256
x))
| W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
32 = W256 -> Expr 'EWord
Lit W256
0
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(EVM.Types.LT (Lit W256
x) (BufLength (WriteWord {})))
| W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
32 = W256 -> Expr 'EWord
Lit W256
1
| Bool
otherwise = Expr a
o
go (EVM.Types.Not (EVM.Types.Not Expr 'EWord
a)) = Expr a
Expr 'EWord
a
go (Max Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
a Expr 'EWord
b
go (Min Expr 'EWord
a Expr 'EWord
b) = case (Expr 'EWord
a, Expr 'EWord
b) of
(Lit W256
0, Expr 'EWord
_) -> W256 -> Expr 'EWord
Lit W256
0
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.min Expr 'EWord
a Expr 'EWord
b
go (Mul Expr 'EWord
a (Mul Expr 'EWord
b Expr 'EWord
c)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c
go (Mul (Mul (Lit W256
a) Expr 'EWord
x) (Lit W256
b)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul (W256 -> Expr 'EWord
Lit (W256
aW256 -> W256 -> W256
forall a. Num a => a -> a -> a
*W256
b)) Expr 'EWord
x
go (Mul Expr 'EWord
a Expr 'EWord
b) = case (Expr 'EWord
a, Expr 'EWord
b) of
(Lit W256
0, Expr 'EWord
_) -> W256 -> Expr 'EWord
Lit W256
0
(Lit W256
1, Expr 'EWord
_) -> Expr a
Expr 'EWord
b
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul Expr 'EWord
a Expr 'EWord
b
go (Div (Lit W256
0) Expr 'EWord
_) = W256 -> Expr 'EWord
Lit W256
0
go (Div Expr 'EWord
_ (Lit W256
0)) = W256 -> Expr 'EWord
Lit W256
0
go (Div Expr 'EWord
a (Lit W256
1)) = Expr a
Expr 'EWord
a
go o :: Expr a
o@(LT (Max (Lit W256
a) Expr 'EWord
_) (Lit W256
b))
| W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
b = W256 -> Expr 'EWord
Lit W256
0
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(SLT (Sub (Max (Lit W256
a) Expr 'EWord
_) (Lit W256
b)) (Lit W256
c))
= let sa, sb, sc :: Int256
sa :: Int256
sa = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
a
sb :: Int256
sb = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
b
sc :: Int256
sc = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
c
in if Int256
sa Int256 -> Int256 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int256
sb Bool -> Bool -> Bool
&& Int256
sa Int256 -> Int256 -> Int256
forall a. Num a => a -> a -> a
- Int256
sb Int256 -> Int256 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int256
sc
then W256 -> Expr 'EWord
Lit W256
0
else Expr a
o
go Expr a
a = Expr a
a
simplifyProps :: [Prop] -> [Prop]
simplifyProps :: [Prop] -> [Prop]
simplifyProps [Prop]
ps = if Bool
canBeSat then [Prop]
simplified else [Bool -> Prop
PBool Bool
False]
where
simplified :: [Prop]
simplified = [Prop] -> [Prop]
remRedundantProps ([Prop] -> [Prop]) -> ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Prop
simplifyProp ([Prop] -> [Prop]) -> ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Prop] -> [Prop]
flattenProps ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop]
ps
canBeSat :: Bool
canBeSat = [Prop] -> Bool
constFoldProp [Prop]
simplified
simplifyProp :: Prop -> Prop
simplifyProp :: Prop -> Prop
simplifyProp Prop
prop =
let new :: Prop
new = (Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
go (Prop -> Prop
simpInnerExpr Prop
prop)
in if (Prop
new Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
prop) then Prop
prop else Prop -> Prop
simplifyProp Prop
new
where
go :: Prop -> Prop
go :: Prop -> Prop
go (PLT (Var Text
_) (Lit W256
0)) = Bool -> Prop
PBool Bool
False
go (PLEq (Lit W256
0) (Var Text
_)) = Bool -> Prop
PBool Bool
True
go (PLT (Lit W256
val) (Var Text
_)) | W256
val W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
maxLit = Bool -> Prop
PBool Bool
False
go (PLEq (Var Text
_) (Lit W256
val)) | W256
val W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
maxLit = Bool -> Prop
PBool Bool
True
go (PLT (Lit W256
l) (Lit W256
r)) = Bool -> Prop
PBool (W256
l W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
r)
go (PLEq (Lit W256
l) (Lit W256
r)) = Bool -> Prop
PBool (W256
l W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
r)
go (PLEq Expr 'EWord
a (Max Expr 'EWord
b Expr 'EWord
_)) | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = Bool -> Prop
PBool Bool
True
go (PLEq Expr 'EWord
a (Max Expr 'EWord
_ Expr 'EWord
b)) | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = Bool -> Prop
PBool Bool
True
go (PLT (Max (Lit W256
a) Expr 'EWord
b) (Lit W256
c)) | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
c = Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
b (W256 -> Expr 'EWord
Lit W256
c)
go (PLT (Lit W256
0) (Eq Expr 'EWord
a Expr 'EWord
b)) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b
go (PNeg (PBool Bool
b)) = Bool -> Prop
PBool (Bool -> Bool
Prelude.not Bool
b)
go (PNeg (PNeg Prop
a)) = Prop
a
go (PEq (IsZero (Eq Expr 'EWord
a Expr 'EWord
b)) (Lit W256
0)) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b
go (PEq (IsZero (IsZero (Eq Expr 'EWord
a Expr 'EWord
b))) (Lit W256
0)) = Prop -> Prop
PNeg (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b)
go (PNeg (PEq (IsZero (IsZero Expr 'EWord
a)) (Lit W256
0))) = Expr 'EWord -> Expr 'EWord -> Prop
PGT Expr 'EWord
a (W256 -> Expr 'EWord
Lit W256
0)
go (PNeg (PEq (IsZero Expr 'EWord
a) (Lit W256
0))) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a (W256 -> Expr 'EWord
Lit W256
0)
go (PNeg (PEq (LT Expr 'EWord
a Expr 'EWord
b) (Lit W256
0x0))) = Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
a Expr 'EWord
b
go (PAnd (PBool Bool
l) (PBool Bool
r)) = Bool -> Prop
PBool (Bool
l Bool -> Bool -> Bool
&& Bool
r)
go (PAnd (PBool Bool
False) Prop
_) = Bool -> Prop
PBool Bool
False
go (PAnd Prop
_ (PBool Bool
False)) = Bool -> Prop
PBool Bool
False
go (POr (PBool Bool
True) Prop
_) = Bool -> Prop
PBool Bool
True
go (POr Prop
_ (PBool Bool
True)) = Bool -> Prop
PBool Bool
True
go (POr (PBool Bool
l) (PBool Bool
r)) = Bool -> Prop
PBool (Bool
l Bool -> Bool -> Bool
|| Bool
r)
go (PImpl Prop
_ (PBool Bool
True)) = Bool -> Prop
PBool Bool
True
go (PImpl (PBool Bool
True) Prop
b) = Prop
b
go (PImpl (PBool Bool
False) Prop
_) = Bool -> Prop
PBool Bool
True
go (PEq (Eq Expr 'EWord
a Expr 'EWord
b) (Lit W256
0)) = Prop -> Prop
PNeg (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b)
go (PEq (Eq Expr 'EWord
a Expr 'EWord
b) (Lit W256
1)) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b
go (PEq (Sub Expr 'EWord
a Expr 'EWord
b) (Lit W256
0)) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b
go (PEq (Lit W256
l) (Lit W256
r)) = Bool -> Prop
PBool (W256
l W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
r)
go o :: Prop
o@(PEq Expr a
l Expr a
r)
| Expr a
l Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
r = Bool -> Prop
PBool Bool
True
| Bool
otherwise = Prop
o
go Prop
p = Prop
p
simpInnerExpr :: Prop -> Prop
simpInnerExpr :: Prop -> Prop
simpInnerExpr (PGEq Expr 'EWord
a Expr 'EWord
b) = Prop -> Prop
simpInnerExpr (Expr 'EWord -> Expr 'EWord -> Prop
PLEq Expr 'EWord
b Expr 'EWord
a)
simpInnerExpr (PGT Expr 'EWord
a Expr 'EWord
b) = Prop -> Prop
simpInnerExpr (Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
b Expr 'EWord
a)
simpInnerExpr (PEq Expr a
a Expr a
b) = Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplify Expr a
a) (Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplify Expr a
b)
simpInnerExpr (PLT Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Prop
PLT (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
a) (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
b)
simpInnerExpr (PLEq Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Prop
PLEq (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
a) (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
b)
simpInnerExpr (PNeg Prop
a) = Prop -> Prop
PNeg (Prop -> Prop
simpInnerExpr Prop
a)
simpInnerExpr (PAnd Prop
a Prop
b) = Prop -> Prop -> Prop
PAnd (Prop -> Prop
simpInnerExpr Prop
a) (Prop -> Prop
simpInnerExpr Prop
b)
simpInnerExpr (POr Prop
a Prop
b) = Prop -> Prop -> Prop
POr (Prop -> Prop
simpInnerExpr Prop
a) (Prop -> Prop
simpInnerExpr Prop
b)
simpInnerExpr (PImpl Prop
a Prop
b) = Prop -> Prop -> Prop
PImpl (Prop -> Prop
simpInnerExpr Prop
a) (Prop -> Prop
simpInnerExpr Prop
b)
simpInnerExpr orig :: Prop
orig@(PBool Bool
_) = Prop
orig
flattenProps :: [Prop] -> [Prop]
flattenProps :: [Prop] -> [Prop]
flattenProps [] = []
flattenProps (Prop
a:[Prop]
ax) = case Prop
a of
PAnd Prop
x1 Prop
x2 -> Prop
x1Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:Prop
x2Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop] -> [Prop]
flattenProps [Prop]
ax
Prop
x -> Prop
xProp -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop] -> [Prop]
flattenProps [Prop]
ax
remRedundantProps :: [Prop] -> [Prop]
remRedundantProps :: [Prop] -> [Prop]
remRedundantProps [Prop]
p = [Prop] -> [Prop]
forall a. Ord a => [a] -> [a]
nubOrd ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop] -> [Prop]
collapseFalse ([Prop] -> [Prop]) -> ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Prop -> Bool) -> [Prop] -> [Prop]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Prop
x -> Prop
x Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Prop
PBool Bool
True) ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop]
p
where
collapseFalse :: [Prop] -> [Prop]
collapseFalse [Prop]
ps = if Maybe Prop -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Prop -> Bool) -> Maybe Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (Prop -> Bool) -> [Prop] -> Maybe Prop
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Prop
PBool Bool
False) [Prop]
ps then [Bool -> Prop
PBool Bool
False] else [Prop]
ps
litAddr :: Addr -> Expr EWord
litAddr :: Addr -> Expr 'EWord
litAddr = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Addr -> W256) -> Addr -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Addr -> W256
forall target source. From source target => source -> target
into
exprToAddr :: Expr EWord -> Maybe Addr
exprToAddr :: Expr 'EWord -> Maybe Addr
exprToAddr (Lit W256
x) = Addr -> Maybe Addr
forall a. a -> Maybe a
Just (W256 -> Addr
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
x)
exprToAddr Expr 'EWord
_ = Maybe Addr
forall a. Maybe a
Nothing
wordToAddr :: Expr EWord -> Maybe (Expr EAddr)
wordToAddr :: Expr 'EWord -> Maybe (Expr 'EAddr)
wordToAddr = Expr 'EWord -> Maybe (Expr 'EAddr)
go (Expr 'EWord -> Maybe (Expr 'EAddr))
-> (Expr 'EWord -> Expr 'EWord)
-> Expr 'EWord
-> Maybe (Expr 'EAddr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify
where
go :: Expr EWord -> Maybe (Expr EAddr)
go :: Expr 'EWord -> Maybe (Expr 'EAddr)
go = \case
WAddr Expr 'EAddr
a -> Expr 'EAddr -> Maybe (Expr 'EAddr)
forall a. a -> Maybe a
Just Expr 'EAddr
a
Lit W256
a -> Expr 'EAddr -> Maybe (Expr 'EAddr)
forall a. a -> Maybe a
Just (Expr 'EAddr -> Maybe (Expr 'EAddr))
-> Expr 'EAddr -> Maybe (Expr 'EAddr)
forall a b. (a -> b) -> a -> b
$ Addr -> Expr 'EAddr
LitAddr (W256 -> Addr
truncateToAddr W256
a)
Expr 'EWord
_ -> Maybe (Expr 'EAddr)
forall a. Maybe a
Nothing
litCode :: BS.ByteString -> [Expr Byte]
litCode :: ByteString -> [Expr 'Byte]
litCode ByteString
bs = (Word8 -> Expr 'Byte) -> [Word8] -> [Expr 'Byte]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word8 -> Expr 'Byte
LitByte (ByteString -> [Word8]
BS.unpack ByteString
bs)
to512 :: W256 -> Word512
to512 :: W256 -> Word512
to512 = W256 -> Word512
forall a b. (Integral a, Num b) => a -> b
fromIntegral
isLitByte :: Expr Byte -> Bool
isLitByte :: Expr 'Byte -> Bool
isLitByte (LitByte Word8
_) = Bool
True
isLitByte Expr 'Byte
_ = Bool
False
isLitWord :: Expr EWord -> Bool
isLitWord :: Expr 'EWord -> Bool
isLitWord (Lit W256
_) = Bool
True
isLitWord (WAddr (LitAddr Addr
_)) = Bool
True
isLitWord Expr 'EWord
_ = Bool
False
isSuccess :: Expr End -> Bool
isSuccess :: Expr 'End -> Bool
isSuccess = \case
Success {} -> Bool
True
Expr 'End
_ -> Bool
False
isFailure :: Expr End -> Bool
isFailure :: Expr 'End -> Bool
isFailure = \case
Failure {} -> Bool
True
Expr 'End
_ -> Bool
False
isPartial :: Expr End -> Bool
isPartial :: Expr 'End -> Bool
isPartial = \case
Partial {} -> Bool
True
Expr 'End
_ -> Bool
False
indexWord :: Expr EWord -> Expr EWord -> Expr Byte
indexWord :: Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord i :: Expr 'EWord
i@(Lit W256
idx) e :: Expr 'EWord
e@(And (Lit W256
mask) Expr 'EWord
w)
| W256
mask W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
fullWordMask = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'EWord
w
| W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
31
, W256 -> Bool
forall {a}. (Bits a, Num a) => a -> Bool
isPower2 (W256
mask W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1)
, W256 -> Bool
forall {b}. FiniteBits b => b -> Bool
isByteAligned W256
mask
, W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
unmaskedBytes
= Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'EWord
w
| W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
31
, W256 -> Bool
forall {a}. (Bits a, Num a) => a -> Bool
isPower2 (W256
mask W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1)
, W256 -> Bool
forall {b}. FiniteBits b => b -> Bool
isByteAligned W256
mask
, W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
unmaskedBytes
= Word8 -> Expr 'Byte
LitByte Word8
0
| W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
31 = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
IndexWord Expr 'EWord
i Expr 'EWord
e
| Bool
otherwise = Word8 -> Expr 'Byte
LitByte Word8
0
where
isPower2 :: a -> Bool
isPower2 a
n = a
n a -> a -> a
forall a. Bits a => a -> a -> a
.&. (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0
fullWordMask :: W256
fullWordMask = (W256
2 W256 -> W256 -> W256
forall a b. (Num a, Integral b) => a -> b -> a
^ (W256
256 :: W256)) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1
unmaskedBytes :: W256
unmaskedBytes = Int -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> W256) -> Int -> W256
forall a b. (a -> b) -> a -> b
$ (W256 -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros W256
mask) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`Prelude.div` Int
8
isByteAligned :: b -> Bool
isByteAligned b
m = (b -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros b
m) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`Prelude.mod` Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
indexWord (Lit W256
idx) (Lit W256
w)
| W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
31 = Word8 -> Expr 'Byte
LitByte (Word8 -> Expr 'Byte) -> (W256 -> Word8) -> W256 -> Expr 'Byte
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (W256 -> Expr 'Byte) -> W256 -> Expr 'Byte
forall a b. (a -> b) -> a -> b
$ W256 -> Int -> W256
forall a. Bits a => a -> Int -> a
shiftR W256
w (Int
248 Int -> Int -> Int
forall a. Num a => a -> a -> a
- W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
Typeable target) =>
source -> target
unsafeInto W256
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8)
| Bool
otherwise = Word8 -> Expr 'Byte
LitByte Word8
0
indexWord (Lit W256
idx) (JoinBytes Expr 'Byte
zero Expr 'Byte
one Expr 'Byte
two Expr 'Byte
three
Expr 'Byte
four Expr 'Byte
five Expr 'Byte
six Expr 'Byte
seven
Expr 'Byte
eight Expr 'Byte
nine Expr 'Byte
ten Expr 'Byte
eleven
Expr 'Byte
twelve Expr 'Byte
thirteen Expr 'Byte
fourteen Expr 'Byte
fifteen
Expr 'Byte
sixteen Expr 'Byte
seventeen Expr 'Byte
eighteen Expr 'Byte
nineteen
Expr 'Byte
twenty Expr 'Byte
twentyone Expr 'Byte
twentytwo Expr 'Byte
twentythree
Expr 'Byte
twentyfour Expr 'Byte
twentyfive Expr 'Byte
twentysix Expr 'Byte
twentyseven
Expr 'Byte
twentyeight Expr 'Byte
twentynine Expr 'Byte
thirty Expr 'Byte
thirtyone)
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr 'Byte
zero
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
1 = Expr 'Byte
one
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
2 = Expr 'Byte
two
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
3 = Expr 'Byte
three
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
4 = Expr 'Byte
four
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
5 = Expr 'Byte
five
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
6 = Expr 'Byte
six
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
7 = Expr 'Byte
seven
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
8 = Expr 'Byte
eight
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
9 = Expr 'Byte
nine
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
10 = Expr 'Byte
ten
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
11 = Expr 'Byte
eleven
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
12 = Expr 'Byte
twelve
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
13 = Expr 'Byte
thirteen
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
14 = Expr 'Byte
fourteen
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
15 = Expr 'Byte
fifteen
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
16 = Expr 'Byte
sixteen
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
17 = Expr 'Byte
seventeen
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
18 = Expr 'Byte
eighteen
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
19 = Expr 'Byte
nineteen
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
20 = Expr 'Byte
twenty
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
21 = Expr 'Byte
twentyone
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
22 = Expr 'Byte
twentytwo
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
23 = Expr 'Byte
twentythree
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
24 = Expr 'Byte
twentyfour
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
25 = Expr 'Byte
twentyfive
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
26 = Expr 'Byte
twentysix
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
27 = Expr 'Byte
twentyseven
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
28 = Expr 'Byte
twentyeight
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
29 = Expr 'Byte
twentynine
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
30 = Expr 'Byte
thirty
| W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
31 = Expr 'Byte
thirtyone
| Bool
otherwise = Word8 -> Expr 'Byte
LitByte Word8
0
indexWord Expr 'EWord
idx Expr 'EWord
w = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
IndexWord Expr 'EWord
idx Expr 'EWord
w
padByte :: Expr Byte -> Expr EWord
padByte :: Expr 'Byte -> Expr 'EWord
padByte (LitByte Word8
b) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord)
-> ([Word8] -> W256) -> [Word8] -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> W256
bytesToW256 ([Word8] -> Expr 'EWord) -> [Word8] -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ [Word8
b]
padByte Expr 'Byte
b = [Expr 'Byte] -> Expr 'EWord
joinBytes [Expr 'Byte
b]
bytesToW256 :: [Word8] -> W256
bytesToW256 :: [Word8] -> W256
bytesToW256 = ByteString -> W256
word (ByteString -> W256) -> ([Word8] -> ByteString) -> [Word8] -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack
padBytesLeft :: Int -> [Expr Byte] -> [Expr Byte]
padBytesLeft :: Int -> [Expr 'Byte] -> [Expr 'Byte]
padBytesLeft Int
n [Expr 'Byte]
bs
| [Expr 'Byte] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'Byte]
bs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = Int -> [Expr 'Byte] -> [Expr 'Byte]
forall a. Int -> [a] -> [a]
Prelude.take Int
n [Expr 'Byte]
bs
| [Expr 'Byte] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'Byte]
bs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n = [Expr 'Byte]
bs
| Bool
otherwise = Int -> [Expr 'Byte] -> [Expr 'Byte]
padBytesLeft Int
n (Word8 -> Expr 'Byte
LitByte Word8
0 Expr 'Byte -> [Expr 'Byte] -> [Expr 'Byte]
forall a. a -> [a] -> [a]
: [Expr 'Byte]
bs)
joinBytes :: [Expr Byte] -> Expr EWord
joinBytes :: [Expr 'Byte] -> Expr 'EWord
joinBytes [Expr 'Byte]
bs
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and ([Bool] -> Bool)
-> ([Expr 'Byte] -> [Bool]) -> [Expr 'Byte] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Bool) -> [Expr 'Byte] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) ([Expr 'Byte] -> Bool) -> [Expr 'Byte] -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bs = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord)
-> ([Expr 'Byte] -> W256) -> [Expr 'Byte] -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> W256
bytesToW256 ([Word8] -> W256)
-> ([Expr 'Byte] -> [Word8]) -> [Expr 'Byte] -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Maybe Word8) -> [Expr 'Byte] -> [Word8]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
maybeLitByte) ([Expr 'Byte] -> Expr 'EWord) -> [Expr 'Byte] -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bs
| Bool
otherwise = let
bytes :: [Expr 'Byte]
bytes = Int -> [Expr 'Byte] -> [Expr 'Byte]
padBytesLeft Int
32 [Expr 'Byte]
bs
in Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'EWord
JoinBytes
([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
4) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
5) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
6) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
7)
([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
8) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
9) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
10) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
11)
([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
12) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
13) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
14) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
15)
([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
16) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
17) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
18) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
19)
([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
20) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
21) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
22) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
23)
([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
24) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
25) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
26) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
27)
([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
28) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
29) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
30) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
31)
eqByte :: Expr Byte -> Expr Byte -> Expr EWord
eqByte :: Expr 'Byte -> Expr 'Byte -> Expr 'EWord
eqByte (LitByte Word8
x) (LitByte Word8
y) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ if Word8
x Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
y then W256
1 else W256
0
eqByte Expr 'Byte
x Expr 'Byte
y = Expr 'Byte -> Expr 'Byte -> Expr 'EWord
EqByte Expr 'Byte
x Expr 'Byte
y
min :: Expr EWord -> Expr EWord -> Expr EWord
min :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
min Expr 'EWord
x Expr 'EWord
y = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Min W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.min Expr 'EWord
x Expr 'EWord
y
max :: Expr EWord -> Expr EWord -> Expr EWord
max :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
max (Lit W256
0) Expr 'EWord
y = Expr 'EWord
y
max Expr 'EWord
x (Lit W256
0) = Expr 'EWord
x
max Expr 'EWord
x Expr 'EWord
y = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Max W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max Expr 'EWord
x Expr 'EWord
y
numBranches :: Expr End -> Int
numBranches :: Expr 'End -> Int
numBranches (ITE Expr 'EWord
_ Expr 'End
t Expr 'End
f) = Expr 'End -> Int
numBranches Expr 'End
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Expr 'End -> Int
numBranches Expr 'End
f
numBranches Expr 'End
_ = Int
1
allLit :: [Expr Byte] -> Bool
allLit :: [Expr 'Byte] -> Bool
allLit = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Data.List.and ([Bool] -> Bool)
-> ([Expr 'Byte] -> [Bool]) -> [Expr 'Byte] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'Byte -> Bool) -> [Expr 'Byte] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Expr 'Byte -> Bool
isLitByte)
containsNode :: (forall a. Expr a -> Bool) -> Expr b -> Bool
containsNode :: forall (b :: EType).
(forall (a :: EType). Expr a -> Bool) -> Expr b -> Bool
containsNode forall (a :: EType). Expr a -> Bool
p = Any -> Bool
getAny (Any -> Bool) -> (Expr b -> Any) -> Expr b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: EType). Expr a -> Any) -> Any -> Expr b -> Any
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> Any
forall (a :: EType). Expr a -> Any
go (Bool -> Any
Any Bool
False)
where
go :: Expr a -> Any
go :: forall (a :: EType). Expr a -> Any
go Expr a
node | Expr a -> Bool
forall (a :: EType). Expr a -> Bool
p Expr a
node = Bool -> Any
Any Bool
True
go Expr a
_ = Bool -> Any
Any Bool
False
inRange :: Int -> Expr EWord -> Prop
inRange :: Int -> Expr 'EWord -> Prop
inRange Int
sz Expr 'EWord
e = Prop -> Prop -> Prop
PAnd (Expr 'EWord -> Expr 'EWord -> Prop
PGEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit W256
0)) (Expr 'EWord -> Expr 'EWord -> Prop
PLEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
2 W256 -> Int -> W256
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1))
preImages :: [(W256, Word8)]
preImages :: [(W256, Word8)]
preImages = [(ByteString -> W256
keccak' (W256 -> ByteString
word256Bytes (W256 -> ByteString) -> (Word8 -> W256) -> Word8 -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> W256
forall target source. From source target => source -> target
into (Word8 -> ByteString) -> Word8 -> ByteString
forall a b. (a -> b) -> a -> b
$ Word8
i), Word8
i) | Word8
i <- [Word8
0..Word8
255]]
data ConstState = ConstState
{ ConstState -> Map (Expr 'EWord) W256
values :: Map.Map (Expr EWord) W256
, ConstState -> Bool
canBeSat :: Bool
}
deriving (Int -> ConstState -> ShowS
[ConstState] -> ShowS
ConstState -> [Char]
(Int -> ConstState -> ShowS)
-> (ConstState -> [Char])
-> ([ConstState] -> ShowS)
-> Show ConstState
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConstState -> ShowS
showsPrec :: Int -> ConstState -> ShowS
$cshow :: ConstState -> [Char]
show :: ConstState -> [Char]
$cshowList :: [ConstState] -> ShowS
showList :: [ConstState] -> ShowS
Show)
constFoldProp :: [Prop] -> Bool
constFoldProp :: [Prop] -> Bool
constFoldProp [Prop]
ps = [Prop] -> ConstState -> Bool
forall {t :: * -> *}. Traversable t => t Prop -> ConstState -> Bool
oneRun [Prop]
ps (Map (Expr 'EWord) W256 -> Bool -> ConstState
ConstState Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty Bool
True)
where
oneRun :: t Prop -> ConstState -> Bool
oneRun t Prop
ps2 ConstState
startState = (State ConstState (t ()) -> ConstState -> ConstState
forall s a. State s a -> s -> s
execState ((Prop -> StateT ConstState Identity ())
-> t Prop -> State ConstState (t ())
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM (Prop -> StateT ConstState Identity ()
go (Prop -> StateT ConstState Identity ())
-> (Prop -> Prop) -> Prop -> StateT ConstState Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> Prop
simplifyProp) t Prop
ps2) ConstState
startState).canBeSat
go :: Prop -> State ConstState ()
go :: Prop -> StateT ConstState Identity ()
go Prop
x = case Prop
x of
PEq (Lit W256
l) Expr a
a -> do
ConstState
s <- StateT ConstState Identity ConstState
forall s (m :: * -> *). MonadState s m => m s
get
case Expr a -> Map (Expr a) W256 -> Maybe W256
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr a
a ConstState
s.values of
Just W256
l2 -> case W256
lW256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
==W256
l2 of
Bool
True -> () -> StateT ConstState Identity ()
forall a. a -> StateT ConstState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Bool
False -> ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ConstState {$sel:canBeSat:ConstState :: Bool
canBeSat=Bool
False, $sel:values:ConstState :: Map (Expr 'EWord) W256
values=Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty}
Maybe W256
Nothing -> do
let vs' :: Map (Expr a) W256
vs' = Expr a -> W256 -> Map (Expr a) W256 -> Map (Expr a) W256
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr a
a W256
l ConstState
s.values
ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ConstState -> StateT ConstState Identity ())
-> ConstState -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ ConstState
s{$sel:values:ConstState :: Map (Expr 'EWord) W256
values=Map (Expr a) W256
Map (Expr 'EWord) W256
vs'}
PEq Expr a
a b :: Expr a
b@(Lit W256
_) -> Prop -> StateT ConstState Identity ()
go (Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr a
b Expr a
a)
PNeg (PEq (Lit W256
l) Expr a
a) -> do
ConstState
s <- StateT ConstState Identity ConstState
forall s (m :: * -> *). MonadState s m => m s
get
case Expr a -> Map (Expr a) W256 -> Maybe W256
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr a
a ConstState
s.values of
Just W256
l2 -> case W256
lW256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
==W256
l2 of
Bool
True -> ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ConstState {$sel:canBeSat:ConstState :: Bool
canBeSat=Bool
False, $sel:values:ConstState :: Map (Expr 'EWord) W256
values=Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty}
Bool
False -> () -> StateT ConstState Identity ()
forall a. a -> StateT ConstState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Maybe W256
Nothing -> () -> StateT ConstState Identity ()
forall a. a -> StateT ConstState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure()
PNeg (PEq Expr a
a b :: Expr a
b@(Lit W256
_)) -> Prop -> StateT ConstState Identity ()
go (Prop -> StateT ConstState Identity ())
-> Prop -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ Prop -> Prop
PNeg (Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr a
b Expr a
a)
PAnd Prop
a Prop
b -> do
Prop -> StateT ConstState Identity ()
go Prop
a
Prop -> StateT ConstState Identity ()
go Prop
b
POr Prop
a Prop
b -> do
ConstState
s <- StateT ConstState Identity ConstState
forall s (m :: * -> *). MonadState s m => m s
get
let
v1 :: Bool
v1 = [Prop] -> ConstState -> Bool
forall {t :: * -> *}. Traversable t => t Prop -> ConstState -> Bool
oneRun [Prop
a] ConstState
s
v2 :: Bool
v2 = [Prop] -> ConstState -> Bool
forall {t :: * -> *}. Traversable t => t Prop -> ConstState -> Bool
oneRun [Prop
b] ConstState
s
Bool
-> StateT ConstState Identity () -> StateT ConstState Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
Prelude.not Bool
v1) (StateT ConstState Identity () -> StateT ConstState Identity ())
-> StateT ConstState Identity () -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ Prop -> StateT ConstState Identity ()
go Prop
b
Bool
-> StateT ConstState Identity () -> StateT ConstState Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
Prelude.not Bool
v2) (StateT ConstState Identity () -> StateT ConstState Identity ())
-> StateT ConstState Identity () -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ Prop -> StateT ConstState Identity ()
go Prop
a
ConstState
s2 <- StateT ConstState Identity ConstState
forall s (m :: * -> *). MonadState s m => m s
get
ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ConstState -> StateT ConstState Identity ())
-> ConstState -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ ConstState
s{$sel:canBeSat:ConstState :: Bool
canBeSat=(ConstState
s2.canBeSat Bool -> Bool -> Bool
&& (Bool
v1 Bool -> Bool -> Bool
|| Bool
v2))}
PBool Bool
False -> ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ConstState -> StateT ConstState Identity ())
-> ConstState -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ ConstState {$sel:canBeSat:ConstState :: Bool
canBeSat=Bool
False, $sel:values:ConstState :: Map (Expr 'EWord) W256
values=Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty}
Prop
_ -> () -> StateT ConstState Identity ()
forall a. a -> StateT ConstState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
concKeccakSimpExpr :: Expr a -> Expr a
concKeccakSimpExpr :: forall (a :: EType). Expr a -> Expr a
concKeccakSimpExpr Expr a
orig = (Expr a -> Expr a) -> Expr a -> Expr a
forall a. Eq a => (a -> a) -> a -> a
untilFixpoint (((forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
concKeccakOnePass) (Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplify) Expr a
orig
concKeccakProps :: [Prop] -> [Prop]
concKeccakProps :: [Prop] -> [Prop]
concKeccakProps [Prop]
orig = ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a. Eq a => (a -> a) -> a -> a
untilFixpoint ((Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
concKeccakOnePass)) [Prop]
orig
concKeccakOnePass :: Expr a -> Expr a
concKeccakOnePass :: forall (a :: EType). Expr a -> Expr a
concKeccakOnePass (Keccak (ConcreteBuf ByteString
bs)) = W256 -> Expr 'EWord
Lit (ByteString -> W256
keccak' ByteString
bs)
concKeccakOnePass orig :: Expr a
orig@(Keccak (CopySlice (Lit W256
0) (Lit W256
0) (Lit W256
64) orig2 :: Expr 'Buf
orig2@(WriteWord (Lit W256
0) Expr 'EWord
_ (ConcreteBuf ByteString
bs)) (ConcreteBuf ByteString
""))) =
case (ByteString -> Int
BS.length ByteString
bs, (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice (W256 -> Expr 'EWord
Lit W256
0) (W256 -> Expr 'EWord
Lit W256
0) (W256 -> Expr 'EWord
Lit W256
64) (Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
simplify Expr 'Buf
orig2) (ByteString -> Expr 'Buf
ConcreteBuf ByteString
""))) of
(Int
64, ConcreteBuf ByteString
a) -> W256 -> Expr 'EWord
Lit (ByteString -> W256
keccak' ByteString
a)
(Int, Expr 'Buf)
_ -> Expr a
orig
concKeccakOnePass Expr a
x = Expr a
x