Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: nicer output #209

Merged
merged 10 commits into from
Oct 20, 2023
Merged

feat: nicer output #209

merged 10 commits into from
Oct 20, 2023

Conversation

karmacoma-eth
Copy link
Collaborator

Includes a bunch of things:

  • type based counterexample rendering (different rendering for uints, signed ints, address, bool, bytes, string, bytes32...)
  • console.log functions leverage the same type based rendering
  • includes a bunch of new console.log functions + tests
  • updates to latest halmos-cheatcode, implements the new cheatcodes (createInt, createInt256, createBytes4, createString) and add tests for these functions

Plus some internal reorganizing:

  • move utils-like functions from sevm.py to utils.py
  • move cheatcode and console.log handling logic from sevm.py to cheatcodes.py
  • switch to a lookup+handler based mechanism in console and halmos_cheat_code

Copy link
Collaborator

@daejunpark daejunpark left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

looks great! the refactoring is amazing! thank you so much!

my only comment is about handling potential exceptions in stringify.

else:
return f"prank({str(addr)})"
return f"prank({str(self.addr)})"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🙏

return handler(ex, arg)

error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}"
raise HalmosException(error_msg)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

😍

info(
f"Unsupported console function: selector = 0x{funsig:0>8x}, "
f"calldata = {hexify(arg)}"
)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

😍

@@ -1883,282 +1641,20 @@ def call_unknown() -> None:
ex.solver.add(exit_code_var != con(0))
ret = arg

# TODO: factor out cheatcode semantics
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

😍 🙏 👏

raise ValueError(x)
if bitsize == 256:
return x
return simplify(SignExt(256 - bitsize, x))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💪

"""
if not is_bv_value(val):
warn(f"{val} is not a bitvector value")
return str(val)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
return str(val)
return hexify(val)

else: # bytes32, bytes4, structs, etc.
return hexify(val)


Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i think we need to catch potential exceptions raised by the render functions here. even if is_bv_value(val) is true, the render functions could still raise an exception, when the type of val somehow differs from expected, e.g., .decode("utf-8") may fail in render_string(), or b.hex() may fail if b is not of type bytes.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

in 5b3c56f

funsig: int = int_of(extract_funsig(arg), "symbolic console function selector")

if handler := console.handlers.get(funsig):
return handler(arg)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

similar to stringify, i think we need to catch potential exceptions from the renter functions here, so that the execution can continue regardless of any logging errors.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you're right, added a test for it in 8b5b151:

Running 1 tests for test/Console.t.sol:ConsoleTest
console.handle: UnicodeDecodeError('utf-8', b'\xff', 0, 1, 'invalid start byte') with arg=0x4b5c4277000000000000000000000000000000000000000000000000000000000000004000000000000000000000000000000000000000000000000000000000000000a0000000000000000000000000000000000000000000000000000000000000002c74686973206973206120737472696e67207468617420776f6e2774206465636f646520746f207574662d383a00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001ff00000000000000000000000000000000000000000000000000000000000000
[PASS] check_log_undecodable_string() (paths: 1/1, time: 0.05s, bounds: [])
Symbolic test result: 1 passed; 0 failed; time: 0.05s

+ factor our console.py out of cheatcodes.py
+ catch and log exceptions in stringify and console.log
@karmacoma-eth karmacoma-eth enabled auto-merge (squash) October 20, 2023 22:46
@karmacoma-eth karmacoma-eth merged commit 4620b71 into main Oct 20, 2023
110 checks passed
@karmacoma-eth karmacoma-eth deleted the feat-nicer-output branch October 20, 2023 23:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants