{-# 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 Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Data.List qualified as List
import Data.List.NonEmpty (NonEmpty((:|)))
import Data.List.NonEmpty qualified as NonEmpty
import Data.String.Here
import Data.Maybe (fromJust, fromMaybe, isJust)
import Data.Either.Extra (fromRight')
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Word (Word8)
import Data.Text.Lazy (Text)
import Data.Text qualified as TS
import Data.Text.Lazy qualified as T
import Data.Text.Lazy.Builder
import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)
import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))
import Numeric (readHex, readBin)
import Witch (into, unsafeInto)
import EVM.Format (formatProp)

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


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


-- | Data that we need to construct a nice counterexample
data CexVars = CexVars
  { -- | variable names that we need models for to reconstruct calldata
    CexVars -> [Text]
calldata     :: [Text]
    -- | symbolic address names
  , CexVars -> [Text]
addrs        :: [Text]
    -- | buffer names and guesses at their maximum size
  , CexVars -> Map Text (Expr 'EWord)
buffers      :: Map Text (Expr EWord)
    -- | reads from abstract storage
  , CexVars -> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
storeReads   :: Map (Expr EAddr, Maybe W256) (Set (Expr EWord))
    -- | the names of any block context variables
  , CexVars -> [Text]
blockContext :: [Text]
    -- | the names of any tx context variables
  , CexVars -> [Text]
txContext    :: [Text]
  }
  deriving (CexVars -> CexVars -> Bool
(CexVars -> CexVars -> Bool)
-> (CexVars -> CexVars -> Bool) -> Eq CexVars
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CexVars -> CexVars -> Bool
== :: CexVars -> CexVars -> Bool
$c/= :: CexVars -> CexVars -> Bool
/= :: CexVars -> CexVars -> Bool
Eq, Int -> CexVars -> ShowS
[CexVars] -> ShowS
CexVars -> [Char]
(Int -> CexVars -> ShowS)
-> (CexVars -> [Char]) -> ([CexVars] -> ShowS) -> Show CexVars
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CexVars -> ShowS
showsPrec :: Int -> CexVars -> ShowS
$cshow :: CexVars -> [Char]
show :: CexVars -> [Char]
$cshowList :: [CexVars] -> ShowS
showList :: [CexVars] -> ShowS
Show)

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

instance Monoid CexVars where
    mempty :: CexVars
mempty = CexVars
      { $sel:calldata:CexVars :: [Text]
calldata = [Text]
forall a. Monoid a => a
mempty
      , $sel:addrs:CexVars :: [Text]
addrs = [Text]
forall a. Monoid a => a
mempty
      , $sel:buffers:CexVars :: Map Text (Expr 'EWord)
buffers = Map Text (Expr 'EWord)
forall a. Monoid a => a
mempty
      , $sel:storeReads:CexVars :: Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
storeReads = Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
forall a. Monoid a => a
mempty
      , $sel:blockContext:CexVars :: [Text]
blockContext = [Text]
forall a. Monoid a => a
mempty
      , $sel:txContext:CexVars :: [Text]
txContext = [Text]
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
(BufModel -> BufModel -> Bool)
-> (BufModel -> BufModel -> Bool) -> Eq BufModel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BufModel -> BufModel -> Bool
== :: BufModel -> BufModel -> Bool
$c/= :: BufModel -> BufModel -> Bool
/= :: BufModel -> BufModel -> Bool
Eq, Int -> BufModel -> ShowS
[BufModel] -> ShowS
BufModel -> [Char]
(Int -> BufModel -> ShowS)
-> (BufModel -> [Char]) -> ([BufModel] -> ShowS) -> Show BufModel
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BufModel -> ShowS
showsPrec :: Int -> BufModel -> ShowS
$cshow :: BufModel -> [Char]
show :: BufModel -> [Char]
$cshowList :: [BufModel] -> ShowS
showList :: [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
(CompressedBuf -> CompressedBuf -> Bool)
-> (CompressedBuf -> CompressedBuf -> Bool) -> Eq CompressedBuf
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CompressedBuf -> CompressedBuf -> Bool
== :: CompressedBuf -> CompressedBuf -> Bool
$c/= :: CompressedBuf -> CompressedBuf -> Bool
/= :: CompressedBuf -> CompressedBuf -> Bool
Eq, Int -> CompressedBuf -> ShowS
[CompressedBuf] -> ShowS
CompressedBuf -> [Char]
(Int -> CompressedBuf -> ShowS)
-> (CompressedBuf -> [Char])
-> ([CompressedBuf] -> ShowS)
-> Show CompressedBuf
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CompressedBuf -> ShowS
showsPrec :: Int -> CompressedBuf -> ShowS
$cshow :: CompressedBuf -> [Char]
show :: CompressedBuf -> [Char]
$cshowList :: [CompressedBuf] -> ShowS
showList :: [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 'EAddr) Addr
addrs :: Map (Expr EAddr) Addr
  , SMTCex -> Map (Expr 'Buf) BufModel
buffers :: Map (Expr Buf) BufModel
  , SMTCex -> Map (Expr 'EAddr) (Map W256 W256)
store :: Map (Expr EAddr) (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
(SMTCex -> SMTCex -> Bool)
-> (SMTCex -> SMTCex -> Bool) -> Eq SMTCex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SMTCex -> SMTCex -> Bool
== :: SMTCex -> SMTCex -> Bool
$c/= :: SMTCex -> SMTCex -> Bool
/= :: SMTCex -> SMTCex -> Bool
Eq, Int -> SMTCex -> ShowS
[SMTCex] -> ShowS
SMTCex -> [Char]
(Int -> SMTCex -> ShowS)
-> (SMTCex -> [Char]) -> ([SMTCex] -> ShowS) -> Show SMTCex
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SMTCex -> ShowS
showsPrec :: Int -> SMTCex -> ShowS
$cshow :: SMTCex -> [Char]
show :: SMTCex -> [Char]
$cshowList :: [SMTCex] -> ShowS
showList :: [SMTCex] -> ShowS
Show)

instance Semigroup SMTCex where
  SMTCex
a <> :: SMTCex -> SMTCex -> SMTCex
<> SMTCex
b = SMTCex
    { $sel:vars:SMTCex :: Map (Expr 'EWord) W256
vars = SMTCex
a.vars Map (Expr 'EWord) W256
-> Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
forall a. Semigroup a => a -> a -> a
<> SMTCex
b.vars
    , $sel:addrs:SMTCex :: Map (Expr 'EAddr) Addr
addrs = SMTCex
a.addrs Map (Expr 'EAddr) Addr
-> Map (Expr 'EAddr) Addr -> Map (Expr 'EAddr) Addr
forall a. Semigroup a => a -> a -> a
<> SMTCex
b.addrs
    , $sel:buffers:SMTCex :: Map (Expr 'Buf) BufModel
buffers = SMTCex
a.buffers Map (Expr 'Buf) BufModel
-> Map (Expr 'Buf) BufModel -> Map (Expr 'Buf) BufModel
forall a. Semigroup a => a -> a -> a
<> SMTCex
b.buffers
    , $sel:store:SMTCex :: Map (Expr 'EAddr) (Map W256 W256)
store = SMTCex
a.store Map (Expr 'EAddr) (Map W256 W256)
-> Map (Expr 'EAddr) (Map W256 W256)
-> Map (Expr 'EAddr) (Map W256 W256)
forall a. Semigroup a => a -> a -> a
<> SMTCex
b.store
    , $sel:blockContext:SMTCex :: Map (Expr 'EWord) W256
blockContext = SMTCex
a.blockContext Map (Expr 'EWord) W256
-> Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
forall a. Semigroup a => a -> a -> a
<> SMTCex
b.blockContext
    , $sel:txContext:SMTCex :: Map (Expr 'EWord) W256
txContext = SMTCex
a.txContext Map (Expr 'EWord) W256
-> Map (Expr 'EWord) W256 -> Map (Expr 'EWord) W256
forall a. Semigroup a => a -> a -> a
<> SMTCex
b.txContext
    }

instance Monoid SMTCex where
  mempty :: SMTCex
mempty = SMTCex
    { $sel:vars:SMTCex :: Map (Expr 'EWord) W256
vars = Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty
    , $sel:addrs:SMTCex :: Map (Expr 'EAddr) Addr
addrs = Map (Expr 'EAddr) Addr
forall a. Monoid a => a
mempty
    , $sel:buffers:SMTCex :: Map (Expr 'Buf) BufModel
buffers = Map (Expr 'Buf) BufModel
forall a. Monoid a => a
mempty
    , $sel:store:SMTCex :: Map (Expr 'EAddr) (Map W256 W256)
store = Map (Expr 'EAddr) (Map W256 W256)
forall a. Monoid a => a
mempty
    , $sel:blockContext:SMTCex :: Map (Expr 'EWord) W256
blockContext = Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty
    , $sel:txContext:SMTCex :: Map (Expr 'EWord) W256
txContext = Map (Expr 'EWord) W256
forall a. Monoid a => a
mempty
    }

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

-- | Attempts 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) -> BufModel -> Maybe BufModel
forall a. a -> Maybe a
Just (BufModel -> Maybe BufModel) -> BufModel -> Maybe BufModel
forall a b. (a -> b) -> a -> b
$ ByteString -> BufModel
Flat ByteString
b
  Maybe (Expr 'Buf)
_ -> Maybe BufModel
forall a. Maybe a
Nothing
  where
    toBuf :: BufModel -> Maybe (Expr 'Buf)
toBuf (Comp (Base Word8
b W256
sz)) | W256
sz W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
<= W256
120_000_000 = Expr 'Buf -> Maybe (Expr 'Buf)
forall a. a -> Maybe a
Just (Expr 'Buf -> Maybe (Expr 'Buf))
-> (ByteString -> Expr 'Buf) -> ByteString -> Maybe (Expr 'Buf)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Maybe (Expr 'Buf))
-> ByteString -> Maybe (Expr 'Buf)
forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate (W256 -> Int
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto W256
sz) Word8
b
    toBuf (Comp (Write Word8
b W256
idx CompressedBuf
next)) = (Expr 'Buf -> Expr 'Buf) -> Maybe (Expr 'Buf) -> Maybe (Expr 'Buf)
forall a b. (a -> b) -> Maybe a -> Maybe b
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 (BufModel -> Maybe (Expr 'Buf)) -> BufModel -> Maybe (Expr 'Buf)
forall a b. (a -> b) -> a -> b
$ CompressedBuf -> BufModel
Comp CompressedBuf
next)
    toBuf (Flat ByteString
b) = Expr 'Buf -> Maybe (Expr 'Buf)
forall a. a -> Maybe a
Just (Expr 'Buf -> Maybe (Expr 'Buf))
-> (ByteString -> Expr 'Buf) -> ByteString -> Maybe (Expr 'Buf)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Expr 'Buf
ConcreteBuf (ByteString -> Maybe (Expr 'Buf))
-> ByteString -> Maybe (Expr 'Buf)
forall a b. (a -> b) -> a -> b
$ ByteString
b
    toBuf BufModel
_ = Maybe (Expr 'Buf)
forall a. Maybe a
Nothing

getVar :: SMTCex -> TS.Text -> W256
getVar :: SMTCex -> Text -> W256
getVar SMTCex
cex Text
name = Maybe W256 -> W256
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe W256 -> W256) -> Maybe W256 -> W256
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Map (Expr 'EWord) W256 -> Maybe W256
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 [Prop]
  deriving (SMT2 -> SMT2 -> Bool
(SMT2 -> SMT2 -> Bool) -> (SMT2 -> SMT2 -> Bool) -> Eq SMT2
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SMT2 -> SMT2 -> Bool
== :: SMT2 -> SMT2 -> Bool
$c/= :: SMT2 -> SMT2 -> Bool
/= :: SMT2 -> SMT2 -> Bool
Eq, Int -> SMT2 -> ShowS
[SMT2] -> ShowS
SMT2 -> [Char]
(Int -> SMT2 -> ShowS)
-> (SMT2 -> [Char]) -> ([SMT2] -> ShowS) -> Show SMT2
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SMT2 -> ShowS
showsPrec :: Int -> SMT2 -> ShowS
$cshow :: SMT2 -> [Char]
show :: SMT2 -> [Char]
$cshowList :: [SMT2] -> ShowS
showList :: [SMT2] -> ShowS
Show)

instance Semigroup SMT2 where
  (SMT2 [Builder]
a CexVars
c [Prop]
d) <> :: SMT2 -> SMT2 -> SMT2
<> (SMT2 [Builder]
a2 CexVars
c2 [Prop]
d2) = [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 ([Builder]
a [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> [Builder]
a2) (CexVars
c CexVars -> CexVars -> CexVars
forall a. Semigroup a => a -> a -> a
<> CexVars
c2) ([Prop]
d [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
d2)

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

formatSMT2 :: SMT2 -> Text
formatSMT2 :: SMT2 -> Text
formatSMT2 (SMT2 [Builder]
ls CexVars
_ [Prop]
ps) = Text
expr Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
smt2
 where
 expr :: Text
expr = [Text] -> Text
T.concat [Char -> Text
T.singleton Char
';', HasCallStack => Text -> Text -> Text -> Text
Text -> Text -> Text -> Text
T.replace Text
"\n" Text
"\n;" (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
T.pack ([Char] -> Text) -> (Text -> [Char]) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
TS.unpack (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$  [Text] -> Text
TS.unlines ((Prop -> Text) -> [Prop] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> Text
formatProp [Prop]
ps)]
 smt2 :: Text
smt2 = [Text] -> Text
T.unlines ((Builder -> Text) -> [Builder] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
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 -> Err SMT2
declareIntermediates :: BufEnv -> StoreEnv -> Either [Char] SMT2
declareIntermediates BufEnv
bufs StoreEnv
stores = do
  let encSs :: Map Int (Either [Char] SMT2)
encSs = (Int -> Expr 'Storage -> Either [Char] SMT2)
-> StoreEnv -> Map Int (Either [Char] SMT2)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey Int -> Expr 'Storage -> Either [Char] SMT2
forall {p} {a :: EType}.
Show p =>
p -> Expr a -> Either [Char] SMT2
encodeStore StoreEnv
stores
      encBs :: Map Int (Either [Char] SMT2)
encBs = (Int -> Expr 'Buf -> Either [Char] SMT2)
-> BufEnv -> Map Int (Either [Char] SMT2)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey Int -> Expr 'Buf -> Either [Char] SMT2
encodeBuf BufEnv
bufs
      sorted :: [(Int, Either [Char] SMT2)]
sorted = ((Int, Either [Char] SMT2)
 -> (Int, Either [Char] SMT2) -> Ordering)
-> [(Int, Either [Char] SMT2)] -> [(Int, Either [Char] SMT2)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int, Either [Char] SMT2) -> (Int, Either [Char] SMT2) -> Ordering
forall {a} {b} {b}. Ord a => (a, b) -> (a, b) -> Ordering
compareFst ([(Int, Either [Char] SMT2)] -> [(Int, Either [Char] SMT2)])
-> [(Int, Either [Char] SMT2)] -> [(Int, Either [Char] SMT2)]
forall a b. (a -> b) -> a -> b
$ Map Int (Either [Char] SMT2) -> [(Int, Either [Char] SMT2)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Int (Either [Char] SMT2) -> [(Int, Either [Char] SMT2)])
-> Map Int (Either [Char] SMT2) -> [(Int, Either [Char] SMT2)]
forall a b. (a -> b) -> a -> b
$ Map Int (Either [Char] SMT2)
encSs Map Int (Either [Char] SMT2)
-> Map Int (Either [Char] SMT2) -> Map Int (Either [Char] SMT2)
forall a. Semigroup a => a -> a -> a
<> Map Int (Either [Char] SMT2)
encBs
  [SMT2]
decls <- ((Int, Either [Char] SMT2) -> Either [Char] SMT2)
-> [(Int, Either [Char] SMT2)] -> Either [Char] [SMT2]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Int, Either [Char] SMT2) -> Either [Char] SMT2
forall a b. (a, b) -> b
snd [(Int, Either [Char] SMT2)]
sorted
  let smt2 :: [SMT2]
smt2 = ([Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Text -> Builder
fromText Text
"; intermediate buffers & stores"] CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty)SMT2 -> [SMT2] -> [SMT2]
forall a. a -> [a] -> [a]
:[SMT2]
decls
  SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ (SMT2 -> SMT2 -> SMT2) -> SMT2 -> [SMT2] -> SMT2
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
(<>) SMT2
forall a. Monoid a => a
mempty [SMT2]
smt2
  where
    compareFst :: (a, b) -> (a, b) -> Ordering
compareFst (a
l, b
_) (a
r, b
_) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
l a
r
    encodeBuf :: Int -> Expr 'Buf -> Either [Char] SMT2
encodeBuf Int
n Expr 'Buf
expr = do
      Builder
buf <- Expr 'Buf -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Buf
expr
      SMT2
bufLen <- Int -> Expr 'Buf -> Either [Char] SMT2
encodeBufLen Int
n Expr 'Buf
expr
      SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder
"(define-fun buf" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ([Char] -> Builder
fromString ([Char] -> Builder) -> (Int -> [Char]) -> Int -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> Builder) -> Int -> Builder
forall a b. (a -> b) -> a -> b
$ Int
n) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"() Buf " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
buf Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")\n"]  CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> SMT2
bufLen
    encodeBufLen :: Int -> Expr 'Buf -> Either [Char] SMT2
encodeBufLen Int
n Expr 'Buf
expr = do
      Builder
bufLen <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (BufEnv -> Bool -> Expr 'Buf -> Expr 'EWord
bufLengthEnv BufEnv
bufs Bool
True Expr 'Buf
expr)
      SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder
"(define-fun buf" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ([Char] -> Builder
fromString ([Char] -> Builder) -> (Int -> [Char]) -> Int -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> Builder) -> Int -> Builder
forall a b. (a -> b) -> a -> b
$ Int
n) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
"_length () (_ BitVec 256) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bufLen Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"] CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty
    encodeStore :: p -> Expr a -> Either [Char] SMT2
encodeStore p
n Expr a
expr = do
      Builder
storage <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
expr
      SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder
"(define-fun store" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ([Char] -> Builder
fromString ([Char] -> Builder) -> (p -> [Char]) -> p -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p -> [Char]
forall a. Show a => a -> [Char]
show (p -> Builder) -> p -> Builder
forall a b. (a -> b) -> a -> b
$ p
n) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" () Storage " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
storage Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"] CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty

data AbstState = AbstState
  { AbstState -> Map (Expr 'EWord) Int
words :: Map (Expr EWord) Int
  , AbstState -> Int
count :: Int
  }
  deriving (Int -> AbstState -> ShowS
[AbstState] -> ShowS
AbstState -> [Char]
(Int -> AbstState -> ShowS)
-> (AbstState -> [Char])
-> ([AbstState] -> ShowS)
-> Show AbstState
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbstState -> ShowS
showsPrec :: Int -> AbstState -> ShowS
$cshow :: AbstState -> [Char]
show :: AbstState -> [Char]
$cshowList :: [AbstState] -> ShowS
showList :: [AbstState] -> ShowS
Show)

smt2Line :: Builder -> SMT2
smt2Line :: Builder -> SMT2
smt2Line Builder
txt = [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder
txt] CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty

assertProps :: Config -> [Prop] -> Err SMT2
-- simplify to rewrite sload/sstore combos
-- notice: it is VERY important not to concretize, because Keccak assumptions
--         will be generated by assertPropsNoSimp, and that needs unconcretized Props
assertProps :: Config -> [Prop] -> Either [Char] SMT2
assertProps Config
conf [Prop]
ps = [Prop] -> Either [Char] SMT2
assertPropsNoSimp ([Prop] -> [Prop]
decompose ([Prop] -> [Prop]) -> ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Prop] -> [Prop]
Expr.simplifyProps ([Prop] -> [Prop]) -> [Prop] -> [Prop]
forall a b. (a -> b) -> a -> b
$ [Prop]
ps)
  where
    decompose :: [Prop] -> [Prop]
    decompose :: [Prop] -> [Prop]
decompose [Prop]
props = if Config
conf.decomposeStorage Bool -> Bool -> Bool
&& Bool
safeExprs Bool -> Bool -> Bool
&& Bool
safeProps
                      then [Prop] -> Maybe [Prop] -> [Prop]
forall a. a -> Maybe a -> a
fromMaybe [Prop]
props ((Prop -> Maybe Prop) -> [Prop] -> Maybe [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> Maybe (Expr a))
-> Prop -> Maybe Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> Maybe (Expr a)
forall (a :: EType). Expr a -> Maybe (Expr a)
Expr.decomposeStorage) [Prop]
props)
                      else [Prop]
props
      where
        -- All in these lists must be a `Just ()` or we cannot decompose
        safeExprs :: Bool
safeExprs = (Prop -> Bool) -> [Prop] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> (Prop -> Maybe ()) -> Prop -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: EType). Expr a -> Maybe ()) -> Prop -> Maybe ()
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m ()) -> Prop -> m ()
mapPropM_ Expr a -> Maybe ()
forall (a :: EType). Expr a -> Maybe ()
Expr.safeToDecompose) [Prop]
props
        safeProps :: Bool
safeProps = (Prop -> Bool) -> [Prop] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Prop -> Bool
Expr.safeToDecomposeProp [Prop]
props

-- Note: we need a version that does NOT call simplify,
-- because we make use of it to verify the correctness of our simplification
-- passes through property-based testing.
assertPropsNoSimp :: [Prop] -> Err SMT2
assertPropsNoSimp :: [Prop] -> Either [Char] SMT2
assertPropsNoSimp [Prop]
psPreConc = do
 [Builder]
encs <- (Prop -> Err Builder) -> [Prop] -> Either [Char] [Builder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Prop -> Err Builder
propToSMT [Prop]
psElim
 [Builder]
smt <- (Prop -> Err Builder) -> [Prop] -> Either [Char] [Builder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Prop -> Err Builder
propToSMT [Prop]
props
 SMT2
intermediates <- BufEnv -> StoreEnv -> Either [Char] SMT2
declareIntermediates BufEnv
bufs StoreEnv
stores
 SMT2
readAssumes' <- Either [Char] SMT2
readAssumes
 SMT2
keccakAssertions' <- Either [Char] SMT2
keccakAssertions
 SMT2
frameCtxs <- ([(Builder, [Prop])] -> Either [Char] SMT2
declareFrameContext ([(Builder, [Prop])] -> Either [Char] SMT2)
-> ([(Builder, [Prop])] -> [(Builder, [Prop])])
-> [(Builder, [Prop])]
-> Either [Char] SMT2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Builder, [Prop])] -> [(Builder, [Prop])]
forall a. Ord a => [a] -> [a]
nubOrd ([(Builder, [Prop])] -> Either [Char] SMT2)
-> [(Builder, [Prop])] -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ ([(Builder, [Prop])] -> [(Builder, [Prop])] -> [(Builder, [Prop])])
-> [(Builder, [Prop])]
-> [[(Builder, [Prop])]]
-> [(Builder, [Prop])]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [(Builder, [Prop])] -> [(Builder, [Prop])] -> [(Builder, [Prop])]
forall a. Semigroup a => a -> a -> a
(<>) [] [[(Builder, [Prop])]]
frameCtx)
 SMT2
blockCtxs <- ([(Builder, [Prop])] -> Either [Char] SMT2
declareBlockContext ([(Builder, [Prop])] -> Either [Char] SMT2)
-> ([(Builder, [Prop])] -> [(Builder, [Prop])])
-> [(Builder, [Prop])]
-> Either [Char] SMT2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Builder, [Prop])] -> [(Builder, [Prop])]
forall a. Ord a => [a] -> [a]
nubOrd ([(Builder, [Prop])] -> Either [Char] SMT2)
-> [(Builder, [Prop])] -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ ([(Builder, [Prop])] -> [(Builder, [Prop])] -> [(Builder, [Prop])])
-> [(Builder, [Prop])]
-> [[(Builder, [Prop])]]
-> [(Builder, [Prop])]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [(Builder, [Prop])] -> [(Builder, [Prop])] -> [(Builder, [Prop])]
forall a. Semigroup a => a -> a -> a
(<>) [] [[(Builder, [Prop])]]
blockCtx)
 SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ SMT2
prelude
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareAbstractStores [Builder]
abstractStores)
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
""
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareAddrs [Builder]
addresses)
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
""
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> ([Prop] -> BufEnv -> StoreEnv -> SMT2
declareBufs [Prop]
toDeclarePsElim BufEnv
bufs StoreEnv
stores)
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
""
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareVars ([Builder] -> SMT2)
-> ([Builder] -> [Builder]) -> [Builder] -> SMT2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Builder] -> [Builder]
forall a. Ord a => [a] -> [a]
nubOrd ([Builder] -> SMT2) -> [Builder] -> SMT2
forall a b. (a -> b) -> a -> b
$ ([Builder] -> [Builder] -> [Builder])
-> [Builder] -> [[Builder]] -> [Builder]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
(<>) [] [[Builder]]
allVars)
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
""
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> SMT2
frameCtxs
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
""
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> SMT2
blockCtxs
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
""
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> SMT2
intermediates
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
""
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> SMT2
keccakAssertions'
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> SMT2
readAssumes'
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
""
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 ((Builder -> Builder) -> [Builder] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Builder
p -> Builder
"(assert " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
p Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")") [Builder]
encs) CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder]
smt CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder]
forall a. Monoid a => a
mempty CexVars
forall a. Monoid a => a
mempty { storeReads = storageReads } [Prop]
forall a. Monoid a => a
mempty
  SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder]
forall a. Monoid a => a
mempty CexVars
forall a. Monoid a => a
mempty [Prop]
psPreConc

  where
    ps :: [Prop]
ps = [Prop] -> [Prop]
Expr.concKeccakProps [Prop]
psPreConc
    ([Prop]
psElim, BufEnv
bufs, StoreEnv
stores) = [Prop] -> ([Prop], BufEnv, StoreEnv)
eliminateProps [Prop]
ps
    abst :: AbstState
abst@(AbstState Map (Expr 'EWord) Int
exprToInt Int
_) = Map (Expr 'EWord) Int -> Int -> AbstState
AbstState Map (Expr 'EWord) Int
forall a. Monoid a => a
mempty Int
0

    props :: [Prop]
props = ((Expr 'EWord, Int) -> Prop) -> [(Expr 'EWord, Int)] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Expr 'EWord, Int) -> Prop
toProp (Map (Expr 'EWord) Int -> [(Expr 'EWord, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Expr 'EWord) Int
exprToInt)
      where
      toProp :: (Expr EWord, Int) -> Prop
      toProp :: (Expr 'EWord, Int) -> Prop
toProp (Expr 'EWord
e, Int
num) = Expr 'EWord -> Expr 'EWord -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr 'EWord
e (Text -> Expr 'EWord
Var ([Char] -> Text
TS.pack ([Char]
"abst_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
num))))

    -- Props storing info that need declaration(s)
    toDeclarePs :: [Prop]
toDeclarePs     = [Prop]
ps [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
keccAssump [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
keccComp
    toDeclarePsElim :: [Prop]
toDeclarePsElim = [Prop]
psElim [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
keccAssump [Prop] -> [Prop] -> [Prop]
forall a. Semigroup a => a -> a -> a
<> [Prop]
keccComp

    -- vars, frames, and block contexts in need of declaration
    allVars :: [[Builder]]
allVars = (Prop -> [Builder]) -> [Prop] -> [[Builder]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
forall a. TraversableTerm a => a -> [Builder]
referencedVars [Prop]
toDeclarePsElim [[Builder]] -> [[Builder]] -> [[Builder]]
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> [Builder]) -> [Expr 'Buf] -> [[Builder]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Buf -> [Builder]
forall a. TraversableTerm a => a -> [Builder]
referencedVars [Expr 'Buf]
bufVals [[Builder]] -> [[Builder]] -> [[Builder]]
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> [Builder]) -> [Expr 'Storage] -> [[Builder]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Storage -> [Builder]
forall a. TraversableTerm a => a -> [Builder]
referencedVars [Expr 'Storage]
storeVals [[Builder]] -> [[Builder]] -> [[Builder]]
forall a. Semigroup a => a -> a -> a
<> [AbstState -> [Builder]
abstrVars AbstState
abst]
    frameCtx :: [[(Builder, [Prop])]]
frameCtx = (Prop -> [(Builder, [Prop])]) -> [Prop] -> [[(Builder, [Prop])]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [(Builder, [Prop])]
forall a. TraversableTerm a => a -> [(Builder, [Prop])]
referencedFrameContext [Prop]
toDeclarePsElim [[(Builder, [Prop])]]
-> [[(Builder, [Prop])]] -> [[(Builder, [Prop])]]
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> [(Builder, [Prop])])
-> [Expr 'Buf] -> [[(Builder, [Prop])]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Buf -> [(Builder, [Prop])]
forall a. TraversableTerm a => a -> [(Builder, [Prop])]
referencedFrameContext [Expr 'Buf]
bufVals [[(Builder, [Prop])]]
-> [[(Builder, [Prop])]] -> [[(Builder, [Prop])]]
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> [(Builder, [Prop])])
-> [Expr 'Storage] -> [[(Builder, [Prop])]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Storage -> [(Builder, [Prop])]
forall a. TraversableTerm a => a -> [(Builder, [Prop])]
referencedFrameContext [Expr 'Storage]
storeVals
    blockCtx :: [[(Builder, [Prop])]]
blockCtx = (Prop -> [(Builder, [Prop])]) -> [Prop] -> [[(Builder, [Prop])]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [(Builder, [Prop])]
forall a. TraversableTerm a => a -> [(Builder, [Prop])]
referencedBlockContext [Prop]
toDeclarePsElim [[(Builder, [Prop])]]
-> [[(Builder, [Prop])]] -> [[(Builder, [Prop])]]
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> [(Builder, [Prop])])
-> [Expr 'Buf] -> [[(Builder, [Prop])]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Buf -> [(Builder, [Prop])]
forall a. TraversableTerm a => a -> [(Builder, [Prop])]
referencedBlockContext [Expr 'Buf]
bufVals [[(Builder, [Prop])]]
-> [[(Builder, [Prop])]] -> [[(Builder, [Prop])]]
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> [(Builder, [Prop])])
-> [Expr 'Storage] -> [[(Builder, [Prop])]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Storage -> [(Builder, [Prop])]
forall a. TraversableTerm a => a -> [(Builder, [Prop])]
referencedBlockContext [Expr 'Storage]
storeVals

    abstrVars :: AbstState -> [Builder]
    abstrVars :: AbstState -> [Builder]
abstrVars (AbstState Map (Expr 'EWord) Int
b Int
_) = ((Expr 'EWord, Int) -> Builder)
-> [(Expr 'EWord, Int)] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map ((\Int
v->[Char] -> Builder
fromString ([Char]
"abst_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
v)) (Int -> Builder)
-> ((Expr 'EWord, Int) -> Int) -> (Expr 'EWord, Int) -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr 'EWord, Int) -> Int
forall a b. (a, b) -> b
snd) (Map (Expr 'EWord) Int -> [(Expr 'EWord, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Expr 'EWord) Int
b)

    -- Buf, Storage, etc. declarations needed
    bufVals :: [Expr 'Buf]
bufVals = BufEnv -> [Expr 'Buf]
forall k a. Map k a -> [a]
Map.elems BufEnv
bufs
    storeVals :: [Expr 'Storage]
storeVals = StoreEnv -> [Expr 'Storage]
forall k a. Map k a -> [a]
Map.elems StoreEnv
stores
    storageReads :: Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
storageReads = (Set (Expr 'EWord) -> Set (Expr 'EWord) -> Set (Expr 'EWord))
-> [Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))]
-> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Set (Expr 'EWord) -> Set (Expr 'EWord) -> Set (Expr 'EWord)
forall a. Semigroup a => a -> a -> a
(<>) ([Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))]
 -> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord)))
-> [Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))]
-> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
forall a b. (a -> b) -> a -> b
$ (Prop -> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord)))
-> [Prop] -> [Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
findStorageReads [Prop]
toDeclarePs
    abstractStores :: [Builder]
abstractStores = Set Builder -> [Builder]
forall a. Set a -> [a]
Set.toList (Set Builder -> [Builder]) -> Set Builder -> [Builder]
forall a b. (a -> b) -> a -> b
$ [Set Builder] -> Set Builder
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Prop -> Set Builder) -> [Prop] -> [Set Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> Set Builder
forall a. TraversableTerm a => a -> Set Builder
referencedAbstractStores [Prop]
toDeclarePs)
    addresses :: [Builder]
addresses = Set Builder -> [Builder]
forall a. Set a -> [a]
Set.toList (Set Builder -> [Builder]) -> Set Builder -> [Builder]
forall a b. (a -> b) -> a -> b
$ [Set Builder] -> Set Builder
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Prop -> Set Builder) -> [Prop] -> [Set Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> Set Builder
forall a. TraversableTerm a => a -> Set Builder
referencedWAddrs [Prop]
toDeclarePs)

    -- Keccak assertions: concrete values, distance between pairs, injectivity, etc.
    --      This will make sure concrete values of Keccak are asserted, if they can be computed (i.e. can be concretized)
    keccAssump :: [Prop]
keccAssump = [Prop] -> [Expr 'Buf] -> [Expr 'Storage] -> [Prop]
keccakAssumptions [Prop]
psPreConc [Expr 'Buf]
bufVals [Expr 'Storage]
storeVals
    keccComp :: [Prop]
keccComp = [Prop] -> [Expr 'Buf] -> [Expr 'Storage] -> [Prop]
keccakCompute [Prop]
psPreConc [Expr 'Buf]
bufVals [Expr 'Storage]
storeVals
    keccakAssertions :: Either [Char] SMT2
keccakAssertions = do
      [Builder]
assumps <- (Prop -> Err Builder) -> [Prop] -> Either [Char] [Builder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Prop -> Err Builder
assertSMT [Prop]
keccAssump
      [Builder]
comps <- (Prop -> Err Builder) -> [Prop] -> Either [Char] [Builder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Prop -> Err Builder
assertSMT [Prop]
keccComp
      SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ Builder -> SMT2
smt2Line Builder
"; keccak assumptions"
        SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder]
assumps CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty
        SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> Builder -> SMT2
smt2Line Builder
"; keccak computations"
        SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder]
comps CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty

    -- assert that reads beyond size of buffer & storage is zero
    readAssumes :: Either [Char] SMT2
readAssumes = do
      [Builder]
assumps <- (Prop -> Err Builder) -> [Prop] -> Either [Char] [Builder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Prop -> Err Builder
assertSMT ([Prop] -> Either [Char] [Builder])
-> [Prop] -> Either [Char] [Builder]
forall a b. (a -> b) -> a -> b
$ [Prop] -> BufEnv -> StoreEnv -> [Prop]
assertReads [Prop]
psElim BufEnv
bufs StoreEnv
stores
      SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ Builder -> SMT2
smt2Line Builder
"; read assumptions" SMT2 -> SMT2 -> SMT2
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder]
assumps CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty

referencedAbstractStores :: TraversableTerm a => a -> Set Builder
referencedAbstractStores :: forall a. TraversableTerm a => a -> Set Builder
referencedAbstractStores a
term = (forall (b :: EType). Expr b -> Set Builder)
-> Set Builder -> a -> Set Builder
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> Set Builder
forall (b :: EType). Expr b -> Set Builder
go Set Builder
forall a. Monoid a => a
mempty a
term
  where
    go :: Expr a -> Set Builder
go = \case
      AbstractStore Expr 'EAddr
s Maybe W256
idx -> Builder -> Set Builder
forall a. a -> Set a
Set.singleton (Expr 'EAddr -> Maybe W256 -> Builder
storeName Expr 'EAddr
s Maybe W256
idx)
      Expr a
_ -> Set Builder
forall a. Monoid a => a
mempty

referencedWAddrs :: TraversableTerm a => a -> Set Builder
referencedWAddrs :: forall a. TraversableTerm a => a -> Set Builder
referencedWAddrs a
term = (forall (b :: EType). Expr b -> Set Builder)
-> Set Builder -> a -> Set Builder
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> Set Builder
forall (b :: EType). Expr b -> Set Builder
go Set Builder
forall a. Monoid a => a
mempty a
term
  where
    go :: Expr a -> Set Builder
go = \case
      WAddr(a :: Expr 'EAddr
a@(SymAddr Text
_)) -> Builder -> Set Builder
forall a. a -> Set a
Set.singleton (Expr 'EAddr -> Builder
formatEAddr Expr 'EAddr
a)
      Expr a
_ -> Set Builder
forall a. Monoid a => a
mempty

referencedBufs :: TraversableTerm a => a -> [Builder]
referencedBufs :: forall a. TraversableTerm a => a -> [Builder]
referencedBufs a
expr = [Builder] -> [Builder]
forall a. Ord a => [a] -> [a]
nubOrd ([Builder] -> [Builder]) -> [Builder] -> [Builder]
forall a b. (a -> b) -> a -> b
$ (forall (b :: EType). Expr b -> [Builder])
-> [Builder] -> a -> [Builder]
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> [Builder]
forall (b :: EType). Expr b -> [Builder]
go [] a
expr
  where
    go :: Expr a -> [Builder]
    go :: forall (b :: EType). Expr b -> [Builder]
go = \case
      AbstractBuf Text
s -> [Text -> Builder
fromText Text
s]
      Expr a
_ -> []

referencedVars :: TraversableTerm a => a -> [Builder]
referencedVars :: forall a. TraversableTerm a => a -> [Builder]
referencedVars a
expr = [Builder] -> [Builder]
forall a. Ord a => [a] -> [a]
nubOrd ([Builder] -> [Builder]) -> [Builder] -> [Builder]
forall a b. (a -> b) -> a -> b
$ (forall (b :: EType). Expr b -> [Builder])
-> [Builder] -> a -> [Builder]
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> [Builder]
forall (b :: EType). Expr b -> [Builder]
go [] a
expr
  where
    go :: Expr a -> [Builder]
    go :: forall (b :: EType). Expr b -> [Builder]
go = \case
      Var Text
s -> [Text -> Builder
fromText Text
s]
      Expr a
_ -> []

referencedFrameContext :: TraversableTerm a => a -> [(Builder, [Prop])]
referencedFrameContext :: forall a. TraversableTerm a => a -> [(Builder, [Prop])]
referencedFrameContext a
expr = [(Builder, [Prop])] -> [(Builder, [Prop])]
forall a. Ord a => [a] -> [a]
nubOrd ([(Builder, [Prop])] -> [(Builder, [Prop])])
-> [(Builder, [Prop])] -> [(Builder, [Prop])]
forall a b. (a -> b) -> a -> b
$ (forall (b :: EType). Expr b -> [(Builder, [Prop])])
-> [(Builder, [Prop])] -> a -> [(Builder, [Prop])]
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> [(Builder, [Prop])]
forall (b :: EType). Expr b -> [(Builder, [Prop])]
go [] a
expr
  where
    go :: Expr a -> [(Builder, [Prop])]
    go :: forall (b :: EType). Expr b -> [(Builder, [Prop])]
go = \case
      Expr a
TxValue -> [([Char] -> Builder
fromString [Char]
"txvalue", [])]
      v :: Expr a
v@(Balance Expr 'EAddr
a) -> [([Char] -> Builder
fromString [Char]
"balance_" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Expr 'EAddr -> Builder
formatEAddr Expr 'EAddr
a, [Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr a
Expr 'EWord
v (W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> W256 -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256
2 W256 -> Int -> W256
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
96 :: Int))])]
      Gas {} -> [Char] -> [(Builder, [Prop])]
forall a. HasCallStack => [Char] -> a
internalError [Char]
"TODO: GAS"
      Expr a
_ -> []

referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]
referencedBlockContext :: forall a. TraversableTerm a => a -> [(Builder, [Prop])]
referencedBlockContext a
expr = [(Builder, [Prop])] -> [(Builder, [Prop])]
forall a. Ord a => [a] -> [a]
nubOrd ([(Builder, [Prop])] -> [(Builder, [Prop])])
-> [(Builder, [Prop])] -> [(Builder, [Prop])]
forall a b. (a -> b) -> a -> b
$ (forall (b :: EType). Expr b -> [(Builder, [Prop])])
-> [(Builder, [Prop])] -> a -> [(Builder, [Prop])]
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> [(Builder, [Prop])]
forall (b :: EType). Expr b -> [(Builder, [Prop])]
go [] a
expr
  where
    go :: Expr a -> [(Builder, [Prop])]
    go :: forall (b :: EType). Expr b -> [(Builder, [Prop])]
go = \case
      Expr a
Origin -> [(Builder
"origin", [Int -> Expr 'EWord -> Prop
inRange Int
160 Expr 'EWord
Origin])]
      Expr a
Coinbase -> [(Builder
"coinbase", [Int -> Expr 'EWord -> Prop
inRange Int
160 Expr 'EWord
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
_ -> []

-- | 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 -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord))
findStorageReads :: Prop -> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
findStorageReads Prop
p = (Set (Expr 'EWord) -> Set (Expr 'EWord) -> Set (Expr 'EWord))
-> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
-> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set (Expr 'EWord) -> Set (Expr 'EWord) -> Set (Expr 'EWord)
forall a. Semigroup a => a -> a -> a
(<>) ([((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
 -> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord)))
-> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
-> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
forall a b. (a -> b) -> a -> b
$ (forall (a :: EType).
 Expr a -> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))])
-> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
-> Prop
-> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp Expr a -> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
forall (a :: EType).
Expr a -> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
go [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
forall a. Monoid a => a
mempty Prop
p
  where
    go :: Expr a -> [((Expr EAddr, Maybe W256), Set (Expr EWord))]
    go :: forall (a :: EType).
Expr a -> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
go = \case
      SLoad Expr 'EWord
slot Expr 'Storage
store ->
        [((Expr 'EAddr -> Maybe (Expr 'EAddr) -> Expr 'EAddr
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Expr 'EAddr
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Expr 'EAddr) -> [Char] -> Expr 'EAddr
forall a b. (a -> b) -> a -> b
$ [Char]
"could not extract address from: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Expr 'Storage -> [Char]
forall a. Show a => a -> [Char]
show Expr 'Storage
store) (Expr 'Storage -> Maybe (Expr 'EAddr)
Expr.getAddr Expr 'Storage
store), Expr 'Storage -> Maybe W256
Expr.getLogicalIdx Expr 'Storage
store), Expr 'EWord -> Set (Expr 'EWord)
forall a. a -> Set a
Set.singleton Expr 'EWord
slot) | (forall (a :: EType). Expr a -> Bool) -> Expr 'Storage -> Bool
forall (b :: EType).
(forall (a :: EType). Expr a -> Bool) -> Expr b -> Bool
containsNode Expr a -> Bool
forall (a :: EType). Expr a -> Bool
isAbstractStore Expr 'Storage
store]
      Expr a
_ -> []

    isAbstractStore :: Expr a -> Bool
isAbstractStore (AbstractStore Expr 'EAddr
_ Maybe W256
_) = 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 = ([(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
 -> a -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)])
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [a]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((forall (b :: EType).
 Expr b -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)])
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> a
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
forall a c.
(TraversableTerm a, Monoid c) =>
(forall (b :: EType). Expr b -> c) -> c -> a -> c
foldTerm Expr b -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall (b :: EType).
Expr b -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
go) [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a. Monoid a => a
mempty
  where
    go :: Expr a -> [(Expr EWord, Expr EWord, Expr Buf)]
    go :: forall (b :: EType).
Expr b -> [(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
_ -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
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 = ((Expr 'EWord, Expr 'EWord, Expr 'Buf) -> [Prop])
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)] -> [Prop]
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
_, Lit W256
0, Expr 'Buf
_) = []
    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)) (Expr 'EWord -> Expr 'EWord -> Prop
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) = [Prop -> Prop -> Prop
PImpl (Expr 'EWord -> Expr 'EWord -> Prop
PGEq (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
idx (Expr 'EWord -> Expr 'EWord) -> Expr 'EWord -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256 -> Expr 'EWord
Lit W256
offset) (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
buf)) (Expr 'Byte -> Expr 'Byte -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (Expr 'EWord -> Expr 'Buf -> Expr 'Byte
ReadByte (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
idx (Expr 'EWord -> Expr 'EWord) -> Expr 'EWord -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ W256 -> Expr 'EWord
Lit W256
offset) Expr 'Buf
buf) (Word8 -> Expr 'Byte
LitByte Word8
0)) | W256
offset <- [(W256
0::W256).. W256
szW256 -> W256 -> W256
forall a. Num a => a -> a -> a
-W256
1]]
    assertRead (Expr 'EWord
_, Expr 'EWord
_, Expr 'Buf
_) = [Char] -> [Prop]
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Cannot generate assertions for accesses of symbolic size"

    allReads :: [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
allReads = ((Expr 'EWord, Expr 'EWord, Expr 'Buf) -> Bool)
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr 'EWord, Expr 'EWord, Expr 'Buf) -> Bool
keepRead ([(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
 -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)])
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a b. (a -> b) -> a -> b
$ [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a. Ord a => [a] -> [a]
nubOrd ([(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
 -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)])
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a b. (a -> b) -> a -> b
$ [Prop] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess [Prop]
props [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a. Semigroup a => a -> a -> a
<> [Expr 'Buf] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess (BufEnv -> [Expr 'Buf]
forall k a. Map k a -> [a]
Map.elems BufEnv
benv) [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a. Semigroup a => a -> a -> a
<> [Expr 'Storage] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess (StoreEnv -> [Expr 'Storage]
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 | W256 -> Integer
forall target source. From source target => source -> target
into (W256
idx W256 -> W256 -> W256
forall a. Num a => a -> a -> a
+ W256
size) Integer -> Integer -> Bool
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 = [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a. Ord a => [a] -> [a]
nubOrd ([(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
 -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)])
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a b. (a -> b) -> a -> b
$ [Prop] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess [Prop]
props [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a. Semigroup a => a -> a -> a
<> [Expr 'Buf] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess (BufEnv -> [Expr 'Buf]
forall k a. Map k a -> [a]
Map.elems BufEnv
benv) [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a. Semigroup a => a -> a -> a
<> [Expr 'Storage] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
forall a.
TraversableTerm a =>
[a] -> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
findBufferAccess (StoreEnv -> [Expr 'Storage]
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 = [(Text, Expr 'EWord)] -> Map Text (Expr 'EWord)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Text, Expr 'EWord)] -> Map Text (Expr 'EWord))
-> ([[Builder]] -> [(Text, Expr 'EWord)])
-> [[Builder]]
-> Map Text (Expr 'EWord)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> (Text, Expr 'EWord)) -> [Text] -> [(Text, Expr 'EWord)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, W256 -> Expr 'EWord
Lit W256
4) ([Text] -> [(Text, Expr 'EWord)])
-> ([[Builder]] -> [Text]) -> [[Builder]] -> [(Text, Expr 'EWord)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Builder -> Text) -> [Builder] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText ([Builder] -> [Text])
-> ([[Builder]] -> [Builder]) -> [[Builder]] -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Builder] -> [Builder]
forall a. Ord a => [a] -> [a]
nubOrd ([Builder] -> [Builder])
-> ([[Builder]] -> [Builder]) -> [[Builder]] -> [Builder]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Builder]] -> [Builder]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Builder]] -> Map Text (Expr 'EWord))
-> [[Builder]] -> Map Text (Expr 'EWord)
forall a b. (a -> b) -> a -> b
$ (Prop -> [Builder]) -> [Prop] -> [[Builder]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
forall a. TraversableTerm a => a -> [Builder]
referencedBufs [Prop]
props [[Builder]] -> [[Builder]] -> [[Builder]]
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> [Builder]) -> [Expr 'Buf] -> [[Builder]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Buf -> [Builder]
forall a. TraversableTerm a => a -> [Builder]
referencedBufs (BufEnv -> [Expr 'Buf]
forall k a. Map k a -> [a]
Map.elems BufEnv
benv) [[Builder]] -> [[Builder]] -> [[Builder]]
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> [Builder]) -> [Expr 'Storage] -> [[Builder]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Storage -> [Builder]
forall a. TraversableTerm a => a -> [Builder]
referencedBufs (StoreEnv -> [Expr 'Storage]
forall k a. Map k a -> [a]
Map.elems StoreEnv
senv)

    bufMap :: Map Text (Expr 'EWord)
bufMap = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> Map Text (Expr 'EWord)
-> Map Text (Expr 'EWord)
-> Map Text (Expr 'EWord)
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 ((Map Text (Expr 'EWord)
 -> (Expr 'EWord, Expr 'EWord, Expr 'Buf) -> Map Text (Expr 'EWord))
-> Map Text (Expr 'EWord)
-> [(Expr 'EWord, Expr 'EWord, Expr 'Buf)]
-> Map Text (Expr 'EWord)
forall b a. (b -> a -> b) -> b -> [a] -> b
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 Map Text (Expr 'EWord)
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 -> (Expr 'EWord -> Expr 'EWord -> Expr 'EWord)
-> Text
-> Expr 'EWord
-> Map Text (Expr 'EWord)
-> Map Text (Expr 'EWord)
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 Int -> BufEnv -> Maybe (Expr 'Buf)
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 -> [Char] -> Expr 'Buf
forall a. HasCallStack => [Char] -> a
internalError [Char]
"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 -> [Prop] -> SMT2
SMT2 (Builder
"; buffers" Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
: (Builder -> Builder) -> [Builder] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Builder
forall {a}. (Semigroup a, IsString a) => a -> a
declareBuf [Builder]
allBufs [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> (Builder
"; buffer lengths" Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
: (Builder -> Builder) -> [Builder] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Builder
forall {a}. (Semigroup a, IsString a) => a -> a
declareLength [Builder]
allBufs)) CexVars
cexvars [Prop]
forall a. Monoid a => a
mempty
  where
    cexvars :: CexVars
cexvars = (CexVars
forall a. Monoid a => a
mempty :: CexVars){ buffers = discoverMaxReads props bufEnv storeEnv }
    allBufs :: [Builder]
allBufs = (Text -> Builder) -> [Text] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Builder
fromLazyText ([Text] -> [Builder]) -> [Text] -> [Builder]
forall a b. (a -> b) -> a -> b
$ Map Text (Expr 'EWord) -> [Text]
forall k a. Map k a -> [k]
Map.keys CexVars
cexvars.buffers
    declareBuf :: a -> a
declareBuf a
n = a
"(declare-fun " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
n a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" () (Array (_ BitVec 256) (_ BitVec 8)))"
    declareLength :: a -> a
declareLength a
n = a
"(declare-fun " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
n a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
"_length" a -> a -> a
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 -> [Prop] -> SMT2
SMT2 ([Builder
"; variables"] [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> (Builder -> Builder) -> [Builder] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Builder
forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
cexvars [Prop]
forall a. Monoid a => a
mempty
  where
    declare :: a -> a
declare a
n = a
"(declare-fun " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
n a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" () (_ BitVec 256))"
    cexvars :: CexVars
cexvars = (CexVars
forall a. Monoid a => a
mempty :: CexVars){ calldata = fmap toLazyText names }

-- Given a list of variable names, create an SMT2 object with the variables declared
declareAddrs :: [Builder] -> SMT2
declareAddrs :: [Builder] -> SMT2
declareAddrs [Builder]
names = [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 ([Builder
"; symbolic addresseses"] [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> (Builder -> Builder) -> [Builder] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Builder
forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
cexvars [Prop]
forall a. Monoid a => a
mempty
  where
    declare :: a -> a
declare a
n = a
"(declare-fun " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
n a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" () Addr)"
    cexvars :: CexVars
cexvars = (CexVars
forall a. Monoid a => a
mempty :: CexVars){ addrs = fmap toLazyText names }

declareFrameContext :: [(Builder, [Prop])] -> Err SMT2
declareFrameContext :: [(Builder, [Prop])] -> Either [Char] SMT2
declareFrameContext [(Builder, [Prop])]
names = do
  [Builder]
decls <- ((Builder, [Prop]) -> Either [Char] [Builder])
-> [(Builder, [Prop])] -> Either [Char] [Builder]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (Builder, [Prop]) -> Either [Char] [Builder]
declare [(Builder, [Prop])]
names
  SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 ([Builder
"; frame context"] [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> [Builder]
decls) CexVars
cexvars [Prop]
forall a. Monoid a => a
mempty
  where
    declare :: (Builder, [Prop]) -> Either [Char] [Builder]
declare (Builder
n,[Prop]
props) = do
      [Builder]
asserts <- (Prop -> Err Builder) -> [Prop] -> Either [Char] [Builder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Prop -> Err Builder
assertSMT [Prop]
props
      [Builder] -> Either [Char] [Builder]
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Builder] -> Either [Char] [Builder])
-> [Builder] -> Either [Char] [Builder]
forall a b. (a -> b) -> a -> b
$ [ Builder
"(declare-fun " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" () (_ BitVec 256))" ] [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> [Builder]
asserts
    cexvars :: CexVars
cexvars = (CexVars
forall a. Monoid a => a
mempty :: CexVars){ txContext = fmap (toLazyText . fst) names }

declareAbstractStores :: [Builder] -> SMT2
declareAbstractStores :: [Builder] -> SMT2
declareAbstractStores [Builder]
names = [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 ([Builder
"; abstract base stores"] [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> (Builder -> Builder) -> [Builder] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Builder
forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty
  where
    declare :: a -> a
declare a
n = a
"(declare-fun " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
n a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" () Storage)"

declareBlockContext :: [(Builder, [Prop])] -> Err SMT2
declareBlockContext :: [(Builder, [Prop])] -> Either [Char] SMT2
declareBlockContext [(Builder, [Prop])]
names = do
  [Builder]
decls <- ((Builder, [Prop]) -> Either [Char] [Builder])
-> [(Builder, [Prop])] -> Either [Char] [Builder]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (Builder, [Prop]) -> Either [Char] [Builder]
declare [(Builder, [Prop])]
names
  SMT2 -> Either [Char] SMT2
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SMT2 -> Either [Char] SMT2) -> SMT2 -> Either [Char] SMT2
forall a b. (a -> b) -> a -> b
$ [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 ([Builder
"; block context"] [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> [Builder]
decls) CexVars
cexvars [Prop]
forall a. Monoid a => a
mempty
  where
    declare :: (Builder, [Prop]) -> Either [Char] [Builder]
declare (Builder
n, [Prop]
props) = do
      [Builder]
asserts <- (Prop -> Err Builder) -> [Prop] -> Either [Char] [Builder]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Prop -> Err Builder
assertSMT [Prop]
props
      [Builder] -> Either [Char] [Builder]
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Builder] -> Either [Char] [Builder])
-> [Builder] -> Either [Char] [Builder]
forall a b. (a -> b) -> a -> b
$ [ Builder
"(declare-fun " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" () (_ BitVec 256))" ] [Builder] -> [Builder] -> [Builder]
forall a. Semigroup a => a -> a -> a
<> [Builder]
asserts
    cexvars :: CexVars
cexvars = (CexVars
forall a. Monoid a => a
mempty :: CexVars){ blockContext = fmap (toLazyText . fst) names }

assertSMT :: Prop -> Either String Builder
assertSMT :: Prop -> Err Builder
assertSMT Prop
p = do
  Builder
p' <- Prop -> Err Builder
propToSMT Prop
p
  Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(assert " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
p' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

prelude :: SMT2
prelude :: SMT2
prelude =  [Builder] -> CexVars -> [Prop] -> SMT2
SMT2 [Builder]
src CexVars
forall a. Monoid a => a
mempty [Prop]
forall a. Monoid a => a
mempty
  where
  src :: [Builder]
src = (Text -> Builder) -> [Text] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Builder
fromLazyText (Text -> Builder) -> (Text -> Text) -> Text -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Text -> Text
T.drop Int64
2) ([Text] -> [Builder]) -> (Text -> [Text]) -> Text -> [Builder]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Text]
T.lines (Text -> [Builder]) -> Text -> [Builder]
forall a b. (a -> b) -> a -> b
$ Text
[i|
  ; logic
  (set-info :smt-lib-version 2.6)
  ;(set-logic QF_AUFBV)
  (set-logic ALL)
  (set-info :source |
  Generator: hevm
  Application: hevm symbolic execution system
  |)
  (set-info :category "industrial")

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

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

  ; hash functions. They take buffer and a buffer size, and return a Word
  (declare-fun keccak (Buf Word) Word)
  (declare-fun sha256 (Buf Word) Word)

  ; helper functions
  (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)
    ))))))))))))))))))))))))))))))))
  )

  (define-fun readWord ((idx Word) (buf Buf)) Word
    (concat
      (select buf idx)
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000001))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000002))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000003))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000004))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000005))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000006))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000007))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000008))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000009))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000a))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000b))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000c))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000d))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000e))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000f))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000010))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000011))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000012))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000013))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000014))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000015))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000016))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000017))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000018))
      (concat (select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000019))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001a))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001b))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001c))
      (concat (select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001d))
      (concat (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)
  (declare-fun codesize (Addr) 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))))))))))))))))))))))))))))))))
  |]

exprToSMT :: Expr a -> Err Builder
exprToSMT :: forall (a :: EType). Expr a -> Err Builder
exprToSMT = \case
  Lit W256
w -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromLazyText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ Text
"(_ bv" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ([Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ Integer -> [Char]
forall a. Show a => a -> [Char]
show (W256 -> Integer
forall target source. From source target => source -> target
into W256
w :: Integer)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" 256)"
  Var Text
s -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromText Text
s
  GVar (BufVar Int
n) -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ [Char] -> Builder
fromString ([Char] -> Builder) -> [Char] -> Builder
forall a b. (a -> b) -> a -> b
$ [Char]
"buf" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
  GVar (StoreVar Int
n) -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ [Char] -> Builder
fromString ([Char] -> Builder) -> [Char] -> Builder
forall a b. (a -> b) -> a -> b
$ [Char]
"store" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Int -> [Char]
forall a. Show a => a -> [Char]
show 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] -> Err 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 -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvadd" Expr 'EWord
a Expr 'EWord
b
  Sub Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvsub" Expr 'EWord
a Expr 'EWord
b
  Mul Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err 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 -> Err Builder
expandExp Expr 'EWord
a W256
b'
               Expr 'EWord
_ -> [Char] -> Err Builder
forall a b. a -> Either a b
Left [Char]
"cannot encode symbolic exponentiation into SMT"
  Min Expr 'EWord
a Expr 'EWord
b -> do
    Builder
aenc <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
a
    Builder
benc <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite (bvule " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
") " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  Max Expr 'EWord
a Expr 'EWord
b -> do
    Builder
aenc <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
a
    Builder
benc <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(max " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  LT Expr 'EWord
a Expr 'EWord
b -> do
    Builder
cond <- Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvult" Expr 'EWord
a Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  SLT Expr 'EWord
a Expr 'EWord
b -> do
    Builder
cond <- Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvslt" Expr 'EWord
a Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  SGT Expr 'EWord
a Expr 'EWord
b -> do
    Builder
cond <- Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvsgt" Expr 'EWord
a Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  GT Expr 'EWord
a Expr 'EWord
b -> do
    Builder
cond <- Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvugt" Expr 'EWord
a Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  LEq Expr 'EWord
a Expr 'EWord
b -> do
    Builder
cond <- Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvule" Expr 'EWord
a Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  GEq Expr 'EWord
a Expr 'EWord
b -> do
    Builder
cond <- Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvuge" Expr 'EWord
a Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  Eq Expr 'EWord
a Expr 'EWord
b -> do
    Builder
cond <- Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"=" Expr 'EWord
a Expr 'EWord
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  IsZero Expr 'EWord
a -> do
    Builder
cond <- Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"=" Expr 'EWord
a (W256 -> Expr 'EWord
Lit W256
0)
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  And Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvand" Expr 'EWord
a Expr 'EWord
b
  Or Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvor" Expr 'EWord
a Expr 'EWord
b
  Xor Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvxor" Expr 'EWord
a Expr 'EWord
b
  Not Expr 'EWord
a -> Builder -> Expr 'EWord -> Err Builder
forall {a :: EType}. Builder -> Expr a -> Err Builder
op1 Builder
"bvnot" Expr 'EWord
a
  SHL Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvshl" Expr 'EWord
b Expr 'EWord
a
  SHR Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvlshr" Expr 'EWord
b Expr 'EWord
a
  SAR Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvashr" Expr 'EWord
b Expr 'EWord
a
  SEx Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"signext" Expr 'EWord
a Expr 'EWord
b
  Div Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2CheckZero Builder
"bvudiv" Expr 'EWord
a Expr 'EWord
b
  SDiv Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2CheckZero Builder
"bvsdiv" Expr 'EWord
a Expr 'EWord
b
  Mod Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2CheckZero Builder
"bvurem" Expr 'EWord
a Expr 'EWord
b
  SMod Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err 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 -> do
    Builder
aExp <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
a
    Builder
bExp <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
b
    Builder
cExp <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
c
    let aLift :: Builder
aLift = Builder
"(concat (_ bv0 256) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aExp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
        bLift :: Builder
bLift = Builder
"(concat (_ bv0 256) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bExp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
        cLift :: Builder
cLift = Builder
"(concat (_ bv0 256) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cExp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"((_ extract 255 0) (ite (= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cExp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" (_ bv0 256)) (_ bv0 512) (bvurem (bvmul " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aLift Builder -> Builder -> Builder
`sp` Builder
bLift Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cLift Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")))"
  AddMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c -> do
    Builder
aExp <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
a
    Builder
bExp <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
b
    Builder
cExp <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
c
    let aLift :: Builder
aLift = Builder
"(concat (_ bv0 256) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aExp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
        bLift :: Builder
bLift = Builder
"(concat (_ bv0 256) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bExp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
        cLift :: Builder
cLift = Builder
"(concat (_ bv0 256) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cExp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"((_ extract 255 0) (ite (= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cExp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" (_ bv0 256)) (_ bv0 512) (bvurem (bvadd " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aLift Builder -> Builder -> Builder
`sp` Builder
bLift Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cLift Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")))"
  EqByte Expr 'Byte
a Expr 'Byte
b -> do
    Builder
cond <- Builder -> Expr 'Byte -> Expr 'Byte -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"=" Expr 'Byte
a Expr 'Byte
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  Keccak Expr 'Buf
a -> do
    Builder
enc <- Expr 'Buf -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Buf
a
    Builder
sz  <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Expr 'EWord -> Err Builder) -> Expr 'EWord -> Err Builder
forall a b. (a -> b) -> a -> b
$ Expr 'Buf -> Expr 'EWord
Expr.bufLength Expr 'Buf
a
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(keccak " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
enc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
sz Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  SHA256 Expr 'Buf
a -> do
    Builder
enc <- Expr 'Buf -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Buf
a
    Builder
sz  <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Expr 'EWord -> Err Builder) -> Expr 'EWord -> Err Builder
forall a b. (a -> b) -> a -> b
$ Expr 'Buf -> Expr 'EWord
Expr.bufLength Expr 'Buf
a
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(sha256 " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
enc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
sz Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

  Expr a
TxValue -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ [Char] -> Builder
fromString [Char]
"txvalue"
  Balance Expr 'EAddr
a -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ [Char] -> Builder
fromString [Char]
"balance_" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Expr 'EAddr -> Builder
formatEAddr Expr 'EAddr
a

  Expr a
Origin ->  Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"origin"
  BlockHash Expr 'EWord
a -> do
    Builder
enc <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
a
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(blockhash " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
enc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  CodeSize Expr 'EAddr
a -> do
    Builder
enc <- Expr 'EAddr -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EAddr
a
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(codesize " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
enc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  Expr a
Coinbase -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"coinbase"
  Expr a
Timestamp -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"timestamp"
  Expr a
BlockNumber -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"blocknumber"
  Expr a
PrevRandao -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"prevrandao"
  Expr a
GasLimit -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"gaslimit"
  Expr a
ChainId -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"chainid"
  Expr a
BaseFee -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"basefee"

  a :: Expr a
a@(SymAddr Text
_) -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Expr 'EAddr -> Builder
formatEAddr Expr a
Expr 'EAddr
a
  WAddr(a :: Expr 'EAddr
a@(SymAddr Text
_)) -> do
    Builder
wa <- Expr 'EAddr -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EAddr
a
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"((_ zero_extend 96)" Builder -> Builder -> Builder
`sp` Builder
wa Builder -> Builder -> Builder
`sp` Builder
")"

  LitByte Word8
b -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromLazyText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ Text
"(_ bv" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (Integer -> [Char]
forall a. Show a => a -> [Char]
show (Word8 -> Integer
forall target source. From source target => source -> target
into Word8
b :: Integer)) Text -> Text -> Text
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 W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
>= W256
0 Bool -> Bool -> Bool
&& W256
n W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
< W256
32
             then do
               Builder
enc <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
w
               Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromLazyText (Text
"(indexWord" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (Integer -> [Char]
forall a. Show a => a -> [Char]
show (W256 -> Integer
forall target source. From source target => source -> target
into W256
n :: Integer))) Builder -> Builder -> Builder
`sp` Builder
enc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
             else Expr 'Byte -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Word8 -> Expr 'Byte
LitByte Word8
0)
    Expr 'EWord
_ -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"indexWord" Expr 'EWord
idx Expr 'EWord
w
  ReadByte Expr 'EWord
idx Expr 'Buf
src -> Builder -> Expr 'Buf -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"select" Expr 'Buf
src Expr 'EWord
idx

  ConcreteBuf ByteString
"" -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"((as const Buf) #b00000000)"
  ConcreteBuf ByteString
bs -> ByteString -> Expr 'Buf -> Err Builder
writeBytes ByteString
bs Expr 'Buf
forall a. Monoid a => a
mempty
  AbstractBuf Text
s -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromText Text
s
  ReadWord Expr 'EWord
idx Expr 'Buf
prev -> Builder -> Expr 'EWord -> Expr 'Buf -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"readWord" Expr 'EWord
idx Expr 'Buf
prev
  BufLength (AbstractBuf Text
b) -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromText Text
b Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"_length"
  BufLength (GVar (BufVar Int
n)) -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromLazyText (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ Text
"buf" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> ([Char] -> Text
T.pack ([Char] -> Text) -> (Int -> [Char]) -> Int -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show (Int -> Text) -> Int -> Text
forall a b. (a -> b) -> a -> b
$ Int
n) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_length"
  BufLength Expr 'Buf
b -> Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Expr 'Buf -> Expr 'EWord
bufLength Expr 'Buf
b)
  WriteByte Expr 'EWord
idx Expr 'Byte
val Expr 'Buf
prev -> do
    Builder
encIdx  <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
idx
    Builder
encVal  <- Expr 'Byte -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Byte
val
    Builder
encPrev <- Expr 'Buf -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Buf
prev
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(store " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
encPrev Builder -> Builder -> Builder
`sp` Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  WriteWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
prev -> do
    Builder
encIdx  <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
idx
    Builder
encVal  <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
val
    Builder
encPrev <- Expr 'Buf -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Buf
prev
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(writeWord " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
`sp` Builder
encPrev Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  CopySlice Expr 'EWord
srcIdx Expr 'EWord
dstIdx Expr 'EWord
size Expr 'Buf
src Expr 'Buf
dst -> do
    Builder
srcSMT <- Expr 'Buf -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Buf
src
    Builder
dstSMT <- Expr 'Buf -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Buf
dst
    Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Builder -> Builder -> Err Builder
copySlice Expr 'EWord
srcIdx Expr 'EWord
dstIdx Expr 'EWord
size Builder
srcSMT Builder
dstSMT

  -- we need to do a bit of processing here.
  ConcreteStore Map W256 W256
s -> Map W256 W256 -> Err Builder
encodeConcreteStore Map W256 W256
s
  AbstractStore Expr 'EAddr
a Maybe W256
idx -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Expr 'EAddr -> Maybe W256 -> Builder
storeName Expr 'EAddr
a Maybe W256
idx
  SStore Expr 'EWord
idx Expr 'EWord
val Expr 'Storage
prev -> do
    Builder
encIdx  <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
idx
    Builder
encVal  <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
val
    Builder
encPrev <- Expr 'Storage -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Storage
prev
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(store" Builder -> Builder -> Builder
`sp` Builder
encPrev Builder -> Builder -> Builder
`sp` Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  SLoad Expr 'EWord
idx Expr 'Storage
store -> Builder -> Expr 'Storage -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"select" Expr 'Storage
store Expr 'EWord
idx

  Expr a
a -> [Char] -> Err Builder
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Err Builder) -> [Char] -> Err Builder
forall a b. (a -> b) -> a -> b
$ [Char]
"TODO: implement: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Expr a -> [Char]
forall a. Show a => a -> [Char]
show Expr a
a
  where
    op1 :: Builder -> Expr a -> Err Builder
op1 Builder
op Expr a
a = do
      Builder
enc <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
a
      Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
enc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    op2 :: Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
op Expr a
a Expr a
b = do
       Builder
aenc <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
a
       Builder
benc <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
b
       Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(" Builder -> Builder -> 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
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    op2CheckZero :: Builder -> Expr a -> Expr a -> Err Builder
op2CheckZero Builder
op Expr a
a Expr a
b = do
      Builder
aenc <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
a
      Builder
benc <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
b
      Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(ite (= " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
benc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" (_ bv0 256)) (_ bv0 256) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>  Builder
"(" Builder -> Builder -> 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
forall a. Semigroup a => a -> a -> a
<> Builder
"))"

sp :: Builder -> Builder -> Builder
Builder
a sp :: Builder -> Builder -> Builder
`sp` Builder
b = Builder
a Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> (Text -> Builder
fromText Text
" ") Builder -> Builder -> Builder
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 -> Err Builder
propToSMT :: Prop -> Err Builder
propToSMT = \case
  PEq Expr a
a Expr a
b -> Builder -> Expr a -> Expr a -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"=" Expr a
a Expr a
b
  PLT Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvult" Expr 'EWord
a Expr 'EWord
b
  PGT Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvugt" Expr 'EWord
a Expr 'EWord
b
  PLEq Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvule" Expr 'EWord
a Expr 'EWord
b
  PGEq Expr 'EWord
a Expr 'EWord
b -> Builder -> Expr 'EWord -> Expr 'EWord -> Err Builder
forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
"bvuge" Expr 'EWord
a Expr 'EWord
b
  PNeg Prop
a -> do
    Builder
enc <- Prop -> Err Builder
propToSMT Prop
a
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(not " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
enc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  PAnd Prop
a Prop
b -> do
    Builder
aenc <- Prop -> Err Builder
propToSMT Prop
a
    Builder
benc <- Prop -> Err Builder
propToSMT Prop
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(and " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
benc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  POr Prop
a Prop
b -> do
    Builder
aenc <- Prop -> Err Builder
propToSMT Prop
a
    Builder
benc <- Prop -> Err Builder
propToSMT Prop
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(or " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
benc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  PImpl Prop
a Prop
b -> do
    Builder
aenc <- Prop -> Err Builder
propToSMT Prop
a
    Builder
benc <- Prop -> Err Builder
propToSMT Prop
b
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(=> " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
benc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  PBool Bool
b -> Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ if Bool
b then Builder
"true" else Builder
"false"
  where
    op2 :: Builder -> Expr a -> Expr a -> Err Builder
op2 Builder
op Expr a
a Expr a
b = do
      Builder
aenc <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
a
      Builder
benc <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
b
      Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
benc Builder -> Builder -> Builder
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 -> Err Builder
copySlice :: Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Builder -> Builder -> Err Builder
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset size0 :: Expr 'EWord
size0@(Lit W256
_) Builder
src Builder
dst = do
  Builder
sz <- Expr 'EWord -> Err Builder
internal Expr 'EWord
size0
  Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(let ((src " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
src Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")) " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
sz Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  where
    internal :: Expr 'EWord -> Err Builder
internal (Lit W256
0) = Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
dst
    internal Expr 'EWord
size = do
      let size' :: Expr 'EWord
size' = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.sub Expr 'EWord
size (W256 -> Expr 'EWord
Lit W256
1))
      Builder
encDstOff <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
dstOffset Expr 'EWord
size')
      Builder
encSrcOff <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Expr.add Expr 'EWord
srcOffset Expr 'EWord
size')
      Builder
child <- Expr 'EWord -> Err Builder
internal Expr 'EWord
size'
      Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(store " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
child Builder -> Builder -> Builder
`sp` Builder
encDstOff Builder -> Builder -> Builder
`sp` Builder
"(select src " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
encSrcOff Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"))"
copySlice Expr 'EWord
_ Expr 'EWord
_ Expr 'EWord
_ Builder
_ Builder
_ = [Char] -> Err Builder
forall a b. a -> Either a b
Left [Char]
"CopySlice with a symbolically sized region not currently implemented, cannot execute SMT solver on this query"

-- | Unrolls an exponentiation into a series of multiplications
expandExp :: Expr EWord -> W256 -> Err Builder
expandExp :: Expr 'EWord -> W256 -> Err Builder
expandExp Expr 'EWord
base W256
expnt
  | W256
expnt W256 -> W256 -> Bool
forall a. Eq a => a -> a -> Bool
== W256
1 = Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
base
  | Bool
otherwise = do
    Builder
b <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
base
    Builder
n <- Expr 'EWord -> W256 -> Err Builder
expandExp Expr 'EWord
base (W256
expnt W256 -> W256 -> W256
forall a. Num a => a -> a -> a
- W256
1)
    Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(bvmul " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
b Builder -> Builder -> Builder
`sp` Builder
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | Concatenates a list of bytes into a larger bitvector
concatBytes :: [Expr Byte] -> Err Builder
concatBytes :: [Expr 'Byte] -> Err Builder
concatBytes [Expr 'Byte]
bytes = do
  let bytesRev :: [Expr 'Byte]
bytesRev = [Expr 'Byte] -> [Expr 'Byte]
forall a. [a] -> [a]
reverse [Expr 'Byte]
bytes
  Builder
a2 <- Expr 'Byte -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT ([Expr 'Byte] -> Expr 'Byte
forall a. HasCallStack => [a] -> a
head [Expr 'Byte]
bytesRev)
  (Builder -> Expr 'Byte -> Err Builder)
-> Builder -> [Expr 'Byte] -> Err Builder
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Builder -> Expr 'Byte -> Err Builder
forall {a :: EType}. Builder -> Expr a -> Err Builder
wrap Builder
a2 ([Expr 'Byte] -> Err Builder) -> [Expr 'Byte] -> Err Builder
forall a b. (a -> b) -> a -> b
$ [Expr 'Byte] -> [Expr 'Byte]
forall a. HasCallStack => [a] -> [a]
tail [Expr 'Byte]
bytesRev
  where
    wrap :: Builder -> Expr a -> Err Builder
    wrap :: forall {a :: EType}. Builder -> Expr a -> Err Builder
wrap Builder
inner Expr a
byte = do
      Builder
byteSMT <- Expr a -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr a
byte
      Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(concat " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
byteSMT Builder -> Builder -> Builder
`sp` Builder
inner Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | Concatenates a list of bytes into a larger bitvector
writeBytes :: ByteString -> Expr Buf -> Err Builder
writeBytes :: ByteString -> Expr 'Buf -> Err Builder
writeBytes ByteString
bytes Expr 'Buf
buf =  do
  Builder
buf' <- Expr 'Buf -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'Buf
buf
  (Int, Builder)
ret <- ((Int, Builder) -> Word8 -> Either [Char] (Int, Builder))
-> (Int, Builder) -> [Word8] -> Either [Char] (Int, Builder)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Int, Builder) -> Word8 -> Either [Char] (Int, Builder)
wrap (Int
0, Builder
buf') ([Word8] -> Either [Char] (Int, Builder))
-> [Word8] -> Either [Char] (Int, Builder)
forall a b. (a -> b) -> a -> b
$ ByteString -> [Word8]
BS.unpack ByteString
bytes
  Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ (Int, Builder) -> Builder
forall a b. (a, b) -> b
snd (Int, Builder)
ret
  where
    -- we don't need to store zeros if the base buffer is empty
    skipZeros :: Bool
skipZeros = Expr 'Buf
buf Expr 'Buf -> Expr 'Buf -> Bool
forall a. Eq a => a -> a -> Bool
== Expr 'Buf
forall a. Monoid a => a
mempty
    wrap :: (Int, Builder) -> Word8 -> Err (Int, Builder)
    wrap :: (Int, Builder) -> Word8 -> Either [Char] (Int, Builder)
wrap (Int
idx, Builder
inner) Word8
byte =
      if Bool
skipZeros Bool -> Bool -> Bool
&& Word8
byte Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0
      then (Int, Builder) -> Either [Char] (Int, Builder)
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Builder
inner)
      else do
          Builder
byteSMT <- Expr 'Byte -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Word8 -> Expr 'Byte
LitByte Word8
byte)
          Builder
idxSMT <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Expr 'EWord -> Err Builder)
-> (Int -> Expr 'EWord) -> Int -> Err Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit (W256 -> Expr 'EWord) -> (Int -> W256) -> Int -> Expr 'EWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> W256
forall target source.
(HasCallStack, TryFrom source target, Show source, Typeable source,
 Typeable target) =>
source -> target
unsafeInto (Int -> Err Builder) -> Int -> Err Builder
forall a b. (a -> b) -> a -> b
$ Int
idx
          (Int, Builder) -> Either [Char] (Int, Builder)
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Builder
"(store " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
inner Builder -> Builder -> Builder
`sp` Builder
idxSMT Builder -> Builder -> Builder
`sp` Builder
byteSMT Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")")

encodeConcreteStore :: Map W256 W256 -> Err Builder
encodeConcreteStore :: Map W256 W256 -> Err Builder
encodeConcreteStore Map W256 W256
s = (Builder -> (W256, W256) -> Err Builder)
-> Builder -> [(W256, W256)] -> Err Builder
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Builder -> (W256, W256) -> Err Builder
encodeWrite (Builder
"((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000)") (Map W256 W256 -> [(W256, W256)]
forall k a. Map k a -> [(k, a)]
Map.toList Map W256 W256
s)
  where
    encodeWrite :: Builder -> (W256, W256) -> Err Builder
    encodeWrite :: Builder -> (W256, W256) -> Err Builder
encodeWrite Builder
prev (W256
key, W256
val) = do
      Builder
encKey <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Expr 'EWord -> Err Builder) -> Expr 'EWord -> Err Builder
forall a b. (a -> b) -> a -> b
$ W256 -> Expr 'EWord
Lit W256
key
      Builder
encVal <- Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT (Expr 'EWord -> Err Builder) -> Expr 'EWord -> Err Builder
forall a b. (a -> b) -> a -> b
$ W256 -> Expr 'EWord
Lit W256
val
      Builder -> Err Builder
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> Err Builder) -> Builder -> Err Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(store " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
prev Builder -> Builder -> Builder
`sp` Builder
encKey Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

storeName :: Expr EAddr -> Maybe W256 -> Builder
storeName :: Expr 'EAddr -> Maybe W256 -> Builder
storeName Expr 'EAddr
a Maybe W256
Nothing = [Char] -> Builder
fromString ([Char]
"baseStore_") Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Expr 'EAddr -> Builder
formatEAddr Expr 'EAddr
a
storeName Expr 'EAddr
a (Just W256
idx) = [Char] -> Builder
fromString ([Char]
"baseStore_") Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Expr 'EAddr -> Builder
formatEAddr Expr 'EAddr
a Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"_" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ([Char] -> Builder
fromString ([Char] -> Builder) -> [Char] -> Builder
forall a b. (a -> b) -> a -> b
$ W256 -> [Char]
forall a. Show a => a -> [Char]
show W256
idx)

formatEAddr :: Expr EAddr -> Builder
formatEAddr :: Expr 'EAddr -> Builder
formatEAddr = \case
  LitAddr Addr
a -> [Char] -> Builder
fromString ([Char]
"litaddr_" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Addr -> [Char]
forall a. Show a => a -> [Char]
show Addr
a)
  SymAddr Text
a -> Text -> Builder
fromText (Text
"symaddr_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a)
  GVar GVar 'EAddr
_ -> [Char] -> Builder
forall a. HasCallStack => [Char] -> a
internalError [Char]
"Unexpected GVar"


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

parseAddr :: SpecConstant -> Addr
parseAddr :: SpecConstant -> Addr
parseAddr = SpecConstant -> Addr
forall a. (Num a, Eq a) => SpecConstant -> a
parseSC

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

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

parseW8 :: SpecConstant -> Word8
parseW8 :: SpecConstant -> Word8
parseW8 = SpecConstant -> Word8
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) = (a, [Char]) -> a
forall a b. (a, b) -> a
fst ((a, [Char]) -> a) -> (Text -> (a, [Char])) -> Text -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, [Char])] -> (a, [Char])
forall a. HasCallStack => [a] -> a
head ([(a, [Char])] -> (a, [Char]))
-> (Text -> [(a, [Char])]) -> Text -> (a, [Char])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReadS a
forall a. (Eq a, Num a) => ReadS a
Numeric.readHex ReadS a -> (Text -> [Char]) -> Text -> [(a, [Char])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack (Text -> [Char]) -> (Text -> Text) -> Text -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
T.fromStrict (Text -> a) -> Text -> a
forall a b. (a -> b) -> a -> b
$ Text
a
parseSC (SCBinary Text
a) = (a, [Char]) -> a
forall a b. (a, b) -> a
fst ((a, [Char]) -> a) -> (Text -> (a, [Char])) -> Text -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, [Char])] -> (a, [Char])
forall a. HasCallStack => [a] -> a
head ([(a, [Char])] -> (a, [Char]))
-> (Text -> [(a, [Char])]) -> Text -> (a, [Char])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReadS a
forall a. (Eq a, Num a) => ReadS a
Numeric.readBin ReadS a -> (Text -> [Char]) -> Text -> [(a, [Char])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack (Text -> [Char]) -> (Text -> Text) -> Text -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
T.fromStrict (Text -> a) -> Text -> a
forall a b. (a -> b) -> a -> b
$ Text
a
parseSC SpecConstant
sc = [Char] -> a
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> SpecConstant -> [Char]
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 = [Char] -> b
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> b) -> [Char] -> b
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse solver response: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show a
res

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

parseEAddr :: TS.Text -> Expr EAddr
parseEAddr :: Text -> Expr 'EAddr
parseEAddr Text
name
  | Just Text
a <- Text -> Text -> Maybe Text
TS.stripPrefix Text
"litaddr_" Text
name = Addr -> Expr 'EAddr
LitAddr ([Char] -> Addr
forall a. Read a => [Char] -> a
read (Text -> [Char]
TS.unpack Text
a))
  | Just Text
a <- Text -> Text -> Maybe Text
TS.stripPrefix Text
"symaddr_" Text
name = Text -> Expr 'EAddr
SymAddr Text
a
  | Bool
otherwise = [Char] -> Expr 'EAddr
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Expr 'EAddr) -> [Char] -> Expr 'EAddr
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
forall a. Show a => a -> [Char]
show Text
name

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 = [Char] -> Expr 'EWord
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Expr 'EWord) -> [Char] -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Text -> [Char]
TS.unpack Text
t) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" into an Expr"

parseTxCtx :: TS.Text -> Expr EWord
parseTxCtx :: Text -> Expr 'EWord
parseTxCtx Text
name
  | Text
name Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"txvalue" = Expr 'EWord
TxValue
  | Just Text
a <- Text -> Text -> Maybe Text
TS.stripPrefix Text
"balance_" Text
name = Expr 'EAddr -> Expr 'EWord
Balance (Text -> Expr 'EAddr
parseEAddr Text
a)
  | Bool
otherwise = [Char] -> Expr 'EWord
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Expr 'EWord) -> [Char] -> Expr 'EWord
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Text -> [Char]
TS.unpack Text
name) [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" into an Expr"

getAddrs :: (TS.Text -> Expr EAddr) -> (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr EAddr) Addr)
getAddrs :: (Text -> Expr 'EAddr)
-> (Text -> IO Text) -> [Text] -> IO (Map (Expr 'EAddr) Addr)
getAddrs Text -> Expr 'EAddr
parseName Text -> IO Text
getVal [Text]
names = (Text -> Expr 'EAddr) -> Map Text Addr -> Map (Expr 'EAddr) Addr
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Text -> Expr 'EAddr
parseName (Map Text Addr -> Map (Expr 'EAddr) Addr)
-> IO (Map Text Addr) -> IO (Map (Expr 'EAddr) Addr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Map Text Addr -> Text -> IO (Map Text Addr))
-> Map Text Addr -> [Text] -> IO (Map Text Addr)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((SpecConstant -> Addr)
-> (Text -> IO Text) -> Map Text Addr -> Text -> IO (Map Text Addr)
forall a.
(SpecConstant -> a)
-> (Text -> IO Text) -> Map Text a -> Text -> IO (Map Text a)
getOne SpecConstant -> Addr
parseAddr Text -> IO Text
getVal) Map Text Addr
forall a. Monoid a => a
mempty [Text]
names

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
parseName Text -> IO Text
getVal [Text]
names = (Text -> Expr 'EWord) -> Map Text W256 -> Map (Expr 'EWord) W256
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Text -> Expr 'EWord
parseName (Map Text W256 -> Map (Expr 'EWord) W256)
-> IO (Map Text W256) -> IO (Map (Expr 'EWord) W256)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Map Text W256 -> Text -> IO (Map Text W256))
-> Map Text W256 -> [Text] -> IO (Map Text W256)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((SpecConstant -> W256)
-> (Text -> IO Text) -> Map Text W256 -> Text -> IO (Map Text W256)
forall a.
(SpecConstant -> a)
-> (Text -> IO Text) -> Map Text a -> Text -> IO (Map Text a)
getOne SpecConstant -> W256
parseW256 Text -> IO Text
getVal) Map Text W256
forall a. Monoid a => a
mempty [Text]
names

getOne :: (SpecConstant -> a) -> (Text -> IO Text) -> Map TS.Text a -> TS.Text -> IO (Map TS.Text a)
getOne :: forall a.
(SpecConstant -> a)
-> (Text -> IO Text) -> Map Text a -> Text -> IO (Map Text a)
getOne SpecConstant -> a
parseVal Text -> IO Text
getVal Map Text a
acc Text
name = do
  Text
raw <- Text -> IO Text
getVal (Text -> Text
T.fromStrict Text
name)
  let
    parsed :: ValuationPair
parsed = case Parser GetValueRes -> Text -> Either Text GetValueRes
forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser GetValueRes
forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
raw) of
      Right (ResSpecific (ValuationPair
valParsed :| [])) -> ValuationPair
valParsed
      Either Text GetValueRes
r -> Either Text GetValueRes -> ValuationPair
forall a b. Show a => a -> b
parseErr Either Text GetValueRes
r
    val :: a
val = case ValuationPair
parsed of
      (TermQualIdentifier (
        Unqualified (IdSymbol Text
symbol)),
        TermSpecConstant SpecConstant
sc)
          -> if Text
symbol Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
name
             then SpecConstant -> a
parseVal SpecConstant
sc
             else [Char] -> a
forall a. HasCallStack => [Char] -> a
internalError [Char]
"solver did not return model for requested value"
      ValuationPair
r -> ValuationPair -> a
forall a b. Show a => a -> b
parseErr ValuationPair
r
  Map Text a -> IO (Map Text a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map Text a -> IO (Map Text a)) -> Map Text a -> IO (Map Text a)
forall a b. (a -> b) -> a -> b
$ Text -> a -> Map Text a -> Map Text a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name a
val Map Text a
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 = (Expr 'EWord -> IO W256)
-> Map Text (Expr 'EWord) -> IO (Map Text W256)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map Text a -> m (Map Text 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 = (Map (Expr 'Buf) BufModel -> Text -> IO (Map (Expr 'Buf) BufModel))
-> Map (Expr 'Buf) BufModel
-> [Text]
-> IO (Map (Expr 'Buf) BufModel)
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 Map (Expr 'Buf) BufModel
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 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_length ")
      W256 -> IO W256
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (W256 -> IO W256) -> W256 -> IO W256
forall a b. (a -> b) -> a -> b
$ case Parser GetValueRes -> Text -> Either Text GetValueRes
forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser GetValueRes
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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== (Text -> Text
T.toStrict (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_length")
               then SpecConstant -> W256
parseW256 SpecConstant
sc
               else [Char] -> W256
forall a. HasCallStack => [Char] -> a
internalError [Char]
"solver did not return model for requested value"
          ValuationPair
res -> ValuationPair -> W256
forall a b. Show a => a -> b
parseErr ValuationPair
res
        Either Text GetValueRes
res -> Either Text GetValueRes -> W256
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 Parser GetValueRes -> Text -> Either Text GetValueRes
forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser GetValueRes
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) Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
name
               then BufModel -> IO BufModel
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BufModel -> IO BufModel) -> BufModel -> IO BufModel
forall a b. (a -> b) -> a -> b
$ W256 -> Term -> BufModel
parseBuf W256
len Term
term
               else [Char] -> IO BufModel
forall a. HasCallStack => [Char] -> a
internalError [Char]
"solver did not return model for requested value"
          ValuationPair
res -> [Char] -> IO BufModel
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> IO BufModel) -> [Char] -> IO BufModel
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse solver response: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> ValuationPair -> [Char]
forall a. Show a => a -> [Char]
show ValuationPair
res
        Either Text GetValueRes
res -> [Char] -> IO BufModel
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> IO BufModel) -> [Char] -> IO BufModel
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse solver response: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Either Text GetValueRes -> [Char]
forall a. Show a => a -> [Char]
show Either Text GetValueRes
res
      Map (Expr 'Buf) BufModel -> IO (Map (Expr 'Buf) BufModel)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map (Expr 'Buf) BufModel -> IO (Map (Expr 'Buf) BufModel))
-> Map (Expr 'Buf) BufModel -> IO (Map (Expr 'Buf) BufModel)
forall a b. (a -> b) -> a -> b
$ Expr 'Buf
-> BufModel -> Map (Expr 'Buf) BufModel -> Map (Expr 'Buf) BufModel
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Text -> Expr 'Buf
AbstractBuf (Text -> Expr 'Buf) -> Text -> Expr 'Buf
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 (CompressedBuf -> BufModel)
-> (Term -> CompressedBuf) -> Term -> BufModel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Text CompressedBuf -> Term -> CompressedBuf
go Map Text CompressedBuf
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 (Text
-> CompressedBuf
-> Map Text CompressedBuf
-> Map Text CompressedBuf
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 Text -> Map Text CompressedBuf -> Maybe CompressedBuf
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 -> [Char] -> CompressedBuf
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> CompressedBuf) -> [Char] -> CompressedBuf
forall a b. (a -> b) -> a -> b
$ [Char]
"could not find "
                            [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Text -> [Char]
TS.unpack Text
name)
                            [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
" in environment mapping"
          Term
p -> Term -> CompressedBuf
forall a b. Show a => a -> b
parseErr Term
p

-- | Takes a Map containing all reads from a store with an abstract base, as
-- well as the concrete part of the storage prestate and returns a fully
-- concretized storage
getStore
  :: (Text -> IO Text)
  -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord))
  -> IO (Map (Expr EAddr) (Map W256 W256))
getStore :: (Text -> IO Text)
-> Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
-> IO (Map (Expr 'EAddr) (Map W256 W256))
getStore Text -> IO Text
getVal Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
abstractReads =
  ([(Expr 'EAddr, Map W256 W256)]
 -> Map (Expr 'EAddr) (Map W256 W256))
-> IO [(Expr 'EAddr, Map W256 W256)]
-> IO (Map (Expr 'EAddr) (Map W256 W256))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Expr 'EAddr, Map W256 W256)] -> Map (Expr 'EAddr) (Map W256 W256)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (IO [(Expr 'EAddr, Map W256 W256)]
 -> IO (Map (Expr 'EAddr) (Map W256 W256)))
-> IO [(Expr 'EAddr, Map W256 W256)]
-> IO (Map (Expr 'EAddr) (Map W256 W256))
forall a b. (a -> b) -> a -> b
$ [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
-> (((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))
    -> IO (Expr 'EAddr, Map W256 W256))
-> IO [(Expr 'EAddr, Map W256 W256)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
-> [((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord))
abstractReads) ((((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))
  -> IO (Expr 'EAddr, Map W256 W256))
 -> IO [(Expr 'EAddr, Map W256 W256)])
-> (((Expr 'EAddr, Maybe W256), Set (Expr 'EWord))
    -> IO (Expr 'EAddr, Map W256 W256))
-> IO [(Expr 'EAddr, Map W256 W256)]
forall a b. (a -> b) -> a -> b
$ \((Expr 'EAddr
addr, Maybe W256
idx), Set (Expr 'EWord)
slots) -> do
    let name :: Text
name = Builder -> Text
toLazyText (Expr 'EAddr -> Maybe W256 -> Builder
storeName Expr 'EAddr
addr Maybe W256
idx)
    Text
raw <- Text -> IO Text
getVal Text
name
    let parsed :: ValuationPair
parsed = case Parser GetValueRes -> Text -> Either Text GetValueRes
forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser GetValueRes
forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
raw) of
                   Right (ResSpecific (ValuationPair
valParsed :| [])) -> ValuationPair
valParsed
                   Either Text GetValueRes
r -> Either Text GetValueRes -> ValuationPair
forall a b. Show a => a -> b
parseErr Either Text GetValueRes
r
        -- first interpret SMT term as a function
        fun :: W256 -> W256
fun = case ValuationPair
parsed of
                (TermQualIdentifier (Unqualified (IdSymbol Text
symbol)), Term
term) ->
                  if Text
symbol Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== (Text -> Text
T.toStrict Text
name)
                  then Map Text Term -> Term -> W256 -> W256
interpret1DArray Map Text Term
forall k a. Map k a
Map.empty Term
term
                  else [Char] -> W256 -> W256
forall a. HasCallStack => [Char] -> a
internalError [Char]
"solver did not return model for requested value"
                ValuationPair
r -> ValuationPair -> W256 -> W256
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
    Map W256 W256
store <- (Map W256 W256 -> Expr 'EWord -> IO (Map W256 W256))
-> Map W256 W256 -> Set (Expr 'EWord) -> IO (Map W256 W256)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Map W256 W256
m Expr 'EWord
slot -> do
      W256
slot' <- (Text -> IO Text) -> Expr 'EWord -> IO W256
queryValue Text -> IO Text
getVal Expr 'EWord
slot
      Map W256 W256 -> IO (Map W256 W256)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map W256 W256 -> IO (Map W256 W256))
-> Map W256 W256 -> IO (Map W256 W256)
forall a b. (a -> b) -> a -> b
$ W256 -> W256 -> Map W256 W256 -> Map W256 W256
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert W256
slot' (W256 -> W256
fun W256
slot') Map W256 W256
m) Map W256 W256
forall k a. Map k a
Map.empty Set (Expr 'EWord)
slots
    (Expr 'EAddr, Map W256 W256) -> IO (Expr 'EAddr, Map W256 W256)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'EAddr
addr, Map W256 W256
store)

-- | Ask the solver to give us the concrete value of an arbitrary abstract word
queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256
queryValue :: (Text -> IO Text) -> Expr 'EWord -> IO W256
queryValue Text -> IO Text
_ (Lit W256
w) = W256 -> IO W256
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure W256
w
queryValue Text -> IO Text
getVal Expr 'EWord
w = do
  -- this exprToSMT should never fail, since we have already ran the solver
  let expr :: Text
expr = Builder -> Text
toLazyText (Builder -> Text) -> Builder -> Text
forall a b. (a -> b) -> a -> b
$ Err Builder -> Builder
forall l r. HasCallStack => Either l r -> r
fromRight' (Err Builder -> Builder) -> Err Builder -> Builder
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Err Builder
forall (a :: EType). Expr a -> Err Builder
exprToSMT Expr 'EWord
w
  Text
raw <- Text -> IO Text
getVal Text
expr
  case Parser GetValueRes -> Text -> Either Text GetValueRes
forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg Parser GetValueRes
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) -> W256 -> IO W256
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (W256 -> IO W256) -> W256 -> IO W256
forall a b. (a -> b) -> a -> b
$ SpecConstant -> W256
parseW256 SpecConstant
sc
        ValuationPair
_ -> [Char] -> IO W256
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> IO W256) -> [Char] -> IO W256
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse model for: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Expr 'EWord -> [Char]
forall a. Show a => a -> [Char]
show Expr 'EWord
w
    Either Text GetValueRes
r -> Either Text GetValueRes -> IO W256
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 Text -> Map Text Term -> Maybe Term
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 -> a) -> Map Text Term -> Term -> W256 -> a
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 -> [Char] -> W256 -> a
forall a. HasCallStack => [Char] -> a
internalError [Char]
"unknown identifier, cannot parse array"
  -- (let (x t') t)
  TermLet (VarBinding Text
x Term
t' :| []) Term
t -> (Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> a
interp (Text -> Term -> Map Text Term -> Map Text Term
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 -> (Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
forall a.
(Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
interpretNDArray Map Text Term -> Term -> a
interp (Text -> Term -> Map Text Term -> Map Text Term
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 ([VarBinding] -> NonEmpty VarBinding
forall a. HasCallStack => [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 W256 -> W256 -> Bool
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 (Map Text Term -> Term -> a) -> Map Text Term -> Term -> W256 -> a
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 -> [Char] -> W256 -> a
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> W256 -> a) -> [Char] -> W256 -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse array value. Unexpected term: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Term -> [Char]
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 QualIdentifier -> QualIdentifier -> Bool
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 = (Map Text Term -> Term -> W256)
-> Map Text Term -> Term -> W256 -> W256
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 Text -> Map Text Term -> Maybe Term
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 -> [Char] -> W256
forall a. HasCallStack => [Char] -> a
internalError [Char]
"unknown identifier, cannot parse array"
    interpretW256 Map Text Term
_ Term
t = [Char] -> W256
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> W256) -> [Char] -> W256
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot parse array value. Unexpected term: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Term -> [Char]
forall a. Show a => a -> [Char]
show Term
t)