Skip to content
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 slicing extension #3026

Merged
merged 53 commits into from
Mar 21, 2023
Merged

Conversation

FliegendeWurst
Copy link
Member

@FliegendeWurst FliegendeWurst commented Feb 6, 2023

Continuation of https://git.key-project.org/key/key/-/merge_requests/596. All review comments have been adressed.


This branch introduces the proof analysis and slicing algorithms implemented for my bachelor's thesis for inclusion in the next KeY version.

Why?

Neat data structure (dependency graph) and algorithm that help many usecases: "optimizing" the loading time of finished proofs, investigating the efficiency of KeY's heuristics, reducing the size of incomplete proofs, ...

Also see https://git.key-project.org/key/key-docs/-/merge_requests/7

Features and Impact

Many new features available in the GUI: inspecting the dependency graph of a proof, proof analysis, proof slicing, ...

The build script has been changed to save the full git commit hash as KeY version.

Changes in key.core

  • new EqualsModProofIrrelevancy interface to ignore certain details when comparing objects across proofs (currently only origin labels)
  • Node: stepIndex and branchLocation
  • BranchLocation class to represent a location in the proof tree
  • KeYMediator: fireProofLoaded event (called just before a loaded proof is replayed)
  • ProofSaver: option to only save the proof obligation
  • OneStepSimplifier: when reloading a proof, restrict the formulas available to the Simplifier to the previously used formulas
  • Taclet: addedBy field to indicate which proof step defined a taclet
  • ModularSMTLib2Translator, SMTFocusResults: new facilities to ask the SMT solver for an unsat core and hide formulas not present in the unsat core from the sequent

Changes in key.util

  • Graph, DirectedGraph, GraphEdge, DefaultEdge: simple implementation of a directed graph

Review

The most "interesting" class to review is probably SlicingProofReplayer, since some parts of it are very similar to the IntermediateProofReplayer.

Persons involved

Commit c9f59aeba25cde9f9db4fc608e99f235575377bc by Mattias Ulbrich (experiments with SMT unsat cores) is included in this branch. It was only intended as a "temporary hack", but it proved to be quite useful and has been adapted slightly to handle SMT solvers that do not produce unsat cores.


Comment edited by @WolframPfeifer: Attached the original description.

CVC5 doesn't support labeled expressions in assertions,
so unsat cores are only enabled for Z3 for now.
# Conflicts:
#   key/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
@WolframPfeifer WolframPfeifer added the Under Review Pull request is currently reviewed. Please assign only when you are currently doing the review! label Mar 14, 2023
Copy link
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I finally completed the review, it was quite a lot of code (> 10,000 LOC)!

The slicing extension is very well crafted in my opinion and a great addition to KeY. As we know from the evaluation in the Bachelor's thesis, slicing proofs often greatly reduces their size. Also, the code is very well documented (JavaDoc, internal comments, and a page in key-docs). Thanks for that!

I have a few minor requests for change. Could you please address them?

Finally, I noticed that some examples such as SumAndMax and BinarySearch can not be proven "as automatically" as with earlier KeY releases. Pressing the green button or running Full Auto Pilot alone is not sufficient (needs another "Try Close" afterward). However, this is already the case in the main branch currently and thus not your fault.

@WolframPfeifer WolframPfeifer added Reviewer Feedback Feedback from the review needs to be addressed and removed Under Review Pull request is currently reviewed. Please assign only when you are currently doing the review! labels Mar 15, 2023
@mattulbrich
Copy link
Member

Thanks indeed.

Finally, I noticed that some examples such as SumAndMax and BinarySearch can not be proven "as automatically" as with earlier KeY releases. Pressing the green button or running Full Auto Pilot alone is not sufficient (needs another "Try Close" afterward). However, this is already the case in the main branch currently and thus not your fault.

How did that happen? 😲 We have so man quality measures in place and yet the most prominent example does not work anymore?

@jwiesler jwiesler mentioned this pull request Mar 20, 2023
1 task
@FliegendeWurst
Copy link
Member Author

I have adressed all review comments.

Copy link
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everything is fine now, thanks!

@WolframPfeifer WolframPfeifer added this pull request to the merge queue Mar 21, 2023
@WolframPfeifer WolframPfeifer merged commit 7408745 into KeYProject:main Mar 21, 2023
jwiesler added a commit that referenced this pull request Apr 3, 2023
This MR does some automated code cleanup.
Lots of changes, I grouped the changes in commits and the review should
happen on a per commit basis.

Some of them might be debateable, please do so.
However, I think most of them really help with parsing of and reasoning
about the code.

- [x] Blocking on #3026.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Reviewer Feedback Feedback from the review needs to be addressed
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants