{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}

{-|
   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 Control.Monad.ST
import Data.Bits hiding (And, Xor)
import Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128))
import Data.List
import Data.Map.Strict qualified as Map
import Data.Maybe (mapMaybe, isJust, fromMaybe)
import Data.Semigroup (Any, Any(..), getAny)
import Data.Vector qualified as V
import Data.Vector (Vector)
import Data.Vector.Mutable qualified as MV
import Data.Vector.Mutable (MVector)
import Data.Vector.Storable qualified as VS
import Data.Vector.Storable.ByteString
import Data.Word (Word8, Word32)
import Witch (unsafeInto, into, tryFrom)
import Data.Containers.ListUtils (nubOrd)
import Control.Monad.State

import Optics.Core

import EVM.Traversals
import EVM.Types

-- ** Constants **

maxLit :: W256
maxLit :: W256
maxLit = W256
0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff

-- ** 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 W256 -> W256 -> W256
forall a. Num a => a -> a -> a
(+)

sub :: Expr EWord -> Expr EWord -> Expr EWord
sub :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Sub (-)

mul :: Expr EWord -> Expr EWord -> Expr EWord
mul :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Mul W256 -> W256 -> W256
forall a. Num a => a -> a -> a
(*)

div :: Expr EWord -> Expr EWord -> Expr EWord
div :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
div = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Div (\W256
x W256
y -> if W256
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else W256 -> W256 -> W256
forall a. Integral a => a -> a -> a
Prelude.div W256
x W256
y)

sdiv :: Expr EWord -> Expr EWord -> Expr EWord
sdiv :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sdiv = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SDiv (\W256
x W256
y -> let sx, sy :: Int256
                             sx :: Int256
sx = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
                             sy :: Int256
sy = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
                         in if W256
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else Int256 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int256
sx Int256 -> Int256 -> Int256
forall a. Integral a => a -> a -> a
`quot` Int256
sy))

mod :: Expr EWord -> Expr EWord -> Expr EWord
mod :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mod = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Mod (\W256
x W256
y -> if W256
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
0 else W256
x W256 -> W256 -> W256
forall a. Integral a => a -> a -> a
`Prelude.mod` W256
y)

smod :: Expr EWord -> Expr EWord -> Expr EWord
smod :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
smod = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SMod (\W256
x W256
y ->
  let sx, sy :: Int256
      sx :: Int256
sx = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
      sy :: Int256
sy = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
  in if W256
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0
     then W256
0
     else Int256 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int256
sx Int256 -> Int256 -> Int256
forall a. Integral a => a -> a -> a
`rem` Int256
sy))

addmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
addmod :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
addmod = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op3 Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
AddMod (\W256
x W256
y W256
z ->
  if W256
z W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0
  then W256
0
  else Word512 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word512 -> W256) -> Word512 -> W256
forall a b. (a -> b) -> a -> b
$ (W256 -> Word512
to512 W256
x Word512 -> Word512 -> Word512
forall a. Num a => a -> a -> a
+ W256 -> Word512
to512 W256
y) Word512 -> Word512 -> Word512
forall a. Integral a => a -> a -> a
`Prelude.mod` W256 -> Word512
to512 W256
z)

mulmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
mulmod :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mulmod = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op3 Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
MulMod (\W256
x W256
y W256
z ->
   if W256
z W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0
   then W256
0
   else Word512 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word512 -> W256) -> Word512 -> W256
forall a b. (a -> b) -> a -> b
$ (W256 -> Word512
to512 W256
x Word512 -> Word512 -> Word512
forall a. Num a => a -> a -> a
* W256 -> Word512
to512 W256
y) Word512 -> Word512 -> Word512
forall a. Integral a => a -> a -> a
`Prelude.mod` W256 -> Word512
to512 W256
z)

exp :: Expr EWord -> Expr EWord -> Expr EWord
exp :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
exp = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Exp W256 -> W256 -> W256
forall a b. (Num a, Integral b) => a -> b -> a
(^)

sex :: Expr EWord -> Expr EWord -> Expr EWord
sex :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sex = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SEx (\W256
bytes W256
x ->
  if W256
bytes W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
32 then W256
x
  else let n :: Int
n = W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
bytes Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
7 in
    if W256 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit W256
x Int
n
    then W256
x W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
.|. W256 -> W256
forall a. Bits a => a -> a
complement (Int -> W256
forall a. Bits a => Int -> a
bit Int
n W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1)
    else W256
x W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
.&. (Int -> W256
forall a. Bits a => Int -> a
bit Int
n W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1))

-- 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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
y then W256
1 else W256
0)

gt :: Expr EWord -> Expr EWord -> Expr EWord
gt :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
gt = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
GT (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
y then W256
1 else W256
0)

leq :: Expr EWord -> Expr EWord -> Expr EWord
leq :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
leq = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
LEq (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
y then W256
1 else W256
0)

geq :: Expr EWord -> Expr EWord -> Expr EWord
geq :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
geq = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
GEq (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
y then W256
1 else W256
0)

slt :: Expr EWord -> Expr EWord -> Expr EWord
slt :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
slt = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SLT (\W256
x W256
y ->
  let sx, sy :: Int256
      sx :: Int256
sx = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
      sy :: Int256
sy = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
  in if Int256
sx Int256 -> Int256 -> Bool
forall a. Ord a => a -> a -> Bool
< Int256
sy then W256
1 else W256
0)

sgt :: Expr EWord -> Expr EWord -> Expr EWord
sgt :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sgt = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SGT (\W256
x W256
y ->
  let sx, sy :: Int256
      sx :: Int256
sx = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x
      sy :: Int256
sy = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y
  in if Int256
sx Int256 -> Int256 -> Bool
forall a. Ord a => a -> a -> Bool
> Int256
sy then W256
1 else W256
0)

eq :: Expr EWord -> Expr EWord -> Expr EWord
eq :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
eq = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Eq (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
y then W256
1 else W256
0)

iszero :: Expr EWord -> Expr EWord
iszero :: Expr 'EWord -> Expr 'EWord
iszero = (Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256) -> Expr 'EWord -> Expr 'EWord
op1 Expr 'EWord -> Expr 'EWord
IsZero (\W256
x -> if W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then W256
1 else W256
0)

-- 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 W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
(.&.)

or :: Expr EWord -> Expr EWord -> Expr EWord
or :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
or = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Or W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
(.|.)

xor :: Expr EWord -> Expr EWord -> Expr EWord
xor :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
xor = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Xor W256 -> W256 -> W256
forall a. Bits a => a -> a -> a
Data.Bits.xor

not :: Expr EWord -> Expr EWord
not :: Expr 'EWord -> Expr 'EWord
not = (Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256) -> Expr 'EWord -> Expr 'EWord
op1 Expr 'EWord -> Expr 'EWord
Not W256 -> W256
forall a. Bits a => a -> a
complement

shl :: Expr EWord -> Expr EWord -> Expr EWord
shl :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
shl = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SHL (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
256 then W256
0 else W256 -> Int -> W256
forall a. Bits a => a -> Int -> a
shiftL W256
y (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x))

shr :: Expr EWord -> Expr EWord -> Expr EWord
shr :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
shr = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2
  (\Expr 'EWord
x Expr 'EWord
y -> case (Expr 'EWord
x, Expr 'EWord
y) of
             -- simplify function selector checks
             (Lit W256
0xe0, ReadWord (Lit W256
idx) Expr 'Buf
buf)
               -> [Expr 'Byte] -> Expr 'EWord
joinBytes (
                    Int -> Expr 'Byte -> [Expr 'Byte]
forall a. Int -> a -> [a]
replicate Int
28 (Word8 -> Expr 'Byte
LitByte Word8
0) [Expr 'Byte] -> [Expr 'Byte] -> [Expr 'Byte]
forall a. Semigroup a => a -> a -> a
<>
                      [ Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit W256
idx) Expr 'Buf
buf
                      , Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1) Expr 'Buf
buf
                      , Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
2) Expr 'Buf
buf
                      , Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
3) Expr 'Buf
buf])
             (Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SHR Expr 'EWord
x Expr 'EWord
y)
  (\W256
x W256
y -> if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
256 then W256
0 else W256 -> Int -> W256
forall a. Bits a => a -> Int -> a
shiftR W256
y (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x))

sar :: Expr EWord -> Expr EWord -> Expr EWord
sar :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sar = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
op2 Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SAR (\W256
x W256
y ->
  let msb :: Bool
msb = W256 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit W256
y Int
255
      asSigned :: Int256
asSigned = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
y :: Int256
  in if W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
256 then
       if Bool
msb then W256
forall a. Bounded a => a
maxBound else W256
0
     else
       Int256 -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int256 -> W256) -> Int256 -> W256
forall a b. (a -> b) -> a -> b
$ Int256 -> Int -> Int256
forall a. Bits a => a -> Int -> a
shiftR Int256
asSigned (W256 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
x))

-- ** 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 expression if necessary. 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.

-- fully 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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (Int
forall a. Bounded a => a
maxBound :: Int) Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ByteString -> Int
BS.length ByteString
b
    then Word8 -> Expr 'Byte
LitByte (HasCallStack => ByteString -> Int -> Word8
ByteString -> Int -> Word8
BS.index ByteString
b Int
i)
    else Word8 -> Expr 'Byte
LitByte Word8
0x0
  where
    i :: Int
    i :: Int
i = case W256
x of
          (W256 (Word256 Word128
_ (Word128 Word64
_ Word64
x'))) -> Word64 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto Word64
x'

readByte i :: Expr 'EWord
i@(Lit W256
x) (WriteByte (Lit W256
idx) Expr 'Byte
val Expr 'Buf
src)
  = if W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
idx
    then Expr 'Byte
val
    else Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
i Expr 'Buf
src
readByte i :: Expr 'EWord
i@(Lit W256
x) (WriteWord (Lit W256
idx) Expr 'EWord
val Expr 'Buf
src)
  = if W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
32
    then case Expr 'EWord
val of
           (Lit W256
_) -> Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
idx) Expr 'EWord
val
           Expr 'EWord
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'Byte
IndexWord (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
idx) Expr 'EWord
val
    else Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
i Expr 'Buf
src
readByte i :: Expr 'EWord
i@(Lit W256
x) (CopySlice (Lit W256
srcOffset) (Lit W256
dstOffset) (Lit W256
size) Expr 'Buf
src Expr 'Buf
dst)
  = if W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
size
    then Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- (W256
dstOffset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
srcOffset)) Expr 'Buf
src
    else Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
i Expr 'Buf
dst
readByte i :: Expr 'EWord
i@(Lit W256
x) buf :: Expr 'Buf
buf@(CopySlice Expr 'EWord
_ (Lit W256
dstOffset) (Lit W256
size) Expr 'Buf
_ Expr 'Buf
dst)
  -- the byte we are trying to read is completely outside of the sliced region
  = if W256
x W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size
    then Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
i Expr 'Buf
dst
    else Expr 'EWord -> Expr 'Buf -> Expr 'Byte
ReadByte (W256 -> Expr 'EWord
Lit W256
x) Expr 'Buf
buf

-- 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 (Int -> Int -> Int
forall a. Ord a => a -> a -> a
Prelude.min Int
32 -> Int
n) Expr 'EWord
idx Expr 'Buf
buf
  = [Expr 'Byte] -> Expr 'EWord
joinBytes [Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
idx (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Int -> W256) -> Int -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (Int -> Expr 'EWord) -> Int -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Int
i)) Expr 'Buf
buf | Int
i <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]

-- | 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 Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
idx' = Expr 'EWord
val
  | Bool
otherwise = case (Expr 'EWord
idx, Expr 'EWord
idx') of
    (Lit W256
i, Lit W256
i') ->
      if W256
i' W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
i W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
32 Bool -> Bool -> Bool
&& W256
i' W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
i W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= (W256
forall a. Bounded a => a
maxBound :: W256) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
31
      -- 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 W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
size Bool -> Bool -> Bool
&& W256
32 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
size W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
srcOff W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff)) Expr 'Buf
src
  -- the region we are trying to read is completely outside of the sliced region
  | (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
dstOff) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= (W256
forall a. Bounded a => a
maxBound :: W256) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
31 = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'Buf
dst
  -- 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 (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
word (ByteString -> W256) -> ByteString -> W256
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
padRight Int
32 (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take Int
32 (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.drop Int
i ByteString
bs
readWordFromBytes i :: Expr 'EWord
i@(Lit W256
idx) Expr 'Buf
buf = let
    bytes :: [Expr 'Byte]
bytes = [Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit W256
i') Expr 'Buf
buf | W256
i' <- [W256
idx .. W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
31]]
  in if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and ([Bool] -> Bool)
-> ([Expr 'Byte] -> [Bool]) -> [Expr 'Byte] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Bool) -> [Expr 'Byte] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) ([Expr 'Byte] -> Bool) -> [Expr 'Byte] -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bytes
     then W256 -> Expr 'EWord
Lit ([Word8] -> W256
bytesToW256 ([Word8] -> W256)
-> ([Expr 'Byte] -> [Word8]) -> [Expr 'Byte] -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'Byte -> Maybe Word8) -> [Expr 'Byte] -> [Word8]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
maybeLitByte ([Expr 'Byte] -> W256) -> [Expr 'Byte] -> W256
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bytes)
     else Expr 'EWord -> Expr 'Buf -> Expr 'EWord
ReadWord Expr 'EWord
i Expr 'Buf
buf
readWordFromBytes Expr 'EWord
idx Expr 'Buf
buf = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
ReadWord Expr 'EWord
idx Expr 'Buf
buf

{- | 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 = Word32 -> W256
forall target source. From source target => source -> target
into (Word32
forall a. Bounded a => a
maxBound :: Word32) W256 -> W256 -> W256
forall a. Integral a => a -> a -> a
`Prelude.div` W256
8

copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf

-- 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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) Word8
0
  | Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
e
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset sz :: Expr 'EWord
sz@(Lit W256
size) src :: Expr 'Buf
src@(ConcreteBuf ByteString
"") Expr 'Buf
dst
  | W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset (W256 -> Expr 'EWord
Lit W256
size) (ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) Word8
0) Expr 'Buf
dst
  | Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset Expr 'EWord
sz Expr 'Buf
src Expr 'Buf
dst

-- 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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (ByteString -> Int
BS.length ByteString
src), W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) Word8
0
  | W256
srcOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (ByteString -> Int
BS.length ByteString
src), W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes, W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes = let
    hd :: ByteString
hd = Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
dstOffset) Word8
0
    sl :: ByteString
sl = Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) (Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
srcOffset) ByteString
src)
    in ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ ByteString
hd ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
sl
  | Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
e

copySlice a :: Expr 'EWord
a@(Lit W256
srcOffset) b :: Expr 'EWord
b@(Lit W256
dstOffset) c :: Expr 'EWord
c@(Lit W256
size) d :: Expr 'Buf
d@(ConcreteBuf ByteString
src) e :: Expr 'Buf
e@(ConcreteBuf ByteString
dst)
  | W256
dstOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
  , W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes =
      let hd :: ByteString
hd = Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
dstOffset) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
dstOffset) ByteString
dst
          sl :: ByteString
sl = if W256
srcOffset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (ByteString -> Int
BS.length ByteString
src)
            then Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) Word8
0
            else Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) (Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
srcOffset) ByteString
src)
          tl :: ByteString
tl = Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
dstOffset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) ByteString
dst
      in ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ ByteString
hd ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
sl ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
tl
  | Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
e

-- 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 indices & 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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes, W256
size W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes, W256
srcOffset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ (W256
sizeW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
1) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
srcOffset = let
    hd :: ByteString
hd = Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
dstOffset) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
dstOffset) ByteString
dst
    sl :: [Expr 'Byte]
sl = [Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit W256
i) Expr 'Buf
src | W256
i <- [W256
srcOffset .. W256
srcOffset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ (W256
size W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1)]]
    tl :: ByteString
tl = Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
dstOffset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
size) ByteString
dst
    in if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and ([Bool] -> Bool)
-> ([Expr 'Byte] -> [Bool]) -> [Expr 'Byte] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Bool) -> [Expr 'Byte] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) ([Expr 'Byte] -> Bool) -> [Expr 'Byte] -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
sl
       then ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ ByteString
hd ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ([Word8] -> ByteString
BS.pack ([Word8] -> ByteString)
-> ([Expr 'Byte] -> [Word8]) -> [Expr 'Byte] -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Maybe Word8) -> [Expr 'Byte] -> [Word8]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
maybeLitByte) ([Expr 'Byte] -> ByteString) -> [Expr 'Byte] -> ByteString
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
sl) ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
tl
       else Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
s Expr 'EWord
d Expr 'EWord
sz Expr 'Buf
src Expr 'Buf
ds
  | Bool
otherwise = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
s Expr 'EWord
d Expr 'EWord
sz Expr 'Buf
src Expr 'Buf
ds

-- abstract indices
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset Expr 'EWord
size Expr 'Buf
src Expr 'Buf
dst = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset Expr 'EWord
size Expr 'Buf
src Expr 'Buf
dst


writeByte :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf
writeByte :: Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
writeByte (Lit W256
offset) (LitByte Word8
val) (ConcreteBuf ByteString
"")
  | W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
  = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
offset) Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Word8 -> ByteString
BS.singleton Word8
val
writeByte o :: Expr 'EWord
o@(Lit W256
offset) b :: Expr 'Byte
b@(LitByte Word8
byte) buf :: Expr 'Buf
buf@(ConcreteBuf ByteString
src)
  | W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
    = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ (Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
offset) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
offset) ByteString
src)
                 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> [Word8] -> ByteString
BS.pack [Word8
byte]
                 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ByteString
src
  | Bool
otherwise = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte Expr 'EWord
o Expr 'Byte
b Expr 'Buf
buf
writeByte Expr 'EWord
offset Expr 'Byte
byte Expr 'Buf
src = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte Expr 'EWord
offset Expr 'Byte
byte Expr 'Buf
src


writeWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf
writeWord :: Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord o :: Expr 'EWord
o@(Lit W256
offset) (WAddr (LitAddr Addr
val)) b :: Expr 'Buf
b@(ConcreteBuf ByteString
_)
  | W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes Bool -> Bool -> Bool
&& W256
offset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
  = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord Expr 'EWord
o (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Addr -> W256
forall target source. From source target => source -> target
into Addr
val) Expr 'Buf
b
writeWord (Lit W256
offset) (Lit W256
val) (ConcreteBuf ByteString
"")
  | W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes Bool -> Bool -> Bool
&& W256
offset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
  = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
offset) Word8
0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> W256 -> ByteString
word256Bytes W256
val
writeWord o :: Expr 'EWord
o@(Lit W256
offset) v :: Expr 'EWord
v@(Lit W256
val) buf :: Expr 'Buf
buf@(ConcreteBuf ByteString
src)
  | W256
offset W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes Bool -> Bool -> Bool
&& W256
offset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
    = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ (Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
offset) (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
offset) ByteString
src)
                 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> W256 -> ByteString
word256Bytes W256
val
                 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> Int -> ByteString -> ByteString
BS.drop ((W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
offset) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
32) ByteString
src
  | Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
o Expr 'EWord
v Expr 'Buf
buf
writeWord Expr 'EWord
idx Expr 'EWord
val b :: Expr 'Buf
b@(WriteWord Expr 'EWord
idx' Expr 'EWord
val' Expr 'Buf
buf)
  -- if the indices match exactly then we just replace the value in the current write and return
  | Expr 'EWord
idx Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
idx' = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
buf
  | Bool
otherwise
    = case (Expr 'EWord
idx, Expr 'EWord
idx') of
        (Lit W256
i, Lit W256
i') -> if W256
i W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
i' W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32
                           -- 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 expression will be returned.
bufLength :: Expr Buf -> Expr EWord
bufLength :: Expr 'Buf -> Expr 'EWord
bufLength = Map Int (Expr 'Buf) -> Bool -> Expr 'Buf -> Expr 'EWord
bufLengthEnv Map Int (Expr 'Buf)
forall a. Monoid a => a
mempty Bool
False

bufLengthEnv :: Map.Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord
bufLengthEnv :: Map Int (Expr 'Buf) -> Bool -> Expr 'Buf -> Expr 'EWord
bufLengthEnv Map Int (Expr 'Buf)
env Bool
useEnv Expr 'Buf
buf = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go (W256 -> Expr 'EWord
Lit W256
0) Expr 'Buf
buf
  where
    go :: Expr EWord -> Expr Buf -> Expr EWord
    go :: Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go Expr 'EWord
l (ConcreteBuf ByteString
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (W256 -> Expr 'EWord
Lit (Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (Int -> W256) -> (ByteString -> Int) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length (ByteString -> W256) -> ByteString -> W256
forall a b. (a -> b) -> a -> b
$ ByteString
b))
    go Expr 'EWord
l (AbstractBuf Text
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'Buf -> Expr 'EWord
BufLength (Text -> Expr 'Buf
AbstractBuf Text
b))
    go Expr 'EWord
l (WriteWord Expr 'EWord
idx Expr 'EWord
_ Expr 'Buf
b) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
idx (W256 -> Expr 'EWord
Lit W256
32))) Expr 'Buf
b
    go Expr 'EWord
l (WriteByte Expr 'EWord
idx Expr 'Byte
_ Expr 'Buf
b) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
idx (W256 -> Expr 'EWord
Lit W256
1))) Expr 'Buf
b
    go Expr 'EWord
l (CopySlice Expr 'EWord
_ Expr 'EWord
dstOffset Expr 'EWord
size Expr 'Buf
_ Expr 'Buf
dst) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
dstOffset Expr 'EWord
size)) Expr 'Buf
dst

    go Expr 'EWord
l (GVar (BufVar Int
a)) | Bool
useEnv =
      case Int -> Map Int (Expr 'Buf) -> Maybe (Expr 'Buf)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
a Map Int (Expr 'Buf)
env of
        Just Expr 'Buf
b -> Expr 'EWord -> Expr 'Buf -> Expr 'EWord
go Expr 'EWord
l Expr 'Buf
b
        Maybe (Expr 'Buf)
Nothing -> [Char] -> Expr 'EWord
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot compute length of open expression"
    go Expr 'EWord
l (GVar (BufVar Int
a)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
l (Expr 'Buf -> Expr 'EWord
BufLength (GVar 'Buf -> Expr 'Buf
forall (a :: EType). GVar a -> Expr a
GVar (Int -> GVar 'Buf
BufVar Int
a)))

-- | 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 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 then Maybe Integer
forall a. Maybe a
Nothing else Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ W256 -> Integer
forall target source. From source target => source -> target
into W256
l
    go W256
l (ConcreteBuf ByteString
b) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> (W256 -> Integer) -> W256 -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Integer
forall target source. From source target => source -> target
into (W256 -> Maybe Integer) -> W256 -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max (Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (Int -> W256) -> (ByteString -> Int) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Int
BS.length (ByteString -> W256) -> ByteString -> W256
forall a b. (a -> b) -> a -> b
$ ByteString
b) W256
l
    -- writes to a concrete index
    go W256
l (WriteWord (Lit W256
idx) Expr 'EWord
_ Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go (W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max W256
l (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
32)) Expr 'Buf
b
    go W256
l (WriteByte (Lit W256
idx) Expr 'Byte
_ Expr 'Buf
b) = W256 -> Expr 'Buf -> Maybe Integer
go (W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max W256
l (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1)) Expr 'Buf
b
    go W256
l (CopySlice Expr 'EWord
_ (Lit W256
dstOffset) (Lit W256
size) Expr 'Buf
_ Expr 'Buf
dst) = W256 -> Expr 'Buf -> Maybe Integer
go (W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max (W256
dstOffset W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
size) W256
l) Expr 'Buf
dst
    -- 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 <- Int -> Map Int (Expr 'Buf) -> Maybe (Expr 'Buf)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
a Map Int (Expr 'Buf)
bufEnv
      W256 -> Expr 'Buf -> Maybe Integer
go W256
l Expr 'Buf
b

-- returns the largest prefix that is guaranteed to be concrete (if one exists)
-- partial: will hard error if we encounter an input buf with a concrete size > 500mb
-- partial: will hard error if the prefix is > 500mb
concretePrefix :: Expr Buf -> Vector Word8
concretePrefix :: Expr 'Buf -> Vector Word8
concretePrefix Expr 'Buf
b = (forall s. ST s (MVector s Word8)) -> Vector Word8
forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create ((forall s. ST s (MVector s Word8)) -> Vector Word8)
-> (forall s. ST s (MVector s Word8)) -> Vector Word8
forall a b. (a -> b) -> a -> b
$ do
    MVector s Word8
v <- Int -> ST s (MVector (PrimState (ST s)) Word8)
forall (m :: * -> *) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MV.new (Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
1024 Maybe Int
inputLen)
    (Int
filled, MVector s Word8
v') <- Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
forall s. Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go Int
0 MVector s Word8
v
    MVector s Word8 -> ST s (MVector s Word8)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MVector s Word8 -> ST s (MVector s Word8))
-> MVector s Word8 -> ST s (MVector s Word8)
forall a b. (a -> b) -> a -> b
$ Int -> MVector s Word8 -> MVector s Word8
forall s a. Int -> MVector s a -> MVector s a
MV.take Int
filled MVector s Word8
v'
  where

    -- if our prefix is > 500mb then we have other issues and should just bail...
    maxIdx :: Num i => i
    maxIdx :: forall i. Num i => i
maxIdx = i
500 i -> i -> i
forall a. Num a => a -> a -> a
* (i
10 i -> Int -> i
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
6 :: Int))

    -- attempts to compute a concrete length for the input buffer
    inputLen :: Maybe Int
    inputLen :: Maybe Int
inputLen = case Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
b of
      Lit W256
s -> if W256
s W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
forall i. Num i => i
maxIdx
        then [Char] -> Maybe Int
forall a. HasCallStack => [Char] -> a
internalError [Char]
"concretePrefix: input buffer size exceeds 500mb"
        -- unsafeInto: s is <= 500,000,000
        else Int -> Maybe Int
forall a. a -> Maybe a
Just (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
s)
      Expr 'EWord
_ -> Maybe Int
forall a. Maybe a
Nothing

    -- recursively reads successive bytes from `b` until we reach a symbolic
    -- byte returns the large index read from and a reference to the mutable
    -- vec (might not be the same as the input because of the call to grow)
    go :: forall s . Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
    go :: forall s. Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go Int
i MVector s Word8
v
      -- if the prefix is very large then bail
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
forall i. Num i => i
maxIdx = [Char] -> ST s (Int, MVector s Word8)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"concretePrefix: prefix size exceeds 500mb"
      -- if the input buffer has a concrete size, then don't read past the end
      | Just Int
mr <- Maybe Int
inputLen, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
mr = (Int, MVector s Word8) -> ST s (Int, MVector s Word8)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
i, MVector s Word8
v)
      -- double the size of the vector if we've reached the end
      | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= MVector s Word8 -> Int
forall s a. MVector s a -> Int
MV.length MVector s Word8
v = do
        MVector s Word8
v' <- MVector (PrimState (ST s)) Word8
-> Int -> ST s (MVector (PrimState (ST s)) Word8)
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> m (MVector (PrimState m) a)
MV.grow MVector s Word8
MVector (PrimState (ST s)) Word8
v (MVector s Word8 -> Int
forall s a. MVector s a -> Int
MV.length MVector s Word8
v)
        Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
forall s. Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go Int
i MVector s Word8
v'
      -- read the byte at `i` in `b` into `v` if it is concrete, or halt if we've reached a symbolic byte
      -- unsafeInto: i will always be positive
      | Bool
otherwise = case Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Int -> W256) -> Int -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (Int -> Expr 'EWord) -> Int -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Int
i) Expr 'Buf
b of
          LitByte Word8
byte -> do
            MVector (PrimState (ST s)) Word8 -> Int -> Word8 -> ST s ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s Word8
MVector (PrimState (ST s)) Word8
v Int
i Word8
byte
            Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
forall s. Int -> MVector s Word8 -> ST s (Int, MVector s Word8)
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) MVector s Word8
v
          Expr 'Byte
_ -> (Int, MVector s Word8) -> ST s (Int, MVector s Word8)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
i, MVector s Word8
v)


word256At :: Expr EWord -> Lens (Expr Buf) (Expr Buf) (Expr EWord) (Expr EWord)
word256At :: Expr 'EWord
-> Lens (Expr 'Buf) (Expr 'Buf) (Expr 'EWord) (Expr 'EWord)
word256At Expr 'EWord
i = (Expr 'Buf -> Expr 'EWord)
-> (Expr 'Buf -> Expr 'EWord -> Expr 'Buf)
-> Lens (Expr 'Buf) (Expr 'Buf) (Expr 'EWord) (Expr 'EWord)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens Expr 'Buf -> Expr 'EWord
getter Expr 'Buf -> Expr 'EWord -> Expr 'Buf
setter where
  getter :: Expr 'Buf -> Expr 'EWord
getter = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord Expr 'EWord
i
  setter :: Expr 'Buf -> Expr 'EWord -> Expr 'Buf
setter Expr 'Buf
m Expr 'EWord
x = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord Expr 'EWord
i Expr 'EWord
x Expr 'Buf
m

-- | 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 Expr 'Buf
forall a. Monoid a => a
mempty


toList :: Expr Buf -> Maybe (V.Vector (Expr Byte))
toList :: Expr 'Buf -> Maybe (Vector (Expr 'Byte))
toList (AbstractBuf Text
_) = Maybe (Vector (Expr 'Byte))
forall a. Maybe a
Nothing
toList (ConcreteBuf ByteString
bs) = Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte))
forall a. a -> Maybe a
Just (Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte)))
-> Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte))
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte] -> Vector (Expr 'Byte)
forall a. [a] -> Vector a
V.fromList ([Expr 'Byte] -> Vector (Expr 'Byte))
-> [Expr 'Byte] -> Vector (Expr 'Byte)
forall a b. (a -> b) -> a -> b
$ Word8 -> Expr 'Byte
LitByte (Word8 -> Expr 'Byte) -> [Word8] -> [Expr 'Byte]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ByteString -> [Word8]
BS.unpack ByteString
bs
toList Expr 'Buf
buf = case Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
buf of
  Lit W256
l -> if W256
l W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (Int
forall a. Bounded a => a
maxBound :: Int)
              then Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte))
forall a. a -> Maybe a
Just (Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte)))
-> Vector (Expr 'Byte) -> Maybe (Vector (Expr 'Byte))
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Expr 'Byte) -> Vector (Expr 'Byte)
forall a. Int -> (Int -> a) -> Vector a
V.generate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
l) (\Int
i -> Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto Int
i) Expr 'Buf
buf)
              else [Char] -> Maybe (Vector (Expr 'Byte))
forall a. HasCallStack => [Char] -> a
internalError [Char]
"overflow when converting buffer to list"
  Expr 'EWord
_ -> Maybe (Vector (Expr 'Byte))
forall a. Maybe a
Nothing

fromList :: V.Vector (Expr Byte) -> Expr Buf
fromList :: Vector (Expr 'Byte) -> Expr 'Buf
fromList Vector (Expr 'Byte)
bs = case Vector Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and ((Expr 'Byte -> Bool) -> Vector (Expr 'Byte) -> Vector Bool
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte Vector (Expr 'Byte)
bs) of
  Bool
True -> ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf)
-> (Vector (Expr 'Byte) -> ByteString)
-> Vector (Expr 'Byte)
-> Expr 'Buf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack ([Word8] -> ByteString)
-> (Vector (Expr 'Byte) -> [Word8])
-> Vector (Expr 'Byte)
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Word8 -> [Word8]
forall a. Vector a -> [a]
V.toList (Vector Word8 -> [Word8])
-> (Vector (Expr 'Byte) -> Vector Word8)
-> Vector (Expr 'Byte)
-> [Word8]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'Byte -> Maybe Word8) -> Vector (Expr 'Byte) -> Vector Word8
forall a b. (a -> Maybe b) -> Vector a -> Vector b
V.mapMaybe Expr 'Byte -> Maybe Word8
maybeLitByte (Vector (Expr 'Byte) -> Expr 'Buf)
-> Vector (Expr 'Byte) -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ Vector (Expr 'Byte)
bs
  -- we want to minimize the size of the resulting expression, 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 -> (Expr 'Buf -> Int -> Expr 'Byte -> Expr 'Buf)
-> Expr 'Buf -> Vector (Expr 'Byte) -> Expr 'Buf
forall a b. (a -> Int -> b -> a) -> a -> Vector b -> a
V.ifoldl' Expr 'Buf -> Int -> Expr 'Byte -> Expr 'Buf
applySymWrites (ByteString -> Expr 'Buf
ConcreteBuf ByteString
concreteBytes) Vector (Expr 'Byte)
bs
    where
      concreteBytes :: ByteString
      concreteBytes :: ByteString
concreteBytes = Vector Word8 -> ByteString
forall a. Storable a => Vector a -> ByteString
vectorToByteString (Vector Word8 -> ByteString) -> Vector Word8 -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> Word8) -> Vector Word8
forall a. Storable a => Int -> (Int -> a) -> Vector a
VS.generate (Vector (Expr 'Byte) -> Int
forall a. Vector a -> Int
V.length Vector (Expr 'Byte)
bs) (\Int
idx ->
        case Vector (Expr 'Byte)
bs Vector (Expr 'Byte) -> Int -> Expr 'Byte
forall a. Vector a -> Int -> a
V.! Int
idx of
          LitByte Word8
b -> Word8
b
          Expr 'Byte
_ -> Word8
0)

      applySymWrites :: Expr Buf -> Int -> Expr Byte -> Expr Buf
      applySymWrites :: Expr 'Buf -> Int -> Expr 'Byte -> Expr 'Buf
applySymWrites Expr 'Buf
buf Int
_ (LitByte Word8
_) = Expr 'Buf
buf
      applySymWrites Expr 'Buf
buf Int
idx Expr 'Byte
by = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto Int
idx) Expr 'Byte
by Expr 'Buf
buf

instance Semigroup (Expr Buf) where
  (ConcreteBuf ByteString
a) <> :: Expr 'Buf -> Expr 'Buf -> Expr 'Buf
<> (ConcreteBuf ByteString
b) = ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ ByteString
a ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
b
  Expr 'Buf
a <> Expr 'Buf
b = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice (W256 -> Expr 'EWord
Lit W256
0) (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
a) (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
b) Expr 'Buf
b Expr 'Buf
a

instance Monoid (Expr Buf) where
  mempty :: Expr 'Buf
mempty = ByteString -> Expr 'Buf
ConcreteBuf ByteString
""

-- | 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 (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$ case W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
off W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
size of
                                    Bool
True -> case forall source target.
TryFrom source target =>
source -> Either (TryFromException source target) target
tryFrom @W256 (W256
off W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
size) of
                                      Right Int
n -> Int -> ByteString -> ByteString
BS.take Int
n ByteString
b
                                      Left TryFromException W256 Int
_ -> ByteString
b
                                    Bool
False -> ByteString
b
  WriteByte (Lit W256
idx) Expr 'Byte
v Expr 'Buf
prev
    -> if W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size
       then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev
       else Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte (W256 -> Expr 'EWord
Lit W256
idx) Expr 'Byte
v (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev)
  -- TODO: handle partial overlaps
  WriteWord (Lit W256
idx) Expr 'EWord
v Expr 'Buf
prev
    -> if W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= (W256
forall a. Bounded a => a
maxBound :: W256) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
31
       then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev
       else Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'EWord
v (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev)
  CopySlice (Lit W256
srcOff) (Lit W256
dstOff) (Lit W256
size') Expr 'Buf
src Expr 'Buf
dst
    -> if W256
dstOff W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
size Bool -> Bool -> Bool
&& W256
dstOff W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
off W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= (W256
forall a. Bounded a => a
maxBound :: W256) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
size' W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1
       then W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
dst
       else Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice (W256 -> Expr 'EWord
Lit W256
srcOff) (W256 -> Expr 'EWord
Lit W256
dstOff) (W256 -> Expr 'EWord
Lit W256
size')
                      (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
srcOff W256
size' Expr 'Buf
src)
                      (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
dst)
  WriteByte Expr 'EWord
i Expr 'Byte
v Expr 'Buf
prev -> Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte Expr 'EWord
i Expr 'Byte
v (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev)
  WriteWord Expr 'EWord
i Expr 'EWord
v Expr 'Buf
prev -> Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
i Expr 'EWord
v (W256 -> W256 -> Expr 'Buf -> Expr 'Buf
stripWrites W256
off W256
size Expr 'Buf
prev)
  CopySlice Expr 'EWord
srcOff Expr 'EWord
dstOff Expr 'EWord
size' Expr 'Buf
src Expr 'Buf
dst -> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
srcOff Expr 'EWord
dstOff Expr 'EWord
size' Expr 'Buf
src Expr 'Buf
dst
  GVar GVar 'Buf
_ ->  [Char] -> Expr 'Buf
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Unexpected GVar in stripWrites"


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


readStorage' :: Expr EWord -> Expr Storage -> Expr EWord
readStorage' :: Expr 'EWord -> Expr 'Storage -> Expr 'EWord
readStorage' Expr 'EWord
loc Expr 'Storage
store = case Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
loc Expr 'Storage
store of
                           Just Expr 'EWord
v -> Expr 'EWord
v
                           Maybe (Expr 'EWord)
Nothing -> W256 -> Expr 'EWord
Lit W256
0

-- | 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 Storage -> Maybe (Expr EWord)
readStorage :: Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
readStorage Expr 'EWord
w Expr 'Storage
st = Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
w) Expr 'Storage
st
  where
    go :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
    go :: Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
_ (GVar GVar 'Storage
_) = [Char] -> Maybe (Expr 'EWord)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Can't read from a GVar"
    go Expr 'EWord
slot s :: Expr 'Storage
s@(AbstractStore Expr 'EAddr
_ Maybe W256
_) = Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
Just (Expr 'EWord -> Maybe (Expr 'EWord))
-> Expr 'EWord -> Maybe (Expr 'EWord)
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
slot Expr 'Storage
s
    go (Lit W256
l) (ConcreteStore Map W256 W256
s) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> Maybe W256 -> Maybe (Expr 'EWord)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> W256 -> Map W256 W256 -> Maybe W256
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup W256
l Map W256 W256
s
    go Expr 'EWord
slot store :: Expr 'Storage
store@(ConcreteStore Map W256 W256
_) = Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
Just (Expr 'EWord -> Maybe (Expr 'EWord))
-> Expr 'EWord -> Maybe (Expr 'EWord)
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
slot Expr 'Storage
store
    go Expr 'EWord
slot s :: Expr 'Storage
s@(SStore Expr 'EWord
prevSlot Expr 'EWord
val Expr 'Storage
prev) = case (Expr 'EWord
prevSlot, Expr 'EWord
slot) of
      -- if address and slot match then we return the val in this write
      (Expr 'EWord, Expr 'EWord)
_ | Expr 'EWord
prevSlot Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
slot -> Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
Just Expr 'EWord
val

      -- if the slots don't match (see previous guard) and are lits, we can skip this write
      (Lit W256
_, Lit W256
_) -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      -- slot is for a map + map -> skip write
      (MappingSlot ByteString
idA Expr 'EWord
_, MappingSlot ByteString
idB Expr 'EWord
_)     | ByteString -> ByteString -> Bool
idsDontMatch ByteString
idA ByteString
idB  -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      (MappingSlot ByteString
_ Expr 'EWord
keyA, MappingSlot ByteString
_ Expr 'EWord
keyB)   | Expr 'EWord -> Expr 'EWord -> Bool
forall (a :: EType). Expr a -> Expr a -> Bool
surelyNotEq Expr 'EWord
keyA Expr 'EWord
keyB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      -- special case of array + map -> skip write
      (ArraySlotWithOffset ByteString
idA Expr 'EWord
_, Expr 'EWord
Keccak64Bytes) | ByteString -> Int
BS.length ByteString
idA Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      (ArraySlotZero ByteString
idA, Expr 'EWord
Keccak64Bytes)         | ByteString -> Int
BS.length ByteString
idA Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      -- special case of array + map -> skip write
      (Expr 'EWord
Keccak64Bytes, ArraySlotWithOffset ByteString
idA Expr 'EWord
_) | ByteString -> Int
BS.length ByteString
idA Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      (Expr 'EWord
Keccak64Bytes, ArraySlotZero ByteString
idA)         | ByteString -> Int
BS.length ByteString
idA Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
64 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      -- Fixed SMALL value will never match Keccak (well, it might, but that's VERY low chance)
      (Lit W256
a, Keccak Expr 'Buf
_) | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      (Keccak Expr 'Buf
_, Lit W256
a) | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      -- the chance of adding a value <= 2^32 to any given keccack output
      -- leading to an overflow is effectively zero. the chance of an overflow
      -- occurring here is 2^32/2^256 = 2^-224, which is close enough to zero
      -- for our purposes. This lets us completely simplify reads from write
      -- chains involving writes to arrays at literal offsets.
      (Lit W256
a, Add (Lit W256
b) (Keccak Expr 'Buf
_) ) | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256, W256
b W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxW32 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      (Add (Lit W256
a) (Keccak Expr 'Buf
_) , Lit W256
b) | W256
b W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256, W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxW32 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      --- NOTE these are needed to succeed in rewriting arrays with a variable index
      -- (Lit a, Add (Keccak _) (Var _) ) | a < 256 -> go slot prev
      -- (Add (Keccak _) (Var _) , Lit b) | b < 256 -> go slot prev

      -- Finding two Keccaks that are < 256 away from each other should be VERY hard
      -- This simplification allows us to deal with maps of structs
      (Add (Lit W256
a2) (Keccak Expr 'Buf
_), Add (Lit W256
b2) (Keccak Expr 'Buf
_)) | W256
a2 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
b2, W256 -> W256
forall a. Num a => a -> a
abs(W256
a2W256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
b2) W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      (Add (Lit W256
a2) (Keccak Expr 'Buf
_), (Keccak Expr 'Buf
_)) | W256
a2 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
0, W256
a2 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      ((Keccak Expr 'Buf
_), Add (Lit W256
b2) (Keccak Expr 'Buf
_)) | W256
b2 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
0, W256
b2 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      -- case of array + array, but different id's or different concrete offsets
      -- zero offs vs zero offs
      (ArraySlotZero ByteString
idA, ArraySlotZero ByteString
idB)                   | ByteString
idA ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      -- zero offs vs non-zero offs
      (ArraySlotZero ByteString
idA, ArraySlotWithOffset ByteString
idB Expr 'EWord
_)           | ByteString
idA ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      (ArraySlotZero ByteString
_, ArraySlotWithOffset ByteString
_ (Lit W256
offB))      | W256
offB W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
0  -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      -- non-zero offs vs zero offs
      (ArraySlotWithOffset ByteString
idA Expr 'EWord
_, ArraySlotZero ByteString
idB)           | ByteString
idA ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      (ArraySlotWithOffset ByteString
_ (Lit W256
offA), ArraySlotZero ByteString
_)      | W256
offA W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
0  -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev
      -- non-zero offs vs non-zero offs
      (ArraySlotWithOffset ByteString
idA Expr 'EWord
_, ArraySlotWithOffset ByteString
idB Expr 'EWord
_)   | ByteString
idA ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
idB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      (ArraySlotWithOffset ByteString
_ Expr 'EWord
offA, ArraySlotWithOffset ByteString
_ Expr 'EWord
offB) | Expr 'EWord -> Expr 'EWord -> Bool
forall (a :: EType). Expr a -> Expr a -> Bool
surelyNotEq Expr 'EWord
offA Expr 'EWord
offB -> Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
go Expr 'EWord
slot Expr 'Storage
prev

      -- we are unable to determine statically whether or not we can safely move deeper in the write chain, so return an abstract term
      (Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
Just (Expr 'EWord -> Maybe (Expr 'EWord))
-> Expr 'EWord -> Maybe (Expr 'EWord)
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
slot Expr 'Storage
s

    surelyNotEq :: Expr a -> Expr a -> Bool
    surelyNotEq :: forall (a :: EType). Expr a -> Expr a -> Bool
surelyNotEq (Lit W256
a) (Lit W256
b) = W256
a W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
b
    -- never equal: x+y (y is concrete) vs x+z (z is concrete), y!=z
    surelyNotEq (Add (Lit W256
l1) Expr 'EWord
v1) (Add (Lit W256
l2) Expr 'EWord
v2) = W256
l1 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
l2 Bool -> Bool -> Bool
&& Expr 'EWord
v1 Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
v2
    -- never equal: x+y (y is concrete, non-zero) vs x
    surelyNotEq Expr a
v1 (Add (Lit W256
l2) Expr 'EWord
v2) = W256
l2 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
0 Bool -> Bool -> Bool
&& Expr a
v1 Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
Expr 'EWord
v2
    surelyNotEq (Add (Lit W256
l1) Expr 'EWord
v1) Expr a
v2 = W256
l1 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
0 Bool -> Bool -> Bool
&& Expr 'EWord
v1 Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
Expr 'EWord
v2
    surelyNotEq Expr a
_ Expr a
_ = Bool
False

    maxW32 :: W256
    maxW32 :: W256
maxW32 = Word32 -> W256
forall target source. From source target => source -> target
into (Word32
forall a. Bounded a => a
maxBound :: Word32)

-- storage slots for maps are determined by (keccak (bytes32(key) ++ bytes32(id)))
pattern MappingSlot :: ByteString -> Expr EWord -> Expr EWord
pattern $mMappingSlot :: forall {r}.
Expr 'EWord
-> (ByteString -> Expr 'EWord -> r) -> ((# #) -> r) -> r
$bMappingSlot :: ByteString -> Expr 'EWord -> Expr 'EWord
MappingSlot id key = Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) (WriteWord (Lit 0) key (ConcreteBuf id)) (ConcreteBuf ""))

-- keccak of any 64 bytes value
pattern Keccak64Bytes :: Expr EWord
pattern $mKeccak64Bytes :: forall {r}. Expr 'EWord -> ((# #) -> r) -> ((# #) -> r) -> r
Keccak64Bytes <- Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) _ (ConcreteBuf ""))

-- storage slots for arrays are determined by (keccak(bytes32(id)) + offset)
-- note that `normArgs` puts the Lit as the 2nd argument to `Add`
pattern ArraySlotWithOffset :: ByteString -> Expr EWord -> Expr EWord
pattern $mArraySlotWithOffset :: forall {r}.
Expr 'EWord
-> (ByteString -> Expr 'EWord -> r) -> ((# #) -> r) -> r
$bArraySlotWithOffset :: ByteString -> Expr 'EWord -> Expr 'EWord
ArraySlotWithOffset id offset = Add (Keccak (ConcreteBuf id)) offset

-- special pattern to match the 0th element because the `Add` term gets simplified out
pattern ArraySlotZero :: ByteString -> Expr EWord
pattern $mArraySlotZero :: forall {r}. Expr 'EWord -> (ByteString -> r) -> ((# #) -> r) -> r
$bArraySlotZero :: ByteString -> Expr 'EWord
ArraySlotZero id = Keccak (ConcreteBuf id)

-- checks if two mapping ids match or not
idsDontMatch :: ByteString -> ByteString -> Bool
idsDontMatch :: ByteString -> ByteString -> Bool
idsDontMatch ByteString
a ByteString
b = ByteString -> Int
BS.length ByteString
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
64 Bool -> Bool -> Bool
&& ByteString -> Int
BS.length ByteString
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
64 Bool -> Bool -> Bool
&& ByteString -> ByteString -> Bool
diff32to64Byte ByteString
a ByteString
b
  where
    diff32to64Byte :: ByteString -> ByteString -> Bool
    diff32to64Byte :: ByteString -> ByteString -> Bool
diff32to64Byte ByteString
x ByteString
y = ByteString
x32 ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
/= ByteString
y32
      where
       x32 :: ByteString
x32 = Int -> ByteString -> ByteString
BS.take Int
32 (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.drop Int
32 ByteString
x
       y32 :: ByteString
y32 = Int -> ByteString -> ByteString
BS.take Int
32 (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.drop Int
32 ByteString
y

slotPos :: Word8 -> ByteString
slotPos :: Word8 -> ByteString
slotPos Word8
pos = [Word8] -> ByteString
BS.pack ((Int -> Word8 -> [Word8]
forall a. Int -> a -> [a]
replicate Int
31 (Word8
0::Word8))[Word8] -> [Word8] -> [Word8]
forall a. [a] -> [a] -> [a]
++[Word8
pos])

-- | Turns Literals into keccak(bytes32(id)) + offset (i.e. writes to arrays)
structureArraySlots :: Expr a -> Expr a
structureArraySlots :: forall (a :: EType). Expr a -> Expr a
structureArraySlots Expr a
e = (forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go Expr a
e
  where
    go :: Expr a -> Expr a
    go :: forall (a :: EType). Expr a -> Expr a
go orig :: Expr a
orig@(Lit W256
key) = case W256 -> Maybe (Word8, W256)
litToArrayPreimage W256
key of
      Just (Word8
array, W256
offset) -> ByteString -> Expr 'EWord -> Expr 'EWord
ArraySlotWithOffset (Word8 -> ByteString
slotPos Word8
array) (W256 -> Expr 'EWord
Lit W256
offset)
      Maybe (Word8, W256)
_ -> Expr a
orig
    go Expr a
a = Expr a
a

-- Takes in value, checks if it's within 256 of a pre-computed array hash value
-- if it is, it returns (array_number, offset)
litToArrayPreimage :: W256 -> Maybe (Word8, W256)
litToArrayPreimage :: W256 -> Maybe (Word8, W256)
litToArrayPreimage W256
val = [(W256, Word8)] -> Maybe (Word8, W256)
go [(W256, Word8)]
preImages
  where
    go :: [(W256, Word8)] -> Maybe (Word8, W256)
    go :: [(W256, Word8)] -> Maybe (Word8, W256)
go ((W256
image, Word8
preimage):[(W256, Word8)]
ax) = if W256
val W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
image Bool -> Bool -> Bool
&& W256
valW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
image W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
255 then (Word8, W256) -> Maybe (Word8, W256)
forall a. a -> Maybe a
Just (Word8
preimage, W256
valW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
image)
                                                                    else [(W256, Word8)] -> Maybe (Word8, W256)
go [(W256, Word8)]
ax
    go [] = Maybe (Word8, W256)
forall a. Maybe a
Nothing

-- | 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 Storage -> Expr Storage
writeStorage :: Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage k :: Expr 'EWord
k@(Lit W256
key) v :: Expr 'EWord
v@(Lit W256
val) Expr 'Storage
store = case Expr 'Storage
store of
  ConcreteStore Map W256 W256
s -> Map W256 W256 -> Expr 'Storage
ConcreteStore (W256 -> W256 -> Map W256 W256 -> Map W256 W256
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert W256
key W256
val Map W256 W256
s)
  Expr 'Storage
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
k Expr 'EWord
v Expr 'Storage
store
writeStorage Expr 'EWord
key Expr 'EWord
val store :: Expr 'Storage
store@(SStore Expr 'EWord
key' Expr 'EWord
val' Expr 'Storage
prev)
     = if Expr 'EWord
key Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
key'
       -- if we're overwriting an existing location, then drop the write
       then Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key Expr 'EWord
val Expr 'Storage
prev
       else case (Expr 'EWord
key, Expr 'EWord
key') of
              -- 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
k, Lit W256
k') -> if W256
k W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
k'
                                 then Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key' Expr 'EWord
val' (Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage Expr 'EWord
key Expr 'EWord
val Expr 'Storage
prev)
                                 else Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
              -- otherwise stack a new write on top of the the existing write chain
              (Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store
writeStorage Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store = Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key Expr 'EWord
val Expr 'Storage
store


getAddr :: Expr Storage -> Maybe (Expr EAddr)
getAddr :: Expr 'Storage -> Maybe (Expr 'EAddr)
getAddr (SStore Expr 'EWord
_ Expr 'EWord
_ Expr 'Storage
p) = Expr 'Storage -> Maybe (Expr 'EAddr)
getAddr Expr 'Storage
p
getAddr (AbstractStore Expr 'EAddr
a Maybe W256
_) = Expr 'EAddr -> Maybe (Expr 'EAddr)
forall a. a -> Maybe a
Just Expr 'EAddr
a
getAddr (ConcreteStore Map W256 W256
_) = Maybe (Expr 'EAddr)
forall a. Maybe a
Nothing
getAddr (GVar GVar 'Storage
_) = [Char] -> Maybe (Expr 'EAddr)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot determine addr of a GVar"

getLogicalIdx :: Expr Storage -> Maybe W256
getLogicalIdx :: Expr 'Storage -> Maybe W256
getLogicalIdx (SStore Expr 'EWord
_ Expr 'EWord
_ Expr 'Storage
p) = Expr 'Storage -> Maybe W256
getLogicalIdx Expr 'Storage
p
getLogicalIdx (AbstractStore Expr 'EAddr
_ Maybe W256
idx) = Maybe W256
idx
getLogicalIdx (ConcreteStore Map W256 W256
_) = Maybe W256
forall a. Maybe a
Nothing
getLogicalIdx (GVar GVar 'Storage
_) = [Char] -> Maybe W256
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot determine addr of a GVar"


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


data StorageType = SmallSlot | Array | Map | Mixed | UNK
  deriving (Int -> StorageType -> ShowS
[StorageType] -> ShowS
StorageType -> [Char]
(Int -> StorageType -> ShowS)
-> (StorageType -> [Char])
-> ([StorageType] -> ShowS)
-> Show StorageType
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StorageType -> ShowS
showsPrec :: Int -> StorageType -> ShowS
$cshow :: StorageType -> [Char]
show :: StorageType -> [Char]
$cshowList :: [StorageType] -> ShowS
showList :: [StorageType] -> ShowS
Show, StorageType -> StorageType -> Bool
(StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool) -> Eq StorageType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StorageType -> StorageType -> Bool
== :: StorageType -> StorageType -> Bool
$c/= :: StorageType -> StorageType -> Bool
/= :: StorageType -> StorageType -> Bool
Eq)

safeToDecompose :: Expr a -> Bool
safeToDecompose :: forall (a :: EType). Expr a -> Bool
safeToDecompose Expr a
inp = StorageType
result StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
/= StorageType
Mixed
  where
    result :: StorageType
result = State StorageType () -> StorageType -> StorageType
forall s a. State s a -> s -> s
execState (Expr a -> State StorageType ()
forall (a :: EType). Expr a -> State StorageType ()
safeToDecomposeRunner Expr a
inp) StorageType
UNK

    safeToDecomposeRunner :: forall a. Expr a -> State StorageType ()
    safeToDecomposeRunner :: forall (a :: EType). Expr a -> State StorageType ()
safeToDecomposeRunner Expr a
a = Expr a -> State StorageType ()
forall (a :: EType). Expr a -> State StorageType ()
go Expr a
a

    go :: forall b. Expr b -> State StorageType ()
    go :: forall (a :: EType). Expr a -> State StorageType ()
go e :: Expr b
e@(SLoad (MappingSlot {}) Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setMap Expr b
e
    go e :: Expr b
e@(SLoad (ArraySlotZero {}) Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setArray Expr b
e
    go e :: Expr b
e@(SLoad (ArraySlotWithOffset {}) Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setArray Expr b
e
    go e :: Expr b
e@(SLoad (Lit W256
x) Expr 'Storage
_) | W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setSmall Expr b
e
    go e :: Expr b
e@(SLoad Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setMixed Expr b
e
    go e :: Expr b
e@(SStore (MappingSlot {}) Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setMap Expr b
e
    go e :: Expr b
e@(SStore (ArraySlotZero {}) Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setArray Expr b
e
    go e :: Expr b
e@(SStore (ArraySlotWithOffset {}) Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setArray Expr b
e
    go e :: Expr b
e@(SStore (Lit W256
x) Expr 'EWord
_ Expr 'Storage
_) | W256
x W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256 = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setSmall Expr b
e
    go e :: Expr b
e@(SStore Expr 'EWord
_ Expr 'EWord
_ Expr 'Storage
_) = Expr b -> State StorageType ()
forall {m :: * -> *} {p}. MonadState StorageType m => p -> m ()
setMixed Expr b
e
    go Expr b
_ = () -> State StorageType ()
forall a. a -> StateT StorageType Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    -- Helper functions for detecting mixed load/store
    setMixed :: p -> m ()
setMixed p
_ = do
      StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
      () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    setMap :: p -> m ()
setMap p
_ = do
      StorageType
s <- m StorageType
forall s (m :: * -> *). MonadState s m => m s
get
      case StorageType
s of
        StorageType
Array -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
        StorageType
SmallSlot -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
        StorageType
UNK -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Map
        StorageType
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    setArray :: p -> m ()
setArray p
_ = do
      StorageType
s <- m StorageType
forall s (m :: * -> *). MonadState s m => m s
get
      case StorageType
s of
        StorageType
Map -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
        StorageType
SmallSlot -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
        StorageType
UNK -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Array
        StorageType
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    setSmall :: p -> m ()
setSmall p
_ = do
      StorageType
s <- m StorageType
forall s (m :: * -> *). MonadState s m => m s
get
      case StorageType
s of
        StorageType
Map -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
        StorageType
Array -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
Mixed
        StorageType
UNK -> StorageType -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put StorageType
SmallSlot
        StorageType
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Splits storage into logical sub-stores if (1) all SLoad->SStore* chains are one of:
--     (1a) Lit < 256, (1b) MappingSlot, (1c) ArraySlotWithOffset, (1d) ArraySlotZero
--  and (2) there is no mixing of different types (e.g. Map with Array) within
--  the same SStore -> SLoad* chain, and (3) there is no mixing of different array/map slots.
--
--  Mixing (2) and (3) are attempted to be prevented (if possible) as part of the rewrites
--  done by the `readStorage` function that is ran before this. If there is still mixing here,
--  we abort with a Nothing.
--
--  We do NOT rewrite stand-alone `SStore`-s (i.e. SStores that are not read), since
--  they are often used to describe a post-state, and are not dispatched as-is to
--  the solver
decomposeStorage :: Expr a -> Maybe (Expr a)
decomposeStorage :: forall (a :: EType). Expr a -> Maybe (Expr a)
decomposeStorage = Expr a -> Maybe (Expr a)
forall (a :: EType). Expr a -> Maybe (Expr a)
go
  where
    go :: Expr a -> Maybe (Expr a)
    go :: forall (a :: EType). Expr a -> Maybe (Expr a)
go e :: Expr a
e@(SLoad Expr 'EWord
origKey Expr 'Storage
store) = if Bool -> Bool
Prelude.not (Expr a -> Bool
forall (a :: EType). Expr a -> Bool
safeToDecompose Expr a
e) then Maybe (Expr a)
forall a. Maybe a
Nothing else Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
tryRewrite Expr 'EWord
origKey Expr 'Storage
store
    go Expr a
e = Expr a -> Maybe (Expr a)
forall a. a -> Maybe a
Just Expr a
e

    tryRewrite :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
    tryRewrite :: Expr 'EWord -> Expr 'Storage -> Maybe (Expr 'EWord)
tryRewrite Expr 'EWord
origKey Expr 'Storage
store = case Expr 'EWord -> Maybe (Maybe W256, Expr 'EWord)
inferLogicalIdx Expr 'EWord
origKey of
      Just (Maybe W256
idx, Expr 'EWord
key) -> do
        Expr 'Storage
base <- Maybe W256 -> Expr 'Storage -> Maybe (Expr 'Storage)
setLogicalBase Maybe W256
idx Expr 'Storage
store
        Expr 'EWord -> Maybe (Expr 'EWord)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
key Expr 'Storage
base)
      Maybe (Maybe W256, Expr 'EWord)
_ -> Maybe (Expr 'EWord)
forall a. Maybe a
Nothing

    -- NOTE: we use (Maybe W256) for idx here, because for small slot numbers we want to keep the
    -- Logical Store value a Nothing
    inferLogicalIdx :: Expr EWord -> Maybe (Maybe W256, Expr EWord)
    inferLogicalIdx :: Expr 'EWord -> Maybe (Maybe W256, Expr 'EWord)
inferLogicalIdx = \case
      Lit W256
a | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
256 -> Maybe (Maybe W256, Expr 'EWord)
forall a. Maybe a
Nothing
      Lit W256
a -> (Maybe W256, Expr 'EWord) -> Maybe (Maybe W256, Expr 'EWord)
forall a. a -> Maybe a
Just (Maybe W256
forall a. Maybe a
Nothing, W256 -> Expr 'EWord
Lit W256
a)
      (MappingSlot ByteString
idx Expr 'EWord
key) | ByteString -> Int
BS.length ByteString
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
64 -> (Maybe W256, Expr 'EWord) -> Maybe (Maybe W256, Expr 'EWord)
forall a. a -> Maybe a
Just (W256 -> Maybe W256
forall a. a -> Maybe a
Just (W256 -> Maybe W256) -> W256 -> Maybe W256
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
idxToWord ByteString
idx, Expr 'EWord
key)
      (ArraySlotWithOffset ByteString
idx Expr 'EWord
offset) | ByteString -> Int
BS.length ByteString
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
32 -> (Maybe W256, Expr 'EWord) -> Maybe (Maybe W256, Expr 'EWord)
forall a. a -> Maybe a
Just (W256 -> Maybe W256
forall a. a -> Maybe a
Just (W256 -> Maybe W256) -> W256 -> Maybe W256
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
idxToWord64 ByteString
idx, Expr 'EWord
offset)
      (ArraySlotZero ByteString
idx) | ByteString -> Int
BS.length ByteString
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
32 -> (Maybe W256, Expr 'EWord) -> Maybe (Maybe W256, Expr 'EWord)
forall a. a -> Maybe a
Just (W256 -> Maybe W256
forall a. a -> Maybe a
Just (W256 -> Maybe W256) -> W256 -> Maybe W256
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
idxToWord64 ByteString
idx, W256 -> Expr 'EWord
Lit W256
0)
      Expr 'EWord
_ -> Maybe (Maybe W256, Expr 'EWord)
forall a. Maybe a
Nothing

    idxToWord :: ByteString -> W256
    idxToWord :: ByteString -> W256
idxToWord = Word256 -> W256
W256 (Word256 -> W256) -> (ByteString -> Word256) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Word256
word256 (ByteString -> Word256)
-> (ByteString -> ByteString) -> ByteString -> Word256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> ByteString -> ByteString
BS.takeEnd Int
32)
    -- Arrays take the whole `id` and keccak it. It's supposed to be 64B
    idxToWord64 :: ByteString -> W256
    idxToWord64 :: ByteString -> W256
idxToWord64 = Word256 -> W256
W256 (Word256 -> W256) -> (ByteString -> Word256) -> ByteString -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Word256
word256 (ByteString -> Word256)
-> (ByteString -> ByteString) -> ByteString -> Word256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> ByteString -> ByteString
BS.takeEnd Int
64)

    -- Updates the logical base store of the given expression if it is safe to do so
    setLogicalBase :: Maybe W256 -> Expr Storage -> Maybe (Expr Storage)

    -- abstract bases get their logical idx set to the new value
    setLogicalBase :: Maybe W256 -> Expr 'Storage -> Maybe (Expr 'Storage)
setLogicalBase Maybe W256
idx (AbstractStore Expr 'EAddr
addr Maybe W256
_) = Expr 'Storage -> Maybe (Expr 'Storage)
forall a. a -> Maybe a
Just (Expr 'Storage -> Maybe (Expr 'Storage))
-> Expr 'Storage -> Maybe (Expr 'Storage)
forall a b. (a -> b) -> a -> b
$ Expr 'EAddr -> Maybe W256 -> Expr 'Storage
AbstractStore Expr 'EAddr
addr Maybe W256
idx
    setLogicalBase Maybe W256
idx (SStore Expr 'EWord
i Expr 'EWord
v Expr 'Storage
s) = do
      Expr 'Storage
b <- Maybe W256 -> Expr 'Storage -> Maybe (Expr 'Storage)
setLogicalBase Maybe W256
idx Expr 'Storage
s
      (Maybe W256
idx2, Expr 'EWord
key2) <- Expr 'EWord -> Maybe (Maybe W256, Expr 'EWord)
inferLogicalIdx Expr 'EWord
i
      if Maybe W256
idx Maybe W256 -> Maybe W256 -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe W256
idx2 then Expr 'Storage -> Maybe (Expr 'Storage)
forall a. a -> Maybe a
Just (Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
key2 Expr 'EWord
v Expr 'Storage
b) else Maybe (Expr 'Storage)
forall a. Maybe a
Nothing

    -- empty concrete base is safe to reuse without any rewriting
    setLogicalBase Maybe W256
_ s :: Expr 'Storage
s@(ConcreteStore Map W256 W256
m) | Map W256 W256 -> Bool
forall k a. Map k a -> Bool
Map.null Map W256 W256
m = Expr 'Storage -> Maybe (Expr 'Storage)
forall a. a -> Maybe a
Just Expr 'Storage
s

    -- if the existing base is concrete but we have writes to only keys < 256
    -- then we can safely rewrite the base to an empty ConcreteStore (safe because we assume keccack(x) > 256)
    setLogicalBase Maybe W256
_ (ConcreteStore Map W256 W256
store) =
      if (W256 -> Bool) -> [W256] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
256) (Map W256 W256 -> [W256]
forall k a. Map k a -> [k]
Map.keys Map W256 W256
store)
      then Expr 'Storage -> Maybe (Expr 'Storage)
forall a. a -> Maybe a
Just (Map W256 W256 -> Expr 'Storage
ConcreteStore Map W256 W256
forall a. Monoid a => a
mempty)
      else Maybe (Expr 'Storage)
forall a. Maybe a
Nothing
    setLogicalBase Maybe W256
_ (GVar GVar 'Storage
_) = [Char] -> Maybe (Expr 'Storage)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Unexpected GVar"


-- | 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 (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go Expr a
e Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
e)
               then Expr a
e
               else Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplify ((forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go (Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
structureArraySlots Expr a
e))
  where
    go :: Expr a -> Expr a

    go :: forall (a :: EType). Expr a -> Expr a
go (Failure [Prop]
a Traces
b EvmError
c) = [Prop] -> Traces -> EvmError -> Expr 'End
Failure ([Prop] -> [Prop]
simplifyProps [Prop]
a) Traces
b EvmError
c
    go (Partial [Prop]
a Traces
b PartialExec
c) = [Prop] -> Traces -> PartialExec -> Expr 'End
Partial ([Prop] -> [Prop]
simplifyProps [Prop]
a) Traces
b PartialExec
c
    go (Success [Prop]
a Traces
b Expr 'Buf
c Map (Expr 'EAddr) (Expr 'EContract)
d) = [Prop]
-> Traces
-> Expr 'Buf
-> Map (Expr 'EAddr) (Expr 'EContract)
-> Expr 'End
Success ([Prop] -> [Prop]
simplifyProps [Prop]
a) Traces
b Expr 'Buf
c Map (Expr 'EAddr) (Expr 'EContract)
d

    -- redundant CopySlice
    go (CopySlice (Lit W256
0x0) (Lit W256
0x0) (Lit W256
0x0) Expr 'Buf
_ Expr 'Buf
dst) = Expr a
Expr 'Buf
dst

    -- simplify storage
    go (Keccak (ConcreteBuf ByteString
bs)) = case ByteString -> Int
BS.length ByteString
bs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
64 of
      Bool
True -> ByteString -> Expr 'EWord -> Expr 'EWord
MappingSlot ByteString
bs (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ ByteString -> W256
word ByteString
bs)
      Bool
False -> Expr 'Buf -> Expr 'EWord
Keccak (ByteString -> Expr 'Buf
ConcreteBuf ByteString
bs)
    go (SLoad Expr 'EWord
slot Expr 'Storage
store) = Expr 'EWord -> Expr 'Storage -> Expr 'EWord
readStorage' Expr 'EWord
slot Expr 'Storage
store
    go (SStore Expr 'EWord
slot Expr 'EWord
val Expr 'Storage
store) = Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
writeStorage Expr 'EWord
slot Expr 'EWord
val Expr 'Storage
store

    -- simplify buffers
    go o :: Expr a
o@(ReadWord (Lit W256
_) Expr 'Buf
_) = Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplifyReads Expr a
o
    go (ReadWord Expr 'EWord
idx Expr 'Buf
buf) = Expr 'EWord -> Expr 'Buf -> Expr 'EWord
readWord Expr 'EWord
idx Expr 'Buf
buf
    go o :: Expr a
o@(ReadByte (Lit W256
_) Expr 'Buf
_) = Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplifyReads Expr a
o
    go (ReadByte Expr 'EWord
idx Expr 'Buf
buf) = Expr 'EWord -> Expr 'Buf -> Expr 'Byte
readByte Expr 'EWord
idx Expr 'Buf
buf
    go (BufLength Expr 'Buf
buf) = Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
buf

    -- 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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
maxBytes
        = (Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'EWord
val (
            ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Expr 'Buf) -> ByteString -> Expr 'Buf
forall a b. (a -> b) -> a -> b
$
              (Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
idx) (Int -> ByteString -> ByteString
padRight (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
idx) ByteString
b))
              ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> (Int -> Word8 -> ByteString
BS.replicate Int
32 Word8
0)
              ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> (Int -> ByteString -> ByteString
BS.drop (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
32) ByteString
b)))
      | Bool
otherwise = Expr a
o
    go (WriteWord Expr 'EWord
a Expr 'EWord
b Expr 'Buf
c) = Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
writeWord Expr 'EWord
a Expr 'EWord
b Expr 'Buf
c

    go (WriteByte Expr 'EWord
a Expr 'Byte
b Expr 'Buf
c) = Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
writeByte Expr 'EWord
a Expr 'Byte
b Expr 'Buf
c

    -- truncate some concrete source buffers to the portion relevant for the CopySlice if we're copying a fully concrete region
    go orig :: Expr a
orig@(CopySlice srcOff :: Expr 'EWord
srcOff@(Lit W256
n) Expr 'EWord
dstOff size :: Expr 'EWord
size@(Lit W256
sz)
        -- It doesn't matter what wOffs we write to, because only the first
        -- n+sz of ConcreteBuf will be used by CopySlice
        (WriteWord Expr 'EWord
wOff Expr 'EWord
value (ConcreteBuf ByteString
buf)) Expr 'Buf
dst)
          -- Let's not deal with overflow
          | W256
nW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
sz W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
n
          , W256
nW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
sz W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
sz
          , W256
nW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
sz W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
maxBytes
            = (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
srcOff Expr 'EWord
dstOff Expr 'EWord
size
                (Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
wOff Expr 'EWord
value (ByteString -> Expr 'Buf
ConcreteBuf ByteString
simplifiedBuf)) Expr 'Buf
dst)
          | Bool
otherwise = Expr a
orig
            where simplifiedBuf :: ByteString
simplifiedBuf = Int -> ByteString -> ByteString
BS.take (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (W256
nW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
sz)) ByteString
buf
    go (CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
f) = Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
f

    go (IndexWord Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord Expr 'EWord
a Expr 'EWord
b

    -- LT
    go (EVM.Types.LT (Lit W256
a) (Lit W256
b))
      | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
b = W256 -> Expr 'EWord
Lit W256
1
      | Bool
otherwise = W256 -> Expr 'EWord
Lit W256
0
    go (EVM.Types.LT Expr 'EWord
_ (Lit W256
0)) = W256 -> Expr 'EWord
Lit W256
0

    -- normalize all comparisons in terms of LT
    go (EVM.Types.GT Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
lt Expr 'EWord
b Expr 'EWord
a
    go (EVM.Types.GEq Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
leq Expr 'EWord
b Expr 'EWord
a
    go (EVM.Types.LEq Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord
EVM.Types.IsZero (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
gt Expr 'EWord
a Expr 'EWord
b)
    go (IsZero Expr 'EWord
a) = Expr 'EWord -> Expr 'EWord
iszero Expr 'EWord
a
    go (SLT a :: Expr 'EWord
a@(Lit W256
_) b :: Expr 'EWord
b@(Lit W256
_)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
slt Expr 'EWord
a Expr 'EWord
b
    go (SGT Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SLT Expr 'EWord
b Expr 'EWord
a

    -- syntactic Eq reduction
    go (Eq (Lit W256
a) (Lit W256
b))
      | W256
a W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
b = W256 -> Expr 'EWord
Lit W256
1
      | Bool
otherwise = W256 -> Expr 'EWord
Lit W256
0
    go (Eq (Lit W256
0) (Sub Expr 'EWord
a Expr 'EWord
b)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
eq Expr 'EWord
a Expr 'EWord
b
    go (Eq Expr 'EWord
a Expr 'EWord
b)
      | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = W256 -> Expr 'EWord
Lit W256
1
      | Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
eq Expr 'EWord
a Expr 'EWord
b

    -- redundant ITE
    go (ITE (Lit W256
x) Expr 'End
a Expr 'End
b)
      | W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr a
Expr 'End
b
      | Bool
otherwise = Expr a
Expr 'End
a

    -- address masking
    go (And (Lit W256
0xffffffffffffffffffffffffffffffffffffffff) a :: Expr 'EWord
a@(WAddr Expr 'EAddr
_)) = Expr a
Expr 'EWord
a

    -- literal addresses
    go (WAddr (LitAddr Addr
a)) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ Addr -> W256
forall target source. From source target => source -> target
into Addr
a

    -- 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
    -- Notice: all Add is normalized, hence the 1st argument is
    --    expected to be Lit, if any. Hence `orig` needs to be the
    --    2nd argument for Add. However, Sub is not normalized
    go (Add (Lit W256
x) (Add (Lit W256
y) Expr 'EWord
orig)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
y)) Expr 'EWord
orig
    -- add + sub NOTE: every combination of Sub is needed (2)
    go (Add (Lit W256
x) (Sub (Lit W256
y) Expr 'EWord
orig)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
y)) Expr 'EWord
orig
    go (Add (Lit W256
x) (Sub Expr 'EWord
orig (Lit W256
y))) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
    -- sub + sub NOTE: every combination of Sub is needed (2x2)
    go (Sub (Lit W256
x) (Sub (Lit W256
y) Expr 'EWord
orig)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
    go (Sub (Lit W256
x) (Sub Expr 'EWord
orig (Lit W256
y))) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
y)) Expr 'EWord
orig
    go (Sub (Sub (Lit W256
x) Expr 'EWord
orig) (Lit W256
y)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
    go (Sub (Sub Expr 'EWord
orig (Lit W256
x)) (Lit W256
y)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub Expr 'EWord
orig (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
y))
    -- sub + add NOTE: every combination of Sub is needed (2)
    go (Sub (Lit W256
x) (Add (Lit W256
y) Expr 'EWord
orig)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig
    go (Sub (Add (Lit W256
x) Expr 'EWord
orig) (Lit W256
y) ) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
xW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
y)) Expr 'EWord
orig

    -- redundant add / sub
    go (Sub (Add Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c)
      | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c = Expr a
Expr 'EWord
b
      | Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c = Expr a
Expr 'EWord
a
      | Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c

    -- Add is associative. We are doing left-growing trees because LIT is
    -- arranged to the left. This way, they accumulate in all combinations.
    -- See `sim-assoc-add` test cases in test.hs
    go (Add Expr 'EWord
a (Add Expr 'EWord
b Expr 'EWord
c)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c
    go (Add (Add (Lit W256
a) Expr 'EWord
x) (Lit W256
b)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add (W256 -> Expr 'EWord
Lit (W256
aW256 -> W256 -> W256
forall a. Num a => a -> a -> a
+W256
b)) Expr 'EWord
x

    -- add / sub identities
    go (Add Expr 'EWord
a Expr 'EWord
b)
      | Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
a
      | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
b
      | Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
a Expr 'EWord
b
    go (Sub Expr 'EWord
a Expr 'EWord
b)
      | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = W256 -> Expr 'EWord
Lit W256
0
      | Expr 'EWord
b Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
a
      | Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub Expr 'EWord
a Expr 'EWord
b

    -- SHL / SHR by 0
    go (SHL Expr 'EWord
a Expr 'EWord
v)
      | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
v
      | Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
shl Expr 'EWord
a Expr 'EWord
v
    go (SHR Expr 'EWord
a Expr 'EWord
v)
      | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Expr a
Expr 'EWord
v
      | Bool
otherwise = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
shr Expr 'EWord
a Expr 'EWord
v

    -- doubled And
    go o :: Expr a
o@(And Expr 'EWord
a (And Expr 'EWord
b Expr 'EWord
c))
      | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
c = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
And Expr 'EWord
a Expr 'EWord
b)
      | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
And Expr 'EWord
b Expr 'EWord
c)
      | Bool
otherwise = Expr a
o

    -- Bitwise AND & OR. These MUST preserve bitwise equivalence
    go o :: Expr a
o@(And (Lit W256
x) Expr 'EWord
_)
      | W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = W256 -> Expr 'EWord
Lit W256
0
      | Bool
otherwise = Expr a
o
    go o :: Expr a
o@(And Expr 'EWord
v (Lit W256
x))
      | W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = W256 -> Expr 'EWord
Lit W256
0
      | W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
maxLit = Expr a
Expr 'EWord
v
      | Bool
otherwise = Expr a
o
    go o :: Expr a
o@(Or (Lit W256
x) Expr 'EWord
b)
      | W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr a
Expr 'EWord
b
      | Bool
otherwise = Expr a
o
    go o :: Expr a
o@(Or Expr 'EWord
a (Lit W256
x))
      | W256
x W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr a
Expr 'EWord
a
      | Bool
otherwise = Expr a
o

    -- 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 W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE Expr 'EWord
a Expr 'End
t Expr 'End
f
      | Bool
otherwise = Expr a
Expr 'End
t
    go (ITE (Or Expr 'EWord
a b :: Expr 'EWord
b@(Lit W256
_)) Expr 'End
t Expr 'End
f) = Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Or Expr 'EWord
b Expr 'EWord
a) Expr 'End
t Expr 'End
f

    -- 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 W256 -> W256 -> Bool
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 W256 -> W256 -> Bool
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 a
Expr 'EWord
a

    -- Some trivial min / max eliminations
    go (Max Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.max Expr 'EWord
a Expr 'EWord
b
    go (Min Expr 'EWord
a Expr 'EWord
b) = case (Expr 'EWord
a, Expr 'EWord
b) of
                     (Lit W256
0, Expr 'EWord
_) -> W256 -> Expr 'EWord
Lit W256
0
                     (Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
EVM.Expr.min Expr 'EWord
a Expr 'EWord
b

    -- Mul is associative. We are doing left-growing trees because LIT is
    -- arranged to the left. This way, they accumulate in all combinations.
    -- See `sim-assoc-add` test cases in test.hs
    go (Mul Expr 'EWord
a (Mul Expr 'EWord
b Expr 'EWord
c)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul Expr 'EWord
a Expr 'EWord
b) Expr 'EWord
c
    go (Mul (Mul (Lit W256
a) Expr 'EWord
x) (Lit W256
b)) = Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul (W256 -> Expr 'EWord
Lit (W256
aW256 -> W256 -> W256
forall a. Num a => a -> a -> a
*W256
b)) Expr 'EWord
x

    -- Some trivial mul eliminations
    go (Mul Expr 'EWord
a Expr 'EWord
b) = case (Expr 'EWord
a, Expr 'EWord
b) of
                     (Lit W256
0, Expr 'EWord
_) -> W256 -> Expr 'EWord
Lit W256
0
                     (Lit W256
1, Expr 'EWord
_) -> Expr a
Expr 'EWord
b
                     (Expr 'EWord, Expr 'EWord)
_ -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
mul Expr 'EWord
a Expr 'EWord
b

    -- Some trivial div eliminations
    go (Div (Lit W256
0) Expr 'EWord
_) = W256 -> Expr 'EWord
Lit W256
0 -- divide 0 by anything (including 0) is zero in EVM
    go (Div Expr 'EWord
_ (Lit W256
0)) = W256 -> Expr 'EWord
Lit W256
0 -- divide anything by 0 is zero in EVM
    go (Div Expr 'EWord
a (Lit W256
1)) = Expr a
Expr 'EWord
a

    -- 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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
b = W256 -> Expr 'EWord
Lit W256
0
      | Bool
otherwise = Expr a
o
    go o :: Expr a
o@(SLT (Sub (Max (Lit W256
a) Expr 'EWord
_) (Lit W256
b)) (Lit W256
c))
      = let sa, sb, sc :: Int256
            sa :: Int256
sa = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
a
            sb :: Int256
sb = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
b
            sc :: Int256
sc = W256 -> Int256
forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
c
        in if Int256
sa Int256 -> Int256 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int256
sb Bool -> Bool -> Bool
&& Int256
sa Int256 -> Int256 -> Int256
forall a. Num a => a -> a -> a
- Int256
sb Int256 -> Int256 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int256
sc
           then W256 -> Expr 'EWord
Lit W256
0
           else Expr a
o

    go Expr a
a = Expr a
a


-- ** Prop Simplification ** -----------------------------------------------------------------------


simplifyProps :: [Prop] -> [Prop]
simplifyProps :: [Prop] -> [Prop]
simplifyProps [Prop]
ps = if Bool
canBeSat then [Prop]
simplified else [Bool -> Prop
PBool Bool
False]
  where
    simplified :: [Prop]
simplified = [Prop] -> [Prop]
remRedundantProps ([Prop] -> [Prop]) -> ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Prop
simplifyProp ([Prop] -> [Prop]) -> ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Prop] -> [Prop]
flattenProps ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop]
ps
    canBeSat :: Bool
canBeSat = [Prop] -> Bool
constFoldProp [Prop]
simplified

-- | Evaluate the provided proposition down to its most concrete result
-- Also simplifies the inner Expr, if it exists
simplifyProp :: Prop -> Prop
simplifyProp :: Prop -> Prop
simplifyProp Prop
prop =
  let new :: Prop
new = (Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
go (Prop -> Prop
simpInnerExpr Prop
prop)
  in if (Prop
new Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Prop
prop) then Prop
prop else Prop -> Prop
simplifyProp Prop
new
  where
    go :: Prop -> Prop

    -- LT/LEq comparisons
    go :: Prop -> Prop
go (PLT  (Var Text
_) (Lit W256
0)) = Bool -> Prop
PBool Bool
False
    go (PLEq (Lit W256
0) (Var Text
_)) = Bool -> Prop
PBool Bool
True
    go (PLT  (Lit W256
val) (Var Text
_)) | W256
val W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
maxLit = Bool -> Prop
PBool Bool
False
    go (PLEq (Var Text
_) (Lit W256
val)) | W256
val W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
maxLit = Bool -> Prop
PBool Bool
True
    go (PLT (Lit W256
l) (Lit W256
r)) = Bool -> Prop
PBool (W256
l W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
r)
    go (PLEq (Lit W256
l) (Lit W256
r)) = Bool -> Prop
PBool (W256
l W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
r)
    go (PLEq Expr 'EWord
a (Max Expr 'EWord
b Expr 'EWord
_)) | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = Bool -> Prop
PBool Bool
True
    go (PLEq Expr 'EWord
a (Max Expr 'EWord
_ Expr 'EWord
b)) | Expr 'EWord
a Expr 'EWord -> Expr 'EWord -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'EWord
b = Bool -> Prop
PBool Bool
True
    go (PLT (Max (Lit W256
a) Expr 'EWord
b) (Lit W256
c)) | W256
a W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
c = Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
b (W256 -> Expr 'EWord
Lit W256
c)
    go (PLT (Lit W256
0) (Eq Expr 'EWord
a Expr 'EWord
b)) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b

    -- negations
    go (PNeg (PBool Bool
b)) = Bool -> Prop
PBool (Bool -> Bool
Prelude.not Bool
b)
    go (PNeg (PNeg Prop
a)) = Prop
a

    -- solc specific stuff
    go (PEq (IsZero (Eq Expr 'EWord
a Expr 'EWord
b)) (Lit W256
0)) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b
    go (PEq (IsZero (IsZero (Eq Expr 'EWord
a Expr 'EWord
b))) (Lit W256
0)) = Prop -> Prop
PNeg (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b)

    -- iszero(a) -> (a == 0)
    -- iszero(iszero(a))) -> ~(a == 0) -> a > 0
    -- iszero(iszero(a)) == 0 -> ~~(a == 0) -> a == 0
    -- ~(iszero(iszero(a)) == 0) -> ~~~(a == 0) -> ~(a == 0) -> a > 0
    go (PNeg (PEq (IsZero (IsZero Expr 'EWord
a)) (Lit W256
0))) = Expr 'EWord -> Expr 'EWord -> Prop
PGT Expr 'EWord
a (W256 -> Expr 'EWord
Lit W256
0)

    -- iszero(a) -> (a == 0)
    -- iszero(a) == 0 -> ~(a == 0)
    -- ~(iszero(a) == 0) -> ~~(a == 0) -> a == 0
    go (PNeg (PEq (IsZero Expr 'EWord
a) (Lit W256
0))) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a (W256 -> Expr 'EWord
Lit W256
0)

    -- a < b == 0 -> ~(a < b)
    -- ~(a < b == 0) -> ~~(a < b) -> a < b
    go (PNeg (PEq (LT Expr 'EWord
a Expr 'EWord
b) (Lit W256
0x0))) = Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
a Expr 'EWord
b

    -- And/Or
    go (PAnd (PBool Bool
l) (PBool Bool
r)) = Bool -> Prop
PBool (Bool
l Bool -> Bool -> Bool
&& Bool
r)
    go (PAnd (PBool Bool
False) Prop
_) = Bool -> Prop
PBool Bool
False
    go (PAnd Prop
_ (PBool Bool
False)) = Bool -> Prop
PBool Bool
False
    go (POr (PBool Bool
True) Prop
_) = Bool -> Prop
PBool Bool
True
    go (POr Prop
_ (PBool Bool
True)) = Bool -> Prop
PBool Bool
True
    go (POr (PBool Bool
l) (PBool Bool
r)) = Bool -> Prop
PBool (Bool
l Bool -> Bool -> Bool
|| Bool
r)

    -- Imply
    go (PImpl Prop
_ (PBool Bool
True)) = Bool -> Prop
PBool Bool
True
    go (PImpl (PBool Bool
True) Prop
b) = Prop
b
    go (PImpl (PBool Bool
False) Prop
_) = Bool -> Prop
PBool Bool
True

    -- Eq
    go (PEq (Eq Expr 'EWord
a Expr 'EWord
b) (Lit W256
0)) = Prop -> Prop
PNeg (Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b)
    go (PEq (Eq Expr 'EWord
a Expr 'EWord
b) (Lit W256
1)) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b
    go (PEq (Sub Expr 'EWord
a Expr 'EWord
b) (Lit W256
0)) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
a Expr 'EWord
b
    go (PEq (Lit W256
l) (Lit W256
r)) = Bool -> Prop
PBool (W256
l W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
r)
    go o :: Prop
o@(PEq Expr a
l Expr a
r)
      | Expr a
l Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
r = Bool -> Prop
PBool Bool
True
      | Bool
otherwise = Prop
o
    go Prop
p = Prop
p


    -- Applies `simplify` to the inner part of a Prop, e.g.
    -- (PEq (Add (Lit 1) (Lit 2)) (Var "a")) becomes
    -- (PEq (Lit 3) (Var "a")
    simpInnerExpr :: Prop -> Prop
    -- rewrite everything as LEq or LT
    simpInnerExpr :: Prop -> Prop
simpInnerExpr (PGEq Expr 'EWord
a Expr 'EWord
b) = Prop -> Prop
simpInnerExpr (Expr 'EWord -> Expr 'EWord -> Prop
PLEq Expr 'EWord
b Expr 'EWord
a)
    simpInnerExpr (PGT Expr 'EWord
a Expr 'EWord
b) = Prop -> Prop
simpInnerExpr (Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
b Expr 'EWord
a)
    -- simplifies the inner expression
    simpInnerExpr (PEq Expr a
a Expr a
b) = Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplify Expr a
a) (Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplify Expr a
b)
    simpInnerExpr (PLT Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Prop
PLT (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
a) (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
b)
    simpInnerExpr (PLEq Expr 'EWord
a Expr 'EWord
b) = Expr 'EWord -> Expr 'EWord -> Prop
PLEq (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
a) (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify Expr 'EWord
b)
    simpInnerExpr (PNeg Prop
a) = Prop -> Prop
PNeg (Prop -> Prop
simpInnerExpr Prop
a)
    simpInnerExpr (PAnd Prop
a Prop
b) = Prop -> Prop -> Prop
PAnd (Prop -> Prop
simpInnerExpr Prop
a) (Prop -> Prop
simpInnerExpr Prop
b)
    simpInnerExpr (POr Prop
a Prop
b) = Prop -> Prop -> Prop
POr (Prop -> Prop
simpInnerExpr Prop
a) (Prop -> Prop
simpInnerExpr Prop
b)
    simpInnerExpr (PImpl Prop
a Prop
b) = Prop -> Prop -> Prop
PImpl (Prop -> Prop
simpInnerExpr Prop
a) (Prop -> Prop
simpInnerExpr Prop
b)
    simpInnerExpr orig :: Prop
orig@(PBool Bool
_) = Prop
orig

-- Makes [PAnd a b] into [a,b]
flattenProps :: [Prop] -> [Prop]
flattenProps :: [Prop] -> [Prop]
flattenProps [] = []
flattenProps (Prop
a:[Prop]
ax) = case Prop
a of
  PAnd Prop
x1 Prop
x2 -> Prop
x1Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:Prop
x2Prop -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop] -> [Prop]
flattenProps [Prop]
ax
  Prop
x -> Prop
xProp -> [Prop] -> [Prop]
forall a. a -> [a] -> [a]
:[Prop] -> [Prop]
flattenProps [Prop]
ax

-- removes redundant (constant True/False) props
remRedundantProps :: [Prop] -> [Prop]
remRedundantProps :: [Prop] -> [Prop]
remRedundantProps [Prop]
p = [Prop] -> [Prop]
forall a. Ord a => [a] -> [a]
nubOrd ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop] -> [Prop]
collapseFalse ([Prop] -> [Prop]) -> ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Prop -> Bool) -> [Prop] -> [Prop]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Prop
x -> Prop
x Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Prop
PBool Bool
True) ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop]
p
  where
    collapseFalse :: [Prop] -> [Prop]
collapseFalse [Prop]
ps = if Maybe Prop -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Prop -> Bool) -> Maybe Prop -> Bool
forall a b. (a -> b) -> a -> b
$ (Prop -> Bool) -> [Prop] -> Maybe Prop
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Prop
PBool Bool
False) [Prop]
ps then [Bool -> Prop
PBool Bool
False] else [Prop]
ps


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


litAddr :: Addr -> Expr EWord
litAddr :: Addr -> Expr 'EWord
litAddr = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Addr -> W256) -> Addr -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Addr -> W256
forall target source. From source target => source -> target
into

exprToAddr :: Expr EWord -> Maybe Addr
exprToAddr :: Expr 'EWord -> Maybe Addr
exprToAddr (Lit W256
x) = Addr -> Maybe Addr
forall a. a -> Maybe a
Just (W256 -> Addr
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
x)
exprToAddr Expr 'EWord
_ = Maybe Addr
forall a. Maybe a
Nothing

-- TODO: make this smarter, probably we will need to use the solver here?
wordToAddr :: Expr EWord -> Maybe (Expr EAddr)
wordToAddr :: Expr 'EWord -> Maybe (Expr 'EAddr)
wordToAddr = Expr 'EWord -> Maybe (Expr 'EAddr)
go (Expr 'EWord -> Maybe (Expr 'EAddr))
-> (Expr 'EWord -> Expr 'EWord)
-> Expr 'EWord
-> Maybe (Expr 'EAddr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
simplify
  where
    go :: Expr EWord -> Maybe (Expr EAddr)
    go :: Expr 'EWord -> Maybe (Expr 'EAddr)
go = \case
      WAddr Expr 'EAddr
a -> Expr 'EAddr -> Maybe (Expr 'EAddr)
forall a. a -> Maybe a
Just Expr 'EAddr
a
      Lit W256
a -> Expr 'EAddr -> Maybe (Expr 'EAddr)
forall a. a -> Maybe a
Just (Expr 'EAddr -> Maybe (Expr 'EAddr))
-> Expr 'EAddr -> Maybe (Expr 'EAddr)
forall a b. (a -> b) -> a -> b
$ Addr -> Expr 'EAddr
LitAddr (W256 -> Addr
truncateToAddr W256
a)
      Expr 'EWord
_ -> Maybe (Expr 'EAddr)
forall a. Maybe a
Nothing

litCode :: BS.ByteString -> [Expr Byte]
litCode :: ByteString -> [Expr 'Byte]
litCode ByteString
bs = (Word8 -> Expr 'Byte) -> [Word8] -> [Expr 'Byte]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word8 -> Expr 'Byte
LitByte (ByteString -> [Word8]
BS.unpack ByteString
bs)

to512 :: W256 -> Word512
to512 :: W256 -> Word512
to512 = W256 -> Word512
forall a b. (Integral a, Num b) => a -> b
fromIntegral


-- ** 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 (WAddr (LitAddr Addr
_)) = Bool
True
isLitWord Expr 'EWord
_ = Bool
False

isSuccess :: Expr End -> Bool
isSuccess :: Expr 'End -> Bool
isSuccess = \case
  Success {} -> Bool
True
  Expr 'End
_ -> Bool
False

isFailure :: Expr End -> Bool
isFailure :: Expr 'End -> Bool
isFailure = \case
  Failure {} -> Bool
True
  Expr 'End
_ -> Bool
False

isPartial :: Expr End -> Bool
isPartial :: Expr 'End -> Bool
isPartial = \case
  Partial {} -> Bool
True
  Expr 'End
_ -> Bool
False

-- | Returns the byte at idx from the given word.
indexWord :: Expr EWord -> Expr EWord -> Expr Byte
-- Simplify masked reads:
--
--
--                reads across the mask boundary
--                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 underlying word
  -- we need this case to avoid overflow
  | W256
mask W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
fullWordMask = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'EWord
w
  -- if the index is a read from the masked region then read from the underlying word
  | W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
31
  , W256 -> Bool
forall {a}. (Bits a, Num a) => a -> Bool
isPower2 (W256
mask W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1)
  , W256 -> Bool
forall {b}. FiniteBits b => b -> Bool
isByteAligned W256
mask
  , W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
unmaskedBytes
    = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
indexWord (W256 -> Expr 'EWord
Lit W256
idx) Expr 'EWord
w
  -- if the read is outside of the masked region return 0
  | W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
31
  , W256 -> Bool
forall {a}. (Bits a, Num a) => a -> Bool
isPower2 (W256
mask W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
1)
  , W256 -> Bool
forall {b}. FiniteBits b => b -> Bool
isByteAligned W256
mask
  , W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
unmaskedBytes
    = Word8 -> Expr 'Byte
LitByte Word8
0
  -- if the mask is not a power of 2, or it does not align with a byte boundary return an abstract expression
  | W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
31 = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
IndexWord Expr 'EWord
i Expr 'EWord
e
  -- 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 a -> a -> a
forall a. Bits a => a -> a -> a
.&. (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0
    fullWordMask :: W256
fullWordMask = (W256
2 W256 -> W256 -> W256
forall a b. (Num a, Integral b) => a -> b -> a
^ (W256
256 :: W256)) W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1
    unmaskedBytes :: W256
unmaskedBytes = Int -> W256
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> W256) -> Int -> W256
forall a b. (a -> b) -> a -> b
$ (W256 -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros W256
mask) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`Prelude.div` Int
8
    isByteAligned :: b -> Bool
isByteAligned b
m = (b -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros b
m) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`Prelude.mod` Int
8 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
indexWord (Lit W256
idx) (Lit W256
w)
  | W256
idx W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
31 = Word8 -> Expr 'Byte
LitByte (Word8 -> Expr 'Byte) -> (W256 -> Word8) -> W256 -> Expr 'Byte
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (W256 -> Expr 'Byte) -> W256 -> Expr 'Byte
forall a b. (a -> b) -> a -> b
$ W256 -> Int -> W256
forall a. Bits a => a -> Int -> a
shiftR W256
w (Int
248 Int -> Int -> Int
forall a. Num a => a -> a -> a
- W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8)
  | Bool
otherwise = Word8 -> Expr 'Byte
LitByte Word8
0
indexWord (Lit W256
idx) (JoinBytes Expr 'Byte
zero        Expr 'Byte
one        Expr 'Byte
two       Expr 'Byte
three
                               Expr 'Byte
four        Expr 'Byte
five       Expr 'Byte
six       Expr 'Byte
seven
                               Expr 'Byte
eight       Expr 'Byte
nine       Expr 'Byte
ten       Expr 'Byte
eleven
                               Expr 'Byte
twelve      Expr 'Byte
thirteen   Expr 'Byte
fourteen  Expr 'Byte
fifteen
                               Expr 'Byte
sixteen     Expr 'Byte
seventeen  Expr 'Byte
eighteen  Expr 'Byte
nineteen
                               Expr 'Byte
twenty      Expr 'Byte
twentyone  Expr 'Byte
twentytwo Expr 'Byte
twentythree
                               Expr 'Byte
twentyfour  Expr 'Byte
twentyfive Expr 'Byte
twentysix Expr 'Byte
twentyseven
                               Expr 'Byte
twentyeight Expr 'Byte
twentynine Expr 'Byte
thirty    Expr 'Byte
thirtyone)
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
0 = Expr 'Byte
zero
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
1 = Expr 'Byte
one
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
2 = Expr 'Byte
two
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
3 = Expr 'Byte
three
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
4 = Expr 'Byte
four
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
5 = Expr 'Byte
five
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
6 = Expr 'Byte
six
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
7 = Expr 'Byte
seven
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
8 = Expr 'Byte
eight
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
9 = Expr 'Byte
nine
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
10 = Expr 'Byte
ten
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
11 = Expr 'Byte
eleven
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
12 = Expr 'Byte
twelve
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
13 = Expr 'Byte
thirteen
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
14 = Expr 'Byte
fourteen
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
15 = Expr 'Byte
fifteen
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
16 = Expr 'Byte
sixteen
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
17 = Expr 'Byte
seventeen
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
18 = Expr 'Byte
eighteen
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
19 = Expr 'Byte
nineteen
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
20 = Expr 'Byte
twenty
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
21 = Expr 'Byte
twentyone
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
22 = Expr 'Byte
twentytwo
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
23 = Expr 'Byte
twentythree
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
24 = Expr 'Byte
twentyfour
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
25 = Expr 'Byte
twentyfive
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
26 = Expr 'Byte
twentysix
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
27 = Expr 'Byte
twentyseven
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
28 = Expr 'Byte
twentyeight
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
29 = Expr 'Byte
twentynine
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
30 = Expr 'Byte
thirty
  | W256
idx W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
31 = Expr 'Byte
thirtyone
  | Bool
otherwise = Word8 -> Expr 'Byte
LitByte Word8
0
indexWord Expr 'EWord
idx Expr 'EWord
w = Expr 'EWord -> Expr 'EWord -> Expr 'Byte
IndexWord Expr 'EWord
idx Expr 'EWord
w


padByte :: Expr Byte -> Expr EWord
padByte :: Expr 'Byte -> Expr 'EWord
padByte (LitByte Word8
b) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord)
-> ([Word8] -> W256) -> [Word8] -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> W256
bytesToW256 ([Word8] -> Expr 'EWord) -> [Word8] -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ [Word8
b]
padByte Expr 'Byte
b = [Expr 'Byte] -> Expr 'EWord
joinBytes [Expr 'Byte
b]

-- | 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 (ByteString -> W256) -> ([Word8] -> ByteString) -> [Word8] -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack

padBytesLeft :: Int -> [Expr Byte] -> [Expr Byte]
padBytesLeft :: Int -> [Expr 'Byte] -> [Expr 'Byte]
padBytesLeft Int
n [Expr 'Byte]
bs
  | [Expr 'Byte] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'Byte]
bs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = Int -> [Expr 'Byte] -> [Expr 'Byte]
forall a. Int -> [a] -> [a]
Prelude.take Int
n [Expr 'Byte]
bs
  | [Expr 'Byte] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr 'Byte]
bs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n = [Expr 'Byte]
bs
  | Bool
otherwise = Int -> [Expr 'Byte] -> [Expr 'Byte]
padBytesLeft Int
n (Word8 -> Expr 'Byte
LitByte Word8
0 Expr 'Byte -> [Expr 'Byte] -> [Expr 'Byte]
forall a. a -> [a] -> [a]
: [Expr 'Byte]
bs)

joinBytes :: [Expr Byte] -> Expr EWord
joinBytes :: [Expr 'Byte] -> Expr 'EWord
joinBytes [Expr 'Byte]
bs
  | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Prelude.and ([Bool] -> Bool)
-> ([Expr 'Byte] -> [Bool]) -> [Expr 'Byte] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Bool) -> [Expr 'Byte] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Byte -> Bool
isLitByte) ([Expr 'Byte] -> Bool) -> [Expr 'Byte] -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bs = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord)
-> ([Expr 'Byte] -> W256) -> [Expr 'Byte] -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> W256
bytesToW256 ([Word8] -> W256)
-> ([Expr 'Byte] -> [Word8]) -> [Expr 'Byte] -> W256
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr 'Byte -> Maybe Word8) -> [Expr 'Byte] -> [Word8]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Expr 'Byte -> Maybe Word8
maybeLitByte) ([Expr 'Byte] -> Expr 'EWord) -> [Expr 'Byte] -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte]
bs
  | Bool
otherwise = let
      bytes :: [Expr 'Byte]
bytes = Int -> [Expr 'Byte] -> [Expr 'Byte]
padBytesLeft Int
32 [Expr 'Byte]
bs
    in Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'EWord
JoinBytes
      ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)  ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)  ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)  ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
      ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
4)  ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
5)  ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
6)  ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
7)
      ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
8)  ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
9)  ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
10) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
11)
      ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
12) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
13) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
14) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
15)
      ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
16) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
17) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
18) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
19)
      ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
20) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
21) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
22) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
23)
      ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
24) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
25) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
26) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
27)
      ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
28) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
29) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
30) ([Expr 'Byte]
bytes [Expr 'Byte] -> Int -> Expr 'Byte
forall a. HasCallStack => [a] -> Int -> a
!! Int
31)

eqByte :: Expr Byte -> Expr Byte -> Expr EWord
eqByte :: Expr 'Byte -> Expr 'Byte -> Expr 'EWord
eqByte (LitByte Word8
x) (LitByte Word8
y) = W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ if Word8
x Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
y then W256
1 else W256
0
eqByte Expr 'Byte
x Expr 'Byte
y = Expr 'Byte -> Expr 'Byte -> Expr 'EWord
EqByte Expr 'Byte
x Expr 'Byte
y

min :: Expr EWord -> Expr EWord -> Expr EWord
min :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
min Expr 'EWord
x Expr 'EWord
y = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Min W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.min Expr 'EWord
x Expr 'EWord
y

max :: Expr EWord -> Expr EWord -> Expr EWord
max :: Expr 'EWord -> Expr 'EWord -> Expr 'EWord
max (Lit W256
0) Expr 'EWord
y = Expr 'EWord
y
max Expr 'EWord
x (Lit W256
0) = Expr 'EWord
x
max Expr 'EWord
x Expr 'EWord
y = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> (W256 -> W256 -> W256)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
normArgs Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Max W256 -> W256 -> W256
forall a. Ord a => a -> a -> a
Prelude.max Expr 'EWord
x Expr 'EWord
y

numBranches :: Expr End -> Int
numBranches :: Expr 'End -> Int
numBranches (ITE Expr 'EWord
_ Expr 'End
t Expr 'End
f) = Expr 'End -> Int
numBranches Expr 'End
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Expr 'End -> Int
numBranches Expr 'End
f
numBranches Expr 'End
_ = Int
1

allLit :: [Expr Byte] -> Bool
allLit :: [Expr 'Byte] -> Bool
allLit = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Data.List.and ([Bool] -> Bool)
-> ([Expr 'Byte] -> [Bool]) -> [Expr 'Byte] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'Byte -> Bool) -> [Expr 'Byte] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Expr 'Byte -> Bool
isLitByte)

-- | 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 (Any -> Bool) -> (Expr b -> Any) -> Expr b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: EType). Expr a -> Any) -> Any -> Expr b -> Any
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> Any
forall (a :: EType). Expr a -> Any
go (Bool -> Any
Any Bool
False)
  where
    go :: Expr a -> Any
    go :: forall (a :: EType). Expr a -> Any
go Expr a
node | Expr a -> Bool
forall (a :: EType). Expr a -> Bool
p Expr a
node  = Bool -> Any
Any Bool
True
    go Expr a
_ = Bool -> Any
Any Bool
False

inRange :: Int -> Expr EWord -> Prop
inRange :: Int -> Expr 'EWord -> Prop
inRange Int
sz Expr 'EWord
e = Prop -> Prop -> Prop
PAnd (Expr 'EWord -> Expr 'EWord -> Prop
PGEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit W256
0)) (Expr 'EWord -> Expr 'EWord -> Prop
PLEq Expr 'EWord
e (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
2 W256 -> Int -> W256
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1))


-- | images of keccak(bytes32(x)) where 0 <= x < 256
preImages :: [(W256, Word8)]
preImages :: [(W256, Word8)]
preImages = [(ByteString -> W256
keccak' (W256 -> ByteString
word256Bytes (W256 -> ByteString) -> (Word8 -> W256) -> Word8 -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> W256
forall target source. From source target => source -> target
into (Word8 -> ByteString) -> Word8 -> ByteString
forall a b. (a -> b) -> a -> b
$ Word8
i), Word8
i) | Word8
i <- [Word8
0..Word8
255]]

data ConstState = ConstState
  { ConstState -> Map (Expr 'EWord) W256
values :: Map.Map (Expr EWord) W256
  , ConstState -> Bool
canBeSat :: Bool
  }
  deriving (Int -> ConstState -> ShowS
[ConstState] -> ShowS
ConstState -> [Char]
(Int -> ConstState -> ShowS)
-> (ConstState -> [Char])
-> ([ConstState] -> ShowS)
-> Show ConstState
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConstState -> ShowS
showsPrec :: Int -> ConstState -> ShowS
$cshow :: ConstState -> [Char]
show :: ConstState -> [Char]
$cshowList :: [ConstState] -> ShowS
showList :: [ConstState] -> ShowS
Show)

-- | Folds constants
constFoldProp :: [Prop] -> Bool
constFoldProp :: [Prop] -> Bool
constFoldProp [Prop]
ps = [Prop] -> ConstState -> Bool
forall {t :: * -> *}. Traversable t => t Prop -> ConstState -> Bool
oneRun [Prop]
ps (Map (Expr 'EWord) W256 -> Bool -> ConstState
ConstState Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty Bool
True)
  where
    oneRun :: t Prop -> ConstState -> Bool
oneRun t Prop
ps2 ConstState
startState = (State ConstState (t ()) -> ConstState -> ConstState
forall s a. State s a -> s -> s
execState ((Prop -> StateT ConstState Identity ())
-> t Prop -> State ConstState (t ())
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
mapM (Prop -> StateT ConstState Identity ()
go (Prop -> StateT ConstState Identity ())
-> (Prop -> Prop) -> Prop -> StateT ConstState Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop -> Prop
simplifyProp) t Prop
ps2) ConstState
startState).canBeSat
    go :: Prop -> State ConstState ()
    go :: Prop -> StateT ConstState Identity ()
go Prop
x = case Prop
x of
        -- PEq
        PEq (Lit W256
l) Expr a
a -> do
          ConstState
s <- StateT ConstState Identity ConstState
forall s (m :: * -> *). MonadState s m => m s
get
          case Expr a -> Map (Expr a) W256 -> Maybe W256
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr a
a ConstState
s.values of
            Just W256
l2 -> case W256
lW256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
==W256
l2 of
                Bool
True -> () -> StateT ConstState Identity ()
forall a. a -> StateT ConstState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                Bool
False -> ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ConstState {$sel:canBeSat:ConstState :: Bool
canBeSat=Bool
False, $sel:values:ConstState :: Map (Expr 'EWord) W256
values=Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty}
            Maybe W256
Nothing -> do
              let vs' :: Map (Expr a) W256
vs' = Expr a -> W256 -> Map (Expr a) W256 -> Map (Expr a) W256
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr a
a W256
l ConstState
s.values
              ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ConstState -> StateT ConstState Identity ())
-> ConstState -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ ConstState
s{$sel:values:ConstState :: Map (Expr 'EWord) W256
values=Map (Expr a) W256
Map (Expr 'EWord) W256
vs'}
        PEq Expr a
a b :: Expr a
b@(Lit W256
_) -> Prop -> StateT ConstState Identity ()
go (Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr a
b Expr a
a)
        -- PNeg
        PNeg (PEq (Lit W256
l) Expr a
a) -> do
          ConstState
s <- StateT ConstState Identity ConstState
forall s (m :: * -> *). MonadState s m => m s
get
          case Expr a -> Map (Expr a) W256 -> Maybe W256
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr a
a ConstState
s.values of
            Just W256
l2 -> case W256
lW256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
==W256
l2 of
                Bool
True -> ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ConstState {$sel:canBeSat:ConstState :: Bool
canBeSat=Bool
False, $sel:values:ConstState :: Map (Expr 'EWord) W256
values=Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty}
                Bool
False -> () -> StateT ConstState Identity ()
forall a. a -> StateT ConstState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Maybe W256
Nothing -> () -> StateT ConstState Identity ()
forall a. a -> StateT ConstState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure()
        PNeg (PEq Expr a
a b :: Expr a
b@(Lit W256
_)) -> Prop -> StateT ConstState Identity ()
go (Prop -> StateT ConstState Identity ())
-> Prop -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ Prop -> Prop
PNeg (Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr a
b Expr a
a)
        -- Others
        PAnd Prop
a Prop
b -> do
          Prop -> StateT ConstState Identity ()
go Prop
a
          Prop -> StateT ConstState Identity ()
go Prop
b
        POr Prop
a Prop
b -> do
          ConstState
s <- StateT ConstState Identity ConstState
forall s (m :: * -> *). MonadState s m => m s
get
          let
            v1 :: Bool
v1 = [Prop] -> ConstState -> Bool
forall {t :: * -> *}. Traversable t => t Prop -> ConstState -> Bool
oneRun [Prop
a] ConstState
s
            v2 :: Bool
v2 = [Prop] -> ConstState -> Bool
forall {t :: * -> *}. Traversable t => t Prop -> ConstState -> Bool
oneRun [Prop
b] ConstState
s
          Bool
-> StateT ConstState Identity () -> StateT ConstState Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
Prelude.not Bool
v1) (StateT ConstState Identity () -> StateT ConstState Identity ())
-> StateT ConstState Identity () -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ Prop -> StateT ConstState Identity ()
go Prop
b
          Bool
-> StateT ConstState Identity () -> StateT ConstState Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
Prelude.not Bool
v2) (StateT ConstState Identity () -> StateT ConstState Identity ())
-> StateT ConstState Identity () -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ Prop -> StateT ConstState Identity ()
go Prop
a
          ConstState
s2 <- StateT ConstState Identity ConstState
forall s (m :: * -> *). MonadState s m => m s
get
          ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ConstState -> StateT ConstState Identity ())
-> ConstState -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ ConstState
s{$sel:canBeSat:ConstState :: Bool
canBeSat=(ConstState
s2.canBeSat Bool -> Bool -> Bool
&& (Bool
v1 Bool -> Bool -> Bool
|| Bool
v2))}
        PBool Bool
False -> ConstState -> StateT ConstState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ConstState -> StateT ConstState Identity ())
-> ConstState -> StateT ConstState Identity ()
forall a b. (a -> b) -> a -> b
$ ConstState {$sel:canBeSat:ConstState :: Bool
canBeSat=Bool
False, $sel:values:ConstState :: Map (Expr 'EWord) W256
values=Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty}
        Prop
_ -> () -> StateT ConstState Identity ()
forall a. a -> StateT ConstState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- Concretize & simplify Keccak expressions until fixed-point.
concKeccakSimpExpr :: Expr a -> Expr a
concKeccakSimpExpr :: forall (a :: EType). Expr a -> Expr a
concKeccakSimpExpr Expr a
orig = (Expr a -> Expr a) -> Expr a -> Expr a
forall a. Eq a => (a -> a) -> a -> a
untilFixpoint (((forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
concKeccakOnePass) (Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
simplify) Expr a
orig

-- Only concretize Keccak in Props
-- Needed because if it also simplified, we may not find some simplification errors, as
-- simplification would always be ON
concKeccakProps :: [Prop] -> [Prop]
concKeccakProps :: [Prop] -> [Prop]
concKeccakProps [Prop]
orig = ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a. Eq a => (a -> a) -> a -> a
untilFixpoint ((Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
concKeccakOnePass)) [Prop]
orig

-- Simplifies in case the input to the Keccak is of specific array/map format and
--            can be simplified into a concrete value
-- Turns (Keccak ConcreteBuf) into a Lit
concKeccakOnePass :: Expr a -> Expr a
concKeccakOnePass :: forall (a :: EType). Expr a -> Expr a
concKeccakOnePass (Keccak (ConcreteBuf ByteString
bs)) = W256 -> Expr 'EWord
Lit (ByteString -> W256
keccak' ByteString
bs)
concKeccakOnePass orig :: Expr a
orig@(Keccak (CopySlice (Lit W256
0) (Lit W256
0) (Lit W256
64) orig2 :: Expr 'Buf
orig2@(WriteWord (Lit W256
0) Expr 'EWord
_ (ConcreteBuf ByteString
bs)) (ConcreteBuf ByteString
""))) =
  case (ByteString -> Int
BS.length ByteString
bs, (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
copySlice (W256 -> Expr 'EWord
Lit W256
0) (W256 -> Expr 'EWord
Lit W256
0) (W256 -> Expr 'EWord
Lit W256
64) (Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
simplify Expr 'Buf
orig2) (ByteString -> Expr 'Buf
ConcreteBuf ByteString
""))) of
    (Int
64, ConcreteBuf ByteString
a) -> W256 -> Expr 'EWord
Lit (ByteString -> W256
keccak' ByteString
a)
    (Int, Expr 'Buf)
_ -> Expr a
orig
concKeccakOnePass Expr a
x = Expr a
x