Proof Refactoring #671

maul-esel · 2024-08-09T15:32:00Z

This PR refactors how ULTIMATE works with proof artifacts (for now, primarily Floyd-Hoare annotations). The point is:

to make it easier to work with proofs, by making them first-class concepts (e.g. 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).
to make the handling of proofs more flexible, in preparation for supporting other kinds of proofs; most importantly, thread-modular proofs at many levels and Owicki-Gries proofs. These other kinds of proofs are e.g. needed for concurrency correctness witnesses.

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 for TraceAbstraction:

The setting Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG has been removed. The existing setting Positions where we compute the Hoare Annotation has a possible value NONE (the default value) to disable Hoare computation completely.

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.

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.

…kerUtils

…cers

bahnwaerter

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

...s/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/HoareAnnotationComposer.java

.../src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/HoareAnnotationPositions.java

...e/uni_freiburg/informatik/ultimate/plugins/generator/traceabstraction/AbstractCegarLoop.java

...ltimate/plugins/generator/traceabstractionconcurrent/TraceAbstractionConcurrentObserver.java

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

maul-esel · 2024-08-14T16:03:36Z

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.

…ation

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.

maul-esel · 2024-08-18T14:40:14Z

Fixing the tests required some changes:

The precondition for our Floyd-Hoare annotations is not necessarily true; instead, it is a conjunction of (= g |old(g)|) for all modifiable global variables g of the initial location's procedure. This requires supporting different preconditions per initial location, in the case of multiple initial locations.
A bug in BlockEncodingV2 caused contract computation to fail, as some procedures did not have an exit location. I've fixed this, and added some checks to prevent similar bugs in the future.

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 InvariantResult and ProcedureContractResult (in the form of Check objects).

# 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

danieldietsch

Review so far, I would read on, but feel free to merge anyways,

releaseScripts/default/adds/Ultimate.py

trunk/examples/LTL/regression/c/LTLAutomizerC.epf

...eiburg/informatik/ultimate/plugins/generator/buchiautomizer/cegar/BuchiCegarLoopFactory.java

...-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/FloydHoareMapping.java

...Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/PrePostConditionSpecification.java

...-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/FloydHoareMapping.java

...Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/PrePostConditionSpecification.java

# 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

maul-esel added 30 commits November 27, 2023 23:04

begin sketching proof infrastructure: IProofProducer & friends

60055de

IInitialAbstractionProvider should provide proof producers

a30dbb1

begin sketching proof production in CEGAR loops

d72b396

add operators for proof post processing and conversion

62f36a9

start sketching Hoare proof producer

c5a3332

cherry-pick Floyd-Hoare changes from wip/dk/empire-owicki

76a50a2

These changes allow computing Floyd/Hoare annotations for product automata of concurrent programs.

introduce IFloydHoareAnnotation

2c4dc82

move Floyd/Hoare handling

a87a7c0

BasicCegarLoop should not refer to Floyd/Hoare proofs, let NwaCegarLoop handle this. Also, CEGAR loops refer directly to Hoare annotation states, not IcfgLocations.

HoareAnnotationFragments: rely on supplied hoareAnnotationStates

224148a

Do not check the setting again, the caller should supply the appropriate states.

move HoareAnnotationPositions to its own file

0cd9943

Also define their semantics in the class itself, rather than in some utility class.

begin defining interfaces for proof updates in NwaCegarLoop

c9454fe

move NwaHoareProofProducer to its own file

c3557f2

let CEGAR loops accept proof updaters

94a263c

add HoareAnnotationPositions.None

05c0479

specialize return type

87eb079

IFloydHoareAnnoation: decouple from automaton

3f177bc

rename method

276e2b5

move code for Floyd-Hoare annotations to package in Library-TraceChec…

d17f6f0

…kerUtils

IFloydHoareAnnotation: remove unused type parameter

1604cae

FloydHoareMapping: remove unused automaton

6f4c56b

add Validity::and method

f2110d5

add FloydHoareValidityCheck

eea7867

remove duplicate stopwatch stopping

2032d1f

fix failures due to FloydHoare checking

54d3723

small simplifications in Hoare annotation classes

b4501bd

continue refactoring from hard-coded Hoare annotations to proof produ…

b37babc

…cers

simplify settings (will be modified further)

9080e3b

add missing statistics result to initial abstraction providers

eb2b75c

missing license headers

87b555a

continue refactoring

0aaec9c

fix NPEs

a77894b

maul-esel mentioned this pull request Aug 11, 2024

Wip/lf/pea complement only #670

Merged

adapt setting files (epf, json) and CLI arguments to preferences change

ccca8fe

maul-esel marked this pull request as ready for review August 12, 2024 18:37

bahnwaerter approved these changes Aug 12, 2024

View reviewed changes

minor cleanup

1e57a53

schuessf approved these changes Aug 14, 2024

View reviewed changes

maul-esel added 6 commits August 15, 2024 17:47

FloydHoareValidityCheck: add more informative failure messages

2b4fdb3

remove unnecessary type parameter from results

053cbaa

add explicit representations of the specification shown by a proof

9007b66

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.

PrePostConditionSpecification: precondition may depend on initial loc…

a2c4c3b

…ation

include Check objects in InvariantResult / ProcedureContractResult

591e8a7

maul-esel requested review from bahnwaerter and schuessf August 18, 2024 14:40

danieldietsch reviewed Aug 19, 2024

View reviewed changes

extended documentation of PrePostConditionSpecification

6679c7b

danieldietsch reviewed Aug 19, 2024

View reviewed changes

...Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/PrePostConditionSpecification.java Show resolved Hide resolved

danieldietsch reviewed Aug 19, 2024

View reviewed changes

...Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/PrePostConditionSpecification.java Show resolved Hide resolved

maul-esel added 3 commits August 20, 2024 10:30

more documentation

044eca1

Merge branch 'dev' into wip/dk/proof-refactoring

b03ad22

# Conflicts: # releaseScripts/website-config/frontend/config.js # trunk/source/WebsiteStatic/config/config.dist.js

fix Hoare settings in new settings files

5f48c28

maul-esel merged commit df06d5d into dev Aug 20, 2024
2 checks passed

maul-esel deleted the wip/dk/proof-refactoring branch August 20, 2024 19:46

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Proof Refactoring #671

Proof Refactoring #671

maul-esel commented Aug 9, 2024 •

edited

Loading

bahnwaerter left a comment

maul-esel commented Aug 14, 2024 •

edited

Loading

maul-esel commented Aug 18, 2024 •

edited

Loading

danieldietsch left a comment

Proof Refactoring #671

Proof Refactoring #671

Conversation

maul-esel commented Aug 9, 2024 • edited Loading

bahnwaerter left a comment

Choose a reason for hiding this comment

maul-esel commented Aug 14, 2024 • edited Loading

maul-esel commented Aug 18, 2024 • edited Loading

danieldietsch left a comment

Choose a reason for hiding this comment

maul-esel commented Aug 9, 2024 •

edited

Loading

maul-esel commented Aug 14, 2024 •

edited

Loading

maul-esel commented Aug 18, 2024 •

edited

Loading