{-# Language DataKinds #-}
{-# Language GADTs #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
{-# Language QuasiQuotes #-}

{- |
    Module: EVM.SMT
    Description: Utilities for building and executing SMT queries from Expr instances
-}
module EVM.SMT where

import Prelude hiding (LT, GT)

import Control.Monad
import Data.Containers.ListUtils (nubOrd)
import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)
import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))
import Data.Word
import Numeric (readHex, readBin)
import Data.ByteString (ByteString)

import qualified Data.ByteString as BS
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty((:|)))
import qualified Data.List.NonEmpty as NonEmpty
import Data.String.Here
import Data.Maybe (fromJust)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Text.Lazy (Text)
import qualified Data.Text as TS
import qualified Data.Text.Lazy as T
import Data.Text.Lazy.Builder
import Data.Bifunctor (second)

import EVM.Types
import EVM.Traversals
import EVM.CSE
import EVM.Keccak
import EVM.Expr (writeByte, bufLengthEnv, containsNode, bufLength, minLength)
import qualified EVM.Expr as Expr


-- ** Encoding ** ----------------------------------------------------------------------------------


-- variable names in SMT that we want to get values for
data CexVars = CexVars
  { CexVars -> [Text]
calldata     :: [Text]
  , CexVars -> Map Text (Expr 'EWord)
buffers      :: Map Text (Expr EWord) -- buffers and guesses at their maximum size
  , CexVars -> [(Expr 'EWord, Expr 'EWord)]
storeReads   :: [(Expr EWord, Expr EWord)] -- a list of relevant store reads
  , CexVars -> [Text]
blockContext :: [Text]
  , CexVars -> [Text]
txContext    :: [Text]
  }
  deriving (CexVars -> CexVars -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CexVars -> CexVars -> Bool
$c/= :: CexVars -> CexVars -> Bool
== :: CexVars -> CexVars -> Bool
$c== :: CexVars -> CexVars -> Bool
Eq, Int -> CexVars -> ShowS
[CexVars] -> ShowS
CexVars -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CexVars] -> ShowS
$cshowList :: [CexVars] -> ShowS
show :: CexVars -> [Char]
$cshow :: CexVars -> [Char]
showsPrec :: Int -> CexVars -> ShowS
$cshowsPrec :: Int -> CexVars -> ShowS
Show)

instance Semigroup CexVars where
  (CexVars [Text]
a Map Text (Expr 'EWord)
b [(Expr 'EWord, Expr 'EWord)]
c [Text]
d [Text]
e) <> :: CexVars -> CexVars -> CexVars
<> (CexVars [Text]
a2 Map Text (Expr 'EWord)
b2 [(Expr 'EWord, Expr 'EWord)]
c2 [Text]
d2 [Text]
e2) = [Text]
-> Map Text (Expr 'EWord)
-> [(Expr 'EWord, Expr 'EWord)]
-> [Text]
-> [Text]
-> CexVars
CexVars ([Text]
a forall a. Semigroup a => a -> a -> a
<> [Text]
a2) (Map Text (Expr 'EWord)
b forall a. Semigroup a => a -> a -> a
<> Map Text (Expr 'EWord)
b2) ([(Expr 'EWord, Expr 'EWord)]
c forall a. Semigroup a => a -> a -> a
<> [(Expr 'EWord, Expr 'EWord)]
c2) ([Text]
d forall a. Semigroup a => a -> a -> a
<> [Text]
d2) ([Text]
e forall a. Semigroup a => a -> a -> a
<> [Text]
e2)

instance Monoid CexVars where
    mempty :: CexVars
mempty = CexVars
      { $sel:calldata:CexVars :: [Text]
calldata = forall a. Monoid a => a
mempty
      , $sel:buffers:CexVars :: Map Text (Expr 'EWord)
buffers = forall a. Monoid a => a
mempty
      , $sel:storeReads:CexVars :: [(Expr 'EWord, Expr 'EWord)]
storeReads = forall a. Monoid a => a
mempty
      , $sel:blockContext:CexVars :: [Text]
blockContext = forall a. Monoid a => a
mempty
      , $sel:txContext:CexVars :: [Text]
txContext = forall a. Monoid a => a
mempty
      }

-- | A model for a buffer, either in it's compressed form (for storing parsed
-- models from a solver), or as a bytestring (for presentation to users)
data BufModel
  = Comp CompressedBuf
  | Flat ByteString
  deriving (BufModel -> BufModel -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BufModel -> BufModel -> Bool
$c/= :: BufModel -> BufModel -> Bool
== :: BufModel -> BufModel -> Bool
$c== :: BufModel -> BufModel -> Bool
Eq, Int -> BufModel -> ShowS
[BufModel] -> ShowS
BufModel -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [BufModel] -> ShowS
$cshowList :: [BufModel] -> ShowS
show :: BufModel -> [Char]
$cshow :: BufModel -> [Char]
showsPrec :: Int -> BufModel -> ShowS
$cshowsPrec :: Int -> BufModel -> ShowS
Show)

-- | This representation lets us store buffers of arbitrary length without
-- exhausting the available memory, it closely matches the format used by
-- smt-lib when returning models for arrays
data CompressedBuf
  = Base { CompressedBuf -> Word8
byte :: Word8, CompressedBuf -> W256
length :: W256}
  | Write { byte :: Word8, CompressedBuf -> W256
idx :: W256, CompressedBuf -> CompressedBuf
next :: CompressedBuf }
  deriving (CompressedBuf -> CompressedBuf -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CompressedBuf -> CompressedBuf -> Bool
$c/= :: CompressedBuf -> CompressedBuf -> Bool
== :: CompressedBuf -> CompressedBuf -> Bool
$c== :: CompressedBuf -> CompressedBuf -> Bool
Eq, Int -> CompressedBuf -> ShowS
[CompressedBuf] -> ShowS
CompressedBuf -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CompressedBuf] -> ShowS
$cshowList :: [CompressedBuf] -> ShowS
show :: CompressedBuf -> [Char]
$cshow :: CompressedBuf -> [Char]
showsPrec :: Int -> CompressedBuf -> ShowS
$cshowsPrec :: Int -> CompressedBuf -> ShowS
Show)


-- | a final post shrinking cex, buffers here are all represented as concrete bytestrings
data SMTCex = SMTCex
  { SMTCex -> Map (Expr 'EWord) W256
vars :: Map (Expr EWord) W256
  , SMTCex -> Map (Expr 'Buf) BufModel
buffers :: Map (Expr Buf) BufModel
  , SMTCex -> Map W256 (Map W256 W256)
store :: Map W256 (Map W256 W256)
  , SMTCex -> Map (Expr 'EWord) W256
blockContext :: Map (Expr EWord) W256
  , SMTCex -> Map (Expr 'EWord) W256
txContext :: Map (Expr EWord) W256
  }
  deriving (SMTCex -> SMTCex -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTCex -> SMTCex -> Bool
$c/= :: SMTCex -> SMTCex -> Bool
== :: SMTCex -> SMTCex -> Bool
$c== :: SMTCex -> SMTCex -> Bool
Eq, Int -> SMTCex -> ShowS
[SMTCex] -> ShowS
SMTCex -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SMTCex] -> ShowS
$cshowList :: [SMTCex] -> ShowS
show :: SMTCex -> [Char]
$cshow :: SMTCex -> [Char]
showsPrec :: Int -> SMTCex -> ShowS
$cshowsPrec :: Int -> SMTCex -> ShowS
Show)

flattenBufs :: SMTCex -> Maybe SMTCex
flattenBufs :: SMTCex -> Maybe SMTCex
flattenBufs SMTCex
cex = do
  Map (Expr 'Buf) BufModel
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM BufModel -> Maybe BufModel
collapse SMTCex
cex.buffers
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SMTCex
cex{ $sel:buffers:SMTCex :: Map (Expr 'Buf) BufModel
buffers = Map (Expr 'Buf) BufModel
bs }

-- | Attemps to collapse a compressed buffer representation down to a flattened one
collapse :: BufModel -> Maybe BufModel
collapse :: BufModel -> Maybe BufModel
collapse BufModel
model = case BufModel -> Maybe (Expr 'Buf)
toBuf BufModel
model of
  Just (ConcreteBuf ByteString
b) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ByteString -> BufModel
Flat ByteString
b
  Maybe (Expr 'Buf)
_ -> forall a. Maybe a
Nothing
  where
    toBuf :: BufModel -> Maybe (Expr 'Buf)
toBuf (Comp (Base Word8
b W256
sz)) | W256
sz forall a. Ord a => a -> a -> Bool
<= W256
120_000_000 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (forall a b. (Integral a, Num b) => a -> b
num W256
sz) Word8
b
    toBuf (Comp (Write Word8
b W256
idx CompressedBuf
next)) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
writeByte (W256 -> Expr 'EWord
Lit W256
idx) (Word8 -> Expr 'Byte
LitByte Word8
b)) (BufModel -> Maybe (Expr 'Buf)
toBuf forall a b. (a -> b) -> a -> b
$ CompressedBuf -> BufModel
Comp CompressedBuf
next)
    toBuf (Flat ByteString
b) = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ ByteString
b
    toBuf BufModel
_ = forall a. Maybe a
Nothing

getVar :: SMTCex -> TS.Text -> W256
getVar :: SMTCex -> Text -> W256
getVar SMTCex
cex Text
name = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Text -> Expr 'EWord
Var Text
name) SMTCex
cex.vars

data SMT2 = SMT2 [Builder] CexVars
  deriving (SMT2 -> SMT2 -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMT2 -> SMT2 -> Bool
$c/= :: SMT2 -> SMT2 -> Bool
== :: SMT2 -> SMT2 -> Bool
$c== :: SMT2 -> SMT2 -> Bool
Eq, Int -> SMT2 -> ShowS
[SMT2] -> ShowS
SMT2 -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SMT2] -> ShowS
$cshowList :: [SMT2] -> ShowS
show :: SMT2 -> [Char]
$cshow :: SMT2 -> [Char]
showsPrec :: Int -> SMT2 -> ShowS
$cshowsPrec :: Int -> SMT2 -> ShowS
Show)

instance Semigroup SMT2 where
  (SMT2 [Builder]
a CexVars
b) <> :: SMT2 -> SMT2 -> SMT2
<> (SMT2 [Builder]
a2 CexVars
b2) = [Builder] -> CexVars -> SMT2
SMT2 ([Builder]
a forall a. Semigroup a => a -> a -> a
<> [Builder]
a2) (CexVars
b forall a. Semigroup a => a -> a -> a
<> CexVars
b2)

instance Monoid SMT2 where
  mempty :: SMT2
mempty = [Builder] -> CexVars -> SMT2
SMT2 forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty

formatSMT2 :: SMT2 -> Text
formatSMT2 :: SMT2 -> Text
formatSMT2 (SMT2 [Builder]
ls CexVars
_) = [Text] -> Text
T.unlines (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
ls)

-- | Reads all intermediate variables from the builder state and produces SMT declaring them as constants
declareIntermediates :: BufEnv -> StoreEnv -> SMT2
declareIntermediates :: BufEnv -> StoreEnv -> SMT2
declareIntermediates BufEnv
bufs StoreEnv
stores =
  let encSs :: Map Int Builder
encSs = forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey forall {p} {a :: EType}. Show p => p -> Expr a -> Builder
encodeStore StoreEnv
stores
      encBs :: Map Int Builder
encBs = forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey Int -> Expr 'Buf -> Builder
encodeBuf BufEnv
bufs
      sorted :: [(Int, Builder)]
sorted = forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy forall {a} {b} {b}. Ord a => (a, b) -> (a, b) -> Ordering
compareFst forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ Map Int Builder
encSs forall a. Semigroup a => a -> a -> a
<> Map Int Builder
encBs
      decls :: [Builder]
decls = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd [(Int, Builder)]
sorted
  in [Builder] -> CexVars -> SMT2
SMT2 ([Text -> Builder
fromText Text
"; intermediate buffers & stores"] forall a. Semigroup a => a -> a -> a
<> [Builder]
decls) forall a. Monoid a => a
mempty
  where
    compareFst :: (a, b) -> (a, b) -> Ordering
compareFst (a
l, b
_) (a
r, b
_) = forall a. Ord a => a -> a -> Ordering
compare a
l a
r
    encodeBuf :: Int -> Expr 'Buf -> Builder
encodeBuf Int
n Expr 'Buf
expr =
      Builder
"(define-const buf" forall a. Semigroup a => a -> a -> a
<> ([Char] -> Builder
fromString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
n) forall a. Semigroup a => a -> a -> a
<> Builder
" Buf " forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
expr forall a. Semigroup a => a -> a -> a
<> Builder
")\n" forall a. Semigroup a => a -> a -> a
<> Int -> Expr 'Buf -> Builder
encodeBufLen Int
n Expr 'Buf
expr
    encodeBufLen :: Int -> Expr 'Buf -> Builder
encodeBufLen Int
n Expr 'Buf
expr =
      Builder
"(define-const buf" forall a. Semigroup a => a -> a -> a
<> ([Char] -> Builder
fromString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
n) forall a. Semigroup a => a -> a -> a
<>Builder
"_length" forall a. Semigroup a => a -> a -> a
<> Builder
" (_ BitVec 256) " forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> Builder
exprToSMT (BufEnv -> Bool -> Expr 'Buf -> Expr 'EWord
bufLengthEnv BufEnv
bufs Bool
True Expr 'Buf
expr) forall a. Semigroup a => a -> a -> a
<> Builder
")"
    encodeStore :: p -> Expr a -> Builder
encodeStore p
n Expr a
expr =
       Builder
"(define-const store" forall a. Semigroup a => a -> a -> a
<> ([Char] -> Builder
fromString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ p
n) forall a. Semigroup a => a -> a -> a
<> Builder
" Storage " forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
expr forall a. Semigroup a => a -> a -> a
<> Builder
")"

assertProps :: [Prop] -> SMT2
assertProps :: [Prop] -> SMT2
assertProps [Prop]
ps =
  let encs :: [Builder]
encs = forall a b. (a -> b) -> [a] -> [b]
map Prop -> Builder
propToSMT [Prop]
ps_elim
      intermediates :: SMT2
intermediates = BufEnv -> StoreEnv -> SMT2
declareIntermediates BufEnv
bufs StoreEnv
stores in
  SMT2
prelude
  forall a. Semigroup a => a -> a -> a
<> ([Prop] -> BufEnv -> StoreEnv -> SMT2
declareBufs [Prop]
ps_elim BufEnv
bufs StoreEnv
stores)
  forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
  forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) [] [[Builder]]
allVars)
  forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
  forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareFrameContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) [] [[Builder]]
frameCtx)
  forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
  forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareBlockContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) [] [[Builder]]
blockCtx)
  forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
  forall a. Semigroup a => a -> a -> a
<> SMT2
intermediates
  forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
  forall a. Semigroup a => a -> a -> a
<> SMT2
keccakAssumes
  forall a. Semigroup a => a -> a -> a
<> SMT2
readAssumes
  forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
  forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Builder
p -> Builder
"(assert " forall a. Semigroup a => a -> a -> a
<> Builder
p forall a. Semigroup a => a -> a -> a
<> Builder
")") [Builder]
encs) forall a. Monoid a => a
mempty
  forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [] forall a. Monoid a => a
mempty{ $sel:storeReads:CexVars :: [(Expr 'EWord, Expr 'EWord)]
storeReads = [(Expr 'EWord, Expr 'EWord)]
storageReads }

  where
    ([Prop]
ps_elim, BufEnv
bufs, StoreEnv
stores) = [Prop] -> ([Prop], BufEnv, StoreEnv)
eliminateProps [Prop]
ps

    allVars :: [[Builder]]
allVars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
referencedVars' [Prop]
ps_elim forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedVars [Expr 'Buf]
bufVals forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedVars [Expr 'Storage]
storeVals
    frameCtx :: [[Builder]]
frameCtx = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
referencedFrameContext' [Prop]
ps_elim forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedFrameContext [Expr 'Buf]
bufVals forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedFrameContext [Expr 'Storage]
storeVals
    blockCtx :: [[Builder]]
blockCtx = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
referencedBlockContext' [Prop]
ps_elim forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedBlockContext [Expr 'Buf]
bufVals forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedBlockContext [Expr 'Storage]
storeVals

    bufVals :: [Expr 'Buf]
bufVals = forall k a. Map k a -> [a]
Map.elems BufEnv
bufs
    storeVals :: [Expr 'Storage]
storeVals = forall k a. Map k a -> [a]
Map.elems StoreEnv
stores

    storageReads :: [(Expr 'EWord, Expr 'EWord)]
storageReads = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Prop -> [(Expr 'EWord, Expr 'EWord)]
findStorageReads [Prop]
ps

    keccakAssumes :: SMT2
keccakAssumes
      = [Builder] -> CexVars -> SMT2
SMT2 [Builder
"; keccak assumptions"] forall a. Monoid a => a
mempty
      forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Prop
p -> Builder
"(assert " forall a. Semigroup a => a -> a -> a
<> Prop -> Builder
propToSMT Prop
p forall a. Semigroup a => a -> a -> a
<> Builder
")") ([Prop] -> [Expr 'Buf] -> [Expr 'Storage] -> [Prop]
keccakAssumptions [Prop]
ps_elim [Expr 'Buf]
bufVals [Expr 'Storage]
storeVals)) forall a. Monoid a => a
mempty

    readAssumes :: SMT2
readAssumes
      = [Builder] -> CexVars -> SMT2
SMT2 [Builder
"; read assumptions"] forall a. Monoid a => a
mempty
        forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Prop
p -> Builder
"(assert " forall a. Semigroup a => a -> a -> a
<> Prop -> Builder
propToSMT Prop
p forall a. Semigroup a => a -> a -> a
<> Builder
")") ([Prop] -> BufEnv -> StoreEnv -> [Prop]
assertReads [Prop]
ps_elim BufEnv
bufs StoreEnv
stores)) forall a. Monoid a => a
mempty

referencedBufsGo :: Expr a -> [Builder]
referencedBufsGo :: forall (a :: EType). Expr a -> [Builder]
referencedBufsGo = \case
  AbstractBuf Text
s -> [Text -> Builder
fromText Text
s]
  Expr a
_ -> []

referencedBufs :: Expr a -> [Builder]
referencedBufs :: forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr a
expr = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> [Builder]
referencedBufsGo [] Expr a
expr

referencedBufs' :: Prop -> [Builder]
referencedBufs' :: Prop -> [Builder]
referencedBufs' Prop
prop = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> [Builder]
referencedBufsGo [] Prop
prop

referencedVarsGo :: Expr a -> [Builder]
referencedVarsGo :: forall (a :: EType). Expr a -> [Builder]
referencedVarsGo = \case
  Var Text
s -> [Text -> Builder
fromText Text
s]
  Expr a
_ -> []

referencedVars :: Expr a -> [Builder]
referencedVars :: forall (a :: EType). Expr a -> [Builder]
referencedVars Expr a
expr = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> [Builder]
referencedVarsGo [] Expr a
expr

referencedVars' :: Prop -> [Builder]
referencedVars' :: Prop -> [Builder]
referencedVars' Prop
prop = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> [Builder]
referencedVarsGo [] Prop
prop

referencedFrameContextGo :: Expr a -> [Builder]
referencedFrameContextGo :: forall (a :: EType). Expr a -> [Builder]
referencedFrameContextGo = \case
  CallValue Int
a -> [Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"callvalue_" ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
a)]
  Caller Int
a -> [Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"caller_" ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
a)]
  Address Int
a -> [Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"address_" ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
a)]
  Balance {} -> forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: BALANCE"
  SelfBalance {} -> forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: SELFBALANCE"
  Gas {} -> forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: GAS"
  Expr a
_ -> []

referencedFrameContext :: Expr a -> [Builder]
referencedFrameContext :: forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr a
expr = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> [Builder]
referencedFrameContextGo [] Expr a
expr

referencedFrameContext' :: Prop -> [Builder]
referencedFrameContext' :: Prop -> [Builder]
referencedFrameContext' Prop
prop = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> [Builder]
referencedFrameContextGo [] Prop
prop


referencedBlockContextGo :: Expr a -> [Builder]
referencedBlockContextGo :: forall (a :: EType). Expr a -> [Builder]
referencedBlockContextGo = \case
  Expr a
Origin -> [Builder
"origin"]
  Expr a
Coinbase -> [Builder
"coinbase"]
  Expr a
Timestamp -> [Builder
"timestamp"]
  Expr a
BlockNumber -> [Builder
"blocknumber"]
  Expr a
PrevRandao -> [Builder
"prevrandao"]
  Expr a
GasLimit -> [Builder
"gaslimit"]
  Expr a
ChainId -> [Builder
"chainid"]
  Expr a
BaseFee -> [Builder
"basefee"]
  Expr a
_ -> []

referencedBlockContext :: Expr a -> [Builder]
referencedBlockContext :: forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr a
expr = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> [Builder]
referencedBlockContextGo [] Expr a
expr

referencedBlockContext' :: Prop -> [Builder]
referencedBlockContext' :: Prop -> [Builder]
referencedBlockContext' Prop
prop = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> [Builder]
referencedBlockContextGo [] Prop
prop

-- | This function overapproximates the reads from the abstract
-- storage. Potentially, it can return locations that do not read a
-- slot directly from the abstract store but from subsequent writes on
-- the store (e.g, SLoad addr idx (SStore addr idx val AbstractStore)).
-- However, we expect that most of such reads will have been
-- simplified away.
findStorageReads :: Prop -> [(Expr EWord, Expr EWord)]
findStorageReads :: Prop -> [(Expr 'EWord, Expr 'EWord)]
findStorageReads = forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> [(Expr 'EWord, Expr 'EWord)]
go []
  where
    go :: Expr a -> [(Expr EWord, Expr EWord)]
    go :: forall (a :: EType). Expr a -> [(Expr 'EWord, Expr 'EWord)]
go = \case
      SLoad Expr 'EWord
addr Expr 'EWord
slot Expr 'Storage
storage -> [(Expr 'EWord
addr, Expr 'EWord
slot) | forall (b :: EType).
(forall (a :: EType). Expr a -> Bool) -> Expr b -> Bool
containsNode forall (a :: EType). Expr a -> Bool
isAbstractStore Expr 'Storage
storage]
      Expr a
_ -> []

    isAbstractStore :: Expr a -> Bool
isAbstractStore Expr a
AbstractStore = Bool
True
    isAbstractStore Expr a
_ = Bool
False


findBufferAccess :: TraversableTerm a => [a] -> [(Expr EWord, Expr EWord, Expr Buf)]
findBufferAccess :: forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm forall (a :: EType).
Expr a -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
go) forall a. Monoid a => a
mempty
  where
    go :: Expr a -> [(Expr EWord, Expr EWord, Expr Buf)]
    go :: forall (a :: EType).
Expr a -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
go = \case
      ReadWord Expr 'EWord
idx Expr 'Buf
buf -> [(Expr 'EWord
idx, W256 -> Expr 'EWord
Lit W256
32, Expr 'Buf
buf)]
      ReadByte Expr 'EWord
idx Expr 'Buf
buf -> [(Expr 'EWord
idx, W256 -> Expr 'EWord
Lit W256
1, Expr 'Buf
buf)]
      CopySlice Expr 'EWord
srcOff Expr 'EWord
_ Expr 'EWord
size Expr 'Buf
src Expr 'Buf
_  -> [(Expr 'EWord
srcOff, Expr 'EWord
size, Expr 'Buf
src)]
      Expr a
_ -> forall a. Monoid a => a
mempty

-- | Asserts that buffer reads beyond the size of the buffer are equal
-- to zero. Looks for buffer reads in the a list of given predicates
-- and the buffer and storage environments.
assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]
assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]
assertReads [Prop]
props BufEnv
benv StoreEnv
senv = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr 'EWord, Expr 'EWord, Expr 'Buf) -> [Prop]
assertRead [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
allReads
  where
    assertRead :: (Expr EWord, Expr EWord, Expr Buf) -> [Prop]
    assertRead :: (Expr 'EWord, Expr 'EWord, Expr 'Buf) -> [Prop]
assertRead (Expr 'EWord
idx, Lit W256
32, Expr 'Buf
buf) = [Prop -> Prop -> Prop
PImpl (Expr 'EWord -> Expr 'EWord -> Prop
PGEq Expr 'EWord
idx (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
buf)) (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (Expr 'EWord -> Expr 'Buf -> Expr 'EWord
ReadWord Expr 'EWord
idx Expr 'Buf
buf) (W256 -> Expr 'EWord
Lit W256
0))]
    assertRead (Expr 'EWord
idx, Lit W256
sz, Expr 'Buf
buf) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Int
s -> Prop -> Prop -> Prop
PImpl (Expr 'EWord -> Expr 'EWord -> Prop
PGEq Expr 'EWord
idx (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
buf)) (forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (Expr 'EWord -> Expr 'Buf -> Expr 'Byte
ReadByte Expr 'EWord
idx Expr 'Buf
buf) (Word8 -> Expr 'Byte
LitByte (forall a b. (Integral a, Num b) => a -> b
num Int
s)))) [(Int
0::Int)..forall a b. (Integral a, Num b) => a -> b
num W256
szforall a. Num a => a -> a -> a
-Int
1]
    assertRead (Expr 'EWord
_, Expr 'EWord
_, Expr 'Buf
_) = forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot generate assertions for accesses of symbolic size"

    allReads :: [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
allReads = forall a. (a -> Bool) -> [a] -> [a]
filter (Expr 'EWord, Expr 'EWord, Expr 'Buf) -> Bool
keepRead forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess [Prop]
props forall a. Semigroup a => a -> a -> a
<> forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess (forall k a. Map k a -> [a]
Map.elems BufEnv
benv) forall a. Semigroup a => a -> a -> a
<> forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess (forall k a. Map k a -> [a]
Map.elems StoreEnv
senv)

    -- discard constraints if we can statically determine that read is less than the buffer length
    keepRead :: (Expr 'EWord, Expr 'EWord, Expr 'Buf) -> Bool
keepRead (Lit W256
idx, Lit W256
size, Expr 'Buf
buf) =
      case BufEnv -> Expr 'Buf -> Maybe Integer
minLength BufEnv
benv Expr 'Buf
buf of
        Just Integer
l | forall a b. (Integral a, Num b) => a -> b
num (W256
idx forall a. Num a => a -> a -> a
+ W256
size) forall a. Ord a => a -> a -> Bool
<= Integer
l -> Bool
False
        Maybe Integer
_ -> Bool
True
    keepRead (Expr 'EWord, Expr 'EWord, Expr 'Buf)
_ = Bool
True

-- | Finds the maximum read index for each abstract buffer in the input props
discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr EWord)
discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr 'EWord)
discoverMaxReads [Prop]
props BufEnv
benv StoreEnv
senv = Map Text (Expr 'EWord)
bufMap
  where
    allReads :: [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
allReads = forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess [Prop]
props forall a. Semigroup a => a -> a -> a
<> forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess (forall k a. Map k a -> [a]
Map.elems BufEnv
benv) forall a. Semigroup a => a -> a -> a
<> forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess (forall k a. Map k a -> [a]
Map.elems StoreEnv
senv)
    -- we can have buffers that are not read from but are still mentioned via BufLength in some branch condition
    -- we assign a default read hint of 4 to start with in these cases (since in most cases we will need at least 4 bytes to produce a counterexample)
    allBufs :: Map Text (Expr 'EWord)
allBufs = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, W256 -> Expr 'EWord
Lit W256
4) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
referencedBufs' [Prop]
props forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedBufs (forall k a. Map k a -> [a]
Map.elems BufEnv
benv) forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedBufs (forall k a. Map k a -> [a]
Map.elems StoreEnv
senv)

    bufMap :: Map Text (Expr 'EWord)
bufMap = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.max (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map Text (Expr 'EWord)
-> (Expr 'EWord, Expr 'EWord, Expr 'Buf) -> Map Text (Expr 'EWord)
addBound forall a. Monoid a => a
mempty [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
allReads) Map Text (Expr 'EWord)
allBufs

    addBound :: Map Text (Expr 'EWord)
-> (Expr 'EWord, Expr 'EWord, Expr 'Buf) -> Map Text (Expr 'EWord)
addBound Map Text (Expr 'EWord)
m (Expr 'EWord
idx, Expr 'EWord
size, Expr 'Buf
buf) =
      case Expr 'Buf -> Expr 'Buf
baseBuf Expr 'Buf
buf of
        AbstractBuf Text
b -> forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.max (Text -> Text
T.fromStrict Text
b) (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
idx Expr 'EWord
size) Map Text (Expr 'EWord)
m
        Expr 'Buf
_ -> Map Text (Expr 'EWord)
m

    baseBuf :: Expr Buf -> Expr Buf
    baseBuf :: Expr 'Buf -> Expr 'Buf
baseBuf (AbstractBuf Text
b) = Text -> Expr 'Buf
AbstractBuf Text
b
    baseBuf (ConcreteBuf ByteString
b) = ByteString -> Expr 'Buf
ConcreteBuf ByteString
b
    baseBuf (GVar (BufVar Int
a)) =
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
a BufEnv
benv of
        Just Expr 'Buf
b -> Expr 'Buf -> Expr 'Buf
baseBuf Expr 'Buf
b
        Maybe (Expr 'Buf)
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: could not find buffer variable"
    baseBuf (WriteByte Expr 'EWord
_ Expr 'Byte
_ Expr 'Buf
b) = Expr 'Buf -> Expr 'Buf
baseBuf Expr 'Buf
b
    baseBuf (WriteWord Expr 'EWord
_ Expr 'EWord
_ Expr 'Buf
b) = Expr 'Buf -> Expr 'Buf
baseBuf Expr 'Buf
b
    baseBuf (CopySlice Expr 'EWord
_ Expr 'EWord
_ Expr 'EWord
_ Expr 'Buf
_ Expr 'Buf
dst)= Expr 'Buf -> Expr 'Buf
baseBuf Expr 'Buf
dst

-- | Returns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached
declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2
declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2
declareBufs [Prop]
props BufEnv
bufEnv StoreEnv
storeEnv = [Builder] -> CexVars -> SMT2
SMT2 (Builder
"; buffers" forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declareBuf [Builder]
allBufs forall a. Semigroup a => a -> a -> a
<> (Builder
"; buffer lengths" forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declareLength [Builder]
allBufs)) CexVars
cexvars
  where
    cexvars :: CexVars
cexvars = (forall a. Monoid a => a
mempty :: CexVars){ $sel:buffers:CexVars :: Map Text (Expr 'EWord)
buffers = [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr 'EWord)
discoverMaxReads [Prop]
props BufEnv
bufEnv StoreEnv
storeEnv }
    allBufs :: [Builder]
allBufs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
Map.keys CexVars
cexvars.buffers
    declareBuf :: a -> a
declareBuf a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
" (Array (_ BitVec 256) (_ BitVec 8)))"
    declareLength :: a -> a
declareLength a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
"_length" forall a. Semigroup a => a -> a -> a
<> a
" (_ BitVec 256))"

-- Given a list of variable names, create an SMT2 object with the variables declared
declareVars :: [Builder] -> SMT2
declareVars :: [Builder] -> SMT2
declareVars [Builder]
names = [Builder] -> CexVars -> SMT2
SMT2 ([Builder
"; variables"] forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
cexvars
  where
    declare :: a -> a
declare a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
" (_ BitVec 256))"
    cexvars :: CexVars
cexvars = (forall a. Monoid a => a
mempty :: CexVars){ $sel:calldata:CexVars :: [Text]
calldata = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
names }


declareFrameContext :: [Builder] -> SMT2
declareFrameContext :: [Builder] -> SMT2
declareFrameContext [Builder]
names = [Builder] -> CexVars -> SMT2
SMT2 ([Builder
"; frame context"] forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
cexvars
  where
    declare :: a -> a
declare a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
" (_ BitVec 256))"
    cexvars :: CexVars
cexvars = (forall a. Monoid a => a
mempty :: CexVars){ $sel:txContext:CexVars :: [Text]
txContext = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
names }


declareBlockContext :: [Builder] -> SMT2
declareBlockContext :: [Builder] -> SMT2
declareBlockContext [Builder]
names = [Builder] -> CexVars -> SMT2
SMT2 ([Builder
"; block context"] forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
cexvars
  where
    declare :: a -> a
declare a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
" (_ BitVec 256))"
    cexvars :: CexVars
cexvars = (forall a. Monoid a => a
mempty :: CexVars){ $sel:blockContext:CexVars :: [Text]
blockContext = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
names }


prelude :: SMT2
prelude :: SMT2
prelude =  (forall a b c. (a -> b -> c) -> b -> a -> c
flip [Builder] -> CexVars -> SMT2
SMT2) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Builder
fromLazyText forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Text -> Text
T.drop Int64
2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Text]
T.lines forall a b. (a -> b) -> a -> b
$ [i|
  ; logic
  ; TODO: this creates an error when used with z3?
  ;(set-logic QF_AUFBV)
  (set-logic ALL)

  ; types
  (define-sort Byte () (_ BitVec 8))
  (define-sort Word () (_ BitVec 256))
  (define-sort Buf () (Array Word Byte))

  ; address -> slot -> value
  (define-sort Storage () (Array Word (Array Word Word)))

  ; hash functions
  (declare-fun keccak (Buf) Word)
  (declare-fun sha256 (Buf) Word)

  (define-fun max ((a (_ BitVec 256)) (b (_ BitVec 256))) (_ BitVec 256) (ite (bvult a b) b a))

  ; word indexing
  (define-fun indexWord31 ((w Word)) Byte ((_ extract 7 0) w))
  (define-fun indexWord30 ((w Word)) Byte ((_ extract 15 8) w))
  (define-fun indexWord29 ((w Word)) Byte ((_ extract 23 16) w))
  (define-fun indexWord28 ((w Word)) Byte ((_ extract 31 24) w))
  (define-fun indexWord27 ((w Word)) Byte ((_ extract 39 32) w))
  (define-fun indexWord26 ((w Word)) Byte ((_ extract 47 40) w))
  (define-fun indexWord25 ((w Word)) Byte ((_ extract 55 48) w))
  (define-fun indexWord24 ((w Word)) Byte ((_ extract 63 56) w))
  (define-fun indexWord23 ((w Word)) Byte ((_ extract 71 64) w))
  (define-fun indexWord22 ((w Word)) Byte ((_ extract 79 72) w))
  (define-fun indexWord21 ((w Word)) Byte ((_ extract 87 80) w))
  (define-fun indexWord20 ((w Word)) Byte ((_ extract 95 88) w))
  (define-fun indexWord19 ((w Word)) Byte ((_ extract 103 96) w))
  (define-fun indexWord18 ((w Word)) Byte ((_ extract 111 104) w))
  (define-fun indexWord17 ((w Word)) Byte ((_ extract 119 112) w))
  (define-fun indexWord16 ((w Word)) Byte ((_ extract 127 120) w))
  (define-fun indexWord15 ((w Word)) Byte ((_ extract 135 128) w))
  (define-fun indexWord14 ((w Word)) Byte ((_ extract 143 136) w))
  (define-fun indexWord13 ((w Word)) Byte ((_ extract 151 144) w))
  (define-fun indexWord12 ((w Word)) Byte ((_ extract 159 152) w))
  (define-fun indexWord11 ((w Word)) Byte ((_ extract 167 160) w))
  (define-fun indexWord10 ((w Word)) Byte ((_ extract 175 168) w))
  (define-fun indexWord9 ((w Word)) Byte ((_ extract 183 176) w))
  (define-fun indexWord8 ((w Word)) Byte ((_ extract 191 184) w))
  (define-fun indexWord7 ((w Word)) Byte ((_ extract 199 192) w))
  (define-fun indexWord6 ((w Word)) Byte ((_ extract 207 200) w))
  (define-fun indexWord5 ((w Word)) Byte ((_ extract 215 208) w))
  (define-fun indexWord4 ((w Word)) Byte ((_ extract 223 216) w))
  (define-fun indexWord3 ((w Word)) Byte ((_ extract 231 224) w))
  (define-fun indexWord2 ((w Word)) Byte ((_ extract 239 232) w))
  (define-fun indexWord1 ((w Word)) Byte ((_ extract 247 240) w))
  (define-fun indexWord0 ((w Word)) Byte ((_ extract 255 248) w))

  ; symbolic word indexing
  ; a bitshift based version might be more performant here...
  (define-fun indexWord ((idx Word) (w Word)) Byte
    (ite (bvuge idx (_ bv32 256)) (_ bv0 8)
    (ite (= idx (_ bv31 256)) (indexWord31 w)
    (ite (= idx (_ bv30 256)) (indexWord30 w)
    (ite (= idx (_ bv29 256)) (indexWord29 w)
    (ite (= idx (_ bv28 256)) (indexWord28 w)
    (ite (= idx (_ bv27 256)) (indexWord27 w)
    (ite (= idx (_ bv26 256)) (indexWord26 w)
    (ite (= idx (_ bv25 256)) (indexWord25 w)
    (ite (= idx (_ bv24 256)) (indexWord24 w)
    (ite (= idx (_ bv23 256)) (indexWord23 w)
    (ite (= idx (_ bv22 256)) (indexWord22 w)
    (ite (= idx (_ bv21 256)) (indexWord21 w)
    (ite (= idx (_ bv20 256)) (indexWord20 w)
    (ite (= idx (_ bv19 256)) (indexWord19 w)
    (ite (= idx (_ bv18 256)) (indexWord18 w)
    (ite (= idx (_ bv17 256)) (indexWord17 w)
    (ite (= idx (_ bv16 256)) (indexWord16 w)
    (ite (= idx (_ bv15 256)) (indexWord15 w)
    (ite (= idx (_ bv14 256)) (indexWord14 w)
    (ite (= idx (_ bv13 256)) (indexWord13 w)
    (ite (= idx (_ bv12 256)) (indexWord12 w)
    (ite (= idx (_ bv11 256)) (indexWord11 w)
    (ite (= idx (_ bv10 256)) (indexWord10 w)
    (ite (= idx (_ bv9 256)) (indexWord9 w)
    (ite (= idx (_ bv8 256)) (indexWord8 w)
    (ite (= idx (_ bv7 256)) (indexWord7 w)
    (ite (= idx (_ bv6 256)) (indexWord6 w)
    (ite (= idx (_ bv5 256)) (indexWord5 w)
    (ite (= idx (_ bv4 256)) (indexWord4 w)
    (ite (= idx (_ bv3 256)) (indexWord3 w)
    (ite (= idx (_ bv2 256)) (indexWord2 w)
    (ite (= idx (_ bv1 256)) (indexWord1 w)
    (indexWord0 w)
    ))))))))))))))))))))))))))))))))
  )

  ; buffers
  (define-const emptyBuf Buf ((as const Buf) #b00000000))

  (define-fun readWord ((idx Word) (buf Buf)) Word
    (concat
      (select buf idx)
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000001))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000002))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000003))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000004))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000005))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000006))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000007))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000008))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000009))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000a))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000b))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000c))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000d))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000e))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000f))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000010))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000011))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000012))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000013))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000014))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000015))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000016))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000017))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000018))
      (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000019))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001a))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001b))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001c))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001d))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001e))
      (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001f))
    )
  )

  (define-fun writeWord ((idx Word) (val Word) (buf Buf)) Buf
      (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store
      (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store buf
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001f) (indexWord31 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001e) (indexWord30 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001d) (indexWord29 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001c) (indexWord28 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001b) (indexWord27 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001a) (indexWord26 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000019) (indexWord25 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000018) (indexWord24 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000017) (indexWord23 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000016) (indexWord22 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000015) (indexWord21 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000014) (indexWord20 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000013) (indexWord19 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000012) (indexWord18 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000011) (indexWord17 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000010) (indexWord16 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000f) (indexWord15 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000e) (indexWord14 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000d) (indexWord13 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000c) (indexWord12 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000b) (indexWord11 val))
      (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000a) (indexWord10 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000009) (indexWord9 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000008) (indexWord8 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000007) (indexWord7 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000006) (indexWord6 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000005) (indexWord5 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000004) (indexWord4 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000003) (indexWord3 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000002) (indexWord2 val))
      (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000001) (indexWord1 val))
      idx (indexWord0 val))
  )

  ; block context
  (declare-fun blockhash (Word) Word)

  ; macros
  (define-fun signext ( (b Word) (val Word)) Word
    (ite (= b (_ bv0  256)) ((_ sign_extend 248) ((_ extract 7    0) val))
    (ite (= b (_ bv1  256)) ((_ sign_extend 240) ((_ extract 15   0) val))
    (ite (= b (_ bv2  256)) ((_ sign_extend 232) ((_ extract 23   0) val))
    (ite (= b (_ bv3  256)) ((_ sign_extend 224) ((_ extract 31   0) val))
    (ite (= b (_ bv4  256)) ((_ sign_extend 216) ((_ extract 39   0) val))
    (ite (= b (_ bv5  256)) ((_ sign_extend 208) ((_ extract 47   0) val))
    (ite (= b (_ bv6  256)) ((_ sign_extend 200) ((_ extract 55   0) val))
    (ite (= b (_ bv7  256)) ((_ sign_extend 192) ((_ extract 63   0) val))
    (ite (= b (_ bv8  256)) ((_ sign_extend 184) ((_ extract 71   0) val))
    (ite (= b (_ bv9  256)) ((_ sign_extend 176) ((_ extract 79   0) val))
    (ite (= b (_ bv10 256)) ((_ sign_extend 168) ((_ extract 87   0) val))
    (ite (= b (_ bv11 256)) ((_ sign_extend 160) ((_ extract 95   0) val))
    (ite (= b (_ bv12 256)) ((_ sign_extend 152) ((_ extract 103  0) val))
    (ite (= b (_ bv13 256)) ((_ sign_extend 144) ((_ extract 111  0) val))
    (ite (= b (_ bv14 256)) ((_ sign_extend 136) ((_ extract 119  0) val))
    (ite (= b (_ bv15 256)) ((_ sign_extend 128) ((_ extract 127  0) val))
    (ite (= b (_ bv16 256)) ((_ sign_extend 120) ((_ extract 135  0) val))
    (ite (= b (_ bv17 256)) ((_ sign_extend 112) ((_ extract 143  0) val))
    (ite (= b (_ bv18 256)) ((_ sign_extend 104) ((_ extract 151  0) val))
    (ite (= b (_ bv19 256)) ((_ sign_extend 96 ) ((_ extract 159  0) val))
    (ite (= b (_ bv20 256)) ((_ sign_extend 88 ) ((_ extract 167  0) val))
    (ite (= b (_ bv21 256)) ((_ sign_extend 80 ) ((_ extract 175  0) val))
    (ite (= b (_ bv22 256)) ((_ sign_extend 72 ) ((_ extract 183  0) val))
    (ite (= b (_ bv23 256)) ((_ sign_extend 64 ) ((_ extract 191  0) val))
    (ite (= b (_ bv24 256)) ((_ sign_extend 56 ) ((_ extract 199  0) val))
    (ite (= b (_ bv25 256)) ((_ sign_extend 48 ) ((_ extract 207  0) val))
    (ite (= b (_ bv26 256)) ((_ sign_extend 40 ) ((_ extract 215  0) val))
    (ite (= b (_ bv27 256)) ((_ sign_extend 32 ) ((_ extract 223  0) val))
    (ite (= b (_ bv28 256)) ((_ sign_extend 24 ) ((_ extract 231  0) val))
    (ite (= b (_ bv29 256)) ((_ sign_extend 16 ) ((_ extract 239  0) val))
    (ite (= b (_ bv30 256)) ((_ sign_extend 8  ) ((_ extract 247  0) val)) val))))))))))))))))))))))))))))))))

  ; storage
  (declare-const abstractStore Storage)
  (define-const emptyStore Storage ((as const Storage) ((as const (Array (_ BitVec 256) (_ BitVec 256))) #x0000000000000000000000000000000000000000000000000000000000000000)))

  (define-fun sstore ((addr Word) (key Word) (val Word) (storage Storage)) Storage (store storage addr (store (select storage addr) key val)))

  (define-fun sload ((addr Word) (key Word) (storage Storage)) Word (select (select storage addr) key))
  |]


exprToSMT :: Expr a -> Builder
exprToSMT :: forall (a :: EType). Expr a -> Builder
exprToSMT = \case
  Lit W256
w -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"(_ bv" forall a. Semigroup a => a -> a -> a
<> ([Char] -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show (forall a b. (Integral a, Num b) => a -> b
num W256
w :: Integer)) forall a. Semigroup a => a -> a -> a
<> Text
" 256)"
  Var Text
s -> Text -> Builder
fromText Text
s
  GVar (BufVar Int
n) -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"buf" forall a. Semigroup a => a -> a -> a
<> ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
n)
  GVar (StoreVar Int
n) -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"store" forall a. Semigroup a => a -> a -> a
<> ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
n)
  JoinBytes
    Expr 'Byte
z Expr 'Byte
o 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
    -> [Expr 'Byte] -> Builder
concatBytes [
        Expr 'Byte
z, Expr 'Byte
o, 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]

  Add Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvadd" Expr 'EWord
a Expr 'EWord
b
  Sub Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvsub" Expr 'EWord
a Expr 'EWord
b
  Mul Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvmul" Expr 'EWord
a Expr 'EWord
b
  Exp Expr 'EWord
a Expr 'EWord
b -> case Expr 'EWord
b of
               Lit W256
b' -> Expr 'EWord -> W256 -> Builder
expandExp Expr 'EWord
a W256
b'
               Expr 'EWord
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"cannot encode symbolic exponentation into SMT"
  Min Expr 'EWord
a Expr 'EWord
b ->
    let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
a
        benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
b in
    Builder
"(ite (bvule " forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
") " forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
  Max Expr 'EWord
a Expr 'EWord
b ->
    let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
a
        benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
b in
    Builder
"(max " forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
  LT Expr 'EWord
a Expr 'EWord
b ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvult" Expr 'EWord
a Expr 'EWord
b in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  SLT Expr 'EWord
a Expr 'EWord
b ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvslt" Expr 'EWord
a Expr 'EWord
b in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  SGT Expr 'EWord
a Expr 'EWord
b ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvsgt" Expr 'EWord
a Expr 'EWord
b in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  GT Expr 'EWord
a Expr 'EWord
b ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvugt" Expr 'EWord
a Expr 'EWord
b in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  LEq Expr 'EWord
a Expr 'EWord
b ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvule" Expr 'EWord
a Expr 'EWord
b in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  GEq Expr 'EWord
a Expr 'EWord
b ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvuge" Expr 'EWord
a Expr 'EWord
b in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  Eq Expr 'EWord
a Expr 'EWord
b ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"=" Expr 'EWord
a Expr 'EWord
b in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  IsZero Expr 'EWord
a ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"=" Expr 'EWord
a (W256 -> Expr 'EWord
Lit W256
0) in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  And Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvand" Expr 'EWord
a Expr 'EWord
b
  Or Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvor" Expr 'EWord
a Expr 'EWord
b
  Xor Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvxor" Expr 'EWord
a Expr 'EWord
b
  Not Expr 'EWord
a -> forall {a :: EType}. Builder -> Expr a -> Builder
op1 Builder
"bvnot" Expr 'EWord
a
  SHL Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvshl" Expr 'EWord
b Expr 'EWord
a
  SHR Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvlshr" Expr 'EWord
b Expr 'EWord
a
  SAR Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvashr" Expr 'EWord
b Expr 'EWord
a
  SEx Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"signext" Expr 'EWord
a Expr 'EWord
b
  Div Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
"bvudiv" Expr 'EWord
a Expr 'EWord
b
  SDiv Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
"bvsdiv" Expr 'EWord
a Expr 'EWord
b
  Mod Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
"bvurem" Expr 'EWord
a Expr 'EWord
b
  SMod Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
"bvsrem" Expr 'EWord
a Expr 'EWord
b
  -- NOTE: this needs to do the MUL at a higher precision, then MOD, then downcast
  MulMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c ->
    let aExp :: Builder
aExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
a
        bExp :: Builder
bExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
b
        cExp :: Builder
cExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
c
        aLift :: Builder
aLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
aExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
        bLift :: Builder
bLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
bExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
        cLift :: Builder
cLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
cExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
    in  Builder
"((_ extract 255 0) (ite (= " forall a. Semigroup a => a -> a -> a
<> Builder
cExp forall a. Semigroup a => a -> a -> a
<> Builder
" (_ bv0 256)) (_ bv0 512) (bvurem (bvmul " forall a. Semigroup a => a -> a -> a
<> Builder
aLift Builder -> Builder -> Builder
`sp` Builder
bLift forall a. Semigroup a => a -> a -> a
<> Builder
")" forall a. Semigroup a => a -> a -> a
<> Builder
cLift forall a. Semigroup a => a -> a -> a
<> Builder
")))"
  AddMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c ->
    let aExp :: Builder
aExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
a
        bExp :: Builder
bExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
b
        cExp :: Builder
cExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
c
        aLift :: Builder
aLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
aExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
        bLift :: Builder
bLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
bExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
        cLift :: Builder
cLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
cExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
    in  Builder
"((_ extract 255 0) (ite (= " forall a. Semigroup a => a -> a -> a
<> Builder
cExp forall a. Semigroup a => a -> a -> a
<> Builder
" (_ bv0 256)) (_ bv0 512) (bvurem (bvadd " forall a. Semigroup a => a -> a -> a
<> Builder
aLift Builder -> Builder -> Builder
`sp` Builder
bLift forall a. Semigroup a => a -> a -> a
<> Builder
")" forall a. Semigroup a => a -> a -> a
<> Builder
cLift forall a. Semigroup a => a -> a -> a
<> Builder
")))"
  EqByte Expr 'Byte
a Expr 'Byte
b ->
    let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"=" Expr 'Byte
a Expr 'Byte
b in
    Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
  Keccak Expr 'Buf
a ->
    let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
a in
    Builder
"(keccak " forall a. Semigroup a => a -> a -> a
<> Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
  SHA256 Expr 'Buf
a ->
    let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
a in
    Builder
"(sha256 " forall a. Semigroup a => a -> a -> a
<> Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"

  CallValue Int
a -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"callvalue_" ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
a)
  Caller Int
a -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"caller_" ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
a)
  Address Int
a -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"address_" ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
a)

  Expr a
Origin ->  Builder
"origin"
  BlockHash Expr 'EWord
a ->
    let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
a in
    Builder
"(blockhash " forall a. Semigroup a => a -> a -> a
<> Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
  Expr a
Coinbase -> Builder
"coinbase"
  Expr a
Timestamp -> Builder
"timestamp"
  Expr a
BlockNumber -> Builder
"blocknumber"
  Expr a
PrevRandao -> Builder
"prevrandao"
  Expr a
GasLimit -> Builder
"gaslimit"
  Expr a
ChainId -> Builder
"chainid"
  Expr a
BaseFee -> Builder
"basefee"

  LitByte Word8
b -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"(_ bv" forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (forall a. Show a => a -> [Char]
show (forall a b. (Integral a, Num b) => a -> b
num Word8
b :: Integer)) forall a. Semigroup a => a -> a -> a
<> Text
" 8)"
  IndexWord Expr 'EWord
idx Expr 'EWord
w -> case Expr 'EWord
idx of
    Lit W256
n -> if W256
n forall a. Ord a => a -> a -> Bool
>= W256
0 Bool -> Bool -> Bool
&& W256
n forall a. Ord a => a -> a -> Bool
< W256
32
             then
               let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
w in
               Text -> Builder
fromLazyText (Text
"(indexWord" forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (forall a. Show a => a -> [Char]
show (forall a b. (Integral a, Num b) => a -> b
num W256
n :: Integer))) Builder -> Builder -> Builder
`sp` Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
             else forall (a :: EType). Expr a -> Builder
exprToSMT (Word8 -> Expr 'Byte
LitByte Word8
0)
    Expr 'EWord
_ -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"indexWord" Expr 'EWord
idx Expr 'EWord
w
  ReadByte Expr 'EWord
idx Expr 'Buf
src -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"select" Expr 'Buf
src Expr 'EWord
idx

  ConcreteBuf ByteString
"" -> Builder
"emptyBuf"
  ConcreteBuf ByteString
bs -> ByteString -> Expr 'Buf -> Builder
writeBytes ByteString
bs forall a. Monoid a => a
mempty
  AbstractBuf Text
s -> Text -> Builder
fromText Text
s
  ReadWord Expr 'EWord
idx Expr 'Buf
prev -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"readWord" Expr 'EWord
idx Expr 'Buf
prev
  BufLength (AbstractBuf Text
b) -> Text -> Builder
fromText Text
b forall a. Semigroup a => a -> a -> a
<> Builder
"_length"
  BufLength (GVar (BufVar Int
n)) -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"buf" forall a. Semigroup a => a -> a -> a
<> ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Int
n) forall a. Semigroup a => a -> a -> a
<> Text
"_length"
  BufLength Expr 'Buf
b -> forall (a :: EType). Expr a -> Builder
exprToSMT (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
b)
  WriteByte Expr 'EWord
idx Expr 'Byte
val Expr 'Buf
prev ->
    let encIdx :: Builder
encIdx = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
idx
        encVal :: Builder
encVal = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Byte
val
        encPrev :: Builder
encPrev = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
prev in
    Builder
"(store " forall a. Semigroup a => a -> a -> a
<> Builder
encPrev Builder -> Builder -> Builder
`sp` Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal forall a. Semigroup a => a -> a -> a
<> Builder
")"
  WriteWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
prev ->
    let encIdx :: Builder
encIdx = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
idx
        encVal :: Builder
encVal = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
val
        encPrev :: Builder
encPrev = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
prev in
    Builder
"(writeWord " forall a. Semigroup a => a -> a -> a
<> Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
`sp` Builder
encPrev forall a. Semigroup a => a -> a -> a
<> Builder
")"
  CopySlice Expr 'EWord
srcIdx Expr 'EWord
dstIdx Expr 'EWord
size Expr 'Buf
src Expr 'Buf
dst ->
    Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Builder -> Builder -> Builder
copySlice Expr 'EWord
srcIdx Expr 'EWord
dstIdx Expr 'EWord
size (forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
src) (forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
dst)
  Expr a
EmptyStore -> Builder
"emptyStore"
  ConcreteStore Map W256 (Map W256 W256)
s -> Map W256 (Map W256 W256) -> Builder
encodeConcreteStore Map W256 (Map W256 W256)
s
  Expr a
AbstractStore -> Builder
"abstractStore"
  SStore Expr 'EWord
addr Expr 'EWord
idx Expr 'EWord
val Expr 'Storage
prev ->
    let encAddr :: Builder
encAddr = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
addr
        encIdx :: Builder
encIdx = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
idx
        encVal :: Builder
encVal = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
val
        encPrev :: Builder
encPrev = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Storage
prev in
    Builder
"(sstore" Builder -> Builder -> Builder
`sp` Builder
encAddr Builder -> Builder -> Builder
`sp` Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
`sp` Builder
encPrev forall a. Semigroup a => a -> a -> a
<> Builder
")"
  SLoad Expr 'EWord
addr Expr 'EWord
idx Expr 'Storage
store -> forall {a :: EType} {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Expr a -> Builder
op3 Builder
"sload" Expr 'EWord
addr Expr 'EWord
idx Expr 'Storage
store

  Expr a
a -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"TODO: implement: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show Expr a
a
  where
    op1 :: Builder -> Expr a -> Builder
op1 Builder
op Expr a
a =
      let enc :: Builder
enc =  forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a in
      Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
    op2 :: Builder -> Expr a -> Expr a -> Builder
op2 Builder
op Expr a
a Expr a
b =
      let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a
          benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
b in
      Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
    op3 :: Builder -> Expr a -> Expr a -> Expr a -> Builder
op3 Builder
op Expr a
a Expr a
b Expr a
c =
      let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a
          benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
b
          cenc :: Builder
cenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
c in
      Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc Builder -> Builder -> Builder
`sp` Builder
cenc forall a. Semigroup a => a -> a -> a
<> Builder
")"
    op2CheckZero :: Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
op Expr a
a Expr a
b =
      let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a
          benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
b in
      Builder
"(ite (= " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
" (_ bv0 256)) (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<>  Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
"))"

sp :: Builder -> Builder -> Builder
Builder
a sp :: Builder -> Builder -> Builder
`sp` Builder
b = Builder
a forall a. Semigroup a => a -> a -> a
<> (Text -> Builder
fromText Text
" ") forall a. Semigroup a => a -> a -> a
<> Builder
b

zero :: Builder
zero :: Builder
zero = Builder
"(_ bv0 256)"

one :: Builder
one :: Builder
one = Builder
"(_ bv1 256)"

propToSMT :: Prop -> Builder
propToSMT :: Prop -> Builder
propToSMT = \case
  PEq Expr a
a Expr a
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"=" Expr a
a Expr a
b
  PLT Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvult" Expr 'EWord
a Expr 'EWord
b
  PGT Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvugt" Expr 'EWord
a Expr 'EWord
b
  PLEq Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvule" Expr 'EWord
a Expr 'EWord
b
  PGEq Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvuge" Expr 'EWord
a Expr 'EWord
b
  PNeg Prop
a ->
    let enc :: Builder
enc = Prop -> Builder
propToSMT Prop
a in
    Builder
"(not " forall a. Semigroup a => a -> a -> a
<> Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
  PAnd Prop
a Prop
b ->
    let aenc :: Builder
aenc = Prop -> Builder
propToSMT Prop
a
        benc :: Builder
benc = Prop -> Builder
propToSMT Prop
b in
    Builder
"(and " forall a. Semigroup a => a -> a -> a
<> Builder
aenc forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
  POr Prop
a Prop
b ->
    let aenc :: Builder
aenc = Prop -> Builder
propToSMT Prop
a
        benc :: Builder
benc = Prop -> Builder
propToSMT Prop
b in
    Builder
"(or " forall a. Semigroup a => a -> a -> a
<> Builder
aenc forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
  PImpl Prop
a Prop
b ->
    let aenc :: Builder
aenc = Prop -> Builder
propToSMT Prop
a
        benc :: Builder
benc = Prop -> Builder
propToSMT Prop
b in
    Builder
"(=> " forall a. Semigroup a => a -> a -> a
<> Builder
aenc forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
  PBool Bool
b -> if Bool
b then Builder
"true" else Builder
"false"
  where
    op2 :: Builder -> Expr a -> Expr a -> Builder
op2 Builder
op Expr a
a Expr a
b =
      let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a
          benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
b in
      Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
aenc forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"



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


-- | Stores a region of src into dst
copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder
copySlice :: Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Builder -> Builder -> Builder
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset size :: Expr 'EWord
size@(Lit W256
_) Builder
src Builder
dst
  | Expr 'EWord
size forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Builder
dst
  | Bool
otherwise =
    let size' :: Expr 'EWord
size' = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.sub Expr 'EWord
size (W256 -> Expr 'EWord
Lit W256
1))
        encDstOff :: Builder
encDstOff = forall (a :: EType). Expr a -> Builder
exprToSMT (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
dstOffset Expr 'EWord
size')
        encSrcOff :: Builder
encSrcOff = forall (a :: EType). Expr a -> Builder
exprToSMT (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
srcOffset Expr 'EWord
size')
        child :: Builder
child = Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Builder -> Builder -> Builder
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset Expr 'EWord
size' Builder
src Builder
dst in
    Builder
"(store " forall a. Semigroup a => a -> a -> a
<> Builder
child Builder -> Builder -> Builder
`sp` Builder
encDstOff Builder -> Builder -> Builder
`sp` Builder
"(select " forall a. Semigroup a => a -> a -> a
<> Builder
src Builder -> Builder -> Builder
`sp` Builder
encSrcOff forall a. Semigroup a => a -> a -> a
<> Builder
"))"
copySlice Expr 'EWord
_ Expr 'EWord
_ Expr 'EWord
_ Builder
_ Builder
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: implement copySlice with a symbolically sized region"

-- | Unrolls an exponentiation into a series of multiplications
expandExp :: Expr EWord -> W256 -> Builder
expandExp :: Expr 'EWord -> W256 -> Builder
expandExp Expr 'EWord
base W256
expnt
  | W256
expnt forall a. Eq a => a -> a -> Bool
== W256
1 = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
base
  | Bool
otherwise =
    let b :: Builder
b = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
base
        n :: Builder
n = Expr 'EWord -> W256 -> Builder
expandExp Expr 'EWord
base (W256
expnt forall a. Num a => a -> a -> a
- W256
1) in
    Builder
"(bvmul " forall a. Semigroup a => a -> a -> a
<> Builder
b Builder -> Builder -> Builder
`sp` Builder
n forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | Concatenates a list of bytes into a larger bitvector
concatBytes :: [Expr Byte] -> Builder
concatBytes :: [Expr 'Byte] -> Builder
concatBytes [Expr 'Byte]
bytes =
  let bytesRev :: [Expr 'Byte]
bytesRev = forall a. [a] -> [a]
reverse [Expr 'Byte]
bytes
      a2 :: Builder
a2 = forall (a :: EType). Expr a -> Builder
exprToSMT (forall a. [a] -> a
head [Expr 'Byte]
bytesRev) in
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall {a :: EType}. Builder -> Expr a -> Builder
wrap Builder
a2 forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
tail [Expr 'Byte]
bytesRev
  where
    wrap :: Builder -> Expr a -> Builder
wrap Builder
inner Expr a
byte =
      let byteSMT :: Builder
byteSMT = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
byte in
      Builder
"(concat " forall a. Semigroup a => a -> a -> a
<> Builder
byteSMT Builder -> Builder -> Builder
`sp` Builder
inner forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | Concatenates a list of bytes into a larger bitvector
writeBytes :: ByteString -> Expr Buf -> Builder
writeBytes :: ByteString -> Expr 'Buf -> Builder
writeBytes ByteString
bytes Expr 'Buf
buf = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. (a -> Word8 -> a) -> a -> ByteString -> a
BS.foldl' (Int, Builder) -> Word8 -> (Int, Builder)
wrap (Int
0, forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
buf) ByteString
bytes
  where
    -- we don't need to store zeros if the base buffer is empty
    skipZeros :: Bool
skipZeros = Expr 'Buf
buf forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty
    wrap :: (Int, Builder) -> Word8 -> (Int, Builder)
    wrap :: (Int, Builder) -> Word8 -> (Int, Builder)
wrap (Int
idx, Builder
inner) Word8
byte =
      if Bool
skipZeros Bool -> Bool -> Bool
&& Word8
byte forall a. Eq a => a -> a -> Bool
== Word8
0
      then (Int
idx forall a. Num a => a -> a -> a
+ Int
1, Builder
inner)
      else let
          byteSMT :: Builder
byteSMT = forall (a :: EType). Expr a -> Builder
exprToSMT (Word8 -> Expr 'Byte
LitByte Word8
byte)
          idxSMT :: Builder
idxSMT = forall (a :: EType). Expr a -> Builder
exprToSMT forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ Int
idx
        in (Int
idx forall a. Num a => a -> a -> a
+ Int
1, Builder
"(store " forall a. Semigroup a => a -> a -> a
<> Builder
inner Builder -> Builder -> Builder
`sp` Builder
idxSMT Builder -> Builder -> Builder
`sp` Builder
byteSMT forall a. Semigroup a => a -> a -> a
<> Builder
")")

encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder
encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder
encodeConcreteStore Map W256 (Map W256 W256)
s = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Builder -> (W256, W256, W256) -> Builder
encodeWrite Builder
"emptyStore" [(W256, W256, W256)]
writes
  where
    asList :: [(W256, [(W256, W256)])]
asList = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall k a. Map k a -> [(k, a)]
Map.toList) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map W256 (Map W256 W256)
s
    writes :: [(W256, W256, W256)]
writes = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(W256
addr, [(W256, W256)]
ws) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(W256
k, W256
v) -> (W256
addr, W256
k, W256
v)) [(W256, W256)]
ws) [(W256, [(W256, W256)])]
asList
    encodeWrite :: Builder -> (W256, W256, W256) -> Builder
encodeWrite Builder
prev (W256
addr, W256
key, W256
val) = let
        encAddr :: Builder
encAddr = forall (a :: EType). Expr a -> Builder
exprToSMT (W256 -> Expr 'EWord
Lit W256
addr)
        encKey :: Builder
encKey = forall (a :: EType). Expr a -> Builder
exprToSMT (W256 -> Expr 'EWord
Lit W256
key)
        encVal :: Builder
encVal = forall (a :: EType). Expr a -> Builder
exprToSMT (W256 -> Expr 'EWord
Lit W256
val)
      in Builder
"(sstore " forall a. Semigroup a => a -> a -> a
<> Builder
encAddr Builder -> Builder -> Builder
`sp` Builder
encKey Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
`sp` Builder
prev forall a. Semigroup a => a -> a -> a
<> Builder
")"


-- ** Cex parsing ** --------------------------------------------------------------------------------


parseW256 :: SpecConstant -> W256
parseW256 :: SpecConstant -> W256
parseW256 = forall a. (Num a, Eq a) => SpecConstant -> a
parseSC

parseInteger :: SpecConstant -> Integer
parseInteger :: SpecConstant -> Integer
parseInteger = forall a. (Num a, Eq a) => SpecConstant -> a
parseSC

parseW8 :: SpecConstant -> Word8
parseW8 :: SpecConstant -> Word8
parseW8 = forall a. (Num a, Eq a) => SpecConstant -> a
parseSC

parseSC :: (Num a, Eq a) => SpecConstant -> a
parseSC :: forall a. (Num a, Eq a) => SpecConstant -> a
parseSC (SCHexadecimal Text
a) = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Num a) => ReadS a
Numeric.readHex forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
T.fromStrict forall a b. (a -> b) -> a -> b
$ Text
a
parseSC (SCBinary Text
a) = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Num a) => ReadS a
Numeric.readBin forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
T.fromStrict forall a b. (a -> b) -> a -> b
$ Text
a
parseSC SpecConstant
sc = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: cannot parse: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show SpecConstant
sc

parseErr :: (Show a) => a -> b
parseErr :: forall a b. Show a => a -> b
parseErr a
res = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: cannot parse solver response: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show a
res

parseVar :: TS.Text -> Expr EWord
parseVar :: Text -> Expr 'EWord
parseVar = Text -> Expr 'EWord
Var

parseBlockCtx :: TS.Text -> Expr EWord
parseBlockCtx :: Text -> Expr 'EWord
parseBlockCtx Text
"origin" = Expr 'EWord
Origin
parseBlockCtx Text
"coinbase" = Expr 'EWord
Coinbase
parseBlockCtx Text
"timestamp" = Expr 'EWord
Timestamp
parseBlockCtx Text
"blocknumber" = Expr 'EWord
BlockNumber
parseBlockCtx Text
"prevrandao" = Expr 'EWord
PrevRandao
parseBlockCtx Text
"gaslimit" = Expr 'EWord
GasLimit
parseBlockCtx Text
"chainid" = Expr 'EWord
ChainId
parseBlockCtx Text
"basefee" = Expr 'EWord
BaseFee
parseBlockCtx Text
t = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: cannot parse " forall a. Semigroup a => a -> a -> a
<> (Text -> [Char]
TS.unpack Text
t) forall a. Semigroup a => a -> a -> a
<> [Char]
" into an Expr"

parseFrameCtx :: TS.Text -> Expr EWord
parseFrameCtx :: Text -> Expr 'EWord
parseFrameCtx Text
name = case Text -> [Char]
TS.unpack Text
name of
  (Char
'c':Char
'a':Char
'l':Char
'l':Char
'v':Char
'a':Char
'l':Char
'u':Char
'e':Char
'_':[Char]
frame) -> Int -> Expr 'EWord
CallValue (forall a. Read a => [Char] -> a
read [Char]
frame)
  (Char
'c':Char
'a':Char
'l':Char
'l':Char
'e':Char
'r':Char
'_':[Char]
frame) -> Int -> Expr 'EWord
Caller (forall a. Read a => [Char] -> a
read [Char]
frame)
  (Char
'a':Char
'd':Char
'd':Char
'r':Char
'e':Char
's':Char
's':Char
'_':[Char]
frame) -> Int -> Expr 'EWord
Address (forall a. Read a => [Char] -> a
read [Char]
frame)
  [Char]
t -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: cannot parse " forall a. Semigroup a => a -> a -> a
<> [Char]
t forall a. Semigroup a => a -> a -> a
<> [Char]
" into an Expr"

getVars :: (TS.Text -> Expr EWord) -> (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr EWord) W256)
getVars :: (Text -> Expr 'EWord)
-> (Text -> IO Text) -> [Text] -> IO (Map (Expr 'EWord) W256)
getVars Text -> Expr 'EWord
parseFn Text -> IO Text
getVal [Text]
names = forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Text -> Expr 'EWord
parseFn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Text W256 -> Text -> IO (Map Text W256)
getOne forall a. Monoid a => a
mempty [Text]
names
  where
    getOne :: Map TS.Text W256 -> TS.Text -> IO (Map TS.Text W256)
    getOne :: Map Text W256 -> Text -> IO (Map Text W256)
getOne Map Text W256
acc Text
name = do
      Text
raw <- Text -> IO Text
getVal (Text -> Text
T.fromStrict Text
name)
      let
        parsed :: ValuationPair
parsed = case forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
raw) of
          Right (ResSpecific (ValuationPair
valParsed :| [])) -> ValuationPair
valParsed
          Either Text GetValueRes
r -> forall a b. Show a => a -> b
parseErr Either Text GetValueRes
r
        val :: W256
val = case ValuationPair
parsed of
          (TermQualIdentifier (
            Unqualified (IdSymbol Text
symbol)),
            TermSpecConstant SpecConstant
sc)
              -> if Text
symbol forall a. Eq a => a -> a -> Bool
== Text
name
                 then SpecConstant -> W256
parseW256 SpecConstant
sc
                 else forall a. HasCallStack => [Char] -> a
error [Char]
"Internal Error: solver did not return model for requested value"
          ValuationPair
r -> forall a b. Show a => a -> b
parseErr ValuationPair
r
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name W256
val Map Text W256
acc

-- | Queries the solver for models for each of the expressions representing the
-- max read index for a given buffer
queryMaxReads :: (Text -> IO Text) -> Map Text (Expr EWord)  -> IO (Map Text W256)
queryMaxReads :: (Text -> IO Text) -> Map Text (Expr 'EWord) -> IO (Map Text W256)
queryMaxReads Text -> IO Text
getVal Map Text (Expr 'EWord)
maxReads = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Text -> IO Text) -> Expr 'EWord -> IO W256
queryValue Text -> IO Text
getVal) Map Text (Expr 'EWord)
maxReads

-- | Gets the initial model for each buffer, these will often be much too large for our purposes
getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr Buf) BufModel)
getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr 'Buf) BufModel)
getBufs Text -> IO Text
getVal [Text]
bufs = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map (Expr 'Buf) BufModel -> Text -> IO (Map (Expr 'Buf) BufModel)
getBuf forall a. Monoid a => a
mempty [Text]
bufs
  where
    getLength :: Text -> IO W256
    getLength :: Text -> IO W256
getLength Text
name = do
      Text
val <- Text -> IO Text
getVal (Text
name forall a. Semigroup a => a -> a -> a
<> Text
"_length ")
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
val) of
        Right (ResSpecific (ValuationPair
parsed :| [])) -> case ValuationPair
parsed of
          (TermQualIdentifier (Unqualified (IdSymbol Text
symbol)), (TermSpecConstant SpecConstant
sc))
            -> if Text
symbol forall a. Eq a => a -> a -> Bool
== (Text -> Text
T.toStrict forall a b. (a -> b) -> a -> b
$ Text
name forall a. Semigroup a => a -> a -> a
<> Text
"_length")
               then SpecConstant -> W256
parseW256 SpecConstant
sc
               else forall a. HasCallStack => [Char] -> a
error [Char]
"Internal Error: solver did not return model for requested value"
          ValuationPair
res -> forall a b. Show a => a -> b
parseErr ValuationPair
res
        Either Text GetValueRes
res -> forall a b. Show a => a -> b
parseErr Either Text GetValueRes
res

    getBuf :: Map (Expr Buf) BufModel -> Text -> IO (Map (Expr Buf) BufModel)
    getBuf :: Map (Expr 'Buf) BufModel -> Text -> IO (Map (Expr 'Buf) BufModel)
getBuf Map (Expr 'Buf) BufModel
acc Text
name = do
      W256
len <- Text -> IO W256
getLength Text
name
      Text
val <- Text -> IO Text
getVal Text
name

      BufModel
buf <- case forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
val) of
        Right (ResSpecific (ValuationPair
valParsed :| [])) -> case ValuationPair
valParsed of
          (TermQualIdentifier (Unqualified (IdSymbol Text
symbol)), Term
term)
            -> if (Text -> Text
T.fromStrict Text
symbol) forall a. Eq a => a -> a -> Bool
== Text
name
               then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ W256 -> Term -> BufModel
parseBuf W256
len Term
term
               else forall a. HasCallStack => [Char] -> a
error [Char]
"Internal Error: solver did not return model for requested value"
          ValuationPair
res -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: cannot parse solver response: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show ValuationPair
res
        Either Text GetValueRes
res -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: cannot parse solver response: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show Either Text GetValueRes
res
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Text -> Expr 'Buf
AbstractBuf forall a b. (a -> b) -> a -> b
$ Text -> Text
T.toStrict Text
name) BufModel
buf Map (Expr 'Buf) BufModel
acc

    parseBuf :: W256 -> Term -> BufModel
    parseBuf :: W256 -> Term -> BufModel
parseBuf W256
len = CompressedBuf -> BufModel
Comp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Text CompressedBuf -> Term -> CompressedBuf
go forall a. Monoid a => a
mempty
      where
        go :: Map Text CompressedBuf -> Term -> CompressedBuf
go Map Text CompressedBuf
env = \case
          -- constant arrays
          (TermApplication (
            Qualified (IdSymbol Text
"const") (
              SortParameter (IdSymbol Text
"Array") (
                SortSymbol (IdIndexed Text
"BitVec" (IxNumeral Text
"256" :| []))
                :| [SortSymbol (IdIndexed Text
"BitVec" (IxNumeral Text
"8" :| []))]
              )
            )) ((TermSpecConstant SpecConstant
val :| [])))
            -> case SpecConstant
val of
                 SCHexadecimal Text
"00" -> Word8 -> W256 -> CompressedBuf
Base Word8
0 W256
0
                 SpecConstant
v -> Word8 -> W256 -> CompressedBuf
Base (SpecConstant -> Word8
parseW8 SpecConstant
v) W256
len

          -- writing a byte over some array
          (TermApplication
            (Unqualified (IdSymbol Text
"store"))
            (Term
base :| [TermSpecConstant SpecConstant
idx, TermSpecConstant SpecConstant
val])
            ) -> let
              pbase :: CompressedBuf
pbase = Map Text CompressedBuf -> Term -> CompressedBuf
go Map Text CompressedBuf
env Term
base
              pidx :: W256
pidx = SpecConstant -> W256
parseW256 SpecConstant
idx
              pval :: Word8
pval = SpecConstant -> Word8
parseW8 SpecConstant
val
            in Word8 -> W256 -> CompressedBuf -> CompressedBuf
Write Word8
pval W256
pidx CompressedBuf
pbase

          -- binding a new name
          (TermLet ((VarBinding Text
name Term
bound) :| []) Term
term) -> let
              pbound :: CompressedBuf
pbound = Map Text CompressedBuf -> Term -> CompressedBuf
go Map Text CompressedBuf
env Term
bound
            in Map Text CompressedBuf -> Term -> CompressedBuf
go (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name CompressedBuf
pbound Map Text CompressedBuf
env) Term
term

          -- looking up a bound name
          (TermQualIdentifier (Unqualified (IdSymbol Text
name))) -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
name Map Text CompressedBuf
env of
            Just CompressedBuf
t -> CompressedBuf
t
            Maybe CompressedBuf
Nothing -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal error: could not find "
                            forall a. Semigroup a => a -> a -> a
<> (Text -> [Char]
TS.unpack Text
name)
                            forall a. Semigroup a => a -> a -> a
<> [Char]
" in environment mapping"
          Term
p -> forall a b. Show a => a -> b
parseErr Term
p

getStore :: (Text -> IO Text) -> [(Expr EWord, Expr EWord)] -> IO (Map W256 (Map W256 W256))
getStore :: (Text -> IO Text)
-> [(Expr 'EWord, Expr 'EWord)] -> IO (Map W256 (Map W256 W256))
getStore Text -> IO Text
getVal [(Expr 'EWord, Expr 'EWord)]
sreads = do
  Text
raw <- Text -> IO Text
getVal Text
"abstractStore"
  let parsed :: ValuationPair
parsed = case forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
raw) of
                 Right (ResSpecific (ValuationPair
valParsed :| [])) -> ValuationPair
valParsed
                 Either Text GetValueRes
r -> forall a b. Show a => a -> b
parseErr Either Text GetValueRes
r
      -- first interpret SMT term as a function
      fun :: W256 -> W256 -> W256
fun = case ValuationPair
parsed of
              (TermQualIdentifier (Unqualified (IdSymbol Text
symbol)), Term
term) ->
                if Text
symbol forall a. Eq a => a -> a -> Bool
== Text
"abstractStore"
                then Map Text Term -> Term -> W256 -> W256 -> W256
interpret2DArray forall k a. Map k a
Map.empty Term
term
                else forall a. HasCallStack => [Char] -> a
error [Char]
"Internal Error: solver did not return model for requested value"
              ValuationPair
r -> forall a b. Show a => a -> b
parseErr ValuationPair
r

  -- then create a map by adding only the locations that are read by the program
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Map W256 (Map W256 W256)
m (Expr 'EWord
addr, Expr 'EWord
slot) -> do
            W256
addr' <- (Text -> IO Text) -> Expr 'EWord -> IO W256
queryValue Text -> IO Text
getVal Expr 'EWord
addr
            W256
slot' <- (Text -> IO Text) -> Expr 'EWord -> IO W256
queryValue Text -> IO Text
getVal Expr 'EWord
slot
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ W256
-> W256
-> Map W256 (Map W256 W256)
-> (W256 -> W256 -> W256)
-> Map W256 (Map W256 W256)
addElem W256
addr' W256
slot' Map W256 (Map W256 W256)
m W256 -> W256 -> W256
fun) forall k a. Map k a
Map.empty [(Expr 'EWord, Expr 'EWord)]
sreads

  where

    addElem :: W256 -> W256 -> Map W256 (Map W256 W256) -> (W256 -> W256 -> W256) -> Map W256 (Map W256 W256)
    addElem :: W256
-> W256
-> Map W256 (Map W256 W256)
-> (W256 -> W256 -> W256)
-> Map W256 (Map W256 W256)
addElem W256
addr W256
slot Map W256 (Map W256 W256)
store W256 -> W256 -> W256
fun =
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup W256
addr Map W256 (Map W256 W256)
store of
        Just Map W256 W256
m -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert W256
addr (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert W256
slot (W256 -> W256 -> W256
fun W256
addr W256
slot) Map W256 W256
m) Map W256 (Map W256 W256)
store
        Maybe (Map W256 W256)
Nothing -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert W256
addr (forall k a. k -> a -> Map k a
Map.singleton W256
slot (W256 -> W256 -> W256
fun W256
addr W256
slot)) Map W256 (Map W256 W256)
store


queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256
queryValue :: (Text -> IO Text) -> Expr 'EWord -> IO W256
queryValue Text -> IO Text
_ (Lit W256
w) = forall (f :: * -> *) a. Applicative f => a -> f a
pure W256
w
queryValue Text -> IO Text
getVal Expr 'EWord
w = do
  let expr :: Text
expr = Builder -> Text
toLazyText forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
w
  Text
raw <- Text -> IO Text
getVal Text
expr
  case forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
raw) of
    Right (ResSpecific (ValuationPair
valParsed :| [])) ->
      case ValuationPair
valParsed of
        (Term
_, TermSpecConstant SpecConstant
sc) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SpecConstant -> W256
parseW256 SpecConstant
sc
        ValuationPair
_ -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: cannot parse model for: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show Expr 'EWord
w
    Either Text GetValueRes
r -> forall a b. Show a => a -> b
parseErr Either Text GetValueRes
r



-- | Interpret an N-dimensional array as a value of type a.
-- Parameterized by an interpretation function for array values.
interpretNDArray :: (Map Symbol Term -> Term -> a) -> (Map Symbol Term) -> Term -> (W256 -> a)
interpretNDArray :: forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> a
interp Map Text Term
env = \case
  -- variable reference
  TermQualIdentifier (Unqualified (IdSymbol Text
s)) ->
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
s Map Text Term
env of
      Just Term
t -> forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> a
interp Map Text Term
env Term
t
      Maybe Term
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: unknown identifier, cannot parse array"
  -- (let (x t') t)
  TermLet (VarBinding Text
x Term
t' :| []) Term
t -> forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> a
interp (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
x Term
t' Map Text Term
env) Term
t
  TermLet (VarBinding Text
x Term
t' :| [VarBinding]
lets) Term
t -> forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> a
interp (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
x Term
t' Map Text Term
env) (NonEmpty VarBinding -> Term -> Term
TermLet (forall a. [a] -> NonEmpty a
NonEmpty.fromList [VarBinding]
lets) Term
t)
  -- (as const (Array (_ BitVec 256) (_ BitVec 256))) SpecConstant
  TermApplication QualIdentifier
asconst (Term
val :| []) | QualIdentifier -> Bool
isArrConst QualIdentifier
asconst ->
    \W256
_ -> Map Text Term -> Term -> a
interp Map Text Term
env Term
val
  -- (store arr ind val)
  TermApplication QualIdentifier
store (Term
arr :| [TermSpecConstant SpecConstant
ind, Term
val]) | QualIdentifier -> Bool
isStore QualIdentifier
store ->
    \W256
x -> if W256
x forall a. Eq a => a -> a -> Bool
== SpecConstant -> W256
parseW256 SpecConstant
ind then Map Text Term -> Term -> a
interp Map Text Term
env Term
val else forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> a
interp Map Text Term
env Term
arr W256
x
  Term
t -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal error: cannot parse array value. Unexpected term: " forall a. Semigroup a => a -> a -> a
<> (forall a. Show a => a -> [Char]
show Term
t)

  where
    isArrConst :: QualIdentifier -> Bool
    isArrConst :: QualIdentifier -> Bool
isArrConst = \case
      Qualified (IdSymbol Text
"const") (SortParameter (IdSymbol Text
"Array") NonEmpty Sort
_) -> Bool
True
      QualIdentifier
_ -> Bool
False

    isStore :: QualIdentifier -> Bool
    isStore :: QualIdentifier -> Bool
isStore QualIdentifier
t = QualIdentifier
t forall a. Eq a => a -> a -> Bool
== Identifier -> QualIdentifier
Unqualified (Text -> Identifier
IdSymbol Text
"store")


-- | Interpret an 1-dimensional array as a function
interpret1DArray :: (Map Symbol Term) -> Term -> (W256 -> W256)
interpret1DArray :: Map Text Term -> Term -> W256 -> W256
interpret1DArray = forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> W256
interpretW256
  where
    interpretW256 :: (Map Symbol Term) -> Term -> W256
    interpretW256 :: Map Text Term -> Term -> W256
interpretW256 Map Text Term
_ (TermSpecConstant SpecConstant
val) = SpecConstant -> W256
parseW256 SpecConstant
val
    interpretW256 Map Text Term
env (TermQualIdentifier (Unqualified (IdSymbol Text
s))) =
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
s Map Text Term
env of
        Just Term
t -> Map Text Term -> Term -> W256
interpretW256 Map Text Term
env Term
t
        Maybe Term
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: unknown identifier, cannot parse array"
    interpretW256 Map Text Term
_ Term
t = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal error: cannot parse array value. Unexpected term: " forall a. Semigroup a => a -> a -> a
<> (forall a. Show a => a -> [Char]
show Term
t)

-- | Interpret an 2-dimensional array as a function
interpret2DArray :: (Map Symbol Term) -> Term -> (W256 -> W256 -> W256)
interpret2DArray :: Map Text Term -> Term -> W256 -> W256 -> W256
interpret2DArray = forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> W256 -> W256
interpret1DArray