Conversation
removed old solc versions, use 0.8.x only instead
WalkthroughThis update restructures symbolic execution and verification in the Echidna smart contract testing framework. It removes the legacy symbolic execution module, replacing it with a modular design featuring new symbolic exploration and verification modules. Configuration and test state handling are updated, including new YAML options and a "verified" test state. Worker-related types and logic are refactored into a dedicated module. Numerous supporting modules and tests are adjusted to reflect these changes. Changes
Sequence Diagram(s)sequenceDiagram
participant User
participant Worker
participant SymbolicEngine
participant SMT_Solver
User->>Worker: Start (config: symbolic verification)
Worker->>SymbolicEngine: verifyMethods()
loop For each contract method
SymbolicEngine->>SMT_Solver: Symbolic verification query
alt Counterexample found
SMT_Solver-->>SymbolicEngine: Counterexample (Tx)
SymbolicEngine->>Worker: SymExecError event
else No bug found
SMT_Solver-->>SymbolicEngine: No counterexample
SymbolicEngine->>Worker: SymExecLog event
end
end
Worker->>User: SymbolicVerificationDone
sequenceDiagram
participant User
participant Worker
participant SymbolicEngine
participant SMT_Solver
User->>Worker: Start (config: symbolic exploration)
Worker->>SymbolicEngine: exploreContract(target method)
SymbolicEngine->>SMT_Solver: Symbolic execution queries
alt New coverage found
SMT_Solver-->>SymbolicEngine: Counterexample(s)
SymbolicEngine->>Worker: NewCoverage event
else No new coverage
SMT_Solver-->>SymbolicEngine: No new states
SymbolicEngine->>Worker: SymExecLog event
end
Worker->>User: SymbolicExplorationDone
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Poem
Note ⚡️ Unit Test Generation is now available in beta!Learn more here, or try it out under "Finishing Touches" below. 📜 Recent review detailsConfiguration used: CodeRabbit UI 📒 Files selected for processing (4)
💤 Files with no reviewable changes (2)
✅ Files skipped from review due to trivial changes (1)
🧰 Additional context used🧠 Learnings (1)📓 Common learnings⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (7)
🔇 Additional comments (3)
✨ Finishing Touches🧪 Generate unit tests
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. 🪧 TipsChatThere are 3 ways to chat with CodeRabbit:
SupportNeed help? Create a ticket on our support page for assistance with any issues or questions. CodeRabbit Commands (Invoked using PR comments)
Other keywords and placeholders
CodeRabbit Configuration File (
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (6)
lib/Echidna/Transaction.hs (1)
158-163: LGTM: New comprehensive transaction regeneration function.The
regenTxfunction provides a useful complement tomutateTxby mutating all ABI call arguments instead of just one. This more aggressive mutation strategy aligns well with the enhanced symbolic execution framework mentioned in the PR objectives.Consider adding a comment to clarify the difference between
mutateTx(mutates single argument) andregenTx(mutates all arguments) for future maintainers.lib/Echidna/Campaign.hs (1)
157-175: Innovative dual-strategy symbolic execution approach.The implementation provides two complementary strategies:
- When
symExecTargetsis set: focuses on random prefixes only- Otherwise: explores both the last transaction and random prefixes
This approach effectively balances targeted and exploratory symbolic execution.
Minor clarification needed: The comment on line 163 states "Discard the last tx, which should be the one increasing coverage", but
ltxis actually used on line 175. Consider updating the comment to clarify that it's separated, not discarded.- -- Discard the last tx, which should be the one increasing coverage + -- Separate the last tx, which should be the one increasing coverage let (itxs, ltx) = (init txs, last txs)lib/Echidna/SymExec.hs (4)
59-63: Consider adding parentheses for clarity.The boolean logic is correct but would be more readable with explicit parentheses to clarify the precedence of operations.
suitableForSymExec :: Method -> Bool -suitableForSymExec m = not $ null m.inputs - && null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs) - && not (T.isInfixOf "_no_symexec" m.name) +suitableForSymExec m = not (null m.inputs) + && null (filter (\(_, t) -> abiKind t == Dynamic) m.inputs) + && not (T.isInfixOf "_no_symexec" m.name)
115-116: Address or remove the TODO comment.The TODO suggests switching to
AbstractBasebut notes it might affect concolic execution. Since concolic execution has been removed, this concern may no longer be valid.Would you like me to investigate the implications of switching to
AbstractBaseand create an issue to track this enhancement?
120-122: Remove commented debugging code.These commented print statements should be removed to keep the codebase clean.
- --liftIO $ mapM_ print $ checkResults results let txs = mapMaybe (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender) results - --liftIO $ print $ map (runReaderT mempty $ ppTx vm True) txs pure txs liftIO $ putMVar resultChan $ concat res - --liftIO $ print "done"Also applies to: 125-125
234-238: Consider documenting the zero-check behavior.The logic correctly handles unconstrained symbolic values (which default to 0) by setting the diff to 0. Consider adding a comment to clarify this behavior for future maintainers.
+ -- If symbolic values are unconstrained (0), no delay is applied newTimestamp = fromMaybe 0 $ Map.lookup (Var "symbolic_block_timestamp") cex.vars diffTimestamp = if newTimestamp == 0 then 0 else newTimestamp - forceLit oldTimestamp newNumber = fromMaybe 0 $ Map.lookup (Var "symbolic_block_number") cex.vars diffNumber = if newNumber == 0 then 0 else newNumber - forceLit oldNumber
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (22)
flake.nix(1 hunks)lib/Echidna/ABI.hs(2 hunks)lib/Echidna/Campaign.hs(5 hunks)lib/Echidna/Config.hs(1 hunks)lib/Echidna/Events.hs(2 hunks)lib/Echidna/Exec.hs(4 hunks)lib/Echidna/Mutator/Corpus.hs(1 hunks)lib/Echidna/Solidity.hs(2 hunks)lib/Echidna/SourceAnalysis/Slither.hs(1 hunks)lib/Echidna/SourceMapping.hs(2 hunks)lib/Echidna/SymExec.hs(3 hunks)lib/Echidna/Transaction.hs(2 hunks)lib/Echidna/Types/Cache.hs(1 hunks)lib/Echidna/Types/Campaign.hs(3 hunks)lib/Echidna/Types/World.hs(1 hunks)package.yaml(1 hunks)src/Main.hs(1 hunks)src/test/Common.hs(1 hunks)stack.yaml(1 hunks)tests/solidity/basic/default.yaml(1 hunks)tests/solidity/symbolic/sym-assert.yaml(0 hunks)tests/solidity/symbolic/sym.yaml(0 hunks)
💤 Files with no reviewable changes (2)
- tests/solidity/symbolic/sym.yaml
- tests/solidity/symbolic/sym-assert.yaml
⏰ Context from checks skipped due to timeout of 90000ms (6)
- GitHub Check: Build Echidna on ubuntu-latest
- GitHub Check: Build Echidna on windows-latest
- GitHub Check: Build macOS (aarch64) binary
- GitHub Check: Build Linux (x86_64) binary
- GitHub Check: Build macOS (x86_64) binary
- GitHub Check: Build Echidna on macos-13
🔇 Additional comments (29)
flake.nix (1)
55-56: Ensure Nix fetch source checksum is valid for updated revisionThe
sha256was updated for the newrev, but please verify that the checksum (sha256-RNT6ySisP1mdR0NJ1Yyu12A4duzsFCfya+l4CNXHlgQ=) matches the actual content of5f48aaa93e18cf8f42b46109c04a76234b746dc6. An incorrect hash will break the Nix build cache and fetch.
Also, consider aligning thisrevwith the one used instack.yamlfor coherent hevm versioning.lib/Echidna/SourceMapping.hs (2)
14-14: LGTM: Import updated for hevm API migration.The import correctly switches from
EVM.TypestoEVM.Exprfor the simplified literal extraction function.
84-84:Details
✅ Verification successful
LGTM: Function call updated for hevm API migration.
The replacement of
maybeLitBytewithmaybeLitByteSimpis consistent with the hevm upgrade. The usage pattern suggests the function signatures are compatible.Let me verify that all usages of the old function have been updated across the codebase:
🏁 Script executed:
#!/bin/bash # Description: Verify that all old literal extraction functions have been updated # Expected: No remaining usages of maybeLitByte, maybeLitWord found echo "Checking for remaining usages of old literal extraction functions..." rg -n "maybeLitByte\b" --type hs rg -n "maybeLitWord\b" --type hs echo "Checking for new simplified functions..." rg -n "maybeLitByteSimp\b" --type hs rg -n "maybeLitWordSimp\b" --type hsLength of output: 742
All old literal extraction functions successfully replaced
- No remaining uses of
maybeLitByteormaybeLitWordfound.- New calls to
maybeLitByteSimpexist in:
- lib/Echidna/SourceMapping.hs (import at line 14, usage at line 84)
- New calls to
maybeLitWordSimpexist in:
- lib/Echidna/Events.hs (import at line 20, usage at line 41)
LGTM—migration to the updated hevm API is complete and consistent.
lib/Echidna/Events.hs (2)
20-20: LGTM: Import added for hevm API migration.The import correctly adds
maybeLitWordSimpfromEVM.Exprfor the simplified literal extraction function.
41-41: LGTM: Function call updated for hevm API migration.The replacement of
maybeLitWordwithmaybeLitWordSimpcompletes the consistent API migration pattern across both files. The usage withfromJustsuggests the function signatures are compatible.package.yaml (1)
60-60: LGTM: Dependency change aligns with symbolic execution enhancements.The addition of
list-shuffledependency supports the corpus shuffling functionality mentioned in the PR objectives, which is part of the enhanced symbolic execution approach.lib/Echidna/Types/World.hs (1)
20-20:Details
✅ Verification successful
Verify all World construction sites include the new field.
The addition of
assertSigsfield is well-structured and aligns with the symbolic execution enhancements. Please ensure all World construction sites have been updated to include this new field.
🏁 Script executed:
#!/bin/bash # Description: Verify all World construction sites include the assertSigs field # Expected: All World constructors should include the new assertSigs field # Search for World constructor usage patterns ast-grep --pattern 'World { $$$ }' # Also search for World record construction patterns rg -A 10 -B 2 "World\s*\{" --type hsLength of output: 1329
🏁 Script executed:
#!/bin/bash # Verify mkWorld definition includes the new assertSigs field # Locate mkWorld implementation with surrounding context rg -n "mkWorld" -C5 --type hsLength of output: 2045
All
Worldconstructions includeassertSigsThe
Worldrecord inlib/Echidna/Solidity.hs(lines 355–361) and themkWorldfunction (lines 346–351) both initialize the newassertSigsfield. No missing initializations were found—no further changes are needed.src/Main.hs (1)
159-161: LGTM: Idiomatic function composition style.The stylistic change to use function composition with
NE.fromListis more idiomatic Haskell and doesn't affect the parsing logic.lib/Echidna/Config.hs (1)
107-107:Details
✅ Verification successful
Verify the default value and data type consistency.
The addition of
symExecMaxExploreconfiguration aligns with the symbolic execution enhancements and removal of concolic execution. Please ensure thedefaultSymExecMaxExploreconstant is properly defined and theCampaignConfdata type includes this field.
🏁 Script executed:
#!/bin/bash # Description: Verify defaultSymExecMaxExplore is defined and CampaignConf includes symExecMaxExplore # Expected: Both the default constant and the data type field should exist # Search for the default constant definition rg "defaultSymExecMaxExplore" --type hs # Search for CampaignConf data type definition to verify the field exists ast-grep --pattern 'data CampaignConf = CampaignConf { $$$ }' # Search for symExecMaxExplore field in data types rg "symExecMaxExplore\s*::" --type hsLength of output: 4599
Configuration integration validated
defaultSymExecMaxExploreis defined in lib/Echidna/Types/Campaign.hs as anInteger(value 10).CampaignConfin lib/Echidna/Types/Campaign.hs includessymExecMaxExplore :: Integer.lib/Echidna/Config.hscorrectly parses"symExecMaxExplore"with the default.All checks pass—no further changes needed.
lib/Echidna/Solidity.hs (2)
350-350: LGTM! Proper extraction of assertion signatures.The extraction of
assertSigsusingfilterResultsfollows the same pattern as other signature extractions in this function and correctly processes the assertion information from Slither.
359-359: LGTM! Consistent addition to World record.The
assertSigsfield is properly included in the World record construction, maintaining consistency with the other extracted signature fields.src/test/Common.hs (1)
157-157: LGTM! Correct update to World constructor.The addition of empty list arguments properly aligns the test code with the updated World data type that now includes the
assertSigsfield. Using empty lists as placeholders in test setup is appropriate.lib/Echidna/SourceAnalysis/Slither.hs (1)
118-118: LGTM! Improved idiomatic expression.The change from
(catMaybes . concat)toconcatMap catMaybesis functionally equivalent but more idiomatic and readable. This is a positive style improvement.lib/Echidna/Types/Cache.hs (1)
1-7: LGTM! Clean and well-designed cache types.This new module provides clear, purpose-built type aliases for caching in symbolic execution:
ContractCacheappropriately maps addresses to optional contractsSlotCacheuses a logical nested map structure for storage slot caching- The module is minimal with appropriate imports and clear naming
These types will likely improve symbolic execution performance through strategic caching.
lib/Echidna/Mutator/Corpus.hs (2)
4-4: LGTM: Import cleanup and abstraction improvement.The qualified import for
Data.Setand addition ofEchidna.Types.Corpusalign well with the type signature update below.Also applies to: 10-10
65-68: LGTM: Type signature abstraction improvement.The change from
Set (Int, [Tx])toCorpusprovides better abstraction while maintaining the same underlying functionality. The implementation correctly usesSet.toDescListwhich suggestsCorpusis still backed by a Set internally.tests/solidity/basic/default.yaml (2)
107-107: LGTM: Configuration comments updated consistently.The removal of
symExecConcolicconditions from these comments aligns with the PR objective to remove concolic execution support. The options now apply wheneversymExecis true, which simplifies the configuration model.Also applies to: 110-110
115-117: LGTM: New symbolic exploration limit configuration.The addition of
symExecMaxExploreprovides useful control over the number of states to explore during symbolic execution, which aligns with the PR's focus on improving symbolic execution efficiency.lib/Echidna/Transaction.hs (1)
208-208: LGTM: Consistent literal wrapping for block number.Wrapping the block number calculation with
Litensures consistency with how block numbers are handled elsewhere in the codebase and maintains proper type safety.lib/Echidna/ABI.hs (2)
194-194: LGTM: Code simplification without logic change.The removal of redundant parentheses improves readability while maintaining the same mathematical calculation for the signed integer range.
355-358: LGTM: Comprehensive ABI call mutation function.The
mutateAllAbiCallfunction provides a useful complement tomutateAbiCallby mutating every argument instead of just one random argument. The implementation correctly usestraverseandmapMto apply mutations across all arguments, supporting the more thorough mutation strategy needed for enhanced symbolic execution.lib/Echidna/Types/Campaign.hs (2)
50-67: LGTM! Clear documentation and sensible configuration changes.The comment updates accurately reflect the removal of concolic execution support, and the new
symExecMaxExplorefield provides useful control over symbolic execution exploration limits.
207-211: Reasonable default values for symbolic execution parameters.The default values are well-chosen:
defaultSymExecMaxExplore = 10provides a reasonable exploration limit- Reducing
defaultSymExecMaxItersfrom 10 to 5 helps balance exploration depth with performancelib/Echidna/Exec.hs (2)
30-31: Correct integration with updated EVM execution interface.The explicit passing of
defaultConfigtoexecandexec1functions ensures consistent execution environment across the refactored symbolic execution framework.Also applies to: 244-244, 293-293
343-343: Consistent literal representation for block numbers.Wrapping the block number with
Litmaintains consistency with similar changes across the codebase.lib/Echidna/Campaign.hs (2)
29-31: Good implementation of randomized corpus exploration.The asynchronous corpus shuffling before symbolic execution helps diversify the exploration and avoid getting stuck in local patterns. The empty corpus check prevents unnecessary work.
Also applies to: 117-130
180-180: Simplified createSymTx interface aligns with new architecture.The removal of explicit configuration parameters from
createSymTxsuggests it now uses environment-based configuration, which is consistent with the broader refactoring.lib/Echidna/SymExec.hs (2)
9-11: Good use of the MonadReader pattern.The refactoring to use
MonadReaderfor accessing the environment is a clean design that improves testability and reduces the need to pass configuration explicitly through function calls.
252-268: Well-implemented cache layer.The
cachedOraclefunction provides an efficient caching mechanism that checks local caches before making RPC calls, which should improve performance during symbolic execution.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (4)
lib/Echidna/SymExec.hs (4)
69-69: Remove or uncomment the assertSigs check.The commented out code
{- methodSigelemassertSigs &&-}creates ambiguity about the intended behavior. Either remove it entirely or uncomment it if the check is needed.
102-102: Limited exploration scope - only one method is explored.The code currently limits symbolic exploration to only the first method after shuffling with
take 1 shuffleMethods. This seems overly restrictive given that the configuration includesmaxExploreparameter. Consider using the configuration value or documenting why only one method is explored.- res <- forM (take 1 shuffleMethods) $ \method -> do + res <- forM (take (fromIntegral $ fromMaybe 1 maxExplore) shuffleMethods) $ \method -> do
169-169: Fix typos in function names.The function names have typos:
addBlockConstrainsshould beaddBlockConstraintsandsenderContraintsshould besenderConstraints.-addBlockConstraints :: W256 -> W256 -> Block -> [Prop] -> [Prop] -addBlockConstraints maxTimestampDiff maxNumberDiff block cs = +addBlockConstraints :: W256 -> W256 -> Block -> [Prop] -> [Prop] +addBlockConstraints maxTimestampDiff maxNumberDiff block cs =Also update the call site:
- & #constraints %~ (++ constraints ++ (senderConstraints conf.solConf.sender)) + & #constraints %~ (++ constraints ++ (senderConstraints conf.solConf.sender))
175-175: Fix typos in function names.The function names have typos:
addBlockConstrainsshould beaddBlockConstraintsandsenderContraintsshould besenderConstraints.-senderConstraints :: Set Addr -> [Prop] -senderConstraints as = [foldr (\a b -> POr b (PEq (SymAddr "caller") (LitAddr a))) (PBool False) $ Set.toList as] +senderConstraints :: Set Addr -> [Prop] +senderConstraints as = [foldr (\a b -> POr b (PEq (SymAddr "caller") (LitAddr a))) (PBool False) $ Set.toList as]
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (3)
flake.nix(1 hunks)lib/Echidna/Campaign.hs(6 hunks)lib/Echidna/SymExec.hs(3 hunks)
✅ Files skipped from review due to trivial changes (1)
- flake.nix
🚧 Files skipped from review as they are similar to previous changes (1)
- lib/Echidna/Campaign.hs
⏰ Context from checks skipped due to timeout of 90000ms (6)
- GitHub Check: Build macOS (aarch64) binary
- GitHub Check: Build Linux (x86_64) binary
- GitHub Check: Build macOS (x86_64) binary
- GitHub Check: Build Echidna on ubuntu-latest
- GitHub Check: Build Echidna on windows-latest
- GitHub Check: Build Echidna on macos-13
🔇 Additional comments (5)
lib/Echidna/SymExec.hs (5)
9-11: Good monadic abstraction improvement.The transition from concrete IO types to monadic constraints
(MonadIO m, MonadThrow m, MonadReader Env m)provides better composability and testability. This aligns well with the overall refactoring objectives.
59-62: Well-designed filtering predicate.The
suitableForSymExecfunction provides clear criteria for method eligibility:
- Methods must have inputs
- No dynamic ABI types (which are harder to handle symbolically)
- Explicit opt-out via naming convention
This filtering approach is practical and maintainable.
255-270: Well-implemented caching strategy.The
cachedOraclefunction provides an efficient caching layer that falls back to the original oracle when cache misses occur. The pattern matching on different query types is clean and the cache lookup logic is correct.
171-173:Details
❓ Verification inconclusive
Verify constraint bounds for symbolic block values.
The constraints for symbolic block timestamp and number use strict inequalities (
PGT,PLT) which could potentially exclude edge cases. Consider if these should be inclusive bounds (PGEq,PLEq) depending on the intended semantics.
🏁 Script executed:
#!/bin/bash # Search for similar constraint patterns in the codebase to verify consistency rg -A 3 -B 3 "PGT.*block|PLT.*block" --type hsLength of output: 688
Verify inclusive/exclusive bounds for symbolic block values
The current
addBlockConstraintsinlib/Echidna/SymExec.hs(around lines 171–173) uses strict inequalities, which exclude the exact boundary values:PGT (Var "symbolic_block_timestamp") (block.timestamp) , PLT (Sub (Var "symbolic_block_timestamp") (block.timestamp)) $ Lit maxTimestampDiff , PGT (Var "symbolic_block_number") (block.number) , PLT (Sub (Var "symbolic_block_number") (block.number)) $ Lit maxNumberDiff• If you intend to allow equality at the boundaries (i.e. permit
symbolic_block_timestamp == block.timestampor a difference equal tomaxTimestampDiff), consider switching toPGEqandPLEq.
• Otherwise, keep the strict checks as-is and confirm this matches your specification.
96-96:Details
❓ Verification inconclusive
Verify Bitwuzla solver selection.
The code switches from Z3 to Bitwuzla as mentioned in the PR objectives. Ensure this change is intentional and that Bitwuzla provides the expected performance improvements for your use case.
🌐 Web query:
What are the performance differences between Bitwuzla and Z3 solvers for symbolic execution?💡 Result:
Bitwuzla and Z3 are both prominent SMT (Satisfiability Modulo Theories) solvers utilized in symbolic execution, each with distinct performance characteristics.
Performance in SMT Competitions:
In the SMT-COMP 2024, Bitwuzla demonstrated superior performance in the QF_Bitvec division, leading in both sequential and parallel tracks. It solved 10,489 benchmarks, outperforming other solvers in the same category. (smt-comp.github.io)
Benchmark Comparisons:
A comparative study involving Bitwuzla and Z3 on various benchmarks revealed that Bitwuzla often outperforms Z3, especially in scenarios involving fixed-size bit-vectors and arrays. For instance, in the "Towards Symbolic Pointers Reasoning in Dynamic Symbolic Execution" study, Bitwuzla solved certain benchmarks more efficiently than Z3. (ar5iv.org)
Considerations for Symbolic Execution:
The choice between Bitwuzla and Z3 for symbolic execution should consider the specific requirements of the application, including the theories involved, the complexity of the constraints, and the need for incremental solving. Bitwuzla's architecture is optimized for bit-vector and array theories, making it suitable for applications in hardware verification and related fields. Z3, being a more general-purpose solver, offers broader support for various theories and may be advantageous in applications requiring extensive theory support.
In summary, while Bitwuzla often outperforms Z3 in benchmarks related to bit-vectors and arrays, the optimal choice depends on the specific context and requirements of the symbolic execution task.
Citations:
- 1: https://smt-comp.github.io/2024/results/qf_bv-single-query/?utm_source=openai
- 2: https://ar5iv.org/html/2109.03698?utm_source=openai
Verify Bitwuzla vs. Z3 for your workload
Based on SMT-COMP 2024¹ and recent benchmark studies², Bitwuzla leads in QF_BV and bit-vector/array‐heavy tasks, while Z3 offers broader theory support and robust incremental solving. Make sure your symbolic execution constraints align with Bitwuzla’s strengths before committing to this switch:• File: lib/Echidna/SymExec.hs, line 96
• Current call:withSolvers Bitwuzla (fromIntegral conf.campaignConf.symExecNSolvers) 1 timeoutSMT $ \solvers -> …• Action:
– Confirm that your use case is bit-vector/array-focused and benefits from Bitwuzla’s optimizations.
– If you rely on other theories or heavy incremental solving, benchmark both solvers in your environment.Citations:
- SMT-COMP 2024 QF_BV results: https://smt-comp.github.io/2024/results/qf_bv-single-query/
- “Towards Symbolic Pointers Reasoning in Dynamic Symbolic Execution”: https://ar5iv.org/html/2109.03698
lib/Echidna/SymExec.hs
Outdated
| newTimestamp = fromMaybe 0 $ Map.lookup (Var "symbolic_block_timestamp") cex.vars | ||
| diffTimestamp = if newTimestamp == 0 then 0 else newTimestamp - forceLit oldTimestamp | ||
|
|
||
| newNumber = fromMaybe 0 $ Map.lookup (Var "symbolic_block_number") cex.vars | ||
| diffNumber = if newNumber == 0 then 0 else newNumber - forceLit oldNumber | ||
|
|
There was a problem hiding this comment.
🛠️ Refactor suggestion
Handle potential arithmetic underflow in delay computation.
The delay computation could result in underflow if newTimestamp or newNumber is less than the old values. Consider adding bounds checking or using safe arithmetic operations.
- diffTimestamp = if newTimestamp == 0 then 0 else newTimestamp - forceLit oldTimestamp
- diffNumber = if newNumber == 0 then 0 else newNumber - forceLit oldNumber
+ diffTimestamp = if newTimestamp == 0 then 0 else max 0 (newTimestamp - forceLit oldTimestamp)
+ diffNumber = if newNumber == 0 then 0 else max 0 (newNumber - forceLit oldNumber)📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| newTimestamp = fromMaybe 0 $ Map.lookup (Var "symbolic_block_timestamp") cex.vars | |
| diffTimestamp = if newTimestamp == 0 then 0 else newTimestamp - forceLit oldTimestamp | |
| newNumber = fromMaybe 0 $ Map.lookup (Var "symbolic_block_number") cex.vars | |
| diffNumber = if newNumber == 0 then 0 else newNumber - forceLit oldNumber | |
| newTimestamp = fromMaybe 0 $ Map.lookup (Var "symbolic_block_timestamp") cex.vars | |
| - diffTimestamp = if newTimestamp == 0 then 0 else newTimestamp - forceLit oldTimestamp | |
| + diffTimestamp = if newTimestamp == 0 then 0 else max 0 (newTimestamp - forceLit oldTimestamp) | |
| newNumber = fromMaybe 0 $ Map.lookup (Var "symbolic_block_number") cex.vars | |
| - diffNumber = if newNumber == 0 then 0 else newNumber - forceLit oldNumber | |
| + diffNumber = if newNumber == 0 then 0 else max 0 (newNumber - forceLit oldNumber) |
🤖 Prompt for AI Agents
In lib/Echidna/SymExec.hs around lines 236 to 241, the current delay computation
subtracts old values from newTimestamp and newNumber without checking if new
values are smaller, risking arithmetic underflow. To fix this, add bounds
checking before subtraction to ensure the result is never negative, or use safe
arithmetic functions that handle underflow gracefully, returning zero or a
minimum bound instead of a negative value.
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (2)
lib/Echidna/SymExec.hs (2)
69-69: Remove commented code to improve clarity.This is a duplicate of a previous review comment. The commented out assertion check
{- methodSigelemassertSigs &&-}creates ambiguity about the intended behavior.
237-241: Handle potential arithmetic underflow in delay computation.This is a duplicate of a previous review comment. The delay computation could result in underflow if
newTimestampornewNumberis less than the old values.- diffTimestamp = if newTimestamp == 0 then 0 else newTimestamp - forceLit oldTimestamp - diffNumber = if newNumber == 0 then 0 else newNumber - forceLit oldNumber + diffTimestamp = if newTimestamp == 0 then 0 else max 0 (newTimestamp - forceLit oldTimestamp) + diffNumber = if newNumber == 0 then 0 else max 0 (newNumber - forceLit oldNumber)
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
flake.nix(1 hunks)lib/Echidna/SymExec.hs(3 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- flake.nix
🧰 Additional context used
🧠 Learnings (1)
lib/Echidna/SymExec.hs (1)
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.202Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
⏰ Context from checks skipped due to timeout of 90000ms (6)
- GitHub Check: Build Echidna on windows-latest
- GitHub Check: Build Echidna on ubuntu-latest
- GitHub Check: Build Echidna on macos-13
- GitHub Check: Build Linux (x86_64) binary
- GitHub Check: Build macOS (x86_64) binary
- GitHub Check: Build macOS (aarch64) binary
🔇 Additional comments (6)
lib/Echidna/SymExec.hs (6)
93-93: LGTM! Fixed undefined rpcInfo issue.Good fix from the previous review -
rpcInfois now properly initialized instead of being set toundefined.
102-102: Single method exploration is intentional for UX.Based on retrieved learnings, the limitation to exploring only one method at a time using
take 1 shuffleMethodsis intentional to improve user experience by providing faster symbolic execution results.
255-271: Well-designed cache-aware oracle implementation.The
cachedOraclefunction provides an elegant solution for consulting contract and slot caches before falling back to the default oracle. The pattern matching on query types is clean and the cache lookup logic is correct.
54-57: LGTM! Good monadic abstraction.The refactoring to use
MonadIO m, MonadThrow m, MonadReader Env mconstraints instead of concrete types improves testability and modularity. The function signature is now more flexible and follows Haskell best practices.
59-70: Excellent filtering logic for symbolic execution suitability.The new filtering functions
suitableForSymExecandfilterTargetprovide comprehensive logic for determining which methods should undergo symbolic execution. The checks for:
- Non-empty inputs
- No dynamic ABI types
- Exclusion of methods with "_no_symexec" in the name
- Target-specific filtering
are all well-reasoned and improve the precision of symbolic execution.
96-96: Good solver choice: Bitwuzla over Z3.The switch from Z3 to Bitwuzla aligns with the PR objectives of using more efficient and precise solving for symbolic execution.
lib/Echidna/SymExec.hs
Outdated
| maxExplore = Just (fromIntegral conf.campaignConf.symExecMaxExplore) | ||
| askSmtIters = conf.campaignConf.symExecAskSMTIters | ||
| rpcInfo = rpcFetcher conf.rpcUrl (fromIntegral <$> conf.rpcBlock) | ||
| defaultSender = fromJust $ fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender <|> Just 0 |
There was a problem hiding this comment.
Avoid unsafe fromJust usage.
The fromJust call could cause a runtime exception if all the alternatives in the <|> chain return Nothing. Consider providing a safe default value instead.
- let defaultSender = fromJust $ fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender <|> Just 0
+ let defaultSender = fromMaybe 0 $ fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| defaultSender = fromJust $ fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender <|> Just 0 | |
| let defaultSender = fromMaybe 0 $ | |
| fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender |
🤖 Prompt for AI Agents
In lib/Echidna/SymExec.hs at line 87, the use of fromJust on the combined Maybe
expression is unsafe and can cause a runtime exception if all options are
Nothing. Refactor the code to avoid fromJust by using a safe default value
directly with fromMaybe or by restructuring the expression to ensure a
guaranteed fallback value without partial functions.
There was a problem hiding this comment.
Actionable comments posted: 0
♻️ Duplicate comments (2)
lib/Echidna/SymExec/Exploration.hs (1)
99-99: Duplicate comment flagged: unsafefromJustusage.lib/Echidna/Campaign.hs (1)
313-313: Duplicate comment flagged: unsafefromJustusage.
🧹 Nitpick comments (5)
lib/Echidna/SymExec/Exploration.hs (4)
12-12: Remove unused import.
fromJustis imported but based on the past review comments, it seems the unsafe usage has been addressed. However, the import is still present and may not be needed.
51-51: Address HLint warning.The pipeline shows a HLint warning about moving brackets to avoid
$.- if (null assertSigs || selector `elem` assertSigs) && suitableForSymExec method && (unpack $ method.methodSignature) `notElem` failedProperties + if (null assertSigs || selector `elem` assertSigs) && suitableForSymExec method && unpack method.methodSignature `notElem` failedProperties
65-67: Remove commented-out code.Dead code should be removed to maintain code cleanliness.
- --(selector, method) = case filter (\(_, m) -> m.name == method.name) allMethods of - -- [] -> error $ "Method " ++ show methodName ++ " not found in contract ABI" - -- (x:_) -> x
68-68: Address HLint warning.The pipeline shows a HLint warning about moving brackets to avoid
$.- filterFunc (selector, method) = (null assertSigs || selector `elem` assertSigs) && suitableForSymExec method && (unpack $ method.methodSignature) `notElem` failedProperties + filterFunc (selector, method) = (null assertSigs || selector `elem` assertSigs) && suitableForSymExec method && unpack method.methodSignature `notElem` failedPropertieslib/Echidna/Campaign.hs (1)
166-166: Address HLint warning.The pipeline shows a HLint warning about using 'when' instead of 'if...then...else'.
- if any shrinkable tests then shrinkLoop shrinkLimit else return () + when (any shrinkable tests) (shrinkLoop shrinkLimit)
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (4)
lib/Echidna/Campaign.hs(4 hunks)lib/Echidna/SymExec/Exploration.hs(1 hunks)lib/Echidna/Types/Test.hs(6 hunks)stack.yaml(1 hunks)
✅ Files skipped from review due to trivial changes (1)
- stack.yaml
🚧 Files skipped from review as they are similar to previous changes (1)
- lib/Echidna/Types/Test.hs
🧰 Additional context used
🧠 Learnings (3)
📓 Common learnings
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
lib/Echidna/SymExec/Exploration.hs (4)
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using `error` to terminate the program when encountering unexpected ABI types in `modelToTx` is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
lib/Echidna/Campaign.hs (4)
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using `error` to terminate the program when encountering unexpected ABI types in `modelToTx` is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
🪛 GitHub Actions: HLint
lib/Echidna/SymExec/Exploration.hs
[warning] 51-51: HLint suggestion: Move brackets to avoid '$' for better readability.
[warning] 68-68: HLint suggestion: Move brackets to avoid '$' for better readability.
lib/Echidna/Campaign.hs
[warning] 166-166: HLint warning: Use 'when' instead of 'if ... then ... else ...' for cleaner code.
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (7)
- GitHub Check: Build Echidna on macos-13
- GitHub Check: Build Echidna on windows-latest
- GitHub Check: Build Echidna on ubuntu-latest
- GitHub Check: Build macOS (x86_64) binary
- GitHub Check: Build Linux (x86_64) binary
- GitHub Check: Build Linux (aarch64) binary
- GitHub Check: Build macOS (aarch64) binary
🔇 Additional comments (9)
lib/Echidna/SymExec/Exploration.hs (3)
80-87: Function logic is correct.The
filterTargetfunction properly handles different cases for method filtering based on configuration and transaction context.
88-122: Robust threading implementation.The
exploreContractfunction correctly implements asynchronous symbolic execution with proper thread management using MVars for synchronization.
47-49: Error handling could be improved.Using
errorfor a missing method is harsh. Consider returningNothinginstead and handling it gracefully upstream.- (selector, method) = case filter (\(_, m) -> m.name == methodName) allMethods of - [] -> error $ "Method " ++ show methodName ++ " not found in contract ABI" - (x:_) -> x + methodMatch = case filter (\(_, m) -> m.name == methodName) allMethods of + [] -> Nothing + (x:_) -> Just xThen handle the
Nothingcase appropriately in the surrounding logic.⛔ Skipped due to learnings
Learnt from: gustavo-grieco PR: gustavo-grieco/echidna#10 File: lib/Echidna/SymExec/Common.hs:139-139 Timestamp: 2025-07-07T12:24:07.157Z Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using `error` to terminate the program when encountering unexpected ABI types in `modelToTx` is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.Learnt from: gustavo-grieco PR: gustavo-grieco/echidna#10 File: lib/Echidna/SymExec.hs:102-102 Timestamp: 2025-06-03T11:55:54.240Z Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.lib/Echidna/Campaign.hs (6)
125-137: Well-structured mode separation.The conditional logic properly separates verification mode (workers=0, seqLen=1) from exploration mode, making the code intent clear.
162-180: Robust recursive loop with proper termination.The
shrinkAndRandomlyExplorefunction correctly implements recursive exploration with proper termination conditions and state checks.
210-232: Complex but correct transaction handling.The
txsToTxAndVmsSymfunction properly handles different modes (onlyRandom vs full) and correctly splits transaction sequences for symbolic execution.
241-249: Robust method selection logic.The pattern matching on
tx(Nothing vs Just) properly handles both random method selection and transaction-based method selection with appropriate error handling.
274-313: Comprehensive verification workflow.The
verifyMethodsandsymExecMethodfunctions implement a thorough verification process with proper error handling, state updates, and event reporting.
625-632: Useful helper function.The
findFailedTestsfunction provides a clean way to filter failed tests, improving code modularity.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (1)
lib/Echidna/Campaign.hs (1)
315-315: UnsafefromJust– duplicate prior feedbackUsing
fromJustonnamewill crash when no contract name is provided. HandleNothingexplicitly or propagate an error.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
lib/Echidna/Campaign.hs(4 hunks)lib/Echidna/SymExec/Exploration.hs(1 hunks)
🧰 Additional context used
🧠 Learnings (3)
📓 Common learnings
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
lib/Echidna/SymExec/Exploration.hs (4)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
lib/Echidna/Campaign.hs (4)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (7)
- GitHub Check: Build macOS (x86_64) binary
- GitHub Check: Build macOS (aarch64) binary
- GitHub Check: Build Linux (x86_64) binary
- GitHub Check: Build Linux (aarch64) binary
- GitHub Check: Build Echidna on windows-latest
- GitHub Check: Build Echidna on ubuntu-latest
- GitHub Check: Build Echidna on macos-13
🔇 Additional comments (2)
lib/Echidna/SymExec/Exploration.hs (1)
107-108: Check constructor usage forNonInteractive
isNonInteractive = conf.uiConf.operationMode == NonInteractive Textcompares a value of typeOperationModewith a partial application of the constructor usingText.
UnlessNonInteractiveactually has the formNonInteractive Text, this will not type-check.Please verify the intended pattern match; e.g.:
let isNonInteractive = case conf.uiConf.operationMode of NonInteractive _ -> True _ -> Falselib/Echidna/Campaign.hs (1)
278-281:verifyMethodspasses the wrong value type tosymExecMethod
contract.abiMapyields(selector, Method)pairs, butsymExecMethodexpects aMethod.
Current code therefore fails to compile:mapM_ (symExecMethod contract) allMethods -- allMethods :: Map k MethodFix by iterating over the
Methods only:- let allMethods = contract.abiMap - mapM_ (symExecMethod contract) allMethods + let allMethods = Map.elems contract.abiMap + mapM_ (symExecMethod contract) allMethods⛔ Skipped due to learnings
Learnt from: gustavo-grieco PR: gustavo-grieco/echidna#10 File: lib/Echidna/SymExec/Common.hs:139-139 Timestamp: 2025-07-07T12:24:07.157Z Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using `error` to terminate the program when encountering unexpected ABI types in `modelToTx` is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.Learnt from: gustavo-grieco PR: gustavo-grieco/echidna#10 File: lib/Echidna/Campaign.hs:259-261 Timestamp: 2025-07-04T12:03:36.010Z Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.Learnt from: gustavo-grieco PR: gustavo-grieco/echidna#10 File: lib/Echidna/SymExec.hs:102-102 Timestamp: 2025-06-03T11:55:54.240Z Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
| unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during symbolic exploration: " <> show e)) errors | ||
| unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic exploration: " <> unpack e)) partials |
There was a problem hiding this comment.
🛠️ Refactor suggestion
Mixing String and Text in error messages
show e returns String, while SymExecError expects Text. Using (<> ) on Strings then passing to a Text field will not compile under OverloadedStrings.
Convert to Text explicitly:
- unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during symbolic exploration: " <> show e)) errors
+ unless (null errors) $
+ mapM_ (\e -> pushWorkerEvent $ SymExecError $
+ "Error(s) during symbolic exploration: " <> Text.pack (show e)) errors(import qualified Data.Text as Text)
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during symbolic exploration: " <> show e)) errors | |
| unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic exploration: " <> unpack e)) partials | |
| unless (null errors) $ | |
| mapM_ (\e -> pushWorkerEvent $ SymExecError $ | |
| "Error(s) during symbolic exploration: " <> Text.pack (show e)) errors | |
| unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic exploration: " <> unpack e)) partials |
🤖 Prompt for AI Agents
In lib/Echidna/Campaign.hs around lines 265 to 266, the code mixes String and
Text types in error messages, causing compilation issues with OverloadedStrings.
Fix this by importing Data.Text qualified as Text and converting all String
values to Text explicitly using Text.pack before concatenation and passing to
SymExecError, ensuring consistent Text usage throughout.
| (Just ms, _) -> liftIO $ rElem (fromList $ map (Just . snd) $ filter (\(_, m) -> m.name `elem` ms) allMethods) | ||
| (_, []) -> return Nothing | ||
| _ -> liftIO $ rElem (fromList $ map (Just . snd) filteredMethods) |
There was a problem hiding this comment.
Possible runtime crash when targets list is empty
fromList throws for an empty list, so if ms is Just [] or none of the names match the ABI, the call to rElem . fromList will raise an exception before you even get to symbolic execution.
Consider guarding against an empty candidate list:
(Just ms, _) -> do
- liftIO $ rElem (fromList $ map (Just . snd) $ filter (\(_, m) -> m.name `elem` ms) allMethods)
+ let candidates = [snd p | p <- allMethods, m <- ms, m == (snd p).name]
+ if null candidates
+ then pure Nothing
+ else liftIO $ rElem (fromList $ map Just candidates)📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| (Just ms, _) -> liftIO $ rElem (fromList $ map (Just . snd) $ filter (\(_, m) -> m.name `elem` ms) allMethods) | |
| (_, []) -> return Nothing | |
| _ -> liftIO $ rElem (fromList $ map (Just . snd) filteredMethods) | |
| (Just ms, _) -> do | |
| let candidates = [snd p | p <- allMethods, m <- ms, m == (snd p).name] | |
| if null candidates | |
| then pure Nothing | |
| else liftIO $ rElem (fromList $ map Just candidates) | |
| (_, []) -> return Nothing | |
| _ -> liftIO $ rElem (fromList $ map (Just . snd) filteredMethods) |
🤖 Prompt for AI Agents
In lib/Echidna/SymExec/Exploration.hs around lines 72 to 74, the code calls
fromList on a list that can be empty when ms is Just [] or no method names
match, causing a runtime crash. To fix this, add a check to ensure the list
passed to fromList is not empty before calling rElem; if it is empty, return
Nothing instead to avoid exceptions.
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
lib/Echidna/Campaign.hs (1)
315-315: Replace unsafefromJustwith explicit error handling.Using
fromJuston the contract name can cause runtime crashes. Since verification mode requires a contract name, validate this earlier or handle theNothingcase explicitly.- pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.")) + pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> maybe "unknown" unpack name <> " using a single symbolic transaction."))
🧹 Nitpick comments (1)
tests/solidity/values/contract.sol (1)
20-23: Clarify the relationship between spawn and verification functions.The
spawn()function creates F instances but doesn't store or return them, creating a disconnect with the verification functions that expect F instances as parameters. While this might be intentional for symbolic execution testing where Echidna explores different combinations, consider adding a mechanism to track or return spawned instances for clearer test logic.Consider this approach to improve clarity:
+ F[] public spawnedInstances; + function spawn() public { - (new F()).init(firstRun); + F newF = new F(); + newF.init(firstRun); + spawnedInstances.push(newF); firstRun = false; }
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (21)
CHANGELOG.md(1 hunks)flake.nix(1 hunks)lib/Echidna/ABI.hs(2 hunks)lib/Echidna/Campaign.hs(7 hunks)lib/Echidna/Shrink.hs(3 hunks)lib/Echidna/Solidity.hs(4 hunks)lib/Echidna/Transaction.hs(2 hunks)lib/Echidna/Types/Campaign.hs(5 hunks)lib/Echidna/Types/Solidity.hs(1 hunks)lib/Echidna/UI.hs(5 hunks)package.yaml(3 hunks)src/test/Common.hs(6 hunks)src/test/Tests/Dapptest.hs(1 hunks)src/test/Tests/Integration.hs(2 hunks)src/test/Tests/Values.hs(3 hunks)tests/solidity/basic/gasleft.sol(1 hunks)tests/solidity/basic/gasleft.yaml(1 hunks)tests/solidity/basic/gasuse.yaml(1 hunks)tests/solidity/basic/propGasLimit.yaml(1 hunks)tests/solidity/values/contract.sol(1 hunks)tests/solidity/values/contract.yaml(1 hunks)
🧠 Learnings (4)
📓 Common learnings
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
lib/Echidna/Shrink.hs (1)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
tests/solidity/values/contract.sol (1)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
lib/Echidna/Campaign.hs (4)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
✅ Files skipped from review due to trivial changes (5)
- tests/solidity/basic/propGasLimit.yaml
- tests/solidity/basic/gasleft.yaml
- lib/Echidna/ABI.hs
- CHANGELOG.md
- tests/solidity/values/contract.yaml
🚧 Files skipped from review as they are similar to previous changes (11)
- src/test/Tests/Dapptest.hs
- package.yaml
- lib/Echidna/Types/Solidity.hs
- lib/Echidna/Transaction.hs
- src/test/Tests/Values.hs
- src/test/Tests/Integration.hs
- lib/Echidna/UI.hs
- src/test/Common.hs
- lib/Echidna/Solidity.hs
- flake.nix
- lib/Echidna/Types/Campaign.hs
🧰 Additional context used
🧠 Learnings (4)
📓 Common learnings
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
lib/Echidna/Shrink.hs (1)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
tests/solidity/values/contract.sol (1)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
lib/Echidna/Campaign.hs (4)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (7)
- GitHub Check: Build Linux (x86_64) binary
- GitHub Check: Build macOS (x86_64) binary
- GitHub Check: Build macOS (aarch64) binary
- GitHub Check: Build Linux (aarch64) binary
- GitHub Check: Build Echidna on windows-latest
- GitHub Check: Build Echidna on macos-13
- GitHub Check: Build Echidna on ubuntu-latest
🔇 Additional comments (14)
tests/solidity/basic/gasuse.yaml (1)
1-1: CI/runtime impact of raisingtestLimitto 10 000
Doubling the limit directly scales the number of generated test cases and can substantially lengthen symbolic-execution runs. Please confirm:• Current CI wall-time and memory budgets still pass comfortably.
• No other YAMLs depend ontestLimitdefaults and now diverge unintentionally.If needed, consider making the limit solver-/mode-dependent or exposing it via CLI to avoid blanket escalation.
tests/solidity/values/contract.sol (2)
1-14: LGTM! Clean and simple contract implementation.Contract
Fprovides a straightforward interface for testing with proper state management and clear function purposes.
25-37: Well-designed verification functions for symbolic execution testing.The verification functions are thoughtfully implemented:
- Proper use of
require()for preconditions andassert()for test conditions- State modifications to ensure Echidna treats these as non-pure functions worth exploring
- Clear separation of test scenarios (
verify_firstexpects true,verify_laterexpects false)This design aligns well with the reworked symbolic execution system mentioned in the PR objectives.
tests/solidity/basic/gasleft.sol (1)
1-6: LGTM! Gas range testing implementation is correct.The contract properly uses
gasleft()to test gas consumption within a specific range. The 2000-5000 gas window provides a reasonable testing boundary for gas accounting functionality.lib/Echidna/Shrink.hs (3)
33-33: LGTM! Comment clarification improves readability.
119-119: LGTM! Comment improvement clarifies the shorten strategy.
131-131: Good improvement to shrinking flexibility.Including the current sender (
i+1instead ofi) in the uniform selection allows the sender to remain unchanged during shrinking, which can be beneficial when the current sender is already optimal. This provides better exploration of the shrinking space.lib/Echidna/Campaign.hs (7)
21-21: LGTM! Import changes support the new symbolic execution architecture.The added imports properly support the restructured symbolic execution functionality with appropriate modularization.
Also applies to: 24-24, 27-27, 31-31, 37-37, 43-47, 54-54, 59-60
120-136: Excellent architectural separation of verification and exploration modes.The clear conditional logic separating symbolic verification (
workers == 0 && seqLen == 1) from symbolic exploration provides a clean architectural boundary. This enables focused single-method verification vs. broader symbolic exploration workflows.
156-160: LGTM! Event handling logic is sound.The listenerFunc properly handles NewCoverage events by triggering symbolic execution and shrinking. The hardcoded iteration count follows the previously discussed approach of using reasonable defaults.
162-180: Well-designed iterative shrinking and exploration strategy.The recursive approach cleanly handles the interleaving of test shrinking and symbolic exploration with appropriate termination conditions based on
stopOnFailand test states.
182-194: Clean helper functions for test state classification.The predicates properly handle worker-specific shrinking and test state identification with clear, readable logic.
210-231: Complex but well-structured transaction preparation for symbolic execution.The function correctly handles different symbolic execution strategies (targeted vs random) and properly prepares VM states and transaction sequences for each approach.
627-633: LGTM! New helper function for finding failed tests.The
findFailedTestsfunction provides a clean way to filter failed tests, supporting the new symbolic execution logic.
| when (not newCoverage && null errors && not (null txs)) ( | ||
| pushWorkerEvent $ SymExecError "No errors but symbolic execution found valid txs breaking assertions. Something is wrong.") | ||
| unless newCoverage (pushWorkerEvent $ SymExecLog "Symbolic execution finished with no new coverage.") |
There was a problem hiding this comment.
💡 Verification agent
🧩 Analysis chain
Verify coverage validation logic for exploration mode.
The error condition assumes that finding valid transactions without new coverage is always wrong, but this may be too strict for symbolic exploration mode (as opposed to verification mode where assertion failures always create coverage).
🏁 Script executed:
#!/bin/bash
# Verify the context where this coverage validation occurs
# Check if this is in exploration or verification mode
# Search for the function context and mode indicators
rg -B 10 -A 5 "No errors but symbolic execution found valid txs breaking assertions"Length of output: 1409
Once we find the line number, view the function body:
🏁 Script executed:
#!/bin/bash
# Locate the definition and full context of symexecTx
rg -n '^symexecTx' lib/Echidna/Campaign.hsLength of output: 44
🏁 Script executed:
#!/bin/bash
# Print the symexecTx function body around lines 200-330
sed -n '200,330p' lib/Echidna/Campaign.hsLength of output: 5942
Adjust non-coverage handling in exploration mode
In exploration mode, discovering valid transactions without increasing coverage is expected. Treating this as an error is too strict. Instead of emitting a SymExecError, downgrade it to a log.
- File: lib/Echidna/Campaign.hs
- Around lines 271–273
Suggested patch:
-- replace strict error on valid txs without coverage...
- when (not newCoverage && null errors && not (null txs)) (
- pushWorkerEvent $ SymExecError "No errors but symbolic execution found valid txs breaking assertions. Something is wrong.")
+ when (not newCoverage && null errors && not (null txs)) $
+ pushWorkerEvent $ SymExecLog "Symbolic execution found valid transactions without new coverage."
-- …then always log if there’s no new coverage
unless newCoverage (pushWorkerEvent $ SymExecLog "Symbolic execution finished with no new coverage.")📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| when (not newCoverage && null errors && not (null txs)) ( | |
| pushWorkerEvent $ SymExecError "No errors but symbolic execution found valid txs breaking assertions. Something is wrong.") | |
| unless newCoverage (pushWorkerEvent $ SymExecLog "Symbolic execution finished with no new coverage.") | |
| when (not newCoverage && null errors && not (null txs)) $ | |
| pushWorkerEvent $ SymExecLog "Symbolic execution found valid transactions without new coverage." | |
| unless newCoverage (pushWorkerEvent $ SymExecLog "Symbolic execution finished with no new coverage.") |
🤖 Prompt for AI Agents
In lib/Echidna/Campaign.hs around lines 271 to 273, the code currently treats
finding valid transactions without new coverage as an error by emitting
SymExecError. Change this behavior to emit a SymExecLog instead, downgrading the
severity from error to log to reflect that this is expected in exploration mode.
Replace the pushWorkerEvent call with SymExecLog for this case.
There was a problem hiding this comment.
Actionable comments posted: 1
🧹 Nitpick comments (2)
CHANGELOG.md (2)
5-5: Add release date for 2.2.7 headerThe previous sections carry dates; inserting one keeps the changelog machine-parsable and consistent.
11-11: Validate ARM64 Linux build artefacts ship via CICross-arch builds often miss CI packaging/signing steps the first time around. Sanity-check that nightly/release workflows now publish functional ARM64 binaries.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (16)
CHANGELOG.md(1 hunks)README.md(3 hunks)lib/Echidna.hs(2 hunks)lib/Echidna/Campaign.hs(8 hunks)lib/Echidna/Config.hs(2 hunks)lib/Echidna/Exec.hs(5 hunks)lib/Echidna/Output/JSON.hs(2 hunks)lib/Echidna/Solidity.hs(4 hunks)lib/Echidna/Types/Campaign.hs(5 hunks)lib/Echidna/UI.hs(7 hunks)lib/Echidna/UI/Report.hs(5 hunks)src/test/Common.hs(5 hunks)src/test/Tests/Seed.hs(1 hunks)tests/solidity/basic/default.yaml(1 hunks)tests/solidity/basic/gasuse.sol(0 hunks)tests/solidity/basic/gasuse.yaml(0 hunks)
🧠 Learnings (3)
📓 Common learnings
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
lib/Echidna/Campaign.hs (4)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
lib/Echidna/Types/Campaign.hs (3)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
🪛 GitHub Actions: CI
lib/Echidna/Types/Campaign.hs
[error] 13-13: GHC Warning treated as error: The import of ‘Echidna.Types.Tx’ is redundant except perhaps to import instances. Use 'import Echidna.Types.Tx()' to import instances alone. (unused-imports)
💤 Files with no reviewable changes (2)
- tests/solidity/basic/gasuse.yaml
- tests/solidity/basic/gasuse.sol
✅ Files skipped from review due to trivial changes (2)
- README.md
- lib/Echidna/UI/Report.hs
🚧 Files skipped from review as they are similar to previous changes (9)
- tests/solidity/basic/default.yaml
- lib/Echidna/UI.hs
- lib/Echidna.hs
- lib/Echidna/Exec.hs
- lib/Echidna/Output/JSON.hs
- lib/Echidna/Solidity.hs
- src/test/Tests/Seed.hs
- src/test/Common.hs
- lib/Echidna/Config.hs
🧰 Additional context used
🧠 Learnings (3)
📓 Common learnings
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
lib/Echidna/Campaign.hs (4)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
lib/Echidna/Types/Campaign.hs (3)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
🪛 GitHub Actions: CI
lib/Echidna/Types/Campaign.hs
[error] 13-13: GHC Warning treated as error: The import of ‘Echidna.Types.Tx’ is redundant except perhaps to import instances. Use 'import Echidna.Types.Tx()' to import instances alone. (unused-imports)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (4)
- GitHub Check: Build Linux (x86_64) binary
- GitHub Check: Build Linux (aarch64) binary
- GitHub Check: Build macOS (x86_64) binary
- GitHub Check: Build macOS (aarch64) binary
🔇 Additional comments (22)
CHANGELOG.md (4)
2-3: Ensure ancillary docs & CLI flags reflect dropped Etheno / estimateGas supportThese bullets announce permanent removals. Double-check that:
- All user-facing docs/examples have been purged or updated.
- CLI options or config keys that toggled these features are now rejected with a clear error.
Missed stragglers confuse users and break scripts.
8-9: Confirm new UI navigation & gas/s metrics are covered by testsUI-heavy changes are prone to regress. Ensure automated UI or integration tests exercise:
- Tab / PgUp / PgDown / arrow flows
- Correct gas-per-second rendering in headless mode
Otherwise future refactors may silently break them.
13-15: Regression tests needed for shrinking & gas-accounting fixesGiven past fragility in these areas, add unit/integration tests asserting:
- Shrink steps monotonically decrease size.
- Intrinsic gas is always included in total gas calculation.
Locks the bug closed.
16-19: Pin CI matrix to upgraded hevm & GHC 9.8.4Toolchain bumps can break build scripts and cached artefacts. Make sure:
- Docker images and nix flakes reference the new versions.
- CI caches are invalidated, otherwise subtle ABI mismatches may surface only in prod.
lib/Echidna/Types/Campaign.hs (3)
45-47: Good addition of SMT solver configuration.The new
symExecSMTSolverfield properly supports the enhanced symbolic execution functionality with clear documentation of supported solvers.
48-66: Appropriate configuration updates for symbolic execution refactoring.The comment updates correctly remove references to concolic execution, and the new
symExecMaxExplorefield provides needed control over exploration depth. The reduced default forsymExecMaxIters(10→5) is reasonable for the new implementation.
114-118: Well-defined defaults for new symbolic execution parameters.The new
defaultSymExecMaxExploreconstant and the updateddefaultSymExecMaxItersvalue provide sensible defaults for the enhanced symbolic execution functionality.lib/Echidna/Campaign.hs (15)
21-60: Import changes support the symbolic execution refactoring.The new imports properly reflect the modular approach to symbolic execution with separate modules for common utilities, exploration, and verification. The imports align with the architectural changes described in the PR objectives.
119-136: Well-implemented dual-mode symbolic execution.The conditional logic properly distinguishes between verification mode (workers=0, seqLen=1) and exploration mode, implementing the architectural changes described in the PR objectives. The mode selection is clear and appropriate.
154-158: Listener function properly handles new coverage events.The function correctly processes coverage events by performing symbolic execution and exploration. This aligns with the new symbolic exploration workflow described in the PR objectives.
160-178: Effective implementation of exploration strategy.The
shrinkAndRandomlyExplorefunction properly implements the iterative approach combining shrinking and symbolic exploration. The recursive structure with countdown and conditional logic for stopping on failures is well-designed.
180-203: Well-structured helper functions for test management.The helper functions (
shrinkable,final,shrinkLoop) provide clear abstractions for test state management and worker-specific processing. The logic is sound and supports the distributed fuzzing approach.
208-230: Complex but necessary transaction preparation logic.The
txsToTxAndVmsSymfunction implements the two strategies for symbolic transaction introduction mentioned in the PR objectives: random insertion and last transaction symbolization. While complex, the logic properly handles the different modes and VM state preparation.
232-249: Appropriate target method selection and exploration dispatch.The
symexecTxfunction properly implements the target method selection logic, handling both random method selection and transaction-specific targeting. The pattern matching approach clearly separates the two exploration strategies.
250-272: Proper implementation of exploration workflow.The
exploreAndVerifyfunction correctly handles the symbolic exploration workflow with appropriate thread management, result processing, and error handling. The coverage validation logic is appropriate for exploration mode.
273-278: Clean implementation of verification mode.The
verifyMethodsfunction properly implements the verification mode by systematically verifying all contract methods. This aligns with the formal verification approach described in the PR objectives.
280-314: Comprehensive method verification implementation.The
symExecMethodfunction properly handles individual method verification with appropriate error handling and test state updates. The logic for handling assertion failures and the "unsolvable" state aligns with the verification mode objectives.Based on previous discussions, the coverage validation logic is correct for verification mode where assertion failures inherently create new coverage.
494-514: Appropriate refactoring of callseq function.The changes to the
callseqfunction appear to be minor refactoring that maintains the core transaction execution and coverage tracking functionality while improving code organization.
538-542: Good encapsulation of corpus management logic.Making
addToCorpusa local function improves encapsulation and maintains the same logic for managing successful transactions in the corpus.
549-559: Maintained functionality in execTxOptC.The changes to
execTxOptCmaintain the essential transaction execution with coverage optimization functionality while adapting to the new architecture.
583-584: Minor structural improvements to evalSeq.The changes maintain the core sequential transaction execution logic while making minor structural improvements to the recursive processing.
600-607: Useful utility function for test filtering.The
findFailedTestsfunction provides a clean abstraction for finding failed tests, supporting the symbolic execution targeting logic described in the PR objectives.
There was a problem hiding this comment.
Actionable comments posted: 0
♻️ Duplicate comments (1)
lib/Echidna/SymExec/Common.hs (1)
48-52: Logical error insuitableForSymExecdue to operator precedence.This issue has already been identified and tracked in issue crytic#1390. The current implementation incorrectly allows methods with dynamic inputs or blacklisted methods due to operator precedence.
🧹 Nitpick comments (1)
lib/Echidna/SymExec/Common.hs (1)
228-229: Remove commented-out debug code.Clean up the commented debug statements for better code maintainability.
- --liftIO $ putStrLn ("Exploring: " ++ T.unpack method.methodSignature) - --pushWorkerEvent undefined calldataSym@(cd, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] ... let results = map fst models - --liftIO $ mapM_ TIO.putStrLn partials return (map (modelToTx dst vm.block.timestamp vm.block.number method conf.solConf.sender defaultSender) results, map formatPartial partials)Also applies to: 248-248
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
lib/Echidna/SymExec/Common.hs(1 hunks)stack.yaml(1 hunks)
✅ Files skipped from review due to trivial changes (1)
- stack.yaml
🧰 Additional context used
🧠 Learnings (2)
📓 Common learnings
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using `error` to terminate the program when encountering unexpected ABI types in `modelToTx` is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
lib/Echidna/SymExec/Common.hs (3)
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using error to terminate the program when encountering unexpected ABI types in modelToTx is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using take 1 shuffleMethods to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: #10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (7)
- GitHub Check: Build macOS (x86_64) binary
- GitHub Check: Build macOS (aarch64) binary
- GitHub Check: Build Echidna on macos-13
- GitHub Check: Build Linux (aarch64) binary
- GitHub Check: Build Echidna on windows-latest
- GitHub Check: Build Echidna on ubuntu-latest
- GitHub Check: Build Linux (x86_64) binary
Co-authored-by: Emilio López <2642849+elopez@users.noreply.github.com>
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (2)
lib/Echidna/Campaign.hs (2)
267-269: Reconsider error condition for exploration mode.The logic treats finding valid transactions without new coverage as an error, but in exploration mode (unlike verification mode), this can be a legitimate outcome. Valid transactions may not always increase coverage during exploration.
261-262: Fix String/Text type mismatch in error messages.The code mixes
String(fromshow e) withTextliterals, causing compilation issues withOverloadedStrings. The<>operator andSymExecErrorexpect consistentTexttypes.Apply this fix:
+import Data.Text qualified as Text + -unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during symbolic exploration: " <> show e)) errors +unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) during symbolic exploration: " <> Text.pack (show e))) errors -unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> show e)) errors +unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> Text.pack (show e))) errorsAlso applies to: 293-294
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
lib/Echidna/Campaign.hs(4 hunks)lib/Echidna/Server.hs(2 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- lib/Echidna/Server.hs
🧰 Additional context used
🧠 Learnings (5)
📓 Common learnings
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using `error` to terminate the program when encountering unexpected ABI types in `modelToTx` is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
📚 Learning: in echidna's symbolic execution verification mode (lib/echidna/campaign.hs verifymethod function), s...
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/Campaign.hs:259-261
Timestamp: 2025-07-04T12:03:36.010Z
Learning: In Echidna's symbolic execution verification mode (lib/Echidna/Campaign.hs verifyMethod function), symbolic execution specifically targets assertion failures. When assertion failures are triggered, they inherently create new coverage by definition. Therefore, finding valid transactions without new coverage in verification mode indicates a logic error, unlike in exploration mode where valid transactions may legitimately exist without increasing coverage.
Applied to files:
lib/Echidna/Campaign.hs
📚 Learning: in echidna's symbolic execution (lib/echidna/symexec.hs), the exploration is intentionally limited t...
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec.hs:102-102
Timestamp: 2025-06-03T11:55:54.240Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec.hs), the exploration is intentionally limited to one method at a time using `take 1 shuffleMethods` to improve user experience by providing faster symbolic execution results rather than waiting for all methods to be explored.
Applied to files:
lib/Echidna/Campaign.hs
📚 Learning: in echidna's symbolic execution (lib/echidna/symexec/common.hs), using `error` to terminate the prog...
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec/Common.hs:139-139
Timestamp: 2025-07-07T12:24:07.157Z
Learning: In Echidna's symbolic execution (lib/Echidna/SymExec/Common.hs), using `error` to terminate the program when encountering unexpected ABI types in `modelToTx` is acceptable and preferred over graceful error handling, as it indicates a programming error that should cause immediate termination.
Applied to files:
lib/Echidna/Campaign.hs
📚 Learning: in haskell, when working in a monad that has a monadio instance (like readert m io), io actions can ...
Learnt from: gustavo-grieco
PR: gustavo-grieco/echidna#10
File: lib/Echidna/SymExec/Exploration.hs:78-82
Timestamp: 2025-07-04T12:01:01.686Z
Learning: In Haskell, when working in a monad that has a MonadIO instance (like ReaderT m IO), IO actions can be used directly without explicitly calling liftIO. The compiler automatically lifts them using the MonadIO instance, making explicit liftIO calls unnecessary in such contexts.
Applied to files:
lib/Echidna/Campaign.hs
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)
- GitHub Check: Build macOS (x86_64) binary
🔇 Additional comments (7)
lib/Echidna/Campaign.hs (7)
21-21: Import updates align with symbolic execution restructuring.The import changes correctly reflect the modular redesign of symbolic execution, adding necessary dependencies for the new verification and exploration modes.
Also applies to: 24-24, 27-27, 35-35, 42-46, 53-53, 58-59
119-133: Well-structured dual-mode symbolic execution.The conditional logic correctly implements the two symbolic execution modes described in the PR objectives:
- Verification mode: Triggered when
workers == Just 0andseqLen == 1- Exploration mode: Uses event listener loop for fuzzing integration
The implementation aligns well with the stated goal of supporting both stateless verification and exploration modes.
152-201: Solid iterative shrinking and exploration logic.The
shrinkAndRandomlyExplorefunction correctly implements:
- Worker-specific shrinking to avoid contention (using
test.workerId == Just workerId)- Proper termination conditions with countdown parameter
- Logical flow: shrink first, then explore, with early exit on failures
The recursive design with bounded iterations ensures the process will terminate while maximizing shrinking opportunities.
204-228: Comprehensive transaction preparation for symbolic execution.The
txsToTxAndVmsSymfunction effectively implements both symbolic transaction strategies mentioned in the PR objectives:
- Normal mode: Prepares both last transaction symbolization and random position insertion
- Random-only mode: Focuses on random position insertion
The VM state building using
foldlMwithexecTxcorrectly constructs intermediate states for symbolic exploration.
230-247: Well-structured symbolic execution orchestration.The
symexecTxfunction correctly implements the symbolic execution workflow:
- Uses
chooseContractfor contract selection- Handles both random method targeting and transaction-specific targeting
- Proper integration with failed test signatures for assertion-focused exploration
600-607: Clean utility function for test filtering.The
findFailedTestsfunction provides a straightforward way to identify failed tests for symbolic execution targeting. The implementation correctly reads test references and applies thedidFailfilter.
154-155: Proper integration of symbolic execution with existing workflow.The integration points correctly connect symbolic execution with the existing fuzzing and shrinking workflow:
symexecTxs Falseenables both symbolic strategies (not random-only)- Integration with
shrinkAndRandomlyExploremaintains the iterative improvement cycleAlso applies to: 202-202
| verifyMethods = do | ||
| dapp <- asks (.dapp) | ||
| let cs = Map.elems dapp.solcByName | ||
| contract <- chooseContract cs name | ||
| let allMethods = contract.abiMap | ||
| mapM_ (symExecMethod contract) allMethods | ||
|
|
||
| symExecMethod contract method = do | ||
| lift callback | ||
| (threadId, symTxsChan) <- verifyMethod method contract vm | ||
|
|
||
| modify' (\ws -> ws { runningThreads = [threadId] }) | ||
| lift callback | ||
|
|
||
| (symTxs, partials) <- liftIO $ takeMVar symTxsChan | ||
| let txs = extractTxs symTxs | ||
| let errors = extractErrors symTxs | ||
|
|
||
| modify' (\ws -> ws { runningThreads = [] }) | ||
| lift callback | ||
| let methodSignature = unpack method.methodSignature | ||
| if not (null partials) || not (null errors) then do | ||
| unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> show e)) errors | ||
| unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic verification of method " <> methodSignature <> ": " <> unpack e)) partials | ||
| updateTests $ \test -> do | ||
| if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then | ||
| pure $ Just $ test { Test.state = Passed } | ||
| else | ||
| pure $ Just test | ||
| else do | ||
| -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event | ||
| newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm [symTx]) txs | ||
|
|
||
| unless newCoverage ( do | ||
| unless (null txs) $ error "No new coverage but symbolic execution found valid txs. Something is wrong." | ||
| updateTests $ \test -> do | ||
| if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then | ||
| pure $ Just $ test { Test.state = Unsolvable } | ||
| else | ||
| pure $ Just test | ||
| pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.")) |
There was a problem hiding this comment.
💡 Verification agent
🧩 Analysis chain
Solid verification mode implementation with proper state management.
The verifyMethods function correctly implements symbolic verification:
- Iterates through all contract methods for comprehensive verification
- Updates test states appropriately (
Passedfor errors/partials,Unsolvablefor no coverage) - The coverage validation logic at Line 305 is correct for verification mode, as assertion failures inherently create new coverage in this context (per retrieved learnings)
However, Line 311 uses fromJust name which could crash if the contract name is Nothing.
🏁 Script executed:
#!/bin/bash
# Verify that contract name is guaranteed to be present in verification mode
ast-grep --pattern 'runSymWorker $_ $_ $_ $_ $_ name' -A 10 -B 5Length of output: 1250
🏁 Script executed:
#!/bin/bash
# Inspect runSymWorker to see how verifyMethods is invoked and how 'name' is used
rg -n "runSymWorker" -A 50 -B 10 lib/Echidna/Campaign.hs
# Show the definition of chooseContract to determine how it handles a Nothing name
rg -n "chooseContract" -A 10 -B 10 lib/Echidna/Campaign.hsLength of output: 6355
🏁 Script executed:
#!/bin/bash
# Locate the file defining chooseContract
echo "Searching for file containing 'chooseContract' definition..."
FILE=$(rg -l "chooseContract :: " -n . | head -n1)
echo "Found in: $FILE"
# Display the implementation of chooseContract
echo "Showing 'chooseContract' implementation:"
rg -n "chooseContract :: " -A 20 -B 0 "$FILE"Length of output: 1508
Fix unsafe use of fromJust in verification logging
The log at lib/Echidna/Campaign.hs:311 uses fromJust name, which will crash if the user did not supply a contract name (name == Nothing). Since chooseContract cs name already defaults to the first contract when name is Nothing, use the selected contract.contractName instead:
- File: lib/Echidna/Campaign.hs
Line ~311
Suggested change:
- pushWorkerEvent $ SymExecLog
- ("Symbolic execution finished verifying contract " <> unpack (fromJust name)
- <> " using a single symbolic transaction.")
+ let loggedName = unpack contract.contractName
+ pushWorkerEvent $ SymExecLog
+ ("Symbolic execution finished verifying contract " <> loggedName
+ <> " using a single symbolic transaction.")📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| verifyMethods = do | |
| dapp <- asks (.dapp) | |
| let cs = Map.elems dapp.solcByName | |
| contract <- chooseContract cs name | |
| let allMethods = contract.abiMap | |
| mapM_ (symExecMethod contract) allMethods | |
| symExecMethod contract method = do | |
| lift callback | |
| (threadId, symTxsChan) <- verifyMethod method contract vm | |
| modify' (\ws -> ws { runningThreads = [threadId] }) | |
| lift callback | |
| (symTxs, partials) <- liftIO $ takeMVar symTxsChan | |
| let txs = extractTxs symTxs | |
| let errors = extractErrors symTxs | |
| modify' (\ws -> ws { runningThreads = [] }) | |
| lift callback | |
| let methodSignature = unpack method.methodSignature | |
| if not (null partials) || not (null errors) then do | |
| unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Error(s) solving constraints produced by method " <> methodSignature <> ": " <> show e)) errors | |
| unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> "Partial explored path(s) during symbolic verification of method " <> methodSignature <> ": " <> unpack e)) partials | |
| updateTests $ \test -> do | |
| if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then | |
| pure $ Just $ test { Test.state = Passed } | |
| else | |
| pure $ Just test | |
| else do | |
| -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event | |
| newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm [symTx]) txs | |
| unless newCoverage ( do | |
| unless (null txs) $ error "No new coverage but symbolic execution found valid txs. Something is wrong." | |
| updateTests $ \test -> do | |
| if isOpen test && isAssertionTest test && getAssertionSignature test == methodSignature then | |
| pure $ Just $ test { Test.state = Unsolvable } | |
| else | |
| pure $ Just test | |
| pushWorkerEvent $ SymExecLog ("Symbolic execution finished verifying contract " <> unpack (fromJust name) <> " using a single symbolic transaction.")) | |
| symExecMethod contract method = do | |
| lift callback | |
| (threadId, symTxsChan) <- verifyMethod method contract vm | |
| modify' (\ws -> ws { runningThreads = [threadId] }) | |
| lift callback | |
| (symTxs, partials) <- liftIO $ takeMVar symTxsChan | |
| let txs = extractTxs symTxs | |
| let errors = extractErrors symTxs | |
| modify' (\ws -> ws { runningThreads = [] }) | |
| lift callback | |
| let methodSignature = unpack method.methodSignature | |
| if not (null partials) || not (null errors) then do | |
| unless (null errors) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> | |
| "Error(s) solving constraints produced by method " | |
| <> methodSignature <> ": " <> show e)) errors | |
| unless (null partials) $ mapM_ ((pushWorkerEvent . SymExecError) . (\e -> | |
| "Partial explored path(s) during symbolic verification of method " | |
| <> methodSignature <> ": " <> unpack e)) partials | |
| updateTests $ \test -> do | |
| if isOpen test | |
| && isAssertionTest test | |
| && getAssertionSignature test == methodSignature | |
| then pure $ Just $ test { Test.state = Passed } | |
| else pure $ Just test | |
| else do | |
| -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event | |
| newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm [symTx]) txs | |
| unless newCoverage ( do | |
| unless (null txs) $ | |
| error "No new coverage but symbolic execution found valid txs. Something is wrong." | |
| updateTests $ \test -> do | |
| if isOpen test | |
| && isAssertionTest test | |
| && getAssertionSignature test == methodSignature | |
| then pure $ Just $ test { Test.state = Unsolvable } | |
| else pure $ Just test | |
| let loggedName = unpack contract.contractName | |
| pushWorkerEvent $ SymExecLog | |
| ("Symbolic execution finished verifying contract " | |
| <> loggedName | |
| <> " using a single symbolic transaction.") | |
| ) |
🤖 Prompt for AI Agents
In lib/Echidna/Campaign.hs around lines 271 to 311, the code uses fromJust name
in the final logging statement, which can cause a runtime crash if name is
Nothing. Since chooseContract defaults to a contract when name is Nothing,
replace fromJust name with contract.contractName to safely reference the
selected contract's name in the log message.
2 participants
This PR brings a good number of important changes to the symbolic execution code:
Some unrelated changes included in this PR:
Known issues:
Summary by CodeRabbit
New Features
Bug Fixes
Refactor
Chores