fix: simplify symbol parsing #334

0xkarmacoma · 2024-07-29T21:59:02Z

simplify method names - get_contract_mapping_info_by_bytecode -> get_by_bytecode - get_contract_mapping_info_by_name -> get_by_name - add_contract_mapping_info -> add
introduce an add_or_create method (like setdefault, but also returns the value)
factor into a separate parse_symbols method to avoid nested try..except blocks
avoid the except Exception: pass pattern, it does hide exceptions
in parse_ast, make contract_name required (it could lead to exceptions when the default was used)

- simplify method names - get_contract_mapping_info_by_bytecode -> get_by_bytecode - get_contract_mapping_info_by_name -> get_by_name - add_contract_mapping_info -> add - introduce an add_or_create method (like setdefault, but also returns the value) - factor into a separate parse_symbols method to avoid nested try..except blocks - avoid the `except Exception: pass` pattern, it does hide exceptions - in parse_ast, make contract_name required (it could lead to exceptions when the default was used)

0xkarmacoma · 2024-07-29T21:59:39Z

cc @pillip wdyt?

daejunpark

it would be great if we could get this reviewed by @pillip, as there is a non-trivial change.

daejunpark · 2024-07-30T00:05:09Z

src/halmos/mapper.py


        for child_node in node.get("nodes", []):
-            self.parse_ast(child_node, current_contract)
+            self.parse_ast(child_node, contract_name)


this doesn't seem semantic-preserving. why not treating differently the case of child_node["nodeType"] == "ContractDefinition"? in that case, child_node.get("name", "") was used instead of contract_name.

i mean, two names could be different, especially for nested contracts.

it is definitely not semantic preserving, because I think there was an issue. The except Exception: pass was swallowing exceptions like this:

error parsing symbols for contract FuzzCantCatch Traceback (most recent call last): File "/Users/karma/projects/halmos/src/halmos/__main__.py", line 1304, in parse_symbols Mapper().parse_ast(contract_map[contract_name][0]["ast"]) File "/Users/karma/projects/halmos/src/halmos/mapper.py", line 103, in parse_ast self.parse_ast(child_node, current_contract) File "/Users/karma/projects/halmos/src/halmos/mapper.py", line 97, in parse_ast self.append_node( File "/Users/karma/projects/halmos/src/halmos/mapper.py", line 79, in append_node raise ValueError(f"Contract {contract_name} not found") ValueError: Contract not found

Now you're right, I had some wrong assumptions about what we would find in the AST. For instance with this contract: https://github.com/karmacoma-eth/halmos-sandbox/blob/main/test/46_hellFunc.t.sol (one solidity file with no eponymous contract, and it contains 2 contract definitions)

Walking the AST in out/46_hellFunc.t.sol/FuzzCantCatch.json we find:

SourceUnit PragmaDirective UserDefinedValueTypeDefinition (Int) UsingForDirective UsingForDirective UsingForDirective UsingForDirective FunctionDefinition (add) Block FunctionDefinition (div) Block FunctionDefinition (mul) Block FunctionDefinition (sub) Block ContractDefinition (FuzzCantCatch) VariableDeclaration (numbr) VariableDeclaration (namber) VariableDeclaration (nunber) VariableDeclaration (mumber) VariableDeclaration (numbor) VariableDeclaration (numbir) FunctionDefinition (hellFunc) Block FunctionDefinition (_numbaar) Block ContractDefinition (HellCatcher) VariableDeclaration (fuzz) FunctionDefinition (setUp) Block FunctionDefinition (test_hellFunc) Block FunctionDefinition (testCatchEasyBugWithFuzz) Block

And if we walk the AST of out/46_hellFunc.t.sol/HellCatcher.json, we get exactly the same thing 😵 it's actually the AST of the whole source file, not just the contract

~~Still, based on this I think we should indeed "guess" contract_name based on the json filename, and dig into the AST until we hit the right node.~~

We still have a couple problems:

how to handle another contract definition that's not the same as contract_name? Currently it would be processed if it has not been seen yet, or skipped if it has

how to handle contract name collisions (A.sol and B.sol both define a contract called C), I think right now it's nondeterministic (whichever one is processed first is added, the other one is skipped)

ok I found what was causing the initial issue, in 46_hellFunc.t.sol:

type Int is uint256;

What happens is this:

it is outside of a contract definition

it results in an AST node of type UserDefinedValueTypeDefinition

because node_type != "SourceUnit", we try to append it to the current_contract mapping

but because we haven't encountered a ContractDefinition yet, it tries to append it to the default contract_name = "", which raises the exception

Similar thing going on here: https://github.com/karmacoma-eth/halmos-sandbox/blob/main/test/17_pAtHExPlOSion.t.sol, the free functions (FunctionDefinition AST nodes) before the contract definition cause the same exception

+ rename to lookup_selector + rename address to selector

we don't need the id and visibility field

by making ContractMappingInfo a dict instead of a list

0xkarmacoma · 2024-08-01T01:44:10Z

Ok I think this is ready for another round of review, I added a couple more tests that show that we handle the previous issue. Plus a couple more goodies:

can now invoke halmos.mapper as a module to inspect a json file containing an ast. For instance:

python -m halmos.mapper tests/regression/out/Address.sol/Address.json

SourceUnit
  PragmaDirective (ignored node type)
  ContractDefinition: Address
    ErrorDefinition: AddressInsufficientBalance (added node with ast_node.selector='0xcd786059'
    ErrorDefinition: AddressEmptyCode (added node with ast_node.selector='0x9996b315'
    ErrorDefinition: FailedInnerCall (added node with ast_node.selector='0x1425ea42'
    FunctionDefinition: sendValue
      Block (ignored node type)
    FunctionDefinition: functionCall
      Block (ignored node type)
    FunctionDefinition: functionCall
      Block (ignored node type)
    FunctionDefinition: functionCallWithValue
      Block (ignored node type)
    FunctionDefinition: functionCallWithValue
      Block (ignored node type)
    FunctionDefinition: functionStaticCall
      Block (ignored node type)
    FunctionDefinition: functionStaticCall
      Block (ignored node type)
    FunctionDefinition: functionDelegateCall
      Block (ignored node type)
    FunctionDefinition: functionDelegateCall
      Block (ignored node type)
    FunctionDefinition: verifyCallResultFromTarget
      Block (ignored node type)
    FunctionDefinition: verifyCallResult
      Block (ignored node type)
    FunctionDefinition: verifyCallResult
      Block (ignored node type)
    FunctionDefinition: defaultRevert
      Block (ignored node type)
    FunctionDefinition: _revert
      Block (ignored node type)

### Results ###

Contract: Address
  0xcd786059: AddressInsufficientBalance
  0x9996b315: AddressEmptyCode
  0x1425ea42: FailedInnerCall

comes with a cutesie little Explanation helper
rename address to selector
rename find_nodes_by_address to lookup_selector
ContractMappingInfo.nodes is a dict instead of a list
☝️ this lets us look up selectors in a contract scope, instead of scanning linearly the entire namespace
AstNodes are simplified, I don't think we need to keep id and visibility
only keep track of AstNodes that have a selector
things that are not scoped to a contract (e.g. global errors and events) are tracked separately under the contract_name = None "namespace", which can be retrieved with Mapper().get_by_name(None)

pillip · 2024-08-03T02:36:14Z

@karmacoma-eth @daejunpark
Sorry for the late checking. I totally agree with the refactoring of parsing.
I think halmos.mapper is too good 👍

0xkarmacoma requested a review from daejunpark July 29, 2024 21:59

daejunpark reviewed Jul 30, 2024

View reviewed changes

0xkarmacoma added 2 commits July 30, 2024 18:31

WIP: rework parse_ast

9ebde62

fix test_mapper

962f8c6

0xkarmacoma marked this pull request as draft July 31, 2024 01:37

0xkarmacoma added 6 commits July 31, 2024 10:10

add test_mapper.test_parse_multicontract_ast

21c920d

find_nodes_by_address returns first match

5242436

+ rename to lookup_selector + rename address to selector

simplify AstNode

8fc3214

we don't need the id and visibility field

add new lookup_selector tests

3be86f6

avoid O(n) search in lookup_selector

5328902

by making ContractMappingInfo a dict instead of a list

fix print output

ec0b124

0xkarmacoma marked this pull request as ready for review August 1, 2024 01:44

daejunpark approved these changes Aug 1, 2024

View reviewed changes

0xkarmacoma merged commit 954ed59 into main Aug 1, 2024
33 checks passed

0xkarmacoma deleted the simplify-symbol-parsing branch August 1, 2024 22:37

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix: simplify symbol parsing #334

fix: simplify symbol parsing #334

0xkarmacoma commented Jul 29, 2024

0xkarmacoma commented Jul 29, 2024

daejunpark left a comment

daejunpark Jul 30, 2024 •

edited

Loading

0xkarmacoma Jul 30, 2024 •

edited

Loading

0xkarmacoma Jul 30, 2024

0xkarmacoma Jul 30, 2024 •

edited

Loading

0xkarmacoma Jul 30, 2024

0xkarmacoma commented Aug 1, 2024

pillip commented Aug 3, 2024

fix: simplify symbol parsing #334

fix: simplify symbol parsing #334

Conversation

0xkarmacoma commented Jul 29, 2024

0xkarmacoma commented Jul 29, 2024

daejunpark left a comment

Choose a reason for hiding this comment

daejunpark Jul 30, 2024 • edited Loading

Choose a reason for hiding this comment

0xkarmacoma Jul 30, 2024 • edited Loading

Choose a reason for hiding this comment

0xkarmacoma Jul 30, 2024

Choose a reason for hiding this comment

0xkarmacoma Jul 30, 2024 • edited Loading

Choose a reason for hiding this comment

0xkarmacoma Jul 30, 2024

Choose a reason for hiding this comment

0xkarmacoma commented Aug 1, 2024

pillip commented Aug 3, 2024

daejunpark Jul 30, 2024 •

edited

Loading

0xkarmacoma Jul 30, 2024 •

edited

Loading

0xkarmacoma Jul 30, 2024 •

edited

Loading