Lambda support by transformation

key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java

@@ -42,6 +42,7 @@ public static KeYJavaPipeline createDefault(TransformationPipelineServices pipel
         p.add(new EnumClassBuilder(pipelineServices));
         p.add(new RecordClassBuilder(pipelineServices));
         p.add(new JMLTransformer(pipelineServices));
+        p.add(new LambdaReplacer(pipelineServices));
         p.add(new JmlDocRemoval(pipelineServices));
         p.add(new ImplicitFieldAdder(pipelineServices));
         p.add(new InstanceAllocationMethodBuilder(pipelineServices));

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

@@ -34,8 +34,11 @@
 import com.github.javaparser.resolution.types.ResolvedReferenceType;
 import com.github.javaparser.resolution.types.ResolvedType;
 import org.jspecify.annotations.NonNull;
+import de.uka.ilkd.key.speclang.PositionedString;
+import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
+import org.key_project.util.collection.ImmutableList;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -523,4 +526,33 @@ private static boolean isInside(Node container, Node declaration) {
                     container.containsWithinRange(declaration);
         }
     }
+
+
+    /**
+     * Generates unique names for generated inner classes.
+     */
+    class NameGenerator {
+
+        private final Set<String> generatedNames = new HashSet<>();
+
+        public String generate(String prefix, Position pos) {
+            return generate(prefix, pos, null);
+        }
+
+        private String generate(String prefix, Position pos, Integer counter) {
+            Integer line = pos != null ? pos.line : null;
+
+            String newName = prefix + "L" + line;
+            if (counter != null) {
+                newName += "_" + counter;
+            }
+
+            if (generatedNames.contains(newName)) {
+                return generate(prefix, pos, counter == null ? 0 : counter + 1);
+            }
+
+            generatedNames.add(newName);
+            return newName;
+        }
+    }
 }

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

@@ -0,0 +1,25 @@
+import com.sun.tools.javac.tree.JCTree;
+import com.sun.tools.javac.util.Context;
+import com.sun.tools.javac.util.List;
+import org.jmlspecs.openjml.JmlTree;
+import org.jmlspecs.openjml.JmlTreeTranslator;
+
+public class DeclarationEmbeddingTranslator extends JmlTreeTranslator {
+    private final JmlTree.Maker maker;
+    private final java.util.List<? extends JCTree> embeddable;
+
+    public DeclarationEmbeddingTranslator(Context context, java.util.List<? extends JCTree> embeddable) {
+        maker = JmlTree.Maker.instance(context);
+        this.embeddable = embeddable;
+    }
+
+    @Override
+    public JCTree translate(JCTree tree) {
+        if (tree instanceof JCTree.JCClassDecl) {
+            JCTree.JCClassDecl classDecl = (JCTree.JCClassDecl) tree;
+            List<JCTree> newDefs = classDecl.defs.appendList(List.from(embeddable));
+            return maker.ClassDef(classDecl.mods, classDecl.name, classDecl.typarams, classDecl.extending, classDecl.implementing, newDefs);
+        }
+        return super.translate(tree);
+    }
+}

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

@@ -0,0 +1,33 @@
+import com.sun.org.apache.bcel.internal.generic.Select;
+import com.sun.tools.javac.code.Symbol;
+import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.tree.JCTree;
+import com.sun.tools.javac.util.Name;
+import org.jmlspecs.openjml.JmlTree;
+import org.jmlspecs.openjml.JmlTreeTranslator;
+
+/**
+ * Converts all Identifiers, that reference class-fields into field accesses.
+ * Example `class Test { int a; void m() {a = 2; }}` will become
+ * `class Test { int a; void m() {this.a = 2; }}`
+ * Usage: identifierToFieldAccessNormalizer.translate(myAst)
+ */
+public class IdentifierToFieldAccessNormalizer {
+    @Override
+    public JCTree translate(JCTree tree) {
+        if (tree instanceof JCTree.JCIdent) {
+            JCTree.JCIdent ident = (JCTree.JCIdent) tree;
+            if (ident.sym != null
+                    && ident.sym.owner instanceof Symbol.ClassSymbol
+                    && !ident.name.toString().equals("this")
+                    && !(ident.type instanceof Type.ClassType)
+            ) {
+                JCTree.JCFieldAccess select = maker.Select(maker.This(ident.sym.owner.type), ident.name);
+                select.sym = ident.sym;
+                return select;
+            }
+        }
+        return super.translate(tree);
+    }
+
+}

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

@@ -0,0 +1,25 @@
+package de.uka.ilkd.key.java.transformations.pipeline.lambda;
+
+import com.sun.tools.javac.util.List;
+
+public class LambdaContractExtractor extends JmlTreeScanner {
+    public List<JmlTree.JmlSpecificationCase> spec;
+
+    @Override
+    public void visitJmlBlock(JmlTree.JmlBlock that) {
+        super.visitJmlBlock(that);
+    }
+
+    @Override
+    public void visitJmlStatementSpec(JmlTree.JmlStatementSpec tree) {
+        this.spec = tree.statementSpecs.cases;
+        tree.statementSpecs.cases = List.nil();
+        super.visitJmlStatementSpec(tree);
+    }
+
+    @Override
+    public void visitJmlStatement(JmlTree.JmlStatement that) {
+        System.out.println("ads");
+        super.visitJmlStatement(that);
+    }
+}

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

@@ -0,0 +1,49 @@
+package de.uka.ilkd.key.java.transformations.pipeline.lambda;
+
+import de.uka.ilkd.key.java.ast.CompilationUnit;
+import de.uka.ilkd.key.java.ast.declaration.ClassDeclaration;
+import de.uka.ilkd.key.java.transformations.pipeline.JavaTransformer;
+import transform.NormalizedLambda;
+import transform.Replacement;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class LambdaReplacer implements JavaTransformer {
+    private final List<ClassDeclaration> exportedDeclarations = new ArrayList<>();
+    private final NameGenerator nameGenerator;
+    private final CompilationUnit compilationUnit;
+
+    public LambdaReplacer(CompilationUnit compilationUnit, NameGenerator nameGenerator) {
+        this.compilationUnit = compilationUnit;
+        this.nameGenerator = nameGenerator;
+    }
+
+    @Override
+    public void apply(com.github.javaparser.ast.CompilationUnit cu) {
+        JavaTransformer.super.apply(cu);
+    }
+
+    @Override
+    public JCTree translate(JCTree tree) {
+        if (tree instanceof JCTree.JCLambda) {
+            JCTree.JCLambda lambda = (JCTree.JCLambda) tree;
+
+            // Replaces other Lambdas in Lambda's Body
+            LambdaReplacer lambdaBodyReplacer = new LambdaReplacer(context, compilationUnit);
+            lambda.body = lambdaBodyReplacer.translate(lambda.body);
+            //TODO: api.typecheck() generated program. Does not seem to help?
+
+            NormalizedLambda normalizedLambda = new NormalizedLambda(lambda, nameGenerator, context);
+            Replacement lambdaReplacement = new Replacement(normalizedLambda, nameGenerator, context);
+            exportedDeclarations.add(lambdaReplacement.getReplacementInnerClass());
+            exportedDeclarations.addAll(lambdaBodyReplacer.getExportedDeclarations());
+            return lambdaReplacement.getReplacementReference();
+        }
+        return super.translate(tree);
+    }
+
+    public List<JCTree.JCClassDecl> getExportedDeclarations() {
+        return exportedDeclarations;
+    }
+}