Lambda support by transformation

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

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java.transformations;
 
+import java.net.URI;
 import java.util.Collection;
 import java.util.LinkedList;
 import java.util.List;
@@ -39,6 +40,7 @@ public static KeYJavaPipeline createDefault(TransformationPipelineServices pipel
         KeYJavaPipeline p = new KeYJavaPipeline(pipelineServices);
         p.add(new EnumClassBuilder(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));
@@ -67,16 +69,16 @@ public void apply() {
 
     public void apply(Collection<CompilationUnit> compilationUnits) {
         for (CompilationUnit compilationUnit : compilationUnits) {
+            URI resource = compilationUnit.getStorage()
+                    .map(it -> it.getPath().toUri())
+                    .orElse(null);
+
             for (JavaTransformer step : steps) {
                 long start = System.currentTimeMillis();
                 step.apply(compilationUnit);
                 long stop = System.currentTimeMillis();
-                if (compilationUnit.getStorage().isPresent()) {
-                    LOGGER.debug("Processed {} on {} ms: {}",
-                        step.getClass().getSimpleName(),
-                        compilationUnit.getStorage().get().getPath(),
-                        stop - start);
-                }
+                LOGGER.debug("Processed {} on {} ms: {}",
+                        step.getClass().getSimpleName(), resource, stop - start);
             }
         }
     }

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

@@ -0,0 +1,162 @@
+package de.uka.ilkd.key.java.transformations.pipeline;
+
+import com.github.javaparser.ast.Node;
+import com.github.javaparser.ast.NodeList;
+import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
+import com.github.javaparser.ast.body.MethodDeclaration;
+import com.github.javaparser.ast.body.TypeDeclaration;
+import com.github.javaparser.ast.expr.LambdaExpr;
+import com.github.javaparser.ast.expr.ObjectCreationExpr;
+import com.github.javaparser.ast.stmt.BlockStmt;
+import com.github.javaparser.ast.stmt.ExpressionStmt;
+import com.github.javaparser.ast.stmt.Statement;
+import com.github.javaparser.ast.type.ClassOrInterfaceType;
+import com.github.javaparser.utils.Pair;
+import org.jspecify.annotations.NonNull;
+
+import java.util.Optional;
+
+/**
+ * Replaces lambda expressions by an internal named class.
+ * <p>
+ * Code was donated by Carsten Czisky @ciskar
+ */
+public class LambdaReplacer extends JavaTransformer {
+
+    /**
+     * creates a transformer for the recoder model
+     *
+     * @param services the CrossReferenceServiceConfiguration to access
+     *                 model information
+     */
+    public LambdaReplacer(@NonNull TransformationPipelineServices services) {
+        super(services);
+    }
+
+    @Override
+    public void apply(TypeDeclaration<?> td) {
+        td.walk(LambdaExpr.class, this::rewriteLambda);
+    }
+
+    private void rewriteLambda(LambdaExpr expr) {
+        @SuppressWarnings({"rawtypes", "unchecked"})
+        Optional<TypeDeclaration> enclosingType = expr.findAncestor(TypeDeclaration.class);
+
+        if (enclosingType.isEmpty()) {
+            throw new IllegalStateException("LambdaExpr is not enclosed in a type declaration");
+        }
+
+        ClassOrInterfaceDeclaration decl = liftToInnerClass(expr);
+        enclosingType.get().addMember(decl);
+
+        var objectCreation = instantiate(decl);
+        expr.replace(objectCreation);
+    }
+
+    private ObjectCreationExpr instantiate(ClassOrInterfaceDeclaration decl) {
+        ClassOrInterfaceType type = new ClassOrInterfaceType(null, decl.getNameAsString());
+        return new ObjectCreationExpr(null, type, new NodeList<>());
+    }
+
+    private ClassOrInterfaceDeclaration liftToInnerClass(LambdaExpr lambdaExpr) {
+        Pair<String, MethodDeclaration> sai = findSingleAbstractInterface(lambdaExpr);
+        String interfaceName = sai.a;
+        MethodDeclaration method = sai.b;
+
+        String name = services.getFreshName("__GENERATED_",
+                lambdaExpr.getRange().map(r -> r.begin).orElse(null));
+
+        ClassOrInterfaceDeclaration it =
+                new ClassOrInterfaceDeclaration(new NodeList<>(), false, name);
+
+        it.addImplementedType(interfaceName);
+        it.addMember(method);
+
+        return it;
+    }
+
+    private Pair<String, MethodDeclaration> findSingleAbstractInterface(LambdaExpr lambdaExpr) {
+        ClassOrInterfaceType type = assignToType(lambdaExpr);
+
+        if (type == null) {
+            return inferDefaultAbstractInterface(lambdaExpr);
+        } else {
+            return new Pair<>(type.getNameAsString(), new MethodDeclaration());
+        }
+    }
+
+    private Pair<String, MethodDeclaration> inferDefaultAbstractInterface(LambdaExpr lambdaExpr) {
+        String interfaze;
+        MethodDeclaration md = new MethodDeclaration();
+
+        Node body = lambdaExpr.getBody();
+        String returnType = null;
+
+        if (body instanceof BlockStmt block) {
+            Statement last = block.getStatements().isEmpty()
+                    ? null
+                    : block.getStatements().getLast();
+
+            if (last != null && last.isReturnStmt()) {
+                returnType = last.asReturnStmt()
+                        .getExpression()
+                        .map(e -> e.calculateResolvedType().toString())
+                        .orElse(null);
+            }
+        }
+
+        if (body instanceof ExpressionStmt es) {
+            returnType = es.getExpression().calculateResolvedType().toString();
+        }
+
+        int paramCount = lambdaExpr.getParameters().size();
+
+        switch (paramCount) {
+            case 0:
+                if (returnType == null) {
+                    interfaze = "Runnable";
+                    md.setName("run");
+                } else {
+                    interfaze = "java.util.function.Supplier<" + returnType + ">";
+                    md.setName("accept");
+                }
+                break;
+
+            case 1:
+                String firstParam = lambdaExpr.getParameter(0).getTypeAsString();
+                if (returnType == null) {
+                    interfaze = "java.util.function.Consumer<" + firstParam + ">";
+                    md.setName("get");
+                } else {
+                    interfaze = "java.util.function.Function<" + firstParam + ", " + returnType + ">";
+                    md.setName("invoke");
+                }
+                break;
+
+            case 2:
+                String p1 = lambdaExpr.getParameter(0).getTypeAsString();
+                String p2 = lambdaExpr.getParameter(1).getTypeAsString();
+                if (returnType == null) {
+                    interfaze = "java.util.function.BiConsumer<" + p1 + "," + p2 + ">";
+                    md.setName("get");
+                } else {
+                    interfaze = "java.util.function.BiFunction<" + p1 + ", " + p2 + ", " + returnType + ">";
+                    md.setName("invoke");
+                }
+                break;
+
+            default:
+                throw new IllegalStateException("ASM could not be inferred");
+        }
+
+        lambdaExpr.getParameters().forEach(p -> md.addParameter(p.clone()));
+
+        return new Pair<>(interfaze, md);
+    }
+
+    private ClassOrInterfaceType assignToType(LambdaExpr lambdaExpr) {
+        var type = lambdaExpr.calculateResolvedType();
+        System.out.println("TEST: " + type);
+        return null; // TODO
+    }
+}

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

@@ -6,6 +6,7 @@
 import java.util.*;
 import java.util.stream.Collectors;
 
+import com.github.javaparser.Position;
 import de.uka.ilkd.key.java.loader.JavaParserFactory;
 import de.uka.ilkd.key.java.transformations.ConstantExpressionEvaluator;
 import de.uka.ilkd.key.java.transformations.EvaluationException;
@@ -307,6 +308,11 @@ public JavaParser getParser() {
         return javaParserFactory.createJavaParser();
     }
 
+    public String getFreshName(String generated, Position position) {
+        //TODO
+        return generated;
+    }
+
     /**
      * Cache of important data. This is done mainly for performance reasons.
      * It contains the following info:
@@ -472,4 +478,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;
+        }
+    }
 }