hevm 0.51.2 → 0.51.3

raw patch · 7 files changed

+157/−76 lines, 7 filesdep ~aesondep ~brickdep ~textPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: aeson, brick, text, time, vector, vty

API changes (from Hackage documentation)

Files

• CHANGELOG.md +16/−0
• hevm.cabal +19/−7
• src/EVM.hs +4/−6
• src/EVM/Expr.hs +6/−4
• src/EVM/Solidity.hs +8/−8
• src/EVM/Types.hs +0/−1
• test/test.hs +104/−50

@@ -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

@@ -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 

@@ -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 ->

@@ -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

@@ -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

@@ -718,7 +718,6 @@   , chainId      :: W256   , storage      :: Expr Storage   , origStorage  :: Map W256 (Map W256 W256)-  , sha3Crack    :: Map W256 ByteString   }   deriving (Show, Generic) 

@@ -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