diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java index da9dff5027..db0c6db697 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java @@ -40,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)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LambdaReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LambdaReplacer.java new file mode 100644 index 0000000000..78baa4a186 --- /dev/null +++ b/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. + *

+ * 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 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 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 findSingleAbstractInterface(LambdaExpr lambdaExpr) { + ClassOrInterfaceType type = assignToType(lambdaExpr); + + if (type == null) { + return inferDefaultAbstractInterface(lambdaExpr); + } else { + return new Pair<>(type.getNameAsString(), new MethodDeclaration()); + } + } + + private Pair 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 + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java index c191d4ddfb..2f37d54d9e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java @@ -6,12 +6,10 @@ 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; -import de.uka.ilkd.key.speclang.PositionedString; - -import org.key_project.util.collection.ImmutableList; import com.github.javaparser.JavaParser; import com.github.javaparser.ast.CompilationUnit; @@ -28,8 +26,11 @@ import com.github.javaparser.resolution.model.SymbolReference; import com.github.javaparser.resolution.types.ResolvedReferenceType; import com.github.javaparser.resolution.types.ResolvedType; +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; @@ -447,4 +448,33 @@ private static boolean isInside(Node container, Node declaration) { container.containsWithinRange(declaration); } } + + + /** + * Generates unique names for generated inner classes. + */ + class NameGenerator { + + private final Set 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; + } + } }