Conversation
| @@ -29,6 +30,7 @@ pub struct Encoder<InstructionsType> { | |||
| ssa_tracker: SSATracker, | |||
| output: Vec<SMTStatement>, | |||
| interpreter: InstructionsType, | |||
There was a problem hiding this comment.
We probably want to change this name now.
| "calldatacopy" => panic!("Builtin {} not implemented", builtin.name), // TODO | ||
| "codesize" => single_return(evm_context::codesize(ssa).into()), | ||
| "codecopy" => panic!("Builtin {} not implemented", builtin.name), // TODO | ||
| "codecopy" => vec![], //panic!("Builtin {} not implemented", builtin.name), // TODO |
There was a problem hiding this comment.
Shouldn't this and extcodecopy havoc memory?
There was a problem hiding this comment.
Yes, this is just to prevent the system from crashing on my example.
|
This now uses the evaluator to determine if some branches cannot be reached at all (and then it does not encode them). This is a trace of the encoded opcodes filtered to mstore, datacopy, create, sload, sstore and call, executed on two transactions: First a call to "setUp()" and then "proveA()" (i.e. calldata is set accordingly). You can see that it does not encode any of the panics in the abi decoder and properly re-retrieves the address of the contract under test from storage: |
|
Got this working now without the hack: |
718e6f7 to
97486c6
Compare
7859944 to
13f6b19
Compare
No description provided.