-
Notifications
You must be signed in to change notification settings - Fork 41
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Proof Refactoring #671
Proof Refactoring #671
Conversation
These changes allow computing Floyd/Hoare annotations for product automata of concurrent programs.
BasicCegarLoop should not refer to Floyd/Hoare proofs, let NwaCegarLoop handle this. Also, CEGAR loops refer directly to Hoare annotation states, not IcfgLocations.
Do not check the setting again, the caller should supply the appropriate states.
Also define their semantics in the class itself, rather than in some utility class.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The introduction of the new library for proofs looks great, at least for my knowledge on the subject. The new proof library has been created correctly. We just need to upgrade the Java version number in the Manifest.MF
file later when we finally migrate to Java 21. In addition, @danieldietsch has to adjust the sonar coverage configuration in the Maven pom.xml
under trunk/source/BA_MavenParentUltimate
so that the code coverage for the library can be reported properly.
trunk/source/Library-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/IProof.java
Outdated
Show resolved
Hide resolved
...s/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/HoareAnnotationComposer.java
Outdated
Show resolved
Hide resolved
.../src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/HoareAnnotationPositions.java
Show resolved
Hide resolved
...e/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java
Show resolved
Hide resolved
...ltimate/plugins/generator/traceabstractionconcurrent/TraceAbstractionConcurrentObserver.java
Outdated
Show resolved
Hide resolved
...ltimate/plugins/generator/traceabstractionconcurrent/TraceAbstractionConcurrentObserver.java
Outdated
Show resolved
Hide resolved
Removes the workaround introduced in 720a012, as proofs of different CEGAR loops are now stored separately in the ICFG. # Conflicts: # trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/NwaCegarLoop.java
Thanks for the reviews. I'll wait for the nightly test run; if no further issues occur I will merge this tomorrow. |
This is particularly useful if we create multiple proof objects for the same program and different (partial) specifications, to distinguish which proof objects relate to which specification.
Every procedure that exists in the IIcfg should have an exit location, even if that location is unreachable. This was not the case for the IIcfgs produced by the BlockEncodingV2 plugin. This commit fixes this bug, and introduces an assert statement after block encoding has finished to check if the produced IIcfg satisfies this invariant. Moreover, we add two sanity checks regarding the computation of procedure contracts, where the problem was discovered (the location of the ProcedureContractResult was null), such that similar issues are caught earlier in the future.
Fixing the tests required some changes:
While doing this, I also added a feature required e.g. in the context of requirements analysis: Each proof now also has an explicit description of the specification that it proves. This information is also added to |
# Conflicts: # trunk/source/InvariantSynthesis/src/de/uni_freiburg/informatik/ultimate/plugins/generator/invariantsynthesis/InvariantSynthesisStarter.java # trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/HoareAnnotation.java # trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/predicates/PredicateFactory.java # trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/HoareAnnotationWriter.java
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Review so far, I would read on, but feel free to merge anyways,
...eiburg/informatik/ultimate/plugins/generator/buchiautomizer/cegar/BuchiCegarLoopFactory.java
Show resolved
Hide resolved
...-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/FloydHoareMapping.java
Show resolved
Hide resolved
...Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/PrePostConditionSpecification.java
Outdated
Show resolved
Hide resolved
...Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/PrePostConditionSpecification.java
Show resolved
Hide resolved
...-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/FloydHoareMapping.java
Show resolved
Hide resolved
...Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/PrePostConditionSpecification.java
Show resolved
Hide resolved
...Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/PrePostConditionSpecification.java
Show resolved
Hide resolved
# Conflicts: # releaseScripts/website-config/frontend/config.js # trunk/source/WebsiteStatic/config/config.dist.js
…nted procedures This was previously done in HoareAnnotationChecker [1], the predecessor of IcfgFloydHoareValidityCheck previous to PR #671. The filter was missed in the PR, and not discovered so far because of another bug in IcfgFloydHoareValidityCheck (see fb77554). [1] https://github.com/ultimate-pa/ultimate/blob/19fd058c3d438585a4f478206c978f85e13399ca/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/predicates/HoareAnnotationChecker.java#L141-L143
Previously, the check did not actually check anything, because the successor edges were calculated incorrectly and, in particular for initial states, were always empty. We also need to filter summary edges for implemented procedures as they are not expected to be inductive. This was previously done in HoareAnnotationChecker [1] previous to PR #671. [1] https://github.com/ultimate-pa/ultimate/blob/19fd058c3d438585a4f478206c978f85e13399ca/trunk/source/TraceAbstraction/src/de/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/predicates/HoareAnnotationChecker.java#L141-L143
This PR refactors how ULTIMATE works with proof artifacts (for now, primarily Floyd-Hoare annotations). The point is:
IFloydHoareAnnotation
) rather than annotations in an Icfg. This allows e.g. considering the proofs of multiple CEGAR loops separately (a more elegant solution than the workaround used in Wip/lf/pea complement only #670).I consider the PR more or less ready for review, if the currently running nightly tests don't show any more issues. The only change I still have planned from my side is to go through the
.epf
files and adapt them to the following change in the settings forTraceAbstraction
:However, I wanted to first ask if anyone objects to this or would propose a different settings structure, before I start going through all the settings files.