Extract Taclets and Prover Main Loop to ncore (#3578)

Author: Drodt

.gitignore

@@ -70,3 +70,6 @@ key.core/src/main/antlr4/gen/
 
 scripts/tools/checkstyle/key_checks_incremental.xml
 checkstyle-diff.txt
+/key.ncore/src/main/gen/
+/key.ncore/src/main/antlr/KeYLexer.tokens
+/keyext.rusty/src/main/gen/

gradle/wrapper/gradle-wrapper.jar

@@ -14,21 +14,21 @@
 import de.uka.ilkd.key.java.reference.MethodReference;
 import de.uka.ilkd.key.java.reference.TypeRef;
 import de.uka.ilkd.key.logic.JavaBlock;
-import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
-import de.uka.ilkd.key.logic.op.SchemaVariable;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.NodeInfo;
 import de.uka.ilkd.key.proof_references.ProofReferenceUtil;
 import de.uka.ilkd.key.proof_references.reference.DefaultProofReference;
 import de.uka.ilkd.key.proof_references.reference.IProofReference;
 import de.uka.ilkd.key.rule.PosTacletApp;
-import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSLList;
 

gradlew

@@ -62,8 +62,7 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
      */
     protected void listReferences(Node node, ProgramElement pe, ProgramVariable arrayLength,
             LinkedHashSet<IProofReference<?>> toFill, boolean includeExpressionContainer) {
-        if (pe instanceof ProgramVariable) {
-            ProgramVariable pv = (ProgramVariable) pe;
+        if (pe instanceof ProgramVariable pv) {
             if (pv.isMember()) {
                 DefaultProofReference<ProgramVariable> reference =
                     new DefaultProofReference<>(IProofReference.ACCESS, node,

gradlew.bat

@@ -10,7 +10,6 @@
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.util.KeYTypeUtil;
 
-import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.Test;
 
 import static org.junit.jupiter.api.Assertions.*;
@@ -54,9 +53,9 @@ public void testIsInnerType() throws Exception {
             // Test class with package
             assertFalse(KeYTypeUtil.isInnerType(services, typeWithPackage));
             // Test inner class without package
-            Assertions.assertTrue(KeYTypeUtil.isInnerType(services, innerTypeWithoutPackage));
+            assertTrue(KeYTypeUtil.isInnerType(services, innerTypeWithoutPackage));
             // Test inner class with package
-            Assertions.assertTrue(KeYTypeUtil.isInnerType(services, innerTypeWithPackage));
+            assertTrue(KeYTypeUtil.isInnerType(services, innerTypeWithPackage));
         } finally {
             environment.dispose();
         }
@@ -87,11 +86,11 @@ public void testGetParentName() throws Exception {
                 KeYTypeUtil.getType(services, "model.InnerAndAnonymousTypeTest.IGetter");
             assertNotNull(innerTypeWithPackage);
             // Test null
-            Assertions.assertNull(KeYTypeUtil.getParentName(services, null));
-            Assertions.assertNull(KeYTypeUtil.getParentName(null, typeWithoutPackage));
-            Assertions.assertNull(KeYTypeUtil.getParentName(null, null));
+            assertNull(KeYTypeUtil.getParentName(services, null));
+            assertNull(KeYTypeUtil.getParentName(null, typeWithoutPackage));
+            assertNull(KeYTypeUtil.getParentName(null, null));
             // Test class without package
-            Assertions.assertNull(KeYTypeUtil.getParentName(services, typeWithoutPackage));
+            assertNull(KeYTypeUtil.getParentName(services, typeWithoutPackage));
             // Test class with package
             assertEquals("model", KeYTypeUtil.getParentName(services, typeWithPackage));
             // Test inner class without package
@@ -127,14 +126,13 @@ public void testIsType() throws Exception {
             assertFalse(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest.Invalid"));
             assertFalse(KeYTypeUtil.isType(services, "model.InnerAndAnonymousTypeTest.Invalid"));
             // Test class without package
-            Assertions.assertTrue(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest"));
+            assertTrue(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest"));
             // Test class with package
-            Assertions.assertTrue(KeYTypeUtil.isType(services, "model.InnerAndAnonymousTypeTest"));
+            assertTrue(KeYTypeUtil.isType(services, "model.InnerAndAnonymousTypeTest"));
             // Test inner class without package
-            Assertions
-                    .assertTrue(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest.IGetter"));
+            assertTrue(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest.IGetter"));
             // Test inner class with package
-            Assertions.assertTrue(
+            assertTrue(
                 KeYTypeUtil.isType(services, "model.InnerAndAnonymousTypeTest.IGetter"));
         } finally {
             environment.dispose();
@@ -153,16 +151,15 @@ public void testGetType() throws Exception {
             Services services = environment.getServices();
             assertNotNull(services);
             // Test null
-            Assertions.assertNull(KeYTypeUtil.getType(services, null));
-            Assertions.assertNull(KeYTypeUtil.getType(null, "InnerAndAnonymousTypeTest"));
-            Assertions.assertNull(KeYTypeUtil.getType(null, null));
+            assertNull(KeYTypeUtil.getType(services, null));
+            assertNull(KeYTypeUtil.getType(null, "InnerAndAnonymousTypeTest"));
+            assertNull(KeYTypeUtil.getType(null, null));
             // Test invalid names
-            Assertions.assertNull(KeYTypeUtil.getType(services, "Invalid"));
-            Assertions.assertNull(KeYTypeUtil.getType(services, "model.Invalid"));
-            Assertions.assertNull(KeYTypeUtil.getType(services, "invalid.Invalid"));
-            Assertions
-                    .assertNull(KeYTypeUtil.getType(services, "InnerAndAnonymousTypeTest.Invalid"));
-            Assertions.assertNull(
+            assertNull(KeYTypeUtil.getType(services, "Invalid"));
+            assertNull(KeYTypeUtil.getType(services, "model.Invalid"));
+            assertNull(KeYTypeUtil.getType(services, "invalid.Invalid"));
+            assertNull(KeYTypeUtil.getType(services, "InnerAndAnonymousTypeTest.Invalid"));
+            assertNull(
                 KeYTypeUtil.getType(services, "model.InnerAndAnonymousTypeTest.Invalid"));
             // Test class without package
             KeYJavaType kjt = KeYTypeUtil.getType(services, "InnerAndAnonymousTypeTest");

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java

@@ -39,7 +39,7 @@ public void testReferenceComputation_ExpandAndContract() throws Exception {
             new ExpectedProofReferences(IProofReference.INLINE_METHOD,
                 "UseOperationContractTest::main"),
             new ExpectedProofReferences(IProofReference.USE_CONTRACT,
-                "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result_magic42,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}; mods: {heap=allLocs, savedHeap=null}; hasMod: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
+                "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result_magic42,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}free post: {heap=true, savedHeap=null}; modifiable: {heap=allLocs, savedHeap=null}; hasModifiable: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
     }
 
     /**

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java

@@ -24,6 +24,6 @@ public void testUseOperationContracts() throws Exception {
             "/proofReferences/UseOperationContractTest/UseOperationContractTest.java",
             "UseOperationContractTest", "main", true, new ContractProofReferencesAnalyst(),
             new ExpectedProofReferences(IProofReference.USE_CONTRACT,
-                "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result_magic42,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}; mods: {heap=allLocs, savedHeap=null}; hasMod: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
+                "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result_magic42,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}free post: {heap=true, savedHeap=null}; modifiable: {heap=allLocs, savedHeap=null}; hasModifiable: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
     }
 }

key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestKeYTypeUtil.java

@@ -65,7 +65,7 @@ public static void main(String[] args) {
         } else {
             final File riflFilename = new File(args[0]);
             final File javaFilename = new File(args[1]);
-            RIFLTransformer.transform(riflFilename, javaFilename);
+            transform(riflFilename, javaFilename);
         }
     }