Value-set analysis: templatise and virtualise to facilitate customisation

[smowton]

This provides sufficient hooks in value-set analysis, a CBMC core pointer-analysis, to permit downstream products such as the security analyser to create derivatives that share most of its logic.

VSA itself is currently unused, as revealed by the need to add support for DEAD statements before it can be used; this also adds unit tests to check its basic functionality has not broken in the meantime.

VSA is based on static_analysist and so will need to be ported to ait in the future if we wish to continue using it; however this should be orthogonal to permitting it to be customised like this.

[reuk]

In general public virtual methods in non-abstract classes are a code smell, as they have two many responsibilities. They specify both the public interface, and a customization point for derived classes (which is an implementation detail). Ideally, the two responsibilities should be decoupled by providing a private virtual method which is called by a public (non-virtual) method. Then, if interface requirements change, the interface can be adjusted independently of the implementation (and vice versa).

I'm particularly concerned about retroactively making this method virtual. Pre-existing clients which always expect this method to do the same thing could be broken when derived classes change its behavior.

[reuk]

Prefer to make these private if at all possible.

[smowton]

The virtual override points definitely need defer-to-base I'm afraid

[reuk]

Plz no camel snake case. ValueSet?

[thk123]

I don't think adopting a different naming convention is a good way of disambiguating it from the existing value_sett. Perhaps selected_value_sett? Perhaps there is a better term. value_set_domaint?

[reuk]

No leading underscores on identifiers.

[reuk]

Overridden methods calling base class methods is a code smell. It implies that the customization points have been chosen incorrectly. This should probably be refactored.

[reuk]

I think these methods are missing overrides too.

[reuk]

If this is never used it should probably be removed.

[smowton]

Shrug, that goes for the entire XML interface. I don't know who (if anyone) uses it and if they use this sometimes, so I'm leaving it alone.

[reuk]

More snake-camel case

[reuk]

Add a comment to make it clear that fall-through is desired.

[reuk]

Again, I find it extremely unlikely that these methods are already suitable customization points. It might be better to find a more focused group of custom behaviors which can be given private virtual interfaces, and called from these (still non-virtual) methods.

[martin-cs]

On Fri, 2017-09-22 at 13:26 +0000, Chris Smowton wrote: This provides sufficient hooks in value-set analysis, a CBMC core pointer-analysis, to permit downstream products such as the security analyser to create derivatives that share most of its logic.

Sounds good.

VSA itself is currently unused, as revealed by the need to add support for DEAD statements before it can be used; this also adds unit tests to check its basic functionality has not broken in the meantime.

I don't quite recall the history but it was either written for CBMC but we used a slightly different version or it was used in other tools; possibly Wolverine...

VSA is based on `static_analysist` and so will need to be ported to `ait` in the future if we wish to continue using it;

Yes; this was the last part of the "we should probably only have one general abstract interpretation framework".

however this should be orthogonal to permitting it to be customised like this.

Yes. There is also quite a bit of duplicate code in the various value analysis variants; if you are refactoring it might be worth having a look at that (the duplication was one of the motivations behind the variable precision domain stuff). Do be a little careful though because IIRC there are some subtle hacks in this code to handle C pointer weirdness. Longer term there may be a question over whether configurations of the variable precision domain might replace the functionality of pointer_analysis/ but even if it does, it will be a while before this code is removed. HTH

[thk123]

This looks good - just a few minor corrections. I also agree with @reuk that the interface could probably be cleaned up so the public methods aren't virtual. I will read up on Value Set Analysis so that I can validate that the tests covers suitable cases - but they look very clean!

[thk123]

Why swap this to a full include when forward declaration was sufficient?

[smowton]

value_set_analysist is a template specialisation now; class value_set_analysist won't work as the forward-decl will clash with the actual definition. There might be a way around this but I don't know it.

[thk123]

I don't think adopting a different naming convention is a good way of disambiguating it from the existing value_sett. Perhaps selected_value_sett? Perhaps there is a better term. value_set_domaint?

[thk123]

Nit: while in the area a range based for might be better here?

[smowton]

True, re: this and below though I'll stick to just moving the code without many changes and perhaps clean up later.

[thk123]

Nit: the formatting on this for loop is a bit hard to follow. You might consider using auto to get each statement on one line or at least aligning each statement

[thk123]

This seems like a weird place to introduce a typedef? If really needed in the header file outside of the class, perhaps put it above the class?

[thk123]

Could this go in the same folder as the test to avoid cluttering unit

[thk123]

Any reason not to do this REQUIRE immediately after initalize_goto_model?

[thk123]

The tests seem good. I'm tempted to say the methods that you don't provide a custom implementation for probably shouldn't be virtual

[thk123]

You might consider pulling this class out into a separate file with just the above documentation left in the test file since it isn't directly relevant to the test. Definitely not a requirement, so do disregard if you disagree.

[martin-cs]

Shrug, that goes for the entire XML interface. I don't know who (if anyone) uses it and if they use this sometimes, so I'm leaving it alone.

The XML interface was developed for a customer (I forget exactly who) and I think there are several people who use it. Any decision to depreciate it should be done across the whole code-base.

[smowton]

@reuk @thk123 all changes applied except as noted.

[thk123]

The code and tests look great, I would feel more conformable if someone who was already familiar with the behaviour of these analyses checked the tests were sufficient.

[thk123]

Still think looks a bit awkward to have this non-conforming to name convention (pointing out in case this isn't intentional, not to start a flame war 😛)

[smowton]

Changed names again to VST, believe everything is applied now

[reuk]

Make private, and provide a protected method which allows this to be called (but nothing else)

[reuk]

Should std::move the simplifier

[reuk]

Below...

[reuk]

You could use static constexpr const char * here and avoid the evil preprocessor

[smowton]

AFAIK I can't concatenate them as is done here, so I'd prefer to leave as-is

[reuk]

In general, if you are specifying interface requirements on a templated item, use non-member rather than member functions (i.e. read_reference_set(value_set, expr, dest, ns)). This allows pre-existing types to be used, without altering their definitions, as the template requirements can be fulfilled by providing external, non-member functions. If necessary, these can even be local to a translation unit, allowing template clients in different locations to use different implementations of these wrapper/interface functions.

[smowton]

Don't follow this, could I have an example?

[reuk]

Let's say I have a type that already exists - maybe it's a std::vector or something where we're not able to change the implementation. Now, if you were to use this type as your template parameter, you would probably find that it doesn't have the right member functions to satisfy the interface implicitly specified by the template class. The problem is that there's nothing you can do now - you can't modify the class definition to add the right methods.

If you use non-member functions inside your template, you have more flexibility to define appropriate implementations of these functions without modifying the original class. This also gives more flexibility when refactoring. At the moment, if you changed a method in one of your classes that's used as a VST, you would have to go and modify this template, too. However, if you use non-member functions you can just modify the non-member passthrough function to call the modified member function (one change), without having to make changes throughout the template class (potentially several changes).

This is about separating the general interface for a class (its member functions) from the specific interface required for a particular template class (non-member functions).

[smowton]

OK, done this this time. In general I think this sort of layer of indirection should be introduced on demand though, as the case where we need it is fairly unlikely (maybe 10% chance of needing this over the life of the code, considering the template parameters are internal code, and the cost of introducing the indirection scales with the size of the implied interface, not the number of subclasses already providing it.

[smowton]

Comments 1-3 done, 4 declined, 5 I don't understand, please give an example?

[smowton]

Change 5 now applied too.

[polgreen]

Hi,
It would be helpful if in future, when large-ish changes like this are introduced, the old api could be kept in develop in addition to the new one at least for a short time, please. Then people who depend on the existing api have a bit of time to alter their code to fit the new api, whilst still being able to rebase against develop to pull in other new changes.
Thanks!

[smowton]

1. Sorry, didn't think anybody was using this code except for goto-instrument.
2. What API break? value_set_analysist and value_sett should be exactly as-was
3. Daniel has requested this reverted, which will happen once CI has passed

[martin-cs]

On Mon, 2017-10-16 at 01:28 -0700, Chris Smowton wrote: 1. Sorry, didn't think anybody was using this code except for goto-instrument.

It should be used in symex and in the dependency graph / slicer at a minimum. As a generally point, we can't entirely assume that something is unused just because it is not used in the main CBMC repository. Also, where possible, introducing the new API, depreciating the old one and then removing it later is A Good Thing. See the ai.h / static_analysis.h divide.

[polgreen]

I'm using value_set_domaint, which has changed quite a bit. I've fixed my stuff now, just it would be nice if there's a bit of a period of overlap for future changes like this.

[smowton]

Ah ok, so would my writing typedef value_set_domaint templated_value_set_domaint<value_sett> have prevented problems, or were there further problems with value_set_domaint's internals?

[polgreen]

You would also need to keep the names of the functions within templated_value_set_domaint<value_sett> the same as the functions within value_set_domaint (e.g., get_value_set is now read_value_set, and a new get_value_set has been introduced)

[smowton]

Ah crap, sure, that was because the 4-operand and 3-operand versions of get_value_set were needlessly overloads, which led to awkwardness when subclassing value_sett as the 3-op version was hidden by overriding the 4-op one. I can make an alias instead. FWIW there isn't a new get_value_set, only the old 4-op version probably showing through where existing code expects the 3-op one. Again the cause was thinking value_set_domaint was a "private" implementation artefact of value_set_analysist.

In any case this is all now reverted per @kroening.

[smowton]

@polgreen made a replacement to this PR here: #1499

Since this broke your stuff the last time around, would you mind checking whether you can merge that PR into your cbmc branch without causing undue mayhem?

[polgreen]

That's great, thanks!