Skip to content

Commit 0742879

Browse files
wadoonwadoon
committed
wip
1 parent 52dbd60 commit 0742879

9 files changed

Lines changed: 137 additions & 54 deletions

File tree

‎key.ncore.java/build.gradle‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,4 +20,10 @@ dependencies {
2020
implementation("org.key-project.proofjava:javaparser-core:$JP_VERSION")
2121
implementation("org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION")
2222
testImplementation("com.google.truth:truth:1.4.5")
23+
}
24+
25+
tasks.register("runGenerator", JavaExec) {
26+
group = "application"
27+
classpath = sourceSets.main.runtimeClasspath
28+
mainClass.set("org.key_project.ncore.java.Generator")
2329
}

‎key.ncore.java/src/adt/java-ast.java‎

Lines changed: 14 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,8 @@
44
import de.uka.ilkd.key.java.ast.PositionInfo;
55
import org.key_project.util.collection.*;
66
import de.uka.ilkd.key.rule.MatchConditions;
7-
7+
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
8+
import org.key_project.logic.op.sv.*;
89

910
@Root
1011
abstract class JavaSourceElement implements Visitable, Matchable {
@@ -179,39 +180,32 @@ class AnnotationUseSpecification extends Modifier {
179180
class ArrayInitializer extends JavaProgramElement {
180181
KeYJavaType kjt;
181182
}
182-
abstract class Expression {}
183183

184184
abstract class ExpressionStatement {}
185185

186-
abstract class Operator extends JavaProgramElement {}
186+
//region expressions
187+
abstract class Expression {
188+
public KeYJavaType getType(Services services) {
189+
return accept(new FindReturnType());
190+
}
191+
}
187192

188-
class ParenthesizedExpression extends Operator {
193+
class ParenthesizedExpression extends Expression{
189194
Expression child;
190195
}
191196

192-
class PassiveExpression extends Operator{
197+
class PassiveExpression extends Expression {
193198
Expression child;
194199
}
195200

196-
abstract class Literal extends JavaProgramElement {
201+
abstract class Literal extends Expression {
197202
String value;
198203
}
199204

200-
abstract class AbstractIntegerLiteral extends Literal {
205+
class BooleanLiteral extends Literal {
201206
}
202207

203-
class BooleanLiteral extends Literal {}
204-
205-
class CharLiteral extends AbstractIntegerLiteral {}
206-
207208
class DoubleLiteral extends Literal {}
208-
209-
class EmptyMapLiteral extends Literal {}
210-
211-
class EmptySeqLiteral extends Literal {}
212-
213-
class EmptySetLiteral extends Literal {}
214-
215209
class FloatLiteral extends Literal {
216210
String value;
217211
}
@@ -397,22 +391,19 @@ class Assert extends JavaStatement {
397391
@Nullable String message;
398392
}
399393

400-
abstract class Branch {}
401-
402394
abstract class BranchStatement extends JavaStatement {}
403395

404396
class Break extends LabelJumpStatement {}
405397

406-
class Case extends Branch {
398+
class Case {
407399
Expression expression;
408400
List<Statement> body;
409401
}
410402

411-
class Default extends Branch {
403+
class Default {
412404
List<Statement> body;
413405
}
414406

415-
416407
abstract class CatchClause {}
417408

418409
class SingleCatch {
@@ -427,11 +418,6 @@ class Continue extends LabelJumpStatement {}
427418

428419
class Do extends LoopStatement {}
429420

430-
class Else extends BranchImp {
431-
432-
Statement body;
433-
}
434-
435421
class EmptyStatement extends JavaProgramElement {}
436422

437423
class EnhancedFor extends LoopStatement {}
@@ -442,11 +428,6 @@ abstract class ExpressionJumpStatement extends JumpStatement {
442428
Expression expression;
443429
}
444430

445-
class Finally extends BranchImp {
446-
447-
StatementBlock body;
448-
}
449-
450431
class For extends LoopStatement {}
451432

452433
class ForUpdates extends JavaProgramElement {
@@ -526,8 +507,6 @@ class SynchronizedBlock extends JavaStatement {
526507
StatementBlock body;
527508
}
528509

529-
class Then extends BranchImp {}
530-
531510
class Throw extends ExpressionJumpStatement {}
532511

533512
class TransactionStatement extends JavaStatement {}

‎key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java‎

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -56,16 +56,22 @@ public Generator() {
5656
addStep(NodeSteps::addAllFieldsConstructor);
5757
addStep(NodeSteps::addAllWoOptFieldsConstructor);
5858
addStep(NodeSteps::addCopyConstructor);
59-
addStep(NodeSteps::addEquals);
60-
addStep(NodeSteps::ToString);
61-
addStep(NodeSteps::addHashCode);
6259
addStep(NodeSteps::addMatch);
6360
addStep(NodeSteps::addWiths);
6461
addStep(NodeSteps::addBuilder);
65-
addStep(NodeSteps::addOverrideConstructor);
66-
addStep(NodeSteps::addOverrideConstructor2);
62+
63+
// weigl: this block adds the processing of
64+
// PROPERTY_* accessors and Node -> Map construction
65+
//addStep(NodeSteps::addOverrideConstructor);
66+
//addStep(NodeSteps::addOverrideConstructor2);
6767
//addStep(NodeSteps::addGetProperties);
68-
addStep(NodeSteps::processFieldsAccessor);
68+
//addStep(NodeSteps::processFieldsAccessor);
69+
70+
addStep(NodeSteps::addEquals);
71+
addStep(NodeSteps::ToString);
72+
addStep(NodeSteps::addHashCode);
73+
74+
addStep(NodeSteps::handleRoot);
6975

7076
postSteps.add(PostSteps::createVisitor);
7177
postSteps.add(PostSteps::createArgVisitor);

‎key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java‎

Lines changed: 45 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@
1111
import com.github.javaparser.ast.nodeTypes.NodeWithName;
1212
import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName;
1313
import com.github.javaparser.ast.stmt.BlockStmt;
14+
import com.github.javaparser.ast.stmt.ExpressionStmt;
15+
import com.github.javaparser.ast.stmt.IfStmt;
1416
import com.github.javaparser.ast.stmt.ReturnStmt;
1517
import com.github.javaparser.ast.type.ClassOrInterfaceType;
1618
import com.github.javaparser.ast.type.PrimitiveType;
@@ -130,6 +132,12 @@ static void addHashCode(ClassOrInterfaceDeclaration target) {
130132
return;
131133
}
132134

135+
FieldDeclaration field = target.addField(Integer.class, "hashCode", PRIVATE);
136+
final var variable = field.getVariables().getFirst();
137+
field.addAnnotation("EqEx");
138+
field.addAnnotation("Nullable");
139+
field.addAnnotation("Internal");
140+
133141
MethodDeclaration hashCode = target.addMethod("hashCode", PUBLIC);
134142
//hashCode.addModifier(FINAL);
135143
hashCode.addAnnotation(Override.class);
@@ -144,9 +152,14 @@ static void addHashCode(ClassOrInterfaceDeclaration target) {
144152

145153
if (args.length == 0)
146154
assert false : "No defined fields";
147-
else
148-
hashCode.getBody().get().addStatement(new ReturnStmt(
149-
callObjects("hash", args)));
155+
else {
156+
final Expression compute = callObjects("hash", args);
157+
final Expression hashCodeIsNull = new BinaryExpr(variable.getNameAsExpression(), new NullLiteralExpr(), BinaryExpr.Operator.EQUALS);
158+
final var setHashCode = new ExpressionStmt(new AssignExpr(variable.getNameAsExpression(), compute, AssignExpr.Operator.ASSIGN));
159+
hashCode.getBody().get().addStatement(
160+
new IfStmt(hashCodeIsNull, setHashCode, null));
161+
hashCode.getBody().get().addStatement(new ReturnStmt(variable.getNameAsExpression()));
162+
}
150163
}
151164

152165
static void ToString(ClassOrInterfaceDeclaration clazz) {
@@ -170,6 +183,32 @@ static void ToString(ClassOrInterfaceDeclaration clazz) {
170183
new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args))));
171184
}
172185

186+
static void handleRoot(ClassOrInterfaceDeclaration clazz) {
187+
if (isRoot(clazz)) {
188+
clazz.setInterface(false);
189+
clazz.addModifier(PUBLIC, ABSTRACT);
190+
clazz.getExtendedTypes().clear();
191+
192+
for (var field : clazz.getMethods()) {
193+
field.addModifier(PUBLIC, ABSTRACT);
194+
}
195+
} else if(isNonTerminal(clazz)) {
196+
197+
}
198+
}
199+
200+
static boolean isRoot(ClassOrInterfaceDeclaration clazz) {
201+
return clazz.getAnnotationByName("Root").isPresent();
202+
}
203+
204+
static boolean isNonTerminal(ClassOrInterfaceDeclaration clazz) {
205+
return isRoot(clazz) || clazz.isInterface();
206+
}
207+
208+
static boolean isTerminal(ClassOrInterfaceDeclaration clazz) {
209+
return !isNonTerminal(clazz);
210+
}
211+
173212
private static Expression callObjects(String method, Expression... args) {
174213
return new MethodCallExpr(new NameExpr("Objects"), method, new NodeList<>(args));
175214
}
@@ -390,6 +429,8 @@ static void setPackage(ClassOrInterfaceDeclaration target) {
390429
for (var s : permittedTypes.get(target.getNameAsString())) {
391430
target.getPermittedTypes().add(new ClassOrInterfaceType(null, s));
392431
}
432+
//target.setExtendedTypes(new NodeList<>());
433+
target.getMethods().forEach(it -> it.addModifier(DEFAULT));
393434
} else {
394435
target.addModifier(FINAL);
395436
target.setImplementedTypes(target.getExtendedTypes());
@@ -549,7 +590,7 @@ private static boolean isList(VariableDeclarator type) {
549590
}
550591

551592
public static void enforceHierarchy(ClassOrInterfaceDeclaration decl) {
552-
if (decl.getExtendedTypes().isEmpty()) {
593+
if (isTerminal(decl)) {
553594
decl.addExtendedType("JavaSourceElement");
554595
}
555596
}

‎key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@
2323

2424
import static com.github.javaparser.ast.Modifier.DefaultKeyword.*;
2525
import static org.key_project.ncore.java.Generator.ROOT;
26+
import static org.key_project.ncore.java.NodeSteps.isNonTerminal;
27+
import static org.key_project.ncore.java.NodeSteps.isRoot;
2628

2729
public class PostSteps {
2830
public static void createVisitor(List<CompilationUnit> nodeUnits, SourceRoot sourceRoot) {
@@ -38,7 +40,7 @@ public static void createVisitor(List<CompilationUnit> nodeUnits, SourceRoot sou
3840
var t = clazz.getPrimaryType().get();
3941
if (!(t instanceof ClassOrInterfaceDeclaration c))
4042
continue;
41-
if (c.isInterface())
43+
if (isNonTerminal(c))
4244
continue;
4345

4446
var m = type.addMethod("visit");
@@ -90,7 +92,7 @@ public static void createVoidVisitor(List<CompilationUnit> nodeUnits, SourceRoot
9092
var t = clazz.getPrimaryType().get();
9193
if (!(t instanceof ClassOrInterfaceDeclaration c))
9294
continue;
93-
if (c.isInterface())
95+
if (isNonTerminal(c))
9496
continue;
9597

9698
var m = type.addMethod("visit");
@@ -126,7 +128,7 @@ public static void createTraversalVisitor(List<CompilationUnit> nodeUnits,
126128

127129
if (!(t instanceof ClassOrInterfaceDeclaration c))
128130
continue;
129-
if (c.isInterface())
131+
if (NodeSteps.isNonTerminal(c))
130132
continue;
131133

132134
var m = type.addMethod("visit", PUBLIC);
@@ -166,7 +168,7 @@ public static void createTraversalCopyOnDemandVisitor(List<CompilationUnit> node
166168

167169
if (!(t instanceof ClassOrInterfaceDeclaration c))
168170
continue;
169-
if (c.isInterface())
171+
if (isNonTerminal(c))
170172
continue;
171173

172174
var m = type.addMethod("visit", PUBLIC);
@@ -299,8 +301,9 @@ public static void createArgVisitor(List<CompilationUnit> nodeUnits, SourceRoot
299301
var t = clazz.getPrimaryType().get();
300302
if (!(t instanceof ClassOrInterfaceDeclaration c))
301303
continue;
302-
if (c.isInterface())
304+
if (isNonTerminal(c)) {
303305
continue;
306+
}
304307

305308
cu.addImport(t.getFullyQualifiedName().get());
306309

‎key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java‎

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
import java.util.TreeMap;
1616

1717
import static com.github.javaparser.ast.Modifier.DefaultKeyword.ABSTRACT;
18+
import static org.key_project.ncore.java.NodeSteps.isRoot;
1819

1920
public class PreSteps {
2021
final static class PreComputation implements PreStep {
@@ -23,16 +24,28 @@ final static class PreComputation implements PreStep {
2324
Multimap<String, String> permittedTypes =
2425
MultimapBuilder.treeKeys().treeSetValues().build();
2526

27+
ClassOrInterfaceDeclaration root;
28+
2629
@Override
2730
public void applyOn(NodeList<TypeDeclaration<?>> types) {
2831
TreeMap<String, ClassOrInterfaceDeclaration> fields = new TreeMap<>();
32+
this.root = (ClassOrInterfaceDeclaration) types.stream()
33+
.filter(decl -> decl instanceof ClassOrInterfaceDeclaration clazz
34+
&& isRoot(clazz))
35+
.findFirst().get();
2936

3037
for (TypeDeclaration<?> decl : types) {
31-
fields.put(decl.getNameAsString(), (ClassOrInterfaceDeclaration) decl);
38+
if (decl instanceof ClassOrInterfaceDeclaration clazz) {
39+
if (isRoot(clazz)) {
40+
this.root = clazz;
41+
}
42+
fields.put(decl.getNameAsString(), clazz);
3243

33-
var zuper = ((ClassOrInterfaceDeclaration) decl).getExtendedTypes().getOFirst()
34-
.map(NodeWithSimpleName::getNameAsString);
35-
zuper.ifPresent(s -> inheritanceMap.put(decl.getNameAsString(), s));
44+
inheritanceMap.put(decl.getNameAsString(), this.root.getNameAsString());
45+
var zuper =
46+
clazz.getExtendedTypes().getOFirst().map(NodeWithSimpleName::getNameAsString);
47+
zuper.ifPresent(s -> inheritanceMap.put(decl.getNameAsString(), s));
48+
}
3649
}
3750

3851
// compute transitive closure of inheritance

‎key.ncore.java/src/main/java/org/key_project/java/ast/Internal.java‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
package org.key_project.java.ast;
2+
3+
/**
4+
* This annotation marks fields and methods that are added for internal purposes,
5+
* and should not be exposed.
6+
* It is used in the code generation to avoid processing of fields or methods.
7+
*
8+
* @author Alexander Weigl
9+
* @version 1 (17.05.26)
10+
*/
11+
public @interface Internal {
12+
}

‎key.ncore.java/src/main/java/org/key_project/java/ast/MatchHelper.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package org.key_project.java.ast;
22

3+
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
34
import de.uka.ilkd.key.rule.MatchConditions;
45
import org.jspecify.annotations.Nullable;
56
import org.key_project.util.collection.RoList;
@@ -50,4 +51,8 @@ public class MatchHelper {
5051
public static MatchConditions match(boolean b1, boolean b2, MatchConditions cond) {
5152
return b1 == b2 ? cond : null;
5253
}
54+
55+
public static MatchConditions match(KeYJavaType a, KeYJavaType b, MatchConditions cond) {
56+
return Objects.equals(a, b) ? cond : null;
57+
}
5358
}

‎key.ncore.java/src/main/java/org/key_project/java/ast/MatchOrder.java‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package org.key_project.java.ast;
2+
3+
import java.lang.annotation.ElementType;
4+
import java.lang.annotation.Retention;
5+
import java.lang.annotation.RetentionPolicy;
6+
import java.lang.annotation.Target;
7+
8+
/**
9+
* This annotation allows you to define the order of matches calls on fields.
10+
*
11+
* @author Alexander Weigl
12+
* @version 1 (17.05.26)
13+
*/
14+
@Retention(RetentionPolicy.SOURCE)
15+
@Target(ElementType.FIELD)
16+
public @interface MatchOrder {
17+
int value() default 0;
18+
}

0 commit comments

Comments
 (0)