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
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
53 commits
Select commit Hold shift + click to select a range
1d5d8e9
Docked sequent view: also select proof if needed
FliegendeWurst Nov 30, 2022
62da14e
Use KeYDesktop consistently + fix BROWSE on Linux
FliegendeWurst Nov 30, 2022
b3ed312
Proof difference view: fix link to docs
FliegendeWurst Nov 30, 2022
2d84896
Proof: clear listeners after dispose
FliegendeWurst Dec 5, 2022
0ee0b8c
Proof slicing extension
FliegendeWurst Nov 15, 2022
db5ab14
Add description to help buttons
FliegendeWurst Dec 5, 2022
882eb5d
Various refactorings
FliegendeWurst Dec 9, 2022
47e943c
Formatting, etc.
FliegendeWurst Dec 14, 2022
82fbd70
Ignore only auto-generated solvers.txt
FliegendeWurst Dec 14, 2022
682a560
Make unsat core production optional
FliegendeWurst Dec 14, 2022
02d6f12
Proof slicing: settings provider + refactorings
FliegendeWurst Dec 14, 2022
57928d8
Fix implementation of hashCode
FliegendeWurst Dec 14, 2022
0c0254e
Checkstyle and formatting
FliegendeWurst Dec 15, 2022
619485a
Checkstyle
FliegendeWurst Dec 15, 2022
cbc6e4a
Slicing of open proofs
FliegendeWurst Dec 15, 2022
29bf194
Drop JGraphT dependency
FliegendeWurst Dec 16, 2022
9ea0563
Add test for de-duplicating open proof
FliegendeWurst Dec 19, 2022
fac0130
Automatically enable safe mode of rule de-duplication
FliegendeWurst Dec 19, 2022
66dc3f8
Another graph test
FliegendeWurst Dec 20, 2022
d1eca14
Refactor and comment rule de-duplication algorithm
FliegendeWurst Dec 21, 2022
db033d4
Formatting, Javadocs
FliegendeWurst Dec 22, 2022
2ecee9d
Merge branch 'master' into 'keller/slicingForMaster'
FliegendeWurst Dec 22, 2022
f376a6c
Slice in background thread
FliegendeWurst Dec 23, 2022
d4c28df
Formatting & Checkstyle
FliegendeWurst Jan 10, 2023
0f58f06
Merge remote-tracking branch 'origin/master' into slicing-rework
FliegendeWurst Jan 10, 2023
46fcc69
Javadocs + Cleanups
FliegendeWurst Jan 17, 2023
201bb35
Merge remote-tracking branch 'origin/master' into slicing-rework
FliegendeWurst Jan 17, 2023
5ec4f43
Merge branch 'master' into 'keller/slicingForMaster'
FliegendeWurst Jan 25, 2023
b1cd4cd
Handle missing dot installation correctly
FliegendeWurst Jan 28, 2023
805ea82
Refactor equals implementation of arrays and lists
FliegendeWurst Feb 6, 2023
a7311ab
Add unit test for dependency graph
FliegendeWurst Feb 6, 2023
58e18f8
Fix TermImpl equals
FliegendeWurst Feb 6, 2023
0a333d5
Docs
FliegendeWurst Feb 6, 2023
c356c86
Merge remote-tracking branch 'origin/main' into slicing
FliegendeWurst Feb 15, 2023
6b84a91
Fix proof test files broken by recent changes
FliegendeWurst Feb 16, 2023
3461a69
Checkstyle
FliegendeWurst Feb 16, 2023
7e1906e
Only run SMT test if a solver is available
FliegendeWurst Feb 17, 2023
c264bab
Split analysis into multiple methods
FliegendeWurst Feb 17, 2023
b50763b
Merge branch 'main' into slicing
wadoon Mar 3, 2023
c816aaf
Merge remote-tracking branch 'origin/main'
FliegendeWurst Mar 8, 2023
c379965
More javadocs
FliegendeWurst Mar 8, 2023
f798b9d
Merge remote-tracking branch 'origin/main' into slicing
FliegendeWurst Mar 17, 2023
9892162
Fix proof files
FliegendeWurst Mar 17, 2023
2a6eb5f
Switch to different test proof
FliegendeWurst Mar 17, 2023
192e575
Merge remote-tracking branch 'origin' into slicing
FliegendeWurst Mar 18, 2023
916de10
Switch tests to existing proof files
FliegendeWurst Mar 18, 2023
d348fbd
Revert change to StatusLine
FliegendeWurst Mar 18, 2023
10789e4
Remove stacktrace printing
FliegendeWurst Mar 18, 2023
44f5aac
Escape HTML manually
FliegendeWurst Mar 18, 2023
6675c08
Don't add slices to recent files
FliegendeWurst Mar 18, 2023
e01dcaa
Merge remote-tracking branch 'origin/main' into slicing
FliegendeWurst Mar 20, 2023
0cbd417
Make dot executable path configurable
FliegendeWurst Mar 20, 2023
cfc9de7
Fix HTML escaping
FliegendeWurst Mar 20, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ key.core/src/main/gen
key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.preamble.xml

# this file is automatically generated by gradle task :key.core:generateSolverPropsList
key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes
key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/solvers.txt

key/key.ui/examples/**/**.proof
**/testresults/**
2 changes: 1 addition & 1 deletion key.core/build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ task generateVersionFiles() {

outputs.files sha1, branch, versionf

def gitRevision = gitRevParse('--short HEAD')
def gitRevision = gitRevParse('HEAD')
def gitBranch = gitRevParse('--abbrev-ref HEAD')

doLast {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,14 @@
import java.util.LinkedList;
import java.util.List;
import java.util.Properties;
import java.util.function.Consumer;
import java.util.logging.Logger;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.macros.ProofMacroFinishedInfo;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.ProofAggregate;
import de.uka.ilkd.key.proof.RuleAppListener;
import de.uka.ilkd.key.proof.init.IPersistablePO.LoadedPOContainer;
import de.uka.ilkd.key.proof.init.InitConfig;
import de.uka.ilkd.key.proof.init.ProblemInitializer;
Expand Down Expand Up @@ -201,12 +203,17 @@ public void taskFinished(TaskFinishedInfo info) {
@Override
public AbstractProblemLoader load(Profile profile, File file, List<File> classPath,
File bootClassPath, List<File> includes, Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
boolean forceNewProfileOfNewProofs,
Consumer<Proof> callback) throws ProblemLoaderException {
AbstractProblemLoader loader = null;
try {
loader = new SingleThreadProblemLoader(file, classPath, bootClassPath, includes,
profile, forceNewProfileOfNewProofs, this, false, poPropertiesToForce);
loader.load();
if (callback != null) {
loader.load(callback);
} else {
loader.load();
}
return loader;
} catch (ProblemLoaderException e) {
if (loader != null && loader.getProof() != null) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,13 @@
import java.io.File;
import java.util.List;
import java.util.Properties;
import java.util.function.Consumer;

import de.uka.ilkd.key.java.JavaInfo;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.parser.Location;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.RuleAppListener;
import de.uka.ilkd.key.proof.init.InitConfig;
import de.uka.ilkd.key.proof.init.Profile;
import de.uka.ilkd.key.proof.init.ProofInputException;
Expand Down Expand Up @@ -247,9 +249,39 @@ public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile,
List<File> classPaths, File bootClassPath, List<File> includes,
Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
return load(profile, location, classPaths, bootClassPath, includes, poPropertiesToForce,
ruleCompletionHandler,
null, forceNewProfileOfNewProofs);
}

/**
* Loads the given location and returns all required references as {@link KeYEnvironment}. The
* {@link MainWindow} is not involved in the whole process.
*
* @param profile The {@link Profile} to use.
* @param location The location to load.
* @param classPaths The class path entries to use.
* @param bootClassPath The boot class path to use.
* @param includes Optional includes to consider.
* @param poPropertiesToForce Some optional PO {@link Properties} to force.
* @param ruleCompletionHandler An optional {@link RuleCompletionHandler}.
* @param callbackProofLoaded An optional callback (called when the proof is loaded, before
* replay)
* @param forceNewProfileOfNewProofs {@code} true
* {@link AbstractProblemLoader#profileOfNewProofs} will be used as {@link Profile} of
* new proofs, {@code false} {@link Profile} specified by problem file will be used for
* new proofs.
* @return The {@link KeYEnvironment} which contains all references to the loaded location.
* @throws ProblemLoaderException Occurred Exception
*/
public static KeYEnvironment<DefaultUserInterfaceControl> load(Profile profile, File location,
List<File> classPaths, File bootClassPath, List<File> includes,
Properties poPropertiesToForce, RuleCompletionHandler ruleCompletionHandler,
Consumer<Proof> callbackProofLoaded,
boolean forceNewProfileOfNewProofs) throws ProblemLoaderException {
DefaultUserInterfaceControl ui = new DefaultUserInterfaceControl(ruleCompletionHandler);
AbstractProblemLoader loader = ui.load(profile, location, classPaths, bootClassPath,
includes, poPropertiesToForce, forceNewProfileOfNewProofs);
includes, poPropertiesToForce, forceNewProfileOfNewProofs, callbackProofLoaded);
InitConfig initConfig = loader.getInitConfig();

return new KeYEnvironment<DefaultUserInterfaceControl>(ui, initConfig, loader.getProof(),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,11 @@
import java.io.File;
import java.util.List;
import java.util.Properties;
import java.util.function.Consumer;

import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.ProofAggregate;
import de.uka.ilkd.key.proof.RuleAppListener;
import de.uka.ilkd.key.proof.init.AbstractProfile;
import de.uka.ilkd.key.proof.init.InitConfig;
import de.uka.ilkd.key.proof.init.Profile;
Expand All @@ -19,7 +21,7 @@
* Provides the user interface independent logic to manage multiple proofs. This includes:
* <ul>
* <li>Functionality to load files via {@link #load(Profile, File, List<File>, File, List<File>,
* Properties, boolean)}.</li>
* Properties, boolean, Consumer<Proof>)}.</li>
* <li>Functionality to instantiate new {@link Proof}s via
* {@link #createProof(InitConfig, ProofOblInput)}.</li>
* <li>Functionality to register existing {@link Proof}s in the user interface via
Expand Down Expand Up @@ -65,12 +67,14 @@ public interface UserInterfaceControl {
* {@link AbstractProblemLoader#profileOfNewProofs} will be used as {@link Profile} of
* new proofs, {@code false} {@link Profile} specified by problem file will be used for
* new proofs.
* @param callbackProofLoaded receives the proof after it is loaded, but before it is replayed
* @return The opened {@link AbstractProblemLoader}.
* @throws ProblemLoaderException Occurred Exception.
*/
AbstractProblemLoader load(Profile profile, File file, List<File> classPaths,
File bootClassPath, List<File> includes, Properties poPropertiesToForce,
boolean forceNewProfileOfNewProofs) throws ProblemLoaderException;
boolean forceNewProfileOfNewProofs,
Consumer<Proof> callbackProofLoaded) throws ProblemLoaderException;

/**
* Instantiates a new {@link Proof} in this {@link UserInterfaceControl} for the given
Expand Down
27 changes: 26 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,11 @@
import de.uka.ilkd.key.java.NameAbstractionTable;
import de.uka.ilkd.key.pp.PrettyPrinter;
import de.uka.ilkd.key.java.StatementBlock;
import org.key_project.util.EqualsModProofIrrelevancy;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

public class JavaBlock {
public final class JavaBlock implements EqualsModProofIrrelevancy {
private static final Logger LOGGER = LoggerFactory.getLogger(JavaBlock.class);

/**
Expand All @@ -22,6 +23,7 @@ public class JavaBlock {
public static final JavaBlock EMPTY_JAVABLOCK = new JavaBlock(new StatementBlock());

private final JavaProgramElement prg;
private int hashCode = -1;


/**
Expand Down Expand Up @@ -125,4 +127,27 @@ public String toString() {
return printer.result();
}

@Override
public boolean equalsModProofIrrelevancy(Object obj) {
if (!(obj instanceof JavaBlock)) {
return false;
}
if (this == obj) {
return true;
}
JavaBlock other = (JavaBlock) obj;
// quite inefficient, but sufficient
return toString().equals(other.toString());
}

@Override
public int hashCodeModProofIrrelevancy() {
if (hashCode == -1) {
hashCode = toString().hashCode();
if (hashCode == -1) {
hashCode = 0;
}
}
return hashCode;
}
}
51 changes: 45 additions & 6 deletions key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java
Original file line number Diff line number Diff line change
@@ -1,13 +1,14 @@
package de.uka.ilkd.key.logic;

import java.util.Objects;
import java.util.stream.Collectors;

import org.key_project.util.EqualsModProofIrrelevancy;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.java.CollectionUtil;
import de.uka.ilkd.key.logic.label.TermLabel;
import de.uka.ilkd.key.logic.op.Operator;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.java.CollectionUtil;

import java.util.Objects;
import java.util.stream.Collectors;

/**
* The labeled term class is used for terms that have a label attached.
Expand All @@ -19,7 +20,7 @@
* @see Term
* @see TermImpl
*/
class LabeledTermImpl extends TermImpl {
class LabeledTermImpl extends TermImpl implements EqualsModProofIrrelevancy {

/**
* @see #getLabels()
Expand Down Expand Up @@ -111,6 +112,44 @@ public int computeHashCode() {
return hash;
}

@Override
public boolean equalsModProofIrrelevancy(Object o) {
if (!super.equalsModProofIrrelevancy(o)) {
return false;
}

if (o instanceof LabeledTermImpl) {
final LabeledTermImpl cmp = (LabeledTermImpl) o;
if (labels.size() == cmp.labels.size()) {
for (int i = 0, sz = labels.size(); i < sz; i++) {
// skip irrelevant (origin) labels that differ for no real reason
if (!labels.get(i).isProofRelevant()) {
continue;
}
// this is not optimal, but as long as number of labels limited ok
if (!cmp.labels.contains(labels.get(i))) {
return false;
}
}
return true;
}
return false;
} else {
return o.getClass() == TermImpl.class;
}
}

@Override
public int hashCodeModProofIrrelevancy() {
int hash = super.hashCodeModProofIrrelevancy();
for (int i = 0, sz = labels.size(); i < sz; i++) {
if (labels.get(i).isProofRelevant()) {
hash += 7 * labels.get(i).hashCode();
}
}
return hash;
}

@Override
public String toString() {
StringBuilder result = new StringBuilder(super.toString());
Expand Down
6 changes: 4 additions & 2 deletions key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,12 @@ private Semisequent() {

/**
* creates a new Semisequent with the Semisequent elements in seqList; the provided list must be
* redundance free, i.e., the created sequent must be exactly the same as when creating the
* redundancy free, i.e., the created sequent must be exactly the same as when creating the
* sequent by subsequently inserting all formulas
*
* @param seqList list of sequent formulas
*/
Semisequent(ImmutableList<SequentFormula> seqList) {
public Semisequent(ImmutableList<SequentFormula> seqList) {
assert !seqList.isEmpty();
this.seqList = seqList;
}
Expand Down
7 changes: 7 additions & 0 deletions key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java
Original file line number Diff line number Diff line change
Expand Up @@ -279,6 +279,13 @@ public int formulaNumberInSequent(boolean inAntec, SequentFormula cfma) {
"Ghost formula " + cfma + " in sequent " + this + " [antec=" + inAntec + "]");
}

/**
* Get a sequent formula by its position in the sequent.
* The first formula has number 1.
*
* @param formulaNumber formula number
* @return the sequent formula at that position
*/
public SequentFormula getFormulabyNr(int formulaNumber) {
if (formulaNumber <= 0 || formulaNumber > size()) {
throw new RuntimeException("No formula nr. " + formulaNumber + " in seq. " + this);
Expand Down
30 changes: 29 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/logic/SequentFormula.java
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

import de.uka.ilkd.key.logic.op.AbstractTermTransformer;
import de.uka.ilkd.key.logic.sort.Sort;
import org.key_project.util.EqualsModProofIrrelevancy;


/**
Expand All @@ -12,11 +13,18 @@
* class by providing a way to add additional annotations or to cache local information about the
* formula.
*/
public class SequentFormula {
public class SequentFormula implements EqualsModProofIrrelevancy {

private final Term term;

/**
* Cached value for {@link #hashCode()}.
*/
private final int hashCode;
/**
* Cached value for {@link #hashCodeModProofIrrelevancy()}.
*/
private final int hashCode2;

/**
* creates a new SequentFormula
Expand All @@ -29,6 +37,7 @@ public SequentFormula(Term term) {
}
this.term = term;
this.hashCode = term.hashCode() * 13;
this.hashCode2 = term.hashCodeModProofIrrelevancy();
}

/** @return the stored Term */
Expand Down Expand Up @@ -56,4 +65,23 @@ public String toString() {
public int hashCode() {
return hashCode;
}

@Override
public boolean equalsModProofIrrelevancy(Object obj) {
if (this == obj) {
return true;
}
if (obj instanceof SequentFormula) {
SequentFormula cmp = (SequentFormula) obj;
if (term.equalsModProofIrrelevancy(cmp.formula())) {
return true;
}
}
return false;
}

@Override
public int hashCodeModProofIrrelevancy() {
return hashCode2;
}
}
4 changes: 3 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
package de.uka.ilkd.key.logic;

import javax.annotation.Nullable;

import org.key_project.util.EqualsModProofIrrelevancy;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableSet;

Expand Down Expand Up @@ -33,7 +35,7 @@
* Term supports the {@link Visitor} pattern. Two different visit strategies are currently
* supported: {@link Term#execPostOrder(Visitor)} and {@link Term#execPreOrder(Visitor)}.
*/
public interface Term extends SVSubstitute, Sorted {
public interface Term extends SVSubstitute, Sorted, EqualsModProofIrrelevancy {

/**
* The top operator (e.g., in "A and B" this is "and", in f(x,y) it is "f").
Expand Down
Loading