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 aea33ddade..8447f5d9a8 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 @@ -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 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); } } } 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 6f975e7722..10d3ce13c9 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,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 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; + } + } }