diff --git a/AGENT.md b/AGENT.md new file mode 100644 index 00000000000..f1065315eea --- /dev/null +++ b/AGENT.md @@ -0,0 +1,217 @@ +# Agent Guidelines for KeY Project + +This document provides guidelines and rules for AI agents working on the KeY deductive Java program verifier project. + +## Project Overview + +**KeY** is an interactive theorem prover for formal verification and analysis of Java programs. It supports: +- Formal verification of Java programs with Java Modeling Language specifications +- Symbolic program execution +- First-order reasoning +- Test case generation + +**License**: GPL v2 (all contributions must be compatible) + +## Technical Stack + +### Build System +- **Gradle** with Groovy DSL (`build.gradle`) +- Multi-module project structure +- Java 21 compatibility required + +```bash +# Common build commands +./gradlew classes # Compile all classes +./gradlew testClasses # Compile all test classes +./gradlew test # Run full test suite (hours) +./gradlew testFast # Run lightweight tests (minutes) +./gradlew spotlessApply # Reformat source code +./gradlew :key.:test --tests "." # Specific test +./gradlew :key.ui:run # Run KeY UI +./gradlew :key.ui:run --args='--experimental' # With experimental features +./gradlew :key.ui:shadowJar # Create fat jar +``` + +### Key Technologies +- **Java 21** (source/target compatibility) +- **JUnit 6** (Jupiter) for testing +- **AssertJ** for assertions +- **SLF4J** with Logback for logging +- **Spotless** for code formatting +- **ANTLR 4** for parser generation + +### Dependencies Management +- Version Catalog (`libs.*` notation in build files) +- All dependencies must be on Maven Central repository +- Use JSpecify for nullability annotations + +## Project Structure + +### Core Modules +``` +key.util - Base utilities +key.core - Core verification engine +key.ui - GUI application +key.ncore - Logic layer +key.ncore.* - Calculus layers +``` +Extension Modules are marked by name `keyext.*` + +### Module Naming Convention +- Base components: `key.*` +- Extensions/plugins: `keyext.*` +- Follow Maven standard directory layout + +## Coding Conventions + +### Java Code Style +- Follow [Java Code Conventions](https://keyproject.github.io/key-docs/devel/CodingConventions/) +- Use Spotless plugin for automatic formatting +- Indentation: 4 spaces (no tabs) +- Line length: Reasonable limits (typically 120 chars) +- Braces: Always use braces for control structures + +### Package Structure +- Root packages: `de.uka.ilkd.key.*`, `org.key_project.*` +- Keep related classes in same package +- Avoid circular dependencies between modules + +### Documentation +- JavaDoc for public APIs +- Inline comments for complex logic +- Reference official docs: https://keyproject.github.io/key-docs/devel/ + +## Testing Guidelines + +### Test Organization +- Tests in `src/test/java` mirroring source structure +- Test fixtures in `src/testFixtures/java` +- Use JUnit 5 Jupiter API +- Prefer AssertJ for fluent assertions + +### Writing Tests +```java +// Example pattern +@Test +void shouldVerifyExpectedBehavior() { + // Given + // When + // Then - use AssertJ + assertThat(result).isEqualTo(expected); +} +``` + +### Running Tests +- Use `testFast` for quick feedback during development +- Use `test` before committing (comprehensive but slow) +- Debug with: `./gradlew test --debug-jvm` (attach at localhost:5005) + +## Quality Assurance + +### Automated Checks +All PRs are automatically checked via GitHub Actions: +- Unit tests execution +- Code formatting (Spotless) +- Static analysis (Checker Framework, SonarQube) +- License compliance + +### Pre-commit Checklist +1. Code compiles: `./gradlew classes` +2. Tests pass: `./gradlew testFast` +3. Reformatting: `./gradlew spotlessApply` +4. No new warnings introduced +5. GPL v2 license compatibility verified + +## Development Workflow + +### Branch Strategy +- Feature branches from main +- Descriptive branch names (e.g., `lastname/xxx`, `feature/xxx`, `fix/yyy`) +- Releases are in `releases/` and pre-releases in `prerelease/` +- Rebase before merging to keep history clean + +### Commit Messages +- Clear, descriptive messages +- Reference issues when applicable +- Follow conventional commits pattern + +### Pull Requests +1. Fork and create feature branch +2. Implement changes with tests +3. Ensure all CI checks pass +4. Open PR with clear description +5. Address review feedback +6. Squash/rebase as requested + +## Architecture Principles + +### Core Design +- Separation of concerns between layers +- Immutable data structures where possible +- Thread-safety considerations documented +- Performance-critical code profiled + +### Key Components +- **Proof Engine**: Sequent calculus-based theorem proving +- **SMT Integration**: Z3, cvc5, Princess solvers +- **GUI**: Java Swing with FlatLaf look-and-feel + +## Tools & Resources + +### Essential Links +- Homepage: https://key-project.org +- Developer Docs: https://keyproject.github.io/key-docs/devel/ +- Issue Tracker: https://github.com/KeYProject/key/issues +- Mailing List: key-all@lists.informatik.kit.edu + +### IDE Setup +- IntelliJ IDEA recommended (project includes `.idea` configs) +- Eclipse supported via gradle eclipse plugin +- Enable annotation processing for Checker Framework + +## Agent-Specific Rules + +### When Making Changes +1. **Understand context first**: Read existing code, tests, and documentation +2. **Follow patterns**: Match existing code style and architecture +3. **Test incrementally**: Verify each change compiles and tests pass +4. **Document decisions**: Add comments explaining non-obvious choices +5. **Respect licensing**: All code must be GPL v2 compatible + +### Communication +- Be explicit about assumptions and limitations +- Provide complete, functional code (no placeholders) +- Include usage examples when adding new features +- Reference relevant documentation or prior art + +### Code Review Expectations +- Manual review by core team required +- Automated checks must pass first +- Be prepared to iterate based on feedback +- Maintain backward compatibility when possible + +## Common Tasks Reference + +### Adding a New Module +1. Create directory following pattern: `key.module.name/` +2. Add to `settings.gradle` +3. Configure `build.gradle` with dependencies +4. Apply standard plugins (java, spotless, checkerframework) + +### Modifying Build Configuration +1. Edit root `build.gradle` for global changes +2. Edit subproject `build.gradle` for module-specific changes +3. Update version catalog if adding dependencies +4. Test build locally before committing + +### Debugging Issues +1. Check existing issues/PRs for similar problems +2. Enable debug logging +3. Use debugger attachment (localhost:5005) +4. Consult developer documentation +5. Ask on mailing list if stuck + +--- + +*Last updated: August 2026* +*For questions, refer to the [KeY Developer Documentation](https://keyproject.github.io/key-docs/devel/)* diff --git a/key.core/src/main/antlr4/JavaKeYLexer.g4 b/key.core/src/main/antlr4/JavaKeYLexer.g4 index 0db9a8b65cf..e7b20c7c01d 100644 --- a/key.core/src/main/antlr4/JavaKeYLexer.g4 +++ b/key.core/src/main/antlr4/JavaKeYLexer.g4 @@ -60,6 +60,8 @@ ADD_ANNOTATION : '\\addAnnotation'; REMOVE_ANNOTATION : '\\removeAnnotation'; // label occurs again for character `!' NOTFREEIN : '\\notFreeIn'; +ISBINDINGEXPR : '\\isBindingExpr'; +ALWAYS_ABNORMALLY_TERMINATES: '\\alwaysAbnormallyTerminates'; STATIC : '\\static'; STATICMETHODREFERENCE : '\\staticMethodReference'; MAXEXPANDMETHOD : '\\mayExpandMethod'; diff --git a/key.core/src/main/antlr4/JavaKeYParser.g4 b/key.core/src/main/antlr4/JavaKeYParser.g4 index d81ac37299f..166a3b14f69 100644 --- a/key.core/src/main/antlr4/JavaKeYParser.g4 +++ b/key.core/src/main/antlr4/JavaKeYParser.g4 @@ -247,6 +247,8 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. | STRICT ISSUBTYPE | DISJOINTMODULONULL | NOTFREEIN + | ISBINDINGEXPR + | ALWAYS_ABNORMALLY_TERMINATES | HASSORT | NEWLABEL | ISREFERENCE diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java index 496bf1b5f54..e6c44ba9f80 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java @@ -9,11 +9,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.TypeConverter; -import de.uka.ilkd.key.java.ast.Comment; -import de.uka.ilkd.key.java.ast.PositionInfo; -import de.uka.ilkd.key.java.ast.ProgramElement; -import de.uka.ilkd.key.java.ast.ProgramElementWithKind; -import de.uka.ilkd.key.java.ast.SourceData; +import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.ast.expression.Operator; @@ -111,4 +107,12 @@ public boolean equals(Object o) { protected int computeHashCode() { return 0x01000193 * super.computeHashCode() + kind.hashCode(); } + + public Expression getLeft() { + return this.getExpressionAt(0); + } + + public Expression getRight() { + return this.getExpressionAt(1); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/InstanceofPattern.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/InstanceofPattern.java new file mode 100644 index 00000000000..afbdd3e13b9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/InstanceofPattern.java @@ -0,0 +1,143 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.java.ast.expression.operator; + +import java.util.List; +import java.util.Objects; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.declaration.VariableSpecification; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.ast.reference.TypeReference; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableArray; + +import org.jspecify.annotations.NullMarked; + +/** + * Instanceof with pattern matching (Java 16+). + * Supports syntax: expr instanceof Type varName + * where varName is bound as a local variable in the true branch. + */ +@NullMarked +public class InstanceofPattern extends TypeOperator { + protected final VariableSpecification patternVariable; + + public InstanceofPattern(ExtList children) { + super(children); + this.patternVariable = + Objects.requireNonNull(children.get(VariableSpecification.class)); + } + + public InstanceofPattern(Expression lhs, TypeReference type, VariableSpecification patternVar) { + super(lhs, type); + this.patternVariable = Objects.requireNonNull(patternVar); + } + + public InstanceofPattern(PositionInfo pi, List c, Expression lhs, TypeReference type, + VariableSpecification patternVar) { + super(pi, c, new ImmutableArray<>(lhs), type); + this.patternVariable = Objects.requireNonNull(patternVar); + } + + /** + * Returns the number of children of this node. + * + * @return an int giving the number of children of this node + */ + public int getChildCount() { + int result = 0; + if (children != null) { + result += children.size(); + } + if (typeReference != null) { + result++; + } + + result++; + assert result == 3; + return result; + } + + public SourceElement getLastElement() { + return patternVariable; + } + + /** + * Returns the child at the specified index in this node's "virtual" child array + * + * @param index an index into this node's "virtual" child array + * @return the program element at the given position + * @throws ArrayIndexOutOfBoundsException if index is out of bounds + */ + public ProgramElement getChildAt(int index) { + return switch (index) { + case 0 -> children.get(0); + case 1 -> typeReference; + case 2 -> patternVariable; + default -> throw new IllegalStateException("Unexpected value: " + index); + }; + } + + /** + * Get arity. + * + * @return the int value. + */ + public int getArity() { + return 1; + } + + /** + * Get precedence. + * + * @return the int value. + */ + public int getPrecedence() { + return 5; + } + + /** + * Get notation. + * + * @return the int value. + */ + public int getNotation() { + return POSTFIX; + } + + /** + * Get the pattern variable bound by this instanceof expression. + * + * @return the VariableSpecification for the pattern variable, or null if no pattern + */ + public VariableSpecification getPatternVariable() { + return patternVariable; + } + + /** + * calls the corresponding method of a visitor in order to perform some action/transformation on + * this element + * + * @param v the Visitor + */ + public void visit(Visitor v) { + v.performActionOnInstanceofPattern(this); + } + + public KeYJavaType getKeYJavaType(Services javaServ) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_BOOLEAN); + } + + public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { + return getKeYJavaType(javaServ); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index e378f9b2eb9..3c5122eeedc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java @@ -913,6 +913,31 @@ public Object visit(InstanceOfExpr n, Void arg) { List c = createComments(n); Expression lhs = accept(n.getExpression()); TypeReference type = requireTypeReference(n.getType()); + + if (n.getName().isPresent()) { + final SimpleName nName = n.getName().get(); + var name = nName.getIdentifier(); + + PositionInfo piVar = createPositionInfo(nName); + List cVar = createComments(nName); + + IProgramVariable pvar; + if (!name.startsWith("#")) { + pvar = new LocationVariable( + new ProgramElementName(name), type); + } else { + pvar = (ProgramSV) lookupSchemaVariable(nName); + } + + final var vs = + new VariableSpecification(piVar, cVar, null, pvar, 0, type.getKeYJavaType()); + return new InstanceofPattern(pi, c, lhs, type, vs); + } + + if (n.getPattern().isPresent()) { + reportUnsupportedElement(n); + } + return new Instanceof(pi, c, lhs, type); } @@ -2000,6 +2025,8 @@ yield reportError(n, case "#init-array-creation" -> new InitArrayCreation(labels.get(0), accept(n.getChild())); case "#reattachLoopInvariant" -> new ReattachLoopInvariant(accept(n.getChild())); + case "#posBinding" -> BindingsOfExpr.createPositive(accept(n.getChild())); + case "#negBinding" -> BindingsOfExpr.createNegative(accept(n.getChild())); default -> reportError(n, "Program meta construct " + n.getKind() + " unknown."); }; } @@ -2212,7 +2239,25 @@ public Object visit(RecordPatternExpr n, Void arg) { @Override public Object visit(TypePatternExpr n, Void arg) { - return reportUnsupportedElement(n); + // weigl: This is somehow crude and called by a type resolution in NameExpr, expecting a + // VariableDeclaration + var nName = n.getName(); + TypeRef type = accept(n.getType()); + var name = nName.getIdentifier(); + + PositionInfo piVar = createPositionInfo(nName); + List cVar = createComments(nName); + + IProgramVariable pvar; + if (!name.startsWith("#")) { + pvar = new LocationVariable( + new ProgramElementName(name), type); + } else { + pvar = (ProgramSV) lookupSchemaVariable(nName); + } + + ImmutableArray mods = map(n.getModifiers()); + return new LocalVariableDeclaration(mods, type, new VariableSpecification(pvar)); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java new file mode 100644 index 00000000000..f8df799d176 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/BindingVariableVisitor.java @@ -0,0 +1,190 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.java.visitor; + +import java.util.*; + +import de.uka.ilkd.key.java.ast.Statement; +import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; +import de.uka.ilkd.key.java.ast.declaration.VariableSpecification; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.ParenthesizedExpression; +import de.uka.ilkd.key.java.ast.expression.operator.*; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.logic.op.LocationVariable; + +/** + * + * @author Alexander Weigl + * @version 1 (20.08.26) + */ +public class BindingVariableVisitor { + public record Bindings(Map whenTrue, + Map whenFalse) { + public Bindings(Map whenTrue, + Map whenFalse) { + this.whenTrue = Collections.unmodifiableMap(whenTrue); + this.whenFalse = Collections.unmodifiableMap(whenFalse); + } + + static Bindings empty() { + return new Bindings(Map.of(), Map.of()); + } + + @Override + public String toString() { + return "Bindings{whenTrue=" + whenTrue + ", whenFalse=" + whenFalse + "}"; + } + } + + public static boolean binds(Expression e) { + if (e instanceof InstanceofPattern io) { + // §6.3.1.5 — a instanceof p + // "when true" = variables declared by p. No "when false" rule: + // it can't be determined at compile time that the match failed + // in a way that still binds anything. + return true; + } else if (e instanceof BinaryOperator bo) { + if (bo.getKind() == BinaryOperatorKind.LOGICAL_AND) { + // §6.3.1.1 — a && b + return binds(bo.getExpressionAt(0)) || binds(bo.getExpressionAt(1)); + } else if (bo.getKind() == BinaryOperatorKind.LOGICAL_OR) { + // §6.3.1.2 — a || b (mirror image of &&) + return binds(bo.getExpressionAt(0)) || binds(bo.getExpressionAt(1)); + } + } else if (e instanceof UnaryOperator not && not.kind == UnaryOperatorKind.LOGICAL_NOT) { + // §6.3.1.3 — !a: true/false swap. + return binds(not.getExpressionAt(0)); + } else if (e instanceof Conditional c) { + // §6.3.1.4 — a ? b : c + return binds(c.getExpressionAt(0)) + || binds(c.getExpressionAt(1)) + || binds(c.getExpressionAt(2)); + } else if (e instanceof ParenthesizedExpression p) { + // §6.3.1.7 — (a): pass through unchanged. + return binds(p.getExpressionAt(0)); + + } + return false; + } + + + public static Bindings analyze(Expression e) { + if (e instanceof InstanceofPattern io) { + // §6.3.1.5 — a instanceof p + // "when true" = variables declared by p. No "when false" rule: + // it can't be determined at compile time that the match failed + // in a way that still binds anything. + var name = (LocationVariable) io.getPatternVariable().getProgramVariable(); + Expression expr = io.getExpressionAt(0); + + // add a cast + expr = new TypeCast(expr, io.getTypeReference()); + + return new Bindings(Map.of(name, expr), Map.of()); + } else if (e instanceof BinaryOperator bo) { + if (bo.getKind() == BinaryOperatorKind.LOGICAL_AND) { + // §6.3.1.1 — a && b + Bindings a = analyze(bo.getExpressionAt(0)); + Bindings b = analyze(bo.getExpressionAt(1)); + + requireDisjoint(a.whenTrue, b.whenTrue, + "both operands of && declare pattern variable when true"); + requireDisjoint(a.whenFalse, b.whenFalse, + "both operands of && declare pattern variable when false"); + + // a's "when true" set is definitely matched at b (scope flows rightward). + var whenTrue = union(a.whenTrue, b.whenTrue); + // No rule for a && b when false: can't tell at compile time which + // operand caused the false result. + return new Bindings(whenTrue, Map.of()); + } else if (bo.getKind() == BinaryOperatorKind.LOGICAL_OR) { + // §6.3.1.2 — a || b (mirror image of &&) + Bindings a = analyze(bo.getExpressionAt(0)); + Bindings b = analyze(bo.getExpressionAt(1)); + + requireDisjoint(a.whenTrue, b.whenTrue, + "both operands of || declare pattern variable when true"); + requireDisjoint(a.whenFalse, b.whenFalse, + "both operands of || declare pattern variable when false"); + // a's "when false" set is definitely matched at b. + var whenFalse = union(a.whenFalse, b.whenFalse); + // No rule for a || b when true. + return new Bindings(Map.of(), whenFalse); + } + } else if (e instanceof UnaryOperator not && not.kind == UnaryOperatorKind.LOGICAL_NOT) { + // §6.3.1.3 — !a: true/false swap. + Bindings a = analyze(not.getExpressionAt(0)); + return new Bindings(a.whenFalse, a.whenTrue); + } else if (e instanceof Conditional c) { + // §6.3.1.4 — a ? b : c + Bindings condB = analyze(c.getExpressionAt(0)); + Bindings thenB = analyze(c.getExpressionAt(1)); + Bindings elseB = analyze(c.getExpressionAt(2)); + // (condB.whenTrue is definitely matched at b; condB.whenFalse at c — + // see DefinitelyMatchedAt below if you need those sets directly.) + + requireDisjoint(condB.whenTrue, elseB.whenTrue, + "cond(true) and else-branch(true) both declare pattern variable"); + requireDisjoint(condB.whenTrue, elseB.whenFalse, + "cond(true) and else-branch(false) both declare pattern variable"); + requireDisjoint(condB.whenFalse, thenB.whenTrue, + "cond(false) and then-branch(true) both declare pattern variable"); + requireDisjoint(condB.whenFalse, thenB.whenFalse, + "cond(false) and then-branch(false) both declare pattern variable"); + requireDisjoint(thenB.whenTrue, elseB.whenTrue, + "then-branch(true) and else-branch(true) both declare pattern variable"); + requireDisjoint(thenB.whenFalse, elseB.whenFalse, + "then-branch(false) and else-branch(false) both declare pattern variable"); + + + // No rule for introducing bindings from a ? b : c itself, in either + // direction: it can't be known at compile time whether a is true. + return Bindings.empty(); + } else if (e instanceof ParenthesizedExpression p) { + // §6.3.1.7 — (a): pass through unchanged. + return analyze(p.getExpressionAt(0)); + + } + return Bindings.empty(); + } + + private static Map union(Map a, + Map b) { + var result = new LinkedHashMap<>(a); + result.putAll(b); + return result; + } + + /** + * Turns a binding (a map from pattern variables to their cast expressions) into a sequence of + * local variable declarations of the form {@code Type var = (Type) expr;}. + *

+ * The declarations introduce the pattern variables of an {@code instanceof} pattern so that + * they are usable in the branch of a conditional in which the analyzed expression is known to + * evaluate to the corresponding truth value, see {@link #analyze(Expression)}. + * + * @param bindings a binding according to {@link Bindings#whenTrue()} or + * {@link Bindings#whenFalse()} + * @return one fresh {@link LocalVariableDeclaration} per bound pattern variable + */ + public static Statement[] toStatements(Map bindings) { + return bindings.entrySet().stream() + .map(entry -> new LocalVariableDeclaration( + new TypeRef(entry.getKey().getKeYJavaType()), + new VariableSpecification(entry.getKey(), entry.getValue(), + entry.getKey().getKeYJavaType()))) + .toArray(Statement[]::new); + } + + private static void requireDisjoint(Map a, + Map b, String message) { + for (LocationVariable name : a.keySet()) { + if (b.containsKey(name)) { + throw new IllegalStateException(message + ": '" + name + "'"); + } + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java index 02c1d1da7be..80a5c7c3a9f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -470,6 +470,17 @@ ProgramElement createNewElement(ExtList changeList) { def.doAction(x); } + @Override + public void performActionOnInstanceofPattern(InstanceofPattern x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new InstanceofPattern(changeList); + } + }; + def.doAction(x); + } + @Override public void performActionOnBreak(Break x) { DefaultAction def = new DefaultAction(x) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java index 7e36fed6fa7..6586265df93 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -250,6 +250,11 @@ public void performActionOnExactInstanceof(ExactInstanceof x) { doDefaultAction(x); } + @Override + public void performActionOnInstanceofPattern(InstanceofPattern x) { + doDefaultAction(x); + } + @Override public void performActionOnExecutionContext(ExecutionContext x) { doDefaultAction(x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index 4c9cf6d5f37..3ae4579c1b5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -164,6 +164,8 @@ void performActionOnAnnotationInterfaceMemberDeclaration( void performActionOnExactInstanceof(ExactInstanceof x); + void performActionOnInstanceofPattern(InstanceofPattern x); + void performActionOnNew(New x); void performActionOnTypeCast(TypeCast x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 561948361a6..8e8bf76e37d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -168,6 +168,13 @@ public void apply(TacletBuilder tacletBuilder, Object[] arguments, public static final TacletBuilderCommand NEW_LOCAL_VARS = new ConstructorBasedBuilder( "newLocalVars", NewLocalVarsCondition.class, SV, SV, SV, SV); + public static final TacletBuilderCommand ABNORMALLY_TERMINATE = new ConstructorBasedBuilder( + "alwaysAbnormallyTerminates", AbnormallyTerminatesCond.class, SV); + + public static final TacletBuilderCommand BINDING_EXPRESSION_SIMPLE = + new ConstructorBasedBuilder( + "isBindingExpr", BindingExpressionCond.class, SV); + static class NotFreeInTacletBuilderCommand extends AbstractTacletBuilderCommand { public NotFreeInTacletBuilderCommand(@NonNull ArgumentType... argumentsTypes) { super("notFreeIn", argumentsTypes); @@ -390,7 +397,8 @@ public IsLabeledCondition build(Object[] arguments, List parameters, STATIC_FIELD, MODEL_FIELD, SUBFORMULA, DROP_EFFECTLESS_STORES, EQUAL_UNIQUE, META_DISJOINT, IS_OBSERVER, CONSTANT, HAS_SORT, LABEL, NEW_LABEL, HAS_ELEM_SORT, IS_IN_STRICTFP, - HAS_ANNOTATION, ADD_ANNOTATION, REMOVE_ANNOTATION); + HAS_ANNOTATION, ADD_ANNOTATION, REMOVE_ANNOTATION, + BINDING_EXPRESSION_SIMPLE, ABNORMALLY_TERMINATE); register(STORE_TERM_IN, STORE_STMT_IN, HAS_INVARIANT, GET_INVARIANT, GET_FREE_INVARIANT, GET_VARIANT, IS_LABELED); loadWithServiceLoader(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index 4378aa041ae..ed45a9627aa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -1365,6 +1365,28 @@ public void performActionOnExactInstanceof(ExactInstanceof x) { printInstanceOfLike(x, "exactInstanceof"); } + @Override + public void performActionOnInstanceofPattern(InstanceofPattern x) { + boolean addParentheses = x.isToBeParenthesized(); + if (addParentheses) { + layouter.print("("); + } + if (x.getArguments() != null) { + x.getExpressionAt(0).visit(this); + } + layouter.print(" instanceof "); + if (x.getTypeReference() != null) { + x.getTypeReference().visit(this); + } + if (x.getPatternVariable() != null) { + layouter.print(" "); + x.getPatternVariable().visit(this); + } + if (addParentheses) { + layouter.print(")"); + } + } + @Override public void performActionOnNew(New x) { boolean addParentheses = x.isToBeParenthesized(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbnormallyTerminatesCond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbnormallyTerminatesCond.java new file mode 100644 index 00000000000..76db4c10a99 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbnormallyTerminatesCond.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, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.rule.conditions; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.Statement; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.VariableCondition; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.util.collection.ImmutableArray; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +/// This is a variable condition, that checks if a given variable binds new variables. +/// +/// @author Alexander Weigl +/// @version 1 (20.08.26) +public class AbnormallyTerminatesCond implements VariableCondition { + /// Is negated + private final boolean negated; + + /// A schema variable representing a Java Expression. + private final SchemaVariable svStmts; + + public AbnormallyTerminatesCond(SchemaVariable svStmts, boolean negated) { + this.svStmts = svStmts; + this.negated = negated; + } + + @Override + public @Nullable MatchResultInfo check( + @Nullable SchemaVariable var, @Nullable SyntaxElement instCandidate, + @NonNull MatchResultInfo matchCond, @NonNull LogicServices services) { + var svInst = (de.uka.ilkd.key.rule.inst.SVInstantiations) matchCond.getInstantiations(); + var s = svInst.getInstantiation(svStmts); + boolean isAbnormallyTerminating = false; + + var analysis = new AlwaysAbnormallyTerminatingAnalysis(null, (Services) services); + if (s instanceof ImmutableArray stmts) { + + } else if (s instanceof Statement stmts) { + + } else { + matchCond = null; + } + + + if (negated) { + return isAbnormallyTerminating ? null : matchCond; + } else { + return isAbnormallyTerminating ? matchCond : null; + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysis.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysis.java new file mode 100644 index 00000000000..8cf6c15a0e2 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysis.java @@ -0,0 +1,256 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.rule.conditions; + +import java.util.HashSet; +import java.util.LinkedList; +import java.util.Set; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.Label; +import de.uka.ilkd.key.java.ast.Statement; +import de.uka.ilkd.key.java.ast.StatementBlock; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.literal.BooleanLiteral; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperatorKind; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.ast.statement.*; + +import org.key_project.util.collection.ImmutableArray; + +import org.jspecify.annotations.Nullable; + +/// This analysis returns true iff a statement has the possibility to terminate normally +/// iff not every run terminates abnormally. +/// +class AlwaysAbnormallyTerminatingAnalysis { + + record TerminationReason(boolean isReturn, Set isThrow, String breakTo, + String continueTo) { + public TerminationReason(boolean isReturn) { + this(isReturn, Set.of(), null, null); + } + + public TerminationReason(KeYJavaType keYJavaType) { + this(false, Set.of(keYJavaType), null, null); + } + + public boolean isAbnormallTerminating() { + return isReturn || !isThrow.isEmpty() || breakTo != null && continueTo != null; + } + } + + private final KeYJavaType assertionException; + private final LinkedList

+ * This is the meta construct {@code #posBinding} (resp. {@code #negBinding}). Given a guard + * expression such as {@code obj instanceof String s} it produces the statement + * {@code String s = (String) obj;}: for {@code #posBinding} the declarations analysed by + * {@link BindingVariableVisitor#analyze(Expression)} in + * {@link BindingVariableVisitor.Bindings#whenTrue()}, + * for {@code #negBinding} those in {@link BindingVariableVisitor.Bindings#whenFalse()}. + */ +public final class BindingsOfExpr extends ProgramTransformer { + public final boolean positive; + + public BindingsOfExpr(String name, ProgramElement body, boolean positive) { + super(name, body); + assert body instanceof SchemaVariable; + this.positive = positive; + } + + public static BindingsOfExpr createPositive(ProgramElement body) { + return new BindingsOfExpr("#posBinding", body, true); + } + + public static BindingsOfExpr createNegative(ProgramElement body) { + return new BindingsOfExpr("#negBinding", body, false); + } + + @Override + public ProgramElement[] transform(ProgramElement pe, Services services, + SVInstantiations svInst) { + var sv = (SchemaVariable) super.body(); + var e = (Expression) svInst.getInstantiation(sv); + var bindings = BindingVariableVisitor.analyze(e); + return BindingVariableVisitor.toStatements( + positive ? bindings.whenTrue() : bindings.whenFalse()); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 5a26acc9589..64b30fe213d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -16,8 +16,10 @@ import de.uka.ilkd.key.java.ast.declaration.ModifierKind; import de.uka.ilkd.key.java.ast.declaration.ParameterDeclaration; import de.uka.ilkd.key.java.ast.declaration.VariableSpecification; +import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.ast.reference.TypeRef; import de.uka.ilkd.key.java.ast.statement.*; +import de.uka.ilkd.key.java.visitor.BindingVariableVisitor; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.ldt.HeapLDT.SplitFieldName; import de.uka.ilkd.key.ldt.JavaDLTheory; @@ -1701,6 +1703,34 @@ private ImmutableList collectLocalVariablesVisibleTo(Statement result = result.prepend(visibleLocalVariables); return result; } + } else if (s instanceof If ifStmt) { + final int branchCount = ifStmt.getBranchCount(); + final var condition = ifStmt.getExpression(); + if (branchCount == 1) { + var thenBranch = ifStmt.getBranchAt(0); + final ImmutableList visibleLocalVariables = + collectLocalVariablesVisibleTo(statement, thenBranch); + if (visibleLocalVariables != null) { + result = result.prepend(visibleLocalVariables); + ImmutableList pattern = + collectPatternVariables(true, condition); + result = result.prepend(pattern); + return result; + } + } + + if (branchCount == 2) { // also consider else-branch + var elseBranch = ifStmt.getBranchAt(1); + final ImmutableList visibleLocalVariables = + collectLocalVariablesVisibleTo(statement, elseBranch); + if (visibleLocalVariables != null) { + result = result.prepend(visibleLocalVariables); + ImmutableList pattern = + collectPatternVariables(false, condition); + result = result.prepend(pattern); + return result; + } + } } else if (s instanceof BranchStatement branch) { final int branchCount = branch.getBranchCount(); for (int j = 0; j < branchCount; j++) { @@ -1878,7 +1908,7 @@ public LoopSpecification createJMLLoopInvariant(IProgramMethod pm, LoopStatement public FunctionalOperationContract initiallyClauseToContract(InitiallyClause ini, IProgramMethod pm) throws SLTranslationException { final ImmutableList modifiers = - ImmutableList.singleton(JMLModifier.PRIVATE); + ImmutableList.singleton(JMLModifier.PRIVATE); final TextualJMLSpecCase specCase = new TextualJMLSpecCase(modifiers, Behavior.NONE); specCase.addName(ini.getName()); for (LabeledParserRuleContext context : createPrecond(pm, ini.getOriginalSpec())) { @@ -1921,4 +1951,12 @@ private ImmutableList createPrecond(IProgramMethod pm, } return res; } + + + private ImmutableList collectPatternVariables(boolean b, + Expression condition) { + var v = BindingVariableVisitor.analyze(condition); + return ImmutableList.fromList(b ? v.whenTrue().keySet() : v.whenFalse().keySet()); + } + } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key index 145cde438f9..ccd6c7ea7e4 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/java5.key @@ -13,7 +13,7 @@ \program SimpleExpression #se; \program NonSimpleExpression #nse; \program Expression #e; - \program Variable #v0; + \program Variable #v0, #fresh; \program Variable #id; \program Variable #a; \program Statement #stm; @@ -26,6 +26,8 @@ \formula post, inv; \term E e; + + \program [list] Statement #then, #else; } /*** diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index 9a338ae91fa..83822532da4 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key @@ -36,7 +36,7 @@ \program Variable #v, #v0, #v1, #v2, #boolv, #a, #a0, #a1; \program ConstantPrimitiveTypeVariable #cv; // variables that are compile-time constants - \program Variable #b0, #ar1; + \program Variable #b, #b0, #ar1, #id; \program VariableInitializer #vi; \program SimpleJavaBooleanExpression #seBool, #seBool0, #seBool1, #seBool2; \program JavaBooleanExpression #exBool, #exBool0, #exBool1, #exBool2; @@ -48,7 +48,7 @@ \program ForUpdates #forupdates; \program ForLoop #forloop; \program Expression #e, #e0, #e1, #e2; - \program NonSimpleExpression #nse, #nse0, #nse1, #nse2, #nv; + \program NonSimpleExpression #nse, #nse0, #nse1, #nse2, #nse3, #nv; \program NonSimpleExpressionNoClassReference #nsencr; \program ClassReference #cr; @@ -1274,6 +1274,181 @@ \displayname "ifElseUnfold" }; + // --- instanceof pattern matching binding (Java 16+) ---------------------- + // These rules handle the variable binding semantics of pattern matching instanceof + // Syntax: if(expr instanceof Type varName) { /* varName is bound to expr */ } + + ifUnfoldPattern { + \find(\modality{#allmodal}{.. if( #nse ) {#slist} ...}\endmodality (post)) + \varcond(\new(#boolv, boolean)) + \varcond(\isBindingExpr(#nse)) + \replacewith( + \modality{#allmodal}{.. + boolean #boolv; + { #boolv = #nse; } + if(#boolv) { + #posBinding(#nse); + #slist + } + ...}\endmodality (post)) + + \heuristics(simplify_autoname) + \displayname "ifElseUnfoldPattern" + }; + + ifUnfoldPatternUnreachable { + \find(\modality{#allmodal}{.. if( #nse ) {#slist} ...}\endmodality (post)) + \varcond(\new(#boolv, boolean)) + \varcond(\isBindingExpr(#nse)) + \varcond(\alwaysAbnormallyTerminates(#slist)) + \replacewith( + \modality{#allmodal}{.. + boolean #boolv; + { #boolv = #nse; } + if(#boolv) { + #posBinding(#nse); + #slist + } + #negBinding(#nse); + ...}\endmodality (post)) + + \heuristics(simplify_autoname) + \displayname "ifElseUnfoldPatternUnrechable" + }; + + ifElseUnfoldPattern { + \find(\modality{#allmodal}{.. if( #nse ) {#slist} else { #slist1 } ...}\endmodality (post)) + \varcond(\new(#boolv, boolean)) + \varcond(\isBindingExpr(#nse)) + \replacewith( + \modality{#allmodal}{.. + boolean #boolv; + { #boolv = #nse; } + if(#boolv) { + #posBinding(#nse); + #slist + } else { + #negBinding(#nse); + #slist1 + } + ...}\endmodality (post)) + + \heuristics(simplify_autoname) + \displayname "ifElseUnfoldPattern" + }; + + instanceofPatternAssignmentSE { + \find(\modality{#allmodal}{.. boolean #b = #se instanceof #t #v; ...}\endmodality(post)) + \replacewith( + \modality{#allmodal}{.. boolean #b = #se instanceof #t; ...}\endmodality(post)) + \displayname "instanceofPatternAssignmentSE" + }; + + + instanceofPatternAssignmentNSE { + \find(\modality{#allmodal}{ + .. boolean #b = #nse instanceof #t #v; ... + }\endmodality(post)) + \replacewith( + \modality{#allmodal}{..boolean #b = #nse instanceof #t; ...}\endmodality(post)) + \displayname "instanceofPatternAssignmentNSE" + }; + + andPatternAssignment { + \find(\modality{#allmodal}{.. boolean #b = #nse && #nse2; ...}\endmodality(post)) + \varcond(\new(#boolv, boolean)) + \varcond(\isBindingExpr(#nse)) + \replacewith( + \modality{#allmodal}{.. + boolean #b; boolean #boolv; + { + #boolv = #nse; + } + if(#boolv) { + #posBinding(#nse); + #b = #nse2; + } else { + #b = false; + } + ...}\endmodality(post)) + + \heuristics(simplify_autoname) + \displayname "andPatternAssignment" + }; + + orPatternAssignment { + \find(\modality{#allmodal}{ + .. boolean #b = #nse || #nse2; ... + }\endmodality(post)) + + \varcond(\new(#boolv, boolean)) + \varcond(\isBindingExpr(#nse)) + + \replacewith( + \modality{#allmodal}{.. + boolean #b; boolean #boolv; + { + #boolv = #nse; + } + if(#boolv) { + #b = true; + } else { + #b = #nse2; + } + ...}\endmodality(post)) + + \heuristics(simplify_autoname) + \displayname "orPatternAssignment" + }; + + notPatternAssignment { + \find(\modality{#allmodal}{ + .. boolean #b = !#nse; ... + }\endmodality(post)) + + \varcond(\new(#boolv, boolean)) + \varcond(\isBindingExpr(#nse)) + + \replacewith( + \modality{#allmodal}{.. + boolean #b; boolean #boolv; + { + #boolv = #nse; + } + #b = !#boolv; + }\endmodality(post)) + + \heuristics(simplify_autoname) + \displayname "notPatternAssignment" + }; + + conditionalPatternAssignment { + \find(\modality{#allmodal}{ + .. #t #v = #nse ? #nse2 : #nse3; ... + }\endmodality(post)) + + \varcond(\new(#boolv, boolean)) + \varcond(\isBindingExpr(#nse)) + + \replacewith( + \modality{#allmodal}{.. + #t #v; + boolean #boolv; + { + #boolv = #nse; + } + if(#boolv) { + #posBinding(#nse); + #v = #nse2; + } else { + #negBinding(#nse); + #v = #nse3; + } + ...}\endmodality(post)) + \heuristics(simplify_autoname) + \displayname "conditionalPatternAssignment" + }; + ifElseUnfold { \find(\modality{#allmodal}{.. if(#nse) #s0 else #s1 ...}\endmodality (post)) \varcond(\new(#boolv, boolean)) @@ -1528,6 +1703,51 @@ // ----------- instanceof ----------- // ---------------------------------------------------------------------------- + instanceof_eval_id { + \find(\modality{#allmodal}{.. #v = #nse instanceof #t #id; ...}\endmodality (post)) + \varcond(\newTypeOf(#v0, #nse)) + \replacewith(\modality{#allmodal}{.. + #typeof(#nse) #v0=#nse; + #v=#v0 instanceof #t; + // not needed #t #id = (#t) #v0; + ...}\endmodality (post)) + \heuristics(simplify_autoname) + }; + + instanceof_eval_id_and { + \find(\modality{#allmodal}{.. #v = #b0 instanceof #t #id && #nse; ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. + #v = #b0 instanceof #t; + if(#v) { + #t #id = (#t) #b0; + #v = /*true&&*/ #nse; + } + ...}\endmodality (post)) + \heuristics(simplify_autoname) + }; + + instanceof_eval_id_or { + \find(\modality{#allmodal}{.. #v = !(#b0 instanceof #t #id) || #nse; ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. + #v = #b0 instanceof #t; + if(!#v) { + #t #id = (#t) #b0; + #v = /*false || */ #nse; + } + ...}\endmodality (post)) + \heuristics(simplify_autoname) + }; + + + instanceof_eval_id_simple { + \find(\modality{#allmodal}{.. #v = #b0 instanceof #t #id; ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. + #v=#b0 instanceof #t; + // not needed #t #id = (#t) #v0; + ...}\endmodality (post)) + \heuristics(simplify_autoname) + }; + instanceof_eval { \find(\modality{#allmodal}{.. #v = #nse instanceof #t; ...}\endmodality (post)) \varcond(\newTypeOf(#v0, #nse)) diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/TestPatternAssignmentRules.java b/key.core/src/test/java/de/uka/ilkd/key/rule/TestPatternAssignmentRules.java new file mode 100644 index 00000000000..6fce9641738 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/TestPatternAssignmentRules.java @@ -0,0 +1,232 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.rule; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.nparser.KeyIO; +import de.uka.ilkd.key.proof.*; +import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit; +import de.uka.ilkd.key.proof.init.*; +import de.uka.ilkd.key.proof.io.KeYFileForTests; +import de.uka.ilkd.key.proof.io.ProofSaver; +import de.uka.ilkd.key.proof.io.RuleSource; +import de.uka.ilkd.key.proof.io.RuleSourceFactory; +import de.uka.ilkd.key.util.HelperClassForTests; +import de.uka.ilkd.key.util.parsing.BuildingException; + +import org.key_project.logic.PosInTerm; +import org.key_project.prover.proof.rulefilter.TacletFilter; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.util.collection.ImmutableList; + +import org.junit.jupiter.api.Assumptions; +import org.junit.jupiter.api.BeforeAll; +import org.junit.jupiter.api.Test; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assertions.assertTrue; + +/** + * Tests the pattern-assignment taclets of the production rule file {@code javaRules.key}, which + * decompose assignments whose initializer binds pattern variables: + * + *

    + *
  • {@code instanceofPatternAssignmentSE/NSE}: {@code b = e instanceof T v;} is rewritten to + * {@code b = e instanceof T;} (the binding is not relevant for a plain assignment)
    • + *
  • {@code andPatternAssignment}/{@code orPatternAssignment}: the guard expression is evaluated + * once into a fresh boolean variable; in the branch where the guard is known to have matched the + * pattern variables are declared by {@code #posBinding}
    • + *
  • {@code notPatternAssignment}: the guard is evaluated into a fresh boolean variable and + * negated
    • + *
  • {@code conditionalPatternAssignment}: the condition of a ternary is evaluated into a fresh + * boolean variable; the branches declare the pattern variables bound by {@code #posBinding} (resp. + * {@code #negBinding})
    • + *
+ * + *

+ * All six rules are loaded from the production rule file {@code javaRules.key} (there are no + * test-only copies). Loading this file requires the jmlparser to support the + * {@code #posBinding}/{@code #negBinding} program meta-constructs; until the parser supports them + * the rule base cannot be loaded and all tests of this class are skipped (see {@link #setUp()}). + */ +class TestPatternAssignmentRules { + private static final Logger LOGGER = LoggerFactory.getLogger(TestPatternAssignmentRules.class); + + /** + * A profile whose standard rules are the LDT declarations plus {@code javaRules.key}, the + * file containing the pattern assignment rules under test. + */ + private static final Profile PROFILE = new JavaProfile() { + @Override + public RuleCollection getStandardRules() { + return new RuleCollection( + ImmutableList.of(RuleSourceFactory.fromDefaultLocation(RuleSource.ldtFile), + RuleSourceFactory.fromDefaultLocation("javaRules.key")), + ImmutableList.nil()); + } + }; + + private static InitConfig initConfig; + private static Services services; + private static TacletIndex allRules; + + @BeforeAll + static void setUp() { + try { + var envInput = new KeYFileForTests( + "TestPatternAssignmentRules", HelperClassForTests.DUMMY_KEY_FILE, PROFILE); + initConfig = new ProblemInitializer(PROFILE).prepare(envInput); + } catch (Exception e) { + if (isMetaConstructParserGap(e)) { + String reason = "javaRules.key cannot be loaded, because the jmlparser does not" + + " support the #posBinding/#negBinding program meta-constructs yet: " + + e.getMessage(); + LOGGER.warn("Skipping the pattern-assignment rule tests. {}", reason); + Assumptions.assumeTrue(false, reason); + } + throw e instanceof RuntimeException re ? re : new RuntimeException(e); + } + services = initConfig.getServices(); + allRules = initConfig.createTacletIndex(); + } + + /** + * Checks whether the given exception chain contains the parse error caused by the jmlparser + * not knowing the {@code #posBinding}/{@code #negBinding} meta-constructs, in which case it + * tries to resolve them as schema variables. + */ + private static boolean isMetaConstructParserGap(Throwable error) { + for (Throwable t = error; t != null; t = t.getCause()) { + if (t instanceof BuildingException) { + String message = t.getMessage(); + if (message != null + && (message.contains("#posBinding") || message.contains("#negBinding"))) { + return true; + } + } + } + return false; + } + + private static JTerm parseTerm(String term) { + return new KeyIO(services, initConfig.namespaces()).parseExpression(term); + } + + /** + * Creates a goal {@code ==> \<{ program }\> true} whose rule set contains only the given rule + * and applies the rule at the top level of the succedent. Asserts that there is exactly one + * complete application and that it produces exactly one successor goal, which is returned. + */ + private Goal applyRule(String ruleName, String program) { + var succ = + ImmutableList.singleton(new SequentFormula(parseTerm("\\<{" + program + "}\\> true"))); + var sequent = JavaDLSequentKit.createSequent(ImmutableList.nil(), succ); + var proof = new Proof("TestPatternAssignmentRules", initConfig.deepCopy()); + proof.setRoot(new Node(proof, sequent)); + + var taclet = allRules.lookup(ruleName); + assertNotNull(taclet, "rule " + ruleName + " not found in javaRules.key"); + var tacletIndex = TacletIndexKit.getKit().createTacletIndex(); + tacletIndex.add(taclet); + var goal = new Goal(proof.root(), tacletIndex, + new BuiltInRuleAppIndex(new BuiltInRuleIndex()), proof.getServices()); + + var pos = + new PosInOccurrence(goal.sequent().succedent().getFirst(), PosInTerm.getTopLevel(), + false); + var apps = goal.ruleAppIndex().getTacletAppAt(TacletFilter.TRUE, pos, services); + assertEquals(1, apps.size(), + "Expected exactly one application of " + ruleName + " at " + pos + ", but found:\n" + + apps); + var app = apps.head(); + assertTrue(app.complete(), "Rule application of " + ruleName + " should be complete"); + + ImmutableList goals = app.taclet().getExecutor().apply(goal, app); + assertEquals(1, goals.size(), "Applying " + ruleName + " should create a single goal"); + return goals.head(); + } + + /** + * Asserts that the succedent of the goal consists of a single formula that is equal to the + * parsed expected formula modulo bound renaming, i.e. the programs are the same up to the + * names of the (locally declared) program variables. + */ + private static void assertSuccedent(Goal goal, String expectedFormula) { + JTerm actual = (JTerm) goal.sequent().succedent().getFirst().formula(); + JTerm expected = parseTerm(expectedFormula); + assertTrue(RENAMING_TERM_PROPERTY.equalsModThisProperty(actual, expected), + "Expected succedent:\n" + ProofSaver.printAnything(expected, services) + + "\nBut was:\n" + ProofSaver.printAnything(actual, services)); + } + + @Test + void instanceofPatternAssignmentSE() { + var goal = applyRule("instanceofPatternAssignmentSE", + "Object o; boolean b = o instanceof String s;"); + // the pattern variable s is dropped, the right hand side becomes a plain instanceof + assertSuccedent(goal, "\\<{Object o; boolean b = o instanceof String;}\\> true"); + } + + @Test + void instanceofPatternAssignmentNSE() { + var goal = applyRule("instanceofPatternAssignmentNSE", + "Object o; boolean b = (o == null ? o : o) instanceof String s;"); + assertSuccedent(goal, + "\\<{Object o; boolean b = (o == null ? o : o) instanceof String;}\\> true"); + } + + @Test + void andPatternAssignment() { + var goal = applyRule("andPatternAssignment", + "Object o; boolean b = o instanceof String s && o == null;"); + // The guard is evaluated once into a fresh boolean variable; the second operand is + // evaluated only in the branch where the guard is known to have matched, where the + // pattern variable s is additionally declared by #posBinding. + assertSuccedent(goal, + "\\<{Object o; boolean b; boolean b_1; { b_1 = o instanceof String s; }" + + " if (b_1) { String s = (String) o; b = o == null; } else { b = false; }}\\> true"); + } + + @Test + void orPatternAssignment() { + var goal = applyRule("orPatternAssignment", + "Object o; boolean b = o instanceof String s || o == null;"); + // The guard is evaluated once into a fresh boolean variable; the second operand is + // evaluated only if the guard is false, in which case b is the value of the second + // operand. + assertSuccedent(goal, + "\\<{Object o; boolean b; boolean b_1; { b_1 = o instanceof String s; }" + + " if (b_1) { b = true; } else { b = o == null; }}\\> true"); + } + + @Test + void notPatternAssignment() { + var goal = applyRule("notPatternAssignment", + "Object o; boolean b = !(o instanceof String s);"); + // The guard is evaluated into a fresh boolean variable and negated; no branch is + // introduced, hence no pattern variable is declared. + assertSuccedent(goal, + "\\<{Object o; boolean b; boolean b_1; { b_1 = (o instanceof String s); } b = !b_1;}" + + "\\> true"); + } + + @Test + void conditionalPatternAssignment() { + var goal = applyRule("conditionalPatternAssignment", + "Object o; boolean r = !(o instanceof String s) ? o != null : o == null;"); + // The negated guard binds s only when it evaluates to false, hence s is declared in the + // else-branch by #negBinding; in the then-branch no pattern variable is bound. + assertSuccedent(goal, + "\\<{Object o; boolean r; boolean b; { b = !(o instanceof String s); }" + + " if (b) { r = o != null; } else { String s = (String) o; r = o == null; }}\\>" + + " true"); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysisTest.java b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysisTest.java new file mode 100644 index 00000000000..cda91ed7338 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/AlwaysAbnormallyTerminatingAnalysisTest.java @@ -0,0 +1,128 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.rule.conditions; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.JPContext; +import de.uka.ilkd.key.java.ast.Statement; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.ast.reference.TypeRef; +import de.uka.ilkd.key.java.loader.JP2KeYConverter; +import de.uka.ilkd.key.logic.ProgramElementName; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.SchemaVariableFactory; +import de.uka.ilkd.key.logic.sort.ProgramSVSort; +import de.uka.ilkd.key.logic.sort.SortImpl; +import de.uka.ilkd.key.nparser.NamespaceBuilder; +import de.uka.ilkd.key.proof.init.JavaProfile; + +import org.key_project.logic.Name; +import org.key_project.logic.Namespace; +import org.key_project.logic.op.sv.SchemaVariable; + +import com.github.javaparser.JavaParser; +import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import org.junit.jupiter.api.TestInstance; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.CsvSource; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +/** + * NOTE ON PACKAGE PLACEMENT: put this file in the same package as + * AlwaysAbnormallyTerminatingAnalysis (it relies on package-private / private + * access to the record and to the and()/or() helpers via reflection, so it + * doesn't need any source changes to the class under test). + *

+ * NOTE ON TIER B (statement-level tests): those need a real Services + + * parsed Statement, which is project-specific plumbing I don't have visibility + * into. `parseStatement(String)` below is a stub — wire it up to however your + * test suite already builds a Services/ExecutionContext and parses a method + * body (KeY 3.x parses via JavaParser under the hood). Everything else in + * this file works standalone. + */ +@TestInstance(TestInstance.Lifecycle.PER_CLASS) +class AlwaysAbnormallyTerminatingAnalysisTest { + private final Services services = new Services(JavaProfile.getDefaultProfile()); + private final JPContext context; + private final JP2KeYConverter converter; + private final JavaParser javaParser; + private final ExecutionContext executionContext; + + + // --- plumbing you need to fill in for your project ----------------- + + private AlwaysAbnormallyTerminatingAnalysis newAnalysis() { + return new AlwaysAbnormallyTerminatingAnalysis(executionContext, services); + } + + private Statement parseStatement(String javaStatementSource) { + return (Statement) services.getJavaService() + .readBlock("{" + javaStatementSource + "}", context, null).program(); + } + + public AlwaysAbnormallyTerminatingAnalysisTest() { + System.out.println("TEST INIT"); + var nss = services.getNamespaces(); + NamespaceBuilder nb = new NamespaceBuilder(nss); + nb.addSort("boolean").addSort("int").addSort("Seq").addSort("LocSet").addSort("double") + .addSort("float"); + + Namespace nsSchema = new Namespace<>(); + nsSchema.add(SchemaVariableFactory.createProgramSV( + new ProgramElementName("#a"), ProgramSVSort.EXPRESSION, false)); + nsSchema.add(SchemaVariableFactory.createProgramSV( + new ProgramElementName("#b"), ProgramSVSort.EXPRESSION, false)); + nsSchema.add(SchemaVariableFactory.createProgramSV( + new ProgramElementName("#c"), ProgramSVSort.EXPRESSION, false)); + + services.activateJava(null); + + + var cu = StaticJavaParser.parse(""" + public class Context { + boolean x, y, z; + } + """); + services.getJavaService().getSymbolResolver().inject(cu); + context = new JPContext((ClassOrInterfaceDeclaration) cu.types().getFirst(), cu); + services.getJavaService().parseSpecialClasses(); + converter = services.getJavaService().getConverter(nsSchema); + javaParser = services.getJavaService().getProgramFactory().createJavaParser(); + + executionContext = new ExecutionContext( + new TypeRef(new KeYJavaType(PrimitiveType.JAVA_BYTE, new SortImpl(new Name("byte")))), + null, new LocationVariable(new ProgramElementName("testVar"), + new SortImpl(new Name("testSort")))); + } + + @ParameterizedTest(name = "[{index}] {1}") + @CsvSource(delimiterString = "|", value = { + // expectedAlwaysAbnormal | description | source + "true | if/else both return | if (x) { return 1; } else { return 2; }", + "true | if/else only then returns | if (true) { return 1; } else { doStuff(); }", + "false | if/else only then returns | if (x) { return 1; } else { doStuff(); }", + "false | if with no else | if (x) { return 1; }", + "true | while(true) with a break | while (true) { if (x) { break; } return 1; }", + "false | while(true) with no break at all | while (true) { doStuff(); }", + "false | switch without default | switch (x) { case 1: return 1; }", + "true | switch with default, all cases return | switch (x) { case 1: return 1; default: throw new RuntimeException(); }", + "false | try/catch that recovers | try { throw new RuntimeException(); } catch (RuntimeException e) { doStuff(); }", + "true | try/finally where finally always returns | try { doStuff(); } finally { return 1; }", + "true | assert with a constant-false condition | assert false;", + "false | assert with a constant-true condition | assert true;", + }) + void statementAlwaysAbnormal(boolean expected, String description, String source) { + Statement stmt = parseStatement(source); + AlwaysAbnormallyTerminatingAnalysis analysis = newAnalysis(); + Object result = analysis.abnormallyTerminating(stmt); + boolean actual = result != null; // TerminationReason#isAbnormallTerminating() should also + // be checked once record fields are trustworthy + assertEquals(expected, actual, description); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/metaconstruct/BindingsOfExprTest.java b/key.core/src/test/java/de/uka/ilkd/key/rule/metaconstruct/BindingsOfExprTest.java new file mode 100644 index 00000000000..2ee13f74cc3 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/metaconstruct/BindingsOfExprTest.java @@ -0,0 +1,127 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.rule.metaconstruct; + +import java.util.Arrays; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.StatementBlock; +import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; +import de.uka.ilkd.key.java.ast.declaration.VariableSpecification; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.TypeCast; +import de.uka.ilkd.key.java.ast.statement.If; +import de.uka.ilkd.key.logic.ProgramElementName; +import de.uka.ilkd.key.logic.op.ProgramSV; +import de.uka.ilkd.key.logic.op.SchemaVariableFactory; +import de.uka.ilkd.key.logic.sort.ProgramSVSort; +import de.uka.ilkd.key.nparser.NamespaceBuilder; +import de.uka.ilkd.key.proof.init.JavaProfile; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import com.github.javaparser.StaticJavaParser; +import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; +import org.junit.jupiter.api.TestInstance; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.CsvSource; + +import static org.junit.jupiter.api.Assertions.assertArrayEquals; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertInstanceOf; + +@TestInstance(TestInstance.Lifecycle.PER_CLASS) +class BindingsOfExprTest { + private final Services services = new Services(JavaProfile.getDefaultProfile()); + private final de.uka.ilkd.key.java.ast.JPContext context; + + public BindingsOfExprTest() { + var nss = services.getNamespaces(); + NamespaceBuilder nb = new NamespaceBuilder(nss); + nb.addSort("boolean").addSort("int").addSort("Seq").addSort("LocSet").addSort("double") + .addSort("float"); + services.activateJava(null); + + var cu = StaticJavaParser.parse(""" + public class Context { + Object o, o2; + } + """); + services.getJavaService().getSymbolResolver().inject(cu); + context = + new de.uka.ilkd.key.java.ast.JPContext( + (ClassOrInterfaceDeclaration) cu.types().getFirst(), cu); + services.getJavaService().parseSpecialClasses(); + } + + /** + * Parses the given condition as the guard of an {@code if} statement and applies the given + * meta construct to it, returning the names of the introduced pattern variables. + */ + private String[] apply(String cond, boolean positive) { + return Arrays.stream(declarations(cond, positive)).map(vs -> vs.getProgramVariable() + .name().toString()).toArray(String[]::new); + } + + private VariableSpecification[] declarations(String cond, boolean positive) { + String block = "{ Object o, o2; if (" + cond + ") { } }"; + StatementBlock sb = + (StatementBlock) services.getJavaService().readBlock(block, context, null).program(); + If ifStmt = (If) sb.getStatementAt(1); + Expression guard = ifStmt.getExpressionAt(0); + + ProgramSV sv = SchemaVariableFactory.createProgramSV( + new ProgramElementName("#nse"), ProgramSVSort.EXPRESSION, false); + var meta = + positive ? BindingsOfExpr.createPositive(sv) : BindingsOfExpr.createNegative(sv); + SVInstantiations inst = SVInstantiations.EMPTY_SVINSTANTIATIONS.add(sv, guard, services); + + return Arrays.stream(meta.transform(null, services, inst)) + .map(pe -> { + assertInstanceOf(LocalVariableDeclaration.class, pe); + return (LocalVariableDeclaration) pe; + }) + .map(decl -> decl.getVariableSpecifications().get(0)) + .toArray(VariableSpecification[]::new); + } + + @ParameterizedTest(name = "positive bindings of [{0}] -> {1}") + @CsvSource(delimiterString = "|", value = { + "o instanceof String s | s", + "!(o instanceof String s) | ", + "o instanceof String s && o2 instanceof Object t | s t", + "o == null | ", + }) + void positiveBindings(String cond, String expected) { + assertArrayEquals(split(expected), apply(cond, true), "positive bindings of: " + cond); + } + + @ParameterizedTest(name = "negative bindings of [{0}] -> {1}") + @CsvSource(delimiterString = "|", value = { + "o instanceof String s | ", + "!(o instanceof String s) | s", + "o instanceof String s || o2 instanceof Object t | ", + "o == null | ", + }) + void negativeBindings(String cond, String expected) { + assertArrayEquals(split(expected), apply(cond, false), "negative bindings of: " + cond); + } + + private String[] split(String expected) { + return expected == null || expected.isBlank() ? new String[0] + : expected.trim().split("\\s+"); + } + + /** the introduced variables must be declared with a type cast as initializer */ + @ParameterizedTest + @CsvSource(delimiterString = "|", value = { + "o instanceof String s | true", + "!(o instanceof String s) | false", + }) + void declaredWithCast(String cond, boolean positive) { + VariableSpecification[] specs = declarations(cond, positive); + assertEquals(1, specs.length); + assertInstanceOf(TypeCast.class, specs[0].getInitializer()); + } +} diff --git a/key.ui/examples/Java/InstanceOfPattern/README.txt b/key.ui/examples/Java/InstanceOfPattern/README.txt new file mode 100644 index 00000000000..38f279cae75 --- /dev/null +++ b/key.ui/examples/Java/InstanceOfPattern/README.txt @@ -0,0 +1,72 @@ +example.name = Binding InstanceOf +example.path = Java 25 +example.file = project.key +example.additionalFile.1 = src/InstanceOfPatternExample.java + + +Java 16+ Instanceof Pattern Matching Example +============================================= + +This example demonstrates KeY's support for Java 16+ instanceof pattern matching, +which allows type checking and variable binding in a single expression. + +Feature Overview +---------------- +Traditional instanceof (pre-Java 16): + if (obj instanceof String) { + String s = (String) obj; + return s.length(); + } + +Pattern matching instanceof (Java 16+): + if (obj instanceof String s) { + // 's' is automatically bound as a String + return s.length(); + } + +What This Example Shows +----------------------- +1. Basic pattern matching (getStringLength method) + - The pattern variable 's' is bound in the true branch + +2. Negated instanceof (checkNotString method) + - Pattern binding happens in the else branch, not the if branch + - Demonstrates: if(!(x instanceof T e)) { ... } else { ... } + +3. Multiple instanceof patterns (processNumber method) + - Chained instanceof checks with different types + +4. Pattern variables in complex expressions (compareIfBothStrings) + - Multiple pattern variables bound in the same branch + - Combined with && operator + +5. Traditional vs pattern matching comparison (traditionalVsPattern) + - Shows both styles work correctly together + +Key Taclets +----------- +The following taclets in genericRules.key handle pattern matching: + +- instanceof_pattern_if_split: Splits if-statements and binds the pattern variable +- instanceof_pattern_negated_if: Handles negated instanceof by swapping branches +- instanceof_pattern_cast_elimination: Eliminates redundant casts after instanceof + +Loading This Example +-------------------- +1. Open KeY +2. Load the project.key file from this directory +3. Select a method to verify +4. Start symbolic execution + +The instanceof pattern matching will be automatically handled during proof search. + +Requirements +------------ +- Java 16 or later (for compilation) +- KeY with instanceof pattern matching support + +See Also +-------- +- Java 16 Release Notes: https://openjdk.java.net/projects/jdk/16/ +- JEP 394: Pattern Matching for instanceof + https://openjdk.java.net/jeps/394 diff --git a/key.ui/examples/Java/InstanceOfPattern/project.key b/key.ui/examples/Java/InstanceOfPattern/project.key new file mode 100644 index 00000000000..e55dd42651e --- /dev/null +++ b/key.ui/examples/Java/InstanceOfPattern/project.key @@ -0,0 +1,3 @@ +\javaSource "src"; + +\chooseContract diff --git a/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java b/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java new file mode 100644 index 00000000000..caa282c51fd --- /dev/null +++ b/key.ui/examples/Java/InstanceOfPattern/src/InstanceOfPatternExample.java @@ -0,0 +1,162 @@ +/** + * Example demonstrating Java 16+ instanceof pattern matching support in KeY. + * + * This feature allows you to write: + * if (obj instanceof String s) { + * // s is automatically bound and can be used here + * return s.length(); + * } + * + * Instead of the traditional: + * if (obj instanceof String) { + * String s = (String) obj; + * return s.length(); + * } + */ +public class InstanceOfPatternExample { + //@ static invariant_free (\forall String s; true; s.length() >= 0); + + /*@ normal_behavior + @ requires obj != null; + @ ensures \result instanceof String; + @*/ + public static Object getString(Object obj) { + return "ha"; + } + + /*@ normal_behavior + @ requires obj != null; + @ ensures \result; + @*/ + public static boolean isString(Object obj) { + return getString(obj) instanceof String id && id.length() >= 0; + } + + /*@ normal_behavior + @ requires obj instanceof String; + @ ensures \result >= 0; + @*/ + public static int getStringLength(Object obj) { + if (obj instanceof String s) { + // Pattern variable 's' is bound and has type String here + // @ assert s != null; + return s.length(); + } + return -1; + } + + /** + * Negated instanceof pattern - note that the binding only happens + * in the else branch, not the if branch. + */ + /*@ normal_behavior + @ requires true; + @ ensures \result >= 0; + @*/ + public static int checkNotString(Object obj) { + Object a = new Object(); + //@ assert a != null; + if (!(obj instanceof String s)) { + // 's' is NOT bound here + return 0; + } else { + // 's' IS bound here (in the else branch) + // @ assert s != null; + return s.length(); + } + } + + /** + * Multiple instanceof patterns in sequence. + */ + /*@ normal_behavior + @ requires true; + @ ensures \result >= 0; + @*/ + public static int processNumber(Object obj) { + if (obj instanceof Integer i) { + return i.intValue(); + } else if (obj instanceof Double d) { + return d.intValue(); + } else if (obj instanceof Long l) { + return l.intValue(); + } + return -1; + } + + /** + * Pattern matching with method calls. + */ + /*@ normal_behavior + @ requires true; + @ ensures \result >= -1; + @*/ + public static int getToStringLength(Object obj) { + if (obj instanceof String s) { + // Can call methods on the pattern variable + return s.toString().length(); + } + return -1; + } + +// /** +// * Pattern matching in complex expressions. +// */ +// /*@ normal_behavior +// @ requires obj1 != null && obj2 != null; +// @ ensures \result == 0 || \result > 0; +// @*/ +// public static int compareIfBothStrings(Object obj1, Object obj2) { +// if (obj1 instanceof String s1 && obj2 instanceof String s2) { +// // Both s1 and s2 are bound in this branch +// //@ assert s1 != null && s2 != null; +// return s1.compareTo(s2); +// } +// return 0; +// } + + /** + * Traditional instanceof vs pattern matching. + * This shows both styles for comparison. + */ + /*@ normal_behavior + @ requires true; + @ ensures \result >= -1; + @*/ + public static int traditionalVsPattern(Object obj) { + // Traditional style (still supported) + if (obj instanceof String) { + String s = (String) obj; + int traditional = s.length(); + + // Pattern matching style (more concise) + if (obj instanceof String pattern) { + int patternStyle = pattern.length(); + //@ assert traditional == patternStyle; + } + + return traditional; + } + return -1; + } + + /** + * Main method for testing. + */ + public static void main(String[] args) { + System.out.println(getStringLength("Hello")); // 5 + System.out.println(getStringLength(42)); // -1 + + System.out.println(checkNotString(42)); // 0 + System.out.println(checkNotString("World")); // 5 + + System.out.println(processNumber(42)); // 42 + System.out.println(processNumber(3.14)); // 3 + System.out.println(processNumber(100L)); // 100 + + System.out.println(getToStringLength("Test")); // 4 + + System.out.println(compareIfBothStrings("A", "B")); // -1 + System.out.println(compareIfBothStrings("A", 42)); // 0 + } +} diff --git a/key.ui/examples/index/samplesIndex.txt b/key.ui/examples/index/samplesIndex.txt index 4a217f00039..dc0338a6308 100644 --- a/key.ui/examples/index/samplesIndex.txt +++ b/key.ui/examples/index/samplesIndex.txt @@ -30,6 +30,7 @@ Java/Records/README.txt Java/Records+CompactConstructor/README.txt Java/TextBlockLiterals/README.txt Java/TryWithResources/README.txt +Java/InstanceOfPattern/README.txt # The KeY Book (note: the comments here are only for maintainability, if you want to move an entry to a different section, look into the individual txt file!) ## Chapter 15 - Using the KeY Prover diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TacletMatchDebuggerExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TacletMatchDebuggerExtension.java new file mode 100644 index 00000000000..d233ff1e8d3 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TacletMatchDebuggerExtension.java @@ -0,0 +1,263 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2, + * or (at your option) any later version. + * SPDX-License-Identifier: GPL-2.0-or-later */ +package de.uka.ilkd.key.gui.extension.impl; + +import java.awt.*; +import java.awt.event.ActionEvent; +import java.io.PrintWriter; +import java.io.StringWriter; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Comparator; +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.extension.api.ContextMenuAdapter; +import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.pp.PosInSequent; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.MatchConditions; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.rule.match.vm.VMTacletMatcher; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Term; +import org.key_project.prover.rules.TacletMatcher; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.instantiation.SVInstantiations; + +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Extension that provides a context menu action for debugging taclet matching on terms. + * When clicking on a term in the sequent view, users can select a taclet from a combo box + * and see whether it matches the selected term. + * + * @author Alexander Weigl + */ +@KeYGuiExtension.Info(name = "Taclet Match Debugger", + description = "Debug taclet matching by selecting a term and testing which taclets match.\n" + + "Developer: Alexander Weigl", + experimental = false, optional = true, priority = 50) +@NullMarked +public class TacletMatchDebuggerExtension implements KeYGuiExtension, KeYGuiExtension.ContextMenu { + private static final Logger LOGGER = + LoggerFactory.getLogger(TacletMatchDebuggerExtension.class); + + private final ContextMenuAdapter adapter = new ContextMenuAdapter() { + @Override + public List getContextActions(KeYMediator mediator, ContextMenuKind kind, + @Nullable T underlyingObject) { + if (kind != ContextMenuKind.SEQUENT_VIEW + || !(underlyingObject instanceof PosInSequent pos)) { + return Collections.emptyList(); + } + + // Check if we have a valid proof and goal + Goal goal = mediator.getSelectedGoal(); + if (goal == null) { + return Collections.emptyList(); + } + + // Check if the position has a valid term + if (pos.getPosInOccurrence() == null) { + return Collections.emptyList(); + } + + var selectedTerm = pos.getPosInOccurrence().subTerm(); + if (selectedTerm == null) { + return Collections.emptyList(); + } + + return Collections.singletonList(new MatchTacletAction(mediator, pos, selectedTerm)); + } + }; + + @Override + public List getContextActions(KeYMediator mediator, ContextMenuKind kind, + @Nullable T underlyingObject) { + return adapter.getContextActions(mediator, kind, underlyingObject); + } + + /** + * Action that opens a dialog to select a taclet and test matching. + */ + private static class MatchTacletAction extends KeyAction { + private final KeYMediator mediator; + private final PosInSequent pos; + private final Term selectedTerm; + + public MatchTacletAction(KeYMediator mediator, PosInSequent pos, Term selectedTerm) { + this.mediator = mediator; + this.pos = pos; + this.selectedTerm = selectedTerm; + setName("Match Taclets..."); + } + + @Override + public void actionPerformed(ActionEvent e) { + MainWindow mainWindow = MainWindow.getInstance(); + + // Get all available taclets from the current goal + Goal goal = mediator.getSelectedGoal(); + if (goal == null) { + JOptionPane.showMessageDialog(mainWindow, + "No active proof goal available.", + "Error", + JOptionPane.ERROR_MESSAGE); + return; + } + + // Collect all taclets + List tacletApps = new ArrayList<>( + goal.ruleAppIndex().tacletIndex().allNoPosTacletApps()); + + // Add taclets from OneStepSimplifier if available + var simplifier = MiscTools.findOneStepSimplifier(goal.proof()); + if (simplifier != null && !simplifier.isShutdown()) { + tacletApps.addAll(simplifier.getCapturedTaclets()); + } + + if (tacletApps.isEmpty()) { + JOptionPane.showMessageDialog(mainWindow, + "No taclets available for matching.", + "Information", + JOptionPane.INFORMATION_MESSAGE); + return; + } + + // Sort taclets by name for easier selection + tacletApps.sort(Comparator.comparing(app -> app.rule().name().toString())); + + // Create array of taclet names for the combo box + String[] tacletNames = tacletApps.stream() + .map(app -> app.rule().name().toString()) + .toArray(String[]::new); + + // Show dialog with combo box for taclet selection + JComboBox tacletComboBox = new JComboBox<>(tacletNames); + tacletComboBox.setEditable(false); + tacletComboBox.setMaximumRowCount(25); + + JPanel panel = new JPanel(new BorderLayout()); + panel.add(new JLabel("Select a taclet to match against the term:"), BorderLayout.NORTH); + panel.add(tacletComboBox, BorderLayout.CENTER); + panel.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); + + int result = JOptionPane.showConfirmDialog( + mainWindow, + panel, + "Match Taclet", + JOptionPane.OK_CANCEL_OPTION, + JOptionPane.PLAIN_MESSAGE); + + if (result == JOptionPane.OK_OPTION) { + int selectedIndex = tacletComboBox.getSelectedIndex(); + if (selectedIndex >= 0 && selectedIndex < tacletApps.size()) { + NoPosTacletApp selectedTacletApp = tacletApps.get(selectedIndex); + Taclet selectedTaclet = selectedTacletApp.rule(); + + performMatching(selectedTaclet, selectedTerm, goal); + } + } + } + + /** + * Performs the actual taclet matching and displays the results. + */ + private void performMatching(Taclet taclet, Term term, Goal goal) { + StringWriter out = new StringWriter(); + PrintWriter output = new PrintWriter(out); + var services = goal.proof().getServices(); + TacletMatcher matcher = new VMTacletMatcher(taclet, output); + + output.printf("=== Taclet Match Debug ===\n\n"); + output.printf("Selected Term: %s\n\n", term); + output.printf("Selected Taclet: %s\n\n", taclet.name()); + + // Print taclet definition + output.printf("Taclet Definition:\n"); + output.printf("----------------------------------------\n"); + try { + var lp = de.uka.ilkd.key.pp.LogicPrinter.purePrinter( + new de.uka.ilkd.key.pp.NotationInfo(), null); + lp.printTaclet(taclet); + output.println(lp.result()); + } catch (Exception ex) { + output.printf("Could not print taclet: %s\n", ex.getMessage()); + } + output.printf("----------------------------------------\n\n"); + + // Try to match + output.printf("Matching Result:\n"); + output.printf("----------------------------------------\n"); + + try { + // Create initial match conditions + MatchResultInfo initialMatchCond = MatchConditions.EMPTY_MATCHCONDITIONS; + + MatchResultInfo matchResult = matcher.matchFind(term, initialMatchCond, services); + + if (matchResult != null) { + output.printf("✓ MATCH SUCCESSFUL!\n\n"); + + // Print variable instantiations + SVInstantiations instantiations = matchResult.getInstantiations(); + var instMap = instantiations.getInstantiationMap(); + if (instMap != null && !instMap.isEmpty()) { + output.printf("Variable Instantiations:\n"); + for (var entry : instMap) { + output.printf(" %s := %s\n", entry.key().name(), + entry.value().getInstantiation()); + } + } else { + output.printf("No variable instantiations needed.\n"); + } + + // Check additional conditions + MatchResultInfo checkedResult = matcher.checkConditions(matchResult, services); + if (checkedResult != null) { + output.printf("\n✓ All taclet conditions satisfied!\n"); + } else { + output.printf("\n✗ Taclet conditions NOT satisfied!\n"); + } + } else { + output.printf("✗ NO MATCH - The taclet does not match the selected term.\n"); + } + } catch (Exception ex) { + output.printf("✗ ERROR during matching: ").printf(ex.getMessage()).printf("\n"); + LOGGER.error("Error during taclet matching", ex); + } + + output.printf("----------------------------------------\n"); + + // Output to console + LOGGER.info("Taclet matching performed for taclet: {}, {}", taclet.name(), out); + + // Also show in a dialog + JTextArea textArea = new JTextArea(out.toString()); + textArea.setEditable(false); + textArea.setCaretPosition(0); + textArea.setFont(new Font(Font.MONOSPACED, Font.PLAIN, 12)); + + JScrollPane scrollPane = new JScrollPane(textArea); + scrollPane.setPreferredSize(new Dimension(700, 500)); + + JOptionPane.showMessageDialog( + MainWindow.getInstance(), + scrollPane, + "Taclet Match Result", + JOptionPane.INFORMATION_MESSAGE); + } + } +} 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 5c590ebaca9..915df3d286e 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 @@ -11,4 +11,5 @@ de.uka.ilkd.key.gui.JmlEnabledKeysIndicator de.uka.ilkd.key.gui.extension.impl.ProfileNameInStatusBar de.uka.ilkd.key.gui.extension.impl.ParallelProverStatusIndicator de.uka.ilkd.key.gui.profileloading.WDLoadDialogOptionPanel -de.uka.ilkd.key.gui.extension.impl.SoundinessExtension \ No newline at end of file +de.uka.ilkd.key.gui.extension.impl.SoundinessExtension +de.uka.ilkd.key.gui.extension.impl.TacletMatchDebuggerExtension \ No newline at end of file