Read assert locations and determinate if they were executed or not (#1110)

* Read assert locations and determinate if they were executed or not

Co-authored-by: ggrieco-tob <[email protected]>

* accomodate older versions of solc

* cleanup

* add SlitherInfo to Env

---------

Co-authored-by: Sam Alws <[email protected]>

Author: gustavo-grieco

lib/Echidna.hs

@@ -70,7 +70,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
@@ -113,8 +113,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
@@ -128,4 +128,5 @@ mkEnv cfg buildOutput tests world = do
   let dapp = dappInfo "/" buildOutput
   pure $ Env { cfg, dapp, codehashMap, fetchContractCache, fetchSlotCache
              , chainId, eventQueue, coverageRef, corpusRef, testRefs, world
+             , slitherInfo
              }

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)
@@ -24,13 +25,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 (..))
 import Echidna.Types.Tx (TxResult(..))
+import Echidna.SourceAnalysis.Slither (AssertLocation(..), assertLocationList, SlitherInfo(..))
 
 saveCoverages
   :: Env
@@ -188,3 +190,30 @@ 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
+  -> IO ()
+checkAssertionsCoverage sc env = 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 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]) -> 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]

lib/Echidna/Types/Config.hs

@@ -12,6 +12,7 @@ import Data.Word (Word64)
 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)
@@ -73,6 +74,7 @@ data Env = Env
   , coverageRef :: IORef CoverageMap
   , 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
+
   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)