{-# Language DataKinds #-}
{-# Language PatternGuards #-}

{-|
   Helper functions for working with Expr instances.
   All functions here will return a concrete result if given a concrete input.
-}
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 Optics.Core

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)


-- ** Stack Ops ** ---------------------------------------------------------------------------------


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

-- | If a given binary op is commutative, then we always force Lits to the lhs if
-- only one argument is a Lit. This makes writing pattern matches in the
-- simplifier easier.
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

-- Integers

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))

-- Booleans

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)

-- Bits

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
             -- simplify function selector checks
             (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))

-- ** Bufs ** --------------------------------------------------------------------------------------


-- | Extracts the byte at a given index from a Buf.
--
-- We do our best to return a concrete value wherever possible, but fallback to
-- an abstract expresion if nescessary. Note that a Buf is an infinite
-- structure, so reads outside of the bounds of a ConcreteBuf return 0. This is
-- inline with the semantics of calldata and memory, but not of returndata.

-- fuly concrete reads
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
x forall a. Num a => a -> a -> a
- W256
idx 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 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
x forall a. Num a => a -> a -> a
- W256
dstOffset forall a. Ord a => a -> a -> Bool
< 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)
  -- the byte we are trying to read is compeletely outside of the sliced region
  = if W256
x forall a. Num a => a -> a -> a
- W256
dstOffset 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

-- fully abstract reads
readByte Expr 'EWord
i Expr 'Buf
buf = Expr 'EWord -> Expr 'Buf -> Expr 'Byte
ReadByte Expr 'EWord
i Expr 'Buf
buf


-- | Reads n bytes starting from idx in buf and returns a left padded word
--
-- If n is >= 32 this is the same as readWord
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]]

-- | Reads the word starting at idx from the given buf
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)
  -- the word we are trying to read exactly matches a WriteWord
  | 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. Num a => a -> a -> a
- W256
i forall a. Ord a => a -> a -> Bool
>= W256
32 Bool -> Bool -> Bool
&& W256
i' forall a. Num a => a -> a -> a
- W256
i forall a. Ord a => a -> a -> Bool
<= (forall a. Bounded a => a
maxBound :: W256) forall a. Num a => a -> a -> a
- W256
31
      -- the region we are trying to read is completely outside of the WriteWord
      then Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord Expr 'EWord
idx Expr 'Buf
buf
      -- the region we are trying to read partially overlaps the WriteWord
      else Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWordFromBytes Expr 'EWord
idx Expr 'Buf
b
    -- we do not have enough information to statically determine whether or not
    -- the region we want to read overlaps the WriteWord
    (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)
  -- the region we are trying to read is enclosed in the sliced region
  | (W256
idx forall a. Num a => a -> a -> a
- W256
dstOff) forall a. Ord a => a -> a -> Bool
< W256
size Bool -> Bool -> Bool
&& W256
32 forall a. Ord a => a -> a -> Bool
<= W256
size forall a. Num a => a -> a -> a
- (W256
idx forall a. Num a => a -> a -> a
- W256
dstOff) = 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
  -- the region we are trying to read is compeletely outside of the sliced region
  | (W256
idx forall a. Num a => a -> a -> a
- W256
dstOff) forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& (W256
idx forall a. Num a => a -> a -> a
- W256
dstOff) forall a. Ord a => a -> a -> Bool
<= (forall a. Bounded a => a
maxBound :: 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
  -- the region we are trying to read partially overlaps the sliced region
  | 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

-- Attempts to read a concrete word from a buffer by reading 32 individual bytes and joining them together
-- returns an abstract ReadWord expression if a concrete word cannot be constructed
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
maybeLitByte 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

{- | Copies a slice of src into dst.

        0           srcOffset       srcOffset + size     length src
        ┌--------------┬------------------┬-----------------┐
   src: |              | ------ sl ------ |                 |
        └--------------┴------------------┴-----------------┘

        0     dstOffset       dstOffset + size     length dst
        ┌--------┬------------------┬-----------------┐
   dst: |   hd   |                  |       tl        |
        └--------┴------------------┴-----------------┘
-}

-- The maximum number of bytes we will expand as part of simplification
--     this limits the amount of memory we will use while simplifying to ~1 GB / rewrite
--     note that things can still stack up, e.g. N such rewrites could eventually eat
--     N*1GB.
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

-- Copies from empty buffers
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

-- Fully concrete copies
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

-- copying 32 bytes can be rewritten to a WriteWord on dst (e.g. CODECOPY of args during constructors)
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

-- concrete indicies & abstract src (may produce a concrete result if we are
-- copying from a concrete region of src)
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
maybeLitByte) 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

-- abstract indicies
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)
  -- if the indices match exactly then we just replace the value in the current write and return
  | 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
                           -- if we can statically determine that the write at
                           -- idx doesn't overlap the write at idx', then we
                           -- push the write down we only consider writes where
                           -- i > i' to avoid infinite loops in this routine.
                           -- This also has the nice side effect of imposing a
                           -- canonical ordering on write chains, making exact
                           -- syntactic equalities between abstract terms more
                           -- likely to occur
                           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)
                           -- if we cannot statically determine freedom from
                           -- overlap, then we just return an abstract term
                           else Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
b
        -- if we cannot determine statically that the write at idx' is out of
        -- bounds for idx, then we return an abstract term
        (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


-- | Returns the length of a given buffer
--
-- If there are any writes to abstract locations, or CopySlices with an
-- abstract size or dstOffset, an abstract expresion will be returned.
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)))

-- | If a buffer has a concrete prefix, we return it's length here
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
    -- base cases
    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

    -- writes to a concrete index
    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

    -- writes to an abstract index are ignored
    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


-- | Return the minimum possible length of a buffer. In the case of an
-- abstract buffer, it is the largest write that is made on a concrete
-- location. Parameterized by an environment for buffer variables.
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
    -- base cases
    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
    -- writes to a concrete index
    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
    -- writes to an abstract index are ignored
    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 :: 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 = 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

-- | Returns the first n bytes of buf
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)


-- | Returns everything but the first n bytes of buf
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
maybeLitByte forall a b. (a -> b) -> a -> b
$ Vector (Expr 'Byte)
bs
  -- we want to minimize the size of the resulting expresion, so we do two passes:
  --   1. write all concrete bytes to some base buffer
  --   2. write all symbolic writes on top of this buffer
  -- this is safe because each write in the input vec is to a single byte at a distinct location
  -- runs in O(2n) time, and has pretty minimal allocation & copy overhead in
  -- the concrete part (a single preallocated vec, with no copies)
  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
""

-- | Removes any irrelevant writes when reading from a buffer
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

-- | Strips writes from the buffer that can be statically determined to be out of range
-- TODO: are the bounds here correct? I think there might be some off by one mistakes...
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 forall a b. (a -> b) -> a -> b
$ if W256
off forall a. Ord a => a -> a -> Bool
<= W256
off forall a. Num a => a -> a -> a
+ W256
size
                                 then Int -> ByteString -> ByteString
BS.take (forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ W256
offforall a. Num a => a -> a -> a
+W256
size) ByteString
b
                                 else ByteString
b
  WriteByte (Lit W256
idx) Expr 'Byte
v Expr 'Buf
prev
    -> if W256
idx forall a. Num a => a -> a -> a
- W256
off 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)
  -- TODO: handle partial overlaps
  WriteWord (Lit W256
idx) Expr 'EWord
v Expr 'Buf
prev
    -> if W256
idx forall a. Num a => a -> a -> a
- W256
off forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& W256
idx forall a. Num a => a -> a -> a
- W256
off forall a. Ord a => a -> a -> Bool
<= (forall a. Bounded a => a
maxBound :: 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 forall a. Num a => a -> a -> a
- W256
off forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& W256
dstOff forall a. Num a => a -> a -> a
- W256
off forall a. Ord a => a -> a -> Bool
<= (forall a. Bounded a => a
maxBound :: W256) forall a. Num a => a -> a -> a
- W256
size' 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
_ ->  forall a. HasCallStack => [Char] -> a
error [Char]
"unexpected GVar in stripWrites"


-- ** Storage ** -----------------------------------------------------------------------------------


-- | Reads the word at the given slot from the given storage expression.
--
-- Note that we return a Nothing instead of a 0x0 if we are reading from a
-- store that is backed by a ConcreteStore or an EmptyStore and there have been
-- no explicit writes to the requested slot. This makes implementing rpc
-- storage lookups much easier. If the store is backed by an AbstractStore we
-- always return a symbolic value.
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'
       -- if address and slot match then we return the val in this write
       then forall a. a -> Maybe a
Just Expr 'EWord
val
       else case (Expr 'EWord
slot, Expr 'EWord
slot') of
              -- if the slots don't match and are lits, we can skip this write
              (Lit W256
_, Lit W256
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
addr' Expr 'EWord
slot' Expr 'Storage
prev
              -- if the slots don't match syntactically and are abstract then we can't skip this write
              (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
    -- if the the addresses don't match and are lits, we can skip this write
    (Lit W256
_, Lit W256
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
addr' Expr 'EWord
slot' Expr 'Storage
prev
    -- if the the addresses don't match syntactically and are abstract then we can't skip this write
    (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


-- | Writes a value to a key in a storage expression.
--
-- Concrete writes on top of a concrete or empty store will produce a new
-- ConcreteStore, otherwise we add a new write to the storage expression.
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'
       -- if we're overwriting an existing location, then drop the write
       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
              -- if we can know statically that the new write doesn't overlap with the existing write, then we continue down the write chain
              -- we impose an ordering relation on the writes that we push down to ensure termination when this routine is called from the simplifier
              (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
              -- otherwise stack a new write on top of the the existing write chain
              (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
        -- if we can know statically that the new write doesn't overlap with the existing write, then we continue down the write chain
        -- once again we impose an ordering relation on the pushed down writes to ensure termination
        (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
        -- otherwise stack a new write on top of the the existing write chain
        (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


-- ** Whole Expression Simplification ** -----------------------------------------------------------


-- | Simple recursive match based AST simplification
-- Note: may not terminate!
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
    -- redundant CopySlice
    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

    -- simplify storage
    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

    -- simplify buffers
    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

    -- We can zero out any bytes in a base ConcreteBuf that we know will be overwritten by a later write
    -- TODO: make this fully general for entire write chains, not just a single write.
    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

    -- LT
    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

    -- normalize all comparisons in terms of LT
    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

    -- syntactic Eq reduction
    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

    -- redundant ITE
    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

    -- simple div/mod/add/sub
    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

    -- double add/sub.
    -- Notice that everything is done mod 2**256. So for example:
    -- (a-b)+c observes the same arithmetic equalities as we are used to
    --         in infinite integers. In fact, it can be re-written as:
    -- (a+(W256Max-b)+c), which is the same as:
    -- (a+c+(W256Max-b)), which is the same as:
    -- (a+(c-b))
    -- In other words, subtraction is just adding a much larger number.
    --    So 3-1 mod 6 = 3+(6-1) mod 6 = 3+5 mod 6 = 5+3 mod 6 = 2
    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))

    -- redundant add / sub
    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

    -- add / sub identities
    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

    -- SHL / SHR by 0
    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

    -- doubled And
    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

    -- Bitwise AND & OR. These MUST preserve bitwise equivalence
    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

    -- If x is ever non zero the Or will always evaluate to some non zero value and the false branch will be unreachable
    -- NOTE: with AND this does not work, because and(0x8, 0x4) = 0
    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

    -- we write at least 32, so if x <= 32, it's FALSE
    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
    -- we write at least 32, so if x < 32, it's TRUE
    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

    -- Double NOT is a no-op, since it's a bitwise inversion
    go (EVM.Types.Not (EVM.Types.Not Expr 'EWord
a)) = Expr 'EWord
a

    -- Some trivial min / max eliminations
    go (Max (Lit W256
0) Expr 'EWord
a) = Expr 'EWord
a
    go (Min (Lit W256
0) Expr 'EWord
_) = W256 -> Expr 'EWord
Lit W256
0

    -- If a >= b then the value of the `Max` expression can never be < b
    go o :: Expr a
o@(LT (Max (Lit W256
a) Expr 'EWord
_) (Lit W256
b))
      | W256
a 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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
a
            sb :: Int256
sb = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
b
            sc :: Int256
sc = forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
c
        in if Int256
sa forall a. Ord a => a -> a -> Bool
>= Int256
sb Bool -> Bool -> Bool
&& Int256
sa forall a. Num a => a -> a -> a
- Int256
sb 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


-- ** Conversions ** -------------------------------------------------------------------------------


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


-- ** Helpers ** -----------------------------------------------------------------------------------


-- Is the given expr a literal byte?
isLitByte :: Expr Byte -> Bool
isLitByte :: Expr 'Byte -> Bool
isLitByte (LitByte Word8
_) = Bool
True
isLitByte Expr 'Byte
_ = Bool
False

-- Is the given expr a literal word?
isLitWord :: Expr EWord -> Bool
isLitWord :: Expr 'EWord -> Bool
isLitWord (Lit W256
_) = Bool
True
isLitWord Expr 'EWord
_ = Bool
False

-- | Returns the byte at idx from the given word.
indexWord :: Expr EWord -> Expr EWord -> Expr Byte
-- Simplify masked reads:
--
--
--                reads across the mask boundry
--                return an abstract expression
--                            │
--                            │
--   reads outside of         │             reads over the mask read
--   the mask return 0        │             from the underlying word
--          │                 │                       │
--          │           ┌─────┘                       │
--          ▼           ▼                             ▼
--        ┌───┐       ┌─┬─┬─────────────────────────┬───┬──────────────┐
--        │   │       │ │ │                         │   │              │    mask
--        │   │       │ └─┼─────────────────────────┼───┼──────────────┘
--        │   │       │   │                         │   │
--    ┌───┼───┼───────┼───┼─────────────────────────┼───┼──────────────┐
--    │   │┼┼┼│       │┼┼┼│                         │┼┼┼│              │    w
--    └───┴───┴───────┴───┴─────────────────────────┴───┴──────────────┘
--   MSB                                                              LSB
--    ────────────────────────────────────────────────────────────────►
--    0                                                               31
--
--                    indexWord 0 reads from the MSB
--                    indexWord 31 reads from the LSB
--
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)
  -- if the mask is all 1s then read from the undelrying word
  -- we need this case to avoid overflow
  | 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
  -- if the index is a read from the masked region then read from the underlying word
  | 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
  -- if the read is outside of the masked region return 0
  | 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
  -- if the mask is not a power of 2, or it does not align with a byte boundry return an abstract expression
  | W256
idx forall a. Ord a => a -> a -> Bool
<= W256
31 = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
IndexWord Expr 'EWord
i Expr 'EWord
e
  -- reads outside the range of the source word return 0
  | 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]

-- | Converts a list of bytes into a W256.
-- TODO: semantics if the input is too large?
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
maybeLitByte) 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)

-- | True if the given expression contains any node that satisfies the
-- input predicate
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