Cleanup asserts and unstructured throws in builtin_functions

[hannes-steffenhagen-diffblue]

Marked as WIP because we'll change how we add exception types in a bit, the main part of the PR is reviewable as is.

• Each commit message has a non-empty body, explaining why the change was made.
• My contribution is formatted in line with CODING_STANDARD.md.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[allredj]

Passed Diffblue compatibility checks (cbmc commit: 9a3a93c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85179797

[tautschnig]

@hannes-steffenhagen-diffblue I'll apologise upfront for picking you up on this, but you may have made a somewhat brave statement:

[...] main part of the PR is reviewable as is.

Err, no. It's actually not. The commit message is not sufficiently informative to even tell me what I should be looking for in this change. So I started looking at the actual diff, and find a whitespace change at the very top - so is this going to be a formatting-only commit? Apparently not, as the further changes tell.

#2973 was proposed and merged to help us get the number of (open) PRs under control by making sure that PRs are in a state that enables quick "open PR" -> "review" -> "merge" turnarounds. I have re-added the template to this PR's description, and was only able to tick a single box. There are very reasonable cases where we need to create PRs that do not tick all the boxes, for example as a basis for discussion, or to announce some work in progress. This may even be such a case. But even in those cases, sufficient context needs to be available to enable such discussion or make clear what work is in progress.

Spending five extra minutes on good commit messages would be appreciated. It would appreciated very very much indeed.

[hannes-steffenhagen-diffblue]

@tautschnig Not a review request as such (as the PR is currently still not in a state where you'd consider it reviewable according to the standards we've set), but just a request for clarification/discussion.

In #2970 @kroening said the errors there are user caused/facing errors and argued they should therefore be treated as exceptions. You argued that all of them should have been detected prior to that stage, and therefore they should be invariants at that point. Before going ahead with further changes I'd like to clarify which approach is preferred here now.

[tautschnig]

I think we should have test cases with input programs violating each of the constraints tested here and make sure that none of them can get past the front-end. @NlightNFotis just went through this exercise in #3055. Once we are confident (by way of having tests for all the cases) the use of DATA_INVARIANT should be safe.

[hannes-steffenhagen-diffblue]

@tautschnig So @xbauch has done some investigation and we currently have lots of tests showing that pretty much all the "error" conditions in this file can in fact be reached (i.e. are not checked for in the frontend right now).

We were planning to do some work on the frontend anyway, so I suggest we park this for now and use the invariant version instead as soon as we are sure that these error conditions can't be reached anymore.

[tautschnig]

So @xbauch has done some investigation and we currently have lots of tests showing that pretty much all the "error" conditions in this file can in fact be reached (i.e. are not checked for in the frontend right now).

Excellent work! Would you mind putting together a PR that includes all those as regression tests? I'd say that would be the first step towards moving this PR forward at some future date.

[chrisr-diffblue]

@tautschnig All these regression tests will indeed make it into one or more PRs as we progress with additional front-end checks. @danpoe - you may also want to sync up with @xbauch regarding those tests too.

[danpoe]

@chrisr-diffblue The code that this PR touches is actually for converting the parsing result to a goto program. It would thus run before the additional well-formedness checks on the goto model.

[tautschnig]

@hannes-steffenhagen-diffblue This seemed like a useful piece of work, what's the rationale for abandoning this?