From 8d061d55f71fbbe9855a4511c7ba63ec6626e3c6 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 11 Mar 2026 21:33:12 +0100 Subject: [PATCH 1/4] Csiky @csicar Lambda to Plain Java transformation # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java --- .../java/transformations/KeYJavaPipeline.java | 1 + .../pipeline/LambdaReplacer.java | 162 ++++++++++++++++++ .../TransformationPipelineServices.java | 32 ++++ 3 files changed, 195 insertions(+) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LambdaReplacer.java 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 a5fd03e0dcd..dc4a2f8ca58 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 @@ -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)); 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 00000000000..78baa4a186e --- /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 e72cc176ab8..d4e9d6a6d54 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 @@ -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 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; + } + } } From bf5f156df377e1cd95b2390820292cec8020f01b Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 5 Jul 2026 21:17:28 +0200 Subject: [PATCH 2/4] add csiky's stuff completely. looks like we should rather completely rewrite it. --- .../pipeline/LambdaReplacer.java | 162 ---------- .../DeclarationEmbeddingTranslator.java | 25 ++ .../IdentifierToFieldAccessNormalizer.java | 33 ++ .../lambda/LambdaContractExtractor.java | 25 ++ .../pipeline/lambda/LambdaReplacer.java | 49 +++ .../pipeline/lambda/NameGenerator.java | 53 ++++ .../lambda/analyzer/FreeVariablesLocator.java | 212 +++++++++++++ .../transform/ContractToModelMethods.java | 23 ++ .../lambda/transform/LambdaContract.java | 161 ++++++++++ .../lambda/transform/NormalizedLambda.java | 296 ++++++++++++++++++ .../lambda/transform/RenameVariable.java | 67 ++++ .../lambda/transform/Replacement.java | 62 ++++ .../pipeline/lambda/transform/TLambda.java | 19 ++ 13 files changed, 1025 insertions(+), 162 deletions(-) delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LambdaReplacer.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/DeclarationEmbeddingTranslator.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/IdentifierToFieldAccessNormalizer.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaContractExtractor.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaReplacer.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/NameGenerator.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/analyzer/FreeVariablesLocator.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/ContractToModelMethods.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/LambdaContract.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/NormalizedLambda.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/RenameVariable.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/Replacement.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/TLambda.java 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 deleted file mode 100644 index 78baa4a186e..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LambdaReplacer.java +++ /dev/null @@ -1,162 +0,0 @@ -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/lambda/DeclarationEmbeddingTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/DeclarationEmbeddingTranslator.java new file mode 100644 index 00000000000..e93d5e23b35 --- /dev/null +++ b/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 embeddable; + + public DeclarationEmbeddingTranslator(Context context, java.util.List 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 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); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/IdentifierToFieldAccessNormalizer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/IdentifierToFieldAccessNormalizer.java new file mode 100644 index 00000000000..cb65d7ad527 --- /dev/null +++ b/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); + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaContractExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaContractExtractor.java new file mode 100644 index 00000000000..fcfac9a25d9 --- /dev/null +++ b/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 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); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaReplacer.java new file mode 100644 index 00000000000..f0c4580e166 --- /dev/null +++ b/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 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 getExportedDeclarations() { + return exportedDeclarations; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/NameGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/NameGenerator.java new file mode 100644 index 00000000000..ad61572124e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/NameGenerator.java @@ -0,0 +1,53 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda; + +import com.github.javaparser.Position; +import com.github.javaparser.ast.expr.SimpleName; +import com.sun.source.tree.LineMap; + +import java.util.ArrayList; +import java.util.List; + +/** + * Generates names guaranteeing uniqueness in generated names by one instance of NameGenerator. + */ +public class NameGenerator { + private final LineMap lineMap; + private final List generatedNames; + + public NameGenerator(LineMap lineMap) { + this.lineMap = lineMap; + this.generatedNames = new ArrayList<>(); + } + + /** + * Generates a unique name based on the prefix and position. + * + * @param prefix the prefix for the generated name + * @param pos the position in the source file + * @return a unique Name + */ + public SimpleName generate(String prefix, Position pos) { + return generate(prefix, pos, null); + } + + /** + * Recursively generates a unique name. + * + * @param prefix the prefix for the generated name + * @param pos the position in the source file + * @param counter an optional counter for disambiguation + * @return a unique Name + */ + private SimpleName generate(String prefix, Position pos, Integer counter) { + int line = pos.line; + String newName = "%sL%d".formatted(prefix, line); + if (counter != null) { + newName += "_" + counter; + } + if (generatedNames.contains(newName)) { + return generate(prefix, pos, counter == null ? 0 : counter + 1); + } + generatedNames.add(newName); + return new SimpleName(newName); + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/analyzer/FreeVariablesLocator.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/analyzer/FreeVariablesLocator.java new file mode 100644 index 00000000000..3ee82ae17f2 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/analyzer/FreeVariablesLocator.java @@ -0,0 +1,212 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda.analyzer; + +import java.util.*; + +/** + * Locates and extracts free variables from Java trees. + */ +public class FreeVariablesLocator extends JmlTreeScanner { + + /** + * Tracks the binding status of variables during traversal. + */ + private static class VariableBindingStatus { + private final Set innerFreeVariables = new HashSet<>(); + private final Set boundVariables = new HashSet<>(); + + /** + * Adds all symbols as bound variables. + * + * @param syms the symbols to add as bound + */ + void addAllBound(Collection syms) { + for (Symbol sym : syms) { + boundVariables.add(sym); + } + // Ensure uniqueness by name + Set seen = new HashSet<>(); + boundVariables.removeIf(sym -> !seen.add(new NameWrapper(sym.name.toString()))); + } + + /** + * Adds all symbols as free variables. + * + * @param syms the symbols to add as free + */ + void addAllFree(Collection syms) { + for (Symbol sym : syms) { + innerFreeVariables.add(sym); + } + // Ensure uniqueness by name + Set seen = new HashSet<>(); + innerFreeVariables.removeIf(sym -> !seen.add(new NameWrapper(sym.name.toString()))); + } + + /** + * Gets the set of free variables (free minus bound). + * + * @return the set of free variables + */ + Set getFreeVariables() { + Set result = new HashSet<>(innerFreeVariables); + result.removeAll(boundVariables); + // Ensure uniqueness by name + Set seen = new HashSet<>(); + result.removeIf(sym -> !seen.add(new NameWrapper(sym.name.toString()))); + return result; + } + + /** + * Adds a single symbol as a free variable. + * + * @param sym the symbol to add + */ + void addFree(Symbol sym) { + addAllFree(Collections.singletonList(sym)); + } + + /** + * Adds a single symbol as a bound variable. + * + * @param sym the symbol to add + */ + void addBound(Symbol sym) { + addAllBound(Collections.singletonList(sym)); + } + } + + /** + * Wrapper class for comparing names by string value. + */ + private static class NameWrapper { + private final String name; + + NameWrapper(String name) { + this.name = name; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + NameWrapper that = (NameWrapper) o; + return Objects.equals(name, that.name); + } + + @Override + public int hashCode() { + return Objects.hash(name); + } + } + + private final VariableBindingStatus variablesBindings; + private final JmlTree.Maker maker; + private final Names names; + + /** + * Constructs a FreeVariablesLocator. + * + * @param context the javac context + */ + public FreeVariablesLocator(Context context) { + this.context = context; + this.variablesBindings = new VariableBindingStatus(); + this.maker = JmlTree.Maker.instance(context); + this.names = Names.instance(context); + } + + /** + * Convenience method for extracting free variables from multiple trees. + * + * @param trees the trees to analyze + * @return the set of free variable symbols + */ + public Set extractFreeVariables(JCTree... trees) { + for (JCTree tree : trees) { + if (tree != null) { + tree.accept(this); + } + } + return variablesBindings.getFreeVariables(); + } + + @Override + public void visitJmlQuantifiedExpr(JmlTree.JmlQuantifiedExpr that) { + FreeVariablesLocator nested = new FreeVariablesLocator(context); + Set vars = nested.extractFreeVariables(that.racexpr, that.racexpr, that.value); + + Set declSymbols = new HashSet<>(); + for (JmlTree.JmlVariableDecl decl : that.decls) { + declSymbols.add(decl.sym); + } + + Set freeVars = new HashSet<>(vars); + freeVars.removeAll(declSymbols); + variablesBindings.addAllFree(freeVars); + } + + @Override + public void visitMethodDef(JCTree.JCMethodDecl tree) { + FreeVariablesLocator nested = new FreeVariablesLocator(context); + Set vars = nested.extractFreeVariables(tree.body); + + Set paramSymbols = new HashSet<>(); + for (JCTree.JCVariableDecl param : tree.params) { + paramSymbols.add(param.sym); + } + + Set freeVars = new HashSet<>(vars); + // Filter out 'this' references + freeVars.removeIf(sym -> sym.name.equals(names._this)); + freeVars.removeAll(paramSymbols); + variablesBindings.addAllFree(freeVars); + } + + @Override + public void visitVarDef(JCTree.JCVariableDecl tree) { + variablesBindings.addBound(tree.sym); + super.visitVarDef(tree); + } + + @Override + public void visitAnnotation(JCTree.JCAnnotation tree) { + System.out.println("ignore annotation " + tree); + // Don't traverse into annotations + } + + @Override + public void visitLambda(JCTree.JCLambda tree) { + FreeVariablesLocator nested = new FreeVariablesLocator(context); + Set vars = nested.extractFreeVariables(tree.body); + + Set paramSymbols = new HashSet<>(); + for (JCTree.JCVariableDecl param : tree.params) { + paramSymbols.add(param.sym); + } + + Set freeVars = new HashSet<>(vars); + freeVars.removeAll(paramSymbols); + variablesBindings.addAllFree(freeVars); + } + + @Override + public void visitIdent(JCTree.JCIdent tree) { + if (tree.name.toString().isEmpty()) { + return; + } + if (tree.sym == null) { + // FIXME this case can be removed if types are regenerated after each lambda-replacement pass + return; + } + if (tree.sym instanceof Symbol.ClassSymbol) { + // Class-Symbols are no free variables + return; + } + if (tree.sym.owner instanceof Symbol.ClassSymbol && !tree.name.toString().equals("this")) { + JCTree.JCIdent ref = (JCTree.JCIdent) maker.This(tree.sym.owner.type); + variablesBindings.addFree(ref.sym); + return; + } + variablesBindings.addFree(tree.sym); + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/ContractToModelMethods.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/ContractToModelMethods.java new file mode 100644 index 00000000000..7d966be645a --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/ContractToModelMethods.java @@ -0,0 +1,23 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda.transform; + +import com.sun.tools.javac.util.List; +import org.jmlspecs.openjml.JmlTokenKind; +import org.jmlspecs.openjml.JmlTree; + +/** + * Utility class for converting contracts to model methods. + */ +public class ContractToModelMethods { + /** + * Converts a contract to a model method declaration. + * + * @param maker the JML tree maker + * @param contracts the JML method clause contract + * @return a JML method clause declaration with MODEL token + */ + public static JmlTree.JmlMethodClauseDecl contractToModelMethod( + JmlTree.Maker maker, JmlTree.JmlMethodClause contracts) { + // Both REQUIRES and other contract types are converted to MODEL + return maker.JmlMethodClauseDecl(JmlTokenKind.MODEL, List.nil()); + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/LambdaContract.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/LambdaContract.java new file mode 100644 index 00000000000..8aa03d61dd4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/LambdaContract.java @@ -0,0 +1,161 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda.transform; + +import com.sun.tools.javac.code.Symbol; +import com.sun.tools.javac.code.Symtab; +import com.sun.tools.javac.tree.JCTree; +import com.sun.tools.javac.util.Context; +import com.sun.tools.javac.util.List; +import com.sun.tools.javac.util.Name; +import org.jmlspecs.openjml.JmlTokenKind; +import org.jmlspecs.openjml.JmlTree; +import org.jmlspecs.openjml.Utils; + +/** + * Represents a lambda expression with its associated JML contract specifications. + */ +public class LambdaContract { + + private final NormalizedLambda normalizedLambda; + private final JCTree.JCMethodDecl lambdaReplacementMethod; + private final Context context; + private final List lambdaContract; + private final JmlTree.Maker maker; + + /** + * Constructs a LambdaContract from a normalized lambda and its replacement method. + * + * @param normalizedLambda the normalized lambda expression + * @param lambdaReplacementMethod the method declaration that replaces the lambda + * @param context the javac context + */ + public LambdaContract(NormalizedLambda normalizedLambda, + JCTree.JCMethodDecl lambdaReplacementMethod, + Context context) { + this.normalizedLambda = normalizedLambda; + this.lambdaReplacementMethod = lambdaReplacementMethod; + this.context = context; + this.maker = JmlTree.Maker.instance(context); + this.lambdaContract = extractSpec(); + } + + /** + * Converts the lambda contract clauses to model method declarations. + * + * @return a list of JML method declarations representing the contract as model methods + */ + public List toModelMethods() { + if (lambdaContract.isEmpty()) { + return List.nil(); + } + + // Process only the first specification case (matching Kotlin implementation) + JmlTree.JmlSpecificationCase specCase = lambdaContract.head; + List result = List.nil(); + for (JmlTree.JmlMethodClause clause : specCase.clauses) { + JmlTree.JmlMethodDecl translated; + switch (clause.token) { + case REQUIRES: + translated = translateRequires(clause); + break; + case ENSURES: + translated = translateEnsures(clause); + break; + default: + throw new UnsupportedOperationException("Unsupported clause type: " + clause.token); + } + result = result.append(translated); + } + return List.from(result); + } + + /** + * Translates an ENSURES clause to a model method. + * + * @param clause the ENSURES clause to translate + * @return a JML method declaration representing the ensures condition + */ + private JmlTree.JmlMethodDecl translateEnsures(JmlTree.JmlMethodClause clause) { + Name name = maker.Name("postConditionMethod"); + System.out.println("Found clause "); + System.out.print(clause); + + if (clause instanceof JmlTree.JmlMethodClauseExpr) { + JmlTree.JmlMethodClauseExpr exprClause = (JmlTree.JmlMethodClauseExpr) clause; + Symbol.VarSymbol resultSymbol = new Symbol.VarSymbol( + 0, + maker.Name("__result"), + normalizedLambda.lambdaReturnType(), + null + ); + List extraParams = List.of(maker.VarDef(resultSymbol, null)); + return modelMethod(exprClause.expression, name, extraParams); + } + throw new UnsupportedOperationException("Unsupported ensures clause: " + clause.toString()); + } + + /** + * Translates a REQUIRES clause to a model method. + * + * @param clause the REQUIRES clause to translate + * @return a JML method declaration representing the requires condition + */ + private JmlTree.JmlMethodDecl translateRequires(JmlTree.JmlMethodClause clause) { + Name name = maker.Name("preConditionMethod"); + System.out.println("Found clause "); + System.out.print(clause); + + if (clause instanceof JmlTree.JmlMethodClauseExpr) { + JmlTree.JmlMethodClauseExpr exprClause = (JmlTree.JmlMethodClauseExpr) clause; + return modelMethod(exprClause.expression, name, List.nil()); + } + throw new UnsupportedOperationException("Unsupported requires clause: " + clause.toString()); + } + + /** + * Creates a model method from an expression. + * + * @param expression the expression to use in the method body + * @param methodName the name of the method + * @param extraParams additional parameters for the method + * @return a JML method declaration + */ + private JmlTree.JmlMethodDecl modelMethod(JCTree.JCExpression expression, + Name methodName, + List extraParams) { + Utils utils = Utils.instance(context); + + JmlTree.JmlAnnotation annotation = utils.tokenToAnnotationAST( + JmlTokenKind.MODEL, + expression.startPosition, + expression.startPosition + ); + JmlTree.JmlModifiers mods = maker.Modifiers(0, List.of(annotation)); + + Symtab symtab = Symtab.instance(context); + JCTree.JCExpression restype = maker.Type(symtab.booleanType); + + return maker.MethodDef( + mods, + methodName, + restype, + lambdaReplacementMethod.typarams, + null, + lambdaReplacementMethod.params.appendList(extraParams), + List.nil(), + maker.Block(0, List.of(maker.Return(expression))), + null + ); + } + + /** + * Extracts the JML specification from the lambda expression. + * + * @return a list of JML specification cases found in the lambda + */ + private List extractSpec() { + LambdaContractExtractor extractor = new LambdaContractExtractor(); + + normalizedLambda.lambda.accept(extractor); + return extractor.spec != null ? extractor.spec : List.nil(); + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/NormalizedLambda.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/NormalizedLambda.java new file mode 100644 index 00000000000..ca579d6f564 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/NormalizedLambda.java @@ -0,0 +1,296 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda.transform; + +import com.sun.tools.javac.code.Flags; +import com.sun.tools.javac.code.Symbol; +import com.sun.tools.javac.code.Symtab; +import com.sun.tools.javac.code.Type; +import com.sun.tools.javac.tree.JCTree; +import com.sun.tools.javac.tree.TreeMaker; +import com.sun.tools.javac.util.Context; +import com.sun.tools.javac.util.List; +import com.sun.tools.javac.util.Name; +import de.uka.ilkd.key.java.transformations.pipeline.lambda.IdentifierToFieldAccessNormalizer; +import de.uka.ilkd.key.java.transformations.pipeline.lambda.NameGenerator; +import org.jmlspecs.openjml.JmlTree; + +/** + * Represents a normalized lambda expression with methods to convert it to an inner class. + */ +public class NormalizedLambda extends TLambda { + + private final JCTree.JCLambda lambdaToNormalize; + + /** + * Constructs a NormalizedLambda from a lambda expression. + * + * @param lambdaToNormalize the lambda to normalize + * @param nameGenerator the name generator for creating unique names + * @param context the javac context + */ + public NormalizedLambda(JCTree.JCLambda lambdaToNormalize, NameGenerator nameGenerator, Context context) { + super(normalizeLambda(lambdaToNormalize, context, nameGenerator), nameGenerator, context); + this.lambdaToNormalize = lambdaToNormalize; + } + + /** + * Gets the return type of the lambda expression. + * + * @return the return type of the lambda's functional interface method + */ + public Type lambdaReturnType() { + return ((Type.MethodType) lambdaToNormalize.type.tsym.members().elems.sym.type).restype; + // TODO generate body-type for lambda and use that instead + // return lambdaToNormalize.body.type; + } + + /** + * Converts the lambda to an inner class definition and a new class instantiation. + * + * @param nameGenerator the name generator for creating unique names + * @param context the javac context + * @return a pair containing the inner class definition and the new class expression + */ + public Replacement.Pair lambdaToInnerMethod( + NameGenerator nameGenerator, Context context) { + + Name name = (lambda.type.tsym.name == null) + ? nameGenerator.generate("Lambda", lambda.startPosition) + : nameGenerator.generate(lambda.type.tsym.name.toString(), lambda.startPosition); + + JmlTree.Maker maker = JmlTree.Maker.instance(context); + IdentifierToFieldAccessNormalizer lambdaNormalizer = new IdentifierToFieldAccessNormalizer(maker); + JCTree.JCLambda normalizedLambda = (JCTree.JCLambda) lambdaNormalizer.translate(lambda); + TLambda normalizedLambdaInfo = new TLambda(normalizedLambda, nameGenerator, context); + + return new Replacement.Pair<>( + innerClassDefinition(name), + maker.NewClass( + null, + List.nil(), + maker.Ident(name), + List.from(normalizedLambdaInfo.getFreeVariables().stream() + .map(it -> maker.Ident(it.name)) + .collect(List.collector())), + null + ) + ); + } + + /** + * Creates the inner class definition for the lambda. + * + * @param name the name for the inner class + * @return the JML class declaration + */ + private JmlTree.JmlClassDecl innerClassDefinition(Name name) { + JmlTree.Maker maker = JmlTree.Maker.instance(context); + + Symbol.MethodSymbol methodSymbol = findAbstractMethodSymbol(); + Symbol.MethodSymbol definedMethodSymbol = new Symbol.MethodSymbol( + Flags.PUBLIC, + methodSymbol.name, + methodSymbol.type, + methodSymbol.owner + ); + definedMethodSymbol.params = List.from( + methodSymbol.params.stream() + .map(it -> new Symbol.VarSymbol( + it.flags(), + lambda.params.get(methodSymbol.params.indexOf(it)).name, + it.type, + it.owner + )) + .collect(List.collector()) + ); + + JCTree body = lambda.body; + JmlTree.JmlClassDecl clazz = maker.ClassDef( + maker.Modifiers(Flags.PUBLIC | Flags.FINAL | Flags.STATIC), + name, + List.nil(), + null, + List.of(maker.Ident(lambda.type.tsym.name)), + List.nil() + ); + + Name thisReplacement = maker.Name("outer_this"); + Name superReplacement = maker.Name("outer_super"); + JCTree.JCMethodDecl classConstructor = createInnerConstructor( + name, clazz, thisReplacement, superReplacement); + JCTree.JCMethodDecl lambdaMethod = createLambdaMethod( + maker, definedMethodSymbol, body, thisReplacement, superReplacement); + List modelMethods = + new LambdaContract(this, (JCTree.JCMethodDecl) lambdaMethod, context).toModelMethods(); + + List pseudoClosure = List.from(getFreeVariables().stream() + .map(it -> { + Name fieldName = (it.name.equals(maker.Name("this"))) ? thisReplacement : it.name; + if (it instanceof Symbol.VarSymbol) { + Symbol.VarSymbol varSym = (Symbol.VarSymbol) it; + return maker.VarDef( + maker.Modifiers(Flags.PRIVATE | Flags.FINAL), + fieldName, + maker.Type(varSym.type), + null + ); + } else if (it instanceof Symtab) { + Symtab symtab = (Symtab) it; + System.out.println(symtab); + return maker.VarDef(symtab.lengthVar, null); + } else { + throw new UnsupportedOperationException(it.toString()); + } + }) + .collect(List.collector())); + + clazz.defs = List.from(pseudoClosure.appendList(modelMethods).append(lambdaMethod).append(classConstructor)); + return clazz; + } + + /** + * Finds the abstract method symbol from the lambda's functional interface. + * + * @return the method symbol for the functional interface method + */ + private Symbol.MethodSymbol findAbstractMethodSymbol() { + return (Symbol.MethodSymbol) lambda.type.tsym.members().elements.stream() + .filter(it -> { + long flags = Flags.asFlagSet(it.flags()); + return it instanceof Symbol.MethodSymbol + && (flags & Flags.ABSTRACT) != 0 + && (flags & Flags.SYNTHETIC) == 0 + && (flags & Flags.DEFAULT) == 0; + }) + .findFirst() + .orElseThrow(() -> new IllegalStateException("No abstract method found in functional interface")); + } + + /** + * Creates the lambda method inside the inner class. + * + * @param maker the tree maker + * @param definedMethodSymbol the method symbol for the generated method + * @param body the lambda body + * @param thisReplacement replacement name for "this" + * @param superReplacement replacement name for "super" + * @return the method declaration + */ + private JCTree.JCMethodDecl createLambdaMethod( + JmlTree.Maker maker, + Symbol.MethodSymbol definedMethodSymbol, + JCTree body, + Name thisReplacement, + Name superReplacement) { + + RenameVariable thisSanitizer = new RenameVariable( + maker.Name("this"), context, name -> thisReplacement); + RenameVariable superSanitizer = new RenameVariable( + maker.Name("super"), context, name -> superReplacement); + + JCTree sanitizedBody = thisSanitizer.translate(superSanitizer.translate(body)); + + JCTree.JCStatement bodyStatement = (body instanceof JCTree.JCExpression) + ? maker.Return((JCTree.JCExpression) sanitizedBody) + : (JCTree.JCStatement) sanitizedBody; + + return maker.MethodDef( + definedMethodSymbol, + maker.Block(0, List.of(bodyStatement)) + ); + } + + /** + * Creates the constructor for the inner class. + * + * @param name the class name + * @param clazz the class declaration + * @param thisNameReplacement replacement name for "this" + * @param superNameReplacement replacement name for "super" + * @return the constructor declaration + */ + private JCTree.JCMethodDecl createInnerConstructor( + Name name, + JmlTree.JmlClassDecl clazz, + Name thisNameReplacement, + Name superNameReplacement) { + + JmlTree.Maker maker = JmlTree.Maker.instance(context); + TreeMaker jcMaker = TreeMaker.instance(context); + + Symbol.MethodSymbol constructorSymbol = new Symbol.MethodSymbol( + Flags.PUBLIC, name, Type.JCVoidType(), clazz.thisSymbol); + + List assignments = List.from(getFreeVariables().stream() + .map(it -> { + Name assignmentName = sanitizeName(maker, it.name, thisNameReplacement, superNameReplacement); + return jcMaker.Exec( + maker.Assign( + maker.QualIdent("this", assignmentName.toString()), + maker.Ident(assignmentName) + ) + ); + }) + .collect(List.collector())); + + JCTree.JCMethodDecl ctor = maker.MethodDef( + constructorSymbol, + maker.Block(0, assignments) + ); + + ctor.params = List.from(getFreeVariables().stream() + .map(it -> { + Name argumentName = sanitizeName(maker, it.name, thisNameReplacement, superNameReplacement); + return maker.VarDef( + maker.Modifiers(0), + argumentName, + maker.Type(it.type), + null + ); + }) + .collect(List.collector())); + + return ctor; + } + + /** + * Sanitizes a name by replacing special names like "this" and "super". + * + * @param maker the tree maker + * @param name the original name + * @param thisReplacementName replacement for "this" + * @param superReplacementName replacement for "super" + * @return the sanitized name + */ + private static Name sanitizeName( + JmlTree.Maker maker, + Name name, + Name thisReplacementName, + Name superReplacementName) { + + if (name.equals(maker.Name("this"))) { + return thisReplacementName; + } else if (name.equals(maker.Name("super"))) { + return superReplacementName; + } else { + return name; + } + } + + /** + * Normalizes a lambda expression by converting identifier accesses to field accesses. + * + * @param lambda the lambda to normalize + * @param context the javac context + * @param nameGenerator the name generator + * @return the normalized lambda + */ + public static JCTree.JCLambda normalizeLambda( + JCTree.JCLambda lambda, + Context context, + NameGenerator nameGenerator) { + + JmlTree.Maker maker = JmlTree.Maker.instance(context); + IdentifierToFieldAccessNormalizer lambdaNormalizer = new IdentifierToFieldAccessNormalizer(maker); + return (JCTree.JCLambda) lambdaNormalizer.translate(lambda); + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/RenameVariable.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/RenameVariable.java new file mode 100644 index 00000000000..bd6bb293d6f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/RenameVariable.java @@ -0,0 +1,67 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda.transform; + +import com.sun.tools.javac.code.Symbol; +import com.sun.tools.javac.tree.JCTree; +import com.sun.tools.javac.util.Context; +import com.sun.tools.javac.util.Name; +import org.jmlspecs.openjml.JmlTree; + +/** + * Renames variables in a JML tree by replacing occurrences of a specified name with a new name. + */ +public class RenameVariable extends JmlTreeTranslator { + + private final Name currentName; + private final Context context; + private final java.util.function.Function replacer; + private final JmlTree.Maker maker; + + /** + * Constructs a RenameVariable visitor. + * + * @param currentName the name to replace + * @param context the javac context + * @param replacer a function that takes the current name and returns the replacement name + */ + public RenameVariable(Name currentName, Context context, java.util.function.Function replacer) { + this.currentName = currentName; + this.context = context; + this.replacer = replacer; + this.maker = JmlTree.Maker.instance(context); + } + + @Override + public T translate(T tree) { + if (tree == null) { + return null; + } + + if (tree instanceof JCTree.JCIdent) { + JCTree.JCIdent ident = (JCTree.JCIdent) tree; + if (ident.name.equals(currentName)) { + Name newName = replacer.apply(ident.name); + Symbol.VarSymbol newSym = new Symbol.VarSymbol( + ident.sym.flags(), + newName, + ident.type, + ident.sym.owner + ); + return (T) maker.Ident(newSym); + } + } else if (tree instanceof JCTree.JCVariableDecl) { + JCTree.JCVariableDecl varDecl = (JCTree.JCVariableDecl) tree; + if (varDecl.name.equals(currentName)) { + Name newName = replacer.apply(varDecl.name); + Symbol.VarSymbol newSym = new Symbol.VarSymbol( + varDecl.sym.flags(), + newName, + varDecl.type, + varDecl.sym.owner + ); + return (T) maker.VarDef(newSym, varDecl.init); + } + } + + return super.translate(tree); + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/Replacement.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/Replacement.java new file mode 100644 index 00000000000..e53d7500869 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/Replacement.java @@ -0,0 +1,62 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda.transform; + +import de.uka.ilkd.key.java.transformations.pipeline.lambda.NameGenerator; +import com.sun.tools.javac.util.Context; +import org.jmlspecs.openjml.JmlTree; +import com.sun.tools.javac.tree.JCTree; + +/** + * Represents a replacement for a lambda expression with an inner class. + */ +public class Replacement { + + private final NormalizedLambda normalizedLambda; + private final NameGenerator nameGenerator; + private final Context context; + private final Pair replacements; + + /** + * Constructs a Replacement from a normalized lambda. + * + * @param normalizedLambda the normalized lambda to replace + * @param nameGenerator the name generator for creating unique names + * @param context the javac context + */ + public Replacement(NormalizedLambda normalizedLambda, NameGenerator nameGenerator, Context context) { + this.normalizedLambda = normalizedLambda; + this.nameGenerator = nameGenerator; + this.context = context; + this.replacements = normalizedLambda.lambdaToInnerMethod(nameGenerator, context); + } + + /** + * Gets the replacement inner class definition. + * + * @return the JML class declaration for the inner class + */ + public JmlTree.JmlClassDecl getReplacementInnerClass() { + return replacements.first; + } + + /** + * Gets the replacement reference (new class instantiation). + * + * @return the new class expression + */ + public JCTree.JCNewClass getReplacementReference() { + return replacements.second; + } + + /** + * Simple pair class to hold two values. + */ + public static class Pair { + public final F first; + public final S second; + + public Pair(F first, S second) { + this.first = first; + this.second = second; + } + } +} \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/TLambda.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/TLambda.java new file mode 100644 index 00000000000..81179088db9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/transform/TLambda.java @@ -0,0 +1,19 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda.transform; + +import analyzer.FreeVariablesLocator; +import com.github.javaparser.ast.expr.LambdaExpr; +import de.uka.ilkd.key.java.transformations.pipeline.lambda.NameGenerator; + +import java.util.Set; + +/** + * Represents a lambda expression with its free variables. + */ +public class TLambda { + protected final LambdaExpr lambda; + protected final NameGenerator nameGenerator; + + public Set getFreeVariables() { + return new FreeVariablesLocator(context).extractFreeVariables(lambda); + } +} \ No newline at end of file From 025488f14d00e6b1bb46467dda458b9ff715f1bc Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 5 Jul 2026 21:30:42 +0200 Subject: [PATCH 3/4] ask the AI to generate something --- .../lambda/LambdaToInnerClassTransformer.java | 312 ++++++++++++++++++ 1 file changed, 312 insertions(+) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaToInnerClassTransformer.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaToInnerClassTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaToInnerClassTransformer.java new file mode 100644 index 00000000000..22b3d18011a --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/lambda/LambdaToInnerClassTransformer.java @@ -0,0 +1,312 @@ +package de.uka.ilkd.key.java.transformations.pipeline.lambda; + +import com.github.javaparser.ast.*; +import com.github.javaparser.ast.body.*; +import com.github.javaparser.ast.expr.*; +import com.github.javaparser.ast.stmt.*; +import com.github.javaparser.ast.type.*; +import com.github.javaparser.ast.visitor.*; +import com.github.javaparser.resolution.types.ResolvedType; +import com.github.javaparser.resolution.declarations.ResolvedReferenceTypeDeclaration; +import com.github.javaparser.resolution.declarations.ResolvedMethodDeclaration; + +import java.util.*; + +/** + * Transforms lambda expressions into named inner classes that implement the + * appropriate Single Abstract Method (SAM) interface. + */ +public class LambdaToInnerClassTransformer extends VoidVisitorAdapter { + + private final String classPrefix; + private int counter = 0; + private final List> generatedInnerClasses = new ArrayList<>(); + + /** + * Constructs a LambdaToInnerClassTransformer. + * + * @param classPrefix the prefix for generated class names + */ + public LambdaToInnerClassTransformer(String classPrefix) { + this.classPrefix = classPrefix; + } + + /** + * Gets the list of generated inner classes. + * + * @return list of generated type declarations + */ + public List> getGeneratedInnerClasses() { + return generatedInnerClasses; + } + + @Override + public void visit(LambdaExpr lambdaExpr, Void arg) { + super.visit(lambdaExpr, arg); + + // Determine the parent node context + Node parent = lambdaExpr.getParentNode().orElse(null); + if (parent == null) { + return; + } + + // Generate a unique name for the inner class + String className = classPrefix + "_" + (counter++); + + // Create the inner class replacement + Expression innerClassInstance = createInnerClassForLambda(lambdaExpr, className); + + // Replace the lambda with the inner class instantiation + lambdaExpr.replace(innerClassInstance); + } + + /** + * Creates an inner class definition and returns an expression to instantiate it. + * + * @param lambdaExpr the lambda expression to convert + * @param className the name for the generated inner class + * @return an expression that instantiates the generated inner class + */ + private Expression createInnerClassForLambda(LambdaExpr lambdaExpr, String className) { + // Resolve the lambda's functional interface type + ResolvedType resolvedType = lambdaExpr.calculateResolvedType(); + ResolvedReferenceTypeDeclaration functionalInterface = resolvedType.asReferenceType().getTypeDeclaration(); + + // Find the single abstract method (SAM) + ResolvedMethodDeclaration sam = findSam(functionalInterface); + + // Extract captured variables (free variables) + List capturedVariables = findCapturedVariables(lambdaExpr); + + // Create the inner class declaration + ClassOrInterfaceDeclaration innerClass = new ClassOrInterfaceDeclaration( + new NodeList<>(Modifier.publicModifier(), Modifier.staticModifier(), Modifier.finalModifier()), + false, + className + ); + + // Add fields for captured variables + for (CapturedVariable captured : capturedVariables) { + FieldDeclaration field = new FieldDeclaration( + new NodeList<>(Modifier.privateModifier(), Modifier.finalModifier()), + captured.getType(), + captured.getName() + ); + innerClass.addMember(field); + } + + // Add constructor that accepts captured variables + ConstructorDeclaration constructor = new ConstructorDeclaration( + new NodeList<>(Modifier.publicModifier()), + className + ); + + // Add constructor parameters and assignments + for (CapturedVariable captured : capturedVariables) { + Parameter param = new Parameter(captured.getType(), captured.getName()); + constructor.addParameter(param); + + // Create assignment: this.fieldName = fieldName + AssignExpr assignExpr = new AssignExpr( + new FieldAccessExpr(new ThisExpr(), captured.getName()), + new NameExpr(captured.getName()), + AssignExpr.Operator.ASSIGN + ); + constructor.getBody().get().addStatement(new ExpressionStmt(assignExpr)); + } + innerClass.addMember(constructor); + + // Implement the SAM method + MethodDeclaration methodImpl = new MethodDeclaration( + new NodeList<>(Modifier.publicModifier()), + sam.getReturnType(), + sam.getName() + ); + + // Add parameters matching SAM signature + for (int i = 0; i < sam.getNumberOfParams(); i++) { + var param = sam.getParam(i); + methodImpl.addParameter(param.getType(), param.getName()); + } + + // Set the method body based on lambda body + setMethodBody(methodImpl, lambdaExpr, sam); + + innerClass.addMember(methodImpl); + + // Store the generated class + generatedInnerClasses.add(innerClass); + + // Create the instantiation expression + ObjectCreationExpr creationExpr = new ObjectCreationExpr(); + creationExpr.setType(className); + + // Add arguments for captured variables + for (CapturedVariable captured : capturedVariables) { + creationExpr.addArgument(new NameExpr(captured.getName())); + } + + return creationExpr; + } + + /** + * Finds the Single Abstract Method in a functional interface. + * + * @param functionalInterface the functional interface declaration + * @return the single abstract method + */ + private ResolvedMethodDeclaration findSam(ResolvedReferenceTypeDeclaration functionalInterface) { + List abstractMethods = new ArrayList<>(); + + for (ResolvedMethodDeclaration method : functionalInterface.getDeclaredMethods()) { + if (method.isAbstract() && !method.isDefaultMethod()) { + abstractMethods.add(method); + } + } + + if (abstractMethods.size() != 1) { + throw new IllegalStateException( + "Expected exactly one abstract method in functional interface, found: " + abstractMethods.size() + ); + } + + return abstractMethods.get(0); + } + + /** + * Finds all captured (free) variables in a lambda expression. + * + * @param lambdaExpr the lambda expression + * @return list of captured variables + */ + private List findCapturedVariables(LambdaExpr lambdaExpr) { + CapturedVariableCollector collector = new CapturedVariableCollector(); + lambdaExpr.getBody().accept(collector, null); + + // Remove lambda parameters from captured variables + Set paramNames = new HashSet<>(); + for (Parameter param : lambdaExpr.getParameters()) { + paramNames.add(param.getNameAsString()); + } + + List captured = new ArrayList<>(); + for (CapturedVariable var : collector.getCapturedVariables()) { + if (!paramNames.contains(var.getName())) { + captured.add(var); + } + } + + return captured; + } + + /** + * Sets the method body based on the lambda body. + * + * @param methodDecl the method declaration to populate + * @param lambdaExpr the source lambda expression + * @param sam the single abstract method + */ + private void setMethodBody(MethodDeclaration methodDecl, LambdaExpr lambdaExpr, ResolvedMethodDeclaration sam) { + var lambdaBody = lambdaExpr.getBody(); + + // Check if SAM returns void + if (sam.getReturnType().isVoid()) { + methodDecl.setBody(new BlockStmt(new NodeList<>(new ExpressionStmt(lambdaBody)))); + } else { + methodDecl.setBody(new BlockStmt(new NodeList<>(new ReturnStmt(lambdaBody.asExpressionStmt().expression())))); + } + } + + /** + * Represents a captured variable with its type and name. + */ + private static class CapturedVariable { + private final Type type; + private final String name; + + CapturedVariable(Type type, String name) { + this.type = type; + this.name = name; + } + + Type getType() { + return type; + } + + String getName() { + return name; + } + } + + /** + * Visitor that collects captured variables from a lambda body. + */ + private static class CapturedVariableCollector extends VoidVisitorAdapter { + private final List capturedVariables = new ArrayList<>(); + private final Set declaredInScope = new HashSet<>(); + + @Override + public void visit(NameExpr nameExpr, Void arg) { + super.visit(nameExpr, arg); + + // Try to resolve the name and check if it's a captured variable + try { + var resolved = nameExpr.resolve(); + String name = nameExpr.getNameAsString(); + + // Skip if already declared in local scope + if (declaredInScope.contains(name)) { + return; + } + + // Add as captured variable + Type type = parseType(resolved.describeType()); + capturedVariables.add(new CapturedVariable(type, name)); + } catch (Exception e) { + // Resolution failed, skip this name + } + } + + @Override + public void visit(Parameter parameter, Void arg) { + super.visit(parameter, arg); + declaredInScope.add(parameter.getNameAsString()); + } + + @Override + public void visit(VariableDeclarationExpr varDecl, Void arg) { + super.visit(varDecl, arg); + for (VariableDeclarator vd : varDecl.getVariables()) { + declaredInScope.add(vd.getNameAsString()); + } + } + + List getCapturedVariables() { + // Deduplicate by name + Map unique = new LinkedHashMap<>(); + for (CapturedVariable cv : capturedVariables) { + unique.putIfAbsent(cv.getName(), cv); + } + return new ArrayList<>(unique.values()); + } + + /** + * Parses a type description string into a Type object. + */ + private Type parseType(String typeDescription) { + // Handle common primitive types and simple references + return switch (typeDescription) { + case "int" -> PrimitiveType.intType(); + case "long" -> PrimitiveType.longType(); + case "double" -> PrimitiveType.doubleType(); + case "float" -> PrimitiveType.floatType(); + case "boolean" -> PrimitiveType.booleanType(); + case "byte" -> PrimitiveType.byteType(); + case "short" -> PrimitiveType.shortType(); + case "char" -> PrimitiveType.charType(); + case "void" -> new VoidType(); + default -> new ClassOrInterfaceType(null, typeDescription); + }; + } + } +} \ No newline at end of file From 54d0000c89097ed0c53f2c2b607d405d68452ecb Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Mon, 6 Jul 2026 22:19:17 +0200 Subject: [PATCH 4/4] forgot testcases --- .../lambda/FreeVariablesLocatorResource.java | 14 ++++++ .../lambda/RenameVariableResource.java | 14 ++++++ .../transformations/pipeline/lambda/Test.java | 24 ++++++++++ .../pipeline/lambda/TestGeneric.java | 25 ++++++++++ .../pipeline/lambda/TestPredicateInline.java | 48 +++++++++++++++++++ 5 files changed, 125 insertions(+) create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/FreeVariablesLocatorResource.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/RenameVariableResource.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/Test.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/TestGeneric.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/TestPredicateInline.java diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/FreeVariablesLocatorResource.java b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/FreeVariablesLocatorResource.java new file mode 100644 index 00000000000..3efe2a99d78 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/FreeVariablesLocatorResource.java @@ -0,0 +1,14 @@ +class A { + int a; + void test() { + int u = 2; + Function f = (x) -> { + //@ ensures this.a+x != 23; + int n = 2; + return x+u+ this.a; }; + } + + interface Function { + int apply(int x); + } +} \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/RenameVariableResource.java b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/RenameVariableResource.java new file mode 100644 index 00000000000..b0573d952cb --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/RenameVariableResource.java @@ -0,0 +1,14 @@ +class A { + int a; + void test() { + int u = 2; + u++; + Function f = (x) -> { + //@ ensures this.a+x != 23; + return x+u+ this.a; }; + } + + interface Function { + int apply(int x); + } +} \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/Test.java b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/Test.java new file mode 100644 index 00000000000..6d36d8b3888 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/Test.java @@ -0,0 +1,24 @@ +class A { + private final int test; + public A() { + this.test = 1; + } + + void m(int i) { + int outer = 10; + make(a -> { + MyFunctionalInterface g = (x) -> test*2+x; + return test+g.apply(a)*2; + }); + } + + void make(MyFunctionalInterface f) { + f.apply(10); + } + + @java.lang.FunctionalInterface + interface MyFunctionalInterface { + + public int apply(int i); + } +} \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/TestGeneric.java b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/TestGeneric.java new file mode 100644 index 00000000000..c5af6f6b9b9 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/TestGeneric.java @@ -0,0 +1,25 @@ +class A { + private final int test; + public A() { + this.test = 1; + } + + void m(int i) { + int outer = 10; + make(a -> { + MyFunctionalInterface g = (x) -> (test*2+x) > 0; + + return g.apply(a) && a > 2; + }); + } + + void make(MyFunctionalInterface f) { + f.apply(10); + } + + @java.lang.FunctionalInterface + interface MyFunctionalInterface { + + public boolean apply(T i); + } +} \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/TestPredicateInline.java b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/TestPredicateInline.java new file mode 100644 index 00000000000..0c5f81e4b82 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/lambda/TestPredicateInline.java @@ -0,0 +1,48 @@ +import java.util.Objects; + +class A { + private final int test; + public A() { + this.test = 1; + } + + void m(int i) { + int outer = 10; + Predicate tester = (a) -> a > 10; + tester.test(outer); + } + + + @FunctionalInterface + public interface Predicate { + boolean test(T var1); + + default Predicate and(Predicate var1) { + Objects.requireNonNull(var1); + return (var2) -> { + return this.test(var2) && var1.test(var2); + }; + } + + default Predicate negate() { + return (var1) -> { + return !this.test(var1); + }; + } + + default Predicate or(Predicate var1) { + Objects.requireNonNull(var1); + return (var2) -> { + return this.test(var2) || var1.test(var2); + }; + } + + static Predicate isEqual(Object var0) { + return null == var0 ? Objects::isNull : (var1) -> { + return var0.equals(var1); + }; + } + + } + +} \ No newline at end of file