Report invariants enforced by vacuous requirements #675
Conversation
…iants that are silently enforced by vacuous requirements
| // Return a ReqCheckVacuousResult, i.e., a ReqCheckFailResult with additional | ||
| // VacuityAnnotation containing an invariant that might be enforced by the | ||
| // vacuous requirement. | ||
| VacuityAnnotation enforcedInv = VacuityAnnotation |
There was a problem hiding this comment.
Should be final -- do you have your save actions configured correctly?
| if (pnr > 0) { | ||
| for (int i = 0; i < phases.size(); i++) { | ||
| final PhaseBits bits = phases.get(i).getPhaseBits(); | ||
| if (bits == null || (bits.getActive() & 1 << pnr - 1) == 0) { | ||
| checkReached.add(genComparePhaseCounter(i, mSymbolTable.getPcName(aut), bl)); | ||
| } | ||
| // Store state invariants of PEA locations where max DC phase is not active. | ||
| if (bits.getActive() < (1 << pnr - 1)) { |
There was a problem hiding this comment.
If the mask 1 << pnr - 1 is now used multiple times, perhaps give it its own variable and a nice name. I am struggling a bit to understand what exactly the condition here is -- its weird for me to see a mask used as mask and as comparison.
| if (pnr > 0) { | ||
| for (int i = 0; i < phases.size(); i++) { | ||
| final PhaseBits bits = phases.get(i).getPhaseBits(); | ||
| if (bits == null || (bits.getActive() & 1 << pnr - 1) == 0) { | ||
| checkReached.add(genComparePhaseCounter(i, mSymbolTable.getPcName(aut), bl)); | ||
| } | ||
| // Store state invariants of PEA locations where max DC phase is not active. | ||
| if (bits.getActive() < (1 << pnr - 1)) { | ||
| enforcedInv.put(phases.get(i), phases.get(i).getStateInv()); |
There was a problem hiding this comment.
As phases.get(i) is now also used multiple times, it would be nice to have a separate var for it as well
| VacuityAnnotation enforcedInv = VacuityAnnotation | ||
| .getAnnotation(((BoogieIcfgLocation) element).getBoogieASTNode()); | ||
| return new ReqCheckVacuousResult<>(element, plugin, | ||
| enforcedInv.getInvariant().toString()); |
There was a problem hiding this comment.
It would be slightly cheaper to already check here if the invariant is different from CDD.TRUE and only then create the string, else use null.
| @@ -0,0 +1,58 @@ | |||
| /* | |||
| * Copyright (C) 2024 University of Freiburg | |||
There was a problem hiding this comment.
Please also add your name and email address if you create a new file.
| public String getLongDescription() { | ||
| final StringBuilder sb = new StringBuilder(); | ||
| sb.append(getShortDescription()); | ||
| if (mEnforcedInvariant != CDD.TRUE.toString()) { |
There was a problem hiding this comment.
Check for null instead of CDD.TRUE.toString(), and move stringbuilder into the if, e.g.:
if (mEnforcedInvariant != null) {
final StringBuilder sb = new StringBuilder();
sb.append(getShortDescription());
...
return sb...
else {
return getShortDescription();
}
| @@ -0,0 +1,61 @@ | |||
| /* | |||
| * Copyright (C) 2024 University of Freiburg | |||
| * | |||
This adds a ReqCheckVacuousResult to report invariants that are enforced by vacuous requirements.
A vacuous requirement enforces an invariant if there exists only one location in its PEA representation in which the maximal phase of its corresponding countertrace is not active.
Reporting such invariants may help to better understand vacuous results (e.g. as in #530) and their implications, as for example needed to approach #438.