Read assert locations and determinate if they were executed or not

lib/Echidna.hs

@@ -51,7 +51,7 @@ prepareContract
   -> BuildOutput
   -> Maybe ContractName
   -> Seed
-  -> IO (VM Concrete RealWorld, Env, GenDict)
+  -> IO (VM Concrete RealWorld, Env, GenDict, AssertListingByContract)
 prepareContract cfg solFiles buildOutput selectedContract seed = do
   let solConf = cfg.solConf
       (Contracts contractMap) = buildOutput.contracts
@@ -90,7 +90,7 @@ prepareContract cfg solFiles buildOutput selectedContract seed = do
                      seed
                      (returnTypes contracts)
 
-  pure (vm, env, dict)
+  pure (vm, env, dict, slitherInfo.asserts)
 
 loadInitialCorpus :: Env -> IO [(FilePath, [Tx])]
 loadInitialCorpus env = do

lib/Echidna/Output/Source.hs

@@ -4,6 +4,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)
@@ -31,6 +32,7 @@ import Echidna.Types.Campaign (CampaignConf(..))
 import Echidna.Types.Config (Env(..), EConfig(..))
 import Echidna.Types.Coverage (OpIx, unpackTxResults, CoverageMap, CoverageFileType (..))
 import Echidna.Types.Tx (TxResult(..))
+import Echidna.SourceAnalysis.Slither (AssertListingByContract, AssertLocation(..), assertLocationList)
 
 saveCoverages
   :: Env
@@ -188,3 +190,29 @@ 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
+  -> [SolcContract]
+  -> CoverageMap
+  -> AssertListingByContract
+  -> IO ()
+checkAssertionsCoverage sc cs covMap assertMap = do
+  covLines <- srcMapCov sc covMap cs
+  let asserts = concatMap assertLocationList $ Map.elems assertMap
+  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]) -> AssertLocation -> IO ()
+checkAssertionReached covLines assert =
+  maybe
+    warnAssertNotReached checkCoverage
+    (Map.lookup assert.filenameAbsolute 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/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]

src/Main.hs

@@ -62,14 +62,18 @@ main = withUtf8 $ withCP65001 $ do
 
   -- take the seed from config, otherwise generate a new one
   seed <- maybe (getRandomR (0, maxBound)) pure cfg.campaignConf.seed
-  (vm, env, dict) <- prepareContract cfg cliFilePath buildOutput cliSelectedContract seed
+  (vm, env, dict, asserts) <- prepareContract cfg cliFilePath buildOutput cliSelectedContract seed
 
   initialCorpus <- loadInitialCorpus env
   -- start ui and run tests
   _campaign <- runReaderT (ui vm dict initialCorpus cliSelectedContract) env
 
   tests <- traverse readIORef env.testRefs
 
+  let contracts = Map.elems env.dapp.solcByName
+  coverage <- readIORef env.coverageRef
+  checkAssertionsCoverage buildOutput.sources contracts coverage asserts
+
   Onchain.saveRpcCache env
 
   -- save corpus
@@ -108,7 +112,6 @@ main = withUtf8 $ withCP65001 $ do
         Onchain.saveCoverageReport env runId
 
         -- save source coverage reports
-        let contracts = Map.elems env.dapp.solcByName
         saveCoverages env runId dir buildOutput.sources contracts
 
   if isSuccessful tests then exitSuccess else exitWith (ExitFailure 1)

src/test/Common.hs

@@ -94,7 +94,7 @@ runContract f selectedContract cfg workerType = do
   seed <- maybe (getRandomR (0, maxBound)) pure cfg.campaignConf.seed
   buildOutput <- compileContracts cfg.solConf (f :| [])
 
-  (vm, env, dict) <- prepareContract cfg (f :| []) buildOutput selectedContract seed
+  (vm, env, dict, _) <- prepareContract cfg (f :| []) buildOutput selectedContract seed
 
   (_stopReason, finalState) <- flip runReaderT env $
     runWorker workerType (pure ()) vm dict 0 [] cfg.campaignConf.testLimit selectedContract