Merge remote-tracking branch 'origin' into fixed-sym-exec

Author: gustavo-grieco

lib/Echidna/Campaign.hs

@@ -36,6 +36,7 @@ import EVM.Types hiding (Env, Frame(state), Gas)
 import EVM.Solidity (SolcContract(..), Method(..))
 
 import Echidna.ABI
+import Echidna.Events (extractEventValues)
 import Echidna.Exec
 import Echidna.Mutator.Corpus
 import Echidna.Shrink (shrinkTest)
@@ -490,11 +491,13 @@ callseq vm txSeq = do
       diffs = Map.fromList [(AbiAddressType, Set.fromList $ AbiAddress . forceAddr <$> newAddrs)]
       -- Now we try to parse the return values as solidity constants, and add them to 'GenDict'
       resultMap = returnValues results workerState.genDict.rTypes
+      -- compute the new events to be stored
+      eventDiffs = extractEventValues env.dapp vm vm'
       -- union the return results with the new addresses
-      additions = Map.unionWith Set.union diffs resultMap
+      additions = Map.unionsWith Set.union [resultMap, eventDiffs, diffs]
       -- append to the constants dictionary
       updatedDict = workerState.genDict
-        { constants = Map.unionWith Set.union additions workerState.genDict.constants
+        { constants = Map.unionWith Set.union workerState.genDict.constants additions
         , dictValues = Set.union (mkDictValues $ Set.unions $ Map.elems additions)
                                  workerState.genDict.dictValues
         }

lib/Echidna/Events.hs

@@ -3,19 +3,23 @@
 
 module Echidna.Events where
 
+import Data.Binary.Get
 import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.ByteString.Lazy (fromStrict)
+import Data.List (foldl')
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (fromJust, catMaybes, maybeToList)
+import Data.Set (Set)
+import Data.Set qualified as Set
 import Data.Text (pack, Text)
 import Data.Tree (flatten)
 import Data.Tree.Zipper (fromForest, TreePos, Empty)
 import Data.Vector (fromList)
 
 import EVM (traceForest)
-import EVM.ABI (Event(..), Indexed(..), decodeAbiValue, AbiType(..), AbiValue(..))
+import EVM.ABI (Event(..), Indexed(..), decodeAbiValue, getAbi, AbiType(..), AbiValue(..))
 import EVM.Dapp (DappContext(..), DappInfo(..))
 import EVM.Expr (maybeLitWordSimp)
 import EVM.Format (showValues, showError, contractNamePart)
@@ -72,6 +76,35 @@ extractEvents decodeErrors dappInfo vm =
         Just $ humanPanic $ decodePanic d
       _ -> Nothing
 
+-- | Extract all non‑indexed event values emitted between two VM states.
+extractEventValues :: DappInfo -> VM Concrete s -> VM Concrete s -> Map AbiType (Set AbiValue)
+extractEventValues dappInfo vm vm' =
+  let
+    oldLogs = vm.logs
+    newLogs = vm'.logs
+
+    -- only the newly emitted entries
+    delta   = filter (`notElem` oldLogs) newLogs
+
+    -- decode each Expr Log
+    goLog = \case
+      LogEntry _addr (ConcreteBuf bs) (sigHash : _) ->
+        case Map.lookup (forceWord sigHash) dappInfo.eventMap of
+          Just (Event _ _ params) ->
+            [ (ty, val)
+            | (_, ty, NotIndexed) <- params
+            , Right (_, _, val) <- [ runGetOrFail (getAbi ty) (fromStrict bs) ]
+            ]
+          Nothing -> []
+      _ -> []
+
+    pairs = concatMap goLog delta
+  in
+    foldl'
+      (\m (ty,v) -> Map.insertWith Set.union ty (Set.singleton v) m)
+      Map.empty
+      pairs
+
 maybeContractNameFromCodeHash :: DappInfo -> W256 -> Maybe Text
 maybeContractNameFromCodeHash info codeHash = contractToName <$> maybeContract
   where maybeContract = snd <$> Map.lookup codeHash info.solcByHash

lib/Echidna/Output/Source.hs

@@ -85,10 +85,10 @@ ppCoveredCode fileType sc cs s | null s = "Coverage map is empty"
     topHeader = case fileType of
       Lcov -> "TN:\n"
       Html -> "<style> code { white-space: pre-wrap; display: block; background-color: #eee; }" <>
-              ".executed { background-color: #afa; }" <>
-              ".reverted { background-color: #ffa; }" <>
-              ".unexecuted { background-color: #faa; }" <>
-              ".neutral { background-color: #eee; }" <>
+              ".e { background-color: #afa; }" <> -- executed
+              ".r { background-color: #ffa; }" <> -- reverted
+              ".u { background-color: #faa; }" <> -- unexecuted
+              ".n { background-color: #eee; }" <> -- neutral
               "</style>"
       Txt  -> ""
     -- ^ Text to add to top of the file
@@ -123,7 +123,7 @@ markLines fileType codeLines runtimeLines resultMap =
                      "</span>"
           _ -> line
           where
-          cssClass = if n `elem` runtimeLines then getCSSClass markers else "neutral"
+          cssClass = if n `elem` runtimeLines then getCSSClass markers else "n" -- fallback to 'neutral' class.
         result = case fileType of
           Lcov -> pack $ printf "DA:%d,%d" n (length results)
           _ -> pack $ printf " %*d | %-4s| %s" lineNrSpan n markers (wrapLine codeLine)
@@ -134,9 +134,9 @@ markLines fileType codeLines runtimeLines resultMap =
 getCSSClass :: String -> Text
 getCSSClass markers =
   case markers of
-   []                      -> "unexecuted"
-   _  | '*' `elem` markers -> "executed"
-   _                       -> "reverted"
+   []                      -> "u" -- unexecuted
+   _  | '*' `elem` markers -> "e" -- executed
+   _                       -> "r" -- reverted
 
 -- | Select the proper marker, according to the result of the transaction
 getMarker :: TxResult -> Char

lib/Echidna/Transaction.hs

@@ -177,7 +177,7 @@ setupTx tx@Tx{call} = fromEVM $ do
                  , callvalue = Lit tx.value
                  }
     , block = advanceBlock vm.block tx.delay
-    , tx = vm.tx { gasprice = tx.gasprice, origin = LitAddr tx.src }
+    , tx = vm.tx { gasprice = tx.gasprice, origin = LitAddr tx.src, subState = subState vm }
     }
   when isCreate $ do
     #env % #contracts % at (LitAddr tx.dst) .=
@@ -207,6 +207,12 @@ setupTx tx@Tx{call} = fromEVM $ do
       SolCreate bc -> bc
       SolCall cd -> encode cd
       SolCalldata cd -> cd
+    subState vm = let
+        initialAccessedAddrs = Set.fromList $
+            [LitAddr tx.src, LitAddr tx.dst, vm.block.coinbase]
+          ++ fmap LitAddr [1..10] -- precompile addresses
+        touched = if isCreate then [LitAddr tx.src] else [LitAddr tx.src, LitAddr tx.dst]
+      in SubState mempty touched initialAccessedAddrs mempty mempty mempty
 
 advanceBlock :: Block -> (W256, W256) -> Block
 advanceBlock blk (t,b) =

src/test/Tests/Values.hs

@@ -46,5 +46,6 @@ valuesTests = testGroup "Value extraction tests"
     , testContract' "values/contract.sol" (Just "Test") Nothing (Just "values/contract.yaml") False FuzzWorker
       [ ("verify_first passed",                    solved      "verify_first")
       , ("verify_later passed",                    solved      "verify_later") ]
-
+    , testContract' "values/events.sol" Nothing Nothing (Just "values/events.yaml") False FuzzWorker
+      [ ("check passed",                           solved      "check") ]
   ]

tests/solidity/values/events.sol

@@ -0,0 +1,15 @@
+contract EventAssert {
+    bytes32 private hash;
+    event Secret(bytes32);
+    function reset(uint seed) public {
+        require(hash == 0);
+	bytes32 secret = keccak256(abi.encodePacked(seed));
+	emit Secret(secret);
+        hash = keccak256(abi.encodePacked(secret));
+    }
+    function check(bytes32 seed) public {
+        if (keccak256(abi.encodePacked(seed)) == hash) {
+            assert(false);
+        }
+    }
+}

tests/solidity/values/events.yaml

@@ -0,0 +1,2 @@
+testLimit: 5000
+testMode: assertion