From 3e48d37e161fe6010f68a821300adf8fbf65fe57 Mon Sep 17 00:00:00 2001 From: dxo Date: Mon, 2 Oct 2023 15:55:23 +0200 Subject: [PATCH] SymExec: formatCex decodes calldata if an abi is known --- cli/cli.hs | 4 ++-- src/EVM/Format.hs | 6 ++++++ src/EVM/SymExec.hs | 24 +++++++++++++++++++----- src/EVM/UnitTest.hs | 21 ++------------------- 4 files changed, 29 insertions(+), 26 deletions(-) diff --git a/cli/cli.hs b/cli/cli.hs index 99b70b0fc..fa7165cd5 100644 --- 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 index 7b24a6fe9..3337f424d 100644 --- 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) @@ -802,3 +803,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 index 5a02a45d9..dfc886bfc 100644 --- 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 @@ -811,7 +811,7 @@ 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 "" @@ -819,8 +819,8 @@ showModel cd (expr, res) = do 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' , "" @@ -836,7 +836,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 @@ -892,6 +894,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 index d41fa98bf..7f8a0b200 100644 --- 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