Skip to content

Commit

Permalink
fix rebase fuckups
Browse files Browse the repository at this point in the history
  • Loading branch information
MrChico committed Sep 14, 2020
1 parent a101fc8 commit cb523e4
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 28 deletions.
39 changes: 11 additions & 28 deletions src/hevm/src/EVM/Symbolic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -101,9 +101,9 @@ sgt (S _ x) (S _ y) =

shiftRight' :: SymWord -> SymWord -> SymWord
shiftRight' a@(S _ a') b@(S _ b') = case (num <$> unliteral a', b) of
(Just n, (S (FromBytes (SymbolicBuffer a)) i)) | n `mod` 8 == 0 && n <= 256 ->
(Just n, (S (FromBytes (StaticSymBuffer a)) i)) | n `mod` 8 == 0 && n <= 256 ->
let bs = replicate (n `div` 8) 0 <> (take ((256 - n) `div` 8) a)
in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)
in S (FromBytes (StaticSymBuffer bs)) (fromBytes bs)
_ -> sw256 $ sShiftRight b' a'

-- | Operations over static symbolic memory (list of symbolic bytes)
Expand Down Expand Up @@ -154,7 +154,8 @@ truncpad' n m = case m of
Nothing -> StaticSymBuffer $ takeStatic n (xs .++ literal (replicate n 0))

swordAt :: Int -> [SWord 8] -> SymWord
swordAt i bs = sw256 . fromBytes $ truncpad 32 $ drop i bs
swordAt i bs = let b = truncpad 32 $ drop i bs
in S (FromBytes (StaticSymBuffer b)) (fromBytes b)

swordAt' :: SymWord -> SList (WordN 8) -> SymWord
swordAt' i@(S _ i') bs =
Expand Down Expand Up @@ -213,29 +214,6 @@ readByteOrZero'' i bs =
(bs .!! (sFromIntegral i))
(literal 0)

-- Generates a ridiculously large set of constraints (roughly 25k) when
-- the index is symbolic, but it still seems (kind of) manageable
-- for the solvers.
readSWordWithBound :: SWord 32 -> Buffer -> SWord 32 -> SymWord
readSWordWithBound ind (SymbolicBuffer xs) bound = case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of
(Just i, Just b) ->
let bs = truncpad 32 $ drop i (take b xs)
in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)
_ ->
let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]

readSWordWithBound ind (ConcreteBuffer xs) bound =
case fromSized <$> unliteral ind of
Nothing -> readSWordWithBound ind (SymbolicBuffer (litBytes xs)) bound
Just x' ->
-- INVARIANT: bound should always be length xs for concrete bytes
-- so we should be able to safely ignore it here
litWord $ Concrete.readMemoryWord (num x') xs

readMemoryWord' :: Word -> [SWord 8] -> SymWord
readMemoryWord' (C _ i) m = sw256 $ fromBytes $ truncpad 32 (drop (num i) m)

-- pad up to 1000 bytes
sslice :: SymWord -> SymWord -> SList (WordN 8) -> SList (WordN 8)
sslice (S _ o) (S _ l) bs = case (unliteral $ SL.length bs, unliteral (o + l)) of
Expand Down Expand Up @@ -405,8 +383,13 @@ select' xs err ind = walk xs ind err
-- for the solvers.
readStaticWordWithBound :: SWord 32 -> ([SWord 8], SWord 32) -> SymWord
readStaticWordWithBound ind (xs, bound) =
let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]
case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of
(Just i, Just b) ->
let bs = truncpad 32 $ drop i (take b xs)
in S (FromBytes (StaticSymBuffer bs)) (fromBytes bs)
_ ->
let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
in sw256 $ fromBytes [select' boundedList 0 (ind + j) | j <- [0..31]]

-- | Custom instances for SymWord, many of which have direct
-- analogues for concrete words defined in Concrete.hs
Expand Down
2 changes: 2 additions & 0 deletions src/hevm/src/EVM/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ import Data.Aeson (FromJSONKey (..), FromJSONKeyFunction (..))
#endif

import Data.SBV
import Data.SBV.List ((.++))
import qualified Data.SBV.List as SL
import Data.Kind
import Data.Monoid ((<>))
import Data.Bifunctor (first)
Expand Down

0 comments on commit cb523e4

Please sign in to comment.