Requirement redundancies: Approximation of explanation via invariants

[Paswalt]

Pea2Boogie is capable of analyzing a set of requirements for the property of redundancy. In order to better explain a redundancy, we work on post-processing steps in an attempt to extract a set of requirements that are directly involved in the redundancy, a so-called redundancy set. Trace Abstraction (Automizer) offers invariants for the locations of ICFGs that already act as a first good approximation in many cases. For this purpose the following changes have been implemented:

ReqCheckRedundancyResult.java

A new result class ReqCheckRedundancyResult has been added to the results of Pea2Boogie. The result simply reports the redundancy of a given requirement and additionally, outputs the approximation that was computed. A static method inside of it does a simple (and not yet bulletproof) matching on a given invariant which is represented by a string. In the future, functionality like that can be put into a post-processing class that maybe also works in the VerificationResultTransformer class.

InvariantResult.java

For this change, I want to ask especially for the approval of @maul-esel
The InvariantResults were extended by a method to check the boolean field mIsLoopLocation. This can be useful when distinguishing between loop locations, and e.g., pre-error locations that we need for a better approximation. However, if in the future more than just loop/pre-error location invariants can be created, then a better approach is needed in order to distinguish between the different locations, rather than just through a binary decision (which stems from the fact that currently, with my changes and for our purpose, we can assume an InvariantResult to either correspond to a loop location or a pre-error location)

VerificationResultTransformer.java

The VerificationResultTransformer has been extended to also handle incoming InvariantResults that trace abstraction delivers. Loop invariants are just returned. Location invariants are pre-processed in the scope of a new if-statement that adds specific behavior in case of a redundancy spec, similar to the case of rt-inconsistency above it. If we check a requirement for redundancy and an invariant result is present. The creation of location invariants are implemented through a hack in the following explanation.

FloydHoareUtils.java

Because this is an area in which @maul-esel works (from what I noticed during my time working here) I want to ask specifically for his approval or ideas for a change. If I should add someone else as a reviewer just let me know!

I am very certain that this is not an acceptable hack and needs a better solution. This is only a temporary workaround so I can see results for my thesis. However, this hack assumes that there is only one pre-error location, i.e., one direct predecessor location in the ICFG for all error locations. This assumption is true for our redundancy checks but of course not true in general. Hence, I think one could add an extraction similar to loop invariants, just for all pre-error locations of an ICFG. Maybe @maul-esel has an idea? For now, the hack works out fine. Overall, the results of the approximations obtained by the location invariants have been rather great.

Additional remarks

This implementation works only under the following settings:

• Automizer has to run one cegar loop per error location
• Automizer needs to compute Hoare annotations for all locations (otherwise, the more detailed redundancy results will not be computed). This is expensive but one could also change the code via a setting to decide whether loop or location invariants should be used for the first approximation, as I assume that the former is more efficient than the latter.

Example of one specific output:
- ReqCheckRedundancyResult [Line: -1]: Requirement ID_007 is redundant
Extracted redundancy set for ID_007: [ID_003, ID_012, ID_000, ID_007] derived by location invariant: (Omitted for brevity)

I am looking forward to hear your feedback in order to improve, as I only started delving into ULTIMATE very recently! Thank you! Again, if certain people are missing as reviewers just let me know!

[maul-esel]

I've taken a look and left some small comments.

I hope to find some time in the next 2-3 weeks to implement some changes related to this, which are required for a different project but might also help here:

• More options for the locations at which the Hoare annotation is computed. We need (combinations of): loop heads, (C) labels, initial and final locations of procedures, predecessors of error locations
• Analogously, settings for the locations at which InvariantResults are produced.
• Backtranslation of invariants (and contracts) to data structures instead of strings. We need this to properly backtranslate contracts; but it would probably also help here as one can actually look at the Boogie expression data structures rather than doing regex-matching.

[maul-esel]

The easiest and cleanest solution to me seems to be to write a small method (here, or perhaps even in IcfgUtils) which collects all predecessors of error locations in a Set<IcfgLocation>, and then just add them to locsForLoopLocations (just like getPotentialCycleProgramPoints above).

At that point, we could then rename the set to sth like locsForInvariants ;-)

[Paswalt]

Agree, this seems like the best solution. In our setting, we only have a single unique predecessor for all error locations whose invariant we utilize. That means for each requirement check, we do something with the resulting invariant of said location. There's not really any combining involved as it is obscuring the results. However, I don't think that changing the code to handle all predecessors of error locations in general would change anything for our setting, so a cleaner implementation like that can easily be done while still being in agreement to our use case, at least if I understand correctly.

[Paswalt]

I have implemented a function in IcfgUtils that returns the predecessors of all error locations in b4ff0a6

After looking more into the code, the issue is more complicated than I initially thought, however. I try to explain in a short manner:

• In our redundancy analysis, assuming we look at N requirements, we have N error locations. While conceptually it is true that there is only one predecessor, in truth there is a predecessor for each of the N error locations. However, all of the predecessors will always have the same location invariant in our setting (we run one CEGAR per error location + the structure of our problem leads to this observation). Hence, we only need a single invariant result from any of these predecessor locations.

• The way it is coded now, we create an invariant result for all predecessors. What happens in Pea2Boogie is the following: we have a method that takes trace abstraction results and transforms them into our desired results. (Now, if we check the redundancy of let's say a requirement called r1 with a total of N = 1000 requirements, and it turns out that r1 is indeed redundant, trace abstraction will throw 1000 location invariant results for the predecessors of the error locations into this method. However, all of them will have the same location invariant, which we only want to receive once to output it.

  ultimate/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/VerificationResultTransformer.java

  Line 130 in c80803b

  public IResult convertTraceAbstractionResult(final IResult result) {

  ultimate/trunk/source/PEAtoBoogie/src/de/uni_freiburg/informatik/ultimate/pea2boogie/PEAtoBoogieObserver.java

  Line 99 in c80803b

  final UnaryOperator<IResult> resultTransformer = reporter::convertTraceAbstractionResult;

• To circumvent the issue, I added a temporary set into the VerificationResultTransformer until I can think of a better way to handle this. This way the same location invariant is not output N times but only once per requirement that is redundant. Though, the issue remains as all of the 1000 invariant results still enter the method per redundant requirement, and each time 999 are then rejected which is just a waste and not acceptable if the possibility exists to just create one for our use case. In order to think of a better solution I have the following questions:

1. Would it be possible to have settings for the invariants one wants to create?
2. Is it possible to check the settings of a project in a different project?
3. Do you maybe have an idea how we could fit the need of the use case described?

[maul-esel]

1. I'm planning to add something like this. We should discuss your use case in more detail (preferably in person) so we can figure out how to best design such settings.
2. We should not read settings of other projects.
3. If I understand correctly, you start one CEGAR loop per error location, and you always want the invariant at the predecessor of that particular error location that the CEGAR loop was started for? I think this is possible as follows:
   • In FloydHoareUtils::createInvariantResults you have access to the checked specification as spec = annotation.getSpecification()
   • From this specification, you should be able to identify which error location's unreachability the CEGAR loop has proven. Just filter the error locations by spec::isFinalState. Have a look at FloydHoareUtils::getCheckedSpecifications for an example.

[Paswalt]

Thanks, that worked, see 8aa2980

I left the new function in IcfgUtils still there in case it is useful in the future. But if the argument that it's non-usage at the moment makes it superfluous, I can also still remove it. This current version now perfectly matches what I wanted.

In summary, I think in the future a setting for the predecessors of the locations obtained via the spec through isFinalState would be helpful for our purpose. Thank you both so much for your help!

[Paswalt]

I've taken a look and left some small comments.

I hope to find some time in the next 2-3 weeks to implement some changes related to this, which are required for a different project but might also help here:

* More options for the locations at which the Hoare annotation is computed. We need (combinations of): loop heads, (C) labels, initial and final locations of procedures, predecessors of error locations

* Analogously, settings for the locations at which `InvariantResult`s are produced.

* Backtranslation of invariants (and contracts) to data structures instead of strings. We need this to properly backtranslate contracts; but it would probably also help here as one can actually look at the Boogie expression data structures rather than doing regex-matching.

Thank you very much! Some of these issues (Especially the ugly string matching) has been on my mind already too, but I wasn't sure what code I can touch and what you already planned to change anyways, it's good that I now know, thank you.

[Paswalt]

Using a LinkedHashSet here to keep the order of

1. Loop invariant results first
2. All other invariant results + their potential use inside a project second