diff --git a/README.md b/README.md index 8c7d1ef4cc4..0d170796ae0 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ For more information, refer to * [Verification of `java.util.IdentityHashMap`](https://doi.org/10.1007/978-3-031-07727-2_4), * [Google Award for analysing a bug in `LinkedList`](https://www.key-project.org/2023/07/23/cwi-researchers-win-google-award-for-finding-a-bug-in-javas-linkedlist-using-key/) -The current version of KeY is 2.12.0, licensed under GPL v2. +The current version of KeY is 2.12.2, licensed under GPL v2. Feel free to use the project templates to get started using KeY: @@ -26,7 +26,7 @@ Feel free to use the project templates to get started using KeY: * Hardware: >=2 GB RAM * Operating System: Linux/Unix, MacOSX, Windows -* Java SE 11 or newer +* Java 17 or newer * Optionally, KeY can make use of the following binaries: * SMT Solvers: * [Z3](https://github.com/Z3Prover/z3#z3) @@ -113,7 +113,7 @@ This is the KeY project - Integrated Deductive Software Design Copyright (C) 2001-2011 Universität Karlsruhe, Germany Universität Koblenz-Landau, Germany and Chalmers University of Technology, Sweden -Copyright (C) 2011-2023 Karlsruhe Institute of Technology, Germany +Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany Technical University Darmstadt, Germany Chalmers University of Technology, Sweden diff --git a/build.gradle b/build.gradle index 873bf2fedd0..e82e80644d4 100644 --- a/build.gradle +++ b/build.gradle @@ -70,16 +70,16 @@ subprojects { } dependencies { - implementation("org.slf4j:slf4j-api:2.0.11") + implementation("org.slf4j:slf4j-api:2.0.12") - testImplementation("ch.qos.logback:logback-classic:1.4.14") - testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.1' - testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.1' + testImplementation("ch.qos.logback:logback-classic:1.5.0") + testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2' + testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2' testImplementation project(':key.util') testCompileOnly 'junit:junit:4.13.2' - testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.1' - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.1' + testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.2' + testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2' implementation("org.jspecify:jspecify:0.3.0") } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java b/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java index 32322f6bd3f..0d556acb369 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Comment.java @@ -5,6 +5,9 @@ import de.uka.ilkd.key.java.visitor.Visitor; +/** + * Comment element of Java source code. + */ public class Comment extends JavaSourceElement { private final String text; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java index 6ab94f6813c..04346acf3a7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java @@ -22,12 +22,35 @@ public class MethodDeclaration extends JavaDeclaration implements MemberDeclaration, TypeReferenceContainer, NamedProgramElement, ParameterContainer, Method, VariableScope { + /** + * The return type of the method. + */ protected final TypeReference returnType; + /** + * In case of void return type: comments associated with the method. + */ protected final Comment[] voidComments; + /** + * The name of the method. + */ protected final ProgramElementName name; + /** + * Parameters of the method. + */ protected final ImmutableArray parameters; + /** + * 'throws' part of the method. Indicates which exceptions the method may throw. + * May be null. + */ protected final Throws exceptions; + /** + * Body of the method. + * May be null, in which case the body is referenced in a file using {@link #posInfo}. + */ protected final StatementBlock body; + /** + * JML modifiers of the referenced method. Includes e.g. {@code pure}. + */ protected final JMLModifiers jmlModifiers; /** @@ -53,12 +76,14 @@ public record JMLModifiers(boolean pure, boolean strictlyPure, boolean helper, /** * Method declaration. * - * @param children an ExtList of children. May include: a TypeReference (as a reference to the - * return type), a de.uka.ilkd.key.logic.ProgramElementName (as Name of the method), - * several ParameterDeclaration (as parameters of the declared method), a StatementBlock - * (as body of the declared method), several Modifier (taken as modifiers of the - * declaration), a Comment + * @param children an ExtList of children. Must include: a TypeReference (as a reference to the + * return type), + * a {@link ProgramElementName} (as Name of the method), + * one or more {@link ParameterDeclaration} (as parameters of the declared method), + * optionally a {@link StatementBlock} (as body of the declared method), + * optionally a {@link Throws} to indicate exceptional behaviour * @param parentIsInterfaceDeclaration a boolean set true iff parent is an InterfaceDeclaration + * @param voidComments in case of void return type: comments associated with the method */ public MethodDeclaration(ExtList children, boolean parentIsInterfaceDeclaration, Comment[] voidComments) { @@ -266,6 +291,12 @@ public TypeReference getTypeReference() { } + /** + * Get the "void comments" of this method declaration. + * Only non-null if the method has void return type. + * + * @return the "void comments" + */ public Comment[] getVoidComments() { return voidComments; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java index 8a42178b202..35d0279ec88 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java @@ -23,7 +23,7 @@ public class Throws extends JavaNonTerminalProgramElement implements TypeReferen /** - * Exceptions. + * Exceptions thrown. */ protected final ImmutableArray exceptions; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java index 0a210bd3c57..d813f591bec 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic; +import java.util.Collection; import java.util.Iterator; import org.key_project.util.collection.ImmutableList; @@ -27,11 +28,10 @@ private Semisequent() { seqList = ImmutableSLList.nil(); } - /** - * creates a new Semisequent with the Semisequent elements in seqList; the provided list must be - * redundancy free, i.e., the created sequent must be exactly the same as when creating the - * sequent by subsequently inserting all formulas + * Create a new Semisequent from an ordered collection of formulas. + * The provided list must be 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 */ @@ -40,6 +40,33 @@ public Semisequent(ImmutableList seqList) { this.seqList = seqList; } + /** + * Create a new Semisequent from an ordered collection of formulas. + * The provided collection must be 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 + */ + public Semisequent(Collection seqList) { + assert !seqList.isEmpty(); + this.seqList = ImmutableList.fromList(seqList); + } + + /** + * Create a new Semisequent from an ordered collection of formulas (possibly empty). + * The provided collection must be 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 + */ + public static Semisequent create(Collection seqList) { + if (seqList.isEmpty()) { + return EMPTY_SEMISEQUENT; + } + return new Semisequent(seqList); + } + /** * creates a new Semisequent with the Semisequent elements in seqList diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java index e03c824d415..c8181096e46 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java @@ -22,24 +22,31 @@ import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.key_project.util.collection.ImmutableSet; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; /** * The program method represents a (pure) method in the logic. In case of a non-static method the * first argument represents the object on which the method is invoked. + *

+ * This data is used in + * {@link de.uka.ilkd.key.speclang.QueryAxiom#getTaclets(ImmutableSet, Services)}. */ public final class ProgramMethod extends ObserverFunction implements ProgramInLogic, IProgramMethod { - private static final Logger LOGGER = LoggerFactory.getLogger(ProgramMethod.class); + /** + * The referenced method. + */ private final MethodDeclaration method; /** * Return type of the method. Must not be null. Use KeYJavaType.VOID_TYPE for void methods. */ private final KeYJavaType returnType; + /** + * Where the method is located in a .java file. + */ private final PositionInfo pi; // ------------------------------------------------------------------------- @@ -63,6 +70,12 @@ public ProgramMethod(MethodDeclaration method, KeYJavaType container, KeYJavaTyp // internal methods // ------------------------------------------------------------------------- + /** + * Get the java types of the parameters required by the method md. + * + * @param md some method declaration + * @return java types of the parameters required by md + */ private static ImmutableArray getParamTypes(MethodDeclaration md) { KeYJavaType[] result = new KeYJavaType[md.getParameterDeclarationCount()]; for (int i = 0; i < result.length; i++) { @@ -80,11 +93,6 @@ private static ImmutableArray getParamTypes(MethodDeclaration md) { // MethodDeclaration // in a direct way - /* - * (non-Javadoc) - * - * @see de.uka.ilkd.key.logic.op.IProgramMethod#getMethodDeclaration() - */ @Override public MethodDeclaration getMethodDeclaration() { return method; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index 3f58e86f071..6844b16ccec 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java @@ -66,7 +66,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { : null; var origin = BuilderHelpers.getPosition(ctx); var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin); - sorts().add(s); + sorts().addSafely(s); return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index 69785ef1614..66c3f766022 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Name; +import de.uka.ilkd.key.logic.Namespace; import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.logic.op.SortDependingFunction; @@ -52,16 +53,30 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { // weigl: all datatypes are free ==> functions are unique! // boolean freeAdt = ctx.FREE() != null; var sort = sorts().lookup(ctx.name.getText()); + var dtNamespace = new Namespace(); for (KeYParser.Datatype_constructorContext constructorContext : ctx .datatype_constructor()) { Name name = new Name(constructorContext.name.getText()); Sort[] args = new Sort[constructorContext.sortId().size()]; + var argNames = constructorContext.argName; for (int i = 0; i < args.length; i++) { - args[i] = accept(constructorContext.sortId(i)); + Sort argSort = accept(constructorContext.sortId(i)); + args[i] = argSort; + var argName = argNames.get(i).getText(); + var alreadyDefinedFn = dtNamespace.lookup(argName); + if (alreadyDefinedFn != null + && (!alreadyDefinedFn.sort().equals(argSort) + || !alreadyDefinedFn.argSort(0).equals(sort))) { + throw new RuntimeException("Name already in namespace: " + argName); + } + Function fn = new Function(new Name(argName), argSort, new Sort[] { sort }, null, + false, false); + dtNamespace.add(fn); } Function function = new Function(name, sort, args, null, true, false); - namespaces().functions().add(function); + namespaces().functions().addSafely(function); } + namespaces().functions().addSafely(dtNamespace.allElements()); return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index f58f7a4615f..9ba6c08b0f8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -243,9 +243,95 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) { var tbSplit = createConstructorSplit(ctx); registerTaclet(ctx, tbSplit); + Sort dtSort = namespaces().sorts().lookup(ctx.name.getText()); + for (var constructor : ctx.datatype_constructor()) { + for (int i = 0; i < constructor.sortId().size(); i++) { + var argName = constructor.argName.get(i).getText(); + + var tbDeconstructor = createDeconstructorTaclet(constructor, argName, i); + registerTaclet(ctx, tbDeconstructor); + + var tbDeconsEq = createDeconstructorEQTaclet(constructor, argName, i, dtSort); + registerTaclet(ctx, tbDeconsEq); + } + } + return null; } + private TacletBuilder createDeconstructorTaclet( + KeYParser.Datatype_constructorContext constructor, String argName, int argIndex) { + var tacletBuilder = new RewriteTacletBuilder<>(); + tacletBuilder + .setName(new Name(String.format("%s_Dec_%s", argName, constructor.name.getText()))); + tacletBuilder.setDisplayName( + String.format("%s_Deconstruct_%s", argName, constructor.name.getText())); + + var schemaVariables = new SchemaVariable[constructor.argName.size()]; + var args = new Term[constructor.argName.size()]; + var tb = services.getTermBuilder(); + + // Schema vars for constructor, e.g., Cons(head_sv, tail_sv) + for (int i = 0; i < constructor.argName.size(); i++) { + var name = constructor.argName.get(i).getText() + "_sv"; + Sort sort = accept(constructor.argSort.get(i)); + var sv = declareSchemaVariable(constructor, name, sort, false, false, false, + new SchemaVariableModifierSet.TermSV()); + schemaVariables[i] = sv; + args[i] = tb.var(sv); + } + + var function = namespaces().functions().lookup(argName); + var consFn = namespaces().functions().lookup(constructor.name.getText()); + + // Find, e.g, tail(Cons(head_sv, tail_sv)) + tacletBuilder.setFind(tb.func(function, tb.func(consFn, args))); + tacletBuilder.addTacletGoalTemplate( + new RewriteTacletGoalTemplate(tb.var(schemaVariables[argIndex]))); + tacletBuilder.setApplicationRestriction(RewriteTaclet.SAME_UPDATE_LEVEL); + + return tacletBuilder; + } + + private TacletBuilder createDeconstructorEQTaclet( + KeYParser.Datatype_constructorContext constructor, String argName, int argIndex, + Sort dtSort) { + var tacletBuilder = new RewriteTacletBuilder<>(); + tacletBuilder.setName( + new Name(String.format("%s_DecEQ_%s", argName, constructor.name.getText()))); + tacletBuilder.setDisplayName( + String.format("%s_DeconstructEQ_%s", argName, constructor.name.getText())); + + var schemaVariables = new SchemaVariable[constructor.argName.size()]; + var args = new Term[constructor.argName.size()]; + var tb = services.getTermBuilder(); + + // Schema vars for constructor, e.g., Cons(head_sv, tail_sv) + for (int i = 0; i < constructor.argName.size(); i++) { + var name = constructor.argName.get(i).getText() + "_sv"; + Sort sort = accept(constructor.argSort.get(i)); + var sv = declareSchemaVariable(constructor, name, sort, false, false, false, + new SchemaVariableModifierSet.TermSV()); + schemaVariables[i] = sv; + args[i] = tb.var(sv); + } + + var function = namespaces().functions().lookup(argName); + var consFn = namespaces().functions().lookup(constructor.name.getText()); + + var x = declareSchemaVariable(constructor, argName + "_x", dtSort, false, false, false, + new SchemaVariableModifierSet.TermSV()); + var res = schemaVariables[argIndex]; + + tacletBuilder.setFind(tb.func(function, tb.var(x))); + tacletBuilder.setIfSequent(Sequent.createAnteSequent( + new Semisequent(new SequentFormula(tb.equals(tb.var(x), tb.func(consFn, args)))))); + tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(tb.var(res))); + tacletBuilder.setApplicationRestriction(RewriteTaclet.SAME_UPDATE_LEVEL); + + return tacletBuilder; + } + private TacletBuilder createInductionTaclet( KeYParser.Datatype_declContext ctx) { @@ -359,12 +445,14 @@ private RewriteTacletBuilder createConstructorSplit( KeYParser.Datatype_declContext ctx) { final var tb = services.getTermBuilder(); + final String prefix = ctx.name.getText() + "_"; + Map variables = new HashMap<>(); for (KeYParser.Datatype_constructorContext context : ctx.datatype_constructor()) { for (int i = 0; i < context.argName.size(); i++) { var name = context.argName.get(i).getText(); var sort = sorts().lookup(context.argSort.get(i).getText()); - var sv = declareSchemaVariable(ctx, name, sort, + var sv = declareSchemaVariable(ctx, prefix + name, sort, false, true, false, new SchemaVariableModifierSet.TermSV()); variables.put(name, tb.var(sv)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index a574785f3bd..69640391ec8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -464,7 +464,7 @@ public Collection children() { } /** - * @return an iterator for all nodes in the subtree. + * @return an iterator for all nodes in the subtree (including this node). */ public Iterator subtreeIterator() { return new SubtreeIterator(this); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index 548d6d96b8f..ee28c5e813a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -6,6 +6,7 @@ import java.beans.PropertyChangeListener; import java.io.File; import java.util.*; +import java.util.function.Consumer; import java.util.function.Predicate; import de.uka.ilkd.key.java.JavaInfo; @@ -16,8 +17,11 @@ import de.uka.ilkd.key.proof.event.ProofDisposedListener; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.Profile; +import de.uka.ilkd.key.proof.io.IntermediateProofReplayer; import de.uka.ilkd.key.proof.mgt.ProofCorrectnessMgt; import de.uka.ilkd.key.proof.mgt.ProofEnvironment; +import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; import de.uka.ilkd.key.rule.OneStepSimplifier; import de.uka.ilkd.key.settings.GeneralSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; @@ -1254,4 +1258,46 @@ public void deregister(T obj, Class service) { public void setMutedProofCloseEvents(boolean mutedProofCloseEvents) { this.mutedProofCloseEvents = mutedProofCloseEvents; } + + /** + * For each branch closed by reference to another proof, + * copy the relevant proof steps into this proof. + * + * @param referencedFrom filter, if not null copy only from that proof + * @param callbackTotal callback that gets the total number of branches to complete + * @param callbackBranch callback notified every time a branch has been copied + */ + public void copyCachedGoals(Proof referencedFrom, Consumer callbackTotal, + Runnable callbackBranch) { + // first, ensure that all cached goals are copied over + List goals = closedGoals().toList(); + List todo = new ArrayList<>(); + for (Goal g : goals) { + Node node = g.node(); + ClosedBy c = node.lookup(ClosedBy.class); + if (c == null) { + continue; + } + if (referencedFrom != null && referencedFrom != c.proof()) { + continue; + } + todo.add(g); + } + if (callbackTotal != null) { + callbackTotal.accept(todo.size()); + } + for (Goal g : todo) { + reOpenGoal(g); + ClosedBy c = g.node().lookup(ClosedBy.class); + g.node().deregister(c, ClosedBy.class); + try { + new CopyingProofReplayer(c.proof(), this).copy(c.node(), g, c.nodesToSkip()); + } catch (IntermediateProofReplayer.BuiltInConstructionException e) { + throw new RuntimeException(e); + } + if (callbackBranch != null) { + callbackBranch.run(); + } + } + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/SubtreeIterator.java b/key.core/src/main/java/de/uka/ilkd/key/proof/SubtreeIterator.java index 705fc914a11..0e8d159da75 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/SubtreeIterator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/SubtreeIterator.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.proof; import java.util.Iterator; +import java.util.NoSuchElementException; /** * Iterator over subtree. Current implementation iteratively traverses the tree depth-first. @@ -58,6 +59,8 @@ public Node next() { Node s = nextSibling(n); if (s != null) { n = s; + } else { + throw new NoSuchElementException(); } } else { n = n.child(0); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java b/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java index 1fd37398fa5..6ee59d7ae4c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java @@ -3,15 +3,19 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.reference; +import java.util.Set; + import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; /** * Indicates that a branch has been closed by "reference" to another closed proof. + * This is always looked up using {@link Node#lookup(Class)} on the node of that branch. * * @param proof The proof referenced. * @param node The node referenced. + * @param nodesToSkip If the referenced proof has dependency graph information: proof steps to skip. * @author Arne Keller */ -public record ClosedBy(Proof proof, Node node) { +public record ClosedBy(Proof proof, Node node, Set nodesToSkip) { } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/CopyReferenceResolver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/reference/CopyReferenceResolver.java index 071b5282694..9c38b4c5ab6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/CopyReferenceResolver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/reference/CopyReferenceResolver.java @@ -51,7 +51,7 @@ public static void copyCachedGoals( ClosedBy c = g.node().lookup(ClosedBy.class); g.node().deregister(c, ClosedBy.class); try { - new CopyingProofReplayer(c.proof(), toComplete).copy(c.node(), g); + new CopyingProofReplayer(c.proof(), toComplete).copy(c.node(), g, c.nodesToSkip()); } catch (IntermediateProofReplayer.BuiltInConstructionException e) { throw new RuntimeException(e); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/CopyingProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/CopyingProofReplayer.java index 8a9f4be3ec9..ac2739833b8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/CopyingProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/CopyingProofReplayer.java @@ -5,6 +5,7 @@ import java.util.ArrayDeque; import java.util.Deque; +import java.util.Set; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; @@ -35,24 +36,36 @@ public CopyingProofReplayer(Proof originalProof, Proof proof) { * * @param originalNode original proof * @param newNode open goal in new proof + * @param skippedNodes nodes to skip when copying * @throws IntermediateProofReplayer.BuiltInConstructionException on error */ - public void copy(Node originalNode, Goal newNode) + public void copy(Node originalNode, Goal newNode, Set skippedNodes) throws IntermediateProofReplayer.BuiltInConstructionException { newNode.proof().reOpenGoal(newNode); newNode.proof().register(this, CopyingProofReplayer.class); newNode.proof().setMutedProofCloseEvents(true); OneStepSimplifier.refreshOSS(newNode.proof()); + + // nodeQueue: nodes in the ORIGINAL proof Deque nodeQueue = new ArrayDeque<>(); + // queue: nodes in the NEW proof Deque queue = new ArrayDeque<>(); + queue.add(newNode); nodeQueue.add(originalNode); - while (!nodeQueue.isEmpty()) { + while (!nodeQueue.isEmpty() && !queue.isEmpty()) { Node nextNode = nodeQueue.pop(); Goal nextGoal = queue.pop(); for (int i = nextNode.childrenCount() - 1; i >= 0; i--) { nodeQueue.addFirst(nextNode.child(i)); } + // skip explicitly requested nodes + if (skippedNodes.contains(nextNode)) { + if (!nextGoal.node().isClosed()) { + queue.addFirst(nextGoal); + } + continue; + } // skip nextNode if it is a closed goal if (nextNode.getAppliedRuleApp() == null) { continue; diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java index 44d162edb0e..436ec981253 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java @@ -34,21 +34,24 @@ public class GeneralSettings extends AbstractSettings { private static final String CATEGORY = "General"; - private static final String TACLET_FILTER = "StupidMode"; - private static final String DND_DIRECTION_SENSITIVE_KEY = "DnDDirectionSensitive"; - private static final String USE_JML_KEY = "UseJML"; + public static final String TACLET_FILTER = "StupidMode"; + public static final String DND_DIRECTION_SENSITIVE_KEY = "DnDDirectionSensitive"; + public static final String USE_JML_KEY = "UseJML"; - private static final String KEY_JML_ENABLED_KEYS = "JML_ENABLED_KEYS"; + public static final String KEY_JML_ENABLED_KEYS = "JML_ENABLED_KEYS"; - private static final String RIGHT_CLICK_MACROS_KEY = "RightClickMacros"; - private static final String AUTO_SAVE = "AutoSavePeriod"; + public static final String RIGHT_CLICK_MACROS_KEY = "RightClickMacros"; + public static final String AUTO_SAVE = "AutoSavePeriod"; /** * The key for storing the ensureSourceConsistency flag in settings */ private static final String ENSURE_SOURCE_CONSISTENCY = "EnsureSourceConsistency"; - private Set jmlEnabledKeys = new TreeSet<>(Set.of("key")); + /** Default value for {@link #getJmlEnabledKeys()} */ + public static final Set JML_ENABLED_KEYS_DEFAULT = Set.of("key"); + + private Set jmlEnabledKeys = new TreeSet<>(JML_ENABLED_KEYS_DEFAULT); /** * minimize interaction is on by default diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java index 8592d0e06d3..77a165021de 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java @@ -77,6 +77,9 @@ public void addSettings(Settings settings) { if (lastReadedProperties != null) { settings.readSettings(lastReadedProperties); } + if (lastReadedConfiguration != null) { + settings.readSettings(lastReadedConfiguration); + } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/IntegerOpHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/IntegerOpHandler.java index 179ac8d4058..7d1bb3ee68e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/IntegerOpHandler.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/IntegerOpHandler.java @@ -48,6 +48,7 @@ public void init(MasterHandler masterHandler, Services services, Properties hand supportedOperators.put(mul, "*"); supportedOperators.put(integerLDT.getSub(), "-"); supportedOperators.put(integerLDT.getDiv(), "div"); + supportedOperators.put(integerLDT.getMod(), "mod"); supportedOperators.put(integerLDT.getNeg(), "-"); supportedOperators.put(integerLDT.getLessOrEquals(), "<="); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java index 1c88075d6b6..0793ba65a02 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java @@ -180,6 +180,7 @@ public ImmutableSet getTaclets(ImmutableSet sig = ImmutableSLList.nil() .append(target.getParamTypes().toArray(new KeYJavaType[target.getNumParams()])); + // get real implementation of program method final IProgramMethod targetImpl = services.getJavaInfo().getProgramMethod(kjt, target.getName(), sig, kjt); final MethodBodyStatement mbs = new MethodBodyStatement(targetImpl, selfProgSV, diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java index 41167b54bb1..ee6a0f9382f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java @@ -110,7 +110,7 @@ private static ImmutableList getJMLComments(MethodDeclaration method) { coms = coms.prepend(method.getTypeReference().getComments()); } - // ... or to 'void' ... + // ... or to 'void' (special case) ... if (method.getVoidComments() != null) { coms = coms.prepend(method.getVoidComments()); } @@ -137,11 +137,6 @@ public static MethodDeclaration.JMLModifiers parseMethod(MethodDeclaration metho return new MethodDeclaration.JMLModifiers(pure, strictlyPure, helper, specMathMode); } - private static boolean hasJMLModifier(MethodDeclaration pm, String mod) { - var coms = getJMLComments(pm); - return checkFor(mod, coms); - } - /** * Extracts the list of comments for a given field. The comments should usually be modifiers. diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java index 6d2d73e21a1..f7e81afcd2e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java @@ -99,8 +99,8 @@ public OverloadedOperatorHandler(Services services, SpecMathMode specMathMode) { this.integerHandler = new IntegerHandler(services, specMathMode); handlers.add(new BinaryBooleanHandler(services)); - // handlers.add(new SequenceHandler(services)); - // handlers.add(new LocSetHandler(services)); + handlers.add(new SequenceHandler(services)); + handlers.add(new LocSetHandler(services)); handlers.add(this.integerHandler); handlers.add(new FloatHandler(services)); handlers.add(new DoubleHandler(services)); @@ -150,6 +150,9 @@ public SequenceHandler(Services services) { @Override public SLExpression build(JMLOperator op, SLExpression left, SLExpression right) throws SLTranslationException { + if (right == null) { + return null; + } if (left.getTerm().sort() == ldtSequence.targetSort() && right.getTerm().sort() == ldtSequence.targetSort()) { if (op == JMLOperator.ADD) { @@ -173,17 +176,20 @@ public LocSetHandler(Services services) { @Override public SLExpression build(JMLOperator op, SLExpression left, SLExpression right) throws SLTranslationException { + if (right == null) { + return null; + } final var l = left.getTerm(); final var r = right.getTerm(); if (l.sort() == ldt.targetSort() && r.sort() == ldt.targetSort()) { return switch (op) { case ADD, BITWISE_OR -> new SLExpression(tb.union(l, r)); case SUBTRACT -> new SLExpression(tb.setMinus(l, r)); - case BITWISE_AND -> new SLExpression(tb.intersect(l, r)); - case LT -> new SLExpression(tb.subset(l, r)); - case LTE -> new SLExpression(tb.and(tb.subset(l, r), tb.equals(l, r))); - case GT -> new SLExpression(tb.subset(r, l)); - case GTE -> new SLExpression(tb.and(tb.subset(r, l), tb.equals(l, r))); + case MULT, BITWISE_AND -> new SLExpression(tb.intersect(l, r)); + case LT -> new SLExpression(tb.and(tb.subset(l, r), tb.not(tb.equals(l, r)))); + case LTE -> new SLExpression(tb.subset(l, r)); + case GT -> new SLExpression(tb.and(tb.subset(r, l), tb.not(tb.equals(l, r)))); + case GTE -> new SLExpression(tb.subset(r, l)); default -> null; }; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index 562ed291651..0b6611a1fce 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -571,6 +571,7 @@ public SLExpression visitEqualityexpr(JmlParser.EqualityexprContext ctx) { if (floatResult != null) { return floatResult; } + exc.updatePosition(ctx.getStart()); if (tok.getText().equals("==")) { result = termFactory.eq(result, expr.get(i)); } else { diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java index 831c78398f1..73af6f82c50 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic; +import java.util.ArrayList; + import de.uka.ilkd.key.logic.op.Function; import de.uka.ilkd.key.logic.sort.Sort; import de.uka.ilkd.key.logic.sort.SortImpl; @@ -306,4 +308,11 @@ public void testListReplaceAddRedundantList() { assertEquals(expected, extract(sci), "Both semisequents should be equal."); } + @Test + void constructorTest() { + var a = Semisequent.EMPTY_SEMISEQUENT; + var b = Semisequent.create(new ArrayList<>()); + assertSame(a, b); + } + } diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java new file mode 100644 index 00000000000..d68c2d94e17 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java @@ -0,0 +1,60 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.nparser; + +import java.io.File; +import java.util.Collection; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.logic.Name; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; +import de.uka.ilkd.key.rule.Taclet; + +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.Test; + +/** + * Tests for handling of abstract datatypes in KeY files. + */ +public class AdtTests { + private static final String EXPECTED_PRED_DEC_SUCC = """ + pred_Dec_succ { + \\find(pred(succ(pred_sv))) + \\sameUpdateLevel\\replacewith(pred_sv)\s + + Choices: true}"""; + private static final String EXPECTED_PRED_DECEQ_SUCC = """ + pred_DecEQ_succ { + \\assumes ([equals(pred_x,succ(pred_sv))]==>[])\s + \\find(pred(pred_x)) + \\sameUpdateLevel\\replacewith(pred_sv)\s + + Choices: true}"""; + + @Test + public void destructorTest() throws ProblemLoaderException { + var path = new File("../key.ui/examples/standard_key/adt/dt_nat.key"); + var env = KeYEnvironment.load(path); + var taclets = env.getInitConfig().activatedTaclets(); + + for (Taclet taclet : taclets) { + if (taclet.name().toString().contains("_Dec")) + System.out.println(taclet.name()); + } + + var predDecsucc = get("pred_Dec_succ", taclets); + var predDecEqSucc = get("pred_DecEQ_succ", taclets); + + Assertions.assertEquals(EXPECTED_PRED_DEC_SUCC, predDecsucc.toString()); + Assertions.assertEquals(EXPECTED_PRED_DECEQ_SUCC, predDecEqSucc.toString()); + + } + + private Taclet get(String name, Collection taclets) { + var n = new Name(name); + var t = taclets.stream().filter(it -> n.equals(it.name())).findAny().orElse(null); + Assertions.assertNotNull(t); + return t; + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java b/key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java index ffa13d6709d..ffbd0d43486 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.proof.replay; import java.io.File; +import java.util.HashSet; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; @@ -45,7 +46,7 @@ void testJavaProof() throws Exception { proof2.pruneProof(proof2.root()); proof2.getServices().resetCounters(); new CopyingProofReplayer(proof1, proof2).copy(proof1.root(), - proof2.getOpenGoal(proof2.root())); + proof2.getOpenGoal(proof2.root()), new HashSet<>()); Assertions.assertTrue(proof2.closed()); Assertions.assertEquals(proof1.countNodes(), proof2.countNodes()); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index f0e986b7327..d217367f555 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -970,6 +970,7 @@ public static ProofCollection automaticJavaDL() throws IOException { g.loadable("standard_key/adt/dt_list_revrev.proof"); g.loadable("standard_key/adt/dt_list_appnil.proof"); g.loadable("standard_key/adt/dt_color.proof"); + g.loadable("standard_key/adt/dt_list_deconstruct.key"); return c; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java new file mode 100644 index 00000000000..664b631aca8 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java @@ -0,0 +1,90 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.smt.newsmt2; + +import java.io.File; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; +import de.uka.ilkd.key.smt.SMTProblem; +import de.uka.ilkd.key.smt.SMTSolverResult; +import de.uka.ilkd.key.smt.SMTTestSettings; +import de.uka.ilkd.key.smt.SolverLauncher; +import de.uka.ilkd.key.smt.solvertypes.SolverType; +import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation; +import de.uka.ilkd.key.smt.solvertypes.SolverTypes; + +import org.key_project.util.helper.FindResources; + +import org.junit.Test; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * This class is for testing the translation of modulo from KeY to SMT + * + * @author Nils Buchholz, 2024 + */ +public class TestSMTMod { + + private static final Logger LOGGER = LoggerFactory.getLogger(TestSMTMod.class); + + private static final File testCaseDirectory = FindResources.getTestCasesDirectory(); + + private static final SolverType Z3_SOLVER = SolverTypes.getSolverTypes().stream() + .filter(it -> it.getClass().equals(SolverTypeImplementation.class) + && it.getName().equals("Z3")) + .findFirst().orElse(null); + + private static final SolverType CVC4_SOLVER = SolverTypes.getSolverTypes().stream() + .filter(it -> it.getClass().equals(SolverTypeImplementation.class) + && it.getName().equals("CVC4")) + .findFirst().orElse(null); + + /** + * This tests if x mod y is non-negative and x mod y < |y| for y != 0 + * thus satisfying the definition of euclidean modulo + * Tests for Z3 and CVC4 + * + * @throws ProblemLoaderException Occured Exception during load of problem file + */ + @Test + public void testModSpec() throws ProblemLoaderException { + KeYEnvironment env = + KeYEnvironment.load(new File(testCaseDirectory, "smt/modSpec.key")); + try { + Proof proof = env.getLoadedProof(); + assertNotNull(proof); + assertEquals(1, proof.openGoals().size()); + Goal g = proof.openGoals().iterator().next(); + SMTSolverResult result; + if (Z3_SOLVER.isInstalled(true)) { + result = checkGoal(g, Z3_SOLVER); + assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid()); + } else { + LOGGER.warn("Warning:Z3 solver not installed, tests skipped."); + } + if (CVC4_SOLVER.isInstalled(true)) { + result = checkGoal(g, CVC4_SOLVER); + assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid()); + } else { + LOGGER.warn("Warning:CVC4 solver not installed, tests skipped."); + } + } finally { + env.dispose(); + } + } + + private SMTSolverResult checkGoal(Goal g, SolverType solverType) { + SolverLauncher launcher = new SolverLauncher(new SMTTestSettings()); + SMTProblem problem = new SMTProblem(g); + launcher.launch(problem, g.proof().getServices(), solverType); + return problem.getFinalResult(); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java index 7dbebc230ee..c73a5c13445 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java @@ -25,6 +25,8 @@ import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.CsvSource; import static java.lang.String.format; import static org.junit.jupiter.api.Assertions.*; @@ -444,4 +446,36 @@ public void testCorrectImplicitThisResolution() { ProofSaver.printTerm(expected, services), ProofSaver.printTerm(result, services))); } + @ParameterizedTest + @CsvSource(value = { + "\\seq(1) + \\seq(2,3) : \\seq_concat(\\seq(1), \\seq(2,3))", + "\\locset(this.b) + \\locset(this.s) : \\set_union(\\locset(this.b), \\locset(this.s))", + "\\locset(this.b) | \\locset(this.s) : \\set_union(\\locset(this.b), \\locset(this.s))", + "\\locset(this.b) & \\locset(this.s) : \\intersect(\\locset(this.b), \\locset(this.s))", + "\\locset(this.b) * \\locset(this.s) : \\intersect(\\locset(this.b), \\locset(this.s))", + "\\locset(this.b) <= \\locset(this.s) : \\subset(\\locset(this.b), \\locset(this.s))", + "\\locset(this.b) < \\locset(this.s) : \\subset(\\locset(this.b), \\locset(this.s)) && \\locset(this.b) != \\locset(this.s)", + "\\locset(this.b) >= \\locset(this.s) : \\subset(\\locset(this.s), \\locset(this.b))", + "\\locset(this.b) > \\locset(this.s) : \\subset(\\locset(this.s), \\locset(this.b)) && \\locset(this.b) != \\locset(this.s)", + }, delimiter = ':') + public void testOperatorOverloading(String expression, String expected) { + Term tTrans = null, tExp = null; + try { + tTrans = jmlIO.parseExpression(expression); + } catch (Exception e) { + fail("Cannot parse " + expression, e); + } + + try { + tExp = jmlIO.parseExpression(expected); + } catch (Exception e) { + fail("Cannot parse " + expected, e); + } + + if (!tTrans.equalsModTermLabels(tExp)) { + // this gives nicer error + assertEquals(tExp, tTrans); + } + } + } diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/TypeError.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/TypeError.java index 8d57c617ce2..1be9fbf4568 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/TypeError.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/TypeError.java @@ -1,8 +1,7 @@ // exceptionClass: RuntimeException // msgContains: Error in equality-expression -// position: 12/17 +// position: 11/19 // verbose: true -// broken: true // It's not the best of error messages ... // and there is no file location information diff --git a/key.core/src/test/resources/testcase/smt/modSpec.key b/key.core/src/test/resources/testcase/smt/modSpec.key new file mode 100644 index 00000000000..56efa24ac41 --- /dev/null +++ b/key.core/src/test/resources/testcase/smt/modSpec.key @@ -0,0 +1,9 @@ +\functions { + int y; + int x; +} + +\problem { + ((y>0) -> x % y >= 0 & x % y < y) & ((y<0) -> x%y >= 0 & x % y < -y) +} + diff --git a/key.ui/build.gradle b/key.ui/build.gradle index ea66e0b38ab..74e41bee931 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -23,12 +23,13 @@ dependencies { api 'com.miglayout:miglayout-swing:11.3' //logging implementation used by the slf4j - implementation 'ch.qos.logback:logback-classic:1.4.14' + implementation 'ch.qos.logback:logback-classic:1.5.0' api 'org.key-project:docking-frames-common:1.1.3p1' api 'org.key-project:docking-frames-core:1.1.3p1' runtimeOnly project(":keyext.ui.testgen") + runtimeOnly project(":keyext.caching") runtimeOnly project(":keyext.exploration") runtimeOnly project(":keyext.slicing") runtimeOnly project(":keyext.proofmanagement") @@ -63,7 +64,7 @@ run { systemProperties["key.examples.dir"] = "$projectDir/examples" //systemProperties["slf4j.detectLoggerNameMismatch"] = true //systemProperties["KeyDebugFlag"] = "on" - args "--experimental" + //args "--experimental" // this can be used to solve a problem where the OS hangs during debugging of popup menus // (see https://docs.oracle.com/javase/10/troubleshoot/awt.htm#JSTGD425) diff --git a/key.ui/examples/standard_key/adt/dt_list_deconstruct.key b/key.ui/examples/standard_key/adt/dt_list_deconstruct.key new file mode 100644 index 00000000000..e2e0ad56ef9 --- /dev/null +++ b/key.ui/examples/standard_key/adt/dt_list_deconstruct.key @@ -0,0 +1,11 @@ +\datatypes { + List = Nil | Cons(any head, List tail) | Cons2(any head2, List tail); +} + +\functions { + List x; +} + +\problem { + Nil = tail(Cons(0, Nil)) & Nil = tail(Cons2(0, Nil)) & (x = Cons(0, Cons(1, Nil)) -> head(x) = 0) +} \ No newline at end of file diff --git a/key.ui/examples/standard_key/adt/dt_list_deconstruct.proof b/key.ui/examples/standard_key/adt/dt_list_deconstruct.proof new file mode 100644 index 00000000000..aa1303ee817 --- /dev/null +++ b/key.ui/examples/standard_key/adt/dt_list_deconstruct.proof @@ -0,0 +1,116 @@ +\profile "Java Profile"; + +\settings // Proof-Settings-Config-File +{ + "Choice" : { + "JavaCard" : "JavaCard:on", + "Strings" : "Strings:on", + "assertions" : "assertions:on", + "bigint" : "bigint:on", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "wdChecks" : "wdChecks:off", + "wdOperator" : "wdOperator:L" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "JavaCardDLStrategy", + "MaximumNumberOfAutomaticApplications" : 500, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE", + "OSS_OPTIONS_KEY" : "OSS_OFF", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } + } + +\datatypes { + List = Nil | Cons(any head, List tail) | Cons2(any head2, List tail); +} + +\functions { + List x; +} +\problem { + Nil = tail(Cons(Z(0(#)), Nil)) +& Nil = tail(Cons2(Z(0(#)), Nil)) +& ( x = Cons(Z(0(#)), Cons(Z(1(#)), Nil)) + -> head(x) = Z(0(#))) +} + +\proof { +(keyLog "0" (keyUser "daniel" ) (keyVersion "1fb0c10630b493ce138850ae0f9803d3f2fffc51")) + +(autoModeTime "0") + +(branch "dummy ID" +(rule "andRight" (formula "1") (userinteraction)) +(branch "Case 1" + (rule "andRight" (formula "1") (userinteraction)) + (branch "Case 1" + (rule "tail_Dec_Cons" (formula "1") (term "1") (userinteraction)) + (rule "equalUnique" (formula "1") (userinteraction)) + (rule "closeTrue" (formula "1") (userinteraction)) + ) + (branch "Case 2" + (rule "tail_Dec_Cons2" (formula "1") (term "1") (userinteraction)) + (rule "equalUnique" (formula "1") (userinteraction)) + (rule "closeTrue" (formula "1") (userinteraction)) + ) +) +(branch "Case 2" + (rule "impRight" (formula "1") (userinteraction)) + (rule "head_DecEQ_Cons" (formula "2") (term "0") (ifseqformula "1") (userinteraction)) + (rule "equal_literals" (formula "2") (userinteraction)) + (rule "closeTrue" (formula "2") (userinteraction)) +) +) +} diff --git a/key.ui/examples/standard_key/adt/dt_nat.key b/key.ui/examples/standard_key/adt/dt_nat.key index 07a8b6d8845..51bed19f749 100644 --- a/key.ui/examples/standard_key/adt/dt_nat.key +++ b/key.ui/examples/standard_key/adt/dt_nat.key @@ -1,5 +1,5 @@ \datatypes { - \free Nat = zero | succ(Nat pred); + Nat = zero | succ(Nat pred); } \predicates { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java index f4ee4884408..f5e40873058 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java @@ -21,6 +21,8 @@ import javax.swing.tree.TreeSelectionModel; import de.uka.ilkd.key.gui.utilities.GuiUtilities; +import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.settings.ViewSettings; import org.key_project.util.java.IOUtil; @@ -277,6 +279,15 @@ public void mouseClicked(MouseEvent e) { .setMaximumSize(new Dimension(Integer.MAX_VALUE, (int) buttonDim.getHeight() + 10)); getContentPane().add(buttonPanel); + // create the checkbox to hide example load on next startup + ViewSettings vs = ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings(); + JCheckBox showAgainCheckbox = + new JCheckBox("Show this dialog on startup", vs.getShowLoadExamplesDialog()); + buttonPanel.add(showAgainCheckbox); + showAgainCheckbox.addActionListener(e -> { + vs.setShowLoadExamplesDialog(showAgainCheckbox.isSelected()); + }); + // create "load" button loadButton = new JButton("Load Example"); loadButton.addActionListener(e -> { @@ -312,6 +323,7 @@ public void mouseClicked(MouseEvent e) { buttonPanel.add(cancelButton); GuiUtilities.attachClickOnEscListener(cancelButton); + // select first example DefaultMutableTreeNode firstLeaf = ((DefaultMutableTreeNode) model.getRoot()).getFirstLeaf(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/JmlEnabledKeysIndicator.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/JmlEnabledKeysIndicator.java new file mode 100644 index 00000000000..8b34fc7794a --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/JmlEnabledKeysIndicator.java @@ -0,0 +1,49 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui; + +import java.util.List; +import javax.swing.*; + +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.settings.GeneralSettings; +import de.uka.ilkd.key.settings.ProofIndependentSettings; + +/** + * Provides a Label in the status line for the indication of the current enabled keys for the JML + * condition evaluation. + * + * @author weigl + * @see GeneralSettings#getJmlEnabledKeys() + */ +@KeYGuiExtension.Info(experimental = false, name = "JML Enabled Keys Indicator for the Status Line") +public class JmlEnabledKeysIndicator implements KeYGuiExtension, KeYGuiExtension.StatusLine { + private final GeneralSettings settings = + ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings(); + private final JLabel lblIndicator = new JLabel(); + + public JmlEnabledKeysIndicator() { + lblIndicator.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5)); + lblIndicator.setToolTipText("Currently enabled keys for tool-specific JML annotations"); + settings.addPropertyChangeListener(GeneralSettings.KEY_JML_ENABLED_KEYS, it -> update()); + update(); + } + + private void update() { + final var current = settings.getJmlEnabledKeys(); + if (!GeneralSettings.JML_ENABLED_KEYS_DEFAULT.equals(current)) { + var lbl = String.join(", ", current); + lblIndicator.setText(lbl); + lblIndicator.setVisible(true); + } else { + lblIndicator.setText(""); + lblIndicator.setVisible(false); + } + } + + @Override + public List getStatusLineComponents() { + return List.of(lblIndicator); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java index 1ca5ca4e929..faafde53aba 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java @@ -13,7 +13,7 @@ /** * Status line of the KeY MainWindow. *

- * The status line hold a lblStatusText and a progress panel. + * The status line holds a lblStatusText and a progress panel. *

* You add additional components by using the extension points * {@link de.uka.ilkd.key.gui.extension.api.KeYGuiExtension.StatusLine} @@ -28,7 +28,6 @@ * @see de.uka.ilkd.key.gui.extension.api.KeYGuiExtension.StatusLine */ class MainStatusLine extends JPanel { - private static final long serialVersionUID = 2278249652314818379L; private final JLabel lblStatusText = new JLabel(); private final JProgressBar progressBar = new JProgressBar(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index cd00d4bbe5f..1537e96149d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -833,6 +833,9 @@ public void unfreezeExceptAutoModeButton() { } } + /** + * Update the sequent view. + */ public void makePrettyView() { if (getMediator().ensureProofLoaded()) { getMediator().getNotationInfo().refresh(mediator.getServices()); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java index f7978a92249..4ffd981ff96 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java @@ -26,8 +26,6 @@ import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent; -import de.uka.ilkd.key.gui.plugins.caching.DefaultReferenceSearchDialogListener; -import de.uka.ilkd.key.gui.plugins.caching.ReferenceSearchDialog; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Statistics; @@ -39,6 +37,7 @@ import org.slf4j.LoggerFactory; public class ShowProofStatistics extends MainWindowAction { + private static final String CSV_SEPERATOR = ";"; private static final Logger LOGGER = LoggerFactory.getLogger(ShowProofStatistics.class); private static final long serialVersionUID = -8814798230037775905L; @@ -84,7 +83,7 @@ public void actionPerformed(ActionEvent e) { public static String getCSVStatisticsMessage(Proof proof) { final int openGoals = proof.openGoals().size(); StringBuilder stats = new StringBuilder(); - stats.append("open goals,").append(openGoals).append("\n"); + stats.append("open goals" + CSV_SEPERATOR).append(openGoals).append("\n"); final Statistics s = proof.getStatistics(); @@ -92,7 +91,7 @@ public static String getCSVStatisticsMessage(Proof proof) { if ("".equals(x.second)) { stats.append(x.first).append("\n"); } else { - stats.append(x.first).append(",").append(x.second).append("\n"); + stats.append(x.first).append(CSV_SEPERATOR).append(x.second).append("\n"); } } @@ -109,7 +108,8 @@ public static String getCSVStatisticsMessage(Proof proof) { sortedEntries.addAll(s.getInteractiveAppsDetails().entrySet()); for (Map.Entry entry : sortedEntries) { - stats.append("interactive,").append(entry.getKey()).append(",") + stats.append("interactive" + CSV_SEPERATOR).append(entry.getKey()) + .append(CSV_SEPERATOR) .append(entry.getValue()).append("\n"); } } @@ -315,6 +315,8 @@ private void init(MainWindow mainWindow, String stats) { buttonPane2.add(saveButton); buttonPane2.add(saveBundleButton); + // spotless:off + /* if (proof.closedGoals().stream() .anyMatch(g -> g.node().lookup(ClosedBy.class) != null)) { JButton copyReferences = new JButton("Realize cached branches"); @@ -332,6 +334,8 @@ private void init(MainWindow mainWindow, String stats) { }); buttonPane2.add(copyReferences); } + */ + // spotless:on getRootPane().setDefaultButton(okButton); getRootPane().addKeyListener(new KeyAdapter() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java index 63850efec13..e60fccd4ede 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java @@ -10,12 +10,16 @@ import de.uka.ilkd.key.settings.AbstractPropertiesSettings; public class ExtensionSettings extends AbstractPropertiesSettings { - public final static String KEY_DISABLED = "disabled"; + private static final String NAME = "Extensions"; + public static final String KEY_DISABLED = "disabled"; + /** + * Class names of disabled extensions. + */ private final PropertyEntry> forbiddenClasses = createStringSetProperty(KEY_DISABLED, ""); public ExtensionSettings() { - super("Extensions"); + super(NAME); } public Collection getForbiddenClasses() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java index 7b3f8b2f933..1b2e01c96af 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java @@ -223,17 +223,29 @@ public static List getContextMenuExtensions() { return getExtensionInstances(KeYGuiExtension.ContextMenu.class); } + /** + * Create a context menu with extension-provided actions for the specified kind and underlying + * object. + *

+ * If the underlying object is a proof, this will also include the usual actions. + *

+ * + * @param kind what kind of object the context menu is built on + * @param underlyingObject the object the context menu is built on + * @param mediator the KeY mediator + * @return populated context menu + */ public static JPopupMenu createContextMenu(ContextMenuKind kind, Object underlyingObject, KeYMediator mediator) { JPopupMenu menu = new JPopupMenu(); - if (underlyingObject instanceof Proof) { - for (Component comp : MainWindow.getInstance().createProofMenu((Proof) underlyingObject) + if (underlyingObject instanceof Proof proof) { + for (Component comp : MainWindow.getInstance().createProofMenu(proof) .getMenuComponents()) { menu.add(comp); } } List content = getContextMenuItems(kind, underlyingObject, mediator); - content.forEach(menu::add); + content.forEach(it -> sortActionIntoMenu(it, menu)); return menu; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java index 4fbc7ecf688..af3bf9cbfe4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java @@ -179,6 +179,8 @@ protected JTextField addFileChooserPanel(String title, String file, String info, } /** + * Adds a new combobox to the panel. + * * @param title label of the combo box * @param info help text * @param selectionIndex which item to initially select diff --git a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension index 0861ef03748..99b38233d0c 100644 --- a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension +++ b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -7,4 +7,5 @@ de.uka.ilkd.key.gui.nodeviews.ShowHashcodesExtension de.uka.ilkd.key.gui.LogView de.uka.ilkd.key.gui.plugins.javac.JavacExtension de.uka.ilkd.key.gui.plugins.caching.CachingExtension -de.uka.ilkd.key.gui.utilities.HeapStatusExt \ No newline at end of file +de.uka.ilkd.key.gui.utilities.HeapStatusExt +de.uka.ilkd.key.gui.JmlEnabledKeysIndicator \ No newline at end of file diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/closed-cached.png b/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/closed-cached.png index dd1943da175..a69bf849179 100644 Binary files a/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/closed-cached.png and b/key.ui/src/main/resources/de/uka/ilkd/key/gui/images/closed-cached.png differ diff --git a/keyext.caching/build.gradle b/keyext.caching/build.gradle new file mode 100644 index 00000000000..c927e4b9910 --- /dev/null +++ b/keyext.caching/build.gradle @@ -0,0 +1,6 @@ +dependencies { + implementation project(":key.core") + implementation project(":key.ui") + + implementation project(":keyext.slicing") +} \ No newline at end of file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachedProofBranch.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachedProofBranch.java similarity index 100% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachedProofBranch.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachedProofBranch.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingException.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingException.java similarity index 100% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingException.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingException.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java similarity index 67% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java index 7c2a9c1dd5d..c0f7f1d813c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java @@ -3,9 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.plugins.caching; -import java.awt.event.ActionEvent; import java.util.ArrayList; -import java.util.Arrays; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -14,12 +12,18 @@ import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.core.KeYSelectionEvent; import de.uka.ilkd.key.core.KeYSelectionListener; -import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.help.HelpInfo; +import de.uka.ilkd.key.gui.plugins.caching.actions.CloseAllByReference; +import de.uka.ilkd.key.gui.plugins.caching.actions.CloseByReference; +import de.uka.ilkd.key.gui.plugins.caching.actions.CopyReferencedProof; +import de.uka.ilkd.key.gui.plugins.caching.actions.GotoReferenceAction; +import de.uka.ilkd.key.gui.plugins.caching.actions.RemoveCachingInformationAction; +import de.uka.ilkd.key.gui.plugins.caching.settings.CachingSettingsProvider; +import de.uka.ilkd.key.gui.plugins.caching.settings.ProofCachingSettings; +import de.uka.ilkd.key.gui.plugins.caching.toolbar.CachingToggleAction; import de.uka.ilkd.key.gui.settings.SettingsProvider; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.TryCloseMacro; @@ -38,7 +42,6 @@ import de.uka.ilkd.key.prover.TaskFinishedInfo; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.ApplyStrategy; -import de.uka.ilkd.key.settings.ProofCachingSettings; import org.key_project.util.collection.ImmutableList; @@ -57,7 +60,8 @@ @HelpInfo(path = "/user/ProofCaching/") public class CachingExtension implements KeYGuiExtension, KeYGuiExtension.Startup, KeYGuiExtension.ContextMenu, - KeYGuiExtension.StatusLine, KeYGuiExtension.Settings, + KeYGuiExtension.StatusLine, KeYGuiExtension.Settings, KeYGuiExtension.Toolbar, + KeYGuiExtension.MainMenu, KeYSelectionListener, RuleAppListener, ProofDisposedListener, ProverTaskListener { private static final Logger LOGGER = LoggerFactory.getLogger(CachingExtension.class); @@ -66,8 +70,8 @@ public class CachingExtension */ private KeYMediator mediator; /** - * Whether to try to close the current proof after a rule application. - * Will be false when running certain macros. + * Whether to try to close the current proof (by caching) after a rule application. + * Will be false when running certain macros, like the "close provable goals" macro. */ private boolean tryToClose = false; @@ -76,6 +80,43 @@ public class CachingExtension */ private final Set trackedProofs = new HashSet<>(); private ReferenceSearchButton referenceSearchButton; + private CachingToggleAction toggleAction = null; + private CachingPruneHandler cachingPruneHandler = null; + + private void initActions(MainWindow mainWindow) { + if (toggleAction == null) { + toggleAction = new CachingToggleAction(mainWindow); + } + } + + /** + * Update the GUI state of the status line button. + * + * @param proof the currently open proof + */ + public void updateGUIState(Proof proof) { + referenceSearchButton.updateState(proof); + } + + @Override + public @NonNull JToolBar getToolbar(MainWindow mainWindow) { + initActions(mainWindow); + JToolBar tb = new JToolBar("Proof Caching"); + JToggleButton comp = new JToggleButton(toggleAction); + comp.setToolTipText((String) toggleAction.getValue(Action.LONG_DESCRIPTION)); + tb.add(comp); + return tb; + } + + @Override + public @NonNull List getMainMenuActions(@NonNull MainWindow mainWindow) { + initActions(mainWindow); + return List.of(toggleAction); + } + + public boolean getProofCachingEnabled() { + return toggleAction.isSelected(); + } @Override public void selectedProofChanged(KeYSelectionEvent e) { @@ -86,10 +127,13 @@ public void selectedProofChanged(KeYSelectionEvent e) { trackedProofs.add(p); p.addRuleAppListener(this); p.addProofDisposedListener(this); + p.addProofTreeListener(cachingPruneHandler); } @Override public void ruleApplied(ProofEvent e) { + // main entry point for proof caching logic: + // this is called after every rule application in the proof if (!tryToClose) { return; } @@ -102,6 +146,10 @@ public void ruleApplied(ProofEvent e) { if (!CachingSettingsProvider.getCachingSettings().getEnabled()) { return; } + // new global off switch + if (!getProofCachingEnabled()) { + return; + } Proof p = e.getSource(); if (e.getRuleAppInfo().getOriginalNode().getNodeInfo().getInteractiveRuleApplication()) { return; // only applies for automatic proof search @@ -111,9 +159,15 @@ public void ruleApplied(ProofEvent e) { return; } for (Goal goal : newGoals) { - ClosedBy c = ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), - goal.node()); + ClosedBy c = null; + try { + c = ReferenceSearcher.findPreviousProof(mediator.getCurrentlyOpenedProofs(), + goal.node()); + } catch (Exception exception) { + LOGGER.warn("error during reference search ", exception); + } if (c != null) { + // stop automode from working on this goal goal.setEnabled(false); goal.node().register(c, ClosedBy.class); @@ -133,7 +187,7 @@ public void preInit(MainWindow window, KeYMediator mediator) { @Override public void init(MainWindow window, KeYMediator mediator) { - + cachingPruneHandler = new CachingPruneHandler(mediator); } @Override @@ -153,9 +207,15 @@ public List getContextActions(@NonNull KeYMediator mediator, if (kind.getType() == Node.class) { Node node = (Node) underlyingObject; List actions = new ArrayList<>(); - actions.add(new CloseByReference(mediator, node)); + actions.add(new CloseByReference(this, mediator, node)); actions.add(new CopyReferencedProof(mediator, node)); actions.add(new GotoReferenceAction(mediator, node)); + actions.add(new RemoveCachingInformationAction(mediator, node)); + return actions; + } else if (kind.getType() == Proof.class) { + Proof proof = (Proof) underlyingObject; + List actions = new ArrayList<>(); + actions.add(new CloseAllByReference(this, mediator, proof)); return actions; } return new ArrayList<>(); @@ -269,117 +329,6 @@ public void proofDisposed(ProofDisposedEvent e) { } } - /** - * Action to search for suitable references on a single node. - * - * @author Arne Keller - */ - private final class CloseByReference extends KeyAction { - /** - * The mediator. - */ - private final KeYMediator mediator; - /** - * The node to try to close by reference. - */ - private final Node node; - - /** - * Construct new action. - * - * @param mediator the mediator - * @param node the node - */ - public CloseByReference(KeYMediator mediator, Node node) { - this.mediator = mediator; - this.node = node; - setName("Close by reference to other proof"); - setEnabled(!node.isClosed() && node.lookup(ClosedBy.class) == null); - setMenuPath("Proof Caching"); - } - - @Override - public void actionPerformed(ActionEvent e) { - List nodes = new ArrayList<>(); - if (node.leaf()) { - nodes.add(node); - } else { - node.subtreeIterator().forEachRemaining(n -> { - if (n.leaf() && !n.isClosed()) { - nodes.add(n); - } - }); - } - List mismatches = new ArrayList<>(); - for (Node n : nodes) { - // search other proofs for matching nodes - ClosedBy c = ReferenceSearcher.findPreviousProof( - mediator.getCurrentlyOpenedProofs(), n); - if (c != null) { - n.proof().closeGoal(n.proof().getOpenGoal(n)); - n.register(c, ClosedBy.class); - } else { - mismatches.add(n.serialNr()); - } - } - if (!nodes.isEmpty()) { - referenceSearchButton.updateState(nodes.get(0).proof()); - } - if (!mismatches.isEmpty()) { - // since e.getSource() is the popup menu, it is better to use the MainWindow - // instance here as a parent - JOptionPane.showMessageDialog(MainWindow.getInstance(), - "No matching branch found for node(s) " + Arrays.toString(mismatches.toArray()), - "Proof Caching error", JOptionPane.WARNING_MESSAGE); - } - } - } - - /** - * Action to copy referenced proof steps to the new proof. - * - * @author Arne Keller - */ - private static class CopyReferencedProof extends KeyAction { - /** - * The mediator. - */ - private final KeYMediator mediator; - /** - * The node to copy the steps to. - */ - private final Node node; - - /** - * Construct a new action. - * - * @param mediator the mediator - * @param node the node - */ - public CopyReferencedProof(KeYMediator mediator, Node node) { - this.mediator = mediator; - this.node = node; - setName("Copy referenced proof steps here"); - setEnabled(node.leaf() && node.isClosed() - && node.lookup(ClosedBy.class) != null); - setMenuPath("Proof Caching"); - } - - @Override - public void actionPerformed(ActionEvent e) { - ClosedBy c = node.lookup(ClosedBy.class); - Goal current = node.proof().getClosedGoal(node); - try { - mediator.stopInterface(true); - new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current); - mediator.startInterface(true); - } catch (Exception ex) { - LOGGER.error("failed to copy proof ", ex); - IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex); - } - } - } - @Override public SettingsProvider getSettings() { return new CachingSettingsProvider(); diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingPruneHandler.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingPruneHandler.java new file mode 100644 index 00000000000..ef4cc2c269e --- /dev/null +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingPruneHandler.java @@ -0,0 +1,79 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.caching; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.IssueDialog; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.plugins.caching.settings.CachingSettingsProvider; +import de.uka.ilkd.key.gui.plugins.caching.settings.ProofCachingSettings; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.ProofTreeEvent; +import de.uka.ilkd.key.proof.ProofTreeListener; +import de.uka.ilkd.key.proof.io.IntermediateProofReplayer; +import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Handles prunes in proofs that are referenced elsewhere. + * If the branch that is pruned away is used as caching target (via {@link ClosedBy}) + * elsewhere, that reference is removed before the prune occurs. + * + * @author Arne Keller + */ +public class CachingPruneHandler implements ProofTreeListener { + public static final Logger LOGGER = LoggerFactory.getLogger(CachingPruneHandler.class); + + /** + * The KeY mediator. + */ + private final KeYMediator mediator; + + /** + * Create a new handler. + * + * @param mediator the KeY mediator + */ + public CachingPruneHandler(KeYMediator mediator) { + this.mediator = mediator; + } + + @Override + public void proofIsBeingPruned(ProofTreeEvent e) { + Proof proofToBePruned = e.getSource(); + // check other proofs for any references to this proof + for (Proof p : mediator.getCurrentlyOpenedProofs()) { + for (Goal g : p.closedGoals()) { + ClosedBy c = g.node().lookup(ClosedBy.class); + if (c == null || c.proof() != proofToBePruned) { + continue; + } + var commonAncestor = e.getNode().commonAncestor(c.node()); + if (commonAncestor == c.node()) { + boolean copySteps = CachingSettingsProvider.getCachingSettings().getPrune() + .equals(ProofCachingSettings.PRUNE_COPY); + // proof is now open + // => remove caching reference + g.node().deregister(c, ClosedBy.class); + p.reOpenGoal(g); + if (copySteps) { + // quickly copy the proof before it is pruned + try { + new CopyingProofReplayer(c.proof(), p).copy(c.node(), g, + c.nodesToSkip()); + } catch (IntermediateProofReplayer.BuiltInConstructionException ex) { + LOGGER.warn("failed to copy referenced proof that" + + "is about to be pruned", ex); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex); + } + } + } + } + } + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java similarity index 100% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java similarity index 100% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java similarity index 100% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialogListener.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialogListener.java similarity index 100% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialogListener.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialogListener.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java similarity index 100% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseAllByReference.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseAllByReference.java new file mode 100644 index 00000000000..b2232ecaafe --- /dev/null +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseAllByReference.java @@ -0,0 +1,81 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.caching.actions; + +import java.awt.event.ActionEvent; +import java.util.ArrayList; +import java.util.List; +import javax.swing.*; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.gui.plugins.caching.CachingExtension; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.proof.reference.ReferenceSearcher; + +/** + * Proof context menu action to perform proof caching for all open goals on that proof. + * + * @author Arne Keller + */ +public class CloseAllByReference extends KeyAction { + /** + * The caching extension. + */ + private final CachingExtension cachingExtension; + /** + * The mediator. + */ + private final KeYMediator mediator; + /** + * The proof whose open goals we try to close by reference. + */ + private final Proof proof; + + /** + * Construct new action. + * + * @param mediator the mediator + * @param proof the proof + */ + public CloseAllByReference(CachingExtension cachingExtension, KeYMediator mediator, + Proof proof) { + this.cachingExtension = cachingExtension; + this.mediator = mediator; + this.proof = proof; + setName("Run proof caching search for open goals"); + setEnabled(!proof.closed()); + setMenuPath("Proof Caching"); + } + + @Override + public void actionPerformed(ActionEvent e) { + // nodes will be the open goals for which to + // perform proof caching + List nodes = new ArrayList<>(); + proof.openGoals().forEach(x -> nodes.add(x.node())); + int matches = 0; + for (Node n : nodes) { + // search other proofs for matching nodes + ClosedBy c = ReferenceSearcher.findPreviousProof( + mediator.getCurrentlyOpenedProofs(), n); + if (c != null) { + n.proof().closeGoal(n.proof().getOpenGoal(n)); + n.register(c, ClosedBy.class); + matches++; + } + } + if (matches > 0) { + cachingExtension.updateGUIState(proof); + // since e.getSource() is the popup menu, it is better to use the MainWindow + // instance here as a parent + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "Successfully closed " + matches + " open goal(s) by cache", + "Proof Caching info", JOptionPane.INFORMATION_MESSAGE); + } + } +} diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java new file mode 100644 index 00000000000..7dcafc483f2 --- /dev/null +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java @@ -0,0 +1,91 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.caching.actions; + +import java.awt.event.ActionEvent; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import javax.swing.*; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.gui.plugins.caching.CachingExtension; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.proof.reference.ReferenceSearcher; + +/** + * Action to search for suitable references on a single node. + * + * @author Arne Keller + */ +public final class CloseByReference extends KeyAction { + /** + * The caching extension. + */ + private final CachingExtension cachingExtension; + /** + * The mediator. + */ + private final KeYMediator mediator; + /** + * The node to try to close by reference. + */ + private final Node node; + + /** + * Construct new action. + * + * @param mediator the mediator + * @param node the node + */ + public CloseByReference(CachingExtension cachingExtension, KeYMediator mediator, Node node) { + this.cachingExtension = cachingExtension; + this.mediator = mediator; + this.node = node; + setName("Close by reference to other proof"); + setEnabled(!node.isClosed() && node.lookup(ClosedBy.class) == null); + setMenuPath("Proof Caching"); + } + + @Override + public void actionPerformed(ActionEvent e) { + // nodes will be the open goals for which to + // perform proof caching + List nodes = new ArrayList<>(); + if (node.leaf()) { + nodes.add(node); + } else { + node.subtreeIterator().forEachRemaining(n -> { + if (n.leaf() && !n.isClosed()) { + nodes.add(n); + } + }); + } + List mismatches = new ArrayList<>(); + for (Node n : nodes) { + // search other proofs for matching nodes + ClosedBy c = ReferenceSearcher.findPreviousProof( + mediator.getCurrentlyOpenedProofs(), n); + if (c != null) { + n.proof().closeGoal(n.proof().getOpenGoal(n)); + n.register(c, ClosedBy.class); + } else { + mismatches.add(n.serialNr()); + } + } + if (!nodes.isEmpty()) { + cachingExtension.updateGUIState(nodes.get(0).proof()); + } + if (!mismatches.isEmpty()) { + // since e.getSource() is the popup menu, it is better to use the MainWindow + // instance here as a parent + JOptionPane.showMessageDialog(MainWindow.getInstance(), + "No matching branch found for node(s) " + Arrays.toString(mismatches.toArray()), + "Proof Caching error", JOptionPane.WARNING_MESSAGE); + } + } +} diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java new file mode 100644 index 00000000000..cd818b55d8c --- /dev/null +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java @@ -0,0 +1,66 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.caching.actions; + +import java.awt.event.ActionEvent; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.IssueDialog; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Action to copy referenced proof steps to the new proof. + * + * @author Arne Keller + */ +public final class CopyReferencedProof extends KeyAction { + private static final Logger LOGGER = LoggerFactory.getLogger(CopyReferencedProof.class); + + /** + * The mediator. + */ + private final KeYMediator mediator; + /** + * The node to copy the steps to. + */ + private final Node node; + + /** + * Construct a new action. + * + * @param mediator the mediator + * @param node the node + */ + public CopyReferencedProof(KeYMediator mediator, Node node) { + this.mediator = mediator; + this.node = node; + setName("Copy referenced proof steps here"); + setEnabled(node.leaf() && node.isClosed() + && node.lookup(ClosedBy.class) != null); + setMenuPath("Proof Caching"); + } + + @Override + public void actionPerformed(ActionEvent e) { + ClosedBy c = node.lookup(ClosedBy.class); + Goal current = node.proof().getClosedGoal(node); + try { + mediator.stopInterface(true); + new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current, + c.nodesToSkip()); + mediator.startInterface(true); + } catch (Exception ex) { + LOGGER.error("failed to copy proof ", ex); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex); + } + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/GotoReferenceAction.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/GotoReferenceAction.java similarity index 91% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/GotoReferenceAction.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/GotoReferenceAction.java index 4071642cdf9..234749e63e6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/GotoReferenceAction.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/GotoReferenceAction.java @@ -1,7 +1,7 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.gui.plugins.caching; +package de.uka.ilkd.key.gui.plugins.caching.actions; import java.awt.event.ActionEvent; @@ -15,7 +15,7 @@ * * @author Arne Keller */ -public class GotoReferenceAction extends KeyAction { +public final class GotoReferenceAction extends KeyAction { private final KeYMediator mediator; private final Node node; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/RemoveCachingInformationAction.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/RemoveCachingInformationAction.java new file mode 100644 index 00000000000..7037248ea28 --- /dev/null +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/RemoveCachingInformationAction.java @@ -0,0 +1,49 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.caching.actions; + +import java.awt.event.ActionEvent; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.reference.ClosedBy; + +/** + * Action to remove caching information on a goal closed by caching. + * + * @author Arne Keller + */ +public final class RemoveCachingInformationAction extends KeyAction { + + /** + * The KeY mediator. + */ + private final KeYMediator mediator; + /** + * The node to apply the action on. + */ + private final Node node; + + public RemoveCachingInformationAction(KeYMediator mediator, Node node) { + this.mediator = mediator; + this.node = node; + + setMenuPath("Proof Caching"); + setEnabled(node.lookup(ClosedBy.class) != null); + + setName("Re-open cached goal"); + putValue(SHORT_DESCRIPTION, "Make this an open goal again."); + } + + @Override + public void actionPerformed(ActionEvent e) { + // remove associated info + node.deregister(node.lookup(ClosedBy.class), ClosedBy.class); + // and re-open the goal + node.proof().reOpenGoal(node.proof().getClosedGoal(node)); + // refresh selection to ensure UI is updated + mediator.getSelectionModel().setSelectedNode(node); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingSettingsProvider.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/settings/CachingSettingsProvider.java similarity index 61% rename from key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingSettingsProvider.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/settings/CachingSettingsProvider.java index 544e392b3bc..f77b3deb6b3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingSettingsProvider.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/settings/CachingSettingsProvider.java @@ -1,29 +1,30 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.gui.plugins.caching; +package de.uka.ilkd.key.gui.plugins.caching.settings; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.settings.SettingsPanel; import de.uka.ilkd.key.gui.settings.SettingsProvider; -import de.uka.ilkd.key.settings.ProofCachingSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; import net.miginfocom.layout.CC; -import static de.uka.ilkd.key.settings.ProofCachingSettings.DISPOSE_COPY; -import static de.uka.ilkd.key.settings.ProofCachingSettings.DISPOSE_REOPEN; +import static de.uka.ilkd.key.gui.plugins.caching.settings.ProofCachingSettings.DISPOSE_COPY; +import static de.uka.ilkd.key.gui.plugins.caching.settings.ProofCachingSettings.DISPOSE_REOPEN; +import static de.uka.ilkd.key.gui.plugins.caching.settings.ProofCachingSettings.PRUNE_COPY; +import static de.uka.ilkd.key.gui.plugins.caching.settings.ProofCachingSettings.PRUNE_REOPEN; /** - * Settings for the proof slicing extension. + * Settings for the proof caching extension. * * @author Arne Keller */ public class CachingSettingsProvider extends SettingsPanel implements SettingsProvider { /** - * Singleton instance of the slicing settings. + * Singleton instance of the caching settings. */ private static final ProofCachingSettings CACHING_SETTINGS = new ProofCachingSettings(); @@ -36,14 +37,29 @@ public class CachingSettingsProvider extends SettingsPanel implements SettingsPr */ private static final String STRATEGY_SEARCH = "Automatically search for references in auto mode"; + /** + * Label for second option. + */ private static final String DISPOSE_TITLE = "Behaviour when disposing referenced proof"; + /** + * Label for third option. + */ + private static final String PRUNE_TITLE = + "Behaviour when pruning into referenced proof"; /** * Checkbox for first option. */ private final JCheckBox strategySearch; + /** + * Combobox for second option (dispose behaviour). + */ private final JComboBox disposeOption; + /** + * Combobox for third option (prune behaviour). + */ + private final JComboBox pruneOption; /** * Construct a new settings provider. @@ -55,8 +71,16 @@ public CachingSettingsProvider() { strategySearch = addCheckBox(STRATEGY_SEARCH, "", true, emptyValidator()); - disposeOption = addComboBox(DISPOSE_TITLE, null, 0, x -> { - }, DISPOSE_COPY, DISPOSE_REOPEN); + disposeOption = addComboBox(DISPOSE_TITLE, """ + When a referenced proof is disposed, this is what happens to + all cached branches that reference it.""", + 0, x -> { + }, DISPOSE_COPY, DISPOSE_REOPEN); + pruneOption = addComboBox(PRUNE_TITLE, """ + When a referenced proof is pruned, this is what happens to + all cached branches that reference it.""", + 0, x -> { + }, PRUNE_REOPEN, PRUNE_COPY); } @Override @@ -77,6 +101,7 @@ public JPanel getPanel(MainWindow window) { ProofCachingSettings ss = getCachingSettings(); strategySearch.setSelected(ss.getEnabled()); disposeOption.setSelectedItem(ss.getDispose()); + pruneOption.setSelectedItem(ss.getPrune()); return this; } @@ -85,6 +110,7 @@ public void applySettings(MainWindow window) { ProofCachingSettings ss = getCachingSettings(); ss.setEnabled(strategySearch.isEnabled()); ss.setDispose(disposeOption.getSelectedItem().toString()); + ss.setPrune(pruneOption.getSelectedItem().toString()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofCachingSettings.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/settings/ProofCachingSettings.java similarity index 60% rename from key.core/src/main/java/de/uka/ilkd/key/settings/ProofCachingSettings.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/settings/ProofCachingSettings.java index 81d370feb14..30d9e09f68f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofCachingSettings.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/settings/ProofCachingSettings.java @@ -1,7 +1,9 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.settings; +package de.uka.ilkd.key.gui.plugins.caching.settings; + +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; /** * Settings for the proof caching functionality. @@ -11,15 +13,21 @@ public class ProofCachingSettings extends AbstractPropertiesSettings { public static final String DISPOSE_COPY = "Copy steps into new proof"; public static final String DISPOSE_REOPEN = "Reopen proof"; + public static final String PRUNE_COPY = "Copy steps just before prune"; + public static final String PRUNE_REOPEN = "Reopen cached goal(s)"; /** * Key ID for {@link #enabled}. */ private static final String ENABLED_KEY = "Enabled"; /** - * Key ID for {@link #enabled}. + * Key ID for {@link #dispose}. */ private static final String DISPOSE_KEY = "Dispose"; + /** + * Key ID for {@link #prune}. + */ + private static final String PRUNE_KEY = "Prune"; /** @@ -32,6 +40,11 @@ public class ProofCachingSettings extends AbstractPropertiesSettings { */ private final AbstractPropertiesSettings.PropertyEntry dispose = createStringProperty(DISPOSE_KEY, ""); + /** + * Behaviour when pruning a proof that is referenced elsewhere. + */ + private final AbstractPropertiesSettings.PropertyEntry prune = + createStringProperty(PRUNE_KEY, ""); public ProofCachingSettings() { super("ProofCaching"); @@ -63,4 +76,23 @@ public String getDispose() { public void setDispose(String operation) { dispose.set(operation); } + + /** + * Returns the current setting for behaviour when pruning into referenced branches. + * + * @return either an empty string, {@link #PRUNE_REOPEN} or {@link #PRUNE_COPY} + */ + public String getPrune() { + return prune.get(); + } + + /** + * Set the operation to be done when a referenced proof is pruned. + * Allowed operations: {@link #PRUNE_REOPEN}, {@link #PRUNE_COPY}. + * + * @param operation the operation + */ + public void setPrune(String operation) { + prune.set(operation); + } } diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/toolbar/CachingToggleAction.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/toolbar/CachingToggleAction.java new file mode 100644 index 00000000000..70dde29a490 --- /dev/null +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/toolbar/CachingToggleAction.java @@ -0,0 +1,44 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.caching.toolbar; + +import java.awt.event.ActionEvent; +import javax.swing.*; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.gui.actions.MainWindowAction; +import de.uka.ilkd.key.gui.fonticons.IconFactory; + +/** + * Action to enable/disable Proof Caching. + * + * @author Arne Keller + */ +public class CachingToggleAction extends MainWindowAction { + public static final Icon ICON = + IconFactory.keyCachedClosed((int) IconFactory.DEFAULT_SIZE, (int) IconFactory.DEFAULT_SIZE); + private static final String DESCRIPTION = + "Enable or disable proof caching for currently open proofs."; + + public CachingToggleAction(MainWindow mainWindow) { + super(mainWindow); + + setName("Proof Caching"); + setMenuPath("Options"); + setEnabled(true); + setSelected(true); + putValue(Action.LONG_DESCRIPTION, DESCRIPTION); + // for main menu variant of action + putValue(KeyAction.CHECKBOX, true); + setTooltip(DESCRIPTION); + + setIcon(ICON); + } + + @Override + public void actionPerformed(ActionEvent e) { + // no action, status of checkbox is checked in extension class + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java similarity index 95% rename from key.core/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java index 67dc6694f36..16ed8b2a958 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java @@ -21,7 +21,8 @@ public class ProgramMethodFinder implements Visitor { @Override public boolean visitSubtree(Term visited) { - return false; + // visit all sub-terms + return true; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java similarity index 76% rename from key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java index 0f135a28465..14b5265c330 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java @@ -16,6 +16,9 @@ import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.merge.CloseAfterMerge; +import org.key_project.slicing.DependencyTracker; +import org.key_project.slicing.analysis.AnalysisResults; + /** * Utility class for proof caching. * @@ -42,22 +45,19 @@ public static ClosedBy findPreviousProof(List previousProofs, Node newNod for (int i = 0; i < previousProofs.size(); i++) { Proof p = previousProofs.get(i); if (p == newNode.proof()) { - continue; // doesn't make sense + continue; // doesn't make sense to cache in the same proof } // conservative check: all user-defined rules in a previous proof // have to also be available in the new proof var proofFile = p.getProofFile() != null ? p.getProofFile().toString() : "////"; var tacletIndex = p.allGoals().head().ruleAppIndex().tacletIndex(); var newTacletIndex = newNode.proof().allGoals().head().ruleAppIndex().tacletIndex(); - Set newTaclets = null; + Set newTaclets = newTacletIndex.allNoPosTacletApps(); var tacletsOk = true; for (var taclet : tacletIndex.allNoPosTacletApps().stream() .filter(x -> x.taclet().getOrigin() != null && x.taclet().getOrigin().contains(proofFile)) .toList()) { - if (newTaclets == null) { - newTaclets = newTacletIndex.allNoPosTacletApps(); - } if (newTaclets.stream().noneMatch(newTaclet -> Objects .equals(taclet.taclet().toString(), newTaclet.taclet().toString()))) { tacletsOk = false; @@ -84,6 +84,17 @@ public static ClosedBy findPreviousProof(List previousProofs, Node newNod } return n; }).filter(Objects::nonNull).collect(Collectors.toCollection(ArrayDeque::new)); + var depTracker = p.lookup(DependencyTracker.class); + AnalysisResults results = null; + // only try to get analysis results if it is a pure proof + if (depTracker != null && p.closedGoals().stream() + .noneMatch(x -> x.node().lookup(ClosedBy.class) != null)) { + try { + results = depTracker.analyze(true, false); + } catch (Exception ignored) { + // if the analysis for some reason fails, we simply proceed as usual + } + } while (!nodesToCheck.isEmpty()) { // for each node, check that the sequent in the reference is // a subset of the new sequent @@ -100,14 +111,28 @@ public static ClosedBy findPreviousProof(List previousProofs, Node newNod if (n.parent() != null) { nodesToCheck.add(n.parent()); } - Semisequent ante = n.sequent().antecedent(); - Semisequent succ = n.sequent().succedent(); + Sequent seq = n.sequent(); + if (results != null) { + seq = results.reduceSequent(n); + } + Semisequent ante = seq.antecedent(); + Semisequent succ = seq.succedent(); Semisequent anteNew = newNode.sequent().antecedent(); Semisequent succNew = newNode.sequent().succedent(); if (!containedIn(anteNew, ante) || !containedIn(succNew, succ)) { continue; } - return new ClosedBy(p, n); + Set toSkip = new HashSet<>(); + if (results != null) { + // computed skipped nodes by iterating through all nodes + AnalysisResults finalResults = results; + n.subtreeIterator().forEachRemaining(x -> { + if (!finalResults.usefulSteps.contains(x)) { + toSkip.add(x); + } + }); + } + return new ClosedBy(p, n, toSkip); } } return null; @@ -149,9 +174,13 @@ public static boolean suitableForCloseByReference(Node node) { Sequent seq = node.sequent(); for (int i = 1; i <= seq.size(); i++) { Term term = seq.getFormulabyNr(i).formula(); + // first, check for a java block if (term.containsJavaBlockRecursive()) { + // not suitable for caching return false; } + // then, check for program methods + // (may expand differently depending on Java code associated with proofs) term.execPreOrder(f); if (f.getFoundProgramMethod()) { return false; diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java b/keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java similarity index 85% rename from key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java rename to keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java index 82c9358249b..047eb9b2e2f 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java +++ b/keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.GeneralSettings; +import org.key_project.slicing.DependencyTracker; import org.key_project.util.helper.FindResources; import org.junit.jupiter.api.Test; @@ -79,6 +80,24 @@ void testFindsReferenceInSameProof() throws Exception { Proof proof = foundReference.proof(); CopyReferenceResolver.copyCachedGoals(proof, p2, null, null); assertTrue(p.closed()); + + assertNotEquals(55, foundReference.serialNr()); + // test that copying with slicing information works + new DependencyTracker(p2); + Node n55 = p.findAny(x -> x.serialNr() == 55); + assertTrue(ReferenceSearcher.suitableForCloseByReference(n55)); + ClosedBy n55Close = ReferenceSearcher.findPreviousProof(previousProofs, n55); + assertEquals(n55.serialNr(), n55Close.node().serialNr()); + assertSame(p2, n55Close.proof()); + int previousTotal = p.countNodes(); + n55.register(n55Close, ClosedBy.class); + p.pruneProof(n55); + p.closeGoal(p.getOpenGoal(n55)); + assertTrue(p.closed()); + n55.proof().copyCachedGoals(p2, null, null); + assertTrue(p.closed()); + assertEquals(previousTotal - 4, p.countNodes()); + GeneralSettings.noPruningClosed = true; p.dispose(); p2.dispose(); diff --git a/key.core/src/test/resources/testcase/proofCaching/proofWithRule.proof b/keyext.caching/src/test/resources/testcase/proofCaching/proofWithRule.proof similarity index 100% rename from key.core/src/test/resources/testcase/proofCaching/proofWithRule.proof rename to keyext.caching/src/test/resources/testcase/proofCaching/proofWithRule.proof diff --git a/key.core/src/test/resources/testcase/proofCaching/proofWithoutRule.proof b/keyext.caching/src/test/resources/testcase/proofCaching/proofWithoutRule.proof similarity index 100% rename from key.core/src/test/resources/testcase/proofCaching/proofWithoutRule.proof rename to keyext.caching/src/test/resources/testcase/proofCaching/proofWithoutRule.proof diff --git a/keyext.slicing/build.gradle b/keyext.slicing/build.gradle index 1555494e063..c448ade9d8c 100644 --- a/keyext.slicing/build.gradle +++ b/keyext.slicing/build.gradle @@ -1,5 +1,3 @@ -description "Computiation of the proof core (the essential rule applications to close a proof)" - dependencies { implementation project(":key.core") implementation project(":key.ui") diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index 32034724837..05440bcca99 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -64,6 +64,10 @@ public DependencyTracker(Proof proof) { if (!SlicingSettingsProvider.getSlicingSettings().getAlwaysTrack()) { return; } + // exotic use case: registering a dependency tracker after the proof is loaded + if (proof.countNodes() > 1) { + graph.ensureProofIsTracked(proof); + } proof.addRuleAppListener(this); } @@ -404,10 +408,12 @@ public void proofIsBeingPruned(ProofTreeEvent e) { * See {@link DotExporter}. * * @param abbreviateFormulas whether to shorten formula labels + * @param abbreviateChains whether to reduce long chains to one link * @return DOT string */ - public String exportDot(boolean abbreviateFormulas) { - return DotExporter.exportDot(proof, graph, analysisResults, abbreviateFormulas); + public String exportDot(boolean abbreviateFormulas, boolean abbreviateChains) { + return DotExporter.exportDot(proof, abbreviateChains ? graph.removeChains() : graph, + analysisResults, abbreviateFormulas); } /** diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingProofReplayer.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingProofReplayer.java index 0927e990468..2e8fb3148d0 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingProofReplayer.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingProofReplayer.java @@ -231,13 +231,19 @@ private File saveProof(Proof currentProof, Proof proof) throws IOException { // proofs) filename = MiscTools.toValidFileName(filename); } - int prevSlice = filename.indexOf("_slice"); + String sliceSuffix = "_slice"; + int prevSlice = filename.indexOf(sliceSuffix); if (prevSlice != -1) { - int sliceNr = Integer.parseInt(filename.substring(prevSlice + "_slice".length())); - sliceNr++; - filename = filename.substring(0, prevSlice) + "_slice" + sliceNr; + var slicingIteration = filename.substring(prevSlice + sliceSuffix.length()); + if (slicingIteration.matches("\\d+")) { + int sliceNr = Integer.parseInt(slicingIteration); + sliceNr++; + filename = filename.substring(0, prevSlice) + sliceSuffix + sliceNr; + } else { + filename = filename + sliceSuffix + "1"; + } } else { - filename = filename + "_slice1"; + filename = filename + sliceSuffix + "1"; } filename = filename + ".proof"; File tempFile = tempDir.resolve(filename).toFile(); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/AnalysisResults.java b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/AnalysisResults.java index 8a46fada1f1..0b0e0b0e578 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/AnalysisResults.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/AnalysisResults.java @@ -3,11 +3,17 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.slicing.analysis; +import java.util.ArrayList; import java.util.Collections; import java.util.List; import java.util.Map; import java.util.Set; +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.PosInTerm; +import de.uka.ilkd.key.logic.Semisequent; +import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.logic.SequentFormula; import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -16,6 +22,7 @@ import org.key_project.slicing.RuleStatistics; import org.key_project.slicing.SlicingProofReplayer; import org.key_project.slicing.SlicingSettingsProvider; +import org.key_project.slicing.graph.DependencyGraph; import org.key_project.slicing.graph.GraphNode; import org.key_project.slicing.util.ExecutionTime; @@ -30,6 +37,7 @@ public final class AnalysisResults { * The analyzed proof. */ public final Proof proof; + public final DependencyGraph dependencyGraph; /** * Total amount of rule applications. */ @@ -84,6 +92,7 @@ public final class AnalysisResults { * Specify the results of analyzing a proof. * * @param proof the analyzed proof + * @param dependencyGraph the dependency graph of the proof * @param totalSteps the number of steps in the proof * @param ruleStatistics statistics on analyzed rules * @param usefulSteps set of useful steps to include in the slice @@ -96,6 +105,7 @@ public final class AnalysisResults { */ public AnalysisResults( Proof proof, + DependencyGraph dependencyGraph, int totalSteps, RuleStatistics ruleStatistics, Set usefulSteps, @@ -106,6 +116,7 @@ public AnalysisResults( boolean didDeduplicateRuleApps, ExecutionTime executionTime) { this.proof = proof; + this.dependencyGraph = dependencyGraph; this.totalSteps = totalSteps; this.usefulStepsNr = usefulSteps.size(); this.ruleStatistics = ruleStatistics; @@ -139,6 +150,31 @@ public boolean indicateSlicingPotential() { return totalSteps > usefulStepsNr; } + /** + * Reduce the sequent of the provided node to formulas deemed useful. + * (Formulas are useful if they are used to close the branch.) + * + * @param node proof node + * @return sequent with only useful formulas + */ + public Sequent reduceSequent(Node node) { + final Sequent seq = node.sequent(); + return Sequent.createSequent(reduce(seq.antecedent(), node, true), + reduce(seq.succedent(), node, false)); + } + + private Semisequent reduce(Semisequent semi, Node node, boolean antec) { + var semiList = new ArrayList(); + for (SequentFormula sf : semi) { + var graphNode = dependencyGraph.getGraphNode(node.proof(), node.getBranchLocation(), + new PosInOccurrence(sf, PosInTerm.getTopLevel(), antec)); + if (usefulNodes.contains(graphNode)) { + semiList.add(sf); + } + } + return Semisequent.create(semiList); + } + @Override public String toString() { return "AnalysisResults{" + diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java index 862ea98e7a3..ec0eb122bec 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java @@ -243,7 +243,7 @@ public AnalysisResults analyze() { executionTime.stop(TOTAL_WORK); return new AnalysisResults( - proof, steps, rules, usefulSteps, usefulFormulas, uselessBranches, + proof, graph, steps, rules, usefulSteps, usefulFormulas, uselessBranches, branchStacks, doDependencyAnalysis, doDeduplicateRuleApps, executionTime); } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java index dcf39c0dd19..0b1b1f08388 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedEdge.java @@ -34,7 +34,7 @@ public AnnotatedEdge(Node proofStep, boolean consumesInput) { } /** - * @return tte node that added this edge to the dependency graph + * @return the node that added this edge to the dependency graph */ public Node getProofStep() { return proofStep; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedShortenedEdge.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedShortenedEdge.java new file mode 100644 index 00000000000..07f8752ec9d --- /dev/null +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/AnnotatedShortenedEdge.java @@ -0,0 +1,60 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.slicing.graph; + +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.rule.RuleApp; + +/** + * An annotated edge representing a chain of real proof nodes. + * + * @author Arne Keller + */ +public class AnnotatedShortenedEdge extends AnnotatedEdge { + /** + * The initial node in this shortened chain. + */ + private final Node initial; + /** + * The last node in this shortened chain. + */ + private final Node last; + + /** + * Create a new shortened edge. + * + * @param initial the initial node for this shortened chain + * @param last the last node of this shortened chain + * @param consumesInput whether the input graph node is consumed + */ + public AnnotatedShortenedEdge(Node initial, Node last, boolean consumesInput) { + super(last, consumesInput); + this.initial = initial; + this.last = last; + } + + /** + * Get the proper label for this edge. + * Will list both the initial and the last node's ruleapp. + * + * @return label for this edge (to use in DOT export) + */ + public String getEdgeLabel() { + var sb = new StringBuilder(); + RuleApp ruleApp1 = initial.getAppliedRuleApp(); + if (ruleApp1 != null) { + sb.append(ruleApp1.rule().displayName()).append("_").append(initial.serialNr()); + sb.append(" ... "); + } + RuleApp ruleApp2 = last.getAppliedRuleApp(); + if (ruleApp2 != null) { + sb.append(ruleApp2.rule().displayName()).append("_").append(last.serialNr()); + } + return sb.toString(); + } + + public Node getInitial() { + return initial; + } +} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index cc08cd743ce..8d8fa7a9aa3 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -5,6 +5,7 @@ import java.util.*; import java.util.stream.Stream; +import java.util.stream.StreamSupport; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.proof.BranchLocation; @@ -33,21 +34,28 @@ * @author Arne Keller */ public class DependencyGraph { - /** - * Logger. - */ private static final Logger LOGGER = LoggerFactory.getLogger(DependencyGraph.class); /** * Main storage container of graph nodes and edges. */ - private final EquivalenceDirectedGraph graph = new EquivalenceDirectedGraph(); + private final EquivalenceDirectedGraph graph; /** * Mapping of rule applications to graph edges. * Stores the edges introduced by a proof step. */ private final Map> edgeDataReversed = new IdentityHashMap<>(); + public DependencyGraph() { + graph = new EquivalenceDirectedGraph(); + } + + private DependencyGraph(DependencyGraph copyFrom) { + graph = copyFrom.graph.copy(); + graph.edgeSet().forEach(x -> edgeDataReversed + .computeIfAbsent(x.getProofStep(), _node -> new ArrayList<>()).add(x)); + } + /** * Ensure the provided proof is fully represented in this dependency graph. * @@ -68,7 +76,6 @@ public void ensureProofIsTracked(Proof p) { } } - /** * Add a rule application to the dependency graph. * @@ -216,13 +223,13 @@ public Stream neighborsOf(GraphNode node) { /** * Gets all the edges representing the supplied proof step. - * May be used to reconstruct the hyperedge corresponding to the proof step. + * The combination of these represents the hyperedge corresponding to the proof step. * * @param proofStep the proof step * @return the edges representing this step */ public Collection edgesOf(Node proofStep) { - return edgeDataReversed.get(proofStep); + return edgeDataReversed.getOrDefault(proofStep, Collections.emptyList()); } /** @@ -360,4 +367,85 @@ public record NodeData(Node /* proofStep */ first, GraphNode /* edgeSource */ se AnnotatedEdge /* edge */ third) { } + + /** + * Remove all nodes B with degree 2: + * A → B → C + * + * @return modified copy + */ + public DependencyGraph removeChains() { + // first, create a copy of the graph + var nGraph = new DependencyGraph(this); + // get all nodes in the proof + var allNodes = proof().root().subtreeIterator(); + // take the outputs "produced" by the nodes + var toCheck = StreamSupport.stream(Spliterators.spliteratorUnknownSize(allNodes, 0), false) + .flatMap(this::outputsOf).toList(); + int removed = 0; + // toCheck now contains dependency graph nodes + // (TrackedFormulas etc.) + for (var node : toCheck) { + var incoming = nGraph.incomingGraphEdgesOf(node).toList(); + var outgoing = nGraph.outgoingGraphEdgesOf(node).toList(); + if (incoming.size() != 1 || outgoing.size() != 1) { + continue; + } + // we want to remove the incoming edge. + // that edge is part of a node startNode, + // whose hyperedge should not connect more nodes + // (otherwise we cannot remove the edge without + // making the graph inconsistent) + Node startNode = incoming.get(0).first; + if (edgesOf(startNode).size() != 1) { + continue; + } + GraphNode startGraphNode = incoming.get(0).second; + AnnotatedEdge edge = incoming.get(0).third; + + // get real initial node + // (in case of repeated shortenings) + Node initialNode = startNode; + if (edge instanceof AnnotatedShortenedEdge ase) { + initialNode = ase.getInitial(); + } + + // we want to remove the outgoing edge. + // that edge is part of a node endNode, + // whose hyperedge should not connect more nodes + // (otherwise we cannot remove the edge without + // making the graph inconsistent) + Node endNode = outgoing.get(0).first; + GraphNode endGraphNode = outgoing.get(0).second; + var edge2 = outgoing.get(0).third; + if (edgesOf(endNode).size() != 1) { + continue; + } + + // situation: + // startGraphNode ---> node ---> endGraphNode + + // chain removal: + // remove node and connected edges + nGraph.graph.removeVertex(node); + // create new edge + var edge3 = new AnnotatedShortenedEdge(initialNode, endNode, edge.replacesInputNode()); + nGraph.graph.addEdge(startGraphNode, endGraphNode, edge3); + nGraph.edgeDataReversed.remove(startNode); + nGraph.edgeDataReversed.get(endNode).remove(edge2); + nGraph.edgeDataReversed.get(endNode).add(edge3); + removed++; + } + LOGGER.debug("removeChains: {} nodes deleted", removed); + return nGraph; + } + + /** + * The proof associated with this graph. May be null if the graph is empty. + * + * @return the proof + */ + public Proof proof() { + return this.edgeDataReversed.keySet().stream().map(Node::proof).findFirst().orElse(null); + } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java index 1a6ac1c5255..c217ae3f370 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DotExporter.java @@ -4,6 +4,7 @@ package org.key_project.slicing.graph; import java.util.ArrayList; +import java.util.Collection; import java.util.HashSet; import java.util.IdentityHashMap; import java.util.List; @@ -63,11 +64,12 @@ public static String exportDot( while (!queue.isEmpty()) { Node node = queue.remove(queue.size() - 1); node.childrenIterator().forEachRemaining(queue::add); - DependencyNodeData data = node.lookup(DependencyNodeData.class); - if (data == null) { + var edges = graph.edgesOf(node); + var data = node.lookup(DependencyNodeData.class); + if (edges == null || edges.isEmpty() || data == null) { continue; } - outputEdge(buf, analysisResults, abbreviateFormulas, false, node, data); + outputEdge(buf, analysisResults, abbreviateFormulas, false, node, data, edges); } // colorize useless nodes if (analysisResults != null) { @@ -197,4 +199,57 @@ private static void outputEdge(StringBuilder buf, AnalysisResults analysisResult } } } + + private static void outputEdge(StringBuilder buf, AnalysisResults analysisResults, + boolean abbreviateFormulas, boolean omitBranch, Node node, DependencyNodeData data, + Collection edges) { + for (var edge : edges) { + var in = ((GraphNode) edge.getSource()); + var out = ((GraphNode) edge.getTarget()); + // input node label + String inString = in.toString(abbreviateFormulas, omitBranch); + // output node label + String outString = out.toString(abbreviateFormulas, omitBranch); + // label for edge itself + String label = data.label; + if (edge instanceof AnnotatedShortenedEdge ase) { + label = ase.getEdgeLabel(); + } + buf + .append('"') + .append(inString) + .append("\" -> \"") + .append(outString) + .append("\" [label=\"") + .append(label); + // mark useless steps / formulas in red + if (analysisResults != null + && !analysisResults.usefulSteps.contains(node)) { + buf.append("\" color=\"red"); + } + buf + .append("\"]\n"); + if (analysisResults != null) { + if (!analysisResults.usefulNodes.contains(in)) { + buf.append('"').append(inString).append('"') + .append(" [color=\"red\"]\n"); + } + if (!analysisResults.usefulNodes.contains(out)) { + buf.append('"').append(outString).append('"') + .append(" [color=\"red\"]\n"); + } + } + // make sure the formulas are drawn with the correct shape + String shape = SHAPES.get(in.getClass()); + if (shape != null) { + buf.append('"').append(inString).append("\" [shape=\"").append(shape) + .append("\"]\n"); + } + shape = SHAPES.get(out.getClass()); + if (shape != null) { + buf.append('"').append(outString).append("\" [shape=\"").append(shape) + .append("\"]\n"); + } + } + } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/EquivalenceDirectedGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/EquivalenceDirectedGraph.java index 983bae40599..dcfc8e179cc 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/EquivalenceDirectedGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/EquivalenceDirectedGraph.java @@ -67,4 +67,15 @@ public Collection getVerticesModProofIrrelevancy(GraphNode v) { return List.of(v); } } + + public EquivalenceDirectedGraph copy() { + var g = new EquivalenceDirectedGraph(); + for (var vertex : vertexSet()) { + g.addVertex(vertex); + } + for (var edge : edgeSet()) { + g.addEdge((GraphNode) edge.getSource(), (GraphNode) edge.getTarget(), edge); + } + return g; + } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java index 53aa579d151..6af1fb82d77 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java @@ -138,6 +138,10 @@ public class SlicingLeftPanel extends JPanel implements TabPanel, KeYSelectionLi * Checkbox to abbreviate formulas in DOT output. */ private JCheckBox abbreviateFormulas = null; + /** + * Checkbox to shorten chains in DOT output. + */ + private JCheckBox abbreviateChains = null; /** * Checkbox to enable the dependency analysis algorithm. */ @@ -286,7 +290,14 @@ private JPanel getDependencyGraphPanel() { panel1.setLayout(new BoxLayout(panel1, BoxLayout.Y_AXIS)); panel1.setBorder(new TitledBorder("Dependency graph")); - abbreviateFormulas = new JCheckBox("Abbreviate formulas"); + abbreviateFormulas = new JCheckBox("Abbreviate node labels"); + abbreviateFormulas.setToolTipText("Replace node labels with their hash value."); + abbreviateChains = new JCheckBox("Shorten long chains"); + abbreviateChains.setToolTipText(""" + Collapse long chains when rendering the graph. + When enabled: dependency graph nodes with both input and output degree equal to one + will be collapsed. + These shortened edges are labeled by: initial step ... last step"""); dotExport = new JButton("Export as DOT"); dotExport.addActionListener(this::exportDot); showGraphRendering = new JButton("Show rendering of graph"); @@ -303,12 +314,14 @@ private JPanel getDependencyGraphPanel() { resetGraphLabels(); abbreviateFormulas.setAlignmentX(Component.LEFT_ALIGNMENT); + abbreviateChains.setAlignmentX(Component.LEFT_ALIGNMENT); dotExport.setAlignmentX(Component.LEFT_ALIGNMENT); showGraphRendering.setAlignmentX(Component.LEFT_ALIGNMENT); panel1.add(graphNodes); panel1.add(graphEdges); panel1.add(abbreviateFormulas); + panel1.add(abbreviateChains); panel1.add(dotExport); panel1.add(showGraphRendering); @@ -348,7 +361,7 @@ private void exportDot(ActionEvent event) { try (BufferedWriter writer = new BufferedWriter( new OutputStreamWriter(new FileOutputStream(file), StandardCharsets.UTF_8))) { String text = extension.trackers.get(currentProof) - .exportDot(abbreviateFormulas.isSelected()); + .exportDot(abbreviateFormulas.isSelected(), abbreviateChains.isSelected()); writer.write(text); } catch (IOException e) { LOGGER.error("failed to export DOT file", e); @@ -374,7 +387,7 @@ private void previewGraph(ActionEvent e) { return; } String text = extension.trackers.get(currentProof) - .exportDot(abbreviateFormulas.isSelected()); + .exportDot(abbreviateFormulas.isSelected(), abbreviateChains.isSelected()); new PreviewDialog(MainWindow.getInstance(), text); } diff --git a/recoder/build.gradle b/recoder/build.gradle index 3e0bbf39ec6..27147e285c5 100644 --- a/recoder/build.gradle +++ b/recoder/build.gradle @@ -11,5 +11,5 @@ dependencies { implementation 'net.sf.retrotranslator:retrotranslator-transformer:1.2.9' testCompileOnly 'junit:junit:4.13.2' - testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.1' + testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.2' } \ No newline at end of file diff --git a/settings.gradle b/settings.gradle index e71fc368308..0f65c7fe42c 100644 --- a/settings.gradle +++ b/settings.gradle @@ -13,3 +13,4 @@ include 'keyext.ui.testgen' include 'keyext.proofmanagement' include 'keyext.exploration' include 'keyext.slicing' +include 'keyext.caching'