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.
| 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.
| 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.
what do you mean maybe?
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.
I think it should even be bvuge(length, 4)
| @@ -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.
Doesn't this encode "reachable"? We should really take care to negate our terms at the right time...
| @@ -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.
Panic(uint)?
I mean it's nothing solc specific...
There was a problem hiding this comment.
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.
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.
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