Distinguishing explicit and implicit throws

[wuestholz]

From what I can tell Solidity currently translates explicit, user-provided throw statements just like implicit ones (e.g., for division-by-zero or other runtime exceptions).

It would be nice if one were able to distinguish these to cases by looking at the resulting EVM byte code. For instance, a failing implicit throw usually constitutes an error in the contract. On the other hand, an implicit one is often used for parameter validation (i.e., a precondition) and usually the client contact (i.e., caller) is to blame (at least if the exception it is not properly dealt with).

Would it be possible to use different error tags for these two cases? Or is there some other way to tell them apart?

[chriseth]

We are planning, especially for formal verification, to use different revert mechanisms for "wanted" and "unwanted" situations. What would your exact use-case be here?

[wuestholz]

@chriseth Great! This is precisely the use case I'm interested in. I'm working on a formal analysis for smart contracts and without this it is difficult to tell which errors should be reported to a developer that's using the analyzer.

I assume that you agree that all the "implicit throws" would constitute "unwanted" situations, comparable to runtime errors. On the other hand, for "explicit throws" it's more difficult to tell if they are wanted or unwanted. I would argue that ones that essentially express preconditions of a procedure should only be reported as errors in clients that call the procedure, comparable to a precondition violation.

Now, a user might also want to express assertions explicitly and I would consider violations of those to be "unwanted". I don't think Solidity supports assert-statements at the moment, but if they would be added they should be treated much like other runtime errors. Do you agree?

I haven't looked at enough Solidity code out there, but I haven't seen explicit throws that didn't essentially express preconditions or assume-statements. Can you confirm this?

[chriseth]

@pirapira we already talked about this, do you remember what our conclusions were? Did we create an issue somewhere?

[pirapira]

@chriseth our conclusion was to use an invalid opcode for this purpose.

[pirapira]

#1130, that is.

[wuestholz]

@chriseth @pirapira Thanks for the pointer! In that case I would argue that implicit assertions (e.g., division-by-zero) should also be translated as invalid opcodes, just like explicit assertions that may be added to the language in the future. Do you agree?

[pirapira]

@wuestholz that makes sense.

[wuestholz]

@pirapira @chriseth Great! Please let me know if there is something I can help with to implement this change.

[chriseth]

@wuestholz if you want to do it, then please go ahead. We need a new INVALID opcode with number 0xef in Instructions.cpp and then just replace the jumpToErrorTag calls in the code generator by m_context << Instruction::INVALID.
Having said that, I would like to clarify with the client developers whether this invalid opcode is the invalid opcode we want.

[wuestholz]

@chriseth Thank you for the pointers. I have tried to address this issue in the following PR: #1598. It would be great if you could have a look.