{-# LANGUAGE ScopedTypeVariables #-}

{- |
    Module: EVM.Fuzz
    Description: Concrete Fuzzer of Exprs
-}

module EVM.Fuzz where

import Prelude hiding (LT, GT, lookup)
import Control.Monad.State
import Data.Maybe (fromMaybe)
import Data.Map.Strict as Map (fromList, Map, (!), (!?), insert)
import EVM.Expr qualified as Expr
import EVM.Expr (bytesToW256)
import Data.Set as Set (insert, Set, empty, toList, fromList)
import EVM.Traversals
import Data.ByteString qualified as BS
import Data.Word (Word8)
import Test.QuickCheck.Gen

import EVM.Types (Prop(..), W256, Expr(..), EType(..), internalError, keccak')
import EVM.SMT qualified as SMT (BufModel(..), SMTCex(..))
import Test.QuickCheck (Arbitrary(arbitrary))
import Test.QuickCheck.Random (mkQCGen)

-- TODO: Extract Var X = Lit Z, and set it
tryCexFuzz :: [Prop] -> Integer -> (Maybe (SMT.SMTCex))
tryCexFuzz :: [Prop] -> Integer -> Maybe SMTCex
tryCexFuzz [Prop]
prePs Integer
tries = Gen (Maybe SMTCex) -> QCGen -> Int -> Maybe SMTCex
forall a. Gen a -> QCGen -> Int -> a
unGen (Integer -> Gen (Maybe SMTCex)
testVals Integer
tries) (Int -> QCGen
mkQCGen Int
0) Int
1337
  where
    ps :: [Prop]
ps = [Prop] -> [Prop]
Expr.simplifyProps ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop] -> [Prop]
Expr.concKeccakProps [Prop]
prePs
    vars :: CollectVars
vars = [Prop] -> CollectVars
extractVars [Prop]
ps
    bufs :: [Expr 'Buf]
bufs = [Prop] -> [Expr 'Buf]
extractBufs [Prop]
ps
    stores :: CollectStorage
stores = [Prop] -> CollectStorage
extractStorage [Prop]
ps
    testVals :: Integer -> Gen (Maybe SMT.SMTCex)
    testVals :: Integer -> Gen (Maybe SMTCex)
testVals Integer
0 = Maybe SMTCex -> Gen (Maybe SMTCex)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SMTCex
forall a. Maybe a
Nothing
    testVals Integer
todo = do
      Map (Expr 'EWord) W256
varvals <- CollectVars -> Gen (Map (Expr 'EWord) W256)
getvals CollectVars
vars
      Map (Expr 'Buf) BufModel
bufVals <- [Expr 'Buf] -> Gen (Map (Expr 'Buf) BufModel)
getBufs [Expr 'Buf]
bufs
      Map (Expr 'EAddr) (Map W256 W256)
storeVals <- CollectStorage -> Gen (Map (Expr 'EAddr) (Map W256 W256))
getStores CollectStorage
stores
      let
        ret :: [Prop]
ret = [Prop] -> [Prop]
filterCorrectKeccak ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ (Prop -> Prop) -> [Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Map (Expr 'EWord) W256 -> Prop -> Prop
substituteEWord Map (Expr 'EWord) W256
varvals (Prop -> Prop) -> (Prop -> Prop) -> Prop -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Expr 'Buf) BufModel -> Prop -> Prop
substituteBuf Map (Expr 'Buf) BufModel
bufVals (Prop -> Prop) -> (Prop -> Prop) -> Prop -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Expr 'EAddr) (Map W256 W256) -> Prop -> Prop
substituteStores Map (Expr 'EAddr) (Map W256 W256)
storeVals) [Prop]
ps
        retSimp :: [Prop]
retSimp = [Prop] -> [Prop]
Expr.simplifyProps ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop] -> [Prop]
Expr.concKeccakProps [Prop]
ret
      if [Prop] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Prop]
retSimp then Maybe SMTCex -> Gen (Maybe SMTCex)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe SMTCex -> Gen (Maybe SMTCex))
-> Maybe SMTCex -> Gen (Maybe SMTCex)
forall a b. (a -> b) -> a -> b
$ SMTCex -> Maybe SMTCex
forall a. a -> Maybe a
Just (SMT.SMTCex {
                                    $sel:vars:SMTCex :: Map (Expr 'EWord) W256
vars = Map (Expr 'EWord) W256
varvals
                                    , $sel:addrs:SMTCex :: Map (Expr 'EAddr) Addr
addrs = Map (Expr 'EAddr) Addr
forall a. Monoid a => a
mempty
                                    , $sel:buffers:SMTCex :: Map (Expr 'Buf) BufModel
buffers = Map (Expr 'Buf) BufModel
bufVals
                                    , $sel:store:SMTCex :: Map (Expr 'EAddr) (Map W256 W256)
store = Map (Expr 'EAddr) (Map W256 W256)
storeVals
                                    , $sel:blockContext:SMTCex :: Map (Expr 'EWord) W256
blockContext = Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty
                                    , $sel:txContext:SMTCex :: Map (Expr 'EWord) W256
txContext = Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty
                                    })
                                    else Integer -> Gen (Maybe SMTCex)
testVals (Integer
todoInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)

-- Filter out PEq (Lit X) (keccak (ConcreteBuf Y)) if it's correct
filterCorrectKeccak :: [Prop] -> [Prop]
filterCorrectKeccak :: [Prop] -> [Prop]
filterCorrectKeccak [Prop]
ps = (Prop -> Bool) -> [Prop] -> [Prop]
forall a. (a -> Bool) -> [a] -> [a]
filter Prop -> Bool
checkKecc [Prop]
ps
  where
    checkKecc :: Prop -> Bool
checkKecc (PEq (Lit W256
x) (Keccak (ConcreteBuf ByteString
y))) = ByteString -> W256
keccak' ByteString
y W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
/= W256
x
    checkKecc Prop
_ = Bool
True

substituteEWord :: Map (Expr EWord) W256 -> Prop -> Prop
substituteEWord :: Map (Expr 'EWord) W256 -> Prop -> Prop
substituteEWord Map (Expr 'EWord) W256
valMap Prop
p = (forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go Prop
p
  where
    go :: Expr a -> Expr a
    go :: forall (a :: EType). Expr a -> Expr a
go orig :: Expr a
orig@(Var Text
_) = W256 -> Expr 'EWord
Lit (Map (Expr 'EWord) W256
valMap Map (Expr 'EWord) W256 -> Expr 'EWord -> W256
forall k a. Ord k => Map k a -> k -> a
! Expr a
Expr 'EWord
orig)
    go orig :: Expr a
orig@(Expr a
TxValue) = W256 -> Expr 'EWord
Lit (Map (Expr 'EWord) W256
valMap Map (Expr 'EWord) W256 -> Expr 'EWord -> W256
forall k a. Ord k => Map k a -> k -> a
! Expr a
Expr 'EWord
orig)
    go Expr a
a = Expr a
a


substituteBuf :: Map (Expr Buf) SMT.BufModel -> Prop -> Prop
substituteBuf :: Map (Expr 'Buf) BufModel -> Prop -> Prop
substituteBuf Map (Expr 'Buf) BufModel
valMap Prop
p = (forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go Prop
p
  where
    go :: Expr a -> Expr a
    go :: forall (a :: EType). Expr a -> Expr a
go orig :: Expr a
orig@(AbstractBuf Text
_) = case (Map (Expr 'Buf) BufModel
valMap Map (Expr 'Buf) BufModel -> Expr 'Buf -> Maybe BufModel
forall k a. Ord k => Map k a -> k -> Maybe a
!? Expr a
Expr 'Buf
orig) of
                                Just (SMT.Flat ByteString
x) -> ByteString -> Expr 'Buf
ConcreteBuf ByteString
x
                                Just (SMT.Comp CompressedBuf
_) -> [Char] -> Expr a
forall a. HasCallStack => [Char] -> a
internalError [Char]
"No compressed allowed in fuzz"
                                Maybe BufModel
Nothing -> Expr a
orig
    go Expr a
a = Expr a
a

substituteStores ::  Map (Expr 'EAddr) (Map W256 W256) -> Prop -> Prop
substituteStores :: Map (Expr 'EAddr) (Map W256 W256) -> Prop -> Prop
substituteStores Map (Expr 'EAddr) (Map W256 W256)
valMap Prop
p = (forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
go Prop
p
  where
    go :: Expr a -> Expr a
    -- TODO: Is this OK??
    go :: forall (a :: EType). Expr a -> Expr a
go (AbstractStore Expr 'EAddr
a Maybe W256
_) = case Map (Expr 'EAddr) (Map W256 W256)
valMap Map (Expr 'EAddr) (Map W256 W256)
-> Expr 'EAddr -> Maybe (Map W256 W256)
forall k a. Ord k => Map k a -> k -> Maybe a
!? Expr 'EAddr
a of
                                  Just Map W256 W256
m -> Map W256 W256 -> Expr 'Storage
ConcreteStore Map W256 W256
m
                                  Maybe (Map W256 W256)
Nothing -> Map W256 W256 -> Expr 'Storage
ConcreteStore Map W256 W256
forall a. Monoid a => a
mempty
    go Expr a
a = Expr a
a

-- Var extraction
data CollectVars = CollectVars {CollectVars -> Set (Expr 'EWord)
vars :: Set.Set (Expr EWord)
                               ,CollectVars -> Set W256
vals :: Set.Set W256
                               }
  deriving (Int -> CollectVars -> ShowS
[CollectVars] -> ShowS
CollectVars -> [Char]
(Int -> CollectVars -> ShowS)
-> (CollectVars -> [Char])
-> ([CollectVars] -> ShowS)
-> Show CollectVars
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CollectVars -> ShowS
showsPrec :: Int -> CollectVars -> ShowS
$cshow :: CollectVars -> [Char]
show :: CollectVars -> [Char]
$cshowList :: [CollectVars] -> ShowS
showList :: [CollectVars] -> ShowS
Show)

initVarsState :: CollectVars
initVarsState :: CollectVars
initVarsState = CollectVars {$sel:vars:CollectVars :: Set (Expr 'EWord)
vars = Set (Expr 'EWord)
forall a. Set a
Set.empty
                            ,$sel:vals:CollectVars :: Set W256
vals =  Set W256
forall a. Set a
Set.empty
                            }

findVarProp :: Prop -> State CollectVars Prop
findVarProp :: Prop -> State CollectVars Prop
findVarProp Prop
p = (forall (a :: EType).
 Expr a -> StateT CollectVars Identity (Expr a))
-> Prop -> State CollectVars Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> State CollectVars (Expr a)
forall (a :: EType). Expr a -> StateT CollectVars Identity (Expr a)
go Prop
p
  where
    go :: forall a. Expr a -> State CollectVars (Expr a)
    go :: forall (a :: EType). Expr a -> StateT CollectVars Identity (Expr a)
go = \case
      e :: Expr a
e@(Var Text
a) -> do
        CollectVars
s <- StateT CollectVars Identity CollectVars
forall s (m :: * -> *). MonadState s m => m s
get
        CollectVars -> StateT CollectVars Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put CollectVars
s {$sel:vars:CollectVars :: Set (Expr 'EWord)
vars = Expr 'EWord -> Set (Expr 'EWord) -> Set (Expr 'EWord)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Text -> Expr 'EWord
Var Text
a) CollectVars
s.vars}
        Expr a -> State CollectVars (Expr a)
forall a. a -> StateT CollectVars Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e
      e :: Expr a
e@(Lit W256
a) -> do
        CollectVars
s <- StateT CollectVars Identity CollectVars
forall s (m :: * -> *). MonadState s m => m s
get
        CollectVars -> StateT CollectVars Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (CollectVars
s {$sel:vals:CollectVars :: Set W256
vals=W256 -> Set W256 -> Set W256
forall a. Ord a => a -> Set a -> Set a
Set.insert W256
a CollectVars
s.vals} ::CollectVars)
        Expr a -> State CollectVars (Expr a)
forall a. a -> StateT CollectVars Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e
      Expr a
e -> Expr a -> State CollectVars (Expr a)
forall a. a -> StateT CollectVars Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e


extractVars :: [Prop] -> CollectVars
extractVars :: [Prop] -> CollectVars
extractVars [Prop]
ps = StateT CollectVars Identity () -> CollectVars -> CollectVars
forall s a. State s a -> s -> s
execState ((Prop -> State CollectVars Prop)
-> [Prop] -> StateT CollectVars Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop -> State CollectVars Prop
findVarProp [Prop]
ps) CollectVars
initVarsState


--- Buf extraction
newtype CollectBufs = CollectBufs { CollectBufs -> Set (Expr 'Buf)
bufs :: Set.Set (Expr Buf) }
  deriving (Int -> CollectBufs -> ShowS
[CollectBufs] -> ShowS
CollectBufs -> [Char]
(Int -> CollectBufs -> ShowS)
-> (CollectBufs -> [Char])
-> ([CollectBufs] -> ShowS)
-> Show CollectBufs
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CollectBufs -> ShowS
showsPrec :: Int -> CollectBufs -> ShowS
$cshow :: CollectBufs -> [Char]
show :: CollectBufs -> [Char]
$cshowList :: [CollectBufs] -> ShowS
showList :: [CollectBufs] -> ShowS
Show)

initBufsState :: CollectBufs
initBufsState :: CollectBufs
initBufsState = CollectBufs { $sel:bufs:CollectBufs :: Set (Expr 'Buf)
bufs = Set (Expr 'Buf)
forall a. Set a
Set.empty }

extractBufs :: [Prop] -> [Expr Buf]
extractBufs :: [Prop] -> [Expr 'Buf]
extractBufs [Prop]
ps = Set (Expr 'Buf) -> [Expr 'Buf]
forall a. Set a -> [a]
Set.toList Set (Expr 'Buf)
bufs
 where
  CollectBufs Set (Expr 'Buf)
bufs = State CollectBufs () -> CollectBufs -> CollectBufs
forall s a. State s a -> s -> s
execState ((Prop -> StateT CollectBufs Identity Prop)
-> [Prop] -> State CollectBufs ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop -> StateT CollectBufs Identity Prop
findBufProp [Prop]
ps) CollectBufs
initBufsState

findBufProp :: Prop -> State CollectBufs Prop
findBufProp :: Prop -> StateT CollectBufs Identity Prop
findBufProp Prop
p = (forall (a :: EType).
 Expr a -> StateT CollectBufs Identity (Expr a))
-> Prop -> StateT CollectBufs Identity Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> State CollectBufs (Expr a)
forall (a :: EType). Expr a -> StateT CollectBufs Identity (Expr a)
go Prop
p
  where
    go :: forall a. Expr a -> State CollectBufs (Expr a)
    go :: forall (a :: EType). Expr a -> StateT CollectBufs Identity (Expr a)
go = \case
      e :: Expr a
e@(AbstractBuf Text
a) -> do
        CollectBufs
s <- StateT CollectBufs Identity CollectBufs
forall s (m :: * -> *). MonadState s m => m s
get
        CollectBufs -> State CollectBufs ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put CollectBufs
s {$sel:bufs:CollectBufs :: Set (Expr 'Buf)
bufs=Expr 'Buf -> Set (Expr 'Buf) -> Set (Expr 'Buf)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Text -> Expr 'Buf
AbstractBuf Text
a) CollectBufs
s.bufs}
        Expr a -> State CollectBufs (Expr a)
forall a. a -> StateT CollectBufs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e
      Expr a
e -> Expr a -> State CollectBufs (Expr a)
forall a. a -> StateT CollectBufs Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e

--- Store extraction
data CollectStorage = CollectStorage { CollectStorage -> Set (Expr 'EAddr, Maybe W256)
addrs :: Set.Set (Expr EAddr, Maybe W256)
                                     , CollectStorage -> Set W256
keys :: Set.Set W256
                                     , CollectStorage -> Set W256
vals :: Set.Set W256
                                     }
  deriving (Int -> CollectStorage -> ShowS
[CollectStorage] -> ShowS
CollectStorage -> [Char]
(Int -> CollectStorage -> ShowS)
-> (CollectStorage -> [Char])
-> ([CollectStorage] -> ShowS)
-> Show CollectStorage
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CollectStorage -> ShowS
showsPrec :: Int -> CollectStorage -> ShowS
$cshow :: CollectStorage -> [Char]
show :: CollectStorage -> [Char]
$cshowList :: [CollectStorage] -> ShowS
showList :: [CollectStorage] -> ShowS
Show)

instance Semigroup (CollectStorage) where
  (CollectStorage Set (Expr 'EAddr, Maybe W256)
a Set W256
b Set W256
c) <> :: CollectStorage -> CollectStorage -> CollectStorage
<> (CollectStorage Set (Expr 'EAddr, Maybe W256)
a2 Set W256
b2 Set W256
c2) = Set (Expr 'EAddr, Maybe W256)
-> Set W256 -> Set W256 -> CollectStorage
CollectStorage (Set (Expr 'EAddr, Maybe W256)
a Set (Expr 'EAddr, Maybe W256)
-> Set (Expr 'EAddr, Maybe W256) -> Set (Expr 'EAddr, Maybe W256)
forall a. Semigroup a => a -> a -> a
<> Set (Expr 'EAddr, Maybe W256)
a2) (Set W256
b Set W256 -> Set W256 -> Set W256
forall a. Semigroup a => a -> a -> a
<> Set W256
b2) (Set W256
c Set W256 -> Set W256 -> Set W256
forall a. Semigroup a => a -> a -> a
<> Set W256
c2)

initStorageState :: CollectStorage
initStorageState :: CollectStorage
initStorageState = CollectStorage { $sel:addrs:CollectStorage :: Set (Expr 'EAddr, Maybe W256)
addrs = Set (Expr 'EAddr, Maybe W256)
forall a. Set a
Set.empty, $sel:keys:CollectStorage :: Set W256
keys = Set W256
forall a. Set a
Set.empty, $sel:vals:CollectStorage :: Set W256
vals = [W256] -> Set W256
forall a. Ord a => [a] -> Set a
Set.fromList [W256
0x0, W256
0x1, W256
Expr.maxLit] }

extractStorage :: [Prop] -> CollectStorage
extractStorage :: [Prop] -> CollectStorage
extractStorage [Prop]
ps = State CollectStorage () -> CollectStorage -> CollectStorage
forall s a. State s a -> s -> s
execState ((Prop -> StateT CollectStorage Identity Prop)
-> [Prop] -> State CollectStorage ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop -> StateT CollectStorage Identity Prop
findStoragePropInner [Prop]
ps) CollectStorage
initStorageState CollectStorage -> CollectStorage -> CollectStorage
forall a. Semigroup a => a -> a -> a
<>
    State CollectStorage () -> CollectStorage -> CollectStorage
forall s a. State s a -> s -> s
execState ((Prop -> StateT CollectStorage Identity Prop)
-> [Prop] -> State CollectStorage ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop -> StateT CollectStorage Identity Prop
findStoragePropComp [Prop]
ps) CollectStorage
initStorageState

findStoragePropComp :: Prop -> State CollectStorage Prop
findStoragePropComp :: Prop -> StateT CollectStorage Identity Prop
findStoragePropComp Prop
p = Prop -> StateT CollectStorage Identity Prop
go2 Prop
p
  where
    go2 :: Prop -> State CollectStorage (Prop)
    go2 :: Prop -> StateT CollectStorage Identity Prop
go2 = \case
      PNeg Prop
x -> Prop -> StateT CollectStorage Identity Prop
go2 Prop
x
      e :: Prop
e@(PEq (Lit W256
val) (SLoad {})) -> do
        CollectStorage
s <- StateT CollectStorage Identity CollectStorage
forall s (m :: * -> *). MonadState s m => m s
get
        CollectStorage -> State CollectStorage ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (CollectStorage
s {$sel:vals:CollectStorage :: Set W256
vals=W256 -> Set W256 -> Set W256
forall a. Ord a => a -> Set a -> Set a
Set.insert W256
val CollectStorage
s.vals} :: CollectStorage)
        Prop -> StateT CollectStorage Identity Prop
forall a. a -> StateT CollectStorage Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
e
      e :: Prop
e@(PLT (Lit W256
val) (SLoad {})) -> do
        CollectStorage
s <- StateT CollectStorage Identity CollectStorage
forall s (m :: * -> *). MonadState s m => m s
get
        CollectStorage -> State CollectStorage ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (CollectStorage
s {$sel:vals:CollectStorage :: Set W256
vals=W256 -> Set W256 -> Set W256
forall a. Ord a => a -> Set a -> Set a
Set.insert W256
val CollectStorage
s.vals} :: CollectStorage)
        Prop -> StateT CollectStorage Identity Prop
forall a. a -> StateT CollectStorage Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
e
      (PGT a :: Expr 'EWord
a@(Lit W256
_) b :: Expr 'EWord
b@(SLoad {})) -> Prop -> StateT CollectStorage Identity Prop
go2 (Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
a Expr 'EWord
b)
      (PGEq a :: Expr 'EWord
a@(Lit W256
_) b :: Expr 'EWord
b@(SLoad {})) -> Prop -> StateT CollectStorage Identity Prop
go2 (Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
a Expr 'EWord
b)
      (PLEq a :: Expr 'EWord
a@(Lit W256
_) b :: Expr 'EWord
b@(SLoad {})) -> Prop -> StateT CollectStorage Identity Prop
go2 (Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
a Expr 'EWord
b)
      Prop
e -> Prop -> StateT CollectStorage Identity Prop
forall a. a -> StateT CollectStorage Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
e

findStoragePropInner :: Prop -> State CollectStorage Prop
findStoragePropInner :: Prop -> StateT CollectStorage Identity Prop
findStoragePropInner Prop
p = (forall (a :: EType).
 Expr a -> StateT CollectStorage Identity (Expr a))
-> Prop -> StateT CollectStorage Identity Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> State CollectStorage (Expr a)
forall (a :: EType).
Expr a -> StateT CollectStorage Identity (Expr a)
go Prop
p
  where
    go :: forall a. Expr a -> State CollectStorage (Expr a)
    go :: forall (a :: EType).
Expr a -> StateT CollectStorage Identity (Expr a)
go = \case
      e :: Expr a
e@(AbstractStore Expr 'EAddr
a Maybe W256
idx) -> do
        CollectStorage
s <- StateT CollectStorage Identity CollectStorage
forall s (m :: * -> *). MonadState s m => m s
get
        CollectStorage -> State CollectStorage ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put CollectStorage
s {$sel:addrs:CollectStorage :: Set (Expr 'EAddr, Maybe W256)
addrs=(Expr 'EAddr, Maybe W256)
-> Set (Expr 'EAddr, Maybe W256) -> Set (Expr 'EAddr, Maybe W256)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Expr 'EAddr
a, Maybe W256
idx) CollectStorage
s.addrs}
        Expr a -> State CollectStorage (Expr a)
forall a. a -> StateT CollectStorage Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e
      e :: Expr a
e@(SLoad (Lit W256
val) Expr 'Storage
_) -> do
        CollectStorage
s <- StateT CollectStorage Identity CollectStorage
forall s (m :: * -> *). MonadState s m => m s
get
        CollectStorage -> State CollectStorage ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put CollectStorage
s {$sel:keys:CollectStorage :: Set W256
keys=W256 -> Set W256 -> Set W256
forall a. Ord a => a -> Set a -> Set a
Set.insert W256
val CollectStorage
s.keys}
        Expr a -> State CollectStorage (Expr a)
forall a. a -> StateT CollectStorage Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e
      e :: Expr a
e@(SStore Expr 'EWord
_ (Lit W256
val) Expr 'Storage
_) -> do
        CollectStorage
s <- StateT CollectStorage Identity CollectStorage
forall s (m :: * -> *). MonadState s m => m s
get
        CollectStorage -> State CollectStorage ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (CollectStorage
s {$sel:vals:CollectStorage :: Set W256
vals=W256 -> Set W256 -> Set W256
forall a. Ord a => a -> Set a -> Set a
Set.insert W256
val CollectStorage
s.vals} :: CollectStorage)
        Expr a -> State CollectStorage (Expr a)
forall a. a -> StateT CollectStorage Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e
      Expr a
e -> Expr a -> State CollectStorage (Expr a)
forall a. a -> StateT CollectStorage Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr a
e

-- Var value and TX value generation
getvals :: CollectVars -> Gen (Map (Expr EWord) W256)
getvals :: CollectVars -> Gen (Map (Expr 'EWord) W256)
getvals CollectVars
vars = do
    Map (Expr 'EWord) W256
bufs <- [Expr 'EWord]
-> Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256)
go (Set (Expr 'EWord) -> [Expr 'EWord]
forall a. Set a -> [a]
Set.toList CollectVars
vars.vars) Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty
    Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256)
addTxStuff Map (Expr 'EWord) W256
bufs
  where
    addTxStuff :: Map (Expr EWord) W256 -> Gen (Map (Expr EWord) W256)
    addTxStuff :: Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256)
addTxStuff Map (Expr 'EWord) W256
a = do
      W256
val <- [(Int, Gen W256)] -> Gen W256
forall a. [(Int, Gen a)] -> Gen a
frequency [ (Int
20, W256 -> Gen W256
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure W256
0)
                       , (Int
1, Gen W256
getRndW256)
                       ]
      Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256))
-> Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256)
forall a b. (a -> b) -> a -> b
$ Expr 'EWord
-> W256 -> Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr 'EWord
TxValue W256
val Map (Expr 'EWord) W256
a
    go :: [Expr EWord] -> Map (Expr EWord) W256 -> Gen (Map (Expr EWord) W256)
    go :: [Expr 'EWord]
-> Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256)
go [] Map (Expr 'EWord) W256
valMap = Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map (Expr 'EWord) W256
valMap
    go (Expr 'EWord
a:[Expr 'EWord]
ax) Map (Expr 'EWord) W256
valMap = do
      Bool
pickKnown :: Bool <- Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
      W256
val <- if (Bool -> Bool
not Bool
pickKnown) Bool -> Bool -> Bool
|| (Set W256 -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null CollectVars
vars.vals) then do Gen W256
getRndW256
                                                    else [W256] -> Gen W256
forall a. [a] -> Gen a
elements ([W256] -> Gen W256) -> [W256] -> Gen W256
forall a b. (a -> b) -> a -> b
$ Set W256 -> [W256]
forall a. Set a -> [a]
Set.toList (CollectVars
vars.vals)
      [Expr 'EWord]
-> Map (Expr 'EWord) W256 -> Gen (Map (Expr 'EWord) W256)
go [Expr 'EWord]
ax (Expr 'EWord
-> W256 -> Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr 'EWord
a W256
val Map (Expr 'EWord) W256
valMap)

-- Storage value generation
getStores :: CollectStorage -> Gen (Map (Expr EAddr) (Map W256 W256))
getStores :: CollectStorage -> Gen (Map (Expr 'EAddr) (Map W256 W256))
getStores CollectStorage
storesLoads = [(Expr 'EAddr, Maybe W256)]
-> Map (Expr 'EAddr) (Map W256 W256)
-> Gen (Map (Expr 'EAddr) (Map W256 W256))
go (Set (Expr 'EAddr, Maybe W256) -> [(Expr 'EAddr, Maybe W256)]
forall a. Set a -> [a]
Set.toList CollectStorage
storesLoads.addrs) Map (Expr 'EAddr) (Map W256 W256)
forall a. Monoid a => a
mempty
  where
    go :: [(Expr EAddr, Maybe W256)] -> Map (Expr EAddr) (Map W256 W256) -> Gen (Map (Expr EAddr) (Map W256 W256))
    go :: [(Expr 'EAddr, Maybe W256)]
-> Map (Expr 'EAddr) (Map W256 W256)
-> Gen (Map (Expr 'EAddr) (Map W256 W256))
go [] Map (Expr 'EAddr) (Map W256 W256)
addrToValsMap = Map (Expr 'EAddr) (Map W256 W256)
-> Gen (Map (Expr 'EAddr) (Map W256 W256))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map (Expr 'EAddr) (Map W256 W256)
addrToValsMap
    go ((Expr 'EAddr
addr, Maybe W256
_):[(Expr 'EAddr, Maybe W256)]
ax) Map (Expr 'EAddr) (Map W256 W256)
addrToValsMap = do
      -- number of elements inserted into storage
      Int
numElems :: Int <- [(Int, Gen Int)] -> Gen Int
forall a. [(Int, Gen a)] -> Gen a
frequency [(Int
1, Int -> Gen Int
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0)
                                   ,(Int
10, (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
10))
                                   ,(Int
1, (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
11, Int
100))
                                   ]
      [(W256, W256)]
l <- Int -> Gen (W256, W256) -> Gen [(W256, W256)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
numElems Gen (W256, W256)
oneWrite
      [(Expr 'EAddr, Maybe W256)]
-> Map (Expr 'EAddr) (Map W256 W256)
-> Gen (Map (Expr 'EAddr) (Map W256 W256))
go [(Expr 'EAddr, Maybe W256)]
ax (Expr 'EAddr
-> Map W256 W256
-> Map (Expr 'EAddr) (Map W256 W256)
-> Map (Expr 'EAddr) (Map W256 W256)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr 'EAddr
addr ([(W256, W256)] -> Map W256 W256
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(W256, W256)]
l) Map (Expr 'EAddr) (Map W256 W256)
addrToValsMap)
        where
          oneWrite :: Gen (W256, W256)
          oneWrite :: Gen (W256, W256)
oneWrite = do
                    Maybe W256
a <- Set W256 -> Gen (Maybe W256)
getRndElem CollectStorage
storesLoads.keys
                    W256
b <- [(Int, Gen W256)] -> Gen W256
forall a. [(Int, Gen a)] -> Gen a
frequency [(Int
1, Gen W256
getRndW256)
                                   ,(Int
3, [W256] -> Gen W256
forall a. [a] -> Gen a
elements ([W256] -> Gen W256) -> [W256] -> Gen W256
forall a b. (a -> b) -> a -> b
$ Set W256 -> [W256]
forall a. Set a -> [a]
Set.toList CollectStorage
storesLoads.vals)
                                   ]
                    (W256, W256) -> Gen (W256, W256)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (W256 -> Maybe W256 -> W256
forall a. a -> Maybe a -> a
fromMaybe (W256
0::W256) Maybe W256
a, W256
b)
    getRndElem :: Set W256 -> Gen (Maybe W256)
    getRndElem :: Set W256 -> Gen (Maybe W256)
getRndElem Set W256
choices = if Set W256 -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set W256
choices then Maybe W256 -> Gen (Maybe W256)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe W256
forall a. Maybe a
Nothing
                         else do (W256 -> Maybe W256) -> Gen W256 -> Gen (Maybe W256)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap W256 -> Maybe W256
forall a. a -> Maybe a
Just (Gen W256 -> Gen (Maybe W256)) -> Gen W256 -> Gen (Maybe W256)
forall a b. (a -> b) -> a -> b
$ [W256] -> Gen W256
forall a. [a] -> Gen a
elements ([W256] -> Gen W256) -> [W256] -> Gen W256
forall a b. (a -> b) -> a -> b
$ Set W256 -> [W256]
forall a. Set a -> [a]
Set.toList Set W256
choices

-- Buf value generation
getBufs :: [Expr Buf] -> Gen (Map (Expr Buf) SMT.BufModel)
getBufs :: [Expr 'Buf] -> Gen (Map (Expr 'Buf) BufModel)
getBufs [Expr 'Buf]
bufs = [Expr 'Buf]
-> Map (Expr 'Buf) BufModel -> Gen (Map (Expr 'Buf) BufModel)
go [Expr 'Buf]
bufs Map (Expr 'Buf) BufModel
forall a. Monoid a => a
mempty
  where
    go :: [Expr Buf] -> Map (Expr Buf) SMT.BufModel -> Gen (Map (Expr Buf) SMT.BufModel)
    go :: [Expr 'Buf]
-> Map (Expr 'Buf) BufModel -> Gen (Map (Expr 'Buf) BufModel)
go [] Map (Expr 'Buf) BufModel
valMap = Map (Expr 'Buf) BufModel -> Gen (Map (Expr 'Buf) BufModel)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map (Expr 'Buf) BufModel
valMap
    go (Expr 'Buf
a:[Expr 'Buf]
ax) Map (Expr 'Buf) BufModel
valMap = do
      [Word8]
bytes :: [Word8] <- [(Int, Gen [Word8])] -> Gen [Word8]
forall a. [(Int, Gen a)] -> Gen a
frequency [
              (Int
1, do
                Int
x :: Int <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)
                Int -> Gen Word8 -> Gen [Word8]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
x Gen Word8
forall a. Arbitrary a => Gen a
arbitrary)
            , (Int
1, Int -> Gen Word8 -> Gen [Word8]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
0 Gen Word8
forall a. Arbitrary a => Gen a
arbitrary)
       ]
      [Expr 'Buf]
-> Map (Expr 'Buf) BufModel -> Gen (Map (Expr 'Buf) BufModel)
go [Expr 'Buf]
ax (Expr 'Buf
-> BufModel -> Map (Expr 'Buf) BufModel -> Map (Expr 'Buf) BufModel
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr 'Buf
a (ByteString -> BufModel
SMT.Flat (ByteString -> BufModel) -> ByteString -> BufModel
forall a b. (a -> b) -> a -> b
$ [Word8] -> ByteString
BS.pack [Word8]
bytes) Map (Expr 'Buf) BufModel
valMap)

getRndW256 :: Gen W256
getRndW256 :: Gen W256
getRndW256 = do
      [Word8]
val <- Int -> Gen Word8 -> Gen [Word8]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
32 Gen Word8
forall a. Arbitrary a => Gen a
arbitrary
      W256 -> Gen W256
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (W256 -> Gen W256) -> W256 -> Gen W256
forall a b. (a -> b) -> a -> b
$ [Word8] -> W256
bytesToW256 [Word8]
val