Merge pull request #276 from crytic/dev-assertions-take2

Detect assertion failure

examples/solidity/basic/assert.sol

@@ -0,0 +1,7 @@
+contract Test {
+  function set0(int val) public returns (bool){
+    assert(val % 100 != 0);
+  }
+  function set1(int val) public returns (bool){
+  }
+}

examples/solidity/basic/assert.yaml

@@ -0,0 +1 @@
+checkAsserts: true

lib/Echidna/ABI.hs

@@ -24,11 +24,12 @@ import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
 import Data.Text (Text)
 import Data.Vector (Vector)
 import Data.Word8 (Word8)
-import EVM.ABI (AbiType(..), AbiValue(..), abiValueType)
+import EVM.ABI (AbiType(..), AbiValue(..), abiTypeSolidity, abiValueType)
 import Numeric (showHex)
 
 import qualified Data.ByteString as BS
 import qualified Data.HashMap.Strict as M
+import qualified Data.Text as T
 import qualified Data.Vector as V
 
 -- | Pretty-print some 'AbiValue'.
@@ -72,6 +73,10 @@ type SolCall      = (Text, [AbiValue])
 -- A tuple of 'Text' for the name of the function, and then the 'AbiType's of any arguments it expects.
 type SolSignature = (Text, [AbiType])
 
+-- | Get the text signature of a solidity method (for later hashing)
+encodeSig :: SolSignature -> Text
+encodeSig (n, ts) = n <> "(" <> T.intercalate "," (abiTypeSolidity <$> ts) <> ")"
+
 -- | Configuration necessary for generating new 'SolCalls'. Don't construct this by hand! Use 'mkConf'.
 data GenDict = GenDict { _pSynthA    :: Float
                          -- ^ Fraction of time to use dictionary vs. synthesize

lib/Echidna/Campaign.hs

@@ -20,7 +20,6 @@ import Control.Monad.State.Strict (MonadState(..), StateT(..), evalStateT, execS
 import Control.Monad.Trans (lift)
 import Control.Monad.Trans.Random.Strict (liftCatch)
 import Data.Aeson (ToJSON(..), object)
-import Data.Bifunctor (Bifunctor(..))
 import Data.Binary.Get (runGetOrFail)
 import Data.Bool (bool)
 import Data.Either (lefts)
@@ -30,7 +29,6 @@ import Data.Maybe (fromMaybe, isNothing, mapMaybe, maybeToList)
 import Data.Ord (comparing)
 import Data.Has (Has(..))
 import Data.Set (Set, union)
-import Data.Text (unpack)
 import EVM
 import EVM.ABI
 import EVM.Types (W256)
@@ -94,8 +92,11 @@ data Campaign = Campaign { _tests    :: [(SolTest, TestState)] -- ^ Tests being
                          }
 
 instance ToJSON Campaign where
-  toJSON (Campaign ts co _) = object $ ("tests", toJSON $ bimap (unpack . fst) toJSON <$> ts)
-    : if co == mempty then [] else [("coverage",) . toJSON . mapKeys (`showHex` "") $ toList <$> co]
+  toJSON (Campaign ts co _) = object $ ("tests", toJSON $ mapMaybe format ts)
+    : if co == mempty then [] else [("coverage",) . toJSON . mapKeys (`showHex` "") $ toList <$> co] where
+      format (Right _,      Open _) = Nothing
+      format (Right (n, _), s)      = Just ("assertion in " <> n, toJSON s)
+      format (Left (n, _),  s)      = Just (n,                    toJSON s)
 
 makeLenses ''Campaign
 

lib/Echidna/Config.hs

@@ -96,7 +96,8 @@ instance FromJSON EConfig where
                          <*> v .:? "prefix"         .!= "echidna_"
                          <*> v .:? "solcArgs"       .!= ""
                          <*> v .:? "solcLibs"       .!= []
-                         <*> v .:? "quiet"          .!= False)
+                         <*> v .:? "quiet"          .!= False
+                         <*> v .:? "checkAsserts"   .!= False)
             <*> tc
             <*> xc
             <*> (UIConf <$> v .:? "dashboard" .!= True <*> style)

lib/Echidna/Exec.hs

@@ -67,8 +67,11 @@ execTxWith :: (MonadState x m, Has VM x) => (Error -> m ()) -> m VMResult -> Tx
 execTxWith h m t = do og <- get
                       setupTx t
                       res <- m
+                      cd  <- use $ hasLens . state . calldata
                       case (res, isRight $ t ^. call) of
-                        (f@Reversion, _)         -> put og >> liftSH (result .= Just f)
+                        (f@Reversion, _)         -> do put og 
+                                                       hasLens . state . calldata .= cd
+                                                       hasLens . result ?= f
                         (VMFailure x, _)         -> h x
                         (VMSuccess bc, True)     -> (hasLens %=) . execState $ do
                           env . contracts . at (t ^. dst) . _Just . contractcode .= InitCode ""

lib/Echidna/Solidity.hs

@@ -72,18 +72,23 @@ instance Show SolException where
 instance Exception SolException
 
 -- | Configuration for loading Solidity for Echidna testing.
-data SolConf = SolConf { _contractAddr    :: Addr    -- ^ Contract address to use
-                       , _deployer        :: Addr    -- ^ Contract deployer address to use
-                       , _sender          :: [Addr]  -- ^ Sender addresses to use
-                       , _balanceAddr     :: Integer -- ^ Initial balance of deployer and senders
-                       , _balanceContract :: Integer -- ^ Initial balance of contract to test
-                       , _prefix          :: Text    -- ^ Function name prefix used to denote tests
-                       , _solcArgs        :: String  -- ^ Args to pass to @solc@
+data SolConf = SolConf { _contractAddr    :: Addr     -- ^ Contract address to use
+                       , _deployer        :: Addr     -- ^ Contract deployer address to use
+                       , _sender          :: [Addr]   -- ^ Sender addresses to use
+                       , _balanceAddr     :: Integer  -- ^ Initial balance of deployer and senders
+                       , _balanceContract :: Integer  -- ^ Initial balance of contract to test
+                       , _prefix          :: Text     -- ^ Function name prefix used to denote tests
+                       , _solcArgs        :: String   -- ^ Args to pass to @solc@
                        , _solcLibs        :: [String] -- ^ List of libraries to load, in order.
-                       , _quiet           :: Bool    -- ^ Suppress @solc@ output, errors, and warnings
+                       , _quiet           :: Bool     -- ^ Suppress @solc@ output, errors, and warnings
+                       , _checkAsserts    :: Bool     -- ^ Test if we can cause assertions to fail
                        }
 makeLenses ''SolConf
 
+-- | An Echidna test is either the name of the function to call and the address where its contract is,
+-- or a function that could experience an exception
+type SolTest = Either (Text, Addr) SolSignature
+
 -- | Given a file, use its extenstion to check if it is a precompiled contract or try to compile it and
 -- get a list of its contracts, throwing exceptions if necessary.
 contracts :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x) => FilePath -> m [SolcContract]
@@ -100,9 +105,8 @@ contracts fp = let usual = ["--solc-disable-warnings", "--export-format", "solc"
 
 
 addresses :: (MonadReader x m, Has SolConf x) => m [AbiValue]
-addresses = do 
-              (SolConf ca d ads _ _ _ _ _ _) <- view hasLens
-              return $ map (AbiAddress . fromIntegral) $ nub $ ads ++ [ca, d, 0x0]
+addresses = view hasLens <&> \(SolConf ca d ads _ _ _ _ _ _ _) ->
+  AbiAddress . fromIntegral <$> nub (ads ++ [ca, d, 0x0])
 
 populateAddresses :: [Addr] -> Integer -> VM -> VM
 populateAddresses []     _ vm = vm
@@ -143,7 +147,7 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
     unless q . putStrLn $ "Analyzing contract: " <> c ^. contractName . unpacked
 
   -- Local variables
-  (SolConf ca d ads bala balc pref _ libs _) <- view hasLens
+  (SolConf ca d ads bala balc pref _ libs _ ch) <- view hasLens
   let bc = c ^. creationCode
       blank = populateAddresses (ads |> d) bala (vmForEthrunCreation bc)
       abi = liftM2 (,) (view methodName) (fmap snd . view methodInputs) <$> toList (c ^. abiMap)
@@ -153,10 +157,11 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
   ls <- mapM (choose cs . Just . T.pack) libs
 
   -- Make sure everything is ready to use, then ship it
-  mapM_ (uncurry ensure) [(abi, NoFuncs), (tests, NoTests), (funs, OnlyTests)] -- ABI checks
-  ensure bc (NoBytecode $ c ^. contractName)                                   -- Bytecode check
+  mapM_ (uncurry ensure) $ [(abi, NoFuncs), (funs, OnlyTests)]
+                        ++ if ch then [] else [(tests, NoTests)] -- ABI checks
+  ensure bc (NoBytecode $ c ^. contractName)                     -- Bytecode check
   case find (not . null . snd) tests of
-    Just (t,_) -> throwM $ TestArgsFound t                                     -- Test args check
+    Just (t,_) -> throwM $ TestArgsFound t                       -- Test args check
     Nothing    -> loadLibraries ls addrLibrary d blank >>= fmap (, fallback : funs, fst <$> tests) .
       execStateT (execTx $ Tx (Right bc) d ca 0xffffffff (w256 $ fromInteger balc))
 
@@ -182,14 +187,15 @@ loadWithCryticCompile fp name = contracts fp >>= loadSpecified name
 -- | Given the results of 'loadSolidity', assuming a single-contract test, get everything ready
 -- for running a 'Campaign' against the tests found.
 prepareForTest :: (MonadReader x m, Has SolConf x)
-               => (VM, [SolSignature], [Text]) -> m (VM, World, [(Text, Addr)])
-prepareForTest (v, a, ts) = let r = v ^. state . contract in
-  view (hasLens . sender) <&> \s -> (v, World s [(r, a)], zip ts $ repeat r)
+               => (VM, [SolSignature], [Text]) -> m (VM, World, [SolTest])
+prepareForTest (v, a, ts) = view hasLens <&> \(SolConf _ _ s _ _ _ _ _ _ ch) ->
+  (v, World s [(r, a)], fmap Left (zip ts $ repeat r) ++ if ch then Right <$> drop 1 a else []) where
+    r = v ^. state . contract
 
 -- | Basically loadSolidity, but prepares the results to be passed directly into
 -- a testing function.
 loadSolTests :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x)
-             => FilePath -> Maybe Text -> m (VM, World, [(Text, Addr)])
+             => FilePath -> Maybe Text -> m (VM, World, [SolTest])
 loadSolTests fp name = loadWithCryticCompile fp name >>= prepareForTest
 
 mkValidAbiInt :: Int -> Int256 -> Maybe AbiValue

lib/Echidna/Test.hs

@@ -9,23 +9,23 @@ import Control.Monad ((<=<), ap)
 import Control.Monad.Catch (MonadThrow)
 import Control.Monad.Random.Strict (MonadRandom, getRandomR, uniform, uniformMay)
 import Control.Monad.Reader.Class (MonadReader, asks)
-import Control.Monad.State.Strict (MonadState(..), gets)
+import Control.Monad.State.Strict (MonadState(get, put), gets)
 import Data.Bool (bool)
 import Data.Foldable (traverse_)
 import Data.Has (Has(..))
 import Data.Maybe (fromMaybe)
 import Data.Text (Text)
-import EVM (VMResult(..), VM)
-import EVM.ABI (AbiValue(..), encodeAbiValue)
+import EVM (Error(..), VMResult(..), VM, calldata, result, state)
+import EVM.ABI (AbiValue(..), abiCalldata, encodeAbiValue)
 import EVM.Types (Addr)
 
+import qualified Data.ByteString as BS
+
+import Echidna.ABI
 import Echidna.Exec
 import Echidna.Solidity
 import Echidna.Transaction
 
--- | An Echidna test is just the name of the function to call and the address where its contract is.
-type SolTest = (Text, Addr)
-
 -- | Configuration for evaluating Echidna tests.
 data TestConf = TestConf { classifier :: Text -> VM -> Bool
                            -- ^ Given a VM state and test name, check if a test just passed (typically
@@ -48,10 +48,22 @@ classifyRes Reversion = ResRevert
 classifyRes _ = ResOther
 
 -- | Given a 'SolTest', evaluate it and see if it currently passes.
-checkETest :: (MonadReader x m, Has TestConf x, Has TxConf x, MonadState y m, Has VM y, MonadThrow m) => SolTest -> m Bool
-checkETest (f, a) = asks getter >>= \(TestConf p s) -> view (hasLens . propGas) >>= \g -> do
+checkETest :: (MonadReader x m, Has TestConf x, Has TxConf x, MonadState y m, Has VM y, MonadThrow m)
+           => SolTest -> m Bool
+checkETest t = asks getter >>= \(TestConf p s) -> view (hasLens . propGas) >>= \g -> do
   og <- get 
-  res <- execTx (Tx (Left (f, [])) (s a) a g 0) >> gets (p f . getter)
+  -- To check these tests, we're going to need a couple auxilary functions:
+  --   * matchR[eturn] checks if we just tried to exec 0xfe, which means we failed an assert
+  --   * matchC[alldata] checks if we just executed the function we thought we did, based on calldata
+  let matchR (Just (VMFailure (UnrecognizedOpcode 0xfe))) = False
+      matchR _                                            = True
+      matchC sig = not . (BS.isPrefixOf . BS.take 4 $ abiCalldata (encodeSig sig) mempty)
+  res <- case t of
+    -- If our test is a regular user-defined test, we exec it and check the result
+    Left  (f, a) -> execTx (Tx (Left (f, [])) (s a) a g 0) >> gets (p f . getter)
+    -- If our test is an auto-generated assertion test, we check if we failed an assert on that fn
+    Right sig    -> (||) <$> fmap matchR       (use $ hasLens . result)
+                         <*> fmap (matchC sig) (use $ hasLens . state . calldata)
   put og
   pure res
 

lib/Echidna/Transaction.hs

@@ -21,7 +21,7 @@ import Data.Has (Has(..))
 import Data.List (intercalate)
 import Data.Set (Set)
 import EVM
-import EVM.ABI (abiCalldata, abiTypeSolidity, abiValueType)
+import EVM.ABI (abiCalldata, abiValueType)
 import EVM.Concrete (Word(..), w256)
 import EVM.Types (Addr)
 
@@ -133,4 +133,4 @@ setupTx (Tx c s r g v) = liftSH . sequence_ $
       Left cd  -> loadContract r >> state . calldata .= encode cd
       Right bc -> assign (env . contracts . at r) (Just $ initialContract (RuntimeCode bc) & set balance v) >> loadContract r
     encode (n, vs) = abiCalldata
-      (n <> "(" <> T.intercalate "," (abiTypeSolidity . abiValueType <$> vs) <> ")") $ V.fromList vs
+      (encodeSig (n, abiValueType <$> vs)) $ V.fromList vs

lib/Echidna/UI.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Echidna.UI where
 
@@ -20,7 +21,7 @@ import Data.Either (either)
 import Data.Has (Has(..))
 import Data.List (nub)
 import Data.Map (Map)
-import Data.Maybe (maybe, fromMaybe)
+import Data.Maybe (catMaybes, maybe, fromMaybe)
 import Data.Set (Set)
 import EVM (VM)
 import EVM.Types (Addr, W256)
@@ -85,7 +86,10 @@ ppTS (Large n l) = view (hasLens . to shrinkLimit) >>= \m -> ppFail (if n < m th
 
 -- | Pretty-print the status of all 'SolTest's in a 'Campaign'.
 ppTests :: (MonadReader x m, Has CampaignConf x, Has Names x, Has TxConf x) => Campaign -> m String
-ppTests (Campaign ts _ _) = unlines <$> mapM (\((n, _), s) -> ((T.unpack n ++ ": ") ++ ) <$> ppTS s) ts
+ppTests (Campaign ts _ _) = unlines . catMaybes <$> mapM pp ts where
+  pp (Left  (n, _), s)      = Just .                    ((T.unpack n ++ ": ") ++) <$> ppTS s
+  pp (Right _,      Open _) = pure Nothing
+  pp (Right (n, _), s)      = Just . (("assertion in " ++ T.unpack n ++ ": ") ++) <$> ppTS s
 
 -- | Pretty-print the coverage a 'Campaign' has obtained.
 ppCoverage :: Map W256 (Set Int) -> Maybe String

src/Main.hs

@@ -32,7 +32,6 @@ opts = info (options <**> helper) $ fullDesc
   <> header "Echidna"
 
 main :: IO ()
-
 main = do Options f c conf <- execParser opts
           g   <- getRandom
           cfg <- maybe (pure defaultConfig) parseConfig conf

src/test/Spec.hs

@@ -110,7 +110,7 @@ integrationTests = testGroup "Solidity Integration Testing"
         ("echidna_all_sender solved without " ++ unpack n, solvedWith (n, []) "echidna_all_sender"))
 
   , testContract "basic/memory-reset.sol" Nothing
-      [ ("echidna_memory failed",      passed "echidna_memory") ]
+      [ ("echidna_memory failed",                  passed      "echidna_memory") ]
   , testContract "basic/contractAddr.sol" Nothing
       [ ("echidna_address failed",                 solved      "echidna_address") ]
   , testContract "basic/contractAddr.sol" (Just "basic/contractAddr.yaml")
@@ -131,18 +131,21 @@ integrationTests = testGroup "Solidity Integration Testing"
   , testContract "basic/balance.sol"      (Just "basic/balance.yaml")
       [ ("echidna_balance failed",                 passed      "echidna_balance") ]
   , testContract "basic/library.sol"      (Just "basic/library.yaml")
-      [ ("echidna_library_call failed",            solved "echidna_library_call") ]
+      [ ("echidna_library_call failed",            solved      "echidna_library_call") ]
   , testContract "harvey/foo.sol"         Nothing
-      [ ("echidna_assert failed",                  solved "echidna_assert") ]
+      [ ("echidna_assert failed",                  solved      "echidna_assert") ]
   , testContract "harvey/baz.sol"         Nothing
-      [ ("echidna_all_states failed",              solved "echidna_all_states") ]
+      [ ("echidna_all_states failed",              solved      "echidna_all_states") ]
   , testContract "basic/fallback.sol"     Nothing
       [ ("echidna_fallback failed",                solved      "echidna_fallback") ]
   , testContract "basic/darray.sol"       Nothing
       [ ("echidna_darray passed",                  solved      "echidna_darray")
       , ("echidna_darray didn't shrink optimally", solvedLen 1 "echidna_darray") ]
   , testContract "basic/propGasLimit.sol" (Just "basic/propGasLimit.yaml") 
-      [ ("echidna_runForever passed",              solved      "echidna_runForever")]
+      [ ("echidna_runForever passed",              solved      "echidna_runForever") ]
+  , testContract "basic/assert.sol"       (Just "basic/assert.yaml") 
+      [ ("echidna_set0 passed",                    solved      "ASSERTION set0")
+      , ("echidna_set1 failed",                    passed      "ASSERTION set1") ]
   ]
 
 testContract :: FilePath -> Maybe FilePath -> [(String, Campaign -> Bool)] -> TestTree
@@ -161,7 +164,7 @@ runContract fp c =
     campaign (pure ()) v w ts (Just $ mkGenDict 0.15 (extractConstants cs ++ ads) [] g (returnTypes cs))
 
 getResult :: Text -> Campaign -> Maybe TestState
-getResult t = fmap snd <$> find ((t ==) . fst . fst) . view tests
+getResult t = fmap snd <$> find ((t ==) . either fst (("ASSERTION " <>) . fst) . fst) . view tests
 
 solnFor :: Text -> Campaign -> Maybe [Tx]
 solnFor t c = case getResult t c of