Convert throws and asserts to INVARIANTs for goto_convert.cpp #2814
Conversation
apaschos
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
I would like to apologise in advance for asking for a bit more work - this sort of cleanup is really important, but just does turn up a number of places where code has been left unmaintained for a while. And we need to make sure all such changes are accompanied by tests -we must not end up in a situation where invariants in this bit of code can be triggered by user input already having passed successfully earlier stages. (Those invariants may of course be triggered by internal code doing stupid things - that's what they are supposed to guard against.)
| DATA_INVARIANT( | ||
| l_it != targets.labels.end(), | ||
| i.code.find_source_location().as_string() + ": goto label '" + | ||
| id2string(goto_label) + "' not found"); |
There was a problem hiding this comment.
May I ask for additional tests to be included to make sure the language front-end actually catches these? For this particular example, I just convinced myself by using
int main()
{
goto x;
return 0;
}
as a test. Such a test would go in the regression/ansi-c/ folder with the expectation that it produces a front-end provided, semi-friendly error message (it currently does).
I am saying this as it needs to be made sure that such invariants cannot be triggered by input coming in via the regular parser.
There was a problem hiding this comment.
At least this one is now checked by the ansi-c/c_typecheck_base. I guess the only way to trigger this now is to supply an incorrect goto program.
src/goto-programs/goto_convert.cpp
Outdated
| INVARIANT( | ||
| false, | ||
| i.code.find_source_location().as_string() + | ||
| ": finish_gotos: unexpected goto"); |
There was a problem hiding this comment.
I would just have used UNREACHABLE() here.
There was a problem hiding this comment.
I had it as UNREACHABLE initially. The intention was to keep the message.
There was a problem hiding this comment.
Ok, no big deal - but I don't think the error message is particularly helpful to understand what may have gone wrong anyway (not your fault, it just never was helpful).
src/goto-programs/goto_convert.cpp
Outdated
| assert(destination.id()==ID_dereference); | ||
| assert(destination.operands().size()==1); | ||
| DATA_INVARIANT( | ||
| destination.id() != ID_dereference, "dereference ID not allowed here"); |
There was a problem hiding this comment.
That's the opposite of what the original assert said! Really, I'd suggest to rewrite a bunch of lines here to: const exprt pointer = to_dereference_expr(i.code.op0()).pointer(); (the copy is intentional, i.code is replaced later on).
| DATA_INVARIANT( | ||
| code.operands().size() == 1, | ||
| code.find_source_location().as_string() + | ||
| ": label statement expected to have one operand"); |
There was a problem hiding this comment.
I would dare to drop this entirely, a code_labelt is guaranteed to have exactly one operand.
There was a problem hiding this comment.
Yes, but "data structure X is guaranteed to have property Y" is exactly the kind of thing DATA_INVARIANT is there for.
| DATA_INVARIANT( | ||
| lb.has_value() && ub.has_value(), | ||
| code.find_source_location().as_string() + | ||
| ": GCC's switch-case-range statement requires constant bounds"); |
There was a problem hiding this comment.
Again, please add a test (possibly copying from one of regression/cbmc/gcc_switch_case_range*) to make sure the language front-end has caught this already.
| } | ||
| DATA_INVARIANT( | ||
| targets.continue_set, | ||
| code.find_source_location().as_string() + ": continue without target"); |
There was a problem hiding this comment.
Use a test similar to the one I proposed for break above.
| DATA_INVARIANT( | ||
| code.operands().size() == 3, | ||
| code.find_source_location().as_string() + | ||
| ": ifthenelse takes three operands"); |
There was a problem hiding this comment.
Should be covered by checks in std_code.h.
|
|
||
| assert(code.then_case().is_not_nil()); | ||
| DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body"); |
There was a problem hiding this comment.
Should be covered by checks in std_code.h.
| @@ -1821,7 +1766,7 @@ void goto_convertt::generate_conditional_branch( | |||
| { | |||
| if(guard.id()==ID_not) | |||
| { | |||
| assert(guard.operands().size()==1); | |||
| PRECONDITION(guard.operands().size() == 1); | |||
There was a problem hiding this comment.
I would use to_not_expr (and change guard.op0() to use .op())
| if(s_it==symbol_table.symbols.end()) | ||
| throw "failed to find main symbol"; | ||
| DATA_INVARIANT( | ||
| s_it != symbol_table.symbols.end(), "failed to find main symbol"); |
There was a problem hiding this comment.
Is this code ever called? The hardcoded "main" above makes me think this must be removed as quickly as possible.
| } | ||
| DATA_INVARIANT( | ||
| l_it != targets.labels.end(), | ||
| i.code.find_source_location().as_string() + ": goto label '" + |
There was a problem hiding this comment.
Invariant messages should describe why the invariant holds, not what happened when it was violated - they are meant for source code documentation, not for reporting errors. If this is something that can be triggered by e.g. incorrect input source code it should not be an invariant at all (or more precisely, it is in fact not an invariant) but rather an exception. This applies to most of the other changes in here as well.
Arguably most of these things should be invariants once we get past a type/sanity checking stage, but as @tautschnig says it's not obvious that this is in fact the case at the moment.
| assert(destination.id()==ID_dereference); | ||
| assert(destination.operands().size()==1); | ||
| DATA_INVARIANT( | ||
| destination.id() == ID_dereference, "dereference ID not allowed here"); |
There was a problem hiding this comment.
The message here seems to say the opposite of what's actually being asserted.
There was a problem hiding this comment.
to_dereference_expr should solve it nicely.
| assert(destination.operands().size()==1); | ||
| DATA_INVARIANT( | ||
| destination.id() == ID_dereference, "dereference ID not allowed here"); | ||
| DATA_INVARIANT(destination.operands().size() == 1, "expected 1 argument"); |
There was a problem hiding this comment.
Again, the important question here isn't that you expect one argument (that much can be seen from the condition) but why it is ok to expect one argument here.
There was a problem hiding this comment.
I know the message is obvious but the check is also obvious. The dereference expects 1 argument. There's no secret message.
| INVARIANT( | ||
| assertion.is_false(), | ||
| code.op0().find_source_location().as_string() + ": static assertion " + | ||
| id2string(get_string_constant(code.op1()))); |
There was a problem hiding this comment.
@tautschnig I agree that this should be checked by the frontend, but if it is checked by the frontend then it should be to OK to assert that this condition does indeed hold here.
| // we may wish to complain | ||
| } | ||
| INVARIANT( | ||
| assertion.is_false(), |
There was a problem hiding this comment.
The logic here is flipped compared to the previous version (should be !assertion.is_false())
| @@ -1218,7 +1187,7 @@ exprt goto_convertt::case_guard( | |||
| dest.move_to_operands(eq_expr); | |||
| } | |||
|
|
|||
| assert(!dest.operands().empty()); | |||
| CHECK_RETURN(!dest.operands().empty()); | |||
There was a problem hiding this comment.
Should arguably be PRECONDITION(!case_op.operands.empty()) + INVARIANT(dest.operands().size() == case_op.operands.size()).
| DATA_INVARIANT( | ||
| code.operands().empty() || code.operands().size() == 1, | ||
| code.find_source_location().as_string() + | ||
| ": return takes none or one operand"); |
There was a problem hiding this comment.
I think it's fine to have "redundant" invariant checks as long as the following code actually requires the condition holds.
|
Further development of this will continue in #2905 because the original repository is now defunct and I can't continue work on this PR. |
No description provided.