Merge pull request #393 from ethereum/formatcex-abi-decode

SymExec: formatCex decodes calldata if an abi is known
ethereum · Oct 5, 2023 · 6c32727 · 6c32727
2 parents c5e4050 + 3e48d37
commit 6c32727
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 26 deletions.
diff --git a/cli/cli.hs b/cli/cli.hs
@@ -238,7 +238,7 @@ equivalence cmd = do
         T.putStrLn . T.unlines $
           [ "Not equivalent. The following inputs result in differing behaviours:"
           , "" , "-----", ""
-          ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (formatCex (AbstractBuf "txdata")) cexs)
+          ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (formatCex (AbstractBuf "txdata") Nothing) cexs)
         exitFailure
 
 getSolver :: Command Options.Unwrapped -> IO Solver
@@ -322,7 +322,7 @@ assert cmd = do
                  [ ""
                  , "Discovered the following counterexamples:"
                  , ""
-                 ] <> fmap (formatCex (fst calldata)) cexs
+                 ] <> fmap (formatCex (fst calldata) Nothing) cexs
             unknowns
               | null timeouts = []
               | otherwise =

diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs
@@ -30,6 +30,7 @@ module EVM.Format
   , hexByteString
   , hexText
   , bsToHex
+  , showVal
   ) where
 
 import Prelude hiding (LT, GT)
@@ -803,3 +804,8 @@ hexText t =
 
 bsToHex :: ByteString -> String
 bsToHex bs = concatMap (paddedShowHex 2) (BS.unpack bs)
+
+showVal :: AbiValue -> Text
+showVal (AbiBytes _ bs) = formatBytes bs
+showVal (AbiAddress addr) = T.pack  . show $ addr
+showVal v = T.pack . show $ v
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
@@ -33,7 +33,7 @@ import EVM.Exec
 import EVM.Fetch qualified as Fetch
 import EVM.ABI
 import EVM.Expr qualified as Expr
-import EVM.Format (formatExpr, formatPartial)
+import EVM.Format (formatExpr, formatPartial, showVal, bsToHex)
 import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2)
 import EVM.SMT qualified as SMT
 import EVM.Solvers
@@ -812,16 +812,16 @@ showModel cd (expr, res) = do
       putStrLn ""
       putStrLn "Inputs:"
       putStrLn ""
-      T.putStrLn $ indent 2 $ formatCex cd cex
+      T.putStrLn $ indent 2 $ formatCex cd Nothing cex
       putStrLn ""
       putStrLn "End State:"
       putStrLn ""
       T.putStrLn $ indent 2 $ formatExpr expr
       putStrLn ""
 
 
-formatCex :: Expr Buf -> SMTCex -> Text
-formatCex cd m@(SMTCex _ _ _ store blockContext txContext) = T.unlines $
+formatCex :: Expr Buf -> Maybe Sig -> SMTCex -> Text
+formatCex cd sig m@(SMTCex _ _ _ store blockContext txContext) = T.unlines $
   [ "Calldata:"
   , indent 2 cd'
   , ""
@@ -837,7 +837,9 @@ formatCex cd m@(SMTCex _ _ _ store blockContext txContext) = T.unlines $
     -- it for branches that do not refer to calldata at all (e.g. the top level
     -- callvalue check inserted by solidity in contracts that don't have any
     -- payable functions).
-    cd' = prettyBuf . Expr.simplify . defaultSymbolicValues $ subModel m cd
+    cd' = case sig of
+      Nothing -> prettyBuf . Expr.simplify . defaultSymbolicValues $ subModel m cd
+      Just (Sig n ts) -> prettyCalldata m cd n ts
 
     storeCex :: [Text]
     storeCex
@@ -893,6 +895,18 @@ formatCex cd m@(SMTCex _ _ _ store blockContext txContext) = T.unlines $
     prettyBuf (ConcreteBuf bs) = formatBinary bs
     prettyBuf b = internalError $ "Unexpected symbolic buffer:\n" <> T.unpack (formatExpr b)
 
+prettyCalldata :: SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
+prettyCalldata cex buf sig types = head (T.splitOn "(" sig) <> "(" <> body <> ")"
+  where
+    argdata = Expr.drop 4 . Expr.simplify . defaultSymbolicValues $ subModel cex buf
+    body = case decodeBuf types argdata of
+      CAbi v -> T.intercalate "," (fmap showVal v)
+      NoVals -> case argdata of
+          ConcreteBuf c -> T.pack (bsToHex c)
+          _ -> err
+      SAbi _ -> err
+    err = internalError $ "unable to produce a concrete model for calldata: " <> show buf
+
 -- | If the expression contains any symbolic values, default them to some
 -- concrete value The intuition here is that if we still have symbolic values
 -- in our calldata expression after substituing in our cex, then they can have

diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
@@ -9,13 +9,13 @@ import EVM.SMT
 import EVM.Solvers
 import EVM.Dapp
 import EVM.Exec
-import EVM.Expr (readStorage', simplify)
+import EVM.Expr (readStorage')
 import EVM.Expr qualified as Expr
 import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
 import EVM.Format
 import EVM.Solidity
-import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, defaultSymbolicValues, panicMsg, VeriOpts(..), flattenExpr)
+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr)
 import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
@@ -280,23 +280,6 @@ symFailure UnitTestOptions {..} testName cd types failures' =
             _ -> ""
         ]
 
-prettyCalldata :: SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
-prettyCalldata cex buf sig types = head (Text.splitOn "(" sig) <> "(" <> body <> ")"
-  where
-    argdata = Expr.drop 4 . simplify . defaultSymbolicValues $ subModel cex buf
-    body = case decodeBuf types argdata of
-      CAbi v -> intercalate "," (fmap showVal v)
-      NoVals -> case argdata of
-          ConcreteBuf c -> pack (bsToHex c)
-          _ -> err
-      SAbi _ -> err
-    err = internalError $ "unable to produce a concrete model for calldata: " <> show buf
-
-showVal :: AbiValue -> Text
-showVal (AbiBytes _ bs) = formatBytes bs
-showVal (AbiAddress addr) = Text.pack  . show $ addr
-showVal v = Text.pack . show $ v
-
 execSymTest :: UnitTestOptions RealWorld -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper RealWorld (Expr End)
 execSymTest UnitTestOptions{ .. } method cd = do
   -- Set up the call to the test method