-
Notifications
You must be signed in to change notification settings - Fork 71
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
feat: nicer output #209
Conversation
There was a problem hiding this 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)})" |
There was a problem hiding this comment.
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) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
😍
src/halmos/cheatcodes.py
Outdated
info( | ||
f"Unsupported console function: selector = 0x{funsig:0>8x}, " | ||
f"calldata = {hexify(arg)}" | ||
) |
There was a problem hiding this comment.
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 |
There was a problem hiding this comment.
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)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
💪
src/halmos/utils.py
Outdated
""" | ||
if not is_bv_value(val): | ||
warn(f"{val} is not a bitvector value") | ||
return str(val) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
return str(val) | |
return hexify(val) |
else: # bytes32, bytes4, structs, etc. | ||
return hexify(val) | ||
|
||
|
There was a problem hiding this comment.
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
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
in 5b3c56f
src/halmos/cheatcodes.py
Outdated
funsig: int = int_of(extract_funsig(arg), "symbolic console function selector") | ||
|
||
if handler := console.handlers.get(funsig): | ||
return handler(arg) |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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
Includes a bunch of things:
Plus some internal reorganizing: