{-# Language DataKinds #-}
{-# Language GADTs #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
{-# Language QuasiQuotes #-}
module EVM.SMT where
import Prelude hiding (LT, GT)
import GHC.Natural
import Control.Monad
import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..))
import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
import Control.Concurrent (forkIO, killThread)
import Data.Char (isSpace)
import Data.Containers.ListUtils (nubOrd)
import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)
import Language.SMT2.Syntax (SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))
import Data.Word
import Numeric (readHex)
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty((:|)))
import Data.String.Here
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Text.Lazy (Text)
import qualified Data.Text as TS
import qualified Data.Text.Lazy as T
import qualified Data.Text.Lazy.IO as T
import Data.Text.Lazy.Builder
import Data.Bifunctor (second)
import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))
import EVM.Types
import EVM.Traversals
import EVM.CSE
import EVM.Keccak
import EVM.Expr hiding (copySlice, writeWord, op1, op2, op3, drop)
data CexVars = CexVars
{ CexVars -> [Text]
calldataV :: [Text]
, CexVars -> [Text]
buffersV :: [Text]
, CexVars -> [Text]
blockContextV :: [Text]
, CexVars -> [Text]
txContextV :: [Text]
}
deriving (CexVars -> CexVars -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CexVars -> CexVars -> Bool
$c/= :: CexVars -> CexVars -> Bool
== :: CexVars -> CexVars -> Bool
$c== :: CexVars -> CexVars -> Bool
Eq, Int -> CexVars -> ShowS
[CexVars] -> ShowS
CexVars -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CexVars] -> ShowS
$cshowList :: [CexVars] -> ShowS
show :: CexVars -> String
$cshow :: CexVars -> String
showsPrec :: Int -> CexVars -> ShowS
$cshowsPrec :: Int -> CexVars -> ShowS
Show)
instance Semigroup CexVars where
(CexVars [Text]
a [Text]
b [Text]
c [Text]
d) <> :: CexVars -> CexVars -> CexVars
<> (CexVars [Text]
a2 [Text]
b2 [Text]
c2 [Text]
d2) = [Text] -> [Text] -> [Text] -> [Text] -> CexVars
CexVars ([Text]
a forall a. Semigroup a => a -> a -> a
<> [Text]
a2) ([Text]
b forall a. Semigroup a => a -> a -> a
<> [Text]
b2) ([Text]
c forall a. Semigroup a => a -> a -> a
<> [Text]
c2) ([Text]
d forall a. Semigroup a => a -> a -> a
<> [Text]
d2)
instance Monoid CexVars where
mempty :: CexVars
mempty = CexVars
{ calldataV :: [Text]
calldataV = forall a. Monoid a => a
mempty
, buffersV :: [Text]
buffersV = forall a. Monoid a => a
mempty
, blockContextV :: [Text]
blockContextV = forall a. Monoid a => a
mempty
, txContextV :: [Text]
txContextV = forall a. Monoid a => a
mempty
}
data SMTCex = SMTCex
{ SMTCex -> Map (Expr 'EWord) W256
vars :: Map (Expr EWord) W256
, SMTCex -> Map (Expr 'Buf) ByteString
buffers :: Map (Expr Buf) ByteString
, SMTCex -> Map (Expr 'EWord) W256
blockContext :: Map (Expr EWord) W256
, SMTCex -> Map (Expr 'EWord) W256
txContext :: Map (Expr EWord) W256
}
deriving (SMTCex -> SMTCex -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTCex -> SMTCex -> Bool
$c/= :: SMTCex -> SMTCex -> Bool
== :: SMTCex -> SMTCex -> Bool
$c== :: SMTCex -> SMTCex -> Bool
Eq, Int -> SMTCex -> ShowS
[SMTCex] -> ShowS
SMTCex -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMTCex] -> ShowS
$cshowList :: [SMTCex] -> ShowS
show :: SMTCex -> String
$cshow :: SMTCex -> String
showsPrec :: Int -> SMTCex -> ShowS
$cshowsPrec :: Int -> SMTCex -> ShowS
Show)
getVar :: EVM.SMT.SMTCex -> TS.Text -> W256
getVar :: SMTCex -> Text -> W256
getVar SMTCex
cex Text
name = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Text -> Expr 'EWord
Var Text
name) (SMTCex -> Map (Expr 'EWord) W256
vars SMTCex
cex)
data SMT2 = SMT2 [Builder] CexVars
deriving (SMT2 -> SMT2 -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMT2 -> SMT2 -> Bool
$c/= :: SMT2 -> SMT2 -> Bool
== :: SMT2 -> SMT2 -> Bool
$c== :: SMT2 -> SMT2 -> Bool
Eq, Int -> SMT2 -> ShowS
[SMT2] -> ShowS
SMT2 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMT2] -> ShowS
$cshowList :: [SMT2] -> ShowS
show :: SMT2 -> String
$cshow :: SMT2 -> String
showsPrec :: Int -> SMT2 -> ShowS
$cshowsPrec :: Int -> SMT2 -> ShowS
Show)
instance Semigroup SMT2 where
(SMT2 [Builder]
a CexVars
b) <> :: SMT2 -> SMT2 -> SMT2
<> (SMT2 [Builder]
a2 CexVars
b2) = [Builder] -> CexVars -> SMT2
SMT2 ([Builder]
a forall a. Semigroup a => a -> a -> a
<> [Builder]
a2) (CexVars
b forall a. Semigroup a => a -> a -> a
<> CexVars
b2)
instance Monoid SMT2 where
mempty :: SMT2
mempty = [Builder] -> CexVars -> SMT2
SMT2 forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
formatSMT2 :: SMT2 -> Text
formatSMT2 :: SMT2 -> Text
formatSMT2 (SMT2 [Builder]
ls CexVars
_) = [Text] -> Text
T.unlines (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
ls)
declareIntermediates :: BufEnv -> StoreEnv -> SMT2
declareIntermediates :: BufEnv -> StoreEnv -> SMT2
declareIntermediates BufEnv
bufs StoreEnv
stores =
let encSs :: Map Int Builder
encSs = forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey forall {p} {a :: EType}. Show p => p -> Expr a -> Builder
encodeStore StoreEnv
stores
encBs :: Map Int Builder
encBs = forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey forall {p} {a :: EType}. Show p => p -> Expr a -> Builder
encodeBuf BufEnv
bufs
sorted :: [(Int, Builder)]
sorted = forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy forall {a} {b} {b}. Ord a => (a, b) -> (a, b) -> Ordering
compareFst forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ Map Int Builder
encSs forall a. Semigroup a => a -> a -> a
<> Map Int Builder
encBs
decls :: [Builder]
decls = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd [(Int, Builder)]
sorted
in [Builder] -> CexVars -> SMT2
SMT2 ([Text -> Builder
fromText Text
"; intermediate buffers & stores"] forall a. Semigroup a => a -> a -> a
<> [Builder]
decls) forall a. Monoid a => a
mempty
where
compareFst :: (a, b) -> (a, b) -> Ordering
compareFst (a
l, b
_) (a
r, b
_) = forall a. Ord a => a -> a -> Ordering
compare a
l a
r
encodeBuf :: p -> Expr a -> Builder
encodeBuf p
n Expr a
expr =
Text -> Builder
fromLazyText (Text
"(define-const buf" forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ p
n) forall a. Semigroup a => a -> a -> a
<> Text
" Buf ") forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
expr forall a. Semigroup a => a -> a -> a
<> Builder
")"
encodeStore :: p -> Expr a -> Builder
encodeStore p
n Expr a
expr =
Text -> Builder
fromLazyText (Text
"(define-const store" forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ p
n) forall a. Semigroup a => a -> a -> a
<> Text
" Storage ") forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
expr forall a. Semigroup a => a -> a -> a
<> Builder
")"
assertProps :: [Prop] -> SMT2
assertProps :: [Prop] -> SMT2
assertProps [Prop]
ps =
let encs :: [Builder]
encs = forall a b. (a -> b) -> [a] -> [b]
map Prop -> Builder
propToSMT [Prop]
ps_elim
intermediates :: SMT2
intermediates = BufEnv -> StoreEnv -> SMT2
declareIntermediates BufEnv
bufs StoreEnv
stores in
SMT2
prelude
forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareBufs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) [] [[Builder]]
allBufs)
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) [] [[Builder]]
allVars)
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareFrameContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) [] [[Builder]]
frameCtx)
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
forall a. Semigroup a => a -> a -> a
<> ([Builder] -> SMT2
declareBlockContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) [] [[Builder]]
blockCtx)
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
forall a. Semigroup a => a -> a -> a
<> SMT2
intermediates
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
forall a. Semigroup a => a -> a -> a
<> SMT2
keccakAssumes
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 [Builder
""] forall a. Monoid a => a
mempty
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Builder
p -> Builder
"(assert " forall a. Semigroup a => a -> a -> a
<> Builder
p forall a. Semigroup a => a -> a -> a
<> Builder
")") [Builder]
encs) forall a. Monoid a => a
mempty
where
([Prop]
ps_elim, BufEnv
bufs, StoreEnv
stores) = [Prop] -> ([Prop], BufEnv, StoreEnv)
eliminateProps [Prop]
ps
allBufs :: [[Builder]]
allBufs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
referencedBufs' [Prop]
ps_elim forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedBufs [Expr 'Buf]
bufVals forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedBufs [Expr 'Storage]
storeVals
allVars :: [[Builder]]
allVars = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
referencedVars' [Prop]
ps_elim forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedVars [Expr 'Buf]
bufVals forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedVars [Expr 'Storage]
storeVals
frameCtx :: [[Builder]]
frameCtx = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
referencedFrameContext' [Prop]
ps_elim forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedFrameContext [Expr 'Buf]
bufVals forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedFrameContext [Expr 'Storage]
storeVals
blockCtx :: [[Builder]]
blockCtx = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> [Builder]
referencedBlockContext' [Prop]
ps_elim forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedBlockContext [Expr 'Buf]
bufVals forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> [Builder]
referencedBlockContext [Expr 'Storage]
storeVals
bufVals :: [Expr 'Buf]
bufVals = forall k a. Map k a -> [a]
Map.elems BufEnv
bufs
storeVals :: [Expr 'Storage]
storeVals = forall k a. Map k a -> [a]
Map.elems StoreEnv
stores
keccakAssumes :: SMT2
keccakAssumes
= [Builder] -> CexVars -> SMT2
SMT2 [Builder
"; keccak assumptions"] forall a. Monoid a => a
mempty
forall a. Semigroup a => a -> a -> a
<> [Builder] -> CexVars -> SMT2
SMT2 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Prop
p -> Builder
"(assert " forall a. Semigroup a => a -> a -> a
<> Prop -> Builder
propToSMT Prop
p forall a. Semigroup a => a -> a -> a
<> Builder
")") ([Prop] -> [Expr 'Buf] -> [Expr 'Storage] -> [Prop]
keccakAssumptions [Prop]
ps_elim [Expr 'Buf]
bufVals [Expr 'Storage]
storeVals)) forall a. Monoid a => a
mempty
prelude :: SMT2
prelude :: SMT2
prelude = (forall a b c. (a -> b -> c) -> b -> a -> c
flip [Builder] -> CexVars -> SMT2
SMT2) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Builder
fromLazyText forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Text -> Text
T.drop Int64
2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Text]
T.lines forall a b. (a -> b) -> a -> b
$ [i|
; logic
; TODO: this creates an error when used with z3?
;(set-logic QF_AUFBV)
(set-logic ALL)
; types
(define-sort Byte () (_ BitVec 8))
(define-sort Word () (_ BitVec 256))
(define-sort Buf () (Array Word Byte))
; address -> slot -> value
(define-sort Storage () (Array Word (Array Word Word)))
; hash functions
(declare-fun keccak (Buf) Word)
(declare-fun sha256 (Buf) Word)
; word indexing
(define-fun indexWord31 ((w Word)) Byte ((_ extract 7 0) w))
(define-fun indexWord30 ((w Word)) Byte ((_ extract 15 8) w))
(define-fun indexWord29 ((w Word)) Byte ((_ extract 23 16) w))
(define-fun indexWord28 ((w Word)) Byte ((_ extract 31 24) w))
(define-fun indexWord27 ((w Word)) Byte ((_ extract 39 32) w))
(define-fun indexWord26 ((w Word)) Byte ((_ extract 47 40) w))
(define-fun indexWord25 ((w Word)) Byte ((_ extract 55 48) w))
(define-fun indexWord24 ((w Word)) Byte ((_ extract 63 56) w))
(define-fun indexWord23 ((w Word)) Byte ((_ extract 71 64) w))
(define-fun indexWord22 ((w Word)) Byte ((_ extract 79 72) w))
(define-fun indexWord21 ((w Word)) Byte ((_ extract 87 80) w))
(define-fun indexWord20 ((w Word)) Byte ((_ extract 95 88) w))
(define-fun indexWord19 ((w Word)) Byte ((_ extract 103 96) w))
(define-fun indexWord18 ((w Word)) Byte ((_ extract 111 104) w))
(define-fun indexWord17 ((w Word)) Byte ((_ extract 119 112) w))
(define-fun indexWord16 ((w Word)) Byte ((_ extract 127 120) w))
(define-fun indexWord15 ((w Word)) Byte ((_ extract 135 128) w))
(define-fun indexWord14 ((w Word)) Byte ((_ extract 143 136) w))
(define-fun indexWord13 ((w Word)) Byte ((_ extract 151 144) w))
(define-fun indexWord12 ((w Word)) Byte ((_ extract 159 152) w))
(define-fun indexWord11 ((w Word)) Byte ((_ extract 167 160) w))
(define-fun indexWord10 ((w Word)) Byte ((_ extract 175 168) w))
(define-fun indexWord9 ((w Word)) Byte ((_ extract 183 176) w))
(define-fun indexWord8 ((w Word)) Byte ((_ extract 191 184) w))
(define-fun indexWord7 ((w Word)) Byte ((_ extract 199 192) w))
(define-fun indexWord6 ((w Word)) Byte ((_ extract 207 200) w))
(define-fun indexWord5 ((w Word)) Byte ((_ extract 215 208) w))
(define-fun indexWord4 ((w Word)) Byte ((_ extract 223 216) w))
(define-fun indexWord3 ((w Word)) Byte ((_ extract 231 224) w))
(define-fun indexWord2 ((w Word)) Byte ((_ extract 239 232) w))
(define-fun indexWord1 ((w Word)) Byte ((_ extract 247 240) w))
(define-fun indexWord0 ((w Word)) Byte ((_ extract 255 248) w))
; symbolic word indexing
; a bitshift based version might be more performant here...
(define-fun indexWord ((idx Word) (w Word)) Byte
(ite (bvuge idx (_ bv32 256)) (_ bv0 8)
(ite (= idx (_ bv31 256)) (indexWord31 w)
(ite (= idx (_ bv30 256)) (indexWord30 w)
(ite (= idx (_ bv29 256)) (indexWord29 w)
(ite (= idx (_ bv28 256)) (indexWord28 w)
(ite (= idx (_ bv27 256)) (indexWord27 w)
(ite (= idx (_ bv26 256)) (indexWord26 w)
(ite (= idx (_ bv25 256)) (indexWord25 w)
(ite (= idx (_ bv24 256)) (indexWord24 w)
(ite (= idx (_ bv23 256)) (indexWord23 w)
(ite (= idx (_ bv22 256)) (indexWord22 w)
(ite (= idx (_ bv21 256)) (indexWord21 w)
(ite (= idx (_ bv20 256)) (indexWord20 w)
(ite (= idx (_ bv19 256)) (indexWord19 w)
(ite (= idx (_ bv18 256)) (indexWord18 w)
(ite (= idx (_ bv17 256)) (indexWord17 w)
(ite (= idx (_ bv16 256)) (indexWord16 w)
(ite (= idx (_ bv15 256)) (indexWord15 w)
(ite (= idx (_ bv14 256)) (indexWord14 w)
(ite (= idx (_ bv13 256)) (indexWord13 w)
(ite (= idx (_ bv12 256)) (indexWord12 w)
(ite (= idx (_ bv11 256)) (indexWord11 w)
(ite (= idx (_ bv10 256)) (indexWord10 w)
(ite (= idx (_ bv9 256)) (indexWord9 w)
(ite (= idx (_ bv8 256)) (indexWord8 w)
(ite (= idx (_ bv7 256)) (indexWord7 w)
(ite (= idx (_ bv6 256)) (indexWord6 w)
(ite (= idx (_ bv5 256)) (indexWord5 w)
(ite (= idx (_ bv4 256)) (indexWord4 w)
(ite (= idx (_ bv3 256)) (indexWord3 w)
(ite (= idx (_ bv2 256)) (indexWord2 w)
(ite (= idx (_ bv1 256)) (indexWord1 w)
(indexWord0 w)
))))))))))))))))))))))))))))))))
)
; buffers
(declare-fun bufLength (Buf) Word)
(define-const emptyBuf Buf ((as const Buf) #b00000000))
(define-fun readWord ((idx Word) (buf Buf)) Word
(concat
(select buf idx)
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000001))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000002))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000003))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000004))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000005))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000006))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000007))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000008))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000009))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000a))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000b))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000c))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000d))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000e))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000000f))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000010))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000011))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000012))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000013))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000014))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000015))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000016))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000017))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000018))
(select buf (bvadd idx #x0000000000000000000000000000000000000000000000000000000000000019))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001a))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001b))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001c))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001d))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001e))
(select buf (bvadd idx #x000000000000000000000000000000000000000000000000000000000000001f))
)
)
(define-fun writeWord ((idx Word) (val Word) (buf Buf)) Buf
(store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store
(store (store (store (store (store (store (store (store (store (store (store (store (store (store (store buf
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000001f) (indexWord31 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000001e) (indexWord30 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000001d) (indexWord29 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000001c) (indexWord28 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000001b) (indexWord27 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000001a) (indexWord26 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000019) (indexWord25 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000018) (indexWord24 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000017) (indexWord23 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000016) (indexWord22 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000015) (indexWord21 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000014) (indexWord20 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000013) (indexWord19 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000012) (indexWord18 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000011) (indexWord17 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000010) (indexWord16 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000000f) (indexWord15 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000000e) (indexWord14 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000000d) (indexWord13 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000000c) (indexWord12 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000000b) (indexWord11 val))
(bvadd idx #x000000000000000000000000000000000000000000000000000000000000000a) (indexWord10 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000009) (indexWord9 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000008) (indexWord8 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000007) (indexWord7 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000006) (indexWord6 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000005) (indexWord5 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000004) (indexWord4 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000003) (indexWord3 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000002) (indexWord2 val))
(bvadd idx #x0000000000000000000000000000000000000000000000000000000000000001) (indexWord1 val))
idx (indexWord0 val))
)
; block context
(declare-fun blockhash (Word) Word)
; macros
(define-fun signext ( (b Word) (val Word)) Word
(ite (= b (_ bv0 256)) ((_ sign_extend 248) ((_ extract 7 0) val))
(ite (= b (_ bv1 256)) ((_ sign_extend 240) ((_ extract 15 0) val))
(ite (= b (_ bv2 256)) ((_ sign_extend 232) ((_ extract 23 0) val))
(ite (= b (_ bv3 256)) ((_ sign_extend 224) ((_ extract 31 0) val))
(ite (= b (_ bv4 256)) ((_ sign_extend 216) ((_ extract 39 0) val))
(ite (= b (_ bv5 256)) ((_ sign_extend 208) ((_ extract 47 0) val))
(ite (= b (_ bv6 256)) ((_ sign_extend 200) ((_ extract 55 0) val))
(ite (= b (_ bv7 256)) ((_ sign_extend 192) ((_ extract 63 0) val))
(ite (= b (_ bv8 256)) ((_ sign_extend 184) ((_ extract 71 0) val))
(ite (= b (_ bv9 256)) ((_ sign_extend 176) ((_ extract 79 0) val))
(ite (= b (_ bv10 256)) ((_ sign_extend 168) ((_ extract 87 0) val))
(ite (= b (_ bv11 256)) ((_ sign_extend 160) ((_ extract 95 0) val))
(ite (= b (_ bv12 256)) ((_ sign_extend 152) ((_ extract 103 0) val))
(ite (= b (_ bv13 256)) ((_ sign_extend 144) ((_ extract 111 0) val))
(ite (= b (_ bv14 256)) ((_ sign_extend 136) ((_ extract 119 0) val))
(ite (= b (_ bv15 256)) ((_ sign_extend 128) ((_ extract 127 0) val))
(ite (= b (_ bv16 256)) ((_ sign_extend 120) ((_ extract 135 0) val))
(ite (= b (_ bv17 256)) ((_ sign_extend 112) ((_ extract 143 0) val))
(ite (= b (_ bv18 256)) ((_ sign_extend 104) ((_ extract 151 0) val))
(ite (= b (_ bv19 256)) ((_ sign_extend 96 ) ((_ extract 159 0) val))
(ite (= b (_ bv20 256)) ((_ sign_extend 88 ) ((_ extract 167 0) val))
(ite (= b (_ bv21 256)) ((_ sign_extend 80 ) ((_ extract 175 0) val))
(ite (= b (_ bv22 256)) ((_ sign_extend 72 ) ((_ extract 183 0) val))
(ite (= b (_ bv23 256)) ((_ sign_extend 64 ) ((_ extract 191 0) val))
(ite (= b (_ bv24 256)) ((_ sign_extend 56 ) ((_ extract 199 0) val))
(ite (= b (_ bv25 256)) ((_ sign_extend 48 ) ((_ extract 207 0) val))
(ite (= b (_ bv26 256)) ((_ sign_extend 40 ) ((_ extract 215 0) val))
(ite (= b (_ bv27 256)) ((_ sign_extend 32 ) ((_ extract 223 0) val))
(ite (= b (_ bv28 256)) ((_ sign_extend 24 ) ((_ extract 231 0) val))
(ite (= b (_ bv29 256)) ((_ sign_extend 16 ) ((_ extract 239 0) val))
(ite (= b (_ bv30 256)) ((_ sign_extend 8 ) ((_ extract 247 0) val)) val))))))))))))))))))))))))))))))))
; storage
(declare-const abstractStore Storage)
(define-const emptyStore Storage ((as const Storage) ((as const (Array (_ BitVec 256) (_ BitVec 256))) #x0000000000000000000000000000000000000000000000000000000000000000)))
(define-fun sstore ((addr Word) (key Word) (val Word) (storage Storage)) Storage (store storage addr (store (select storage addr) key val)))
(define-fun sload ((addr Word) (key Word) (storage Storage)) Word (select (select storage addr) key))
|]
declareBufs :: [Builder] -> SMT2
declareBufs :: [Builder] -> SMT2
declareBufs [Builder]
names = [Builder] -> CexVars -> SMT2
SMT2 (Builder
"; buffers" forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declareBuf [Builder]
names forall a. Semigroup a => a -> a -> a
<> (Builder
"; buffer lengths" forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declareLength [Builder]
names)) CexVars
cexvars
where
declareBuf :: a -> a
declareBuf a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
" (Array (_ BitVec 256) (_ BitVec 8)))"
declareLength :: a -> a
declareLength a
n = a
"(define-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
"_length" forall a. Semigroup a => a -> a -> a
<> a
" (_ BitVec 256) (bufLength " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
"))"
cexvars :: CexVars
cexvars = CexVars
{ calldataV :: [Text]
calldataV = forall a. Monoid a => a
mempty
, buffersV :: [Text]
buffersV = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
names)
, blockContextV :: [Text]
blockContextV = forall a. Monoid a => a
mempty
, txContextV :: [Text]
txContextV = forall a. Monoid a => a
mempty
}
referencedBufs :: Expr a -> [Builder]
referencedBufs :: forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr a
expr = forall a. Ord a => [a] -> [a]
nubOrd (forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> [Builder]
go [] Expr a
expr)
where
go :: Expr a -> [Builder]
go :: forall (a :: EType). Expr a -> [Builder]
go = \case
AbstractBuf Text
s -> [Text -> Builder
fromText Text
s]
Expr a
_ -> []
referencedBufs' :: Prop -> [Builder]
referencedBufs' :: Prop -> [Builder]
referencedBufs' = \case
PEq Expr a
a Expr a
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr a
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr a
b
PLT Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr 'EWord
b
PGT Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr 'EWord
b
PLEq Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr 'EWord
b
PGEq Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBufs Expr 'EWord
b
PAnd Prop
a Prop
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ Prop -> [Builder]
referencedBufs' Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> [Builder]
referencedBufs' Prop
b
POr Prop
a Prop
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ Prop -> [Builder]
referencedBufs' Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> [Builder]
referencedBufs' Prop
b
PNeg Prop
a -> Prop -> [Builder]
referencedBufs' Prop
a
PBool Bool
_ -> []
referencedVars' :: Prop -> [Builder]
referencedVars' :: Prop -> [Builder]
referencedVars' = \case
PEq Expr a
a Expr a
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedVars Expr a
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedVars Expr a
b
PLT Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedVars Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedVars Expr 'EWord
b
PGT Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedVars Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedVars Expr 'EWord
b
PLEq Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedVars Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedVars Expr 'EWord
b
PGEq Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedVars Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedVars Expr 'EWord
b
PAnd Prop
a Prop
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ Prop -> [Builder]
referencedVars' Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> [Builder]
referencedVars' Prop
b
POr Prop
a Prop
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ Prop -> [Builder]
referencedVars' Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> [Builder]
referencedVars' Prop
b
PNeg Prop
a -> Prop -> [Builder]
referencedVars' Prop
a
PBool Bool
_ -> []
referencedFrameContext' :: Prop -> [Builder]
referencedFrameContext' :: Prop -> [Builder]
referencedFrameContext' = \case
PEq Expr a
a Expr a
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr a
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr a
b
PLT Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr 'EWord
b
PGT Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr 'EWord
b
PLEq Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr 'EWord
b
PGEq Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr 'EWord
b
PAnd Prop
a Prop
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ Prop -> [Builder]
referencedFrameContext' Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> [Builder]
referencedFrameContext' Prop
b
POr Prop
a Prop
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ Prop -> [Builder]
referencedFrameContext' Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> [Builder]
referencedFrameContext' Prop
b
PNeg Prop
a -> Prop -> [Builder]
referencedFrameContext' Prop
a
PBool Bool
_ -> []
referencedBlockContext' :: Prop -> [Builder]
referencedBlockContext' :: Prop -> [Builder]
referencedBlockContext' = \case
PEq Expr a
a Expr a
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr a
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr a
b
PLT Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr 'EWord
b
PGT Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr 'EWord
b
PLEq Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr 'EWord
b
PGEq Expr 'EWord
a Expr 'EWord
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr 'EWord
b
PAnd Prop
a Prop
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ Prop -> [Builder]
referencedBlockContext' Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> [Builder]
referencedBlockContext' Prop
b
POr Prop
a Prop
b -> forall a. Ord a => [a] -> [a]
nubOrd forall a b. (a -> b) -> a -> b
$ Prop -> [Builder]
referencedBlockContext' Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> [Builder]
referencedBlockContext' Prop
b
PNeg Prop
a -> Prop -> [Builder]
referencedBlockContext' Prop
a
PBool Bool
_ -> []
declareVars :: [Builder] -> SMT2
declareVars :: [Builder] -> SMT2
declareVars [Builder]
names = [Builder] -> CexVars -> SMT2
SMT2 ([Builder
"; variables"] forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
cexvars
where
declare :: a -> a
declare a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
" (_ BitVec 256))"
cexvars :: CexVars
cexvars = CexVars
{ calldataV :: [Text]
calldataV = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
names
, buffersV :: [Text]
buffersV = forall a. Monoid a => a
mempty
, blockContextV :: [Text]
blockContextV = forall a. Monoid a => a
mempty
, txContextV :: [Text]
txContextV = forall a. Monoid a => a
mempty
}
referencedVars :: Expr a -> [Builder]
referencedVars :: forall (a :: EType). Expr a -> [Builder]
referencedVars Expr a
expr = forall a. Ord a => [a] -> [a]
nubOrd (forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> [Builder]
go [] Expr a
expr)
where
go :: Expr a -> [Builder]
go :: forall (a :: EType). Expr a -> [Builder]
go = \case
Var Text
s -> [Text -> Builder
fromText Text
s]
Expr a
_ -> []
declareFrameContext :: [Builder] -> SMT2
declareFrameContext :: [Builder] -> SMT2
declareFrameContext [Builder]
names = [Builder] -> CexVars -> SMT2
SMT2 ([Builder
"; frame context"] forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
cexvars
where
declare :: a -> a
declare a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
" (_ BitVec 256))"
cexvars :: CexVars
cexvars = CexVars
{ calldataV :: [Text]
calldataV = forall a. Monoid a => a
mempty
, buffersV :: [Text]
buffersV = forall a. Monoid a => a
mempty
, blockContextV :: [Text]
blockContextV = forall a. Monoid a => a
mempty
, txContextV :: [Text]
txContextV = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
names
}
referencedFrameContext :: Expr a -> [Builder]
referencedFrameContext :: forall (a :: EType). Expr a -> [Builder]
referencedFrameContext Expr a
expr = forall a. Ord a => [a] -> [a]
nubOrd (forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> [Builder]
go [] Expr a
expr)
where
go :: Expr a -> [Builder]
go :: forall (a :: EType). Expr a -> [Builder]
go = \case
CallValue Int
a -> [Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"callvalue_" (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Int
a)]
Caller Int
a -> [Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"caller_" (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Int
a)]
Address Int
a -> [Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"address_" (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Int
a)]
Balance {} -> forall a. HasCallStack => String -> a
error String
"TODO: BALANCE"
SelfBalance {} -> forall a. HasCallStack => String -> a
error String
"TODO: SELFBALANCE"
Gas {} -> forall a. HasCallStack => String -> a
error String
"TODO: GAS"
Expr a
_ -> []
declareBlockContext :: [Builder] -> SMT2
declareBlockContext :: [Builder] -> SMT2
declareBlockContext [Builder]
names = [Builder] -> CexVars -> SMT2
SMT2 ([Builder
"; block context"] forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a}. (Semigroup a, IsString a) => a -> a
declare [Builder]
names) CexVars
cexvars
where
declare :: a -> a
declare a
n = a
"(declare-const " forall a. Semigroup a => a -> a -> a
<> a
n forall a. Semigroup a => a -> a -> a
<> a
" (_ BitVec 256))"
cexvars :: CexVars
cexvars = CexVars
{ calldataV :: [Text]
calldataV = forall a. Monoid a => a
mempty
, buffersV :: [Text]
buffersV = forall a. Monoid a => a
mempty
, blockContextV :: [Text]
blockContextV = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
names
, txContextV :: [Text]
txContextV = forall a. Monoid a => a
mempty
}
referencedBlockContext :: Expr a -> [Builder]
referencedBlockContext :: forall (a :: EType). Expr a -> [Builder]
referencedBlockContext Expr a
expr = forall a. Ord a => [a] -> [a]
nubOrd (forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> [Builder]
go [] Expr a
expr)
where
go :: Expr a -> [Builder]
go :: forall (a :: EType). Expr a -> [Builder]
go = \case
Expr a
Origin -> [Builder
"origin"]
Expr a
Coinbase -> [Builder
"coinbase"]
Expr a
Timestamp -> [Builder
"timestamp"]
Expr a
BlockNumber -> [Builder
"blocknumber"]
Expr a
PrevRandao -> [Builder
"prevrandao"]
Expr a
GasLimit -> [Builder
"gaslimit"]
Expr a
ChainId -> [Builder
"chainid"]
Expr a
BaseFee -> [Builder
"basefee"]
Expr a
_ -> []
exprToSMT :: Expr a -> Builder
exprToSMT :: forall (a :: EType). Expr a -> Builder
exprToSMT = \case
Lit W256
w -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"(_ bv" forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show (forall a b. (Integral a, Num b) => a -> b
num W256
w :: Integer)) forall a. Semigroup a => a -> a -> a
<> Text
" 256)"
Var Text
s -> Text -> Builder
fromText Text
s
GVar (BufVar Int
n) -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"buf" forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Int
n)
GVar (StoreVar Int
n) -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"store" forall a. Semigroup a => a -> a -> a
<> (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Int
n)
JoinBytes
Expr 'Byte
z Expr 'Byte
o Expr 'Byte
two Expr 'Byte
three Expr 'Byte
four Expr 'Byte
five Expr 'Byte
six Expr 'Byte
seven
Expr 'Byte
eight Expr 'Byte
nine Expr 'Byte
ten Expr 'Byte
eleven Expr 'Byte
twelve Expr 'Byte
thirteen Expr 'Byte
fourteen Expr 'Byte
fifteen
Expr 'Byte
sixteen Expr 'Byte
seventeen Expr 'Byte
eighteen Expr 'Byte
nineteen Expr 'Byte
twenty Expr 'Byte
twentyone Expr 'Byte
twentytwo Expr 'Byte
twentythree
Expr 'Byte
twentyfour Expr 'Byte
twentyfive Expr 'Byte
twentysix Expr 'Byte
twentyseven Expr 'Byte
twentyeight Expr 'Byte
twentynine Expr 'Byte
thirty Expr 'Byte
thirtyone
-> [Expr 'Byte] -> Builder
concatBytes [
Expr 'Byte
z, Expr 'Byte
o, Expr 'Byte
two, Expr 'Byte
three, Expr 'Byte
four, Expr 'Byte
five, Expr 'Byte
six, Expr 'Byte
seven
, Expr 'Byte
eight, Expr 'Byte
nine, Expr 'Byte
ten, Expr 'Byte
eleven, Expr 'Byte
twelve, Expr 'Byte
thirteen, Expr 'Byte
fourteen, Expr 'Byte
fifteen
, Expr 'Byte
sixteen, Expr 'Byte
seventeen, Expr 'Byte
eighteen, Expr 'Byte
nineteen, Expr 'Byte
twenty, Expr 'Byte
twentyone, Expr 'Byte
twentytwo, Expr 'Byte
twentythree
, Expr 'Byte
twentyfour, Expr 'Byte
twentyfive, Expr 'Byte
twentysix, Expr 'Byte
twentyseven, Expr 'Byte
twentyeight, Expr 'Byte
twentynine, Expr 'Byte
thirty, Expr 'Byte
thirtyone]
Add Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvadd" Expr 'EWord
a Expr 'EWord
b
Sub Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvsub" Expr 'EWord
a Expr 'EWord
b
Mul Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvmul" Expr 'EWord
a Expr 'EWord
b
Exp Expr 'EWord
a Expr 'EWord
b -> case Expr 'EWord
b of
Lit W256
b' -> Expr 'EWord -> W256 -> Builder
expandExp Expr 'EWord
a W256
b'
Expr 'EWord
_ -> forall a. HasCallStack => String -> a
error String
"cannot encode symbolic exponentation into SMT"
Min Expr 'EWord
a Expr 'EWord
b ->
let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
a
benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
b in
Builder
"(ite (bvule " forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
") " forall a. Semigroup a => a -> a -> a
<> Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
LT Expr 'EWord
a Expr 'EWord
b ->
let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvult" Expr 'EWord
a Expr 'EWord
b in
Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
SLT Expr 'EWord
a Expr 'EWord
b ->
let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvslt" Expr 'EWord
a Expr 'EWord
b in
Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
GT Expr 'EWord
a Expr 'EWord
b ->
let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvugt" Expr 'EWord
a Expr 'EWord
b in
Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
LEq Expr 'EWord
a Expr 'EWord
b ->
let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvule" Expr 'EWord
a Expr 'EWord
b in
Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
GEq Expr 'EWord
a Expr 'EWord
b ->
let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvuge" Expr 'EWord
a Expr 'EWord
b in
Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
Eq Expr 'EWord
a Expr 'EWord
b ->
let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"=" Expr 'EWord
a Expr 'EWord
b in
Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
IsZero Expr 'EWord
a ->
let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"=" Expr 'EWord
a (W256 -> Expr 'EWord
Lit W256
0) in
Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
And Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvand" Expr 'EWord
a Expr 'EWord
b
Or Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvor" Expr 'EWord
a Expr 'EWord
b
Xor Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvxor" Expr 'EWord
a Expr 'EWord
b
Not Expr 'EWord
a -> forall {a :: EType}. Builder -> Expr a -> Builder
op1 Builder
"bvnot" Expr 'EWord
a
SHL Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvshl" Expr 'EWord
b Expr 'EWord
a
SHR Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvlshr" Expr 'EWord
b Expr 'EWord
a
SAR Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvashr" Expr 'EWord
b Expr 'EWord
a
SEx Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"signext" Expr 'EWord
a Expr 'EWord
b
Div Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
"bvudiv" Expr 'EWord
a Expr 'EWord
b
SDiv Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
"bvsdiv" Expr 'EWord
a Expr 'EWord
b
Mod Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
"bvurem" Expr 'EWord
a Expr 'EWord
b
SMod Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
"bvsrem" Expr 'EWord
a Expr 'EWord
b
MulMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c ->
let aExp :: Builder
aExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
a
bExp :: Builder
bExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
b
cExp :: Builder
cExp = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
c
aLift :: Builder
aLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
aExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
bLift :: Builder
bLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
bExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
cLift :: Builder
cLift = Builder
"(concat (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
cExp forall a. Semigroup a => a -> a -> a
<> Builder
")"
in Builder
"((_ extract 255 0) (ite (= " forall a. Semigroup a => a -> a -> a
<> Builder
cExp forall a. Semigroup a => a -> a -> a
<> Builder
" (_ bv0 256)) (_ bv0 512) (bvurem (bvmul " forall a. Semigroup a => a -> a -> a
<> Builder
aLift Builder -> Builder -> Builder
`sp` Builder
bLift forall a. Semigroup a => a -> a -> a
<> Builder
")" forall a. Semigroup a => a -> a -> a
<> Builder
cLift forall a. Semigroup a => a -> a -> a
<> Builder
")))"
EqByte Expr 'Byte
a Expr 'Byte
b ->
let cond :: Builder
cond = forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"=" Expr 'Byte
a Expr 'Byte
b in
Builder
"(ite " forall a. Semigroup a => a -> a -> a
<> Builder
cond Builder -> Builder -> Builder
`sp` Builder
one Builder -> Builder -> Builder
`sp` Builder
zero forall a. Semigroup a => a -> a -> a
<> Builder
")"
Keccak Expr 'Buf
a ->
let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
a in
Builder
"(keccak " forall a. Semigroup a => a -> a -> a
<> Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
SHA256 Expr 'Buf
a ->
let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
a in
Builder
"(sha256 " forall a. Semigroup a => a -> a -> a
<> Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
CallValue Int
a -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"callvalue_" (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Int
a)
Caller Int
a -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"caller_" (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Int
a)
Address Int
a -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"address_" (String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Int
a)
Expr a
Origin -> Builder
"origin"
BlockHash Expr 'EWord
a ->
let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
a in
Builder
"(blockhash " forall a. Semigroup a => a -> a -> a
<> Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
Expr a
Coinbase -> Builder
"coinbase"
Expr a
Timestamp -> Builder
"timestamp"
Expr a
BlockNumber -> Builder
"blocknumber"
Expr a
PrevRandao -> Builder
"prevrandao"
Expr a
GasLimit -> Builder
"gaslimit"
Expr a
ChainId -> Builder
"chainid"
Expr a
BaseFee -> Builder
"basefee"
LitByte Word8
b -> Text -> Builder
fromLazyText forall a b. (a -> b) -> a -> b
$ Text
"(_ bv" forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show (forall a b. (Integral a, Num b) => a -> b
num Word8
b :: Integer)) forall a. Semigroup a => a -> a -> a
<> Text
" 8)"
IndexWord Expr 'EWord
idx Expr 'EWord
w -> case Expr 'EWord
idx of
Lit W256
n -> if W256
n forall a. Ord a => a -> a -> Bool
>= W256
0 Bool -> Bool -> Bool
&& W256
n forall a. Ord a => a -> a -> Bool
< W256
32
then
let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
w in
Text -> Builder
fromLazyText (Text
"(indexWord" forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show (forall a b. (Integral a, Num b) => a -> b
num W256
n :: Integer))) Builder -> Builder -> Builder
`sp` Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
else forall (a :: EType). Expr a -> Builder
exprToSMT (Word8 -> Expr 'Byte
LitByte Word8
0)
Expr 'EWord
_ -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"indexWord" Expr 'EWord
idx Expr 'EWord
w
ReadByte Expr 'EWord
idx Expr 'Buf
src -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"select" Expr 'Buf
src Expr 'EWord
idx
ConcreteBuf ByteString
"" -> Builder
"emptyBuf"
ConcreteBuf ByteString
bs -> ByteString -> Expr 'Buf -> Builder
writeBytes ByteString
bs forall a. Monoid a => a
mempty
AbstractBuf Text
s -> Text -> Builder
fromText Text
s
ReadWord Expr 'EWord
idx Expr 'Buf
prev -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"readWord" Expr 'EWord
idx Expr 'Buf
prev
BufLength Expr 'Buf
b -> forall {a :: EType}. Builder -> Expr a -> Builder
op1 Builder
"bufLength" Expr 'Buf
b
WriteByte Expr 'EWord
idx Expr 'Byte
val Expr 'Buf
prev ->
let encIdx :: Builder
encIdx = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
idx
encVal :: Builder
encVal = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Byte
val
encPrev :: Builder
encPrev = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
prev in
Builder
"(store " forall a. Semigroup a => a -> a -> a
<> Builder
encPrev Builder -> Builder -> Builder
`sp` Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal forall a. Semigroup a => a -> a -> a
<> Builder
")"
WriteWord Expr 'EWord
idx Expr 'EWord
val Expr 'Buf
prev ->
let encIdx :: Builder
encIdx = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
idx
encVal :: Builder
encVal = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
val
encPrev :: Builder
encPrev = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
prev in
Builder
"(writeWord " forall a. Semigroup a => a -> a -> a
<> Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
`sp` Builder
encPrev forall a. Semigroup a => a -> a -> a
<> Builder
")"
CopySlice Expr 'EWord
srcIdx Expr 'EWord
dstIdx Expr 'EWord
size Expr 'Buf
src Expr 'Buf
dst ->
Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Builder -> Builder -> Builder
copySlice Expr 'EWord
srcIdx Expr 'EWord
dstIdx Expr 'EWord
size (forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
src) (forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
dst)
Expr a
EmptyStore -> Builder
"emptyStore"
ConcreteStore Map W256 (Map W256 W256)
s -> Map W256 (Map W256 W256) -> Builder
encodeConcreteStore Map W256 (Map W256 W256)
s
Expr a
AbstractStore -> Builder
"abstractStore"
SStore Expr 'EWord
addr Expr 'EWord
idx Expr 'EWord
val Expr 'Storage
prev ->
let encAddr :: Builder
encAddr = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
addr
encIdx :: Builder
encIdx = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
idx
encVal :: Builder
encVal = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
val
encPrev :: Builder
encPrev = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Storage
prev in
Builder
"(sstore" Builder -> Builder -> Builder
`sp` Builder
encAddr Builder -> Builder -> Builder
`sp` Builder
encIdx Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
`sp` Builder
encPrev forall a. Semigroup a => a -> a -> a
<> Builder
")"
SLoad Expr 'EWord
addr Expr 'EWord
idx Expr 'Storage
store -> forall {a :: EType} {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Expr a -> Builder
op3 Builder
"sload" Expr 'EWord
addr Expr 'EWord
idx Expr 'Storage
store
Expr a
a -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"TODO: implement: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Expr a
a
where
op1 :: Builder -> Expr a -> Builder
op1 Builder
op Expr a
a =
let enc :: Builder
enc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a in
Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
op2 :: Builder -> Expr a -> Expr a -> Builder
op2 Builder
op Expr a
a Expr a
b =
let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a
benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
b in
Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
op3 :: Builder -> Expr a -> Expr a -> Expr a -> Builder
op3 Builder
op Expr a
a Expr a
b Expr a
c =
let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a
benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
b
cenc :: Builder
cenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
c in
Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc Builder -> Builder -> Builder
`sp` Builder
cenc forall a. Semigroup a => a -> a -> a
<> Builder
")"
op2CheckZero :: Builder -> Expr a -> Expr a -> Builder
op2CheckZero Builder
op Expr a
a Expr a
b =
let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a
benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
b in
Builder
"(ite (= " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
" (_ bv0 256)) (_ bv0 256) " forall a. Semigroup a => a -> a -> a
<> Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
`sp` Builder
aenc Builder -> Builder -> Builder
`sp` Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
"))"
sp :: Builder -> Builder -> Builder
Builder
a sp :: Builder -> Builder -> Builder
`sp` Builder
b = Builder
a forall a. Semigroup a => a -> a -> a
<> (Text -> Builder
fromText Text
" ") forall a. Semigroup a => a -> a -> a
<> Builder
b
zero :: Builder
zero :: Builder
zero = Builder
"(_ bv0 256)"
one :: Builder
one :: Builder
one = Builder
"(_ bv1 256)"
propToSMT :: Prop -> Builder
propToSMT :: Prop -> Builder
propToSMT = \case
PEq Expr a
a Expr a
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"=" Expr a
a Expr a
b
PLT Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvult" Expr 'EWord
a Expr 'EWord
b
PGT Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvugt" Expr 'EWord
a Expr 'EWord
b
PLEq Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvule" Expr 'EWord
a Expr 'EWord
b
PGEq Expr 'EWord
a Expr 'EWord
b -> forall {a :: EType} {a :: EType}.
Builder -> Expr a -> Expr a -> Builder
op2 Builder
"bvuge" Expr 'EWord
a Expr 'EWord
b
PNeg Prop
a ->
let enc :: Builder
enc = Prop -> Builder
propToSMT Prop
a in
Builder
"(not " forall a. Semigroup a => a -> a -> a
<> Builder
enc forall a. Semigroup a => a -> a -> a
<> Builder
")"
PAnd Prop
a Prop
b ->
let aenc :: Builder
aenc = Prop -> Builder
propToSMT Prop
a
benc :: Builder
benc = Prop -> Builder
propToSMT Prop
b in
Builder
"(and " forall a. Semigroup a => a -> a -> a
<> Builder
aenc forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
POr Prop
a Prop
b ->
let aenc :: Builder
aenc = Prop -> Builder
propToSMT Prop
a
benc :: Builder
benc = Prop -> Builder
propToSMT Prop
b in
Builder
"(or " forall a. Semigroup a => a -> a -> a
<> Builder
aenc forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
PBool Bool
b -> if Bool
b then Builder
"true" else Builder
"false"
where
op2 :: Builder -> Expr a -> Expr a -> Builder
op2 Builder
op Expr a
a Expr a
b =
let aenc :: Builder
aenc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
a
benc :: Builder
benc = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
b in
Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
op forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
aenc forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
benc forall a. Semigroup a => a -> a -> a
<> Builder
")"
data Solver
= Z3
| CVC5
| Bitwuzla
| Custom Text
instance Show Solver where
show :: Solver -> String
show Solver
Z3 = String
"z3"
show Solver
CVC5 = String
"cvc5"
show Solver
Bitwuzla = String
"bitwuzla"
show (Custom Text
s) = Text -> String
T.unpack Text
s
data SolverInstance = SolverInstance
{ SolverInstance -> Solver
_type :: Solver
, SolverInstance -> Handle
_stdin :: Handle
, SolverInstance -> Handle
_stdout :: Handle
, SolverInstance -> Handle
_stderr :: Handle
, SolverInstance -> ProcessHandle
_process :: ProcessHandle
}
newtype SolverGroup = SolverGroup (Chan Task)
data Task = Task
{ Task -> SMT2
script :: SMT2
, Task -> Chan CheckSatResult
resultChan :: Chan CheckSatResult
}
data CheckSatResult
= Sat SMTCex
| Unsat
| Unknown
| Error TS.Text
deriving (Int -> CheckSatResult -> ShowS
[CheckSatResult] -> ShowS
CheckSatResult -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CheckSatResult] -> ShowS
$cshowList :: [CheckSatResult] -> ShowS
show :: CheckSatResult -> String
$cshow :: CheckSatResult -> String
showsPrec :: Int -> CheckSatResult -> ShowS
$cshowsPrec :: Int -> CheckSatResult -> ShowS
Show, CheckSatResult -> CheckSatResult -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CheckSatResult -> CheckSatResult -> Bool
$c/= :: CheckSatResult -> CheckSatResult -> Bool
== :: CheckSatResult -> CheckSatResult -> Bool
$c== :: CheckSatResult -> CheckSatResult -> Bool
Eq)
isSat :: CheckSatResult -> Bool
isSat :: CheckSatResult -> Bool
isSat (Sat SMTCex
_) = Bool
True
isSat CheckSatResult
_ = Bool
False
isErr :: CheckSatResult -> Bool
isErr :: CheckSatResult -> Bool
isErr (Error Text
_) = Bool
True
isErr CheckSatResult
_ = Bool
False
isUnsat :: CheckSatResult -> Bool
isUnsat :: CheckSatResult -> Bool
isUnsat CheckSatResult
Unsat = Bool
True
isUnsat CheckSatResult
_ = Bool
False
checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
checkSat (SolverGroup Chan Task
taskQueue) SMT2
script = do
Chan CheckSatResult
resChan <- forall a. IO (Chan a)
newChan
forall a. Chan a -> a -> IO ()
writeChan Chan Task
taskQueue (SMT2 -> Chan CheckSatResult -> Task
Task SMT2
script Chan CheckSatResult
resChan)
forall a. Chan a -> IO a
readChan Chan CheckSatResult
resChan
parseW256 :: SpecConstant -> W256
parseW256 :: SpecConstant -> W256
parseW256 = forall a. (Num a, Eq a) => SpecConstant -> a
parseSC
parseInteger :: SpecConstant -> Integer
parseInteger :: SpecConstant -> Integer
parseInteger = forall a. (Num a, Eq a) => SpecConstant -> a
parseSC
parseW8 :: SpecConstant -> Word8
parseW8 :: SpecConstant -> Word8
parseW8 = forall a. (Num a, Eq a) => SpecConstant -> a
parseSC
parseErr :: (Show a) => a -> b
parseErr :: forall a b. Show a => a -> b
parseErr a
res = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: cannot parse solver response: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show a
res
parseVar :: TS.Text -> Expr EWord
parseVar :: Text -> Expr 'EWord
parseVar = Text -> Expr 'EWord
Var
parseBlockCtx :: TS.Text -> Expr EWord
parseBlockCtx :: Text -> Expr 'EWord
parseBlockCtx Text
"origin" = Expr 'EWord
Origin
parseBlockCtx Text
"coinbase" = Expr 'EWord
Coinbase
parseBlockCtx Text
"timestamp" = Expr 'EWord
Timestamp
parseBlockCtx Text
"blocknumber" = Expr 'EWord
BlockNumber
parseBlockCtx Text
"prevrandao" = Expr 'EWord
PrevRandao
parseBlockCtx Text
"gaslimit" = Expr 'EWord
GasLimit
parseBlockCtx Text
"chainid" = Expr 'EWord
ChainId
parseBlockCtx Text
"basefee" = Expr 'EWord
BaseFee
parseBlockCtx Text
t = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: cannot parse " forall a. Semigroup a => a -> a -> a
<> (Text -> String
TS.unpack Text
t) forall a. Semigroup a => a -> a -> a
<> String
" into an Expr"
parseFrameCtx :: TS.Text -> Expr EWord
parseFrameCtx :: Text -> Expr 'EWord
parseFrameCtx Text
name = case Text -> String
TS.unpack Text
name of
(Char
'c':Char
'a':Char
'l':Char
'l':Char
'v':Char
'a':Char
'l':Char
'u':Char
'e':Char
'_':String
frame) -> Int -> Expr 'EWord
CallValue (forall a. Read a => String -> a
read String
frame)
(Char
'c':Char
'a':Char
'l':Char
'l':Char
'e':Char
'r':Char
'_':String
frame) -> Int -> Expr 'EWord
Caller (forall a. Read a => String -> a
read String
frame)
(Char
'a':Char
'd':Char
'd':Char
'r':Char
'e':Char
's':Char
's':Char
'_':String
frame) -> Int -> Expr 'EWord
Address (forall a. Read a => String -> a
read String
frame)
String
t -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: cannot parse " forall a. Semigroup a => a -> a -> a
<> String
t forall a. Semigroup a => a -> a -> a
<> String
" into an Expr"
getVars :: (TS.Text -> Expr EWord) -> SolverInstance -> [TS.Text] -> IO (Map (Expr EWord) W256)
getVars :: (Text -> Expr 'EWord)
-> SolverInstance -> [Text] -> IO (Map (Expr 'EWord) W256)
getVars Text -> Expr 'EWord
parseFn SolverInstance
inst [Text]
names = forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Text -> Expr 'EWord
parseFn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Text W256 -> Text -> IO (Map Text W256)
getOne forall a. Monoid a => a
mempty [Text]
names
where
getOne :: Map TS.Text W256 -> TS.Text -> IO (Map TS.Text W256)
getOne :: Map Text W256 -> Text -> IO (Map Text W256)
getOne Map Text W256
acc Text
name = do
Text
raw <- SolverInstance -> Text -> IO Text
getValue SolverInstance
inst (Text -> Text
T.fromStrict Text
name)
let
parsed :: ValuationPair
parsed = case forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
raw) of
Right (ResSpecific (ValuationPair
valParsed :| [])) -> ValuationPair
valParsed
Either Text GetValueRes
r -> forall a b. Show a => a -> b
parseErr Either Text GetValueRes
r
val :: W256
val = case ValuationPair
parsed of
(TermQualIdentifier (
Unqualified (IdSymbol Text
symbol)),
TermSpecConstant SpecConstant
sc)
-> if Text
symbol forall a. Eq a => a -> a -> Bool
== Text
name
then SpecConstant -> W256
parseW256 SpecConstant
sc
else forall a. HasCallStack => String -> a
error String
"Internal Error: solver did not return model for requested value"
ValuationPair
r -> forall a b. Show a => a -> b
parseErr ValuationPair
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name W256
val Map Text W256
acc
getBufs :: SolverInstance -> [TS.Text] -> IO (Map (Expr Buf) ByteString)
getBufs :: SolverInstance -> [Text] -> IO (Map (Expr 'Buf) ByteString)
getBufs SolverInstance
inst [Text]
names = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map (Expr 'Buf) ByteString
-> Text -> IO (Map (Expr 'Buf) ByteString)
getBuf forall a. Monoid a => a
mempty [Text]
names
where
getLength :: TS.Text -> IO Int
getLength :: Text -> IO Int
getLength Text
name = do
Text
val <- SolverInstance -> Text -> IO Text
getValue SolverInstance
inst (Text -> Text
T.fromStrict Text
name forall a. Semigroup a => a -> a -> a
<> Text
"_length")
W256
len <- case forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
val) of
Right (ResSpecific (ValuationPair
parsed :| [])) -> case ValuationPair
parsed of
(TermQualIdentifier (Unqualified (IdSymbol Text
symbol)), (TermSpecConstant SpecConstant
sc))
-> if Text
symbol forall a. Eq a => a -> a -> Bool
== (Text
name forall a. Semigroup a => a -> a -> a
<> Text
"_length")
then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SpecConstant -> W256
parseW256 SpecConstant
sc
else forall a. HasCallStack => String -> a
error String
"Internal Error: solver did not return model for requested value"
ValuationPair
res -> forall a b. Show a => a -> b
parseErr ValuationPair
res
Either Text GetValueRes
res -> forall a b. Show a => a -> b
parseErr Either Text GetValueRes
res
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ if W256
len forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
num (forall a. Bounded a => a
maxBound :: Int)
then forall a b. (Integral a, Num b) => a -> b
fromIntegral W256
len
else forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: buffer: "
forall a. Semigroup a => a -> a -> a
<> (Text -> String
TS.unpack Text
name)
forall a. Semigroup a => a -> a -> a
<> String
" is too large to be represented in a ByteString. Length: "
forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show W256
len
getBuf :: Map (Expr Buf) ByteString -> TS.Text -> IO (Map (Expr Buf) ByteString)
getBuf :: Map (Expr 'Buf) ByteString
-> Text -> IO (Map (Expr 'Buf) ByteString)
getBuf Map (Expr 'Buf) ByteString
acc Text
name = do
Int
len <- Text -> IO Int
getLength Text
name
Text
val <- SolverInstance -> Text -> IO Text
getValue SolverInstance
inst (Text -> Text
T.fromStrict Text
name)
Expr 'Buf
buf <- case forall a. Parser a -> Text -> Either Text a
parseCommentFreeFileMsg forall st. GenParser st GetValueRes
getValueRes (Text -> Text
T.toStrict Text
val) of
Right (ResSpecific (ValuationPair
valParsed :| [])) -> case ValuationPair
valParsed of
(TermQualIdentifier (Unqualified (IdSymbol Text
symbol)), Term
term)
-> if Text
symbol forall a. Eq a => a -> a -> Bool
== Text
name
then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> Term -> Expr 'Buf
parseBuf Int
len Term
term
else forall a. HasCallStack => String -> a
error String
"Internal Error: solver did not return model for requested value"
ValuationPair
res -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: cannot parse solver response: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show ValuationPair
res
Either Text GetValueRes
res -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: cannot parse solver response: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Either Text GetValueRes
res
let bs :: ByteString
bs = case forall (a :: EType). Expr a -> Expr a
simplify Expr 'Buf
buf of
ConcreteBuf ByteString
b -> ByteString
b
Expr 'Buf
_ -> forall a. HasCallStack => String -> a
error String
"Internal Error: unable to parse solver response into a concrete buffer"
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Text -> Expr 'Buf
AbstractBuf Text
name) ByteString
bs Map (Expr 'Buf) ByteString
acc
parseBuf :: Int -> Term -> Expr Buf
parseBuf :: Int -> Term -> Expr 'Buf
parseBuf Int
len = Map Text (Expr 'Buf) -> Term -> Expr 'Buf
go forall a. Monoid a => a
mempty
where
go :: Map Text (Expr 'Buf) -> Term -> Expr 'Buf
go Map Text (Expr 'Buf)
env = \case
(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" -> forall a. Monoid a => a
mempty
SpecConstant
v -> ByteString -> Expr 'Buf
ConcreteBuf forall a b. (a -> b) -> a -> b
$ Int -> Word8 -> ByteString
BS.replicate Int
len (SpecConstant -> Word8
parseW8 SpecConstant
v)
(TermApplication
(Unqualified (IdSymbol Text
"store"))
(Term
base :| [TermSpecConstant SpecConstant
idx, TermSpecConstant SpecConstant
val])
) -> let
pbase :: Expr 'Buf
pbase = Map Text (Expr 'Buf) -> Term -> Expr 'Buf
go Map Text (Expr 'Buf)
env Term
base
pidx :: W256
pidx = SpecConstant -> W256
parseW256 SpecConstant
idx
pval :: Word8
pval = SpecConstant -> Word8
parseW8 SpecConstant
val
in Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
writeByte (W256 -> Expr 'EWord
Lit W256
pidx) (Word8 -> Expr 'Byte
LitByte Word8
pval) Expr 'Buf
pbase
(TermLet ((VarBinding Text
name Term
bound) :| []) Term
term) -> let
pbound :: Expr 'Buf
pbound = Map Text (Expr 'Buf) -> Term -> Expr 'Buf
go Map Text (Expr 'Buf)
env Term
bound
in Map Text (Expr 'Buf) -> Term -> Expr 'Buf
go (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name Expr 'Buf
pbound Map Text (Expr 'Buf)
env) Term
term
(TermQualIdentifier (Unqualified (IdSymbol Text
name))) -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
name Map Text (Expr 'Buf)
env of
Just Expr 'Buf
t -> Expr 'Buf
t
Maybe (Expr 'Buf)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal error: could not find "
forall a. Semigroup a => a -> a -> a
<> (Text -> String
TS.unpack Text
name)
forall a. Semigroup a => a -> a -> a
<> String
" in environment mapping"
Term
p -> forall a b. Show a => a -> b
parseErr Term
p
parseSC :: (Num a, Eq a) => SpecConstant -> a
parseSC :: forall a. (Num a, Eq a) => SpecConstant -> a
parseSC (SCHexadecimal Text
a) = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Num a) => ReadS a
Numeric.readHex forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
T.fromStrict forall a b. (a -> b) -> a -> b
$ Text
a
parseSC SpecConstant
sc = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Internal Error: cannot parse: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show SpecConstant
sc
withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers :: forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
solver Natural
count Maybe Natural
timeout SolverGroup -> IO a
cont = do
[SolverInstance]
instances <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Solver -> Maybe Natural -> IO SolverInstance
spawnSolver Solver
solver Maybe Natural
timeout) [Natural
1..Natural
count]
Chan Task
taskQueue <- forall a. IO (Chan a)
newChan
Chan SolverInstance
availableInstances <- forall a. IO (Chan a)
newChan
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SolverInstance]
instances (forall a. Chan a -> a -> IO ()
writeChan Chan SolverInstance
availableInstances)
ThreadId
orchestrateId <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ forall {b}. Chan Task -> Chan SolverInstance -> IO b
orchestrate Chan Task
taskQueue Chan SolverInstance
availableInstances
a
res <- SolverGroup -> IO a
cont (Chan Task -> SolverGroup
SolverGroup Chan Task
taskQueue)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SolverInstance -> IO ()
stopSolver [SolverInstance]
instances
ThreadId -> IO ()
killThread ThreadId
orchestrateId
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
res
where
orchestrate :: Chan Task -> Chan SolverInstance -> IO b
orchestrate Chan Task
queue Chan SolverInstance
avail = do
Task
task <- forall a. Chan a -> IO a
readChan Chan Task
queue
SolverInstance
inst <- forall a. Chan a -> IO a
readChan Chan SolverInstance
avail
ThreadId
_ <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ Task -> SolverInstance -> Chan SolverInstance -> IO ()
runTask Task
task SolverInstance
inst Chan SolverInstance
avail
Chan Task -> Chan SolverInstance -> IO b
orchestrate Chan Task
queue Chan SolverInstance
avail
runTask :: Task -> SolverInstance -> Chan SolverInstance -> IO ()
runTask (Task (SMT2 [Builder]
cmds CexVars
cexvars) Chan CheckSatResult
r) SolverInstance
inst Chan SolverInstance
availableInstances = do
Either Text ()
out <- SolverInstance -> SMT2 -> IO (Either Text ())
sendScript SolverInstance
inst ([Builder] -> CexVars -> SMT2
SMT2 (Builder
"(reset)" forall a. a -> [a] -> [a]
: [Builder]
cmds) CexVars
cexvars)
case Either Text ()
out of
Left Text
e -> forall a. Chan a -> a -> IO ()
writeChan Chan CheckSatResult
r (Text -> CheckSatResult
Error (Text
"error while writing SMT to solver: " forall a. Semigroup a => a -> a -> a
<> Text -> Text
T.toStrict Text
e))
Right () -> do
Text
sat <- SolverInstance -> Text -> IO Text
sendLine SolverInstance
inst Text
"(check-sat)"
CheckSatResult
res <- case Text
sat of
Text
"sat" -> do
Map (Expr 'EWord) W256
calldatamodels <- (Text -> Expr 'EWord)
-> SolverInstance -> [Text] -> IO (Map (Expr 'EWord) W256)
getVars Text -> Expr 'EWord
parseVar SolverInstance
inst (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict forall a b. (a -> b) -> a -> b
$ CexVars -> [Text]
calldataV CexVars
cexvars)
Map (Expr 'Buf) ByteString
buffermodels <- SolverInstance -> [Text] -> IO (Map (Expr 'Buf) ByteString)
getBufs SolverInstance
inst (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict forall a b. (a -> b) -> a -> b
$ CexVars -> [Text]
buffersV CexVars
cexvars)
Map (Expr 'EWord) W256
blockctxmodels <- (Text -> Expr 'EWord)
-> SolverInstance -> [Text] -> IO (Map (Expr 'EWord) W256)
getVars Text -> Expr 'EWord
parseBlockCtx SolverInstance
inst (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict forall a b. (a -> b) -> a -> b
$ CexVars -> [Text]
blockContextV CexVars
cexvars)
Map (Expr 'EWord) W256
txctxmodels <- (Text -> Expr 'EWord)
-> SolverInstance -> [Text] -> IO (Map (Expr 'EWord) W256)
getVars Text -> Expr 'EWord
parseFrameCtx SolverInstance
inst (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Text
T.toStrict forall a b. (a -> b) -> a -> b
$ CexVars -> [Text]
txContextV CexVars
cexvars)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ SMTCex -> CheckSatResult
Sat forall a b. (a -> b) -> a -> b
$ SMTCex
{ vars :: Map (Expr 'EWord) W256
vars = Map (Expr 'EWord) W256
calldatamodels
, buffers :: Map (Expr 'Buf) ByteString
buffers = Map (Expr 'Buf) ByteString
buffermodels
, blockContext :: Map (Expr 'EWord) W256
blockContext = Map (Expr 'EWord) W256
blockctxmodels
, txContext :: Map (Expr 'EWord) W256
txContext = Map (Expr 'EWord) W256
txctxmodels
}
Text
"unsat" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unsat
Text
"timeout" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unknown
Text
"unknown" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckSatResult
Unknown
Text
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> CheckSatResult
Error forall a b. (a -> b) -> a -> b
$ Text -> Text
T.toStrict forall a b. (a -> b) -> a -> b
$ Text
"Unable to parse solver output: " forall a. Semigroup a => a -> a -> a
<> Text
sat
forall a. Chan a -> a -> IO ()
writeChan Chan CheckSatResult
r CheckSatResult
res
forall a. Chan a -> a -> IO ()
writeChan Chan SolverInstance
availableInstances SolverInstance
inst
solverArgs :: Solver -> Maybe (Natural) -> [Text]
solverArgs :: Solver -> Maybe Natural -> [Text]
solverArgs Solver
solver Maybe Natural
timeout = case Solver
solver of
Solver
Bitwuzla -> forall a. HasCallStack => String -> a
error String
"TODO: Bitwuzla args"
Solver
Z3 ->
[ Text
"-in" ]
Solver
CVC5 ->
[ Text
"--lang=smt"
, Text
"--no-interactive"
, Text
"--produce-models"
, Text
"--tlimit-per=" forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show (Natural
1000 forall a. Num a => a -> a -> a
* forall a. a -> Maybe a -> a
fromMaybe Natural
10 Maybe Natural
timeout))
]
Custom Text
_ -> []
spawnSolver :: Solver -> Maybe (Natural) -> IO SolverInstance
spawnSolver :: Solver -> Maybe Natural -> IO SolverInstance
spawnSolver Solver
solver Maybe Natural
timeout = do
let cmd :: CreateProcess
cmd = (String -> [String] -> CreateProcess
proc (forall a. Show a => a -> String
show Solver
solver) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Solver -> Maybe Natural -> [Text]
solverArgs Solver
solver Maybe Natural
timeout)) { std_in :: StdStream
std_in = StdStream
CreatePipe, std_out :: StdStream
std_out = StdStream
CreatePipe, std_err :: StdStream
std_err = StdStream
CreatePipe }
(Just Handle
stdin, Just Handle
stdout, Just Handle
stderr, ProcessHandle
process) <- CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess CreateProcess
cmd
Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdin (Maybe Int -> BufferMode
BlockBuffering (forall a. a -> Maybe a
Just Int
1000000))
let solverInstance :: SolverInstance
solverInstance = Solver
-> Handle -> Handle -> Handle -> ProcessHandle -> SolverInstance
SolverInstance Solver
solver Handle
stdin Handle
stdout Handle
stderr ProcessHandle
process
case Maybe Natural
timeout of
Maybe Natural
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
Just Natural
t -> case Solver
solver of
Solver
CVC5 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
Solver
_ -> do
()
_ <- SolverInstance -> Text -> IO ()
sendLine' SolverInstance
solverInstance forall a b. (a -> b) -> a -> b
$ Text
"(set-option :timeout " forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show Natural
t) forall a. Semigroup a => a -> a -> a
<> Text
")"
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverInstance
solverInstance
stopSolver :: SolverInstance -> IO ()
stopSolver :: SolverInstance -> IO ()
stopSolver (SolverInstance Solver
_ Handle
stdin Handle
stdout Handle
stderr ProcessHandle
process) = (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle) -> IO ()
cleanupProcess (forall a. a -> Maybe a
Just Handle
stdin, forall a. a -> Maybe a
Just Handle
stdout, forall a. a -> Maybe a
Just Handle
stderr, ProcessHandle
process)
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
sendScript SolverInstance
solver (SMT2 [Builder]
cmds CexVars
_) = do
SolverInstance -> Text -> IO ()
sendLine' SolverInstance
solver ([Text] -> Text
T.unlines forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Builder -> Text
toLazyText [Builder]
cmds)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right()
sendCommand :: SolverInstance -> Text -> IO Text
sendCommand :: SolverInstance -> Text -> IO Text
sendCommand SolverInstance
inst Text
cmd = do
let cmd' :: Text
cmd' = (Char -> Bool) -> Text -> Text
T.dropWhile Char -> Bool
isSpace Text
cmd
case Text -> String
T.unpack Text
cmd' of
String
"" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"success"
Char
';' : String
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
"success"
String
_ -> SolverInstance -> Text -> IO Text
sendLine SolverInstance
inst Text
cmd'
sendLine :: SolverInstance -> Text -> IO Text
sendLine :: SolverInstance -> Text -> IO Text
sendLine (SolverInstance Solver
_ Handle
stdin Handle
stdout Handle
_ ProcessHandle
_) Text
cmd = do
Handle -> Text -> IO ()
T.hPutStr Handle
stdin (Text -> Text -> Text
T.append Text
cmd Text
"\n")
Handle -> IO ()
hFlush Handle
stdin
Handle -> IO Text
T.hGetLine Handle
stdout
sendLine' :: SolverInstance -> Text -> IO ()
sendLine' :: SolverInstance -> Text -> IO ()
sendLine' (SolverInstance Solver
_ Handle
stdin Handle
_ Handle
_ ProcessHandle
_) Text
cmd = do
Handle -> Text -> IO ()
T.hPutStr Handle
stdin (Text -> Text -> Text
T.append Text
cmd Text
"\n")
Handle -> IO ()
hFlush Handle
stdin
getValue :: SolverInstance -> Text -> IO Text
getValue :: SolverInstance -> Text -> IO Text
getValue (SolverInstance Solver
_ Handle
stdin Handle
stdout Handle
_ ProcessHandle
_) Text
var = do
Handle -> Text -> IO ()
T.hPutStr Handle
stdin (Text -> Text -> Text
T.append (Text -> Text -> Text
T.append Text
"(get-value (" Text
var) Text
"))\n")
Handle -> IO ()
hFlush Handle
stdin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Text] -> Text
T.unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse) (Handle -> IO [Text]
readSExpr Handle
stdout)
readSExpr :: Handle -> IO [Text]
readSExpr :: Handle -> IO [Text]
readSExpr Handle
h = Int64 -> Int64 -> [Text] -> IO [Text]
go Int64
0 Int64
0 []
where
go :: Int64 -> Int64 -> [Text] -> IO [Text]
go Int64
0 Int64
0 [Text]
_ = do
Text
line <- Handle -> IO Text
T.hGetLine Handle
h
let ls :: Int64
ls = Text -> Int64
T.length forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (forall a. Eq a => a -> a -> Bool
== Char
'(') Text
line
rs :: Int64
rs = Text -> Int64
T.length forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (forall a. Eq a => a -> a -> Bool
== Char
')') Text
line
if Int64
ls forall a. Eq a => a -> a -> Bool
== Int64
rs
then forall (f :: * -> *) a. Applicative f => a -> f a
pure [Text
line]
else Int64 -> Int64 -> [Text] -> IO [Text]
go Int64
ls Int64
rs [Text
line]
go Int64
ls Int64
rs [Text]
prev = do
Text
line <- Handle -> IO Text
T.hGetLine Handle
h
let ls' :: Int64
ls' = Text -> Int64
T.length forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (forall a. Eq a => a -> a -> Bool
== Char
'(') Text
line
rs' :: Int64
rs' = Text -> Int64
T.length forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.filter (forall a. Eq a => a -> a -> Bool
== Char
')') Text
line
if (Int64
ls forall a. Num a => a -> a -> a
+ Int64
ls') forall a. Eq a => a -> a -> Bool
== (Int64
rs forall a. Num a => a -> a -> a
+ Int64
rs')
then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Text
line forall a. a -> [a] -> [a]
: [Text]
prev
else Int64 -> Int64 -> [Text] -> IO [Text]
go (Int64
ls forall a. Num a => a -> a -> a
+ Int64
ls') (Int64
rs forall a. Num a => a -> a -> a
+ Int64
rs') (Text
line forall a. a -> [a] -> [a]
: [Text]
prev)
copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder
copySlice :: Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Builder -> Builder -> Builder
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset size :: Expr 'EWord
size@(Lit W256
_) Builder
src Builder
dst
| Expr 'EWord
size forall a. Eq a => a -> a -> Bool
== (W256 -> Expr 'EWord
Lit W256
0) = Builder
dst
| Bool
otherwise =
let size' :: Expr 'EWord
size' = (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
sub Expr 'EWord
size (W256 -> Expr 'EWord
Lit W256
1))
encDstOff :: Builder
encDstOff = forall (a :: EType). Expr a -> Builder
exprToSMT (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
dstOffset Expr 'EWord
size')
encSrcOff :: Builder
encSrcOff = forall (a :: EType). Expr a -> Builder
exprToSMT (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
add Expr 'EWord
srcOffset Expr 'EWord
size')
child :: Builder
child = Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Builder -> Builder -> Builder
copySlice Expr 'EWord
srcOffset Expr 'EWord
dstOffset Expr 'EWord
size' Builder
src Builder
dst in
Builder
"(store " forall a. Semigroup a => a -> a -> a
<> Builder
child Builder -> Builder -> Builder
`sp` Builder
encDstOff Builder -> Builder -> Builder
`sp` Builder
"(select " forall a. Semigroup a => a -> a -> a
<> Builder
src Builder -> Builder -> Builder
`sp` Builder
encSrcOff forall a. Semigroup a => a -> a -> a
<> Builder
"))"
copySlice Expr 'EWord
_ Expr 'EWord
_ Expr 'EWord
_ Builder
_ Builder
_ = forall a. HasCallStack => String -> a
error String
"TODO: implement copySlice with a symbolically sized region"
expandExp :: Expr EWord -> W256 -> Builder
expandExp :: Expr 'EWord -> W256 -> Builder
expandExp Expr 'EWord
base W256
expnt
| W256
expnt forall a. Eq a => a -> a -> Bool
== W256
1 = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
base
| Bool
otherwise =
let b :: Builder
b = forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'EWord
base
n :: Builder
n = Expr 'EWord -> W256 -> Builder
expandExp Expr 'EWord
base (W256
expnt forall a. Num a => a -> a -> a
- W256
1) in
Builder
"(bvmul " forall a. Semigroup a => a -> a -> a
<> Builder
b Builder -> Builder -> Builder
`sp` Builder
n forall a. Semigroup a => a -> a -> a
<> Builder
")"
concatBytes :: [Expr Byte] -> Builder
concatBytes :: [Expr 'Byte] -> Builder
concatBytes [Expr 'Byte]
bytes =
let bytesRev :: [Expr 'Byte]
bytesRev = forall a. [a] -> [a]
reverse [Expr 'Byte]
bytes
a2 :: Builder
a2 = forall (a :: EType). Expr a -> Builder
exprToSMT (forall a. [a] -> a
head [Expr 'Byte]
bytesRev) in
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall {a :: EType}. Builder -> Expr a -> Builder
wrap Builder
a2 forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
tail [Expr 'Byte]
bytesRev
where
wrap :: Builder -> Expr a -> Builder
wrap Builder
inner Expr a
byte =
let byteSMT :: Builder
byteSMT = forall (a :: EType). Expr a -> Builder
exprToSMT Expr a
byte in
Builder
"(concat " forall a. Semigroup a => a -> a -> a
<> Builder
byteSMT Builder -> Builder -> Builder
`sp` Builder
inner forall a. Semigroup a => a -> a -> a
<> Builder
")"
writeBytes :: ByteString -> Expr Buf -> Builder
writeBytes :: ByteString -> Expr 'Buf -> Builder
writeBytes ByteString
bytes Expr 'Buf
buf = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. (a -> Word8 -> a) -> a -> ByteString -> a
BS.foldl' (Int, Builder) -> Word8 -> (Int, Builder)
wrap (Int
0, forall (a :: EType). Expr a -> Builder
exprToSMT Expr 'Buf
buf) ByteString
bytes
where
skipZeros :: Bool
skipZeros = Expr 'Buf
buf forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty
wrap :: (Int, Builder) -> Word8 -> (Int, Builder)
wrap :: (Int, Builder) -> Word8 -> (Int, Builder)
wrap (Int
idx, Builder
inner) Word8
byte =
if Bool
skipZeros Bool -> Bool -> Bool
&& Word8
byte forall a. Eq a => a -> a -> Bool
== Word8
0
then (Int
idx forall a. Num a => a -> a -> a
+ Int
1, Builder
inner)
else let
byteSMT :: Builder
byteSMT = forall (a :: EType). Expr a -> Builder
exprToSMT (Word8 -> Expr 'Byte
LitByte Word8
byte)
idxSMT :: Builder
idxSMT = forall (a :: EType). Expr a -> Builder
exprToSMT forall b c a. (b -> c) -> (a -> b) -> a -> c
. W256 -> Expr 'EWord
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
num forall a b. (a -> b) -> a -> b
$ Int
idx
in (Int
idx forall a. Num a => a -> a -> a
+ Int
1, Builder
"(store " forall a. Semigroup a => a -> a -> a
<> Builder
inner Builder -> Builder -> Builder
`sp` Builder
idxSMT Builder -> Builder -> Builder
`sp` Builder
byteSMT forall a. Semigroup a => a -> a -> a
<> Builder
")")
encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder
encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder
encodeConcreteStore Map W256 (Map W256 W256)
s = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Builder -> (W256, W256, W256) -> Builder
encodeWrite Builder
"emptyStore" [(W256, W256, W256)]
writes
where
asList :: [(W256, [(W256, W256)])]
asList = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall k a. Map k a -> [(k, a)]
Map.toList) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map W256 (Map W256 W256)
s
writes :: [(W256, W256, W256)]
writes = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(W256
addr, [(W256, W256)]
ws) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(W256
k, W256
v) -> (W256
addr, W256
k, W256
v)) [(W256, W256)]
ws) [(W256, [(W256, W256)])]
asList
encodeWrite :: Builder -> (W256, W256, W256) -> Builder
encodeWrite Builder
prev (W256
addr, W256
key, W256
val) = let
encAddr :: Builder
encAddr = forall (a :: EType). Expr a -> Builder
exprToSMT (W256 -> Expr 'EWord
Lit W256
addr)
encKey :: Builder
encKey = forall (a :: EType). Expr a -> Builder
exprToSMT (W256 -> Expr 'EWord
Lit W256
key)
encVal :: Builder
encVal = forall (a :: EType). Expr a -> Builder
exprToSMT (W256 -> Expr 'EWord
Lit W256
val)
in Builder
"(sstore " forall a. Semigroup a => a -> a -> a
<> Builder
encAddr Builder -> Builder -> Builder
`sp` Builder
encKey Builder -> Builder -> Builder
`sp` Builder
encVal Builder -> Builder -> Builder
`sp` Builder
prev forall a. Semigroup a => a -> a -> a
<> Builder
")"