Skip to content

Commit 82e376d

Browse files
wadoonwadoon
committed
Csiky @csicar Lambda to Plain Java transformation
# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TransformationPipelineServices.java
1 parent f1ee30a commit 82e376d

3 files changed

Lines changed: 196 additions & 3 deletions

File tree

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ public static KeYJavaPipeline createDefault(TransformationPipelineServices pipel
4040
KeYJavaPipeline p = new KeYJavaPipeline(pipelineServices);
4141
p.add(new EnumClassBuilder(pipelineServices));
4242
p.add(new JMLTransformer(pipelineServices));
43+
p.add(new LambdaReplacer(pipelineServices));
4344
p.add(new JmlDocRemoval(pipelineServices));
4445
p.add(new ImplicitFieldAdder(pipelineServices));
4546
p.add(new InstanceAllocationMethodBuilder(pipelineServices));

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

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,162 @@
1+
package de.uka.ilkd.key.java.transformations.pipeline;
2+
3+
import com.github.javaparser.ast.Node;
4+
import com.github.javaparser.ast.NodeList;
5+
import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
6+
import com.github.javaparser.ast.body.MethodDeclaration;
7+
import com.github.javaparser.ast.body.TypeDeclaration;
8+
import com.github.javaparser.ast.expr.LambdaExpr;
9+
import com.github.javaparser.ast.expr.ObjectCreationExpr;
10+
import com.github.javaparser.ast.stmt.BlockStmt;
11+
import com.github.javaparser.ast.stmt.ExpressionStmt;
12+
import com.github.javaparser.ast.stmt.Statement;
13+
import com.github.javaparser.ast.type.ClassOrInterfaceType;
14+
import com.github.javaparser.utils.Pair;
15+
import org.jspecify.annotations.NonNull;
16+
17+
import java.util.Optional;
18+
19+
/**
20+
* Replaces lambda expressions by an internal named class.
21+
* <p>
22+
* Code was donated by Carsten Czisky @ciskar
23+
*/
24+
public class LambdaReplacer extends JavaTransformer {
25+
26+
/**
27+
* creates a transformer for the recoder model
28+
*
29+
* @param services the CrossReferenceServiceConfiguration to access
30+
* model information
31+
*/
32+
public LambdaReplacer(@NonNull TransformationPipelineServices services) {
33+
super(services);
34+
}
35+
36+
@Override
37+
public void apply(TypeDeclaration<?> td) {
38+
td.walk(LambdaExpr.class, this::rewriteLambda);
39+
}
40+
41+
private void rewriteLambda(LambdaExpr expr) {
42+
@SuppressWarnings({"rawtypes", "unchecked"})
43+
Optional<TypeDeclaration> enclosingType = expr.findAncestor(TypeDeclaration.class);
44+
45+
if (enclosingType.isEmpty()) {
46+
throw new IllegalStateException("LambdaExpr is not enclosed in a type declaration");
47+
}
48+
49+
ClassOrInterfaceDeclaration decl = liftToInnerClass(expr);
50+
enclosingType.get().addMember(decl);
51+
52+
var objectCreation = instantiate(decl);
53+
expr.replace(objectCreation);
54+
}
55+
56+
private ObjectCreationExpr instantiate(ClassOrInterfaceDeclaration decl) {
57+
ClassOrInterfaceType type = new ClassOrInterfaceType(null, decl.getNameAsString());
58+
return new ObjectCreationExpr(null, type, new NodeList<>());
59+
}
60+
61+
private ClassOrInterfaceDeclaration liftToInnerClass(LambdaExpr lambdaExpr) {
62+
Pair<String, MethodDeclaration> sai = findSingleAbstractInterface(lambdaExpr);
63+
String interfaceName = sai.a;
64+
MethodDeclaration method = sai.b;
65+
66+
String name = services.getFreshName("__GENERATED_",
67+
lambdaExpr.getRange().map(r -> r.begin).orElse(null));
68+
69+
ClassOrInterfaceDeclaration it =
70+
new ClassOrInterfaceDeclaration(new NodeList<>(), false, name);
71+
72+
it.addImplementedType(interfaceName);
73+
it.addMember(method);
74+
75+
return it;
76+
}
77+
78+
private Pair<String, MethodDeclaration> findSingleAbstractInterface(LambdaExpr lambdaExpr) {
79+
ClassOrInterfaceType type = assignToType(lambdaExpr);
80+
81+
if (type == null) {
82+
return inferDefaultAbstractInterface(lambdaExpr);
83+
} else {
84+
return new Pair<>(type.getNameAsString(), new MethodDeclaration());
85+
}
86+
}
87+
88+
private Pair<String, MethodDeclaration> inferDefaultAbstractInterface(LambdaExpr lambdaExpr) {
89+
String interfaze;
90+
MethodDeclaration md = new MethodDeclaration();
91+
92+
Node body = lambdaExpr.getBody();
93+
String returnType = null;
94+
95+
if (body instanceof BlockStmt block) {
96+
Statement last = block.getStatements().isEmpty()
97+
? null
98+
: block.getStatements().getLast();
99+
100+
if (last != null && last.isReturnStmt()) {
101+
returnType = last.asReturnStmt()
102+
.getExpression()
103+
.map(e -> e.calculateResolvedType().toString())
104+
.orElse(null);
105+
}
106+
}
107+
108+
if (body instanceof ExpressionStmt es) {
109+
returnType = es.getExpression().calculateResolvedType().toString();
110+
}
111+
112+
int paramCount = lambdaExpr.getParameters().size();
113+
114+
switch (paramCount) {
115+
case 0:
116+
if (returnType == null) {
117+
interfaze = "Runnable";
118+
md.setName("run");
119+
} else {
120+
interfaze = "java.util.function.Supplier<" + returnType + ">";
121+
md.setName("accept");
122+
}
123+
break;
124+
125+
case 1:
126+
String firstParam = lambdaExpr.getParameter(0).getTypeAsString();
127+
if (returnType == null) {
128+
interfaze = "java.util.function.Consumer<" + firstParam + ">";
129+
md.setName("get");
130+
} else {
131+
interfaze = "java.util.function.Function<" + firstParam + ", " + returnType + ">";
132+
md.setName("invoke");
133+
}
134+
break;
135+
136+
case 2:
137+
String p1 = lambdaExpr.getParameter(0).getTypeAsString();
138+
String p2 = lambdaExpr.getParameter(1).getTypeAsString();
139+
if (returnType == null) {
140+
interfaze = "java.util.function.BiConsumer<" + p1 + "," + p2 + ">";
141+
md.setName("get");
142+
} else {
143+
interfaze = "java.util.function.BiFunction<" + p1 + ", " + p2 + ", " + returnType + ">";
144+
md.setName("invoke");
145+
}
146+
break;
147+
148+
default:
149+
throw new IllegalStateException("ASM could not be inferred");
150+
}
151+
152+
lambdaExpr.getParameters().forEach(p -> md.addParameter(p.clone()));
153+
154+
return new Pair<>(interfaze, md);
155+
}
156+
157+
private ClassOrInterfaceType assignToType(LambdaExpr lambdaExpr) {
158+
var type = lambdaExpr.calculateResolvedType();
159+
System.out.println("TEST: " + type);
160+
return null; // TODO
161+
}
162+
}

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

Lines changed: 33 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,10 @@
66
import java.util.*;
77
import java.util.stream.Collectors;
88

9+
import com.github.javaparser.Position;
910
import de.uka.ilkd.key.java.loader.JavaParserFactory;
1011
import de.uka.ilkd.key.java.transformations.ConstantExpressionEvaluator;
1112
import de.uka.ilkd.key.java.transformations.EvaluationException;
12-
import de.uka.ilkd.key.speclang.PositionedString;
13-
14-
import org.key_project.util.collection.ImmutableList;
1513

1614
import com.github.javaparser.JavaParser;
1715
import com.github.javaparser.ast.CompilationUnit;
@@ -28,8 +26,11 @@
2826
import com.github.javaparser.resolution.model.SymbolReference;
2927
import com.github.javaparser.resolution.types.ResolvedReferenceType;
3028
import com.github.javaparser.resolution.types.ResolvedType;
29+
import de.uka.ilkd.key.speclang.PositionedString;
30+
import org.jspecify.annotations.NonNull;
3131
import org.jspecify.annotations.NullMarked;
3232
import org.jspecify.annotations.Nullable;
33+
import org.key_project.util.collection.ImmutableList;
3334
import org.slf4j.Logger;
3435
import org.slf4j.LoggerFactory;
3536

@@ -447,4 +448,33 @@ private static boolean isInside(Node container, Node declaration) {
447448
container.containsWithinRange(declaration);
448449
}
449450
}
451+
452+
453+
/**
454+
* Generates unique names for generated inner classes.
455+
*/
456+
class NameGenerator {
457+
458+
private final Set<String> generatedNames = new HashSet<>();
459+
460+
public String generate(String prefix, Position pos) {
461+
return generate(prefix, pos, null);
462+
}
463+
464+
private String generate(String prefix, Position pos, Integer counter) {
465+
Integer line = pos != null ? pos.line : null;
466+
467+
String newName = prefix + "L" + line;
468+
if (counter != null) {
469+
newName += "_" + counter;
470+
}
471+
472+
if (generatedNames.contains(newName)) {
473+
return generate(prefix, pos, counter == null ? 0 : counter + 1);
474+
}
475+
476+
generatedNames.add(newName);
477+
return newName;
478+
}
479+
}
450480
}

0 commit comments

Comments
 (0)