-
Notifications
You must be signed in to change notification settings - Fork 5
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
Store revert data. #98
Conversation
wdym |
Sure but what do you store in the signature if the length is 2 or 8? |
Not really interested in that scenario for now, only in solc panics which always have length 36 |
0455e51
to
dadbbea
Compare
Currently this test is caught properly with {
function panic_error_0x11() {
mstore(0, 35408467139433450592217433187231851964531694900788300625387963629091585785856)
mstore(4, 0x11)
revert(0, 0x24)
}
panic_error_0x11()
} |
dadbbea
to
a778842
Compare
I made it the main binary default's behavior to look for solc panics, I think that's more relevant than generic reverts. That's also what hevm does |
pub fn revert(input: MemoryRange, ssa: &mut SSATracker) -> Vec<SMTStatement> { | ||
let sig = smt::ite( | ||
smt::eq(input.length.clone(), 0x24), | ||
mload4(0.into(), ssa), |
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.
mload4(0.into(), ssa), | |
mload4(offset, ssa), |
maybe
src/evm_context.rs
Outdated
mload4(0.into(), ssa), | ||
smt::literal_4_bytes(0), | ||
); | ||
let data = smt::ite(smt::eq(input.length, 0x24), mload(0x04.into(), ssa), 0); |
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.
let data = smt::ite(smt::eq(input.length, 0x24), mload(0x04.into(), ssa), 0); | |
let data = smt::ite(smt::eq(input.length, 0x24), mload(offset + 0x04.into(), ssa), 0); |
maybe
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.
what do you mean maybe?
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.
Changed this.
src/evm_context.rs
Outdated
assign_variable_if_executing_regularly(ssa, &context().revert_flag.identifier, 1.into()) | ||
pub fn revert(input: MemoryRange, ssa: &mut SSATracker) -> Vec<SMTStatement> { | ||
let sig = smt::ite( | ||
smt::eq(input.length.clone(), 0x24), |
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.
Why not bvuge
?
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 it should even be bvuge(length, 4)
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.
Yea true
@@ -405,16 +428,27 @@ pub fn encode_revert_unreachable(ssa: &mut SSATracker) -> SMTStatement { | |||
smt::assert(smt::neq(context().revert_flag.smt_var(ssa), 0)) | |||
} | |||
|
|||
pub fn encode_solc_panic_unreachable(ssa: &mut SSATracker) -> SMTStatement { |
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.
Doesn't this encode "reachable"? We should really take care to negate our terms at the right time...
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.
True
@@ -33,7 +33,7 @@ fn cli() -> Result<(), String> { | |||
|
|||
fn symbolic_subcommand() -> App<'static> { | |||
SubCommand::with_name("symbolic") | |||
.about("Symbolically execute Yul programs checking for revert reachability") | |||
.about("Symbolically execute Yul programs checking for reachability of solc panics") |
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.
Panic(uint)
?
I mean it's nothing solc specific...
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.
Well solc came up with it, it is still the main use case of that error. I think it's better to be explicit about it
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.
What I mean is that there is an EIP about how to interpret revert data and we could just be explicit about it.
src/evm_context.rs
Outdated
pub fn encode_solc_panic_unreachable(ssa: &mut SSATracker) -> SMTStatement { | ||
smt::assert(smt::and_vec(vec![ | ||
smt::neq(context().revert_flag.smt_var(ssa), 0), | ||
smt::neq(context().revert_data_32.smt_var(ssa), 0), |
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.
This line should actually be removed. zero data is still a valid panic.
Added a test. Merging. |
Ahhh @chriseth i still had a bunch of fixes and tests for this |
Fixes #83