prototype of the code to detect when assertions are not reached

lib/Echidna.hs

@@ -45,7 +45,7 @@ prepareContract
   -> NonEmpty FilePath
   -> Maybe ContractName
   -> Seed
-  -> IO (VM, World, GenDict)
+  -> IO (VM, World, GenDict, AssertMappingByContract)
 prepareContract env contracts solFiles specifiedContract seed = do
   let solConf = env.cfg.solConf
 
@@ -85,7 +85,7 @@ prepareContract env contracts solFiles specifiedContract seed = do
                      (returnTypes contracts)
 
   writeIORef env.testsRef echidnaTests
-  pure (vm, world, dict)
+  pure (vm, world, dict, slitherInfo.asserts)
 
 loadInitialCorpus :: Env -> World -> IO [[Tx]]
 loadInitialCorpus env world = 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.Aeson (ToJSON(..), FromJSON(..), withText)
 import Data.ByteString qualified as BS
 import Data.Foldable
@@ -30,6 +31,7 @@ import EVM.Solidity (SourceCache(..), SrcMap, SolcContract(..))
 import Echidna.Types.Coverage (OpIx, unpackTxResults, CoverageMap)
 import Echidna.Types.Tx (TxResult(..))
 import Echidna.Types.Signature (getBytecodeMetadata)
+import Echidna.Processor (AssertMappingByContract, AssertLocation(..))
 
 saveCoverages
   :: [CoverageFileType]
@@ -199,3 +201,26 @@ buildRuntimeLinesMap sc contracts =
   where
   srcMaps = concatMap
     (\c -> toList $ c.runtimeSrcmap <> c.creationSrcmap) contracts
+
+checkAssertionsCoverage
+  :: SourceCache
+  -> [SolcContract]
+  -> CoverageMap
+  -> AssertMappingByContract 
+  -> IO ()
+checkAssertionsCoverage sc cs covMap assertMap = do
+  covLines <- srcMapCov sc covMap cs
+  let asserts = concat $ concatMap Map.elems $ Map.elems assertMap
+  mapM_ (checkAssertionReached covLines) asserts
+
+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/Processor.hs

@@ -71,21 +71,23 @@ data AssertLocation = AssertLocation
   , endingColumn :: Int
   } deriving (Show)
 
+type AssertMappingByContract = Map ContractName (Map FunctionName [AssertLocation])
+
 instance FromJSON AssertLocation where
   parseJSON = withObject "" $ \o -> do
     start <- o.: "start"
     filenameRelative <- o.: "filename_relative"
     filenameAbsolute <- o.: "filename_absolute"
     assertLines <- o.: "lines"
-    startColumn <- o.: "start_column"
+    startColumn <- o.: "starting_column"
     endingColumn <- o.: "ending_column" 
     pure AssertLocation {..}
 
 -- we loose info on what constants are in which functions
 data SlitherInfo = SlitherInfo
   { payableFunctions :: Map ContractName [FunctionName]
   , constantFunctions :: Map ContractName [FunctionName]
-  , asserts :: Map ContractName (Map FunctionName [AssertLocation])
+  , asserts :: AssertMappingByContract
   , constantValues  :: Map ContractName (Map FunctionName [AbiValue])
   , generationGraph :: Map ContractName (Map FunctionName [FunctionName])
   , solcVersions :: [Version]

src/Main.hs

@@ -114,7 +114,7 @@ main = withUtf8 $ withCP65001 $ do
 
   -- take the seed from config, otherwise generate a new one
   seed <- maybe (getRandomR (0, maxBound)) pure cfg.campaignConf.seed
-  (vm, world, dict) <-
+  (vm, world, dict, asserts) <-
     prepareContract env contracts cliFilePath cliSelectedContract seed
 
   initialCorpus <- loadInitialCorpus env world
@@ -125,6 +125,8 @@ main = withUtf8 $ withCP65001 $ do
   slotsCache <- readIORef cacheSlotsRef
 
   tests <- readIORef testsRef
+  coverage <- readIORef coverageRef
+  checkAssertionsCoverage buildOutput.sources contracts coverage asserts
 
   -- save corpus
   case cfg.campaignConf.corpusDir of
@@ -156,8 +158,6 @@ main = withUtf8 $ withCP65001 $ do
         -- as it orders the runs chronologically.
         runId <- fromIntegral . systemSeconds <$> getSystemTime
 
-        coverage <- readIORef coverageRef
-
         -- coverage reports for external contracts, we only support
         -- Ethereum Mainnet for now
         when (chainId == Just 1) $ do