diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,22 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.51.3] - 2023-07-14 + +## Fixed + +- Path joining on Windows +- Fixed overflow issue in stripWrites +- Automatic tests are now more reproducible + +## Changed + +- Removed sha3Crack which has been deprecated for keccakEqs + +## Added + +- Added flag `-f debug` to add debug flags to cabal/GHC + ## [0.51.2] - 2023-07-11 ## Fixed diff --git a/hevm.cabal b/hevm.cabal --- a/hevm.cabal +++ b/hevm.cabal @@ -2,7 +2,7 @@ name: hevm version: - 0.51.2 + 0.51.3 synopsis: Ethereum virtual machine evaluator description: @@ -52,6 +52,11 @@ default: False manual: True +flag debug + description: Sets flags for compilation with extensive debug symbols and eventlog + default: False + manual: True + source-repository head type: git location: https://github.com/ethereum/hevm.git @@ -61,6 +66,13 @@ ghc-options: -Werror if flag(devel) ghc-options: -j + if flag(debug) + ghc-options: + -j + -g3 + -fdistinct-constructor-tables + -finfo-table-map + -eventlog ghc-options: -Wall -Wno-unticked-promoted-constructors @@ -138,17 +150,17 @@ Decimal >= 0.5.1 && < 0.6, containers >= 0.6.0 && < 0.7, deepseq >= 1.4.4 && < 1.5, - time >= 1.11.1.1 && < 1.12, + time >= 1.11 && < 1.14, transformers >= 0.5.6 && < 0.6, tree-view >= 0.5 && < 0.6, abstract-par >= 0.3.3 && < 0.4, - aeson >= 2.0.0 && < 2.1, + aeson >= 2.0.0 && < 2.2, bytestring >= 0.11.3.1 && < 0.12, scientific >= 0.3.6 && < 0.4, binary >= 0.8.6 && < 0.9, - text >= 1.2.3 && < 1.3, + text >= 1.2.3 && < 2.1, unordered-containers >= 0.2.10 && < 0.3, - vector >= 0.12.1 && < 0.13, + vector >= 0.12.1 && < 0.14, ansi-wl-pprint >= 0.6.9 && < 0.7, base16 >= 0.3.2.0 && < 0.3.3.0, megaparsec >= 9.0.0 && < 10.0, @@ -190,8 +202,8 @@ witch >= 1.1 && < 1.3 if !os(windows) build-depends: - brick >= 1.4 && < 1.5, - vty >= 5.37 && < 5.38 + brick >= 1.4 && < 2.0, + vty >= 5.37 && < 5.39 hs-source-dirs: src diff --git a/src/EVM.hs b/src/EVM.hs --- a/src/EVM.hs +++ b/src/EVM.hs @@ -141,8 +141,7 @@ , static = False } , env = Env - { sha3Crack = mempty - , chainId = o.chainId + { chainId = o.chainId , storage = o.initialStorage , origStorage = mempty , contracts = Map.fromList @@ -334,17 +333,16 @@ \xOffset -> forceConcrete xSize' "sha3 size must be concrete" $ \xSize -> burn (g_sha3 + g_sha3word * ceilDiv (unsafeInto xSize) 32) $ accessMemoryRange xOffset xSize $ do - (hash, invMap) <- case readMemory xOffset' xSize' vm of + hash <- case readMemory xOffset' xSize' vm of ConcreteBuf bs -> do let hash' = keccak' bs eqs <- use #keccakEqs assign #keccakEqs $ PEq (Lit hash') (Keccak (ConcreteBuf bs)):eqs - pure (Lit hash', Map.singleton hash' bs) - buf -> pure (Keccak buf, mempty) + pure $ Lit hash' + buf -> pure $ Keccak buf next assign (#state % #stack) (hash : xs) - modifying (#env % #sha3Crack) ((<>) invMap) _ -> underrun OpAddress -> diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -19,7 +19,7 @@ import Data.Vector.Storable qualified as VS import Data.Vector.Storable.ByteString import Data.Word (Word8, Word32) -import Witch (unsafeInto, into) +import Witch (unsafeInto, into, tryFrom) import Optics.Core @@ -532,9 +532,11 @@ stripWrites :: W256 -> W256 -> Expr Buf -> Expr Buf stripWrites off size = \case AbstractBuf s -> AbstractBuf s - ConcreteBuf b -> ConcreteBuf $ if off <= off + size - then BS.take (unsafeInto $ off+size) b - else b + ConcreteBuf b -> ConcreteBuf $ case off <= off + size of + True -> case tryFrom @W256 (off + size) of + Right n -> BS.take n b + Left _ -> b + False -> b WriteByte (Lit idx) v prev -> if idx - off >= size then stripWrites off size prev diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs --- a/src/EVM/Solidity.hs +++ b/src/EVM/Solidity.hs @@ -291,26 +291,26 @@ -- | Reads all solc ouput json files found under the provided filepath and returns them merged into a BuildOutput readBuildOutput :: FilePath -> ProjectType -> IO (Either String BuildOutput) readBuildOutput root DappTools = do - let outDir = root <> "/out/" + let outDir = root "out" jsons <- findJsonFiles outDir case jsons of - [x] -> readSolc DappTools root (outDir <> x) + [x] -> readSolc DappTools root (outDir x) [] -> pure . Left $ "no json files found in: " <> outDir _ -> pure . Left $ "multiple json files found in: " <> outDir readBuildOutput root CombinedJSON = do - let outDir = root <> "/out/" + let outDir = root "out" jsons <- findJsonFiles outDir case jsons of - [x] -> readSolc CombinedJSON root (outDir <> x) + [x] -> readSolc CombinedJSON root (outDir x) [] -> pure . Left $ "no json files found in: " <> outDir _ -> pure . Left $ "multiple json files found in: " <> outDir readBuildOutput root Foundry = do - let outDir = root <> "/out/" - jsons <- findJsonFiles (root <> "/out") + let outDir = root "out" + jsons <- findJsonFiles outDir case (filterMetadata jsons) of [] -> pure . Left $ "no json files found in: " <> outDir js -> do - outputs <- sequence <$> mapM (readSolc Foundry root) ((fmap ((<>) (outDir))) js) + outputs <- sequence <$> mapM (readSolc Foundry root) ((fmap (() (outDir))) js) pure . (fmap mconcat) $ outputs -- | Finds all json files under the provided filepath, searches recursively @@ -326,7 +326,7 @@ files <- Map.fromList <$> forM (Map.toList sources) (\x@(SrcFile id' fp, _) -> do contents <- case x of (_, Just content) -> pure content - (SrcFile _ _, Nothing) -> BS.readFile (root <> "/" <> fp) + (SrcFile _ _, Nothing) -> BS.readFile (root fp) pure (id', (fp, contents)) ) pure $! SourceCache diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -718,7 +718,6 @@ , chainId :: W256 , storage :: Expr Storage , origStorage :: Map W256 (Map W256 W256) - , sha3Crack :: Map W256 ByteString } deriving (Show, Generic) diff --git a/test/test.hs b/test/test.hs --- a/test/test.hs +++ b/test/test.hs @@ -5,6 +5,8 @@ import Prelude hiding (LT, GT) +import GHC.TypeLits +import Data.Proxy import Control.Monad.State.Strict import Data.Bits hiding (And, Xor) import Data.ByteString (ByteString) @@ -23,7 +25,6 @@ import Data.Typeable import Data.Vector qualified as Vector import GHC.Conc (getNumProcessors) -import Numeric.Natural (Natural) import System.Directory import System.Environment import Test.Tasty @@ -125,6 +126,15 @@ let e = ReadWord (Lit 0x0) (CopySlice (Lit 0x0) (Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc) (Lit 0x6) (ConcreteBuf "\255\255\255\255\255\255") (ConcreteBuf "")) b <- checkEquiv e (Expr.simplify e) assertBool "Simplifier failed" b + , testCase "stripWrites-overflow" $ do + -- below eventually boils down to + -- unsafeInto (0xf0000000000000000000000000000000000000000000000000000000000000+1) :: Int + -- which failed before + let + a = ReadByte (Lit 0xf0000000000000000000000000000000000000000000000000000000000000) (WriteByte (And (SHA256 (ConcreteBuf "")) (Lit 0x1)) (LitByte 0) (ConcreteBuf "")) + b = Expr.simplify a + ret <- checkEquiv a b + assertBool "must be equivalent" ret ] -- These tests fuzz the simplifier by generating a random expression, -- applying some simplification rules, and then using the smt encoding to @@ -140,35 +150,15 @@ , testProperty "byte-simplification" $ \(expr :: Expr Byte) -> ioProperty $ do let simplified = Expr.simplify expr checkEquiv expr simplified - , testProperty "word-simplification" $ \(_ :: Int) -> ioProperty $ do - expr <- generate . sized $ genWord 0 -- we want a lower frequency of lits for this test + -- https://github.com/ethereum/hevm/issues/311 + , ignoreTest $ testProperty "word-simplification" $ \(ZeroDepthWord expr) -> ioProperty $ do let simplified = Expr.simplify expr checkEquiv expr simplified , testProperty "readStorage-equivalance" $ \(store, addr, slot) -> ioProperty $ do let simplified = Expr.readStorage' addr slot store full = SLoad addr slot store checkEquiv simplified full - , testProperty "writeStorage-equivalance" $ \(addr, slot, val) -> ioProperty $ do - let mkStore = oneof - [ pure EmptyStore - , fmap ConcreteStore arbitrary - , do - -- generate some write chains where we know that at least one - -- write matches either the input addr, or both the input - -- addr and slot - let matchAddr = liftM2 (SStore addr) arbitrary arbitrary - matchBoth = fmap (SStore addr slot) arbitrary - addWrites :: Expr Storage -> Int -> Gen (Expr Storage) - addWrites b 0 = pure b - addWrites b n = liftM4 SStore arbitrary arbitrary arbitrary (addWrites b (n - 1)) - s <- arbitrary - addMatch <- oneof [ matchAddr, matchBoth ] - let withMatch = addMatch s - newWrites <- oneof [ pure 0, pure 1, fmap (`mod` 5) arbitrary ] - addWrites withMatch newWrites - , arbitrary - ] - store <- generate mkStore + , testProperty "writeStorage-equivalance" $ \(val, GenWriteStorageExpr (addr, slot, store)) -> ioProperty $ do let simplified = Expr.writeStorage addr slot val store full = SStore addr slot val store checkEquiv simplified full @@ -176,14 +166,7 @@ let simplified = Expr.readWord idx buf full = ReadWord idx buf checkEquiv simplified full - , testProperty "writeWord-equivalance" $ \(idx, val) -> ioProperty $ do - let mkBuf = oneof - [ pure $ ConcreteBuf "" -- empty - , fmap ConcreteBuf arbitrary -- concrete - , sized (genBuf 100) -- overlapping writes - , arbitrary -- sparse writes - ] - buf <- generate mkBuf + , testProperty "writeWord-equivalance" $ \(idx, val, WriteWordBuf buf) -> ioProperty $ do let simplified = Expr.writeWord idx val buf full = WriteWord idx val buf checkEquiv simplified full @@ -196,35 +179,21 @@ full = ReadByte idx buf checkEquiv simplified full -- we currently only simplify concrete writes over concrete buffers so that's what we test here - , testProperty "writeByte-equivalance" $ \(LitOnly val, LitOnly buf) -> ioProperty $ do - idx <- generate $ frequency - [ (10, genLit (fromIntegral (1_000_000 :: Int))) -- can never overflow an Int - , (1, fmap Lit arbitrary) -- can overflow an Int - ] + , testProperty "writeByte-equivalance" $ \(LitOnly val, LitOnly buf, GenWriteByteIdx idx) -> ioProperty $ do let simplified = Expr.writeByte idx val buf full = WriteByte idx val buf checkEquiv simplified full - , testProperty "copySlice-equivalance" $ \(srcOff) -> ioProperty $ do + , testProperty "copySlice-equivalance" $ \(srcOff, GenCopySliceBuf src, GenCopySliceBuf dst, LitWord @300 size) -> ioProperty $ do -- we bias buffers to be concrete more often than not - let mkBuf = oneof - [ pure $ ConcreteBuf "" - , fmap ConcreteBuf arbitrary - , arbitrary - ] - src <- generate mkBuf - dst <- generate mkBuf - size <- generate (genLit 300) dstOff <- generate (maybeBoundedLit 100_000) let simplified = Expr.copySlice srcOff dstOff size src dst full = CopySlice srcOff dstOff size src dst checkEquiv simplified full - , testProperty "indexWord-equivalence" $ \(src) -> ioProperty $ do - idx <- generate (genLit 50) + , testProperty "indexWord-equivalence" $ \(src, LitWord @50 idx) -> ioProperty $ do let simplified = Expr.indexWord idx src full = IndexWord idx src checkEquiv simplified full - , testProperty "indexWord-mask-equivalence" $ \(src :: Expr EWord) -> ioProperty $ do - idx <- generate (genLit 35) + , testProperty "indexWord-mask-equivalence" $ \(src :: Expr EWord, LitWord @35 idx) -> ioProperty $ do mask <- generate $ do pow <- arbitrary :: Gen Int frequency @@ -2437,9 +2406,18 @@ instance Arbitrary (Expr End) where arbitrary = sized genEnd +-- LitOnly newtype LitOnly a = LitOnly a deriving (Show, Eq) +newtype LitWord (sz :: Nat) = LitWord (Expr EWord) + deriving (Show) + +instance (KnownNat sz) => Arbitrary (LitWord sz) where + arbitrary = LitWord <$> genLit (fromInteger v) + where + v = natVal (Proxy @sz) + instance Arbitrary (LitOnly (Expr Byte)) where arbitrary = LitOnly . LitByte <$> arbitrary @@ -2448,6 +2426,82 @@ instance Arbitrary (LitOnly (Expr Buf)) where arbitrary = LitOnly . ConcreteBuf <$> arbitrary + +-- ZeroDepthWord +newtype ZeroDepthWord = ZeroDepthWord (Expr EWord) + deriving (Show, Eq) + +instance Arbitrary ZeroDepthWord where + arbitrary = do + fmap ZeroDepthWord . sized $ genWord 0 + +-- WriteWordBuf +newtype WriteWordBuf = WriteWordBuf (Expr Buf) + deriving (Show, Eq) + +instance Arbitrary WriteWordBuf where + arbitrary = do + let mkBuf = oneof + [ pure $ ConcreteBuf "" -- empty + , fmap ConcreteBuf arbitrary -- concrete + , sized (genBuf 100) -- overlapping writes + , arbitrary -- sparse writes + ] + fmap WriteWordBuf mkBuf + +-- GenCopySliceBuf +newtype GenCopySliceBuf = GenCopySliceBuf (Expr Buf) + deriving (Show, Eq) + +instance Arbitrary GenCopySliceBuf where + arbitrary = do + let mkBuf = oneof + [ pure $ ConcreteBuf "" + , fmap ConcreteBuf arbitrary + , arbitrary + ] + fmap GenCopySliceBuf mkBuf + +-- GenWriteStorageExpr +newtype GenWriteStorageExpr = GenWriteStorageExpr (Expr EWord, Expr EWord, Expr Storage) + deriving (Show, Eq) + +instance Arbitrary GenWriteStorageExpr where + arbitrary = do + addr <- arbitrary + slot <- arbitrary + let mkStore = oneof + [ pure EmptyStore + , fmap ConcreteStore arbitrary + , do + -- generate some write chains where we know that at least one + -- write matches either the input addr, or both the input + -- addr and slot + let matchAddr = liftM2 (SStore addr) arbitrary arbitrary + matchBoth = fmap (SStore addr slot) arbitrary + addWrites :: Expr Storage -> Int -> Gen (Expr Storage) + addWrites b 0 = pure b + addWrites b n = liftM4 SStore arbitrary arbitrary arbitrary (addWrites b (n - 1)) + s <- arbitrary + addMatch <- oneof [ matchAddr, matchBoth ] + let withMatch = addMatch s + newWrites <- oneof [ pure 0, pure 1, fmap (`mod` 5) arbitrary ] + addWrites withMatch newWrites + , arbitrary + ] + store <- mkStore + pure $ GenWriteStorageExpr (addr, slot, store) + +-- GenWriteByteIdx +newtype GenWriteByteIdx = GenWriteByteIdx (Expr EWord) + deriving (Show, Eq) + +instance Arbitrary GenWriteByteIdx where + arbitrary = do + -- 1st: can never overflow an Int + -- 2nd: can overflow an Int + let mkIdx = frequency [ (10, genLit (fromIntegral (1_000_000 :: Int))) , (1, fmap Lit arbitrary) ] + fmap GenWriteByteIdx mkIdx genByte :: Int -> Gen (Expr Byte) genByte 0 = fmap LitByte arbitrary