diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index d90a738ff3d..778bdc79b0f 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -70,6 +70,7 @@ PURE: 'pure'; RETURN_BEHAVIOR: 'return_' BEHAVIOR; FINAL: 'final'; MODEL: 'model'/* -> pushMode(expr)*/; +LEMMA: 'lemma' -> pushMode(expr); fragment Pred: '_redundantly'?; //suffix fragment Pfree: '_free'?; //suffix @@ -139,6 +140,7 @@ SEPARATES: 'separates' -> pushMode(expr); SET: 'set' -> pushMode(expr); SIGNALS: ('signals' Pred | 'exsures' Pred) -> pushMode(expr); SIGNALS_ONLY: 'signals_only' Pred -> pushMode(expr); +USE_LEMMA: 'use_lemma' -> pushMode(expr); VAR: 'var'; WHEN: 'when' Pred -> pushMode(expr); WORKING_SPACE: 'working_space' Pred -> pushMode(expr); diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index aed3866b353..1eacc0246ae 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -22,6 +22,7 @@ classlevel_element0: modifiers? (classlevel_element modifiers?); classlevel_element : class_invariant | accessible_clause | method_specification | method_declaration | field_declaration | represents_clause + | lemma_declaration | history_constraint | initially_clause | class_axiom | monitors_for_clause | readable_if_clause | writable_if_clause | datagroup_clause | set_statement | nowarn_pragma @@ -33,7 +34,7 @@ methodlevel_element : field_declaration | set_statement | merge_point_statement | loop_specification | assert_statement | assume_statement | nowarn_pragma | debug_statement | block_specification | block_loop_specification - | assert_statement | assume_statement + | assert_statement | assume_statement | use_lemma_statement ; modifiers: modifier+; @@ -157,13 +158,15 @@ name_clause: SPEC_NAME STRING_LITERAL SEMICOLON ; field_declaration: typespec IDENT (LBRACKET RBRACKET)* initialiser? SEMI_TOPLEVEL; method_declaration: typespec IDENT param_list (method_body=mbody_block | SEMI_TOPLEVEL); -mbody_block: LBRACE mbody_var* mbody_statement RBRACE; +mbody_block: LBRACE (mbody_var | assert_statement)* mbody_statement RBRACE; mbody_statement: RETURN expression SEMI_TOPLEVEL #mbody_return | IF LPAREN expression RPAREN (mbody_statement | mbody_block) ELSE (mbody_statement | mbody_block) #mbody_if ; mbody_var: VAR? IDENT EQUAL_SINGLE expression SEMI_TOPLEVEL; +lemma_declaration: LEMMA IDENT param_list assertionProof SEMI_TOPLEVEL; + param_list: LPAREN (param_decl (COMMA param_decl)*)? RPAREN; param_decl: ((NON_NULL | NULLABLE))? typespec p=IDENT (LBRACKET RBRACKET)*; history_constraint: CONSTRAINT expression; @@ -176,6 +179,7 @@ maps_into_clause: MAPS expression; nowarn_pragma: NOWARN expression; debug_statement: DEBUG expression; set_statement: SET (assignee=expression) EQUAL_SINGLE (value=expression) SEMI_TOPLEVEL; +use_lemma_statement: USE_LEMMA postfixexpr SEMI_TOPLEVEL; merge_point_statement: MERGE_POINT (MERGE_PROC (proc=STRING_LITERAL))? diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java index c148c5b6a51..fa64ae601ba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SpecialJavaPrinter.java @@ -94,7 +94,8 @@ private void print(List spec) { } case TextualJMLInitially c -> print(c.getModifiers(), c.getInv().first); case TextualJMLMergePointDecl c -> print(c.getModifiers(), c.getMergeProc()); - case TextualJMLMethodDecl c -> print(c.getModifiers(), c.getDecl()); + case TextualJMLMethodOrLemmaDecl c -> + print(c.getModifiers(), c.getMethodDefinition()); case TextualJMLModifierList c -> print(c.getModifiers()); case TextualJMLRepresents c -> print(c.getModifiers(), c.getRepresents().first); case TextualJMLSetStatement c -> print(c.getAssignment()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java index a4337f93c26..aa817cc1e9c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLemmaDecl; import de.uka.ilkd.key.speclang.njml.SpecMathMode; import org.key_project.util.ExtList; @@ -424,6 +425,11 @@ public boolean isModel() { return super.isModel(); } + public boolean isLemma() { + return attachedJml.stream().anyMatch(TextualJMLLemmaDecl.class::isInstance); + } + + @Override public int getStateCount() { return super.getStateCount(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ModifierKind.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ModifierKind.java index 18afc540e0d..2ffacdfa121 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ModifierKind.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ModifierKind.java @@ -55,6 +55,7 @@ public enum ModifierKind { JML_CODE("code"), JML_OT_PEER("peer"), JML_OT_REP("rep"), + JML_LEMMA("lemma"), JML_OT_READ_ONLY("read_only"); private final String codeRepresentation; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/UseLemmaStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/UseLemmaStatement.java new file mode 100644 index 00000000000..c0f45132dbe --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/UseLemmaStatement.java @@ -0,0 +1,63 @@ +/* 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.java.ast.statement; + +import de.uka.ilkd.key.java.ast.PositionInfo; +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.speclang.njml.JmlParser; + +/** + * JML use_lemma statement + * + * @author Mattias Ulbrich + */ +public class UseLemmaStatement extends JavaStatement { + + /** + * The parser context of the statement produced during parsing. + */ + private final JmlParser.PostfixexprContext context; + + /** Constructor used in recoderext */ + public UseLemmaStatement(JmlParser.PostfixexprContext context, PositionInfo positionInfo) { + super(positionInfo); + this.context = context; + } + + /** Constructor used when cloning */ + public UseLemmaStatement(UseLemmaStatement copyFrom) { + this(copyFrom.context, copyFrom.getPositionInfo()); + } + + /** + * Removes the attached parser context from this set statement + * + * @return the parser context that was attached + */ + public JmlParser.PostfixexprContext getParserContext() { + return context; + } + + /** {@inheritDoc} */ + @Override + public void visit(Visitor v) { + v.performActionOnUseLemmaStatement(this); + } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public ProgramElement getChildAt(int index) { + throw new IndexOutOfBoundsException("UseLemmaStatement has no program children"); + } + + @Override + protected int computeHashCode() { + return System.identityHashCode(this); + } +} 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 773c8bcbb0b..371707082a2 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 @@ -40,6 +40,7 @@ import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLoopSpec; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLUseLemmaStatement; import org.key_project.logic.MetaSpace; import org.key_project.logic.Namespace; @@ -775,6 +776,10 @@ public Object visit(KeYMarkerStatement n, Void arg) { KeyAst.SetStatementContext context = n.getData(MarkerStatementHelper.KEY_ASSIGN); yield new SetStatement(context, pi); } + case MarkerStatementHelper.KIND_USE_LEMMA -> { + TextualJMLUseLemmaStatement stm = n.getData(MarkerStatementHelper.KEY_USE_LEMMA); + yield new UseLemmaStatement(stm.getExpression(), pi); + } case MarkerStatementHelper.KIND_MERGE_POINT -> { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java index 6e390ca18b5..1d1328f814c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/MarkerStatementHelper.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMergePointDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLUseLemmaStatement; import com.github.javaparser.ast.DataKey; @@ -20,6 +21,7 @@ public class MarkerStatementHelper { public static final int KIND_ASSUME = 2; public static final int KIND_SET = 3; public static final int KIND_MERGE_POINT = 4; + public static final int KIND_USE_LEMMA = 5; public static final DataKey KEY_ASSIGN = new DataKey<>() { }; @@ -27,4 +29,6 @@ public class MarkerStatementHelper { }; public static final DataKey KEY_ASSERT = new DataKey<>() { }; + public static final DataKey KEY_USE_LEMMA = new DataKey<>() { + }; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java index 6db5f5ed9ed..aacf4fccd70 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java @@ -191,7 +191,7 @@ public JMLTransformer(TransformationPipelineServices services) { * @return the new method declaration * @throws SLTranslationException */ - private @NonNull MethodDeclaration transformMethodDecl(TextualJMLMethodDecl decl, + private @NonNull MethodDeclaration transformMethodDecl(TextualJMLMethodOrLemmaDecl decl, @Nullable TextualJMLModifierList jmlModifiers) throws SLTranslationException { // prepend Java modifiers @@ -248,6 +248,13 @@ private Statement transformSetStatement(TextualJMLSetStatement stat) { return stmt; } + + private Statement transformUseLemmaStatement(TextualJMLUseLemmaStatement stat) { + KeYMarkerStatement stmt = new KeYMarkerStatement(KIND_USE_LEMMA); + stmt.setData(KEY_USE_LEMMA, stat); + return stmt; + } + private KeYMarkerStatement transformMergePointDecl(TextualJMLMergePointDecl stat) { KeYMarkerStatement mps = new KeYMarkerStatement(KIND_MERGE_POINT); mps.setData(KEY_MERGE_POINT, stat); @@ -294,7 +301,7 @@ private void transformClassLevelComments(TypeDeclaration td) throws SLTransla if (c instanceof TextualJMLFieldDecl fd) { // ghost/model field decl.: transform into "real" field decl. td.addMember(transformClassFieldDecl(fd)); - } else if (c instanceof TextualJMLMethodDecl md) { + } else if (c instanceof TextualJMLMethodOrLemmaDecl md) { // model method decl.: final MethodDeclaration decl = transformMethodDecl(md, jmlModifiers); jmlModifiers = null; // these are used now @@ -325,6 +332,8 @@ private void transformClassLevelComments(TypeDeclaration td) throws SLTransla String errorMessage = switch (c) { case TextualJMLSetStatement a -> "A set assignment only allowed inside of a method body"; + case TextualJMLUseLemmaStatement a -> + "A use_lemma statement is only allowed inside of a method body"; case TextualJMLMergePointDecl a -> "Merge points are only allowed inside of a method body"; case TextualJMLLoopSpec a -> @@ -442,6 +451,8 @@ private void transformMethodLevelCommentsAt(BlockStmt blockStmt, URI fileName) // local ghost variable declaration! case TextualJMLFieldDecl field -> statement = transformVariableDecl(field); case TextualJMLSetStatement set -> statement = transformSetStatement(set); + case TextualJMLUseLemmaStatement ulema -> + statement = transformUseLemmaStatement(ulema); case TextualJMLMergePointDecl mergePointDecl -> statement = transformMergePointDecl(mergePointDecl); case TextualJMLAssertStatement assertStatement -> 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 8a7e73b6849..1c974769cd7 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 @@ -607,6 +607,19 @@ ProgramElement createNewElement(ExtList changeList) { def.doAction(x); } + @Override + public void performActionOnUseLemmaStatement(UseLemmaStatement x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + // there are no AST elements below the use lemma statement, so we can use the copy + // constructor. + return new UseLemmaStatement(x); + } + }; + def.doAction(x); + } + @Override public void performActionOnReturn(Return 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 10619d18977..972485a159d 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 @@ -216,6 +216,11 @@ public void performActionOnSetStatement(SetStatement x) { doDefaultAction(x); } + @Override + public void performActionOnUseLemmaStatement(UseLemmaStatement x) { + doDefaultAction(x); + } + @Override public void performActionOnDefault(Default 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 4cc400fdb05..701fbbc0bc2 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 @@ -149,6 +149,8 @@ public interface Visitor { void performActionOnSetStatement(SetStatement x); + void performActionOnUseLemmaStatement(UseLemmaStatement x); + void performActionOnConditional(Conditional x); void performActionOnNewArray(NewArray x); 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 8be2ed213ab..b54c6d086c6 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 @@ -226,6 +226,10 @@ public boolean isModel() { return method.isModel(); } + public boolean isLemma() { + return method.isLemma(); + } + /** * Test whether the declaration is strictfp. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java index 9fd345eaf09..c9035d4c20e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java @@ -10,40 +10,25 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.java.JavaTools; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.SourceElement; import de.uka.ilkd.key.java.ast.statement.JmlAssert; -import de.uka.ilkd.key.java.ast.statement.MethodFrame; -import de.uka.ilkd.key.logic.DefaultVisitor; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.*; -import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; import de.uka.ilkd.key.rule.JmlAssertBuiltInRuleApp; import de.uka.ilkd.key.scripts.ProofScriptEngine; import de.uka.ilkd.key.scripts.ScriptCommandAst; -import de.uka.ilkd.key.scripts.ScriptException; -import de.uka.ilkd.key.scripts.TermWithHoles; -import de.uka.ilkd.key.speclang.njml.JmlLexer; -import de.uka.ilkd.key.speclang.njml.JmlParser; -import de.uka.ilkd.key.speclang.njml.JmlParser.ProofArgContext; -import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdCaseContext; -import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdContext; -import de.uka.ilkd.key.util.MiscTools; -import org.key_project.logic.Term; import org.key_project.logic.op.Modality; import org.key_project.prover.engine.ProverTaskListener; import org.key_project.prover.engine.TaskStartedInfo; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; -import org.key_project.util.java.StringUtil; import org.key_project.util.lookup.Property; -import org.key_project.util.parsing.Location; import org.antlr.v4.runtime.ParserRuleContext; import org.jspecify.annotations.NonNull; @@ -77,7 +62,7 @@ public class ApplyScriptsMacro extends AbstractProofMacro { private static final Logger LOGGER = LoggerFactory.getLogger(ApplyScriptsMacro.class); public static final Property> USER_DATA_JML_OBTAIN_VAR_MAP = - new Property<>("jml.obtainVarMap"); + JmlProofScriptSupport.USER_DATA_JML_OBTAIN_VAR_MAP; private final @Nullable ProofMacro fallBackMacro; @@ -107,51 +92,6 @@ public boolean canApplyTo(Proof proof, ImmutableList<@NonNull Goal> goals, || goals.exists(g -> getJmlAssert(g.node()) != null); } - /** - * A wrapper for a {@link JTerm} that contains obtain variables which need to be resolved - * before the term can be used in proof script execution. - *

- * Obtain variables are placeholders (represented as {@link LocationVariable}) that are - * bound to concrete values during script execution via {@code __obtain} commands. This - * record defers the resolution of these variables until the term is actually needed, - * ensuring proper sequencing where obtain variables must be bound before use. - *

- */ - record ObtainAwareTerm(JTerm term) { - /** - * Resolves all obtain variables in this term by replacing them with their bound - * values from the given obtain map. - * - * @param obtainMap a mapping from obtain variables ({@link LocationVariable}) to their - * bound values ({@link JFunction}); variables not present in this map will - * cause an error if they appear in the term - * @param services the proof services used for term factory operations - * @return a new {@link JTerm} with all obtain variables replaced by their resolved values - * @throws RuntimeException if the term contains an obtain variable that has not been - * bound yet (i.e., appears in the term before being obtained) - */ - JTerm resolve(Map obtainMap, Services services) { - OpReplacer pvr = new OpReplacer(obtainMap, services.getTermFactory()); - JTerm result = pvr.replace(term); - assertNoObtainVarsLeft(result, obtainMap); - return result; - } - - private void assertNoObtainVarsLeft(JTerm term, - Map obtainMap) { - var v = new DefaultVisitor() { - @Override - public void visit(Term visited) { - if (obtainMap.containsKey(term.op())) { - throw new RuntimeException( - "Use of obtain variable before it being obtained: " + term.op()); - } - } - }; - term.execPreOrder(v); - } - } - private static JmlAssert getJmlAssert(Node node) { if (node == null || node.parent() == null) { return null; @@ -171,36 +111,6 @@ private static JmlAssert getJmlAssert(Node node) { return null; } - private static @Nullable OpReplacer getUpdateReplacer(Goal goal) { - RuleApp ruleApp = goal.node().parent().getAppliedRuleApp(); - Term appliedOn = ruleApp.posInOccurrence().subTerm(); - if (appliedOn.op() instanceof UpdateApplication) { - var update = UpdateApplication.getUpdate((JTerm) appliedOn); - Map updates = new LinkedHashMap<>(); - Services services = goal.proof().getServices(); - collectUpdates(update, updates, services); - return new OpReplacer(updates, services.getTermFactory()); - } - return null; - } - - private static void collectUpdates(JTerm update, Map updates, Services services) { - switch (update.op()) { - case ElementaryUpdate eu -> - updates.put(services.getTermBuilder().var((ProgramVariable) eu.lhs()), - update.sub(0)); - - case UpdateJunctor uj -> { - collectUpdates(update.sub(0), updates, services); - collectUpdates(update.sub(1), updates, services); - } - - default -> - throw new IllegalStateException( - "Unexpected update operation: " + update.op().getClass()); - } - } - private static JavaBlock getJavaBlock(Goal goal) { RuleApp ruleApp = goal.node().parent().getAppliedRuleApp(); JTerm appliedOn = (JTerm) ruleApp.posInOccurrence().subTerm(); @@ -232,25 +142,15 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, KeyAst.JMLProofScript proofScript = jmlAssert.getAssertionProof(); Map termMap = - getTermMap(jmlAssert, getJavaBlock(goal), proof.getServices()); + JmlProofScriptSupport.getTermMapForAssert(jmlAssert, getJavaBlock(goal), proof.getServices()); // We heavily rely on that variables have been computed before, otherwise this will // raise an NPE. Map obtainMap = - makeObtainVarMap(jmlAssert.collectVariablesInProof(null)); - OpReplacer updateReplacer = getUpdateReplacer(goal); + JmlProofScriptSupport.makeObtainVarMap(jmlAssert.collectVariablesInProof(null)); + OpReplacer updateReplacer = JmlProofScriptSupport.getUpdateReplacer(goal); List renderedProof = - renderProof(proofScript, termMap, updateReplacer, proof.getServices()); - ProofScriptEngine pse = new ProofScriptEngine(proof); - pse.setInitiallySelectedGoal(goal); - pse.getStateMap().getUserData().set(USER_DATA_JML_OBTAIN_VAR_MAP, obtainMap); - pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class, - oat -> oat.resolve(obtainMap, goal.proof().getServices())); - // TODO: Perhaps have holes also in JML? - pse.getStateMap().getValueInjector().addConverter(TermWithHoles.class, - ObtainAwareTerm.class, - oat -> new TermWithHoles(oat.resolve(obtainMap, goal.proof().getServices()))); - pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class, - oat -> Boolean.parseBoolean(oat.term.toString())); + JmlProofScriptSupport.renderProof(proofScript, termMap, updateReplacer, proof.getServices()); + ProofScriptEngine pse = JmlProofScriptSupport.prepareEngine(proof, goal, obtainMap); LOGGER.debug("---- Script"); LOGGER.debug(renderedProof.stream() .map(ScriptCommandAst::asCommandLine) @@ -274,175 +174,5 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, return new ProofMacroFinishedInfo(this, proof); } - - private Map getTermMap(JmlAssert jmlAssert, JavaBlock javaBlock, - Services services) { - SpecificationRepository.@Nullable JmlStatementSpec jmlspec = - services.getSpecificationRepository().getStatementSpec(jmlAssert); - if (jmlspec == null) { - throw new IllegalStateException( - "No specification found for JML assert statement at " + jmlAssert); - } - ImmutableList terms = ImmutableList.of(); - for (int i = jmlspec.terms().size() - 1; i >= 1; i--) { - terms = terms.prepend(correctSelfVar(i, javaBlock, jmlspec, services)); - } - ImmutableList jmlExprs = jmlAssert.collectTerms().tail(); - Map result = new IdentityHashMap<>(); - assert terms.size() == jmlExprs.size(); - for (int i = 0; i < terms.size(); i++) { - result.put(jmlExprs.get(i), terms.get(i)); - } - return result; - } - - /** - * For some reason, the self variable in the spec is not the same as the self variable and needs - * to - * be corrected. - */ - private JTerm correctSelfVar(int index, JavaBlock javaBlock, - SpecificationRepository.JmlStatementSpec spec, Services services) { - final MethodFrame frame = JavaTools.getInnermostMethodFrame(javaBlock, services); - final JTerm self = MiscTools.getSelfTerm(frame, services); - return spec.getTerm(services, self, index); - - } - - private Map makeObtainVarMap( - ImmutableList locationVariables) { - HashMap result = new LinkedHashMap<>(); - for (LocationVariable lv : locationVariables) { - result.put(lv, null); - } - return result; - } - - private static List renderProof(KeyAst.JMLProofScript script, - Map termMap, @Nullable OpReplacer update, Services services) - throws ScriptException { - List result = new ArrayList<>(); - // Push current settings onto the settings stack - result.add(new ScriptCommandAst("set", Map.of("stack", "push"), List.of())); - // Prepare by resolving the update - result.add(new ScriptCommandAst("oss", Map.of("recentOnly", true), List.of())); - for (ProofCmdContext proofCmdContext : script.ctx.proofCmd()) { - result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); - } - // Pop settings stack to restore old settings - result.add(new ScriptCommandAst("set", Map.of("stack", "pop"), List.of())); - return result; - } - - private static List renderProofCmd(ProofCmdContext ctx, - Map termMap, - @Nullable OpReplacer update, Services services) throws ScriptException { - List result = new ArrayList<>(); - - // Push the current branch context - result.add(new ScriptCommandAst("branches", Map.of(), List.of("push"))); - - // Compose the command itself - if (ctx.obtain != null) { - ScriptCommandAst command = renderObtainCommand(ctx, termMap, update, services); - result.add(command); - } else { - ScriptCommandAst command = renderRegularCommand(ctx, termMap, update, services); - result.add(command); - } - - // handle followup proofCmd if present - JmlParser.ProofCmdSuffixContext suffix = ctx.proofCmdSuffix(); - if (suffix != null) { - if (!suffix.proofCmd().isEmpty()) { - result.add(new ScriptCommandAst("branches", Map.of(), List.of("single"))); - for (ProofCmdContext proofCmdContext : suffix.proofCmd()) { - result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); - } - } - - // handle proofCmdCases if present - for (ProofCmdCaseContext pcase : suffix.proofCmdCase()) { - String label = StringUtil.stripQuotes(pcase.label.getText()); - result.add(new ScriptCommandAst("branches", Map.of("branch", label), - List.of("select"))); - for (ProofCmdContext proofCmdContext : pcase.proofCmd()) { - result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); - } - } - } - - // Pop the branch stack - result.add(new ScriptCommandAst("branches", Map.of(), List.of("pop"))); - - return result; - } - - private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, - Map termMap, - @Nullable OpReplacer update, Services services) throws ScriptException { - Map named = new HashMap<>(); - - String argName = switch (ctx.obtKind.getType()) { - case JmlLexer.SUCH_THAT -> "such_that"; - case JmlLexer.EQUAL_SINGLE -> "equals"; - case JmlLexer.FROM_GOAL -> "from_goal"; - default -> throw new ScriptException("Unknown obtain kind: " + ctx.obtKind.getText()); - }; - - named.put("var", ctx.var.getText()); - - if (ctx.expression() == null) { - named.put(argName, true); - } else { - JmlParser.ExpressionContext exp = ctx.expression(); - Object value; - if (isStringLiteral(exp)) { - value = StringUtil.stripQuotes(exp.getText()); - } else { - value = termMap.get(exp); - if (update != null) { - // Wrap in update application if an update is present - value = update.replace((JTerm) value); - } - } - named.put(argName, value); - } - - return new ScriptCommandAst("__obtain", named, List.of(), Location.fromToken(ctx.start)); - } - - private static @NonNull ScriptCommandAst renderRegularCommand(ProofCmdContext ctx, - Map termMap, @Nullable OpReplacer update, Services services) { - Map named = new HashMap<>(); - List positional = new ArrayList<>(); - for (ProofArgContext argContext : ctx.proofArg()) { - Object value; - JmlParser.ExpressionContext exp = argContext.expression(); - if (isStringLiteral(exp)) { - value = StringUtil.stripQuotes(exp.getText()); - } else { - value = termMap.get(exp); - if (update != null) { - // Wrap in update application if an update is present - value = update.replace((JTerm) value); - } - } - if (value instanceof JTerm term) { - value = new ObtainAwareTerm(term); - } - if (argContext.argLabel != null) { - named.put(argContext.argLabel.getText(), value); - } else { - positional.add(value); - } - } - return new ScriptCommandAst(ctx.cmd.getText(), named, positional, - Location.fromToken(ctx.start)); - } - - - private static boolean isStringLiteral(JmlParser.ExpressionContext ctx) { - return ctx.start == ctx.stop && ctx.start.getType() == JmlParser.STRING_LITERAL; - } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/JmlProofScriptSupport.java b/key.core/src/main/java/de/uka/ilkd/key/macros/JmlProofScriptSupport.java new file mode 100644 index 00000000000..82d71cb4219 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/JmlProofScriptSupport.java @@ -0,0 +1,356 @@ +/* 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.macros; + +import java.util.*; + +import de.uka.ilkd.key.java.JavaTools; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.statement.JmlAssert; +import de.uka.ilkd.key.java.ast.statement.MethodFrame; +import de.uka.ilkd.key.logic.DefaultVisitor; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.OpReplacer; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.mgt.SpecificationRepository; +import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.scripts.ScriptCommandAst; +import de.uka.ilkd.key.scripts.ScriptException; +import de.uka.ilkd.key.scripts.TermWithHoles; +import de.uka.ilkd.key.speclang.njml.JmlIO; +import de.uka.ilkd.key.speclang.njml.JmlLexer; +import de.uka.ilkd.key.speclang.njml.JmlParser; +import de.uka.ilkd.key.speclang.njml.JmlParser.ProofArgContext; +import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdCaseContext; +import de.uka.ilkd.key.speclang.njml.JmlParser.ProofCmdContext; +import de.uka.ilkd.key.speclang.njml.SpecMathMode; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Term; +import org.key_project.prover.rules.RuleApp; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.java.StringUtil; +import org.key_project.util.lookup.Property; +import org.key_project.util.parsing.Location; + +import org.antlr.v4.runtime.ParserRuleContext; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +/** + * Utilities for rendering and executing JML proof scripts across different macros. + * This class centralizes common functionality so macros like ApplyScriptsMacro and + * LemmaAndModelMethodScriptMacro can share logic without duplication. + */ +public final class JmlProofScriptSupport { + + private JmlProofScriptSupport() { + // utility + } + + public static final Property> USER_DATA_JML_OBTAIN_VAR_MAP = + new Property<>("jml.obtainVarMap"); + + /** + * Wrapper around a JTerm that defers resolution of obtain variables until use. + */ + public record ObtainAwareTerm(JTerm term) { + JTerm resolve(Map obtainMap, Services services) { + OpReplacer pvr = new OpReplacer(obtainMap, services.getTermFactory()); + JTerm result = pvr.replace(term); + assertNoObtainVarsLeft(result, obtainMap); + return result; + } + + private void assertNoObtainVarsLeft(JTerm term, + Map obtainMap) { + var v = new DefaultVisitor() { + @Override + public void visit(Term visited) { + if (obtainMap.containsKey(term.op())) { + throw new RuntimeException( + "Use of obtain variable before it being obtained: " + term.op()); + } + } + }; + term.execPreOrder(v); + } + } + + /** + * Create an obtain variable map with all provided variables initialized to null. + */ + public static Map makeObtainVarMap( + ImmutableList locationVariables) { + HashMap result = new LinkedHashMap<>(); + for (LocationVariable lv : locationVariables) { + result.put(lv, null); + } + return result; + } + + /** + * Creates an OpReplacer that applies the update found on the goal's applied rule app, if any. + */ + public static OpReplacer getUpdateReplacer(Goal goal) { + Node parent = goal.node().parent(); + if(parent == null) { + // we can also operate on the root ... + return null; + } + RuleApp ruleApp = parent.getAppliedRuleApp(); + org.key_project.logic.Term appliedOn = ruleApp.posInOccurrence().subTerm(); + if (appliedOn.op() instanceof UpdateApplication) { + var update = UpdateApplication.getUpdate((JTerm) appliedOn); + Map updates = new LinkedHashMap<>(); + Services services = goal.proof().getServices(); + collectUpdates(update, updates, services); + return new OpReplacer(updates, services.getTermFactory()); + } + return null; + } + + private static void collectUpdates(JTerm update, Map updates, Services services) { + switch (update.op()) { + case ElementaryUpdate eu -> + updates.put(services.getTermBuilder().var((ProgramVariable) eu.lhs()), + update.sub(0)); + + case UpdateJunctor uj -> { + collectUpdates(update.sub(0), updates, services); + collectUpdates(update.sub(1), updates, services); + } + + default -> + throw new IllegalStateException( + "Unexpected update operation: " + update.op().getClass()); + } + } + + /** + * Render a JML proof script into a list of script command ASTs. + */ + public static List renderProof(KeyAst.JMLProofScript script, + Map termMap, @Nullable OpReplacer update, Services services) + throws ScriptException { + List result = new ArrayList<>(); + // Push current settings onto the settings stack + result.add(new ScriptCommandAst("set", Map.of("stack", "push"), List.of())); + // Prepare by resolving the update + result.add(new ScriptCommandAst("oss", Map.of("recentOnly", true), List.of())); + for (ProofCmdContext proofCmdContext : script.ctx.proofCmd()) { + result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); + } + // Pop settings stack to restore old settings + result.add(new ScriptCommandAst("set", Map.of("stack", "pop"), List.of())); + return result; + } + + private static List renderProofCmd(ProofCmdContext ctx, + Map termMap, + @Nullable OpReplacer update, Services services) throws ScriptException { + List result = new ArrayList<>(); + + // Push the current branch context + result.add(new ScriptCommandAst("branches", Map.of(), List.of("push"))); + + // Compose the command itself + if (ctx.obtain != null) { + ScriptCommandAst command = renderObtainCommand(ctx, termMap, update, services); + result.add(command); + } else { + ScriptCommandAst command = renderRegularCommand(ctx, termMap, update, services); + result.add(command); + } + + // handle followup proofCmd if present + JmlParser.ProofCmdSuffixContext suffix = ctx.proofCmdSuffix(); + if (suffix != null) { + if (!suffix.proofCmd().isEmpty()) { + result.add(new ScriptCommandAst("branches", Map.of(), List.of("single"))); + for (ProofCmdContext proofCmdContext : suffix.proofCmd()) { + result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); + } + } + + // handle proofCmdCases if present + for (ProofCmdCaseContext pcase : suffix.proofCmdCase()) { + String label = StringUtil.stripQuotes(pcase.label.getText()); + result.add(new ScriptCommandAst("branches", Map.of("branch", label), + List.of("select"))); + for (ProofCmdContext proofCmdContext : pcase.proofCmd()) { + result.addAll(renderProofCmd(proofCmdContext, termMap, update, services)); + } + } + } + + // Pop the branch stack + result.add(new ScriptCommandAst("branches", Map.of(), List.of("pop"))); + + return result; + } + + private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, + Map termMap, + @Nullable OpReplacer update, Services services) throws ScriptException { + Map named = new HashMap<>(); + + String argName = switch (ctx.obtKind.getType()) { + case JmlLexer.SUCH_THAT -> "such_that"; + case JmlLexer.EQUAL_SINGLE -> "equals"; + case JmlLexer.FROM_GOAL -> "from_goal"; + default -> throw new ScriptException("Unknown obtain kind: " + ctx.obtKind.getText()); + }; + + named.put("var", ctx.var.getText()); + + if (ctx.expression() == null) { + named.put(argName, true); + } else { + JmlParser.ExpressionContext exp = ctx.expression(); + Object value; + if (isStringLiteral(exp)) { + value = StringUtil.stripQuotes(exp.getText()); + } else { + value = termMap.get(exp); + if (update != null) { + // Wrap in update application if an update is present + value = update.replace((JTerm) value); + } + } + if (value instanceof JTerm term) { + value = new ObtainAwareTerm(term); + } + named.put(argName, value); + } + + return new ScriptCommandAst("__obtain", named, List.of(), Location.fromToken(ctx.start)); + } + + private static @NonNull ScriptCommandAst renderRegularCommand(ProofCmdContext ctx, + Map termMap, @Nullable OpReplacer update, Services services) { + Map named = new HashMap<>(); + List positional = new ArrayList<>(); + for (ProofArgContext argContext : ctx.proofArg()) { + Object value; + JmlParser.ExpressionContext exp = argContext.expression(); + if (isStringLiteral(exp)) { + value = StringUtil.stripQuotes(exp.getText()); + } else { + value = termMap.get(exp); + if (update != null) { + // Wrap in update application if an update is present + value = update.replace((JTerm) value); + } + } + if (value instanceof JTerm term) { + value = new ObtainAwareTerm(term); + } + if (argContext.argLabel != null) { + named.put(argContext.argLabel.getText(), value); + } else { + positional.add(value); + } + } + return new ScriptCommandAst(ctx.cmd.getText(), named, positional, + Location.fromToken(ctx.start)); + } + + private static boolean isStringLiteral(JmlParser.ExpressionContext ctx) { + return ctx.start == ctx.stop && ctx.start.getType() == JmlParser.STRING_LITERAL; + } + + /** + * Build a map from JML expression contexts to corresponding JTerms for a JML assert. + */ + public static Map getTermMapForAssert(JmlAssert jmlAssert, + JavaBlock javaBlock, Services services) { + SpecificationRepository.@org.jspecify.annotations.Nullable JmlStatementSpec jmlspec = + services.getSpecificationRepository().getStatementSpec(jmlAssert); + if (jmlspec == null) { + throw new IllegalStateException( + "No specification found for JML assert statement at " + jmlAssert); + } + ImmutableList terms = ImmutableList.of(); + for (int i = jmlspec.terms().size() - 1; i >= 1; i--) { + terms = terms.prepend(correctSelfVar(i, javaBlock, jmlspec, services)); + } + ImmutableList jmlExprs = jmlAssert.collectTerms().tail(); + Map result = new IdentityHashMap<>(); + assert terms.size() == jmlExprs.size(); + for (int i = 0; i < terms.size(); i++) { + result.put(jmlExprs.get(i), terms.get(i)); + } + return result; + } + + private static JTerm correctSelfVar(int index, JavaBlock javaBlock, + SpecificationRepository.JmlStatementSpec spec, Services services) { + final MethodFrame frame = JavaTools.getInnermostMethodFrame(javaBlock, services); + final JTerm self = MiscTools.getSelfTerm(frame, services); + return spec.getTerm(services, self, index); + } + + /** + * Prepare a ProofScriptEngine with the standard obtain-variable converters and initial state. + */ + public static ProofScriptEngine prepareEngine(Proof proof, Goal initiallySelected, + Map obtainMap) { + ProofScriptEngine pse = new ProofScriptEngine(proof); + pse.setInitiallySelectedGoal(initiallySelected); + pse.getStateMap().getUserData().set(USER_DATA_JML_OBTAIN_VAR_MAP, obtainMap); + pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class, + oat -> oat.resolve(obtainMap, initiallySelected.proof().getServices())); + // TODO: Perhaps have holes also in JML? + pse.getStateMap().getValueInjector().addConverter(TermWithHoles.class, + ObtainAwareTerm.class, + oat -> new TermWithHoles( + oat.resolve(obtainMap, initiallySelected.proof().getServices()))); + pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class, + oat -> Boolean.parseBoolean(oat.term.toString())); + return pse; + } + + + public static JmlIO prepareJmlIO(Services services, ProgramMethod pm) { + JmlIO io = new JmlIO(services); + if(!pm.isStatic()) { + io.selfVar((LocationVariable) services.getNamespaces().programVariables().lookup("self")); + } + io.classType(pm.getContainerType()); + // FIXME: Make this respect the right math mode (but this is not soundess-critical) + io.specMathMode(SpecMathMode.BIGINT); + // check if this lookup is necessary at all ... + ImmutableList instParams = pm.collectParameters().map(param -> (LocationVariable)services.getNamespaces().programVariables().lookup(param.name())); + io.parameters(instParams); + return io; + } + + public static Map createTermMap( + JmlParser.@Nullable ExpressionContext assertedCond, + KeyAst.JMLProofScript script, + List assignments, + ProgramMethod pm, + JmlIO io, + Services services) { + ImmutableList obtainedVars = script.getObtainedProgramVars(io); + io.parameters(io.getParamVars().prepend(obtainedVars)); + ImmutableList collectedTerms = script.collectTerms(); + if(assertedCond != null) { + collectedTerms = collectedTerms.prepend(assertedCond); + } + Map termMap = new IdentityHashMap<>(); + for (JmlParser.ExpressionContext ectx : collectedTerms) { + JTerm term = io.translateTerm(ectx); + termMap.put(ectx, term); + } + return termMap; + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaMethodScriptMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaMethodScriptMacro.java new file mode 100644 index 00000000000..c76ce879efb --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/LemmaMethodScriptMacro.java @@ -0,0 +1,120 @@ +package de.uka.ilkd.key.macros; + +import de.uka.ilkd.key.control.AbstractUserInterfaceControl; +import de.uka.ilkd.key.control.UserInterfaceControl; +import de.uka.ilkd.key.java.JavaTools; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.statement.JmlAssert; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.ProgramMethod; +import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.OpReplacer; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import de.uka.ilkd.key.rule.JmlAssertBuiltInRuleApp; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.scripts.ScriptCommandAst; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLemmaDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; +import de.uka.ilkd.key.speclang.njml.JmlIO; +import de.uka.ilkd.key.speclang.njml.JmlParser; +import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.tree.ParseTree; +import org.key_project.logic.Name; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Modality; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.engine.ProverTaskListener; +import org.key_project.prover.engine.TaskStartedInfo; +import org.key_project.prover.rules.RuleApp; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.Pair; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import java.util.stream.Collectors; + +public class LemmaMethodScriptMacro extends AbstractProofMacro { + + private static final Logger LOGGER = LoggerFactory.getLogger(LemmaMethodScriptMacro.class); + + public static final String ID = "[A-Za-z_$0-9.]+"; + public static final Pattern NAME_PATTERN = + Pattern.compile(ID + "\\[(" + ID + "::" + ID + ")\\(.*\\)\\].JML model_behavior operation contract.\\d+"); + + public LemmaMethodScriptMacro() { + } + + @Override + public String getName() { + return "lemma-script-auto-macro"; + } + + @Override + public String getCategory() { + return null; + } + + @Override + public String getDescription() { + return "Apply scripts in lemmas and model methods"; + } + + public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { + return ModelMethodScriptMacro.canApplyTo(proof, goals, posInOcc, true); + } + + @Override + public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { + ProgramMethod pm = ModelMethodScriptMacro.extractModelMethod(proof); + assert pm != null : "If canApplyTo gives true, this cannot happen"; + + Goal goal = goals.head(); + + // Currently treat lemmas the same way: if an attached JML assert script is present + // at the current goal, execute it using the shared support. + TextualJMLLemmaDecl methodDecl = + (TextualJMLLemmaDecl) pm.getMethodDeclaration().getAttachedJml().stream().filter(TextualJMLLemmaDecl.class::isInstance).findAny().get(); + JmlParser.Lemma_declarationContext ctx = + (JmlParser.Lemma_declarationContext) methodDecl.getMethodDefinition(); + + JmlIO io = JmlProofScriptSupport.prepareJmlIO(proof.getServices(), pm); + KeyAst.JMLProofScript proofScript = new KeyAst.JMLProofScript(ctx.assertionProof()); + Map termMap = JmlProofScriptSupport.createTermMap(null, proofScript, List.of(), pm, io, proof.getServices()); + + // We heavily rely on that variables have been computed before, otherwise this will + // raise an NPE. + Map obtainMap = + JmlProofScriptSupport.makeObtainVarMap(proofScript.getObtainedProgramVars(null)); + OpReplacer updateReplacer = JmlProofScriptSupport.getUpdateReplacer(goal); + List renderedProof = + JmlProofScriptSupport.renderProof(proofScript, termMap, updateReplacer, proof.getServices()); + ProofScriptEngine pse = JmlProofScriptSupport.prepareEngine(proof, goal, obtainMap); + LOGGER.debug("---- Script"); + LOGGER.debug(renderedProof.stream() + .map(ScriptCommandAst::asCommandLine) + .collect(Collectors.joining("\n"))); + LOGGER.debug("---- End Script"); + + pse.execute((AbstractUserInterfaceControl) uic, renderedProof); + + return new ProofMacroFinishedInfo(this, proof); + + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ModelMethodScriptMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ModelMethodScriptMacro.java new file mode 100644 index 00000000000..3bc02947083 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ModelMethodScriptMacro.java @@ -0,0 +1,306 @@ +package de.uka.ilkd.key.macros; + +import de.uka.ilkd.key.control.AbstractUserInterfaceControl; +import de.uka.ilkd.key.control.UserInterfaceControl; +import de.uka.ilkd.key.java.JavaTools; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.statement.JmlAssert; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.logic.op.ProgramMethod; +import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.JmlAssertBuiltInRuleApp; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.scripts.ScriptCommandAst; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLLemmaDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; +import de.uka.ilkd.key.speclang.njml.JmlIO; +import de.uka.ilkd.key.speclang.njml.JmlParser; +import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.tree.ParseTree; +import org.jspecify.annotations.Nullable; +import org.key_project.logic.Name; +import org.key_project.logic.op.Function; +import org.key_project.logic.op.Modality; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.engine.ProverTaskListener; +import org.key_project.prover.rules.RuleApp; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; + +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import de.uka.ilkd.key.proof.OpReplacer; +import org.key_project.util.collection.Pair; + +public class ModelMethodScriptMacro extends AbstractProofMacro { + + private static final String ID = "[A-Za-z_$0-9.]+"; + private static final Pattern NAME_PATTERN = + Pattern.compile(ID+ "\\[(" + ID + "::" + ID + ")\\(.*\\)\\].JML model_behavior operation contract.\\d+"); + + public ModelMethodScriptMacro() { } + + @Override + public String getName() { + return "model-method-script-auto-macro"; + } + + @Override + public String getCategory() { + return null; + } + + @Override + public String getDescription() { + return "Apply scripts in lemmas and model methods"; + } + + @Override + public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc) { + return canApplyTo(proof, goals, posInOcc, false); + } + + /** + * shared code with {@link LemmaMethodScriptMacro} to determine if the macro + * can be applied to the given proof and goals. + */ + static boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrence posInOcc, boolean expectLemma) { + // only applicable on the root of the proof + // todo change this to allow for subproofs of lemmas and model methods + if (!goals.stream().allMatch(g -> g.node() == proof.root())) + return false; + + ProgramMethod pm = extractModelMethod(proof); + if (pm != null) { + return pm.isLemma() == expectLemma; + } + return false; + } + + /** + * shared code with {@link LemmaMethodScriptMacro} to extract the model method from the proof name + * @param proof proof object whose name is to be parsed + * @return null or the model method behind the proof obligation + */ + static @Nullable ProgramMethod extractModelMethod(Proof proof) { + String name = proof.name().toString(); + Matcher m = NAME_PATTERN.matcher(name); + if(!m.matches()) { + return null; + } + Services services = proof.getServices(); + String lemmaName = m.group(1); + Function function = services.getNamespaces().functions().lookup(lemmaName); + if (function instanceof ProgramMethod pm && pm.isModel()) { + return pm; + } + return null; + } + + record CutTree(List localHistory, JmlParser.ExpressionContext cond, CutTree thenTree, CutTree elseTree) { + + private static final Name CUT_TACLET_NAME = new Name("cut"); + + public CutTree(List localHistory) { + this(localHistory, null, null, null); + } + + public boolean hasAssertions() { + return thenTree != null && thenTree.hasAssertions() || elseTree != null && elseTree.hasAssertions() || + localHistory.stream().anyMatch(x -> x instanceof JmlParser.Assert_statementContext); + } + + public void splitAndExecuteScripts(UserInterfaceControl uic, Goal goal) { + if(!hasAssertions()) { + return; + } + List collectedHistory = new ArrayList<>(); + for (ParseTree parseTree : localHistory) { + switch(parseTree) { + case JmlParser.Mbody_varContext varCtx -> collectedHistory.add(varCtx); + case JmlParser.Assert_statementContext assertCtx -> { + Pair goals = doCut(collectedHistory, goal, assertCtx.expression()); + executeScriptsOnAssertion(uic, goals.second, assertCtx.assertionProof()); + goal = goals.first; + } + default -> throw new IllegalStateException("Unexpected value: " + parseTree); + } + } + if(cond != null) { + Pair goals = doCut(collectedHistory, goal, cond); + thenTree.splitAndExecuteScripts(uic, goals.first); + elseTree.splitAndExecuteScripts(uic, goals.second); + } + } + + private Pair doCut(List assignments, Goal goal, JmlParser.ExpressionContext expression) { + if(!assignments.isEmpty()) { + throw new UnsupportedOperationException("Assignments are not yet supported here"); + } + + Taclet cut = goal.proof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(CUT_TACLET_NAME); + TacletApp app = NoPosTacletApp.createNoPosTacletApp(cut); + SchemaVariable sv = app.uninstantiatedVars().iterator().next(); + + // todo ... + JTerm term = new JmlIO(goal.proof().getServices()).translateTerm(expression); + JTerm formula = goal.proof().getServices().getTermBuilder().convertToFormula(term); + + app = app.addCheckedInstantiation(sv, formula, goal.proof().getServices(), true); + ImmutableList goals = goal.apply(app); + assert goals.size() == 2; + return new Pair<>(goals.get(0), goals.get(1)); + } + } + + + + + + @Override + public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { + String name = proof.name().toString(); + Matcher m = NAME_PATTERN.matcher(name); + if (!m.matches()) + throw new RuntimeException("This macro was not applicable"); + + Services services = proof.getServices(); + String lemmaName = m.group(1); + Function function = services.getNamespaces().functions().lookup(lemmaName); + if(function instanceof ProgramMethod pm && pm.isModel()) { + if(pm.isLemma()) { + return applyToLemma(uic, goals.head(), pm); + } else { + return applyToModel(uic, goals.head(), pm); + } + } else { + // do nothing if this is not a lemma or model method, but return the goals unchanged + return new ProofMacroFinishedInfo(this, goals); + } + } + + private ProofMacroFinishedInfo applyToLemma(UserInterfaceControl uic, Goal root, ProgramMethod pm) { + // Currently treat lemmas the same way: if an attached JML assert script is present + // at the current goal, execute it using the shared support. + TextualJMLLemmaDecl methodDecl = (TextualJMLLemmaDecl) pm.getMethodDeclaration().getAttachedJml().last(); + JmlParser.Lemma_declarationContext ctx = + (JmlParser.Lemma_declarationContext) methodDecl.getMethodDefinition(); + executeScriptsOnAssertion(uic, root, ctx.assertionProof()); + return new ProofMacroFinishedInfo(this, ImmutableList.of(root)); + } + + private ProofMacroFinishedInfo applyToModel(UserInterfaceControl uic, Goal root, ProgramMethod pm) { + TextualJMLMethodDecl methodDecl = (TextualJMLMethodDecl) pm.getMethodDeclaration().getAttachedJml().head(); + JmlParser.Method_declarationContext ctx = + (JmlParser.Method_declarationContext) methodDecl.getMethodDefinition(); + + CutTree cutTree = extractCutTree(ctx.method_body); + + cutTree.splitAndExecuteScripts(uic, root); + + return new ProofMacroFinishedInfo(this, ImmutableList.of(root)); + } + + private static void executeScriptsOnAssertion(UserInterfaceControl uic, Goal goal, JmlParser.AssertionProofContext assertionProofContext) { + JmlAssert jmlAssert = getJmlAssert(goal.node()); + if (jmlAssert == null || jmlAssert.getAssertionProof() == null) { + return; + } + KeyAst.JMLProofScript proofScript = jmlAssert.getAssertionProof(); + JavaBlock javaBlock = getJavaBlock(goal); + Map termMap = + JmlProofScriptSupport.getTermMapForAssert(jmlAssert, javaBlock, goal.proof().getServices()); + Map obtainMap = + JmlProofScriptSupport.makeObtainVarMap(jmlAssert.collectVariablesInProof(null)); + OpReplacer updateReplacer = JmlProofScriptSupport.getUpdateReplacer(goal); + try { + List rendered = JmlProofScriptSupport.renderProof(proofScript, termMap, updateReplacer, goal.proof().getServices()); + ProofScriptEngine pse = JmlProofScriptSupport.prepareEngine(goal.proof(), goal, obtainMap); + pse.execute((AbstractUserInterfaceControl) uic, rendered); + } catch (de.uka.ilkd.key.scripts.ScriptException e) { + throw new RuntimeException(e); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + } + + private static JmlAssert getJmlAssert(Node node) { + if (node == null || node.parent() == null) { + return null; + } + RuleApp ruleApp = node.parent().getAppliedRuleApp(); + if (ruleApp instanceof JmlAssertBuiltInRuleApp) { + JTerm target = (JTerm) ruleApp.posInOccurrence().subTerm(); + if (target.op() instanceof UpdateApplication) { + target = UpdateApplication.getTarget(target); + } + final SourceElement activeStatement = JavaTools.getActiveStatement(target.javaBlock()); + if (activeStatement instanceof JmlAssert jmlAssert + && jmlAssert.getAssertionProof() != null) { + return jmlAssert; + } + } + return null; + } + + private static JavaBlock getJavaBlock(Goal goal) { + RuleApp ruleApp = goal.node().parent().getAppliedRuleApp(); + JTerm appliedOn = (JTerm) ruleApp.posInOccurrence().subTerm(); + if (appliedOn.op() instanceof UpdateApplication) { + appliedOn = UpdateApplication.getTarget(appliedOn); + } + assert appliedOn.op() instanceof Modality; + return appliedOn.javaBlock(); + } + + private CutTree extractCutTree(ParserRuleContext ctx) { + JmlParser.Mbody_statementContext stmCtx; + List localHistory; + + switch(ctx) { + case JmlParser.Mbody_blockContext block -> { + localHistory = block.children.stream(). + filter(x -> x instanceof JmlParser.Mbody_varContext + || x instanceof JmlParser.Assert_statementContext). + toList(); + stmCtx = block.mbody_statement(); + } + case JmlParser.Mbody_statementContext stm -> { + localHistory = List.of(); + stmCtx = stm; + } + default -> throw new IllegalStateException("Unexpected value: " + ctx); + } + + if(stmCtx instanceof JmlParser.Mbody_ifContext ifCtx) { + var cond = ifCtx.getChild(JmlParser.ExpressionContext.class, 0); + var thenBr = ifCtx.getChild(ParserRuleContext.class, 1); + var elseBr = ifCtx.getChild(ParserRuleContext.class, 2); + + CutTree thenTree = extractCutTree(thenBr); + CutTree elseTree = extractCutTree(elseBr); + + if (thenTree.hasAssertions() || elseTree.hasAssertions()) { + return new CutTree(localHistory, cond, thenTree, elseTree); + } + } + return new CutTree(localHistory); + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java index f27bd5e89c1..dc70b839c75 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ScriptAwareMacro.java @@ -40,6 +40,8 @@ public class ScriptAwareMacro extends SequentialProofMacro { private final ProofMacro autoMacro = new SymbolicExecutionOnlyMacro(); + private final ProofMacro lemmaScriptMacro = new LemmaMethodScriptMacro(); + private final ProofMacro modelMethodScriptMacro = new ModelMethodScriptMacro(); private final ApplyScriptsMacro applyMacro = new ApplyScriptsMacro(new TryCloseMacro()); @Override @@ -64,6 +66,6 @@ public String getDescription() { @Override protected ProofMacro[] createProofMacroArray() { - return new ProofMacro[] { autoMacro, applyMacro }; + return new ProofMacro[] { autoMacro, lemmaScriptMacro, modelMethodScriptMacro, applyMacro }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 7d608d9c74f..af5e9043641 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -247,7 +247,7 @@ public Void visitProofCmd(JmlParser.ProofCmdContext ctx) { ProgramElementName name = new ProgramElementName(ctx.var.getText()); collectedVars = collectedVars.prepend(new LocationVariable(name, type, true)); } - return null; + return super.visitProofCmd(ctx); } } 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 09348df07c7..22a1006765d 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 @@ -1743,6 +1743,31 @@ public void performActionOnSetStatement(SetStatement x) { layouter.end(); } + public void performActionOnUseLemmaStatement(UseLemmaStatement x) { + layouter.print("//@ "); + layouter.keyWord("use_lemma"); + + layouter.beginRelativeC(); + layouter.brk(); + + if (services != null) { + var spec = + Objects.requireNonNull(services.getSpecificationRepository().getStatementSpec(x)); + JTerm lemma = spec.term(0); + layouter.print(printInLogicPrinter(lemma)); + } else { + var context = x.getParserContext(); + if (context != null) { + // remove all whitespaces (\n\f\t...) with an empty space + var text = context.getText(); + // text = text.substring(11, text.length() - 1); + layouter.print(text); + } + } + layouter.end(); + } + + public String printInLogicPrinter(JTerm t) { var lp = LogicPrinter.quickPrinter(services, usePrettyPrinting, useUnicodeSymbols, hidePackagePrefix); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java index 9bb8c690572..b3f880c299a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java @@ -88,7 +88,7 @@ public class NodeInfo { private String notes; /** Information about changes respective to the parent of this node. */ - private SequentChangeInfo sequentChangeInfo; + private @Nullable SequentChangeInfo sequentChangeInfo; public NodeInfo(Node node) { this.node = node; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java index dd04fd01632..4d0e743ef40 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java @@ -189,6 +189,7 @@ protected ImmutableList initBuiltInRules() { .prepend(LoopApplyHeadRule.INSTANCE).prepend(JmlAssertRule.ASSERT_INSTANCE) .prepend(JmlAssertRule.ASSUME_INSTANCE) .prepend(SetStatementRule.INSTANCE) + .prepend(UseLemmaStatementRule.INSTANCE) .prepend(ObserverToUpdateRule.INSTANCE); // contract insertion rule, ATTENTION: ProofMgt relies on the fact diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementBuiltInRuleApp.java new file mode 100644 index 00000000000..400511fd71b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementBuiltInRuleApp.java @@ -0,0 +1,52 @@ +/* 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.rule; + +import java.util.Objects; + +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NullMarked; + +/** + * The rule application for {@link de.uka.ilkd.key.java.statement.UseLemmaStatement} + * + * @author Julian Wiesler + */ +@NullMarked +public class UseLemmaStatementBuiltInRuleApp extends AbstractBuiltInRuleApp { + /** + * @param rule the rule being applied + * @param occurrence the position at which the rule is applied + */ + public UseLemmaStatementBuiltInRuleApp(UseLemmaStatementRule rule, PosInOccurrence occurrence) { + super(rule, Objects.requireNonNull(occurrence, "rule application needs a position"), null); + if (rule == null) { + throw new IllegalArgumentException(String.format( + "can only create an application for SetStatementRule, not for %s", rule)); + } + } + + @Override + public UseLemmaStatementBuiltInRuleApp replacePos(PosInOccurrence newPos) { + return new UseLemmaStatementBuiltInRuleApp(rule(), newPos); + } + + @Override + public IBuiltInRuleApp setAssumesInsts(ImmutableList ifInsts) { + // XXX: This is overridden in all subclasses to allow making ifInsts final + // when all usages of setIfInsts are corrected to use the result. + // Then a new instance has to be returned here. + setMutable(ifInsts); + return this; + } + + @Override + public UseLemmaStatementBuiltInRuleApp tryToInstantiate(Goal goal) { + return this; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementRule.java new file mode 100644 index 00000000000..4ad498e865f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseLemmaStatementRule.java @@ -0,0 +1,148 @@ +/* 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.rule; + +import java.util.Optional; + +import de.uka.ilkd.key.java.JavaTools; +import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.statement.MethodFrame; +import de.uka.ilkd.key.java.ast.statement.UseLemmaStatement; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.TermBuilder; +import de.uka.ilkd.key.logic.TermServices; +import de.uka.ilkd.key.logic.op.ProgramMethod; +import de.uka.ilkd.key.logic.op.Transformer; +import de.uka.ilkd.key.logic.op.UpdateApplication; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.Name; +import org.key_project.logic.op.Modality; +import org.key_project.prover.rules.RuleAbortException; +import org.key_project.prover.rules.RuleApp; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NonNull; + +/** + * A rule for use_lemma statements. This turns a statement `use_lemma lemma(x)` to an assumption + * `lemma(x) = TRUE` which allows rules to be applied that set the expand the contract. + * + * @author Mattias Ulbrich + */ +public final class UseLemmaStatementRule implements BuiltInRule { + + /** + * The instance + */ + public static final UseLemmaStatementRule INSTANCE = new UseLemmaStatementRule(); + + /** + * The name of this rule + */ + private static final Name name = new Name("Use Lemma Statement"); + + private UseLemmaStatementRule() { + // no statements + } + + @Override + public boolean isApplicable(Goal goal, + PosInOccurrence occurrence) { + if (AbstractAuxiliaryContractRule.occursNotAtTopLevelInSuccedent(occurrence)) { + return false; + } + // abort if inside of transformer + if (Transformer.inTransformer(occurrence)) { + return false; + } + + JTerm target = (JTerm) occurrence.subTerm(); + if (target.op() instanceof UpdateApplication) { + target = UpdateApplication.getTarget(target); + } + final SourceElement activeStatement = JavaTools.getActiveStatement(target.javaBlock()); + return activeStatement instanceof UseLemmaStatement; + } + + @Override + public boolean isApplicableOnSubTerms() { + return false; + } + + @Override + public IBuiltInRuleApp createApp(PosInOccurrence occurrence, TermServices services) { + return new UseLemmaStatementBuiltInRuleApp(this, occurrence); + } + + @Override + public @NonNull ImmutableList apply(Goal goal, RuleApp ruleApp) + throws RuleAbortException { + if (!(ruleApp instanceof UseLemmaStatementBuiltInRuleApp)) { + throw new IllegalArgumentException("can only apply UseLemmaStatementBuiltInRuleApp"); + } + + final var services = goal.getOverlayServices(); + final TermBuilder tb = services.getTermBuilder(); + final PosInOccurrence occurrence = ruleApp.posInOccurrence(); + final JTerm formula = (JTerm) occurrence.subTerm(); + assert formula.op() instanceof UpdateApplication + : "Currently, this can only be applied if there is an update application in front of the modality"; + + JTerm update = UpdateApplication.getUpdate(formula); + JTerm target = UpdateApplication.getTarget(formula); + + UseLemmaStatement useLemmaStatement = + Optional.ofNullable(JavaTools.getActiveStatement(target.javaBlock())) + .filter(UseLemmaStatement.class::isInstance).map(UseLemmaStatement.class::cast) + .orElseThrow(() -> new RuleAbortException("not a JML set statement.")); + + final MethodFrame frame = JavaTools.getInnermostMethodFrame(target.javaBlock(), services); + final JTerm self = MiscTools.getSelfTerm(frame, services); + + var spec = services.getSpecificationRepository().getStatementSpec(useLemmaStatement); + + if (spec == null) { + throw new RuleAbortException( + "No specification for the set statement found in the specification repository."); + } + + var targetTerm = spec.getTerm(services, self, 0); + var assumption = tb.equals(targetTerm, tb.TRUE()); + + assert targetTerm.op() instanceof ProgramMethod pm && pm.isLemma(); + + JTerm updatedAssumption = tb.apply(update, assumption); + + JavaBlock javaBlock = JavaTools.removeActiveStatement(target.javaBlock(), services); + + JTerm term = + tb.prog(((Modality) target.op()).kind(), javaBlock, target.sub(0), target.getLabels()); + JTerm newTerm = tb.apply(update, term); + + ImmutableList result = goal.split(1); + result.head().changeFormula(new SequentFormula(newTerm), occurrence); + result.head().addFormula(new SequentFormula(updatedAssumption), true, true); + return result; + } + + @Override + public Name name() { + return name; + } + + @Override + public String displayName() { + return name.toString(); + } + + @Override + public String toString() { + return name.toString(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java index 86a6ba85cf9..4815c51b0ce 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java @@ -192,6 +192,10 @@ public void performActionOnSetStatement(SetStatement x) { handleJmlStatement(x); } + public void performActionOnUseLemmaStatement(UseLemmaStatement x) { + handleJmlStatement(x); + } + private void handleJmlStatement(Statement x) { var spec = Objects.requireNonNull(services.getSpecificationRepository().getStatementSpec(x)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java index a9dc8f557f5..af328945eb9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java @@ -136,7 +136,7 @@ private Goal findGoalByName(Node root, String branch) throws ScriptException { int number = 1; while (it.hasNext()) { Node node = it.next(); - String label = node.getNodeInfo().getBranchLabel(); + String label = state.getLabel(node); if (label == null) { label = "Case " + number; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java index 7fb7396fc97..5847959a30e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/CutCommand.java @@ -6,6 +6,7 @@ import java.util.List; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; @@ -16,6 +17,7 @@ import org.key_project.logic.op.sv.SchemaVariable; import org.checkerframework.checker.nullness.qual.MonotonicNonNull; +import org.key_project.util.collection.ImmutableList; /** * The command object CutCommand has as scriptcommand name "cut" As parameters: a formula with the @@ -55,7 +57,8 @@ static void execute(EngineState state, Parameters args) throws ScriptException { state.getProof().getServices().getTermBuilder().convertToFormula(args.formula); app = app.addCheckedInstantiation(sv, formula, state.getProof().getServices(), true); - state.getFirstOpenAutomaticGoal().apply(app); + ImmutableList goals = state.getFirstOpenAutomaticGoal().apply(app); + state.labelGoals(goals, "false", "true"); } @Documentation(category = "Fundamental", value = """ diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java index ef33be520e2..38a3b95d3e1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/EngineState.java @@ -63,6 +63,8 @@ public class EngineState { private final PLookup userData = new PLookup(); + private final Map labelMap = new HashMap<>(); + /** * If set to true, outputs all commands to observers and console. Otherwise, only shows explicit * echo messages. @@ -377,4 +379,17 @@ ExprEvaluator getEvaluator() { public PLookup getUserData() { return userData; } + + public void labelGoals(ImmutableList goals, String... labels) { + if (goals.size() != labels.length) { + throw new IllegalStateException("The produced goals and their labels must habe same cardinality."); + } + for(int i = 0; i < labels.length; i++) { + labelMap.put(goals.get(i).node().serialNr(), labels[i]); + } + } + + public @Nullable String getLabel(Node node) { + return labelMap.getOrDefault(node.serialNr(), node.getNodeInfo().getBranchLabel()); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java index 361a73814f6..9bef446d077 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/InstantiateCommand.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.scripts; +import java.util.List; import java.util.Objects; import de.uka.ilkd.key.java.Services; @@ -221,6 +222,11 @@ public String getName() { return "instantiate"; } + @Override + public List getAliases() { + return List.of("inst"); + } + @Documentation(category = "Fundamental", value = """ Instantiate a universally quantified formula (in the antecedent; diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java index dc7eb462f5c..909c107b143 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java @@ -89,8 +89,17 @@ public void execute(ScriptCommandAst ast) private JTerm executeFromGoal(LocationVariable var) throws ScriptException { Goal goal = state.getFirstOpenAutomaticGoal(); - // This works under the assumption that the last succedent formula is the "goal" formula. - SequentFormula sequentFormula = goal.node().sequent().succedent().getLast(); + // Pick the most recently changed succedent formula as the goal formula. + var sci = goal.node().getNodeInfo().getSequentChangeInfo().getSemisequentChangeInfo(false); + SequentFormula sequentFormula; + if (!sci.addedFormulas().isEmpty()) { + sequentFormula = sci.addedFormulas().get(0); + } else if (!sci.modifiedFormulas().isEmpty()) { + sequentFormula = sci.modifiedFormulas().get(0).newFormula(); + } else { + // Fallback to last succedent if no change info is available + sequentFormula = goal.node().sequent().succedent().getLast(); + } JTerm formula = (JTerm) sequentFormula.formula(); while (formula.op() instanceof UpdateApplication) { formula = formula.sub(1); @@ -124,26 +133,79 @@ private JTerm executeFromGoal(LocationVariable var) throws ScriptException { return app.instantiations().getInstantiation(sk); } - private SequentFormula identifySequentFormula(Node node) { - SemisequentChangeInfo changes = - node.getNodeInfo().getSequentChangeInfo().getSemisequentChangeInfo(false); - ImmutableList added = changes.addedFormulas(); - if (!added.isEmpty()) { - if (added.size() == 1) { - return added.get(0); - } - } else { - ImmutableList modified = changes.modifiedFormulas(); - if (modified.size() == 1) { - return modified.get(0).newFormula(); + private JTerm executeSuchThat(LocationVariable var, @Nullable JTerm suchThat) + throws ScriptException { + if (suchThat == null) { + throw new ScriptException("'such_that' must not be null"); + } + + Services services = state().getProof().getServices(); + var tb = services.getTermBuilder(); + + // 1) Replace program variable by a fresh logical variable in the condition. + String base = var.name().toString(); + String lvName = VariableNameProposer.DEFAULT.getNameProposal(base, services, null); + LogicVariable lv = new LogicVariable(new Name(lvName), var.sort()); + + JTerm progVarTerm = tb.var(var); + JTerm lvTerm = tb.var(lv); + JTerm condWithLv = OpReplacer.replace(progVarTerm, lvTerm, suchThat, + services.getTermFactory(), state().getProof()); + + // 2) Ensure it is a formula + JTerm asFormula = tb.convertToFormula(condWithLv); + + // 3) Existentially quantify and cut on it + JTerm exFormula = tb.ex(lv, asFormula); + + Taclet cut = state.getProof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(new Name("cut")); + TacletApp cutApp = NoPosTacletApp.createNoPosTacletApp(cut); + SchemaVariable cutSv = cutApp.uninstantiatedVars().iterator().next(); + cutApp = cutApp.addCheckedInstantiation(cutSv, exFormula, services, true); + ImmutableList goals = state.getFirstOpenAutomaticGoal().apply(cutApp); + + // 4) On the antecedent branch, apply exLeft to introduce a Skolem constant + TermComparisonWithHoles cmp = new TermComparisonWithHoles(exFormula); + Goal antecedentGoal = null; + SequentFormula targetSf = null; + for (Goal g : goals) { + var matches = cmp.findTopLevelMatchesInSequent(g.node().sequent()); + for (var m : matches) { + if (Boolean.TRUE.equals(m.first)) { + antecedentGoal = g; + targetSf = m.second; + break; + } } + if (antecedentGoal != null) break; } - throw new IllegalStateException( - "Multiple or no formulas modified or added in last step, cannot identify sequent formula to skolemize."); - } + if (antecedentGoal == null || targetSf == null) { + throw new ScriptException("Could not locate antecedent \\exists-formula after cut."); + } + + FindTaclet exLeft = (FindTaclet) state.getProof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(new Name("exLeft")); + PosInOccurrence pio = new PosInOccurrence(targetSf, PosInTerm.getTopLevel(), true); + MatchConditions mc = new MatchConditions(); + TacletApp exApp = PosTacletApp.createPosTacletApp(exLeft, mc, pio, services); + + var schemaVars = ImmutableSet.from(exLeft.collectSchemaVars()); + SchemaVariable u = getSV(schemaVars, "u"); + SchemaVariable b = getSV(schemaVars, "b"); + SchemaVariable sk = getSV(schemaVars, "sk"); + + exApp = exApp.addInstantiation(u, + services.getTermBuilder().tf().createTerm(targetSf.formula().boundVars().get(0)), + true, services); + exApp = exApp.addInstantiation(b, targetSf.formula().sub(0), true, services); + + String skName = VariableNameProposer.DEFAULT.getNameProposal(base, services, null); + exApp = exApp.createSkolemConstant(skName, sk, + targetSf.formula().boundVars().get(0).sort(), true, services); - private JTerm executeSuchThat(LocationVariable var, @Nullable JTerm suchThat) { - throw new UnsupportedOperationException("such_that not yet supported in obtain."); + antecedentGoal.apply(exApp); + return exApp.instantiations().getInstantiation(sk); } private JTerm executeEquals(LocationVariable var, @Nullable JTerm equals) diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/OneStepSimplifierCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/OneStepSimplifierCommand.java index 1aefe9ccb8c..74fd6f45dba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/OneStepSimplifierCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/OneStepSimplifierCommand.java @@ -41,6 +41,10 @@ public void execute(ScriptCommandAst command) throws ScriptException, Interrupte if (Boolean.TRUE.equals(arguments.recentOnly)) { SequentChangeInfo sci = goal.node().getNodeInfo().getSequentChangeInfo(); + if(sci == null) { + // sci is null for the root node ... + return; + } var ante = sci.addedFormulas(true) .prepend(sci.modifiedFormulas(true).map(FormulaChangeInfo::newFormula)); applyOSS(ante, goal, true); diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/UseLemmaCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/UseLemmaCommand.java new file mode 100644 index 00000000000..d2adfb4ee9b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/UseLemmaCommand.java @@ -0,0 +1,157 @@ +/* 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.scripts; + +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.scripts.meta.Argument; +import de.uka.ilkd.key.scripts.meta.Documentation; +import de.uka.ilkd.key.rule.FindTaclet; +import de.uka.ilkd.key.rule.PosTacletApp; +import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; +import org.key_project.logic.Name; +import org.key_project.logic.PosInTerm; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.Taclet; +import org.key_project.util.collection.ImmutableList; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.prover.proof.rulefilter.TacletFilter; + +import java.util.List; +import java.util.NoSuchElementException; + +/** + * The command object CutCommand has as scriptcommand name "cut" As parameters: a formula with the + * id "#2" + */ +public class UseLemmaCommand extends AbstractCommand { + private static final Name INTRO_TACLET_NAME = new Name("intro"); + + public UseLemmaCommand() { + super(Parameters.class); + } + + @Override + public String getName() { + return "use_lemma"; + } + + @Override + public void execute(ScriptCommandAst arguments) throws ScriptException, InterruptedException { + var args = state().getValueInjector().inject(new Parameters(), arguments); + execute(state(), args); + } + + static void execute(EngineState state, Parameters args) throws ScriptException { + de.uka.ilkd.key.rule.Taclet intro = state.getProof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(INTRO_TACLET_NAME); + TacletApp app = NoPosTacletApp.createNoPosTacletApp(intro); + + // Explicitly instantiate skolem with the concrete sort of the term (e.g., boolean), + // then instantiate schema variable "t" with the provided term. + var services = state.getProof().getServices(); + SchemaVariable sk = getSV(app, "sk"); + SchemaVariable t = getSV(app, "t"); + + // Use a deterministic name for the skolem; the specific name is not important here. + app = app.createSkolemConstant("use_lemma_sk", sk, args.term.sort(), true, services); + app = app.addCheckedInstantiation(t, args.term, services, true); + + // Apply the intro rule (adds equality to antecedent) + Goal goalAfterIntro = state.getFirstOpenAutomaticGoal(); + ImmutableList afterIntro = goalAfterIntro.apply(app); + Goal workGoal = afterIntro.head(); + + // Identify the added equality sequent formula and apply the Contract_axiom_for_* taclet on the left-hand term + SequentFormula eqFormula = workGoal.sequent().getFormulaByNr(1); + var posLeftTerm = new PosInOccurrence(eqFormula, PosInTerm.getTopLevel().down(0), true); + + // Query taclet apps at/below the method call position that start with "Contract_axiom_for_" + var index = workGoal.ruleAppIndex(); + TacletFilter contractAxiomFilter = new TacletFilter() { + @Override + protected boolean filter(Taclet taclet) { + return taclet.name().toString().startsWith("Contract_axiom_for_"); + } + }; + var matchingApps = index.getTacletAppAtAndBelow(contractAxiomFilter, posLeftTerm, services); + if (matchingApps.isEmpty()) { + throw new ScriptException("No applicable Contract_axiom_for_* rule found at the lemma/method call term."); + } + TacletApp contractApp = matchingApps.head(); + var completedContractApp = contractApp.tryToInstantiate(services); + if (completedContractApp != null) { + contractApp = completedContractApp; + } + ImmutableList afterContract = workGoal.apply(contractApp); + + // Hide the equality we introduced + if (afterContract != null && !afterContract.isEmpty()) { + for (Goal g2 : afterContract) { + try { + SequentFormula changed = identifyAddedOrModifiedSequentFormula(g2); + hideAntecedentFormula(g2, changed); + } catch (Exception ignore) { + // best-effort hiding; skip if not identifiable + } + } + } else { + hideAntecedentFormula(workGoal, eqFormula); + } + } + + private static SchemaVariable getSV(TacletApp app, String name) throws ScriptException { + for (SchemaVariable sv : app.uninstantiatedVars()) { + if (sv.name().toString().equals(name)) { + return sv; + } + } + throw new ScriptException("intro taclet: schema variable '" + name + "' not found"); + } + + // Determine which sequent formula got added or modified by the last step on this goal + private static SequentFormula identifyAddedOrModifiedSequentFormula(Goal goal) { + var changes = goal.node().getNodeInfo().getSequentChangeInfo().getSemisequentChangeInfo(false); + var added = changes.addedFormulas(); + if (!added.isEmpty()) { + return added.get(0); + } + var modified = changes.modifiedFormulas(); + if (!modified.isEmpty()) { + return modified.get(0).newFormula(); + } + throw new NoSuchElementException("Cannot identify added or modified sequent formula after intro."); + } + + private static void hideAntecedentFormula(Goal g, SequentFormula toHide) { + // hide_left applies to antecedent + var tac = g.proof().getEnv().getInitConfigForEnvironment() + .lookupActiveTaclet(new Name("hide_left")); + var pio = new PosInOccurrence(toHide, PosInTerm.getTopLevel(), true); + TacletApp app = PosTacletApp.createPosTacletApp((FindTaclet) tac, SVInstantiations.EMPTY_SVINSTANTIATIONS, pio, + g.proof().getServices()); + // instantiate the single schema variable of hide rule with the full formula + SchemaVariable sv = app.uninstantiatedVars().iterator().next(); + app = app.addCheckedInstantiation(sv, (JTerm) toHide.formula(), g.proof().getServices(), true); + g.apply(app); + } + + @Documentation(category = "Fundamental", value = """ + The cut command makes a case distinction (a cut) on a formula on the current proof goal. + From within JML scripts, the alias 'assert' is more common than using 'cut'. + If followed by a `\\by proof` suffix in JML, it refers the sequent where + the cut formula is introduced to the succedent (i.e. where it is to be established). + """) + public static class Parameters { + @Argument + @Documentation("The lemma to invoke") + public @MonotonicNonNull JTerm term; + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java index 44dec7429b0..1133703738e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java @@ -246,6 +246,8 @@ protected void doAction(final ProgramElement node) { jsf.translateJmlAssertCondition((JmlAssert) node, pm); } else if (node instanceof SetStatement) { jsf.translateSetStatement((SetStatement) node, pm); + } else if (node instanceof UseLemmaStatement useLemmaStatement) { + jsf.translateUseLemmaStatement(useLemmaStatement, pm); } } catch (ProofInputException e) { // Store the first exception that occurred diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java index 63e2ecda3c4..5f7487dda02 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java @@ -295,7 +295,7 @@ public List extractMethodSpecs(IProgramMethod pm, boolean ParserRuleContext modelMethodDefinition = null; for (var c : constructs) { - if (c instanceof TextualJMLMethodDecl m) { + if (c instanceof TextualJMLMethodOrLemmaDecl m) { if (pm.getMethodDeclaration().containsModifier(ModifierKind.JML_MODEL)) { modelMethodDefinition = m.getMethodDefinition(); break; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLemmaDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLemmaDecl.java new file mode 100644 index 00000000000..feba6cea7d6 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLemmaDecl.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.speclang.jml.pretranslation; + +import java.util.Objects; + +import de.uka.ilkd.key.speclang.njml.JmlParser; + +import org.key_project.util.collection.ImmutableList; + +import org.antlr.v4.runtime.ParserRuleContext; + +/** + * A JML lemma declaration in textual form. + * + * This is a special case of a textual JML method declaration. + */ +public final class TextualJMLLemmaDecl extends TextualJMLMethodOrLemmaDecl { + private final JmlParser.Lemma_declarationContext lemmaDefinition; + + + public TextualJMLLemmaDecl(ImmutableList modifiers, + JmlParser.Lemma_declarationContext lemmaDefinition) { + super(modifiers.append(JMLModifier.MODEL)); + this.lemmaDefinition = lemmaDefinition; + setPosition(lemmaDefinition); + } + + public String getMethodName() { + return lemmaDefinition.IDENT().getText(); + } + + public ParserRuleContext getMethodDefinition() { + return lemmaDefinition; + } + + @Override + public String toString() { + return lemmaDefinition.getText(); + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + TextualJMLLemmaDecl that = (TextualJMLLemmaDecl) o; + return Objects.equals(lemmaDefinition, that.lemmaDefinition); + } + + @Override + public int hashCode() { + return Objects.hash(lemmaDefinition); + } + + public int getStateCount() { + if (modifiers.contains(JMLModifier.TWO_STATE)) { + return 2; + } + if (modifiers.contains(JMLModifier.NO_STATE)) { + return 0; + } + return 1; + } + + @Override + protected JmlParser.Param_listContext getParamListContext() { + return lemmaDefinition.param_list(); + } + + @Override + protected String getTypespecText() { + return "boolean"; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java index 9b3aed84fea..f581d979471 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java @@ -4,23 +4,19 @@ package de.uka.ilkd.key.speclang.jml.pretranslation; import java.util.Objects; -import java.util.stream.Collectors; -import de.uka.ilkd.key.java.transformations.pipeline.JMLTransformer; import de.uka.ilkd.key.speclang.njml.JmlParser; import org.key_project.util.collection.ImmutableList; -import org.key_project.util.java.StringUtil; import org.antlr.v4.runtime.ParserRuleContext; /** * A JML model method declaration in textual form. */ -public final class TextualJMLMethodDecl extends TextualJMLConstruct { +public final class TextualJMLMethodDecl extends TextualJMLMethodOrLemmaDecl { private final JmlParser.Method_declarationContext methodDefinition; - public TextualJMLMethodDecl(ImmutableList modifiers, JmlParser.Method_declarationContext methodDefinition) { super(modifiers); @@ -28,38 +24,16 @@ public TextualJMLMethodDecl(ImmutableList modifiers, setPosition(methodDefinition); } - public String getParsableDeclaration() { - String m = modifiers.stream().map(it -> { - if (JMLTransformer.JAVA_MODS.contains(it)) { - return it.toString(); - } else { - JMLModifier jmlModifier = JMLModifier.valueOf(it.name()); - if (jmlModifier == JMLModifier.NON_NULL || jmlModifier == JMLModifier.NULLABLE) { - return "/*@ " + jmlModifier + " @*/"; - } else { - return StringUtil.repeat(" ", it.toString().length()); - } - } - }).collect(Collectors.joining(" ")); - - String paramsString = methodDefinition.param_list().param_decl().stream() - .map(it -> (it.NULLABLE() != null ? "/*@ nullable @*/" - : it.NON_NULL() != null ? "/*@ non_null @*/" : "") - + " " + it.typespec().getText() + " " + it.p.getText() - + StringUtil.repeat("[]", it.LBRACKET().size())) - .collect(Collectors.joining(",")); - return String.format("%s %s %s (%s);", m, methodDefinition.typespec().getText(), - getMethodName(), paramsString); - } - - public JmlParser.Method_declarationContext getDecl() { - return methodDefinition; - } + // public JmlParser.Method_declarationContext getDecl() { + // return methodDefinition; + // } + @Override public String getMethodName() { return methodDefinition.IDENT().getText(); } + @Override public ParserRuleContext getMethodDefinition() { return methodDefinition; } @@ -86,14 +60,13 @@ public int hashCode() { return Objects.hash(methodDefinition); } - public int getStateCount() { - if (modifiers.contains(JMLModifier.TWO_STATE)) { - return 2; - } - if (modifiers.contains(JMLModifier.NO_STATE)) { - return 0; - } - return 1; + @Override + protected JmlParser.Param_listContext getParamListContext() { + return methodDefinition.param_list(); } + @Override + protected String getTypespecText() { + return methodDefinition.typespec().getText(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodOrLemmaDecl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodOrLemmaDecl.java new file mode 100644 index 00000000000..f63f916a62f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodOrLemmaDecl.java @@ -0,0 +1,63 @@ +/* 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.speclang.jml.pretranslation; + +import java.util.stream.Collectors; + +import de.uka.ilkd.key.java.transformations.pipeline.JMLTransformer; +import de.uka.ilkd.key.speclang.njml.JmlParser; + +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.java.StringUtil; + +import org.antlr.v4.runtime.ParserRuleContext; + +public abstract class TextualJMLMethodOrLemmaDecl extends TextualJMLConstruct { + + public TextualJMLMethodOrLemmaDecl(ImmutableList specModifiers) { + super(specModifiers); + } + + public String getParsableDeclaration() { + String m = modifiers.stream().map(it -> { + if (JMLTransformer.JAVA_MODS.contains(it)) { + return it.toString(); + } else { + JMLModifier jmlModifier = JMLModifier.valueOf(it.name()); + if (jmlModifier == JMLModifier.NON_NULL || jmlModifier == JMLModifier.NULLABLE) { + return "/*@ " + jmlModifier + " @*/"; + } else { + return StringUtil.repeat(" ", it.toString().length()); + } + } + }).collect(Collectors.joining(" ")); + + String paramsString = getParamListContext().param_decl().stream() + .map(it -> (it.NULLABLE() != null ? "/*@ nullable @*/" + : it.NON_NULL() != null ? "/*@ non_null @*/" : "") + + " " + it.typespec().getText() + " " + it.p.getText() + + StringUtil.repeat("[]", it.LBRACKET().size())) + .collect(Collectors.joining(",")); + return String.format("%s %s %s (%s);", m, getTypespecText(), + getMethodName(), paramsString); + } + + protected abstract JmlParser.Param_listContext getParamListContext(); + + protected abstract String getTypespecText(); + + public abstract String getMethodName(); + + public abstract ParserRuleContext getMethodDefinition(); + + public int getStateCount() { + if (modifiers.contains(JMLModifier.TWO_STATE)) { + return 2; + } + if (modifiers.contains(JMLModifier.NO_STATE)) { + return 0; + } + return 1; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLUseLemmaStatement.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLUseLemmaStatement.java new file mode 100644 index 00000000000..dee02c371f0 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLUseLemmaStatement.java @@ -0,0 +1,62 @@ +/* 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.speclang.jml.pretranslation; + +import java.util.List; + +import de.uka.ilkd.key.speclang.njml.JmlParser; + +import org.key_project.util.collection.ImmutableList; + +/** + * A JML "use_lemma" statement in textual form. + */ +public final class TextualJMLUseLemmaStatement extends TextualJMLConstruct { + + private final JmlParser.Use_lemma_statementContext statement; + + + public TextualJMLUseLemmaStatement(ImmutableList modifiers, + JmlParser.Use_lemma_statementContext statement) { + super(modifiers); + assert statement != null; + this.statement = statement; + } + + public boolean isSuitableExpression() { + JmlParser.PostfixexprContext postfix = statement.postfixexpr(); + JmlParser.PrimaryexprContext prim = postfix.primaryexpr(); + List primarysuffix = postfix.primarysuffix(); + if (primarysuffix.size() != 1) { + return false; + } + JmlParser.PrimarysuffixContext args = primarysuffix.get(0); + if (!(args instanceof JmlParser.PrimarySuffixCallContext)) { + return false; + } + return true; + } + + public JmlParser.PostfixexprContext getExpression() { + return statement.postfixexpr(); + } + + @Override + public String toString() { + return statement.toString(); + } + + @Override + public boolean equals(Object o) { + if (!(o instanceof TextualJMLUseLemmaStatement ss)) { + return false; + } + return modifiers.equals(ss.modifiers) && statement.equals(ss.statement); + } + + @Override + public int hashCode() { + return modifiers.hashCode() + statement.hashCode(); + } +} 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 16748c266ee..2f34ff9f33b 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 @@ -1596,6 +1596,30 @@ public void translateSetStatement(final SetStatement statement, final IProgramMe new SpecificationRepository.JmlStatementSpec(pv, ImmutableList.of(assignee, value))); } + + public void translateUseLemmaStatement(final UseLemmaStatement statement, + final IProgramMethod pm) + throws SLTranslationException { + final var pv = createProgramVariablesForStatement(statement, pm); + JmlParser.PostfixexprContext context = statement.getParserContext(); + var io = new JmlIO(services).context(Context.inMethod(pm, tb)).selfVar(pv.selfVar) + .parameters(pv.paramVars) + .resultVariable(pv.resultVar).exceptionVariable(pv.excVar).atPres(pv.atPres) + .atBefore(pv.atBefores); + JTerm lemmaCall = io.translateTerm(context); + + if (lemmaCall.op() instanceof ProgramMethod lpm && !lpm.isLemma()) { + throw new SLTranslationException( + "Invalid lemma call for use_lemma statement (only lemma invocations allowed): " + + lemmaCall, + Location.fromToken(context.getStart())); + } + + services.getSpecificationRepository().addStatementSpec( + statement, + new SpecificationRepository.JmlStatementSpec(pv, ImmutableList.of(lemmaCall))); + } + /** * If the LHS of a set statement has been translated into a final term, this method undoes this * encoding since LHS need to be encoded as select terms for KeY's mechanisms to works. diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java index 920da1e5ea3..5bac579bbc6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java @@ -376,13 +376,20 @@ public JmlIO specMathMode(@NonNull SpecMathMode specMathMode) { } /** - * Sets the current list of known parameter. Can also be used to give additionally variables. + * Sets the current list of known parameter. Can also be used to give additional variables. */ public JmlIO parameters(ImmutableList params) { this.paramVars = params; return this; } + /** + * Gets the list of known parameters (and additional variables). + */ + public @Nullable ImmutableList getParamVars() { + return paramVars; + } + /** * Sets the variable that is used to store exceptions. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java index 16b25347d77..1df50932dec 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java @@ -496,6 +496,13 @@ public Object visitMethod_declaration(JmlParser.Method_declarationContext ctx) { return null; } + @Override + public Object visitLemma_declaration(JmlParser.Lemma_declarationContext ctx) { + TextualJMLLemmaDecl decl = new TextualJMLLemmaDecl(mods, ctx); + finishConstruct(decl); + return null; + } + @Override public Object visitSet_statement(JmlParser.Set_statementContext ctx) { TextualJMLSetStatement inv = new TextualJMLSetStatement(mods, ctx); @@ -503,6 +510,16 @@ public Object visitSet_statement(JmlParser.Set_statementContext ctx) { return null; } + public Object visitUse_lemma_statement(JmlParser.Use_lemma_statementContext ctx) { + TextualJMLUseLemmaStatement inv = new TextualJMLUseLemmaStatement(mods, ctx); + if (!inv.isSuitableExpression()) { + // TODO make sure this is amended by a position in the sources + throw new RuntimeException("use_lemma must go with a lemma invocation."); + } + finishConstruct(inv); + return null; + } + @Override public Object visitLoop_specification(JmlParser.Loop_specificationContext ctx) { loopContract = new TextualJMLLoopSpec(mods); 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 9306427fd8e..aad148dd9aa 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 @@ -2369,6 +2369,7 @@ public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext return new SLExpression(tb.tt()); } + // TODO Is the following bit until `Object a = ...` really needed? String paramsString; List paramDecls = ctx.param_list().param_decl(); if (!paramDecls.isEmpty()) { @@ -2398,6 +2399,15 @@ public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext return termFactory.eq(apply, body); } + @Override + public SLExpression visitLemma_declaration(JmlParser.Lemma_declarationContext ctx) { + SLParameters params = visitParameters(ctx.param_list()); + SLExpression apply = lookupIdentifier(ctx.IDENT().getText(), null, params, ctx); + + SLExpression body = new SLExpression(termFactory.tb.TRUE()); + return termFactory.eq(apply, body); + } + @Override public SLExpression visitMbody_return(JmlParser.Mbody_returnContext ctx) { return accept(ctx.expression()); diff --git a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.scripts.ProofScriptCommand b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.scripts.ProofScriptCommand index 5390423b7d6..d5eef82a154 100644 --- a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.scripts.ProofScriptCommand +++ b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.scripts.ProofScriptCommand @@ -40,4 +40,5 @@ de.uka.ilkd.key.scripts.AllCommand de.uka.ilkd.key.scripts.HideCommand de.uka.ilkd.key.scripts.UnhideCommand de.uka.ilkd.key.scripts.BranchesCommand -de.uka.ilkd.key.scripts.CheatCommand \ No newline at end of file +de.uka.ilkd.key.scripts.CheatCommand +de.uka.ilkd.key.scripts.UseLemmaCommand \ No newline at end of file diff --git a/key.core/src/test/java/de/uka/ilkd/key/scripts/DocumentationGenerator.java b/key.core/src/test/java/de/uka/ilkd/key/scripts/DocumentationGenerator.java index 3249ade318f..016b9519a68 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/scripts/DocumentationGenerator.java +++ b/key.core/src/test/java/de/uka/ilkd/key/scripts/DocumentationGenerator.java @@ -8,6 +8,21 @@ import de.uka.ilkd.key.util.KeYResourceManager; +/** + * Generates the Markdown documentation page for all registered KeY proof script commands. + *

+ * The output is written to {@code System.out} and is intended to be committed to the + * {@code key-docs} repository. + *

+ * Usage: + *

    + *
  • Without arguments: prints Markdown to standard output.
    • + *
  • With one argument: redirects output to the given file path.
    • + *
+ * To update the documentation in {@code key-docs}, run this generator and redirect/write the + * result to the target Markdown file in that repository. This is + * `key-docs/docs/user/ProofScripts/commands.md`. + */ public class DocumentationGenerator { private static String branch; @@ -79,6 +94,11 @@ private static void printHeader() { There *named* and *positional* arguments. Named arguments need to be prefixed by their name and a colon. Positional arguments are given in the order defined by the command. Optional arguments are enclosed in square brackets. + + !!! note "Document generation" + + This document is generated by the class `DocumentGenerator`. Look for that in the sources + to find out how to produce a new revision of this document. """, new Date(), branch, version, sha1); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java index c165b32c3a8..eaea6d167e1 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java @@ -3,9 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.speclang.jml; -import de.uka.ilkd.key.speclang.jml.pretranslation.Behavior; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct; -import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSpecCase; +import de.uka.ilkd.key.speclang.jml.pretranslation.*; import de.uka.ilkd.key.speclang.njml.*; import org.key_project.util.collection.ImmutableList; @@ -15,6 +13,7 @@ import org.junit.jupiter.api.Test; import static de.uka.ilkd.key.speclang.njml.JmlLexer.*; +import static org.assertj.core.api.Assertions.assertThat; import static org.junit.jupiter.api.Assertions.*; @@ -269,4 +268,27 @@ public void testFailure2() { @ requires (;((;;);();();(();;;(;))); @*/""")); } + + @Test + public void testLemmaDefinition() { + ImmutableList constructs = parseMethodSpec(""" + /*@ requires n >= 2; + @ ensures 3*n*n >= 7; + @ static lemma someLemma(int n) \\by { + @ assert n >= 3 ==> 3*(n-1)*(n-1) >= 7 \\by { use_lemma someLemma(n-1); auto; } + @ auto; + @ }; + @*/"""); + + assertThat(constructs.get(0)).isInstanceOf(TextualJMLSpecCase.class); + TextualJMLSpecCase contract = (TextualJMLSpecCase) constructs.get(0); + assertThat(contract.getClauses()).hasSize(2); + + assertThat(constructs.get(1)).isInstanceOf(TextualJMLLemmaDecl.class); + TextualJMLLemmaDecl lemma = (TextualJMLLemmaDecl) constructs.get(1); + assertThat(lemma.getMethodName()).isEqualTo("someLemma"); + assertThat(lemma.getStateCount()).isEqualTo(1); + assertThat(lemma.getModifiers()).contains(JMLModifier.MODEL); + assertThat(lemma.getModifiers()).contains(JMLModifier.STATIC); + } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java index 885dfd5f2df..7cc6e1d78e1 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java @@ -9,6 +9,7 @@ import java.util.stream.Stream; import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl; +import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodOrLemmaDecl; import org.antlr.v4.runtime.CommonTokenStream; import org.junit.jupiter.api.DynamicTest; @@ -87,7 +88,7 @@ model nullable Object foo(nullable Nullable n) { assertTrue(translationOpt.isPresent(), "No model method declaration found"); final var methodDecl = - ((TextualJMLMethodDecl) translationOpt.get()).getParsableDeclaration(); + ((TextualJMLMethodOrLemmaDecl) translationOpt.get()).getParsableDeclaration(); assertTrue(methodDecl.contains("/*@ nullable @*/ Object"), "Return value is not nullable"); assertTrue(methodDecl.contains("/*@ nullable @*/ Nullable n"), "Parameter is not nullable"); } @@ -136,7 +137,7 @@ model non_null Object foo(non_null Nullable n) { assertTrue(translationOpt.isPresent(), "No model method declaration found"); final var methodDecl = - ((TextualJMLMethodDecl) translationOpt.get()).getParsableDeclaration(); + ((TextualJMLMethodOrLemmaDecl) translationOpt.get()).getParsableDeclaration(); assertTrue(methodDecl.contains("/*@ non_null @*/ Object"), "Return value is not non_null"); assertTrue(methodDecl.contains("/*@ non_null @*/ Nullable n"), "Parameter is not non_null"); diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalUseLemma.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalUseLemma.java new file mode 100644 index 00000000000..769bafef86b --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalUseLemma.java @@ -0,0 +1,21 @@ +// exceptionClass: SLTranslationException +// msgContains: Invalid lemma call for use_lemma statement (only lemma invocations allowed) +// position: 19/23 +// verbose: true +// broken: false + +/* If there is no error message, this would close illegally. */ + +class IllegalUseLemma { + /*@ model boolean fakeLemma() { + @ return false; + @ } + @*/ + + boolean anything; + + /*@ ensures anything; */ + void m() { + //@ use_lemma fakeLemma(); + } +} diff --git a/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java b/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java new file mode 100644 index 00000000000..e86e3b613ed --- /dev/null +++ b/key.ui/examples/heap/verifyThis25_01_minExcludant/MinExcludant.java @@ -0,0 +1,73 @@ + +// TODO: Add a .key file that runs auto; and then z3 on all remaining open goals. + +class MinExcludant0 { + + /*@ requires (\forall int n; 0 <= n < s.length; (\exists int m; 0 <= m < s.length; (\bigint)s[m] == n)); + @ ensures (\forall int k; 0 <= k < s.length; (\bigint)s[k] < s.length); + @ // measured_by s.length; + @ static no_state lemma nospace(\seq s) \by { + @ oss; macro "nosplit-prop"; + @ obtain \bigint N \from_goal; + @ cut s.length == 0 \by { + @ case "true": + @ auto; // the base case is simple and obvious + @ case "false": + @ obtain \bigint sm \such_that (\bigint)s[sm] == s.length - 1 && 0 <= sm < s.length \by { + @ oss; macro "nosplit-prop"; + @ inst var:"n" with:s.length-1; + @ auto; + @ } + @ obtain \seq t = s[0 .. sm] + s[sm+1 .. s.length]; + @ use_lemma nospace(t); + @ assert (\forall int n; 0 <= n < t.length; (\exists int m; 0<=m sm && (\bigint)t[m1-1] == n1 \by auto; + @ macro "nosplit-prop"; + @ inst var: "m" with: m1-1; + @ auto; + @ } + @ cut N <= sm \by { + @ case "true": // the easy case: up to the split point + @ auto; + @ case "false": // tricky bit if behind the element that was removed. + @ oss; + @ inst var: "k" with: N-1; + @ auto; + @ } + @ } + @ }; + @*/ + + /*@ normal_behaviour + @ ensures (\forall int k; 0 <= k < a.length; a[k] != \result); + @ ensures (\forall int u; 0 <= u < \result; (\exists int j; 0 <= j < a.length; a[j] == u)); + @ assignable \strictly_nothing; + @*/ + static int mex0(int[] a) { + int n = a.length; + + /*@ maintaining 0 <= v <= n; + @ maintaining (\forall int u; 0 <= u < v; (\exists int j; 0 <= j < a.length; a[j] == u)); + @ decreases n - v; + @ assignable \strictly_nothing; + @*/ + for (int v = 0; v < n; v++) { + int i = 0; + /*@ maintaining 0 <= i <= n; + @ maintaining (\forall int k; 0 <= k < i; a[k] != v); + @ decreases n - i; + @ assignable \strictly_nothing; + @*/ + while (i < n && a[i] != v) + i++; + + if (i == n) + return v; + + } + //@ use_lemma nospace(\array2seq(a)); + return n; + } +} diff --git a/key.ui/examples/heap/verifyThis25_01_minExcludant/verifyThis2025-Challenge-1.pdf b/key.ui/examples/heap/verifyThis25_01_minExcludant/verifyThis2025-Challenge-1.pdf new file mode 100644 index 00000000000..0f05242d297 Binary files /dev/null and b/key.ui/examples/heap/verifyThis25_01_minExcludant/verifyThis2025-Challenge-1.pdf differ diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java index 5f7c68a5218..b0e84b86783 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java @@ -76,6 +76,21 @@ public ImmutableArray(@NonNull Collection list) { content = (S[]) list.toArray(); } + /** + *

+ * creates a new immutable array with the contents of the given list. + *

+ *

+ * The order of elements is defined by the collection. + *

+ * + * @param list a non-null collection (order is preserved) + */ + @SuppressWarnings("unchecked") + public ImmutableArray(@NonNull ImmutableList list) { + content = (S[]) list.toArray(Object.class); + } + /** * gets the element at the specified position * @@ -211,11 +226,7 @@ public void remove() { * @return This element converted to an {@link ImmutableList}. */ public ImmutableList toImmutableList() { - ImmutableList ret = ImmutableList.nil(); - for (S s : this) { - ret = ret.prepend(s); - } - return ret.reverse(); + return ImmutableList.fromArray(content); } /**