Merge branch 'main' into branch-perf

CHANGELOG.md

@@ -14,16 +14,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - EVM.Solidity.toCode to include contractName in error string
 - Better cex reconstruction in cases where branches do not refer to all input variables in calldata
 - Correctly handle empty bytestring compiled contracts' JSON
+- `test` now falls back to displaying an unecoded bytestring for calldata when the model returned by the solver has a different length the length of the arguments in the test signature.
+- we now generate correct counterexamples for branches where only a subset of input variables are referenced by the path conditions
 
 ## Changed
 
 - Less noisy console output during tracing
 
 ### UI
 
-- 'check' prefix now recognized as a function signature to symbolically execute for Dapps
-- symbolic solidity tests no longer consider reverts to be a failure, and check only for the ds-test failed bit or unser defined assertion failures (i.e. `Panic(0x01)`)
+- `check` prefix now recognized for symbolic tests
+- solidity tests no longer consider reverts to be a failure, and check only for the ds-test failed bit or unser defined assertion failures (i.e. `Panic(0x01)`). A positive (i.e. non `proveFail`) test with no rechable assertion violations that does not have any succesful branches will still be considered a failure.
 - `vm.prank` now works correctly when passed a symbolic address
+- `test` now takes a `--number` argument to specify which block should be used when making rpc queries
 - The `--initial-storage` flag no longer accepts a concrete prestore (valid values are now `Empty` or `Abstract`)
 - The visual debugger has been removed
 - All concrete ds-test executors have been removed (i.e. plain, fuzzer, invariant)

cli/cli.hs

@@ -134,6 +134,7 @@ data Command w
       { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
       , projectType   :: w ::: Maybe ProjectType        <?> "Is this a Foundry or DappTools project (default: Foundry)"
       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
+      , number        :: w ::: Maybe W256               <?> "Block: number"
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
       , coverage      :: w ::: Bool                     <?> "Coverage analysis"
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"

flake.nix

@@ -33,6 +33,7 @@
           z3
           cvc5
           git
+        ] ++ lib.optional (!(pkgs.stdenv.isDarwin && pkgs.stdenv.isAarch64)) [
           foundry.defaultPackage.${system}
         ];
 

src/EVM/Expr.hs

@@ -847,6 +847,21 @@ isLitWord (Lit _) = True
 isLitWord (WAddr (LitAddr _)) = True
 isLitWord _ = False
 
+isSuccess :: Expr End -> Bool
+isSuccess = \case
+  Success {} -> True
+  _ -> False
+
+isFailure :: Expr End -> Bool
+isFailure = \case
+  Failure {} -> True
+  _ -> False
+
+isPartial :: Expr End -> Bool
+isPartial = \case
+  Partial {} -> True
+  _ -> False
+
 -- | Returns the byte at idx from the given word.
 indexWord :: Expr EWord -> Expr EWord -> Expr Byte
 -- Simplify masked reads:

src/EVM/Format.hs

@@ -142,7 +142,7 @@ showValue t b = head $ textValues [t] b
 
 showCall :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
 showCall ts (ConcreteBuf bs) = showValues ts $ ConcreteBuf (BS.drop 4 bs)
-showCall _ _ = "<symbolic>"
+showCall _ _ = "(<symbolic>)"
 
 showError :: (?context :: DappContext) => Expr Buf -> Text
 showError (ConcreteBuf bs) =
@@ -299,12 +299,12 @@ showTrace dapp env trace =
     FrameTrace (CreationContext addr (Lit hash) _ _ ) -> -- FIXME: irrefutable pattern
       "create "
       <> maybeContractName (preview (ix hash % _2) dapp.solcByHash)
-      <> "@" <> pack (show addr)
+      <> "@" <> formatAddr addr
       <> pos
     FrameTrace (CreationContext addr _ _ _ ) ->
       "create "
       <> "<unknown contract>"
-      <> "@" <> pack (show addr)
+      <> "@" <> formatAddr addr
       <> pos
     FrameTrace (CallContext target context _ _ hash abi calldata _ _) ->
       let calltype = if target == context
@@ -316,7 +316,7 @@ showTrace dapp env trace =
           calltype
             <> case target of
                  LitAddr 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D -> "HEVM"
-                 _ -> pack (show target)
+                 _ -> formatAddr target
             <> pack "::"
             <> case Map.lookup (unsafeInto (fromMaybe 0x00 abi)) fullAbiMap of
                  Just m  ->
@@ -342,6 +342,12 @@ showTrace dapp env trace =
             <> "\x1b[0m"
             <> pos
 
+formatAddr :: Expr EAddr -> Text
+formatAddr = \case
+  LitAddr a -> pack (show a)
+  SymAddr a -> "symbolic(" <> a <> ")"
+  GVar _ -> internalError "Unexpected GVar"
+
 getAbiTypes :: Text -> [Maybe AbiType]
 getAbiTypes abi = map (parseTypeName mempty) types
   where
@@ -427,7 +433,7 @@ formatPartial = \case
       , indent 2 $ T.unlines . fmap formatSomeExpr $ args
       ]
     ]
-  MaxIterationsReached pc addr -> T.pack $ "Max Iterations Reached in contract: " <> show addr <> " pc: " <> show pc
+  MaxIterationsReached pc addr -> "Max Iterations Reached in contract: " <> formatAddr addr <> " pc: " <> pack (show pc)
 
 formatSomeExpr :: SomeExpr -> Text
 formatSomeExpr (SomeExpr e) = formatExpr e

src/EVM/Solidity.hs

@@ -388,7 +388,9 @@ solcRuntime contract src = do
 functionAbi :: Text -> IO Method
 functionAbi f = do
   (json, path) <- solidity' ("contract ABI { function " <> f <> " public {}}")
-  let (Contracts sol, _, _) = fromJust $ readStdJSON json
+  let (Contracts sol, _, _) = fromMaybe
+                                (internalError . T.unpack $ "unable to parse solc output:\n" <> json)
+                                (readStdJSON json)
   case Map.toList $ (fromJust (Map.lookup (path <> ":ABI") sol)).abiMap of
      [(_,b)] -> pure b
      _ -> internalError "unexpected abi format"

src/EVM/SymExec.hs

@@ -878,8 +878,13 @@ formatCex cd m@(SMTCex _ _ _ store blockContext txContext) = T.unlines $
 -- but it's probably good enough for now
 defaultSymbolicValues :: Expr a -> Expr a
 defaultSymbolicValues e = subBufs (foldTerm symbufs mempty e)
-                        . subVars (foldTerm symwords mempty e) $ e
+                        . subVars (foldTerm symwords mempty e)
+                        . subAddrs (foldTerm symaddrs mempty e) $ e
   where
+    symaddrs :: Expr a -> Map (Expr EAddr) Addr
+    symaddrs = \case
+      a@(SymAddr _) -> Map.singleton a (Addr 0x1312)
+      _ -> mempty
     symbufs :: Expr a -> Map (Expr Buf) ByteString
     symbufs = \case
       a@(AbstractBuf _) -> Map.singleton a ""

src/EVM/UnitTest.hs

@@ -15,7 +15,7 @@ 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(..))
+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, defaultSymbolicValues, panicMsg, VeriOpts(..), flattenExpr)
 import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
@@ -228,17 +228,28 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
         get
 
     -- check postconditions against vm
-    (_, results) <- verify solvers (makeVeriOpts opts) vm' (Just postcondition)
+    (e, results) <- verify solvers (makeVeriOpts opts) vm' (Just postcondition)
+    let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
 
     -- display results
     if all isQed results
-    then do
-      pure ("\x1b[32m[PASS]\x1b[0m " <> testName, Right "")
+    then if allReverts && (not shouldFail)
+         then pure ("\x1b[31m[FAIL]\x1b[0m " <> testName, Left $ allBranchRev testName)
+         else pure ("\x1b[32m[PASS]\x1b[0m " <> testName, Right "")
     else do
       let x = mapMaybe extractCex results
       let y = symFailure opts testName (fst cd) types x
       pure ("\x1b[31m[FAIL]\x1b[0m " <> testName, Left y)
 
+allBranchRev :: Text -> Text
+allBranchRev testName = Text.unlines
+  [ "Failure: " <> testName
+  , ""
+  , indentLines 2 $ Text.unlines
+      [ "No reachable assertion violations, but all branches reverted"
+      , "Prefix this testname with `proveFail` if this is expected"
+      ]
+  ]
 symFailure :: UnitTestOptions RealWorld -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text
 symFailure UnitTestOptions {..} testName cd types failures' =
   mconcat
@@ -269,16 +280,17 @@ symFailure UnitTestOptions {..} testName cd types failures' =
             _ -> ""
         ]
 
-prettyCalldata :: (?context :: DappContext) => SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
-prettyCalldata cex buf sig types = head (Text.splitOn "(" sig) <> showCalldata cex types buf
-
-showCalldata :: (?context :: DappContext) => SMTCex -> [AbiType] -> Expr Buf -> Text
-showCalldata cex tps buf = "(" <> intercalate "," (fmap showVal vals) <> ")"
+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
-    vals = case decodeBuf tps argdata of
-             CAbi v -> v
-             _ -> internalError $ "unable to abi decode function arguments:\n" <> (Text.unpack $ formatExpr argdata)
+    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

test/contracts/fail/dsProveFail.sol

@@ -12,6 +12,10 @@ contract SolidityTest is DSTest {
         assert(false);
     }
 
+    function prove_all_branches_fail() public {
+        require(false);
+    }
+
     function prove_trivial_dstest() public {
         assertEq(uint(1), uint(2));
     }

test/contracts/pass/dsProvePass.sol

@@ -49,16 +49,21 @@ contract SolidityTest is DSTest {
     }
 
     // requires do not trigger a failure in `prove_` tests
-    function prove_no_fail_require() public {
-        require(false);
+    function prove_no_fail_require(uint x) public {
+        if (x == 2) {
+            require(false);
+        } else {
+            assert(x != 2);
+        }
     }
 
     // all branches in a proveFail test must end in one of:
     //  - a require
     //  - a failed user defined assert
     //  - a failed ds-test assertion violation
-    function proveFail_require() public {
-        require(false);
+    function proveFail_require(uint x) public {
+        require(x == 100);
+        assert(false);
     }
 
     function proveFail_userAssertSmoke() public {

test/test.hs

@@ -31,7 +31,7 @@ import GHC.Conc (getNumProcessors)
 import System.Directory
 import System.Environment
 import Test.Tasty
-import Test.Tasty.QuickCheck hiding (Failure, Success, isSuccess)
+import Test.Tasty.QuickCheck hiding (Failure, Success)
 import Test.QuickCheck.Instances.Text()
 import Test.QuickCheck.Instances.Natural()
 import Test.QuickCheck.Instances.ByteString()