RFC: Documenting and checking "normal form" properties of goto_models

[martin-cs]

Inspired by #6493 (comment) but a much longer standing problem:

• Various of the transformations and passes in CPROVER remove, normalise away or even introduce particular features. Examples include removing function pointers, removing returns, removing vectors, patching programs so that all functions have bodies, leaving the program needing an .update(), etc.
• Various parts of the code assume that these have been done and will break, sometimes silently or generate incorrect results, if they have not been.
• There is not one single "normal form" of goto_modelt, nor should their be as different parts of the code need different things.
• This is not really documented or at least not obviously so; there are comments deep inside various transforms that say things like "this assumes that X has been removed".
• These various properties are potentially orthogonal making a type-based solution tricky.

I've tried to come up with various approaches to this and #6493 (comment) makes be feel a bit better that @tautschnig hasn't cracked it either.

How about:

1. goto_modelt at least in it's in-memory form gets a struct that contains variables for each angle of 'normalisation'. I am unsure if they are boolean or need more complex settings like "unknown; might contain this", "definitely does contain", "definitely doesn't contain".
2. goto_modelt.validate should check these if they are set, throw an exception if they are incorrect (said there are no function pointer but there are) and set them if they are unknown (said there might be function pointers but there aren't).
3. Transforms and analyses passes could then add:

PRECONDITION(goto_modelt.validate());
PRECONDITION(goto_modelt.form.all_functions_have_bodies() == YES);

// ... code goes here ...

goto_modelt.form.set_has_function_pointers(NO);
POSTCONDITION(goto_modelt.validate());

4. This would both document and enforce the normalisation forms / transforms.

[feliperodri]

@diffblue/diffblue-opensource

[martin-cs]

Another example of program properties : literal back edge vs. topological back edge #7506

[TGWDB]

Note that #7771 may cover some of what what required here (I'm hesitant to call it a complete fix). Thoughts?