Improve documentation and error handing for --code-a/--code-b

CHANGELOG.md

@@ -61,6 +61,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Respect --smt-timeout in equivalence checking
 - Fixed the handling of returndata with an abstract size during transaction finalization
 - Fixed handling of indices overflowing 2^256 when reading from buffers
+- Error handling for user-facing cli commands is much improved
 
 ## [0.53.0] - 2024-02-23
 

cli/cli.hs

@@ -12,7 +12,7 @@ import Control.Monad.IO.Unlift
 import Data.ByteString (ByteString)
 import Data.DoubleWord (Word256)
 import Data.List (intersperse)
-import Data.Maybe (fromMaybe, mapMaybe, fromJust)
+import Data.Maybe (fromMaybe, mapMaybe, fromJust, isNothing)
 import Data.Text qualified as T
 import Data.Text.IO qualified as T
 import Data.Version (showVersion)
@@ -243,35 +243,44 @@ main = withUtf8 $ do
 
 equivalence :: App m => Command Options.Unwrapped -> m ()
 equivalence cmd = do
-  let bytecodeA = hexByteString "--code" . strip0x $ cmd.codeA
-      bytecodeB = hexByteString "--code" . strip0x $ cmd.codeB
-      veriOpts = VeriOpts { simp = True
-                          , maxIter = cmd.maxIterations
-                          , askSmtIters = cmd.askSmtIterations
-                          , loopHeuristic = cmd.loopDetectionHeuristic
-                          , rpcInfo = Nothing
-                          }
-  calldata <- liftIO $ buildCalldata cmd
-  solver <- liftIO $ getSolver cmd
-  cores <- liftIO $ unsafeInto <$> getNumProcessors
-  let solverCount = fromMaybe cores cmd.numSolvers
-  withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \s -> do
-    res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata
-    case any isCex res of
-      False -> liftIO $ do
-        putStrLn "No discrepancies found"
-        when (any isUnknown res || any isError res) $ do
-          putStrLn "But the following issues occurred:"
-          forM_ (groupIssues (filter isError res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
-          forM_ (groupIssues (filter isUnknown res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+  let bytecodeA' = hexByteString $ strip0x cmd.codeA
+      bytecodeB' = hexByteString $ strip0x cmd.codeB
+  if (isNothing bytecodeA') then liftIO $ do
+    putStrLn $ "Error, invalid bytecode for program A: " <> show cmd.codeA
+    exitFailure
+  else if (isNothing bytecodeB') then liftIO $ do
+    putStrLn $ "Error, invalid bytecode for program B: " <> show cmd.codeB
+    exitFailure
+  else do
+    let bytecodeA = fromJust bytecodeA'
+        bytecodeB = fromJust bytecodeB'
+        veriOpts = VeriOpts { simp = True
+                            , maxIter = cmd.maxIterations
+                            , askSmtIters = cmd.askSmtIterations
+                            , loopHeuristic = cmd.loopDetectionHeuristic
+                            , rpcInfo = Nothing
+                            }
+    calldata <- liftIO $ buildCalldata cmd
+    solver <- liftIO $ getSolver cmd
+    cores <- liftIO $ unsafeInto <$> getNumProcessors
+    let solverCount = fromMaybe cores cmd.numSolvers
+    withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \s -> do
+      res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata
+      case any isCex res of
+        False -> liftIO $ do
+          putStrLn "No discrepancies found"
+          when (any isUnknown res || any isError res) $ do
+            putStrLn "But the following issues occurred:"
+            forM_ (groupIssues (filter isError res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+            forM_ (groupIssues (filter isUnknown res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+            exitFailure
+        True -> liftIO $ do
+          let cexs = mapMaybe getCex res
+          T.putStrLn . T.unlines $
+            [ "Not equivalent. The following inputs result in differing behaviours:"
+            , "" , "-----", ""
+            ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (formatCex (AbstractBuf "txdata") Nothing) cexs)
           exitFailure
-      True -> liftIO $ do
-        let cexs = mapMaybe getCex res
-        T.putStrLn . T.unlines $
-          [ "Not equivalent. The following inputs result in differing behaviours:"
-          , "" , "-----", ""
-          ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (formatCex (AbstractBuf "txdata") Nothing) cexs)
-        exitFailure
 
 getSolver :: Command Options.Unwrapped -> IO Solver
 getSolver cmd = case cmd.solver of
@@ -311,7 +320,12 @@ buildCalldata cmd = case (cmd.calldata, cmd.sig) of
   -- fully abstract calldata
   (Nothing, Nothing) -> pure $ mkCalldata Nothing []
   -- fully concrete calldata
-  (Just c, Nothing) -> pure (ConcreteBuf (hexByteString "bytes" . strip0x $ c), [])
+  (Just c, Nothing) -> do
+    let val = hexByteString $ strip0x c
+    if (isNothing val) then do
+      putStrLn $ "Error, invalid calldata: " <>  show c
+      exitFailure
+    else pure (ConcreteBuf (fromJust val), [])
   -- calldata according to given abi with possible specializations from the `arg` list
   (Nothing, Just sig') -> do
     method' <- functionAbi sig'
@@ -425,7 +439,9 @@ vmFromCommand cmd = do
   (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of
     Nothing -> pure (LitAddr 0,Lit 0,0,0,0)
     Just url -> Fetch.fetchBlockFrom block url >>= \case
-      Nothing -> error "Error: Could not fetch block"
+      Nothing -> do
+        putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url
+        exitFailure
       Just Block{..} -> pure ( coinbase
                              , timestamp
                              , baseFee
@@ -435,44 +451,60 @@ vmFromCommand cmd = do
 
   contract <- case (cmd.rpc, cmd.address, cmd.code) of
     (Just url, Just addr', Just c) -> do
-      Fetch.fetchContractFrom block url addr' >>= \case
-        Nothing ->
-          error $ "Error: contract not found: " <> show address
-        Just contract ->
-          -- if both code and url is given,
-          -- fetch the contract and overwrite the code
-          pure $
-            initialContract  (mkCode $ hexByteString "--code" $ strip0x c)
-              & set #balance  (contract.balance)
-              & set #nonce    (contract.nonce)
-              & set #external (contract.external)
+      let code = hexByteString $ strip0x c
+      if (isNothing code) then do
+        putStrLn $ "Error, invalid code: " <> show c
+        exitFailure
+      else
+        Fetch.fetchContractFrom block url addr' >>= \case
+          Nothing -> do
+            putStrLn $ "Error: contract not found: " <> show address
+            exitFailure
+          Just contract ->
+            -- if both code and url is given,
+            -- fetch the contract and overwrite the code
+            pure $
+              initialContract  (mkCode $ fromJust code)
+                & set #balance  (contract.balance)
+                & set #nonce    (contract.nonce)
+                & set #external (contract.external)
 
     (Just url, Just addr', Nothing) ->
       Fetch.fetchContractFrom block url addr' >>= \case
-        Nothing ->
-          error $ "Error: contract not found: " <> show address
+        Nothing -> do
+          putStrLn $ "Error, contract not found: " <> show address
+          exitFailure
         Just contract -> pure contract
 
-    (_, _, Just c)  ->
-      pure $
-        initialContract (mkCode $ hexByteString "--code" $ strip0x c)
+    (_, _, Just c)  -> do
+      let code = hexByteString $ strip0x c
+      if (isNothing code) then do
+        putStrLn $ "Error, invalid code: " <> show c
+        exitFailure
+      else pure $ initialContract (mkCode $ fromJust code)
 
-    (_, _, Nothing) ->
-      error "Error: must provide at least (rpc + address) or code"
+    (_, _, Nothing) -> do
+      putStrLn "Error, must provide at least (rpc + address) or code"
+      exitFailure
 
   let ts' = case maybeLitWord ts of
         Just t -> t
         Nothing -> internalError "unexpected symbolic timestamp when executing vm test"
 
-  vm <- stToIO $ vm0 baseFee miner ts' blockNum prevRan contract
-  pure $ EVM.Transaction.initTx vm
-    where
+  if (isNothing bsCallData) then do
+    putStrLn $ "Error, invalid calldata: " <> show calldata
+    exitFailure
+  else do
+    vm <- stToIO $ vm0 baseFee miner ts' blockNum prevRan contract
+    pure $ EVM.Transaction.initTx vm
+  where
+        bsCallData = bytes (.calldata) (pure "")
         block   = maybe Fetch.Latest Fetch.BlockNumber cmd.block
         value   = word (.value) 0
         caller  = addr (.caller) (LitAddr 0)
         origin  = addr (.origin) (LitAddr 0)
-        calldata = ConcreteBuf $ bytes (.calldata) ""
-        decipher = hexByteString "bytes" . strip0x
+        calldata = ConcreteBuf $ fromJust bsCallData
+        decipher = hexByteString . strip0x
         mkCode bs = if cmd.create
                     then InitCode bs mempty
                     else RuntimeCode (ConcreteRuntimeCode bs)
@@ -518,7 +550,9 @@ symvmFromCommand cmd calldata = do
   (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of
     Nothing -> pure (SymAddr "miner",0,0,0)
     Just url -> Fetch.fetchBlockFrom block url >>= \case
-      Nothing -> error "Error: Could not fetch block"
+      Nothing -> do
+        putStrLn "Error, could not fetch block"
+        exitFailure
       Just Block{..} -> pure ( coinbase
                              , number
                              , baseFee
@@ -534,32 +568,43 @@ symvmFromCommand cmd calldata = do
   contract <- case (cmd.rpc, cmd.address, cmd.code) of
     (Just url, Just addr', _) ->
       Fetch.fetchContractFrom block url addr' >>= \case
-        Nothing ->
-          error "Error: contract not found."
-        Just contract' -> pure contract''
-          where
-            contract'' = case cmd.code of
-              Nothing -> contract'
+        Nothing -> do
+          putStrLn "Error, contract not found."
+          exitFailure
+        Just contract' -> case cmd.code of
+              Nothing -> pure contract'
               -- if both code and url is given,
               -- fetch the contract and overwrite the code
-              Just c -> initialContract (mkCode $ decipher c)
+              Just c -> do
+                let c' = decipher c
+                if (isNothing c') then do
+                  putStrLn $ "Error, invalid code: " <> show c
+                  exitFailure
+                else pure $ do
+                  initialContract (mkCode $ fromJust c')
                         & set #origStorage (contract'.origStorage)
                         & set #balance     (contract'.balance)
                         & set #nonce       (contract'.nonce)
                         & set #external    (contract'.external)
 
-    (_, _, Just c)  -> case storageBase of
-      EmptyBase -> pure (initialContract . mkCode $ decipher c)
-      AbstractBase -> pure ((`abstractContract` address) . mkCode $ decipher c)
+    (_, _, Just c)  -> do
+      let c' = decipher c
+      if (isNothing c') then do
+        putStrLn $ "Error, invalid code: " <> show c
+        exitFailure
+      else case storageBase of
+        EmptyBase -> pure (initialContract . mkCode $ fromJust c')
+        AbstractBase -> pure ((`abstractContract` address) . mkCode $ fromJust c')
 
-    (_, _, Nothing) ->
-      error "Error: must provide at least (rpc + address) or code"
+    (_, _, Nothing) -> do
+      putStrLn "Error, must provide at least (rpc + address) or code"
+      exitFailure
 
   vm <- stToIO $ vm0 baseFee miner ts blockNum prevRan calldata callvalue caller contract storageBase
   pure $ EVM.Transaction.initTx vm
 
   where
-    decipher = hexByteString "bytes" . strip0x
+    decipher = hexByteString . strip0x
     block = maybe Fetch.Latest Fetch.BlockNumber cmd.block
     origin = eaddr (.origin) (SymAddr "origin")
     mkCode bs = if cmd.create

doc/src/equivalence-checking-tutorial.md

@@ -122,3 +122,19 @@ consume the same amount of gas and have widely different EVM bytecodes. Yet for
 an outside observer, they behave the same. Notice that hevm didn't simply fuzz
 the contract and within a given out of time it didn't find a counterexample.
 Instead, it _proved_ the two equivalent from an outside observer perspective.
+
+## Dealing with Already Compiled Contracts
+
+If the contracts have already been compiled into a hex string, you can paste
+them into files `a.txt` and `b.txt` and compare them via:
+
+```shell
+$ hevm equivalence --code-a "$(<a.txt)" --code-b "$(<b.txt)"
+```
+
+You can also copy-paste the contents of the hex strings directly into the
+command line, although this can become cumbersome:
+
+```shell
+$ hevm equivalence --code-a "6080604052348015600e575f80fd5b50600436106026575f3560e01c8063881fc77c14602a575b5f80fd5b60306032565b005b5f600190506002811460455760446048565b5b50565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea26469706673582212208c57ae04774d9ebae7d1d11f9d5e730075068bc7988d4c83c6fed85b7f062e7b64736f6c634300081a0033" --code-b "6080604052348015600e575f80fd5b50600436106030575f3560e01c806385c2fc7114603457806386ae330914603c575b5f80fd5b603a6044565b005b60426055565b005b60025f541460535760526066565b5b565b60035f541460645760636066565b5b565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220bd2f8a1ba281308f845e212d2b5eceab85e029909fa2409cdca7ede039bae26564736f6c634300081a0033"
+```

src/EVM/Format.hs

@@ -824,11 +824,11 @@ strip0x bs = if "0x" `Char8.isPrefixOf` bs then Char8.drop 2 bs else bs
 strip0x' :: String -> String
 strip0x' s = if "0x" `isPrefixOf` s then drop 2 s else s
 
-hexByteString :: String -> ByteString -> ByteString
-hexByteString msg bs =
+hexByteString :: ByteString -> Maybe ByteString
+hexByteString bs =
   case BS16.decodeBase16Untyped bs of
-    Right x -> x
-    _ -> internalError $ "invalid hex bytestring for " ++ msg
+    Right x -> pure x
+    Left _ -> Nothing
 
 hexText :: Text -> ByteString
 hexText t =