Proof Scripts in JML

.github/workflows/tests.yml

@@ -71,9 +71,6 @@ jobs:
             **/build/reports/
             !**/jacocoTestReport.xml
 
-      - name: Upload coverage reports to Codecov
-        uses: codecov/codecov-action@v6
-
   integration-tests:
     env:
       GH_TOKEN: ${{ github.token }}

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java

@@ -117,7 +117,7 @@ public Strategy<Goal> create(Proof proof, StrategyProperties sp) {
          */
         @Override
         public StrategySettingsDefinition getSettingsDefinition() {
-            return JavaProfile.DEFAULT.getSettingsDefinition();
+            return JavaProfile.getDefault().getSettingsDefinition();
         }
     }
 }

key.core/build.gradle

@@ -16,6 +16,10 @@ dependencies {
 
     api project(':key.util')
 
+    // Make Javadoc accessible at runtime
+    annotationProcessor 'com.github.therapi:therapi-runtime-javadoc-scribe:0.13.0'
+    implementation 'com.github.therapi:therapi-runtime-javadoc:0.13.0'
+
     def JP_VERSION = "3.28.0-K13.5"
     api "org.key-project.proofjava:javaparser-core:$JP_VERSION"
     api "org.key-project.proofjava:javaparser-core-serialization:$JP_VERSION"
@@ -31,6 +35,10 @@ dependencies {
     testFixturesApi(testFixtures(project(":key.util")))
 }
 
+tasks.withType(JavaCompile) {
+    options.compilerArgs << "-Ajavadoc.packages=de.uka.ilkd.key.scripts"
+}
+
 // The target directory for JavaCC (parser generation)
 //def javaCCOutputDir = layout.buildDirectory.dir("generated-src/javacc").getOrNull()
 //def javaCCOutputDirMain = file("$javaCCOutputDir/main")
@@ -97,6 +105,7 @@ classes.dependsOn << generateSolverPropsList
 
 tasks.withType(Test) {
     enableAssertions = true
+    systemProperties(System.properties.findAll { key, value -> key.startsWith("key.") })
 }
 
 

key.core/src/main/antlr4/JmlLexer.g4

@@ -175,6 +175,8 @@ mode expr;
 /* Java keywords */
 BOOLEAN: 'boolean';
 BYTE: 'byte';
+CASE: 'case';
+DEFAULT: 'default';
 FALSE: 'false';
 INSTANCEOF: 'instanceof';
 INT: 'int';
@@ -244,6 +246,7 @@ FP_SUBNORMAL: '\\fp_subnormal';   //KeY extension, not official JML
 FP_ZERO: '\\fp_zero';   //KeY extension, not official JML
 FREE: '\\free';  //KeY extension, not official JML
 FRESH: '\\fresh';
+FROM_GOAL: '\\from_goal';  //KeY extension, not official JML
 INDEX: '\\index';
 INDEXOF: '\\seq_indexOf';  //KeY extension, not official JML
 INTERSECT: '\\intersect';  //KeY extension, not official JML

key.core/src/main/antlr4/JmlParser.g4

@@ -9,6 +9,9 @@ options { tokenVocab=JmlLexer; }
 @members {
   private SyntaxErrorReporter errorReporter = new SyntaxErrorReporter(getClass());
   public SyntaxErrorReporter getErrorReporter() { return errorReporter;}
+  private boolean isNextToken(String tokenText) {
+    return _input.LA(1) != Token.EOF && tokenText.equals(_input.LT(1).getText());
+  }
 }
 
 modifiersEOF: modifiers EOF;
@@ -203,12 +206,35 @@ block_specification: method_specification;
 block_loop_specification:
   loop_contract_keyword spec_case ((also_keyword)+ loop_contract_keyword spec_case)*;
 loop_contract_keyword: LOOP_CONTRACT;
-assert_statement: (ASSERT expression | UNREACHABLE) SEMI_TOPLEVEL;
+assert_statement: (ASSERT (label=IDENT COLON)? expression | UNREACHABLE) (assertionProof SEMI_TOPLEVEL? | SEMI_TOPLEVEL);
 //breaks_clause: BREAKS expression;
 //continues_clause: CONTINUES expression;
 //returns_clause: RETURNS expression;
 
 
+// --- proof scripts in JML
+assertionProof: BY (proofCmd | LBRACE ( proofCmd )+ RBRACE) ;
+proofCmd:
+    // TODO allow more than one var in obtain
+  { isNextToken("obtain") }? obtain=IDENT typespec var=IDENT
+       ( obtKind=EQUAL_SINGLE expression SEMI
+       | obtKind=SUCH_THAT expression proofCmdSuffix
+       | obtKind=FROM_GOAL SEMI
+       )
+  | cmd=IDENT ( proofArg )* proofCmdSuffix
+  ;
+
+proofCmdSuffix:
+  SEMI | BY ( proofCmd | LBRACE (proofCmd+ | proofCmdCase+) RBRACE )
+  ;
+
+proofCmdCase:
+    CASE ( label=STRING_LITERAL )? COLON ( proofCmd )*
+  | DEFAULT COLON ( proofCmd )*
+  ;
+proofArg: (argLabel=IDENT COLON)? expression;
+// ---
+
 mergeparamsspec:
     MERGE_PARAMS
       LBRACE

key.core/src/main/antlr4/KeYLexer.g4

@@ -40,6 +40,7 @@ lexer grammar KeYLexer;
    }
 
     private Token tokenBackStorage = null;
+    // see: https://keyproject.github.io/key-docs/devel/NewKeyParser/#why-does-the-lexer-required-some-pieces-of-java-code
     @Override
     public void emit(Token token) {
        int MAX_K = 10;
@@ -220,6 +221,7 @@ AXIOMS : '\\axioms';
 PROBLEM : '\\problem';
 CHOOSECONTRACT : '\\chooseContract';
 PROOFOBLIGATION : '\\proofObligation';
+// for PROOF see: https://keyproject.github.io/key-docs/devel/NewKeyParser/#why-does-the-lexer-required-some-pieces-of-java-code
 PROOF : '\\proof';
 PROOFSCRIPT : '\\proofScript';
 CONTRACTS : '\\contracts';
@@ -428,7 +430,7 @@ fragment HEX
 fragment LETTER:	'a'..'z'|'A'..'Z';
 fragment IDCHAR: LETTER | DIGIT | '_' | '#' | '$';
 
-
+MATCH_IDENT: '?' IDENT?;
 IDENT:  ( (LETTER | '_' | '#' | '$') (IDCHAR)*);
 
 INT_LITERAL:

key.core/src/main/antlr4/KeYParser.g4

@@ -7,6 +7,7 @@ parser grammar KeYParser;
 @members {
 private SyntaxErrorReporter errorReporter = new SyntaxErrorReporter(getClass());
 public SyntaxErrorReporter getErrorReporter() { return errorReporter;}
+public boolean allowMatchId = false; // used in proof script parsing
 }
 
 options { tokenVocab=KeYLexer; } // use tokens from STLexer.g4
@@ -154,6 +155,7 @@ string_value: STRING_LITERAL;
 simple_ident
 :
     id=IDENT
+  | {allowMatchId}? id=MATCH_IDENT
 ;
 
 simple_ident_comma_list
@@ -901,7 +903,7 @@ proofScriptExpression:
   | integer
   | floatnum
   | string_literal
-  | LPAREN (term | seq) RPAREN
+  | LPAREN {allowMatchId=true;} (term | seq) {allowMatchId=false;} RPAREN
   | simple_ident
   | abbreviation
   | literals

key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java

@@ -394,7 +394,7 @@ public static boolean isVisibleTo(SpecificationElement ax, KeYJavaType visibleTo
     /**
      * returns a KeYJavaType having the given sort
      */
-    public KeYJavaType getKeYJavaType(Sort sort) {
+    public @Nullable KeYJavaType getKeYJavaType(Sort sort) {
         List<KeYJavaType> l = lookupSort2KJTCache(sort);
         if (l != null && l.size() > 0) {
             // Return first KeYJavaType found for sort.

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java

@@ -8,10 +8,17 @@
 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.logic.op.LocationVariable;
 import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatement;
+import de.uka.ilkd.key.speclang.njml.JmlIO;
+import de.uka.ilkd.key.speclang.njml.JmlParser;
 
 import org.key_project.util.ExtList;
+import org.key_project.util.collection.ImmutableList;
+
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
 
 /**
  * A JML assert statement.
@@ -29,24 +36,36 @@ public class JmlAssert extends JavaStatement {
      */
     private final TextualJMLAssertStatement.Kind kind;
 
+    /*
+     * Temporary solution until full jml labels are there ...
+     * (To be clarified if compatible still)
+     */
+    private final String optLabel;
+
     /**
      * the condition in parse tree form
      */
-    private KeyAst.Expression condition;
+    private final KeyAst.Expression condition;
+
+    /**
+     * the assertion proof in parse tree form
+     */
+    private final KeyAst.@Nullable JMLProofScript assertionProof;
 
     /**
-     * @param kind
-     *        assert or assume
-     * @param condition
-     *        the condition of this statement
-     * @param positionInfo
-     *        the position information for this statement
+     * @param kind assert or assume
+     * @param condition the condition of this statement
+     * @param assertionProof the optional proof for an assert statement (not for assume)
+     * @param positionInfo the position information for this statement
      */
-    public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression condition,
+    public JmlAssert(TextualJMLAssertStatement.Kind kind, String label, KeyAst.Expression condition,
+            KeyAst.@Nullable JMLProofScript assertionProof,
             PositionInfo positionInfo) {
         super(positionInfo);
         this.kind = kind;
+        this.optLabel = label;
         this.condition = condition;
+        this.assertionProof = assertionProof;
     }
 
     /**
@@ -56,11 +75,25 @@ public JmlAssert(TextualJMLAssertStatement.Kind kind, KeyAst.Expression conditio
     public JmlAssert(ExtList children) {
         super(children);
         this.kind = Objects.requireNonNull(children.get(TextualJMLAssertStatement.Kind.class));
+        this.optLabel = children.get(String.class);
         this.condition = Objects.requireNonNull(children.get(KeyAst.Expression.class));
+        // script may be null
+        this.assertionProof = children.get(KeyAst.JMLProofScript.class);
     }
 
     public JmlAssert(JmlAssert other) {
-        this(other.kind, other.condition, other.getPositionInfo());
+        this(other.kind, other.optLabel, other.condition, other.assertionProof,
+            other.getPositionInfo());
+    }
+
+    public JmlAssert(TextualJMLAssertStatement.Kind kind, TextualJMLAssertStatement construct,
+            PositionInfo pi) {
+        super(pi);
+        this.kind = kind;
+        this.optLabel = construct.getOptLabel();
+        this.condition = construct.getContext();
+        // script may be null
+        this.assertionProof = construct.getAssertionProof();
     }
 
     public TextualJMLAssertStatement.Kind getKind() {
@@ -152,6 +185,10 @@ protected int computeHashCode() {
         return System.identityHashCode(this);
     }
 
+    public KeyAst.@Nullable JMLProofScript getAssertionProof() {
+        return assertionProof;
+    }
+
     @Override
     public int getChildCount() {
         return 0;
@@ -166,4 +203,30 @@ public ProgramElement getChildAt(int index) {
     public void visit(Visitor v) {
         v.performActionOnJmlAssert(this);
     }
+
+    /**
+     * This method collects all terms contained in this assertion. This is at least the condition.
+     * If there is a proof script, all terms in the proof script are collected as well.
+     *
+     * @return a freshly created list of at least one term
+     */
+    public @NonNull ImmutableList<JmlParser.ExpressionContext> collectTerms() {
+        ImmutableList<JmlParser.ExpressionContext> result = ImmutableList.of();
+        if (assertionProof != null) {
+            result = result.prepend(assertionProof.collectTerms());
+        }
+        result = result.prepend(condition.ctx);
+        return result;
+    }
+
+    public ImmutableList<LocationVariable> collectVariablesInProof(JmlIO io) {
+        if (assertionProof != null) {
+            return assertionProof.getObtainedProgramVars(io);
+        }
+        return ImmutableList.of();
+    }
+
+    public String getOptLabel() {
+        return optLabel;
+    }
 }