Read assert locations and determinate if they were executed or not

Co-authored-by: ggrieco-tob <gustavo.grieco@trailofbits.com>

lib/Echidna.hs

@@ -51,7 +51,7 @@ prepareContract
   -> BuildOutput
   -> Maybe ContractName
   -> Seed
-  -> IO (VM Concrete RealWorld, Env, GenDict)
+  -> IO (VM Concrete RealWorld, Env, GenDict, AssertMappingByContract)
 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 (AssertMappingByContract, AssertLocation(..))
 
 saveCoverages
   :: Env
@@ -188,3 +190,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/Solidity.hs

@@ -41,7 +41,7 @@ import Echidna.Etheno (loadEthenoBatch)
 import Echidna.Events (extractEvents)
 import Echidna.Exec (execTx, initialVM)
 import Echidna.SourceAnalysis.Slither
-import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode)
+import Echidna.Test (createTests, isPropertyMode, isDapptestMode)
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
   (ContractName, SolSignature, SignatureMap, FunctionName)
@@ -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 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

@@ -40,11 +40,32 @@ 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)
+
+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.: "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 [FunctionName]
+  , asserts :: AssertMappingByContract
   , 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)