Merge branch 'master' into dev-cov-exec-counts-notup-test

lib/Echidna.hs

@@ -71,7 +71,7 @@ prepareContract cfg solFiles buildOutput selectedContract seed = do
 
   let world = mkWorld cfg.solConf signatureMap selectedContract slitherInfo contracts
 
-  env <- mkEnv cfg buildOutput tests world
+  env <- mkEnv cfg buildOutput tests world (Just slitherInfo)
 
   -- deploy contracts
   vm <- loadSpecified env mainContract contracts
@@ -114,8 +114,8 @@ loadInitialCorpus env = do
 
   pure $ persistedCorpus ++ ethenoCorpus
 
-mkEnv :: EConfig -> BuildOutput -> [EchidnaTest] -> World -> IO Env
-mkEnv cfg buildOutput tests world = do
+mkEnv :: EConfig -> BuildOutput -> [EchidnaTest] -> World -> Maybe SlitherInfo -> IO Env
+mkEnv cfg buildOutput tests world slitherInfo = do
   codehashMap <- newIORef mempty
   chainId <- maybe (pure Nothing) EVM.Fetch.fetchChainIdFrom cfg.rpcUrl
   eventQueue <- newChan
@@ -130,4 +130,5 @@ mkEnv cfg buildOutput tests world = do
   let dapp = dappInfo "/" buildOutput
   pure $ Env { cfg, dapp, codehashMap, fetchContractCache, fetchSlotCache
              , chainId, eventQueue, coverageRef, statsRef, corpusRef, testRefs, world
+             , slitherInfo
              }

lib/Echidna/ABI.hs

@@ -153,14 +153,20 @@ mkDictValues =
         fromValue (AbiInt  _ n) = Just (fromIntegral n)
         fromValue _             = Nothing
 
--- Generation (synthesis)
-
+-- Generate a random integer using a pow scale:
 getRandomPow :: (MonadRandom m) => Int -> m Integer
 getRandomPow n = if n <= 0 then return 0 else
   do
+   -- generate uniformly a number from 20 to n
    mexp <- getRandomR (20, n)
+   -- generate uniformly a number from the range 2 ^ (mexp / 2) to 2 ^ mexp  
    getRandomR (2 ^ (mexp `div` 2), 2 ^ mexp)
 
+-- Generate a random unsigned integer with the following distribution:
+-- * 9% (2/21) uniformly from 0 to 1024
+-- * 76% (16/21) uniformly from 0 to 2 ^ n - 5
+-- * 9% (2/21) uniformly from 2 ^ n - 5 to 2 ^ n - 1.
+-- * 4% (1/21) using the getRandomPow function  
 getRandomUint :: MonadRandom m => Int -> m Integer
 getRandomUint n =
   join $ Random.weighted
@@ -170,6 +176,9 @@ getRandomUint n =
     , (getRandomPow (n - 5), 1)
     ]
 
+-- | Generate a random signed integer with the following distribution:
+-- * 10% uniformly from the range -1023 to 1023.
+-- * 90% uniformly from the range -1 * 2 ^ n to 2 ^ (n - 1). 
 getRandomInt :: MonadRandom m => Int -> m Integer
 getRandomInt n =
   getRandomR =<< Random.weighted
@@ -310,8 +319,8 @@ mutateAbiValue = \case
                 \case 0 -> fixAbiInt n <$> mutateNum x
                       _ -> pure $ AbiInt n x
 
-  AbiAddress x -> pure $ AbiAddress x
-  AbiBool _ -> genAbiValue AbiBoolType
+  AbiAddress x -> pure $ AbiAddress x -- Address are not mutated at all
+  AbiBool _ -> genAbiValue AbiBoolType -- Booleans are regenerated
   AbiBytes n b -> do fs <- replicateM n getRandom
                      xs <- mutateLL (Just n) (BS.pack fs) b
                      pure $ AbiBytes n xs
@@ -327,6 +336,7 @@ mutateAbiValue = \case
   AbiFunction v -> pure $ AbiFunction v
 
 -- | Given a 'SolCall', generate a random \"similar\" call with the same 'SolSignature'.
+-- Note that this funcion will mutate a *single* argument (if any)
 mutateAbiCall :: MonadRandom m => SolCall -> m SolCall
 mutateAbiCall = traverse f
   where f [] = pure []
@@ -354,13 +364,15 @@ genWithDict genDict m g t = do
                    Just cs -> Just <$> rElem' cs
   fromMaybe <$> g t <*> maybeValM
 
+-- | A small number of dummy addresses
 pregenAdds :: [Addr]
 pregenAdds = [i*0xffffffff | i <- [1 .. 3]]
 
 pregenAbiAdds :: [AbiValue]
 pregenAbiAdds = map (AbiAddress . fromIntegral) pregenAdds
 
 -- | Synthesize a random 'AbiValue' given its 'AbiType'. Requires a dictionary.
+-- Only produce lists with number of elements in the range [1, 32]
 genAbiValueM :: MonadRandom m => GenDict -> AbiType -> m AbiValue
 genAbiValueM genDict = genWithDict genDict genDict.constants $ \case
   AbiUIntType n         -> fixAbiUInt n . fromInteger <$> getRandomUint n

lib/Echidna/Output/Source.hs

@@ -5,6 +5,7 @@ module Echidna.Output.Source where
 
 import Prelude hiding (writeFile)
 
+import Control.Monad (unless)
 import Data.ByteString qualified as BS
 import Data.Foldable
 import Data.IORef (readIORef, IORef)
@@ -27,13 +28,14 @@ import System.Directory (createDirectoryIfMissing)
 import System.FilePath ((</>))
 import Text.Printf (printf)
 
-import EVM.Dapp (srcMapCodePos)
+import EVM.Dapp (srcMapCodePos, DappInfo(..))
 import EVM.Solidity (SourceCache(..), SrcMap, SolcContract(..))
 
 import Echidna.Types.Campaign (CampaignConf(..))
 import Echidna.Types.Config (Env(..), EConfig(..))
 import Echidna.Types.Coverage (OpIx, unpackTxResults, CoverageMap, CoverageFileType (..), StatsMap, StatsMapV, StatsInfo)
 import Echidna.Types.Tx (TxResult(..))
+import Echidna.SourceAnalysis.Slither (AssertLocation(..), assertLocationList, SlitherInfo(..))
 import EVM.Types (W256)
 
 zipSumStats :: IO [StatsInfo] -> IO [StatsInfo] -> IO [StatsInfo]
@@ -221,3 +223,31 @@ buildRuntimeLinesMap sc contracts =
   where
   srcMaps = concatMap
     (\c -> toList $ c.runtimeSrcmap <> c.creationSrcmap) contracts
+
+-- | Check that all assertions were hit, and log a warning if they weren't
+checkAssertionsCoverage
+  :: SourceCache
+  -> Env
+  -> StatsMapV
+  -> IO ()
+checkAssertionsCoverage sc env sm = do
+  let
+    cs = Map.elems env.dapp.solcByName
+    asserts = maybe [] (concatMap assertLocationList . Map.elems . (.asserts)) env.slitherInfo
+  covMap <- readIORef env.coverageRef
+  covLines <- srcMapCov sc covMap sm cs
+  mapM_ (checkAssertionReached covLines) asserts
+
+-- | Helper function for `checkAssertionsCoverage` which checks a single assertion
+-- and logs a warning if it wasn't hit
+checkAssertionReached :: Map String (Map Int ([TxResult], StatsInfo)) -> AssertLocation -> IO ()
+checkAssertionReached covLines assert =
+  maybe
+    warnAssertNotReached checkCoverage
+    (Map.lookup assert.filenameAbsolute $ fmap (fmap fst) covLines)
+  where
+   checkCoverage coverage = let lineNumbers = Map.keys coverage in
+     unless ((head assert.assertLines) `elem` lineNumbers) warnAssertNotReached
+   warnAssertNotReached =
+    putStrLn $ "WARNING: assertion at file: " ++ assert.filenameRelative
+       ++ " starting at line: " ++ show (head assert.assertLines) ++ " was never reached"

lib/Echidna/Shrink.hs

@@ -21,6 +21,7 @@ import Echidna.Types.Config
 import Echidna.Types.Campaign (CampaignConf(..))
 import Echidna.Test (getResultFromVM, checkETest)
 
+ -- | Top level function to shrink the complexity of the sequence of transactions once
 shrinkTest
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m)
   => VM Concrete RealWorld
@@ -29,22 +30,28 @@ shrinkTest
 shrinkTest vm test = do
   env <- ask
   case test.state of
+    -- If we run out of tries to shrink, return the sequence as we have them
     Large i | i >= env.cfg.campaignConf.shrinkLimit && not (isOptimizationTest test) ->
       pure $ Just test { state = Solved }
     Large i ->
+      -- Start removing the reverts, if any
       do  repro <- removeReverts vm test.reproducer
-          let rr = removeUselessNoCalls $ catNoCalls repro 
+          let rr = removeUselessNoCalls $ catNoCalls repro
+          -- Check if the sequence can be reduced, in practice this is almost never fails 
+          -- since the canShrinkTx function is hard to enforce for all transaction in the sequence 
           if length rr > 1 || any canShrinkTx rr then do
             maybeShrunk <- shrinkSeq vm (checkETest test) test.value rr
+            -- check if the shrinked sequence passes the test or not
             pure $ case maybeShrunk of
+              -- the test still fails, let's create another test with the reduced sequence
               Just (txs, val, vm') -> do
                 Just test { state = Large (i + 1)
                     , reproducer = txs
                     , vm = Just vm'
                     , result = getResultFromVM vm'
                     , value = val }
               Nothing ->
-                -- No success with shrinking this time, just bump trials
+                -- The test passed, so no success with shrinking this time, just bump number of tries to shrink
                 Just test { state = Large (i + 1), reproducer = rr}
           else
             pure $ Just test { state = if isOptimizationTest test
@@ -55,10 +62,15 @@ shrinkTest vm test = do
 replaceByNoCall :: Tx -> Tx
 replaceByNoCall tx = tx { call = NoCall }
 
+-- | Given a sequence of transactions, remove useless NoCalls. These 
+-- are when the NoCall have both zero increment in timestamp and block number.
 removeUselessNoCalls :: [Tx] -> [Tx]
 removeUselessNoCalls = mapMaybe f
   where f tx = if isUselessNoCall tx then Nothing else Just tx 
 
+-- | Given a VM and a sequence of transactions, execute each transaction except the last one.
+-- If a transaction reverts, replace it by a "NoCall" with the same parameters as the original call
+-- (e.g. same block increment timestamp and number)
 removeReverts :: (MonadIO m, MonadReader Env m, MonadThrow m) => VM Concrete RealWorld -> [Tx] -> m [Tx]
 removeReverts vm txs = do
   let (itxs, le) = (init txs, last txs)
@@ -83,10 +95,14 @@ shrinkSeq
   -> [Tx]
   -> m (Maybe ([Tx], TestValue, VM Concrete RealWorld))
 shrinkSeq vm f v txs = do
+  -- apply one of the two possible simplification strategies (shrunk or shorten) with equal probability
   txs' <- uniform =<< sequence [shorten, shrunk]
+  -- remove certain type of "no calls"
   let txs'' = removeUselessNoCalls txs' 
+  -- check if the sequence still triggers a failed transaction
   (value, vm') <- check txs'' vm
-  -- if the test passed it means we didn't shrink successfully
+  -- if the test passed it means we didn't shrink successfully (returns Nothing)
+  -- otherwise, return a reduced sequence of transaction
   pure $ case (value,v) of
     (BoolValue False, _)              -> Just (txs'', value, vm')
     (IntValue x, IntValue y) | x >= y -> Just (txs'', value, vm')
@@ -96,9 +112,15 @@ shrinkSeq vm f v txs = do
     check (x:xs') vm' = do
       (_, vm'') <- execTx vm' x
       check xs' vm''
+    -- | Simplify a sequence of transactions reducing the complexity of its arguments (using shrinkTx)
+    -- and then reducing its sender (using shrinkSender)
     shrunk = mapM (shrinkSender <=< shrinkTx) txs
+    -- | Simplifiy a sequence of transactions randomly dropping one transaction (with uniform selection)
     shorten = (\i -> take i txs ++ drop (i + 1) txs) <$> getRandomR (0, length txs)
 
+-- | Given a transaction, replace the sender of the transaction by another one
+-- which is simpler (e.g. it is closer to zero). Usually this means that
+-- simplified transactions will try to use 0x10000 as the same caller
 shrinkSender :: (MonadReader Env m, MonadRandom m) => Tx -> m Tx
 shrinkSender x = do
   senderSet <- asks (.cfg.solConf.sender)

lib/Echidna/Solidity.hs

@@ -342,7 +342,7 @@ mkWorld SolConf{sender, testMode} sigMap maybeContract slitherInfo contracts =
   let
     eventMap = Map.unions $ map (.eventMap) contracts
     payableSigs = filterResults maybeContract slitherInfo.payableFunctions
-    as = if isAssertionMode testMode then filterResults maybeContract slitherInfo.asserts else []
+    as = if isAssertionMode testMode then filterResults maybeContract (assertFunctionList <$> slitherInfo.asserts) else []
     cs = if isDapptestMode testMode then [] else filterResults maybeContract slitherInfo.constantFunctions \\ as
     (highSignatureMap, lowSignatureMap) = prepareHashMaps cs as $
       filterFallbacks slitherInfo.fallbackDefined slitherInfo.receiveDefined contracts sigMap

lib/Echidna/SourceAnalysis/Slither.hs

@@ -2,6 +2,7 @@
 
 module Echidna.SourceAnalysis.Slither where
 
+import Control.Applicative ((<|>))
 import Data.Aeson ((.:), (.:?), (.!=), eitherDecode, parseJSON, withEmbeddedJSON, withObject)
 import Data.Aeson.Types (FromJSON, Parser, Value(String))
 import Data.ByteString.Base16 qualified as BS16 (decode)
@@ -40,11 +41,53 @@ enhanceConstants si =
     enh (AbiString s) = makeArrayAbiValues s
     enh v = [v]
 
+data AssertLocation = AssertLocation 
+  { start :: Int
+  , filenameRelative :: String
+  , filenameAbsolute :: String
+  , assertLines :: [Int]
+  , startColumn :: Int
+  , endingColumn :: Int
+  } deriving (Show)
+
+-- | Assertion listing for a contract.
+-- There are two possibilities because different solc's give different formats.
+-- We either have a list of functions that have assertions, or a full listing of individual assertions.
+data ContractAssertListing
+  = AssertFunctionList [FunctionName]
+  | AssertLocationList (Map FunctionName [AssertLocation])
+  deriving (Show)
+
+type AssertListingByContract = Map ContractName ContractAssertListing
+
+-- | Get a list of functions that have assertions
+assertFunctionList :: ContractAssertListing -> [FunctionName]
+assertFunctionList (AssertFunctionList l) = l
+assertFunctionList (AssertLocationList m) = map fst $ filter (not . null . snd) $ Map.toList m
+
+-- | Get a list of assertions, or an empty list if we don't have enough info
+assertLocationList :: ContractAssertListing -> [AssertLocation]
+assertLocationList (AssertFunctionList _) = []
+assertLocationList (AssertLocationList m) = concat $ Map.elems m
+
+instance FromJSON AssertLocation where
+  parseJSON = withObject "" $ \o -> do
+    start <- o.: "start"
+    filenameRelative <- o.: "filename_relative"
+    filenameAbsolute <- o.: "filename_absolute"
+    assertLines <- o.: "lines"
+    startColumn <- o.: "starting_column"
+    endingColumn <- o.: "ending_column" 
+    pure AssertLocation {..}
+
+instance FromJSON ContractAssertListing where
+  parseJSON x = (AssertFunctionList <$> parseJSON x) <|> (AssertLocationList <$> parseJSON x)
+
 -- we loose info on what constants are in which functions
 data SlitherInfo = SlitherInfo
   { payableFunctions :: Map ContractName [FunctionName]
   , constantFunctions :: Map ContractName [FunctionName]
-  , asserts :: Map ContractName [FunctionName]
+  , asserts :: AssertListingByContract
   , constantValues  :: Map ContractName (Map FunctionName [AbiValue])
   , generationGraph :: Map ContractName (Map FunctionName [FunctionName])
   , solcVersions :: [Version]

lib/Echidna/Types/Config.hs

@@ -13,6 +13,7 @@ import Data.TLS.GHC
 import EVM.Dapp (DappInfo)
 import EVM.Types (Addr, Contract, W256)
 
+import Echidna.SourceAnalysis.Slither (SlitherInfo)
 import Echidna.SourceMapping (CodehashMap)
 import Echidna.Types.Campaign (CampaignConf, CampaignEvent)
 import Echidna.Types.Corpus (Corpus)
@@ -75,6 +76,7 @@ data Env = Env
   , statsRef :: TLS (IORef StatsMap)
   , corpusRef :: IORef Corpus
 
+  , slitherInfo :: Maybe SlitherInfo
   , codehashMap :: CodehashMap
   , fetchContractCache :: IORef (Map Addr (Maybe Contract))
   , fetchSlotCache :: IORef (Map Addr (Map W256 (Maybe W256)))

src/Main.hs

@@ -70,6 +70,8 @@ main = withUtf8 $ withCP65001 $ do
 
   tests <- traverse readIORef env.testRefs
 
+  checkAssertionsCoverage buildOutput.sources env mempty
+
   Onchain.saveRpcCache env
 
   -- save corpus

src/test/Common.hs

@@ -157,7 +157,7 @@ loadSolTests cfg buildOutput name = do
       world = World solConf.sender mempty Nothing [] eventMap
   mainContract <- selectMainContract solConf name contracts
   echidnaTests <- mkTests solConf mainContract
-  env <- mkEnv cfg buildOutput echidnaTests world
+  env <- mkEnv cfg buildOutput echidnaTests world Nothing
   vm <- loadSpecified env mainContract contracts
   pure (vm, env, echidnaTests)