Templatize value-set analysis

[smowton]

A second attempt at #1413 -- see there for detailed description.

Differences vs. that PR:

• Name value_set_domaint retained as-is, and the templated version of the same class given a fresh name.
• Kept as similar as possible a file layout to the pre-existing code, to shrink the diff and make merge conflicts easier to resolve.

[smowton]

In comments on #1413 @polgreen confirms this is no longer a breaking change for her derived project. Would be good to find others willing to test it out if possible.

[smowton]

@tautschnig any opinion on this? It should be the same as #1413, which was accepted but then reverted for breaking outside projects, but slightly restructured to minimise churn.

[tautschnig]

What I struggle with in this PR is the number of non-essential changes that make it much harder to understand the key ingredients. (Whether the introduction of templates is the right thing to do is a different question that I'm a bit unsure to answer for any use of value_set_* should rather be abstained from given its poor performance and the use of deprecated static_analysist.)

[tautschnig]

I'm only starting to review this, so please forgive me if I'm asking a dumb question: is this renaming essential?

[smowton]

These were renamed because in an earlier version of this PR, the 4-arg version of get_value_set was virtual but the 3-arg version wasn't, which was annoying as you had to manually forward it in each derived class, hence renaming the overload out of the way. However since that has changed, I'll remove these.

[tautschnig]

Why would one want a different simplifier? What would it look like? What are the minimal requirements?

[smowton]

It simplifies an exprt & in place, like simplify. We use it to turn off the default simplifier's merging of identical struct types.

[tautschnig]

As above: why rename?

[tautschnig]

As much as I agree this is a slightly better name: is the renaming essential?

[smowton]

The case for this was: it's better to rename this and override the private function than to override the public apply_code, thus separating the customisation point (apply_code_rec) from the public interface (apply_code).

[tautschnig]

This is an unrelated change that would warrant a dedicated commit I'd say.

[tautschnig]

What's ambiguous about it? The signature appears to be the same?

[tautschnig]

As above.

[tautschnig]

A few answers to the "why" question would be appreciated.

[tautschnig]

No actual changes here?

[smowton]

Yeah, the existing code spilled over the 80-column boundary so I got linter complaints on moving the file like this.

[tautschnig]

Required?

[smowton]

As above.

[smowton]

@tautschnig removed the read_* renamings; replied to other comments with reasoning.

[smowton]

Also moved the "allow value_sett to handle DEAD if it wants to" change into a different commit.

[smowton]

@tautschnig any further objections?

[smowton]

@tautschnig ping

[tautschnig]

My apologies for the long delay, but I continue to struggle with this custom-simplifier thing. I find this really broken, as outlined in my comment.

[tautschnig]

That's removing the symptom rather than the root cause, I'd say. If Java objects need to be handled differently (which part of the code base requires this?), then the Java front-end needs to make sure this happens. We can't go across all the code base and build in special cases in each place.

[smowton]

It's really quite hard to solve this in general. The problem is that Java stub classes (ones we don't have bytecode for) have an unknown inheritance graph, so you can get apparently unrelated types like

struct A {
  int x;
};
struct B {
  int x;
};

But in truth they are parent and child, and therefore legal to cast between. After get_reference_set or similar have been applied this results in struct casts, like (struct A)dynamic_object1 (where dynamic_object1 has type B). Finally simplify_expr removes typecasts where the operand is base_type_eq the result type, which removes casts between like-shaped structs, and you get a value-set with types that don't match the type of the expression you queried.

Either every query needs to copy with producing potentially wrongly-typed outputs, or the cast needs to be retained.

Possibilities:
(1) simplify_expr was wrong to ever change the type of the expression it's simplifying. It should only eliminate typecasts that are actually redundant, in that they cast an operand to the exact same type.
(1.5) Don't change type when the struct type in question has type == ID_java (or type != ID_C ... ?) This is hard to check since struct tags lack the java:: prefix present in their symbol name. Add a new ID_symbol_name to struct_typet to ensure the ability to look them up in the symtab reliably?
(2) value_sett should re-add casts at the last stage of get_value_set so that querying e only ever returns expressions of matching type (with casts if necessary)
(3) Some users of simplify_expr want cast elimination like this and others don't. Add a flag like the existing simplify_expr_classt::do_simplify_if to customise what it is and isn't allowed to simplify. <-- the approach used here. I allowed customisation and only used the don't-eliminate-struct-casts option in the security product in case some part of goto-symex depends on this behaviour, or loses accuracy when it isn't present.
(4) value_sett::get_value_set should continue to return mixed-type value sets, and users should apply casts themselves.

Any preferences?

[tautschnig]

It seems that simplify_expr is possibly wrong here: it should not be removing type casts when those types aren't literally the same (i.e., comparison using == succeeds). That is, unless we forbid using == on typet and enforce using base_type_eq (which is semantic, but not syntactic equality). In the solver back end it may be safe to drop such casts, but this should not be done in any higher layer.

It should be a postcondition in simplify_expr that the final expression has literally the same type as the initial one.

@smowton I'm aware this is a fair bit of extra work, but one that is highly valuable for C code as well.

[smowton]

@tautschnig I tried just changing base_type_eq for ==; this mostly worked, but broke some string solver tests, which I presume depend on a disappearing typecast. Therefore I've removed the simplifier stuff from here and will keep it out of tree in the security product until I can figure out how to fix the string solver. I haven't tried the broader postcondition yet but I will soon.

[smowton]

@tautschnig I've added another commit documenting value_sett. I can split this off into a separate later PR if you like, but since it's ready, concerns the same code and doesn't cause any functional change I thought it might be appropriate to include here.

[tautschnig]

It seems c67dc8a needs some more work to make the doxygen checks pass?

[tautschnig]

Why is this marked private (yet virtual)?!

[smowton]

There's no base implementation for the subclass implementation to call, so no need to make it protected. Could make it so if you'd prefer subclasses to always call it in case it grows one, but any such base class behaviour could be directly implemented at the callsite.

[smowton]

@tautschnig Doxygen fixes applied