[Feature/#244] Parse symbols from build to print readable traces #309

pillip · 2024-06-11T03:59:08Z

Change Type

Bug fix (Not Breaking-change. Solve issue.)
New feature (Not Breaking-change. Add new feature.)
Breaking change (Bug fix or New featrure that cause Breaking change.)
Code Convention (Edit Code Convention.)
Refactoring (Refactor Code without feature change.)

Description

This PR introduces several significant updates and new functionalities that parse and covert raw hex code to human readable string. The changes primarily focus on enhancing the Mapper class with methods for AST parsing and adding the DeployAddressMapper class for managing deployed contract address mappings.

Related Issues

This PR resolves #244

Changes

Mapper class
- Implemented using the Singleton pattern to manage contract and node mapping information from AST
- Use AstNode and ContractMappingInfo dataclasses
- Methods
  - parse_ast: Recursively parses AST nodes.
  - add_contract_mapping_info: Adds a new contract mapping
  - get_contract_mapping_info_by_name: Retrieves contract mapping by contract name
  - get_contract_mapping_info_by_bytecode: Retrieves contract mapping by bytecode suffix
  - append_node: Appends a new AST node to contract mapping info
  - find_nodes_by_address: Converts hex addresses to human-readable strings including contract name, event name, function name, and variable name
DeployAddressMapper class
- Implemented using the Singleton pattern
- Added to manage deployed contract address mappings with predefined mappings such as HEVM and SVM.
Modify functions when used for printing traces
- render_trace: Added logic to look up deployed contract names.
- rendered_calldata, hexify, find_nodes_by_address: Updated to support contract name parameters for searching nodes in specific contracts.

Tests

> cd halmos/examples/simple
> halmos -vvvv

Screenshot

* Define AstNode and CotractMappingInfo dataclassses for storing contract's AST data * Define SingletonMeta metaclass to enforce singleton pattern for Mapper class * Implement Mapper class using SingletonMeta for managing contract mapping info from AST * Add methods to mapper: * add_contract_mapping_info: Add a new contract mapping * get_contract_mapping_info_by_name: Get contract mapping by contract_name * get_contract_mapping_info_by_bytecode : Get contract mapping by bytecode * append_node : Append a new AST node to contract mapping info

* Add ignored node types to _PARSING_IGNORED_NODE_TYPES * Implement methods for AST parsing: * parse_ast: Recursively parse AST nodes * _get_nodes_info: Helper method to extract id, name, address and visibility of node * _get_node_address: Helper method to extract address based on node type * _get_current_contract: Helper method to determine the name of current contract being parsed * Add testcases of parse_ast method * Add parsing logic in parse_build_out function at __main__.py

* Update _get_node_info method in Mapper classe to prepend 0x to the node address for facilitating trace comparisons

* Implement find_nodes_by_address method in Mapper class to convert hex address to human readable string * Returns formatted string(contract name, event name, function name and variable name) * Handles tricky case where address is 0x * Use find_nodes_by_address method in hexify function

* Add DeployAddressMapper class to manage deployed contract address mappings with predefined mappings such as HEVM and SVM * Update get_contract_mapping_info_by_bytecode method to finding by bytecode suffix * Add deployed contract name lookup logic in render_trace function * Update rendered_calldata, hexify function and find_nodes_by_address method to supprot contract name parameter for searching node in specific contract

src/halmos/__main__.py

pillip · 2024-06-11T04:00:53Z

src/halmos/mapper.py

+    nodes: List[AstNode]
+
+
+class SingletonMeta(type):


a metaclass for implementing the Singleton pattern

pillip · 2024-06-11T04:02:42Z

src/halmos/utils.py

@@ -313,23 +316,25 @@ def decode_hex(hexstring: str) -> Optional[bytes]:
        return None


-def hexify(x):
+def hexify(x, contract_name: str = None):


By setting the default value of contract_name to None, existing usage of this function can use without modification

src/halmos/mapper.py

karmacoma-eth · 2024-07-15T23:29:29Z

this looks great to me, thanks @pillip!

Co-authored-by: karmacoma-eth <[email protected]> Co-authored-by: karmacoma <[email protected]>

Co-authored-by: karmacoma <[email protected]>

daejunpark

amazing, thanks for the contribution! i left a couple of comments.

src/halmos/__main__.py

tests/test_mapper.py

daejunpark · 2024-07-16T19:40:24Z

src/halmos/mapper.py

+        return cls._instances[cls]
+
+
+class Mapper(metaclass=SingletonMeta):


although i prefer avoiding non-constant global objects, i understand that it's too combersome to refer to this inside hexify() without a global reference. also, this should work with multiple tests, even with --test-parallel, since this Mapper class is fully initialized during the build-out parsing phase, and never updated during test execution later.

perhaps we can add a comment to clarify this.

I think this makes sense, it is logically a global object and it is immutable-like (after the parsing phase). I'm not too worried about enforcing the immutability here, a comment should be fine

daejunpark · 2024-07-16T19:49:30Z

src/halmos/mapper.py

+        # }
+
+        for contract_mapping_info in self._contracts.values():
+            if contract_mapping_info.bytecode.endswith(bytecode):


could you please elaborate on why endswith is used here? is it because contract_mapping_info.bytecode is a contract creation (or init) bytecode, and bytecode is a runtime bytecode? if so, i think this may not work for a constructor with non-empty arguments, where the init bytecode is structured as: <contract-creation-preamble> + <runtime-bytecode> + <constructor-arguments>. what do you think? cc: @karmacoma-eth

daejunpark · 2024-07-16T20:00:22Z

src/halmos/mapper.py

+    node_type: str
+    id: int
+    name: str
+    address: str


naming: precisely speaking, this is not an address, but a selector (4-byte signature) for functions, events, or errors.

clarifying this or renaming it would be great.

daejunpark · 2024-07-16T20:18:45Z

src/halmos/mapper.py

+        return result.strip() if result != "" and address != "0x" else address
+
+
+class DeployAddressMapper(metaclass=SingletonMeta):


i'm concerned about DeployAddressMapper being a singleton object. unlike Mapper which is per project, DeployAddressMapper is per test. sharing a singleton across multiple tests don't seem like a good practice to me. also, i don't think this would would work with --test-parallel, due to potential race conditions. what do you think? cc: @karmacoma-eth

good catch, I don't think DeployAddressMapper should be a singleton (or it should be scoped to a single test context).

It seems to currently work with --test-parallel because it is not updated during the test run, it is only updated lazily in render_trace (so from the main thread). This likely means that values from a test can "leak" to another thread

little repro:

contract A {} contract Test82 is Test, SymTest { function setUp() public { console2.log("Test82.setUp"); } function test_DeployMapperLeak1_double_deploy() external { A a = new A(); assert(address(a) != address(b)); } function test_DeployMapperLeak2_deploys_nothing() external { vm.deal(address(this), 1 ether); payable(address(0xaaaa0002)).transfer(1 ether); } }

if deploys_nothing runs first, it has the expected trace (0xaaaa0002 is a naked address, not an A)

Trace: CALL Test82::test_DeployMapperLeak2_deploys_nothing CALL HEVM_ADDRESS::0xc88a5e6d00000000000000000000000000000000000000000000000000000000aaaa00010000000000000000000000000000000000000000000000000de0b6b3a7640000 ↩ 0x CALL 0xaaaa0002::0x (value: 1000000000000000000) ↩ f_ret_256(call_exit_code_02()) ↩ REVERT f_ret_256(call_exit_code_02()) (error: Revert())

If double_deploy runs first, the DeployAddressMapper is now polluted and the trace for deploys_nothing wrongly indicates that eth was transferred to an A instance:

Trace: CALL Test82::test_DeployMapperLeak2_deploys_nothing CALL HEVM_ADDRESS::0xc88a5e6d00000000000000000000000000000000000000000000000000000000aaaa00010000000000000000000000000000000000000000000000000de0b6b3a7640000 ↩ 0x CALL A::0x (value: 1000000000000000000) # wrong label here ↩ f_ret_256(call_exit_code_02()) ↩ STOP 0x

thanks for further clarification, karma!

if it is nontrivial to fix this, i'm ok with adding a todo comment, and opening a separate pr to fix it later.

indeed, let's merge as-is and fix up later. I wanted to try a quick fix by introducing scopes for the singletons, but it's trickier than I thought

Co-authored-by: Daejun Park <[email protected]>

daejunpark

left todo notes for further improvements

pillip added 5 commits June 8, 2024 10:39

Add: Prepend 0x to node address

10aae39

* Update _get_node_info method in Mapper classe to prepend 0x to the node address for facilitating trace comparisons

pillip commented Jun 11, 2024

View reviewed changes

src/halmos/__main__.py Show resolved Hide resolved

pillip commented Jun 11, 2024

View reviewed changes

karmacoma-eth reviewed Jul 15, 2024

View reviewed changes

src/halmos/mapper.py Outdated Show resolved Hide resolved

karmacoma-eth reviewed Jul 15, 2024

View reviewed changes

src/halmos/mapper.py Show resolved Hide resolved

karmacoma-eth and others added 4 commits July 15, 2024 16:29

Merge branch 'main' into feature/a16z#244-convert-hex-to-readable

e465267

Update src/halmos/__main__.py

4d1e1ba

Co-authored-by: karmacoma-eth <[email protected]> Co-authored-by: karmacoma <[email protected]>

Fix: typo contarct -> contract

e502146

Co-authored-by: karmacoma <[email protected]>

Add: TODO comment

0611dd4

daejunpark reviewed Jul 16, 2024

View reviewed changes

karmacoma-eth and others added 3 commits July 16, 2024 14:00

Update src/halmos/__main__.py

56d60cb

Co-authored-by: Daejun Park <[email protected]>

Update tests/test_mapper.py

9863c86

Co-authored-by: Daejun Park <[email protected]>

fix last typo

70951b4

karmacoma-eth approved these changes Jul 17, 2024

View reviewed changes

add more comments and todos

8465b3e

daejunpark approved these changes Jul 17, 2024

View reviewed changes

daejunpark merged commit 7ba5a74 into a16z:main Jul 17, 2024
52 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Feature/#244] Parse symbols from build to print readable traces #309

[Feature/#244] Parse symbols from build to print readable traces #309

pillip commented Jun 11, 2024 •

edited

Loading

pillip Jun 11, 2024

pillip Jun 11, 2024

karmacoma-eth commented Jul 15, 2024

daejunpark left a comment

daejunpark Jul 16, 2024

karmacoma-eth Jul 16, 2024

daejunpark Jul 16, 2024

daejunpark Jul 16, 2024

daejunpark Jul 16, 2024

karmacoma-eth Jul 16, 2024

karmacoma-eth Jul 16, 2024

daejunpark Jul 16, 2024

karmacoma-eth Jul 17, 2024

daejunpark left a comment

		return cls._instances[cls]


		class Mapper(metaclass=SingletonMeta):

		return result.strip() if result != "" and address != "0x" else address


		class DeployAddressMapper(metaclass=SingletonMeta):

[Feature/#244] Parse symbols from build to print readable traces #309

[Feature/#244] Parse symbols from build to print readable traces #309

Conversation

pillip commented Jun 11, 2024 • edited Loading

Change Type

Description

Related Issues

Changes

Tests

Screenshot

Choose a reason for hiding this comment

Choose a reason for hiding this comment

karmacoma-eth commented Jul 15, 2024

daejunpark left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

daejunpark left a comment

Choose a reason for hiding this comment

pillip commented Jun 11, 2024 •

edited

Loading