Move existing type validation checks to new framework

[danpoe]

This removes the validate_type() functions and moves the checks into a new static method
check() of the corresponding type.

• 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).
• n/a 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]

This PR failed Diffblue compatibility checks (cbmc commit: d297f66).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87671157
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[allredj]

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

[martin-cs]

As discussed elsewhere I don't think command-line options are needed for any tool apart from goto-instrument and that only needs one. We should validate on loading (with invariants) and then give the user a way of checking them explicitly via goto-instrument.

[kroening]

1. I still think you should not cast before the check -- you can fix that by making the check methods static
2. The code in validate.h is only used in one place -- when you validate. However, it's included basically everywhere, incurring compile-time cost very globally. The include should be only included where actually used.

[danpoe]

1. Yes, we can potentially make the methods static. The thing I wanted to avoid initially is having to use the generic accessors op0(), op1(), etc. when implementing the checks. When we're just checking the number of operands it doesn't matter but for more comprehensive checks it could make for hard to read code. In any case, could you briefly explain what the issue with first doing the cast is?

2. Yes, that should be fixed.

[kroening]

On 1: yes, using .op0() etc. bugs me as well. The plan is to make these protected on exprt, and only allow them on binary_exprt etc., and those that inherit from these classes.

I would recommend the following idiom:
a) The first step is to check the number of operands, say like this:

  DATA_INVARIANT(
    expr.operands().size()==3,
    "Transition systems must have three operands");

b) Then check any subsequent conditions of these operands, using a static cast to unary_exprt, binary_exprt, ternary_exprt, etc., say like this:

  DATA_INVARIANT(static_cast<const ternary_exprt &>(expr).op0().type().id()==ID_bool, "blah...");

After these are done, the type invariants are checked, it's safe to cast to the type!

[danpoe]

Ok, I'll then turn the methods like check() into static member functions that take exprt.

[allredj]

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 35691f5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90557096
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: fef7925).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91092694

[tautschnig]

Shouldn't this get a corresponding check call?

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: f2dfd2e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92381958