{-# Language DataKinds #-}
{-# Language PatternGuards #-}
module EVM.Expr where
import Prelude hiding (LT, GT)
import Data.Bits hiding (And, Xor)
import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128))
import Data.Int (Int32)
import Data.Word
import Data.Maybe
import Data.List
import Control.Lens (lens)
import EVM.Types
import EVM.Traversals
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import qualified Data.Map.Strict as Map
import qualified Data.Vector as V
import qualified Data.Vector.Storable as VS
import Data.Vector.Storable.ByteString
import Data.Semigroup (Any, Any(..), getAny)
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 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 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 forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else 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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
sy :: Int256
sy = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
in if W256
y forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int256
sx 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 forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else W256
x 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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
sy :: Int256
sy = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
in if W256
y forall a. Eq a => a -> a -> Bool
== W256
0
then W256
0
else forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int256
sx 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 forall a. Eq a => a -> a -> Bool
== W256
0
then W256
0
else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (W256 -> Word512
to512 W256
x forall a. Num a => a -> a -> a
+ W256 -> Word512
to512 W256
y) 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 forall a. Eq a => a -> a -> Bool
== W256
0
then W256
0
else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (W256 -> Word512
to512 W256
x forall a. Num a => a -> a -> a
* W256 -> Word512
to512 W256
y) 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 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 forall a. Ord a => a -> a -> Bool
>= W256
32 then W256
x
else let n :: Int
n = forall a b. (Integral a, Num b) => a -> b
num W256
bytes forall a. Num a => a -> a -> a
* Int
8 forall a. Num a => a -> a -> a
+ Int
7 in
if forall a. Bits a => a -> Int -> Bool
testBit W256
x Int
n
then W256
x forall a. Bits a => a -> a -> a
.|. forall a. Bits a => a -> a
complement (forall a. Bits a => Int -> a
bit Int
n forall a. Num a => a -> a -> a
- W256
1)
else W256
x forall a. Bits a => a -> a -> a
.&. (forall a. Bits a => Int -> a
bit Int
n 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 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 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 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 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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
sy :: Int256
sy = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
in if Int256
sx 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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
sy :: Int256
sy = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
in if Int256
sx 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 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 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 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 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 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 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 forall a. Ord a => a -> a -> Bool
> W256
256 then W256
0 else forall a. Bits a => a -> Int -> a
shiftL W256
y (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 (
forall a. Int -> a -> [a]
replicate Int
28 (Word8 -> Expr 'Byte
LitByte Word8
0) 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 forall a b. (a -> b) -> a -> b
$ W256
idx forall a. Num a => a -> a -> a
+ W256
1) Expr 'Buf
buf
, Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit forall a b. (a -> b) -> a -> b
$ W256
idx forall a. Num a => a -> a -> a
+ W256
2) Expr 'Buf
buf
, Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit forall a b. (a -> b) -> a -> b
$ W256
idx 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 forall a. Ord a => a -> a -> Bool
> W256
256 then W256
0 else forall a. Bits a => a -> Int -> a
shiftR W256
y (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 = forall a. Bits a => a -> Int -> Bool
testBit W256
y Int
255
asSigned :: Int256
asSigned = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y :: Int256
in if W256
x forall a. Ord a => a -> a -> Bool
> W256
256 then
if Bool
msb then forall a. Bounded a => a
maxBound else W256
0
else
forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> a
shiftR Int256
asSigned (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 forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
num (forall a. Bounded a => a
maxBound :: Int) Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< ByteString -> Int
BS.length ByteString
b
then Word8 -> Expr 'Byte
LitByte (HasCallStack => 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'))) -> forall a b. (Integral a, Num b) => a -> b
num Word64
x'
readByte i :: Expr 'EWord
i@(Lit W256
x) (WriteByte (Lit W256
idx) Expr 'Byte
val Expr 'Buf
src)
= if W256
x 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
idx forall a. Ord a => a -> a -> Bool
<= W256
x Bool -> Bool -> Bool
&& W256
x forall a. Ord a => a -> a -> Bool
<= W256
idx forall a. Num a => a -> a -> a
+ W256
31
then case Expr 'EWord
val of
(Lit W256
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord (W256 -> Expr 'EWord
Lit forall a b. (a -> b) -> a -> b
$ W256
x 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 forall a b. (a -> b) -> a -> b
$ W256
x 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
dstOffset forall a. Ord a => a -> a -> Bool
<= W256
x Bool -> Bool -> Bool
&& W256
x forall a. Ord a => a -> a -> Bool
< (W256
dstOffset forall a. Num a => a -> a -> a
+ W256
size)
then Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit forall a b. (a -> b) -> a -> b
$ W256
x forall a. Num a => a -> a -> a
- (W256
dstOffset 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 forall a. Ord a => a -> a -> Bool
< W256
dstOffset Bool -> Bool -> Bool
|| W256
x forall a. Ord a => a -> a -> Bool
>= W256
dstOffset forall a. Num a => a -> a -> a
+ W256
size) Bool -> Bool -> Bool
&& (W256
dstOffset forall a. Ord a => a -> a -> Bool
<= W256
dstOffset forall a. Num a => a -> a -> a
+ 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 (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ Int
i)) Expr 'Buf
buf | Int
i <- [Int
0 .. Int
n 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 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 forall a. Ord a => a -> a -> Bool
>= W256
i' forall a. Num a => a -> a -> a
+ W256
32 Bool -> Bool -> Bool
|| W256
i forall a. Num a => a -> a -> a
+ W256
32 forall a. Ord a => a -> a -> Bool
<= W256
i'
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 forall a. Ord a => a -> a -> Bool
>= W256
dstOff Bool -> Bool -> Bool
&& W256
idx forall a. Num a => a -> a -> a
+ W256
32 forall a. Ord a => a -> a -> Bool
<= W256
dstOff forall a. Num a => a -> a -> a
+ W256
size = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord (W256 -> Expr 'EWord
Lit forall a b. (a -> b) -> a -> b
$ W256
srcOff forall a. Num a => a -> a -> a
+ (W256
idx forall a. Num a => a -> a -> a
- W256
dstOff)) Expr 'Buf
src
| (W256
idx forall a. Ord a => a -> a -> Bool
>= W256
dstOff forall a. Num a => a -> a -> a
+ W256
size Bool -> Bool -> Bool
|| W256
idx forall a. Num a => a -> a -> a
+ W256
32 forall a. Ord a => a -> a -> Bool
<= W256
dstOff) Bool -> Bool -> Bool
&& (W256
dstOffforall a. Ord a => a -> a -> Bool
<= W256
dstOff forall a. Num a => a -> a -> a
+ W256
size) = 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 forall a b. (a -> b) -> a -> b
$ ByteString -> W256
word forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
padRight Int
32 forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take Int
32 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 forall a. Num a => a -> a -> a
+ W256
31]]
in if forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bytes
then W256 -> Expr 'EWord
Lit ([Word8] -> W256
bytesToW256 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
unlitByte 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 = forall a b. (Integral a, Num b) => a -> b
num (forall a. Bounded a => a
maxBound :: Int32) forall a. Integral a => a -> a -> a
`Prelude.div` W256
4
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 forall a. Ord a => a -> a -> Bool
< W256
maxBytes = ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
num 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 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 forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
num 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 forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
num (ByteString -> Int
BS.length ByteString
src), W256
size forall a. Ord a => a -> a -> Bool
< W256
maxBytes = ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
num W256
size) Word8
0
| W256
srcOffset forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
num (ByteString -> Int
BS.length ByteString
src), W256
dstOffset forall a. Ord a => a -> a -> Bool
< W256
maxBytes, W256
size forall a. Ord a => a -> a -> Bool
< W256
maxBytes = let
hd :: ByteString
hd = Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
num W256
dstOffset) Word8
0
sl :: ByteString
sl = Int -> ByteString -> ByteString
padRight (forall a b. (Integral a, Num b) => a -> b
num W256
size) forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num W256
size) (Int -> ByteString -> ByteString
BS.drop (forall a b. (Integral a, Num b) => a -> b
num W256
srcOffset) ByteString
src)
in ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ ByteString
hd 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 forall a. Ord a => a -> a -> Bool
< W256
maxBytes
, W256
size forall a. Ord a => a -> a -> Bool
< W256
maxBytes =
let hd :: ByteString
hd = Int -> ByteString -> ByteString
padRight (forall a b. (Integral a, Num b) => a -> b
num W256
dstOffset) forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num W256
dstOffset) ByteString
dst
sl :: ByteString
sl = if W256
srcOffset forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
num (ByteString -> Int
BS.length ByteString
src)
then Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
num W256
size) Word8
0
else Int -> ByteString -> ByteString
padRight (forall a b. (Integral a, Num b) => a -> b
num W256
size) forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num W256
size) (Int -> ByteString -> ByteString
BS.drop (forall a b. (Integral a, Num b) => a -> b
num W256
srcOffset) ByteString
src)
tl :: ByteString
tl = Int -> ByteString -> ByteString
BS.drop (forall a b. (Integral a, Num b) => a -> b
num W256
dstOffset forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
num W256
size) ByteString
dst
in ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ ByteString
hd forall a. Semigroup a => a -> a -> a
<> ByteString
sl 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 forall a. Ord a => a -> a -> Bool
< W256
maxBytes, W256
size forall a. Ord a => a -> a -> Bool
< W256
maxBytes = let
hd :: ByteString
hd = Int -> ByteString -> ByteString
padRight (forall a b. (Integral a, Num b) => a -> b
num W256
dstOffset) forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num 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 forall a. Num a => a -> a -> a
+ (W256
size forall a. Num a => a -> a -> a
- W256
1)]]
tl :: ByteString
tl = Int -> ByteString -> ByteString
BS.drop (forall a b. (Integral a, Num b) => a -> b
num W256
dstOffset forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
num W256
size) ByteString
dst
in if forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
sl
then ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ ByteString
hd forall a. Semigroup a => a -> a -> a
<> ([Word8] -> ByteString
BS.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
unlitByte) forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
sl) 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 forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
num W256
offset) Word8
0 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 forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ (Int -> ByteString -> ByteString
padRight (forall a b. (Integral a, Num b) => a -> b
num W256
offset) forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num W256
offset) ByteString
src)
forall a. Semigroup a => a -> a -> a
<> [Word8] -> ByteString
BS.pack [Word8
byte]
forall a. Semigroup a => a -> a -> a
<> Int -> ByteString -> ByteString
BS.drop (forall a b. (Integral a, Num b) => a -> b
num W256
offset 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 (Lit W256
offset) (Lit W256
val) (ConcreteBuf ByteString
"")
| W256
offset forall a. Num a => a -> a -> a
+ W256
32 forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
num W256
offset) Word8
0 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 forall a. Num a => a -> a -> a
+ W256
32 forall a. Ord a => a -> a -> Bool
< W256
maxBytes
= ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ (Int -> ByteString -> ByteString
padRight (forall a b. (Integral a, Num b) => a -> b
num W256
offset) forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num W256
offset) ByteString
src)
forall a. Semigroup a => a -> a -> a
<> W256 -> ByteString
word256Bytes W256
val
forall a. Semigroup a => a -> a -> a
<> Int -> ByteString -> ByteString
BS.drop ((forall a b. (Integral a, Num b) => a -> b
num W256
offset) 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 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 forall a. Ord a => a -> a -> Bool
>= W256
i' 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 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 (forall a b. (Integral a, Num b) => a -> b
num forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length forall a b. (a -> b) -> a -> b
$ ByteString
b))
go Expr 'EWord
l (AbstractBuf Text
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
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 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 -> forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: 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 (forall (a :: EType). GVar a -> Expr a
GVar (Int -> GVar 'Buf
BufVar Int
a)))
concPrefix :: Expr Buf -> Maybe Integer
concPrefix :: Expr 'Buf -> Maybe Integer
concPrefix (CopySlice (Lit W256
srcOff) (Lit W256
_) (Lit W256
_) Expr 'Buf
src (ConcreteBuf ByteString
"")) = do
Integer
sz <- W256 -> Expr 'Buf -> Maybe Integer
go W256
0 Expr 'Buf
src
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ (forall a b. (Integral a, Num b) => a -> b
num Integer
sz) forall a. Num a => a -> a -> a
- W256
srcOff
where
go :: W256 -> Expr Buf -> Maybe Integer
go :: W256 -> Expr 'Buf -> Maybe Integer
go W256
_ (AbstractBuf Text
_) = forall a. Maybe a
Nothing
go W256
l (ConcreteBuf ByteString
b) = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
Prelude.max (forall a b. (Integral a, Num b) => a -> b
num forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length forall a b. (a -> b) -> a -> b
$ ByteString
b) W256
l
go W256
l (WriteWord (Lit W256
idx) (Lit W256
_) Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go (forall a. Ord a => a -> a -> a
Prelude.max W256
l (W256
idx forall a. Num a => a -> a -> a
+ W256
32)) Expr 'Buf
b
go W256
l (WriteByte (Lit W256
idx) (LitByte Word8
_) Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go (forall a. Ord a => a -> a -> a
Prelude.max W256
l (W256
idx 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 (forall a. Ord a => a -> a -> a
Prelude.max (W256
dstOffset 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
_ (CopySlice Expr 'EWord
_ Expr 'EWord
_ Expr 'EWord
_ Expr 'Buf
_ Expr 'Buf
_) = forall a. HasCallStack => [Char] -> a
error [Char]
"Internal Error: cannot compute a concrete prefix length for nested copySlice expressions"
go W256
_ (GVar GVar 'Buf
_) = forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: cannot calculate a concrete prefix of an open expression"
concPrefix (ConcreteBuf ByteString
b) = forall a. a -> Maybe a
Just (forall a b. (Integral a, Num b) => a -> b
num forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length forall a b. (a -> b) -> a -> b
$ ByteString
b)
concPrefix Expr 'Buf
e = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal error: cannot compute a concrete prefix length for: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show Expr 'Buf
e
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 forall a. Eq a => a -> a -> Bool
== W256
0 then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
num W256
l
go W256
l (ConcreteBuf ByteString
b) = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
Prelude.max (forall a b. (Integral a, Num b) => a -> b
num forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length 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 (forall a. Ord a => a -> a -> a
Prelude.max W256
l (W256
idx 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 (forall a. Ord a => a -> a -> a
Prelude.max W256
l (W256
idx 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 (forall a. Ord a => a -> a -> a
Prelude.max (W256
dstOffset 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 <- 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
word256At
:: Functor f
=> Expr EWord -> (Expr EWord -> f (Expr EWord))
-> Expr Buf -> f (Expr Buf)
word256At :: forall (f :: * -> *).
Functor f =>
Expr 'EWord
-> (Expr 'EWord -> f (Expr 'EWord)) -> Expr 'Buf -> f (Expr 'Buf)
word256At Expr 'EWord
i = 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 forall a. Monoid a => a
mempty
toList :: Expr Buf -> Maybe (V.Vector (Expr Byte))
toList :: Expr 'Buf -> Maybe (Vector (Expr 'Byte))
toList (AbstractBuf Text
_) = forall a. Maybe a
Nothing
toList (ConcreteBuf ByteString
bs) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Vector a
V.fromList forall a b. (a -> b) -> a -> b
$ Word8 -> Expr 'Byte
LitByte 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 forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
num (forall a. Bounded a => a
maxBound :: Int)
then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Int -> (Int -> a) -> Vector a
V.generate (forall a b. (Integral a, Num b) => a -> b
num W256
l) (\Int
i -> Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
num Int
i) Expr 'Buf
buf)
else forall a. HasCallStack => [Char] -> a
error [Char]
"Internal Error: overflow when converting buffer to list"
Expr 'EWord
_ -> forall a. Maybe a
Nothing
fromList :: V.Vector (Expr Byte) -> Expr Buf
fromList :: Vector (Expr 'Byte) -> Expr 'Buf
fromList Vector (Expr 'Byte)
bs = case forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Vector a -> [a]
V.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> Vector a -> Vector b
V.mapMaybe Expr 'Byte -> Maybe Word8
unlitByte forall a b. (a -> b) -> a -> b
$ Vector (Expr 'Byte)
bs
Bool
False -> 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 = forall a. Storable a => Vector a -> ByteString
vectorToByteString forall a b. (a -> b) -> a -> b
$ forall a. Storable a => Int -> (Int -> a) -> Vector a
VS.generate (forall a. Vector a -> Int
V.length Vector (Expr 'Byte)
bs) (\Int
idx ->
case Vector (Expr 'Byte)
bs 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 forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
num 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 forall a b. (a -> b) -> a -> b
$ ByteString
a 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
idx forall a. Num a => a -> a -> a
+ W256
31) 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
idx 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
bottom W256
top = \case
AbstractBuf Text
s -> Text -> Expr 'Buf
AbstractBuf Text
s
ConcreteBuf ByteString
b -> ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num W256
topforall a. Num a => a -> a -> a
+Int
1) ByteString
b
WriteByte (Lit W256
idx) Expr 'Byte
v Expr 'Buf
prev
-> if W256
idx forall a. Ord a => a -> a -> Bool
< W256
bottom Bool -> Bool -> Bool
|| W256
idx forall a. Ord a => a -> a -> Bool
> W256
top
then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
bottom W256
top 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
bottom W256
top Expr 'Buf
prev)
WriteWord (Lit W256
idx) Expr 'EWord
v Expr 'Buf
prev
-> if W256
idx forall a. Num a => a -> a -> a
+ W256
31 forall a. Ord a => a -> a -> Bool
< W256
bottom Bool -> Bool -> Bool
|| W256
idx forall a. Ord a => a -> a -> Bool
> W256
top
then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
bottom W256
top 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
bottom W256
top Expr 'Buf
prev)
CopySlice (Lit W256
srcOff) (Lit W256
dstOff) (Lit W256
size) Expr 'Buf
src Expr 'Buf
dst
-> if W256
dstOff forall a. Num a => a -> a -> a
+ W256
size forall a. Ord a => a -> a -> Bool
< W256
bottom Bool -> Bool -> Bool
|| W256
dstOff forall a. Ord a => a -> a -> Bool
> W256
top
then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
bottom W256
top 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
srcOff forall a. Num a => a -> a -> a
+ W256
size) Expr 'Buf
src)
(W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
bottom W256
top 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
bottom W256
top 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
bottom W256
top 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
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"unexpected GVar in stripWrites"
readStorage :: Expr EWord -> Expr EWord -> Expr Storage -> Maybe (Expr EWord)
readStorage :: Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
_ Expr 'EWord
_ Expr 'Storage
EmptyStore = forall a. Maybe a
Nothing
readStorage Expr 'EWord
addr Expr 'EWord
slot store :: Expr 'Storage
store@(ConcreteStore Map W256 (Map W256 W256)
s) = case (Expr 'EWord
addr, Expr 'EWord
slot) of
(Lit W256
a, Lit W256
l) -> do
Map W256 W256
ctrct <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup W256
a Map W256 (Map W256 W256)
s
W256
val <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup W256
l Map W256 W256
ctrct
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ W256 -> Expr 'EWord
Lit W256
val
(Expr 'EWord, Expr 'EWord)
_ -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
addr Expr 'EWord
slot Expr 'Storage
store
readStorage Expr 'EWord
addr' Expr 'EWord
slot' s :: Expr 'Storage
s@Expr 'Storage
AbstractStore = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
addr' Expr 'EWord
slot' Expr 'Storage
s
readStorage Expr 'EWord
addr' Expr 'EWord
slot' s :: Expr 'Storage
s@(SStore Expr 'EWord
addr Expr 'EWord
slot Expr 'EWord
val Expr 'Storage
prev) =
if Expr 'EWord
addr forall a. Eq a => a -> a -> Bool
== Expr 'EWord
addr'
then if Expr 'EWord
slot forall a. Eq a => a -> a -> Bool
== Expr 'EWord
slot'
then forall a. a -> Maybe a
Just Expr 'EWord
val
else case (Expr 'EWord
slot, Expr 'EWord
slot') of
(Lit W256
_, Lit W256
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
addr' Expr 'EWord
slot' Expr 'Storage
prev
(Expr 'EWord, Expr 'EWord)
_ -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
addr' Expr 'EWord
slot' Expr 'Storage
s
else case (Expr 'EWord
addr, Expr 'EWord
addr') of
(Lit W256
_, Lit W256
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
addr' Expr 'EWord
slot' Expr 'Storage
prev
(Expr 'EWord, Expr 'EWord)
_ -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
addr' Expr 'EWord
slot' Expr 'Storage
s
readStorage Expr 'EWord
_ Expr 'EWord
_ (GVar GVar 'Storage
_) = forall a. HasCallStack => [Char] -> a
error [Char]
"Can't read from a GVar"
readStorage' :: Expr EWord -> Expr EWord -> Expr Storage -> Expr EWord
readStorage' :: Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
readStorage' Expr 'EWord
addr Expr 'EWord
loc Expr 'Storage
store = case Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
addr Expr 'EWord
loc Expr 'Storage
store of
Just Expr 'EWord
v -> Expr 'EWord
v
Maybe (Expr 'EWord)
Nothing -> W256 -> Expr 'EWord
Lit W256
0
writeStorage :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage
writeStorage :: Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage a :: Expr 'EWord
a@(Lit W256
addr) k :: Expr 'EWord
k@(Lit W256
key) v :: Expr 'EWord
v@(Lit W256
val) Expr 'Storage
store = case Expr 'Storage
store of
Expr 'Storage
EmptyStore -> Map W256 (Map W256 W256) -> Expr 'Storage
ConcreteStore (forall k a. k -> a -> Map k a
Map.singleton W256
addr (forall k a. k -> a -> Map k a
Map.singleton W256
key W256
val))
ConcreteStore Map W256 (Map W256 W256)
s -> let
ctrct :: Map W256 W256
ctrct = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall k a. Map k a
Map.empty W256
addr Map W256 (Map W256 W256)
s
in Map W256 (Map W256 W256) -> Expr 'Storage
ConcreteStore (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert W256
addr (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert W256
key W256
val Map W256 W256
ctrct) Map W256 (Map W256 W256)
s)
Expr 'Storage
_ -> Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
a Expr 'EWord
k Expr 'EWord
v Expr 'Storage
store
writeStorage Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val store :: Expr 'Storage
store@(SStore Expr 'EWord
addr' Expr 'EWord
key' Expr 'EWord
val' Expr 'Storage
prev)
| Expr 'EWord
addr forall a. Eq a => a -> a -> Bool
== Expr 'EWord
addr'
= if Expr 'EWord
key forall a. Eq a => a -> a -> Bool
== Expr 'EWord
key'
then Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
prev
else case (Expr 'EWord
addr, Expr 'EWord
addr', Expr 'EWord
key, Expr 'EWord
key') of
(Lit W256
a, Lit W256
a', Lit W256
k, Lit W256
k') -> if W256
a forall a. Ord a => a -> a -> Bool
> W256
a' Bool -> Bool -> Bool
|| (W256
a forall a. Eq a => a -> a -> Bool
== W256
a' Bool -> Bool -> Bool
&& W256
k forall a. Ord a => a -> a -> Bool
> W256
k')
then Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
addr' Expr 'EWord
key' Expr 'EWord
val' (Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
prev)
else Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
(Expr 'EWord, Expr 'EWord, Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
| Bool
otherwise
= case (Expr 'EWord
addr, Expr 'EWord
addr') of
(Lit W256
a, Lit W256
a') -> if W256
a forall a. Ord a => a -> a -> Bool
> W256
a'
then Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
addr' Expr 'EWord
key' Expr 'EWord
val' (Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
prev)
else Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
(Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
writeStorage Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store = Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
addr Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
simplify :: Expr a -> Expr a
simplify :: forall (a :: EType). Expr a -> Expr a
simplify Expr a
e = if (forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
go Expr a
e forall a. Eq a => a -> a -> Bool
== Expr a
e)
then Expr a
e
else forall (a :: EType). Expr a -> Expr a
simplify (forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr 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 (CopySlice (Lit W256
0x0) (Lit W256
0x0) (Lit W256
0x0) Expr 'Buf
_ Expr 'Buf
dst) = Expr 'Buf
dst
go (SLoad Expr 'EWord
addr Expr 'EWord
slot Expr 'Storage
store) = Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
readStorage' Expr 'EWord
addr Expr 'EWord
slot Expr 'Storage
store
go (SStore Expr 'EWord
addr Expr 'EWord
slot Expr 'EWord
val Expr 'Storage
store) = Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage Expr 'EWord
addr Expr 'EWord
slot Expr 'EWord
val Expr 'Storage
store
go o :: Expr a
o@(ReadWord (Lit W256
_) Expr 'Buf
_) = 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
_) = 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 o :: Expr a
o@(WriteWord (Lit W256
idx) Expr 'EWord
val (ConcreteBuf ByteString
b))
| W256
idx 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 forall a b. (a -> b) -> a -> b
$
(Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num W256
idx) (Int -> ByteString -> ByteString
padRight (forall a b. (Integral a, Num b) => a -> b
num W256
idx) ByteString
b))
forall a. Semigroup a => a -> a -> a
<> (Int -> Word8 -> ByteString
BS.replicate Int
32 Word8
0)
forall a. Semigroup a => a -> a -> a
<> (Int -> ByteString -> ByteString
BS.drop (forall a b. (Integral a, Num b) => a -> b
num W256
idx 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 (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 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
EVM.Types.LT Expr 'EWord
b Expr 'EWord
a
go (EVM.Types.GEq Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Types.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
EVM.Types.GT Expr 'EWord
a Expr 'EWord
b)
go (IsZero Expr 'EWord
a) = Expr 'EWord -> Expr 'EWord
iszero Expr 'EWord
a
go (Eq (Lit W256
a) (Lit W256
b))
| W256
a 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 o :: Expr a
o@(Eq Expr 'EWord
a Expr 'EWord
b)
| Expr 'EWord
a forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = W256 -> Expr 'EWord
Lit W256
1
| Bool
otherwise = Expr a
o
go (ITE (Lit W256
x) Expr 'End
a Expr 'End
b)
| W256
x forall a. Eq a => a -> a -> Bool
== W256
0 = Expr 'End
b
| Bool
otherwise = Expr 'End
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 (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
yforall a. Num a => a -> a -> a
+W256
x))
go (Sub (Add Expr 'EWord
orig (Lit W256
x)) (Lit W256
y)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Sub Expr 'EWord
orig (W256 -> Expr 'EWord
Lit (W256
yforall a. Num a => a -> a -> a
-W256
x))
go (Add (Add Expr 'EWord
orig (Lit W256
x)) (Lit W256
y)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Add Expr 'EWord
orig (W256 -> Expr 'EWord
Lit (W256
yforall a. Num a => a -> a -> a
+W256
x))
go (Add (Sub Expr 'EWord
orig (Lit W256
x)) (Lit W256
y)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Add Expr 'EWord
orig (W256 -> Expr 'EWord
Lit (W256
yforall a. Num a => a -> a -> a
-W256
x))
go o :: Expr a
o@(Sub (Add Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c)
| Expr 'EWord
a forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c = Expr 'EWord
b
| Expr 'EWord
b forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c = Expr 'EWord
a
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(Add Expr 'EWord
a Expr 'EWord
b)
| Expr 'EWord
b forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr 'EWord
a
| Expr 'EWord
a forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr 'EWord
b
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(Sub Expr 'EWord
a Expr 'EWord
b)
| Expr 'EWord
a forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = W256 -> Expr 'EWord
Lit W256
0
| Expr 'EWord
b forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr 'EWord
a
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(SHL Expr 'EWord
a Expr 'EWord
v)
| Expr 'EWord
a forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr 'EWord
v
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(SHR Expr 'EWord
a Expr 'EWord
v)
| Expr 'EWord
a forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr 'EWord
v
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(And Expr 'EWord
a (And Expr 'EWord
b Expr 'EWord
c))
| Expr 'EWord
a 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 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 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
_ (Lit W256
x))
| W256
x 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@(Or (Lit W256
x) Expr 'EWord
b)
| W256
x forall a. Eq a => a -> a -> Bool
== W256
0 = Expr 'EWord
b
| Bool
otherwise = Expr a
o
go o :: Expr a
o@(Or Expr 'EWord
a (Lit W256
x))
| W256
x forall a. Eq a => a -> a -> Bool
== W256
0 = 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 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 '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 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 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 'EWord
a
go (Max (Lit W256
0) Expr 'EWord
a) = Expr 'EWord
a
go (Min (Lit W256
0) Expr 'EWord
_) = W256 -> Expr 'EWord
Lit W256
0
go Expr a
a = Expr a
a
litAddr :: Addr -> Expr EWord
litAddr :: Addr -> Expr 'EWord
litAddr = W256 -> Expr 'EWord
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num
exprToAddr :: Expr EWord -> Maybe Addr
exprToAddr :: Expr 'EWord -> Maybe Addr
exprToAddr (Lit W256
x) = forall a. a -> Maybe a
Just (forall a b. (Integral a, Num b) => a -> b
num W256
x)
exprToAddr Expr 'EWord
_ = forall a. Maybe a
Nothing
litCode :: BS.ByteString -> [Expr Byte]
litCode :: ByteString -> [Expr 'Byte]
litCode ByteString
bs = 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 = 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 Expr 'EWord
_ = 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 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 forall a. Ord a => a -> a -> Bool
<= W256
31
, forall {a}. (Bits a, Num a) => a -> Bool
isPower2 (W256
mask forall a. Num a => a -> a -> a
+ W256
1)
, forall {b}. FiniteBits b => b -> Bool
isByteAligned W256
mask
, W256
idx 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 forall a. Ord a => a -> a -> Bool
<= W256
31
, forall {a}. (Bits a, Num a) => a -> Bool
isPower2 (W256
mask forall a. Num a => a -> a -> a
+ W256
1)
, forall {b}. FiniteBits b => b -> Bool
isByteAligned W256
mask
, W256
idx forall a. Ord a => a -> a -> Bool
< W256
unmaskedBytes
= Word8 -> Expr 'Byte
LitByte Word8
0
| W256
idx 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 forall a. Bits a => a -> a -> a
.&. (a
nforall a. Num a => a -> a -> a
-a
1) forall a. Eq a => a -> a -> Bool
== a
0
fullWordMask :: W256
fullWordMask = (W256
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (W256
256 :: W256)) forall a. Num a => a -> a -> a
- W256
1
unmaskedBytes :: W256
unmaskedBytes = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ (forall b. FiniteBits b => b -> Int
countLeadingZeros W256
mask) forall a. Integral a => a -> a -> a
`Prelude.div` Int
8
isByteAligned :: b -> Bool
isByteAligned b
m = (forall b. FiniteBits b => b -> Int
countLeadingZeros b
m) forall a. Integral a => a -> a -> a
`Prelude.mod` Int
8 forall a. Eq a => a -> a -> Bool
== Int
0
indexWord (Lit W256
idx) (Lit W256
w)
| W256
idx forall a. Ord a => a -> a -> Bool
<= W256
31 = Word8 -> Expr 'Byte
LitByte forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> a
shiftR W256
w (Int
248 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
num W256
idx 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 forall a. Eq a => a -> a -> Bool
== W256
0 = Expr 'Byte
zero
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
1 = Expr 'Byte
one
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
2 = Expr 'Byte
two
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
3 = Expr 'Byte
three
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
4 = Expr 'Byte
four
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
5 = Expr 'Byte
five
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
6 = Expr 'Byte
six
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
7 = Expr 'Byte
seven
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
8 = Expr 'Byte
eight
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
9 = Expr 'Byte
nine
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
10 = Expr 'Byte
ten
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
11 = Expr 'Byte
eleven
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
12 = Expr 'Byte
twelve
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
13 = Expr 'Byte
thirteen
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
14 = Expr 'Byte
fourteen
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
15 = Expr 'Byte
fifteen
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
16 = Expr 'Byte
sixteen
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
17 = Expr 'Byte
seventeen
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
18 = Expr 'Byte
eighteen
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
19 = Expr 'Byte
nineteen
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
20 = Expr 'Byte
twenty
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
21 = Expr 'Byte
twentyone
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
22 = Expr 'Byte
twentytwo
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
23 = Expr 'Byte
twentythree
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
24 = Expr 'Byte
twentyfour
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
25 = Expr 'Byte
twentyfive
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
26 = Expr 'Byte
twentysix
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
27 = Expr 'Byte
twentyseven
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
28 = Expr 'Byte
twentyeight
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
29 = Expr 'Byte
twentynine
| W256
idx forall a. Eq a => a -> a -> Bool
== W256
30 = Expr 'Byte
thirty
| W256
idx 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> W256
bytesToW256 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 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
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'Byte]
bs forall a. Ord a => a -> a -> Bool
> Int
n = forall a. Int -> [a] -> [a]
Prelude.take Int
n [Expr 'Byte]
bs
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'Byte]
bs 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 forall a. a -> [a] -> [a]
: [Expr 'Byte]
bs)
joinBytes :: [Expr Byte] -> Expr EWord
joinBytes :: [Expr 'Byte] -> Expr 'EWord
joinBytes [Expr 'Byte]
bs
| forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bs = W256 -> Expr 'EWord
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> W256
bytesToW256 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
unlitByte) 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 forall a. [a] -> Int -> a
!! Int
0) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
1) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
2) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
3)
([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
4) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
5) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
6) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
7)
([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
8) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
9) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
10) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
11)
([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
12) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
13) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
14) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
15)
([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
16) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
17) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
18) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
19)
([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
20) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
21) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
22) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
23)
([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
24) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
25) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
26) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
27)
([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
28) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
29) ([Expr 'Byte]
bytes forall a. [a] -> Int -> a
!! Int
30) ([Expr 'Byte]
bytes forall a. [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 forall a b. (a -> b) -> a -> b
$ if Word8
x 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 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 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 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 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 = forall (t :: * -> *). Foldable t => t Bool -> Bool
Data.List.and forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr 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 | forall (a :: EType). Expr a -> Bool
p Expr a
node = Bool -> Any
Any Bool
True
go Expr a
_ = Bool -> Any
Any Bool
False