Modularize KeY Grammar

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java

@@ -274,7 +274,7 @@ private Taclet genInfFlowContractApplTaclet(Goal goal, ProofObligationVars appDa
         tacletBuilder.setFind(schemaFind);
         tacletBuilder.setApplicationRestriction(
             new ApplicationRestriction(ApplicationRestriction.ANTECEDENT_POLARITY));
-        tacletBuilder.setIfSequent(assumesSeq);
+        tacletBuilder.setAssumesSequent(assumesSeq);
         RewriteTacletGoalTemplate goalTemplate = new RewriteTacletGoalTemplate(replaceWithSeq,
             ImmutableSLList.nil(), schemaFind);
         tacletBuilder.addTacletGoalTemplate(goalTemplate);
@@ -311,7 +311,7 @@ public InfFlowContractAppTaclet getRewriteTaclet() {
             TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(this);
             prefixBuilder.build();
             return new InfFlowContractAppTaclet(name,
-                new TacletApplPart(ifseq, applicationRestriction, varsNew, varsNotFreeIn,
+                new TacletApplPart(assumesSeq, applicationRestriction, varsNew, varsNotFreeIn,
                     varsNewDependingOn,
                     variableConditions),
                 goals, ruleSets, attrs, (JTerm) find, prefixBuilder.getPrefixMap(),

key.core.testgen/testcases/arrayutil/actual/build.gradle.kts

@@ -0,0 +1,23 @@
+package de.uka.ilkd.key.tcg
+
+plugins {
+    java
+}
+
+repositories {
+    mavenCentral()
+}
+
+dependencies {
+    testImplementation(platform("org.junit:junit-bom:5.13.2"))
+    testImplementation("org.junit.jupiter:junit-jupiter-api")
+    testRuntimeOnly("org.junit.jupiter:junit-jupiter-engine")
+    testRuntimeOnly("org.junit.platform:junit-platform-launcher")
+
+    testImplementation("org.objenesis:objenesis:3.3")
+    testImplementation("org.hamcrest:hamcrest-core:2.2")
+}
+
+tasks.withType<Test> {
+    useJUnitPlatform()
+}

key.core.testgen/testcases/arrayutil/actual/build.xml

@@ -0,0 +1,65 @@
+<project name="MyProject" default="run" basedir=".">
+	<description>
+		simple example build file
+	</description>
+	<!-- set global properties for this build -->
+	<property name="src" location="src"/>
+	<property name="test" location="test"/>
+	<property name="build" location="build"/>
+	<property name="lib" location="lib"/>
+	<property name="dist" location="dist"/>
+
+	<target name="init">
+		<!-- Create the time stamp -->
+		<tstamp/>
+		<!-- Create the build directory structure used by compile -->
+		<mkdir dir="${build}"/>
+
+		<get dest="${lib}" retries="5" skipexisting="true">
+			<url url="https://repo1.maven.org/maven2/org/objenesis/objenesis/3.3/objenesis-3.3.jar"/>
+			<url url="https://repo1.maven.org/maven2/junit/junit/4.13.2/junit-4.13.2.jar"/>
+			<url url="https://repo1.maven.org/maven2/org/hamcrest/hamcrest/2.2/hamcrest-2.2.jar"/>
+		</get>
+	</target>
+
+	<target name="compile" depends="init"
+	        description="compile the source">
+		<!-- Compile the Java code from ${src} into ${build} -->
+		<javac srcdir="${src}" destdir="${build}">
+			<src path="${src}"/>
+			<src path="${test}"/>
+
+			<classpath>
+				<pathelement location="${build}"/>
+				<pathelement path="lib/junit-4.13.2.jar"/>
+				<pathelement path="lib/objenesis-3.3.jar"/>
+				<pathelement path="lib/hamcrest-2.2.jar"/>
+			</classpath>
+		</javac>
+	</target>
+
+	<target name="run" depends="compile">
+		<junit>
+			<classpath>
+				<pathelement location="${build}"/>
+				<pathelement path="lib/junit-4.13.2.jar"/>
+				<pathelement path="lib/objenesis-3.3.jar"/>
+				<pathelement path="lib/hamcrest-2.2.jar"/>
+			</classpath>
+			<batchtest>
+				<fileset dir="${test}">
+					<include name="**/**"/>
+				</fileset>
+			</batchtest>
+			<formatter type="brief" usefile="false"/>
+		</junit>
+
+	</target>
+
+	<target name="clean"
+	        description="clean up">
+		<!-- Delete the ${build} and ${dist} directory trees -->
+		<delete dir="${build}"/>
+		<delete dir="${dist}"/>
+	</target>
+</project>

key.core.testgen/testcases/arrayutil/actual/pom.xml

@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="utf-8" ?>
+<project xmlns="http://maven.apache.org/POM/4.0.0">
+	<modelVersion>4.0.0</modelVersion>
+	<groupId>generated</groupId>
+	<artifactId>generated</artifactId>
+	<version>1.0.0-SNAPSHOT</version>
+	<packaging>jar</packaging>
+
+	<dependencies>
+		<dependency>
+			<groupId>org.junit.jupiter</groupId>
+			<artifactId>junit-jupiter-api</artifactId>
+			<version>5.11.3</version>
+			<scope>test</scope>
+		</dependency>
+		<dependency>
+			<groupId>org.objenesis</groupId>
+			<artifactId>objenesis</artifactId>
+			<version>3.3</version>
+			<scope>test</scope>
+		</dependency>
+		<dependency>
+			<groupId>org.hamcrest</groupId>
+			<artifactId>hamcrest-core</artifactId>
+			<version>2.2</version>
+			<scope>test</scope>
+		</dependency>
+	</dependencies>
+</project>

key.core.testgen/testcases/arrayutil/actual/src/main/java/ArrayUtils.java

@@ -0,0 +1,14 @@
+/** From the second KeY book.
+ * https://link.springer.com/chapter/10.1007/978-3-319-49812-6_12
+ * Listing 12.1
+ */
+public class ArrayUtils {
+    /*@ public normal_behavior
+      @ ensures (\forall int i; 0<=i && i<a.length; a[i]==b[i]);
+      @*/
+    public void arrCopy(int[] a, int[] b) {
+        for (int i = 0; i < a.length; i++) {
+            b[i] = a[i];
+        }
+    }
+}

key.core.testgen/testcases/arrayutil/actual/src/test/java/TestGeneric0.java

@@ -0,0 +1,39 @@
+// This is a test driver generated by KeY "3.0.0-dev (internal: 526b15139d2bd41fc3f7954a98f54ca90c057d3c)" (www.key-project.org).
+// "TestGeneric0.java"
+// @author Christoph Gladisch
+// @author Mihai Herda
+//
+import java.lang.Boolean;
+import java.lang.Object;
+import java.lang.String;
+import java.util.Map;
+import java.util.Set;
+
+class TestGeneric0 {
+  public static final void main(String[] args) {
+  }
+
+  boolean testOracle(java.lang.Throwable exc, java.lang.Throwable _preexc, int[] a, int[] _prea,
+      ArrayUtils self, ArrayUtils _preself, int[] b, int[] _preb, Set<Boolean> allBools,
+      Set<Integer> allInts, Set<java.lang.Object> allObjects, Map<Object, Object> old) {
+    return ((sub1(exc, _preexc, a, _prea, self, _preself, b, _preb, allBools, allInts, allObjects, old) && inv_javalangObject(self, exc, _preexc, a, _prea, self, _preself, b, _preb, allBools, allInts, allObjects, old)) && (exc == null));
+  }
+
+  boolean inv_javalangObject(java.lang.Object o, java.lang.Throwable exc,
+      java.lang.Throwable _preexc, int[] a, int[] _prea, ArrayUtils self, ArrayUtils _preself,
+      int[] b, int[] _preb, Set<Boolean> allBools, Set<Integer> allInts,
+      Set<java.lang.Object> allObjects, Map<Object, Object> old) {
+    return true;
+  }
+
+  boolean sub1(java.lang.Throwable exc, java.lang.Throwable _preexc, int[] a, int[] _prea,
+      ArrayUtils self, ArrayUtils _preself, int[] b, int[] _preb, Set<Boolean> allBools,
+      Set<Integer> allInts, Set<java.lang.Object> allObjects, Map<Object, Object> old) {
+    for(int i : allInts) {
+      if(!(!((0 <= i) && (i < a.length)) || (a[i] == b[i]))) {
+        return false;
+      }
+    }
+    return true;
+  }
+}

key.core/build.gradle

@@ -170,14 +170,15 @@ processResources.dependsOn generateVersionFiles, generateSolverPropsList, genera
 def antlr4OutputKey = "$projectDir/build/generated-src/antlr4/main/de/uka/ilkd/key/nparser"
 tasks.register('runAntlr4Key', JavaExec) {
     //see incremental task api, prevents rerun if nothing has changed.
-    inputs.files "src/main/antlr4/KeYLexer.g4", "src/main/antlr4/KeYParser.g4"
+    inputs.files "src/main/antlr4/JavaKeYLexer.g4", "src/main/antlr4/JavaKeYParser.g4"
     outputs.dir antlr4OutputKey
     classpath = configurations.antlr4
     mainClass.set("org.antlr.v4.Tool")
     args = ["-visitor",
+            "-lib", "../key.ncore/src/main/antlr/",
             "-Xexact-output-dir", "-o", antlr4OutputKey,
             "-package", "de.uka.ilkd.key.nparser",
-            "src/main/antlr4/KeYLexer.g4", "src/main/antlr4/KeYParser.g4"]
+            "src/main/antlr4/JavaKeYLexer.g4", "src/main/antlr4/JavaKeYParser.g4"]
     doFirst {
         file(antlr4OutputKey).mkdirs()
         println("create $antlr4OutputKey")

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

@@ -0,0 +1,108 @@
+lexer grammar JavaKeYLexer;
+
+@header {
+}
+
+@annotateclass{ @SuppressWarnings("all") }
+
+import KeYLexer;
+
+// Keywords used in schema variable declarations
+TERMLABEL : '\\termlabel';
+
+// used in contracts
+MODIFIABLE : '\\modifiable';
+
+// Keywords used in program variable declarations
+PROGRAMVARIABLES : '\\programVariables';
+
+// Keywords for varcond and related stuff
+STORE_TERM_IN : '\\storeTermIn';
+STORE_STMT_IN : '\\storeStmtIn';
+HAS_INVARIANT : '\\hasInvariant';
+GET_INVARIANT : '\\getInvariant';
+GET_FREE_INVARIANT: '\\getFreeInvariant';
+GET_VARIANT: '\\getVariant';
+IS_LABELED: '\\isLabeled';
+
+SAME_OBSERVER : '\\sameObserver';
+DEPENDINGON : '\\dependingOn';
+DISJOINTMODULONULL  : '\\disjointModuloNull';
+DROP_EFFECTLESS_STORES : '\\dropEffectlessStores';
+ENUM_CONST : '\\enumConstant';
+FREELABELIN : '\\freeLabelIn';
+FIELDTYPE : '\\fieldType';
+FINAL : '\\final';
+ELEMSORT : '\\elemSort';
+HASLABEL : '\\hasLabel';
+HASSUBFORMULAS : '\\hasSubFormulas';
+ISARRAY:'\\isArray';
+ISARRAYLENGTH:'\\isArrayLength';
+ISCONSTANT: '\\isConstant';
+ISENUMTYPE:'\\isEnumType';
+ISINDUCTVAR:'\\isInductVar';
+ISLOCALVARIABLE : '\\isLocalVariable';
+ISOBSERVER : '\\isObserver';
+METADISJOINT : '\\metaDisjoint';
+ISTHISREFERENCE:'\\isThisReference';
+DIFFERENTFIELDS:'\\differentFields';
+ISREFERENCE:'\\isReference';
+ISREFERENCEARRAY:'\\isReferenceArray';
+ISSTATICFIELD : '\\isStaticField';
+ISMODELFIELD : '\\isModelField';
+ISINSTRICTFP : '\\isInStrictFp';
+NEW_DEPENDING_ON: '\\newDependingOn';
+NEW_LOCAL_VARS: '\\newLocalVars';
+NEWLABEL : '\\newLabel';
+CONTAINS_ASSIGNMENT : '\\containsAssignment';
+// label occurs again for character `!'
+NOTFREEIN : '\\notFreeIn';
+STATIC : '\\static';
+STATICMETHODREFERENCE : '\\staticMethodReference';
+MAXEXPANDMETHOD : '\\mayExpandMethod';
+
+// inclusion and stuff, things that (usually) come at the beginning
+// of the file
+CLASSPATH:'\\classpath';
+BOOTCLASSPATH:'\\bootclasspath';
+NODEFAULTCLASSES:'\\noDefaultClasses';
+JAVASOURCE:'\\javaSource'; // TODO: remove
+
+CHOOSECONTRACT : '\\chooseContract';
+CONTRACTS : '\\contracts';
+INVARIANTS : '\\invariants';
+
+// The first three guys are not really meta operators, treated separately
+IN_TYPE : '\\inType';
+IS_ABSTRACT_OR_INTERFACE : '\\isAbstractOrInterface';
+IS_FINAL : '\\isFinal';
+CONTAINERTYPE : '\\containerType';
+
+// types that need to be declared as keywords
+//LOCSET : '\\locset';
+//SEQ : '\\seq';
+//BIGINT : '\\bigint';
+
+/**
+  * Here we have to accept all strings of ki01           ERROR_CHAR 0:\                                                 nd \\[a-z_]
+  * and make the decision our selves as to what to do with it
+  * (i.e. is it a modality, keyword, or possibly something else)
+  */
+MODALITYBB:	'\\[[' -> more, pushMode(modBoxBox);
+
+MODAILITYGENERIC3: '\\diamond_transaction'    -> more, pushMode(modGeneric);
+MODAILITYGENERIC5: '\\box_transaction'        -> more, pushMode(modGeneric);
+MODAILITYGENERIC6: '\\throughout'             -> more, pushMode(modGeneric);
+MODAILITYGENERIC7: '\\throughout_transaction' -> more, pushMode(modGeneric);
+
+/* weigl: not working
+MODAILITYGENERIC:
+      ('\\modality' | '\\diamond' | '\\diamond_transaction'
+      '\\box' | '\\box_transaction' | '\\throughout' | '\\throughout_transaction')
+      -> more, pushMode(modGeneric);
+*/
+//BACKSLASH:  '\\';
+
+DOC_COMMENT
+   : '/*!' -> more , pushMode (docComment)
+   ;