Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@wadoon
wadoon committed Jan 25, 2025
1 parent df80f5d commit c485dce
Show file tree
Hide file tree
Showing 9 changed files with 74 additions and 88 deletions.
10 changes: 1 addition & 9 deletions key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ public class JavaService {
public JavaService(Services services, @NonNull Path bootClassPath,
@NonNull Collection<Path> libraryPath) {
this.services = services;
this.mapping = new KeYJPMapping();
this.mapping = new KeYJPMapping(this);
this.bootClassPath = bootClassPath;
this.libraryPath = libraryPath;
programFactory = new JavaParserFactory(services);
Expand Down Expand Up @@ -523,14 +523,6 @@ private void parseBootClasspath(FileRepo fileRepo) throws IOException {
LOGGER.debug("Parsing internal classes from {}", bootClassPath);
var bootClasses = parseBootClasses(fileRepo);

/*
* var defaultCu = unwrapParseResult(programFactory.parseCompilationUnit(
* new StringReader("public class " + JavaInfo.DEFAULT_EXECUTION_CONTEXT_CLASS +
* " { public static void " + JavaInfo.DEFAULT_EXECUTION_CONTEXT_METHOD
* + "() {} }")));
* bootClasses.add(defaultCu);
*/

programFactory.setBootClasses(bootClasses);
LOGGER.debug("Finished parsing internal classes");

Expand Down
35 changes: 24 additions & 11 deletions key.core/src/main/java/de/uka/ilkd/key/java/KeYJPMapping.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@

import java.util.*;

import com.github.javaparser.resolution.declarations.AssociableToAST;
import de.uka.ilkd.key.java.ast.ProgramElement;
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
import de.uka.ilkd.key.util.Debug;
Expand Down Expand Up @@ -59,8 +60,11 @@ public class KeYJPMapping {

private final Set<String> packageNames;

private final JavaService converter;

public KeYJPMapping(JavaService converter) {
this.converter = converter;

public KeYJPMapping() {
this.map = new IdentityHashMap<>(4096);
this.revMap = new IdentityHashMap<>(4096);
this.typeMap = new LinkedHashMap<>(4096);
Expand All @@ -73,8 +77,7 @@ public KeYJPMapping() {
* creates a KeYRecoderMapping object.
* Used for cloning and testing.
*
* @param o
* what to clone
* @param o what to clone
*/
KeYJPMapping(KeYJPMapping o) {
this.map = new IdentityHashMap<>(o.map);
Expand All @@ -85,17 +88,28 @@ public KeYJPMapping() {
this.superArrayType = o.superArrayType;
this.parsedSpecial = o.parsedSpecial;
this.parsingLibraries = o.parsingLibraries;
this.converter = o.converter;
}

/**
* returns a matching ModelElement (KeY) to a given recoder.ModelElement
*
* @param pe
* a recoder.ModelElement
* @param pe a recoder.ModelElement
*/
@Nullable
public KeYJavaType resolvedTypeToKeY(ResolvedType pe) {
return typeMap.get(pe);
var type = typeMap.get(pe);
if (type != null && type.getJavaType() == null && pe.isReferenceType()) {
try {
pe.asReferenceType()
.getTypeDeclaration()
.flatMap(AssociableToAST::toAst)
.ifPresent(converter.getConverter(null)::process);
} catch (ClassCastException e) {
// This class does not exist
}
}
return type;
}

public ResolvedType resolveType(KeYJavaType pe) {
Expand Down Expand Up @@ -125,7 +139,7 @@ public void put(Node node, ProgramElement value) {
var formerNode = revMap.putIfAbsent(value, node);
if (formerValue != null && formerValue != value)
LOGGER.error("Duplicate registration of value: {}, formerValue: {}", value,
formerValue);
formerValue);
if (formerNode != null && formerNode != node)
LOGGER.error("Duplicate registration of node: {}, formerNode: {}", node, formerNode);
}
Expand All @@ -137,7 +151,7 @@ public void put(ResolvedType rec, KeYJavaType key) {
var formerType = typeMapRev.putIfAbsent(key, rec);
if (formerType != null && !Objects.equals(rec, formerType))
LOGGER.error("Duplicate registration of resolved type: {}, former: {}", rec,
formerType);
formerType);
}

public boolean mapped(Node rec) {
Expand Down Expand Up @@ -209,9 +223,8 @@ public int size() {
* this method sets a flag whether the special have been parsed in or
* not
*
* @param b
* boolean indicating if the special classes have been
* parsed in
* @param b boolean indicating if the special classes have been
* parsed in
*/
public void setParsedSpecial(boolean b) {
parsedSpecial = b;
Expand Down
15 changes: 7 additions & 8 deletions key.core/src/main/java/de/uka/ilkd/key/java/Services.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -293,14 +293,15 @@ public Services copyPreservesLDTInformation() {
* copy the {@link InitConfig} via {@link InitConfig#deepCopy()} or one of the other copy
* methods first.
*
* @param p_proof the Proof to which this {@link Services} instance belongs
* @param proof
* the Proof to which this {@link Services} instance belongs
*/
public void setProof(Proof p_proof) {
public void setProof(Proof proof) {
if (this.proof != null) {
throw new IllegalStateException(
"Services are already owned by another proof:" + proof.name());
"Services are already owned by another proof:" + this.proof.name());
}
proof = p_proof;
this.proof = proof;
}


Expand Down Expand Up @@ -483,8 +484,7 @@ public JavaService getJavaService() {
return javaService;
}

private JavaService activateJavaPath(@NonNull Path bootClassPath,
@NonNull Collection<Path> libraryPaths) {
private JavaService activateJavaPath(@NonNull Path bootClassPath, @NonNull Collection<Path> libraryPaths) {
if (javaService != null && javaService.getBootClassPath().equals(bootClassPath)
&& CollectionUtil.containsSame(javaService.getLibraryPath(), libraryPaths)) {
return javaService;
Expand All @@ -495,8 +495,7 @@ private JavaService activateJavaPath(@NonNull Path bootClassPath,
return javaService;
}

public JavaService activateJava(@Nullable Path bootClassPath,
@Nullable Collection<Path> libraryPaths) {
public JavaService activateJava(@Nullable Path bootClassPath, @NonNull Collection<Path> libraryPaths) {
Path path;
if (bootClassPath != null) {
path = bootClassPath;
Expand Down
12 changes: 6 additions & 6 deletions key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/KeYJavaType.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,27 +44,27 @@ public KeYJavaType(Type javaType, Sort sort) {

/** creates a new KeYJavaType */
public KeYJavaType(Sort sort) {
this.sort = sort;
setSort(Objects.requireNonNull(sort));
}

/** creates a new KeYJavaType */
public KeYJavaType(Type type) {
this.javaType = type;
setJavaType(Objects.requireNonNull(type));
}

public void setJavaType(Type type) {
public void setJavaType(@Nullable Type type) {
javaType = type;
}

public void setSort(Sort s) {
public void setSort(@Nullable Sort s) {
sort = s;
}

public Type getJavaType() {
public @Nullable Type getJavaType() {
return javaType;
}

public Sort getSort() {
public @Nullable Sort getSort() {
return sort;
}

Expand Down
63 changes: 26 additions & 37 deletions key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYTypeConverter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,8 +107,7 @@ private void storeInCache(ResolvedType t, KeYJavaType kjt) {
* This method retrieves the recoder nameinfo and queries it for the type for typeName and
* passes this result to {@link #getKeYJavaType(ResolvedType)}
*
* @param typeName
* name of a type to be converted
* @param typeName name of a type to be converted
* @return the KJT for the string representation.
* @author mu
* @see #getKeYJavaType(ResolvedType)
Expand All @@ -123,13 +122,10 @@ public KeYJavaType getKeYJavaType(String typeName) {
* <p>
* Returned the cached value if present - otherwise create a new type.
*
* @param type
* type to be converted, may be null
* @param type type to be converted, may be null
* @return a keytype.
*/
@NonNull
public KeYJavaType getKeYJavaType(ResolvedType type) {
// change from 2012-02-07: there must be a definite KJT
public @NonNull KeYJavaType getKeYJavaType(ResolvedType type) {
if (type == null) {
throw new NullPointerException("null cannot be converted into a KJT");
}
Expand Down Expand Up @@ -199,7 +195,7 @@ private void addArrayType(ResolvedArrayType type) {
// I may not use JavaInfo here because the classes may not yet be cached!
Type elemType = kjt.getJavaType();
var arraySort = ArraySort.getArraySort(kjt.getSort(), elemType, getObjectType().getSort(),
getCloneableType().getSort(), getSerializableType().getSort());
getCloneableType().getSort(), getSerializableType().getSort());
var result = new KeYJavaType(arraySort);
if (getSortsNamespace().lookup(arraySort.name()) == null) {
getSortsNamespace().add(arraySort);
Expand Down Expand Up @@ -249,6 +245,7 @@ private void addReferenceType(ResolvedReferenceType type) {
if (getSortsNamespace().lookup(sort.name()) == null) {
getSortsNamespace().add(sort);
}

// Important: javaType is null until being set by visiting the class/interface/enum
// declaration!
storeInCache(type, new KeYJavaType(sort));
Expand All @@ -266,8 +263,7 @@ private void addReferenceType(ResolvedReferenceType type) {
/**
* get all direct super sorts of a class type (not transitive)
*
* @param classType
* type to examine, not null
* @param classType type to examine, not null
* @return a freshly created set of sorts
*/
private ImmutableSet<Sort> directSuperSorts(ResolvedReferenceTypeDeclaration classType) {
Expand All @@ -285,10 +281,8 @@ private ImmutableSet<Sort> directSuperSorts(ResolvedReferenceTypeDeclaration cla
/**
* create a sort out of a recoder class
*
* @param ct
* classtype to create for, not null
* @param supers
* the set of (direct?) super-sorts
* @param ct classtype to create for, not null
* @param supers the set of (direct?) super-sorts
* @return a freshly created Sort object
*/
private Sort createObjectSort(ResolvedTypeDeclaration ct, ImmutableSet<Sort> supers) {
Expand Down Expand Up @@ -335,13 +329,13 @@ private ArrayDeclaration createArrayType(KeYJavaType baseType, KeYJavaType array
baseTypeRef = new TypeRef(baseType);
} else {
baseTypeRef = new TypeRef(new ProgramElementName(baseType.getSort().name().toString()),
0, null, baseType);
0, null, baseType);
}

ExtList members = new ExtList();
members.add(baseTypeRef);
addImplicitArrayMembers(members, arrayType, baseType,
(ProgramVariable) length.getFieldSpecifications().get(0).getProgramVariable());
(ProgramVariable) length.getFieldSpecifications().get(0).getProgramVariable());

return new ArrayDeclaration(members, baseTypeRef, sat);
}
Expand All @@ -357,32 +351,29 @@ private KeYJavaType createSuperArrayType() {

var superArrayType = new KeYJavaType();
var specLength =
new FieldSpecification(new LocationVariable(new ProgramElementName("length"),
integerType, superArrayType, false, false, false, true));
var f = new FieldDeclaration(new Modifier[] { new Public(), new Final() },
new TypeRef(integerType), new FieldSpecification[] { specLength }, false);
new FieldSpecification(new LocationVariable(new ProgramElementName("length"),
integerType, superArrayType, false, false, false, true));
var f = new FieldDeclaration(new Modifier[]{new Public(), new Final()},
new TypeRef(integerType), new FieldSpecification[]{specLength}, false);
superArrayType.setJavaType(new SuperArrayDeclaration(f));
return superArrayType;
}

/**
* Adds several implicit fields and methods to given list of members.
*
* @param members
* an ExtList with the members of parent
* @param parent
* the KeYJavaType of the array to be enriched by its implicit members
* @param baseType
* the KeYJavaType of the parent's element type
* @param members an ExtList with the members of parent
* @param parent the KeYJavaType of the array to be enriched by its implicit members
* @param baseType the KeYJavaType of the parent's element type
*/
private void addImplicitArrayMembers(ExtList members, KeYJavaType parent, KeYJavaType baseType,
ProgramVariable len) {
ProgramVariable len) {

Type base = baseType.getJavaType();
int dimension = base instanceof ArrayType ? ((ArrayType) base).getDimension() + 1 : 1;
TypeRef parentReference =
new TypeRef(new ProgramElementName(String.valueOf(parent.getSort().name())),
dimension, null, parent);
new TypeRef(new ProgramElementName(String.valueOf(parent.getSort().name())),
dimension, null, parent);

// add methods
// the only situation where base can be null is in case of a
Expand All @@ -398,7 +389,7 @@ private void addImplicitArrayMembers(ExtList members, KeYJavaType parent, KeYJav
}

final IProgramMethod prepare =
arrayMethodBuilder.getPrepareArrayMethod(parentReference, length, defaultValue, fields);
arrayMethodBuilder.getPrepareArrayMethod(parentReference, length, defaultValue, fields);

members.add(arrayMethodBuilder.getArrayInstanceAllocatorMethod(parentReference));
members.add(prepare);
Expand All @@ -409,10 +400,9 @@ private void addImplicitArrayMembers(ExtList members, KeYJavaType parent, KeYJav
/**
* extracts all fields out of fielddeclaration
*
* @param field
* the FieldDeclaration of which the field specifications have to be extracted
* @param field the FieldDeclaration of which the field specifications have to be extracted
* @return a IList<Field> the includes all field specifications found int the field declaration
* of the given list
* of the given list
*/
private ImmutableList<Field> filterField(FieldDeclaration field) {
ImmutableList<Field> result = ImmutableSLList.nil();
Expand All @@ -427,10 +417,9 @@ private ImmutableList<Field> filterField(FieldDeclaration field) {
* extracts all field specifications out of the given list. Therefore it descends into field
* declarations.
*
* @param list
* the ExtList with the members of a type declaration
* @param list the ExtList with the members of a type declaration
* @return a IList<Field> the includes all field specifications found int the field declaration
* of the given list
* of the given list
*/
private ImmutableList<Field> filterField(ExtList list) {
ImmutableList<Field> result = ImmutableSLList.nil();
Expand All @@ -449,6 +438,6 @@ private void initArrayMethodBuilder() {
Sort heapSort = heapLDT == null ? JavaDLTheory.ANY : heapLDT.targetSort();
int heapCount = (heapLDT == null) ? 1 : (heapLDT.getAllHeaps().size() - 1);
arrayMethodBuilder =
new CreateArrayMethodBuilder(integerType, getObjectType(), heapSort, heapCount);
new CreateArrayMethodBuilder(integerType, getObjectType(), heapSort, heapCount);
}
}
Loading

0 comments on commit c485dce

Please sign in to comment.