fix test cases, adapt Java-Redux

Author: wadoon

key.core/pipelineTests/innerclass/expected/02_TryWithResourceReducer/MostSimpleInner.java

@@ -0,0 +1,5 @@
+public class MostSimpleInner {
+
+    public static class MyInnerClass {
+    }
+}

key.core/pipelineTests/records/expected/02_TryWithResourceReducer/CompactConstructor.java

@@ -0,0 +1,8 @@
+record Mapping(String from, String to) {
+
+    Mapping {
+        // compact constructor!
+        from = "abc";
+        to = "def";
+    }
+}

key.core/pipelineTests/records/expected/02_TryWithResourceReducer/InnerRecord.java

@@ -0,0 +1,7 @@
+import java.lang.Object;
+
+public class OuterClass {
+
+    final record MyRecord(String test) {
+    }
+}

key.core/pipelineTests/records/expected/02_TryWithResourceReducer/NotAllowed.java

@@ -0,0 +1,36 @@
+//https://mikemybytes.com/2022/02/16/java-records-and-compact-constructors/
+record // package-private
+Name(// package-private
+String name) {
+
+    // fails with: 'invalid canonical constructor in record Name
+    //              (attempting to assign stronger access privileges;
+    //              was package)'
+    private Name(String name) {
+        this.name = name;
+    }
+
+    static Name of(String name) {
+        return new Name(name);
+    }
+}
+
+record Point(int x, int y) {
+
+    Point(int x, int y) {
+        // boring!
+        this.x = x;
+        this.y = y;
+    }
+
+    Point(int x) {
+        // a bit weird...
+        // ... but perfectly fine for the compiler
+        this(x, 0);
+    }
+
+    Point() {
+        // fails with: 'constructor is not canonical, so its first
+        //              statement must invoke another constructor'
+    }
+}

key.core/pipelineTests/records/expected/02_TryWithResourceReducer/Point3d.java

@@ -0,0 +1,2 @@
+record Point3d(int x, int y, int z) {
+}

key.core/pipelineTests/records/expected/02_TryWithResourceReducer/RecordOverwriting.java

@@ -0,0 +1,14 @@
+record MyRecord(String test) {
+
+    public int hashCode() {
+        return 0;
+    }
+
+    public boolean equals(Object obj) {
+        return obj instanceof MyRecord;
+    }
+
+    public String test() {
+        return "";
+    }
+}

key.core/pipelineTests/records/expected/02_TryWithResourceReducer/SimpleRecord.java

@@ -0,0 +1,6 @@
+public record SimpleRecord(/*@ nullable */ String name) implements Serializable {
+
+    SimpleRecord(String name) {
+        this.name = name;
+    }
+}

key.core/pipelineTests/simple/expected/02_TryWithResourceReducer/Test.java

@@ -0,0 +1,24 @@
+public class Test {
+
+    public static int abc;
+
+    static {
+        // should be resolved to 2
+        abc = 1 + 1;
+    }
+
+    public int memberVar;
+
+    {
+        memberVar = 42;
+    }
+}
+
+public class SubClass extends Test {
+
+    public int memberVar;
+
+    {
+        memberVar = 41;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TryWithResourceReducer.java

@@ -1,5 +1,11 @@
+/* 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.transformations.pipeline;
 
+import java.util.List;
+import java.util.concurrent.atomic.AtomicInteger;
+
 import com.github.javaparser.ast.NodeList;
 import com.github.javaparser.ast.body.Parameter;
 import com.github.javaparser.ast.body.TypeDeclaration;
@@ -10,41 +16,39 @@
 import com.github.javaparser.ast.visitor.ModifierVisitor;
 import com.github.javaparser.ast.visitor.Visitable;
 
-import java.util.List;
-import java.util.concurrent.atomic.AtomicInteger;
-
 /// Rewrites every try-with-resources statement into the equivalent nested
 /// try/finally form that javac itself generates, i.e. for
 /// ```java
 /// try (Resource r = open()) {
-///     body;
+/// body;
 /// }
 /// ```
 /// this produces:
 /// ```java
 /// try {
-///     Resource r = open();
-///     Throwable primaryExc$1 = null;
-///     try {
-///         body;
-///     } catch (Throwable t$1) {
-///         primaryExc$1 = t$1;
-///         throw t$1;
-///     } finally {
-///         if (r != null) {
-///             if (primaryExc$1 != null) {
-///                 try { r.close(); } catch (Throwable suppressedExc$1) {
-///                     primaryExc$1.addSuppressed(suppressedExc$1);
-///                 }
-///             } else { r.close(); }
-///         }
-///     }
+/// Resource r = open();
+/// Throwable primaryExc$1 = null;
+/// try {
+/// body;
+/// } catch (Throwable t$1) {
+/// primaryExc$1 = t$1;
+/// throw t$1;
+/// } finally {
+/// if (r != null) {
+/// if (primaryExc$1 != null) {
+/// try { r.close(); } catch (Throwable suppressedExc$1) {
+/// primaryExc$1.addSuppressed(suppressedExc$1);
+/// }
+/// } else { r.close(); }
+/// }
+/// }
 /// }
 /// ```
 /// Multiple resources are handled by nesting (last-declared resource closes first),
 /// and any catch/finally clauses that were attached to the original try are kept
 /// on an outer try that wraps the whole resource-management block, exactly as
 /// javac does it.
+///
 /// @author weigl, Claude Sonnet
 public class TryWithResourceReducer implements JavaTransformer {
     private final AtomicInteger counter = new AtomicInteger();
@@ -91,18 +95,17 @@ private BlockStmt desugarResources(List<Expression> resources, int index, BlockS
             BlockStmt result = new BlockStmt();
 
             Expression resourceExpr = resources.get(index);
-            String resourceName;
+            Expression resourceName;
 
-            if (resourceExpr instanceof VariableDeclarationExpr) {
+            if (resourceExpr instanceof VariableDeclarationExpr vde) {
                 // try (Resource r = new Resource()) { ... }
-                VariableDeclarationExpr vde = (VariableDeclarationExpr) resourceExpr;
                 VariableDeclarator vd = vde.getVariable(0);
-                resourceName = vd.getNameAsString();
+                resourceName = vd.getNameAsExpression();
                 result.addStatement(new ExpressionStmt(vde.clone()));
             } else {
                 // Java 9+ form: try (existingEffectivelyFinalVar) { ... }
                 // No declaration needed -- the variable already exists in scope.
-                resourceName = resourceExpr.toString();
+                resourceName = resourceExpr;
             }
 
             int id = counter.incrementAndGet();
@@ -118,14 +121,17 @@ private BlockStmt desugarResources(List<Expression> resources, int index, BlockS
 
             // catch (Throwable t$n) { primaryExc$n = t$n; throw t$n; }
             CatchClause catchClause = new CatchClause();
-            catchClause.setParameter(new Parameter(new ClassOrInterfaceType(null, "Throwable"), throwableName));
+            catchClause.setParameter(
+                new Parameter(new ClassOrInterfaceType(null, "Throwable"), throwableName));
             BlockStmt catchBody = new BlockStmt();
             catchBody.addStatement(new ExpressionStmt(
-                    new AssignExpr(new NameExpr(primaryExcName), new NameExpr(throwableName), AssignExpr.Operator.ASSIGN)));
+                new AssignExpr(new NameExpr(primaryExcName), new NameExpr(throwableName),
+                    AssignExpr.Operator.ASSIGN)));
             catchBody.addStatement(new ThrowStmt(new NameExpr(throwableName)));
             catchClause.setBody(catchBody);
 
-            // finally { if (r != null) { if (primaryExc$n != null) { try { r.close(); } catch (Throwable s) { primaryExc$n.addSuppressed(s); } } else { r.close(); } } }
+            // finally { if (r != null) { if (primaryExc$n != null) { try { r.close(); } catch
+            // (Throwable s) { primaryExc$n.addSuppressed(s); } } else { r.close(); } } }
             BlockStmt finallyBlock = new BlockStmt();
 
             IfStmt excCheck = new IfStmt();
@@ -137,10 +143,12 @@ private BlockStmt desugarResources(List<Expression> resources, int index, BlockS
             closeWithSuppression.setTryBlock(closeTryBlock);
 
             CatchClause suppressCatch = new CatchClause();
-            suppressCatch.setParameter(new Parameter(new ClassOrInterfaceType(null, "Throwable"), suppressedExcName));
+            suppressCatch.setParameter(
+                new Parameter(new ClassOrInterfaceType(null, "Throwable"), suppressedExcName));
             BlockStmt suppressBody = new BlockStmt();
             suppressBody.addStatement(new ExpressionStmt(new MethodCallExpr(
-                    new NameExpr(primaryExcName), "addSuppressed", NodeList.nodeList(new NameExpr(suppressedExcName)))));
+                new NameExpr(primaryExcName), "addSuppressed",
+                NodeList.nodeList(new NameExpr(suppressedExcName)))));
             suppressCatch.setBody(suppressBody);
             closeWithSuppression.setCatchClauses(NodeList.nodeList(suppressCatch));
 
@@ -151,7 +159,7 @@ private BlockStmt desugarResources(List<Expression> resources, int index, BlockS
             excCheck.setElseStmt(plainClose);
 
             IfStmt nullCheck = new IfStmt();
-            nullCheck.setCondition(notNull(new NameExpr(resourceName)));
+            nullCheck.setCondition(notNull(resourceName.clone()));
             BlockStmt nullCheckThen = new BlockStmt();
             nullCheckThen.addStatement(excCheck);
             nullCheck.setThenStmt(nullCheckThen);
@@ -171,13 +179,15 @@ private static BinaryExpr notNull(Expression e) {
             return new BinaryExpr(e, new NullLiteralExpr(), BinaryExpr.Operator.NOT_EQUALS);
         }
 
-        private static MethodCallExpr closeCall(String resourceName) {
-            return new MethodCallExpr(new NameExpr(resourceName), "close");
+        private static MethodCallExpr closeCall(Expression resourceName) {
+            return new MethodCallExpr(resourceName.clone(), "close");
         }
 
-        private static Statement declareVar(String typeName, String varName, Expression initializer) {
-            VariableDeclarator vd = new VariableDeclarator(new ClassOrInterfaceType(null, typeName), varName, initializer);
+        private static Statement declareVar(String typeName, String varName,
+                Expression initializer) {
+            VariableDeclarator vd = new VariableDeclarator(new ClassOrInterfaceType(null, typeName),
+                varName, initializer);
             return new ExpressionStmt(new VariableDeclarationExpr(vd));
         }
     }
-}
+}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/AutoCloseable.java

@@ -0,0 +1,5 @@
+package java.lang;
+
+public interface AutoCloseable {
+    void close() throws Exception;
+}