Skip to content

Commit

Permalink
KeYProgModelInfo#getConstructor implemented
Browse files Browse the repository at this point in the history
  • Loading branch information
@wadoon
wadoon committed Jul 22, 2023
1 parent 150a51c commit 3da3422
Show file tree
Hide file tree
Showing 6 changed files with 153 additions and 120 deletions.
37 changes: 20 additions & 17 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
@@ -1,19 +1,18 @@
package de.uka.ilkd.key.java;

import java.util.*;
import javax.annotation.Nonnull;
import javax.annotation.Nullable;

import de.uka.ilkd.key.java.ast.ProgramElement;
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
import de.uka.ilkd.key.util.Debug;

import com.github.javaparser.ast.Node;
import com.github.javaparser.resolution.declarations.ResolvedDeclaration;
import com.github.javaparser.resolution.types.ResolvedType;
import de.uka.ilkd.key.java.ast.ProgramElement;
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
import de.uka.ilkd.key.util.Debug;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import javax.annotation.Nonnull;
import javax.annotation.Nullable;
import java.util.*;

/**
* @author Alexander Weigl
* @version 1 (05.03.22)
Expand Down Expand Up @@ -88,8 +87,9 @@ public KeYJPMapping() {
*
* @param pe a recoder.ModelElement
*/
public Optional<KeYJavaType> resolvedTypeToKeY(ResolvedType pe) {
return Optional.ofNullable(typeMap.get(pe));
@Nullable
public KeYJavaType resolvedTypeToKeY(ResolvedType pe) {
return typeMap.get(pe);
}

public ResolvedType resolveType(KeYJavaType pe) {
Expand All @@ -98,12 +98,15 @@ public ResolvedType resolveType(KeYJavaType pe) {
return res;
}

public Optional<ProgramElement> nodeToKeY(Node rm) {
return Optional.ofNullable(map.get(rm));
@Nullable
public ProgramElement nodeToKeY(Node rm) {
return map.get(rm);
}

public Optional<ProgramElement> resolvedDeclarationToKeY(ResolvedDeclaration rm) {
return rm.toAst().flatMap(this::nodeToKeY);
@Nullable
public ProgramElement resolvedDeclarationToKeY(ResolvedDeclaration rm) {
var ast = rm.toAst();
return ast.map(this::nodeToKeY).orElse(null);
}

@Nullable
Expand All @@ -116,7 +119,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 @@ -128,7 +131,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 @@ -201,7 +204,7 @@ public int size() {
* not
*
* @param b boolean indicating if the special classes have been
* parsed in
* parsed in
*/
public void parsedSpecial(boolean b) {
parsedSpecial = b;
Expand Down
133 changes: 79 additions & 54 deletions key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java
View file
Original file line number Diff line number Diff line change
@@ -1,25 +1,5 @@
package de.uka.ilkd.key.java;

import java.util.*;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import java.util.stream.StreamSupport;
import javax.annotation.Nonnull;
import javax.annotation.Nullable;

import de.uka.ilkd.key.java.ast.ResolvedLogicalType;
import de.uka.ilkd.key.java.ast.abstraction.ArrayType;
import de.uka.ilkd.key.java.ast.abstraction.Field;
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
import de.uka.ilkd.key.java.ast.abstraction.Type;
import de.uka.ilkd.key.java.ast.declaration.*;
import de.uka.ilkd.key.java.loader.JP2KeYTypeConverter;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.logic.op.ProgramMethod;

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;

import com.github.javaparser.ast.AccessSpecifier;
import com.github.javaparser.ast.CompilationUnit;
import com.github.javaparser.ast.Modifier;
Expand All @@ -35,9 +15,27 @@
import com.github.javaparser.resolution.types.ResolvedType;
import com.github.javaparser.symbolsolver.javaparsermodel.declarations.DefaultConstructorDeclaration;
import com.github.javaparser.symbolsolver.javaparsermodel.declarations.JavaParserMethodDeclaration;
import de.uka.ilkd.key.java.ast.ResolvedLogicalType;
import de.uka.ilkd.key.java.ast.abstraction.ArrayType;
import de.uka.ilkd.key.java.ast.abstraction.Field;
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
import de.uka.ilkd.key.java.ast.abstraction.Type;
import de.uka.ilkd.key.java.ast.declaration.*;
import de.uka.ilkd.key.java.loader.JP2KeYTypeConverter;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.logic.op.ProgramMethod;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import javax.annotation.Nonnull;
import javax.annotation.Nullable;
import java.util.*;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import java.util.stream.StreamSupport;


public class KeYProgModelInfo {

Expand Down Expand Up @@ -99,8 +97,8 @@ public List<IProgramMethod> getAllProgramMethods(KeYJavaType kjt) {
List<IProgramMethod> result = new ArrayList<>(methods.size());
for (var rm : methods) {
var declaration = rec2key().resolvedDeclarationToKeY(rm);
if (declaration.isPresent()) {
result.add((IProgramMethod) declaration.get());
if (declaration != null) {
result.add((IProgramMethod) declaration);
}
}
return result;
Expand Down Expand Up @@ -165,15 +163,15 @@ public boolean isFinal(KeYJavaType kjt) {
* Checks whether subType is a subtype of superType or not.
*
* @return true if subType is subtype of superType,
* false in the other case.
* false in the other case.
*/
public boolean isSubtype(KeYJavaType subType, KeYJavaType superType) {
return isSubtype(rec2key().resolveType(subType), rec2key().resolveType(superType));
}

private boolean isSubtype(ResolvedType subType, ResolvedType superType) {
return superType.isAssignableBy(subType); // TODO weigl check if it is the right method and
// order.
// order.
}

public boolean isPackage(String name) {
Expand Down Expand Up @@ -213,8 +211,8 @@ public List<ProgramMethod> getAllProgramMethodsLocallyDeclared(KeYJavaType ct) {
for (MethodUsage methodUsage : rml) {
if (methodUsage.getDeclaration() instanceof JavaParserMethodDeclaration) {
var element = mapping.resolvedDeclarationToKeY(methodUsage.getDeclaration());
if (element.isPresent()) {
result.add((ProgramMethod) element.get());
if (element != null) {
result.add((ProgramMethod) element);
}
}
}
Expand All @@ -240,8 +238,8 @@ public List<IProgramMethod> getConstructors(KeYJavaType ct) {
continue;
}
var m = mapping.resolvedDeclarationToKeY(decl);
if (m.isPresent()) {
result.add((IProgramMethod) m.get());
if (m != null) {
result.add((IProgramMethod) m);
}
}
return result;
Expand All @@ -251,13 +249,40 @@ public List<IProgramMethod> getConstructors(KeYJavaType ct) {
* retrieves the most specific constructor declared in the given type with
* respect to the given signature
*
* @param ct the KeYJavyType where to look for the constructor
* @param ct the KeYJavyType where to look for the constructor
* @param signature IList<KeYJavaType> representing the signature of the constructor
* @return the most specific constructor declared in the given type
*/
@Nullable
public IProgramMethod getConstructor(KeYJavaType ct, ImmutableList<KeYJavaType> signature) {
// TODO javaparser
throw new UnsupportedOperationException();
var rt = getJavaParserType(ct).asReferenceType().getTypeDeclaration();
if (rt.isPresent()) {
List<ResolvedType> sig = signature.stream().map(this::getJavaParserType).toList();

List<ResolvedConstructorDeclaration> constructors = rt.get().getConstructors();
constr: for (var constructor : constructors) {
if (sig.size() != constructor.getNumberOfParams()) {
continue;
}

if (sig.size() == 0) { // fast track for default constructor calls!
var ast = constructor.toAst().get();
return (IProgramMethod) mapping.nodeToKeY(ast);
}

// compare types of the parameters
List<ResolvedType> types = constructor.formalParameterTypes();
for (int i = 0; i < types.size(); i++) {
if (!types.get(i).equals(sig.get(i))) {
break constr;
}
}
var ast = constructor.toAst().get();
return (IProgramMethod) mapping.nodeToKeY(ast);
}
//((ClassOrInterfaceDeclaration) rt.get().toAst().get()).getConstructorByParameterTypes()
}
return null;
}

/**
Expand Down Expand Up @@ -289,16 +314,16 @@ private IProgramMethod getImplicitMethod(KeYJavaType ct, String name) {
* in the given type or in a supertype where it is visible for the
* given type, and has a signature that is compatible to the given one.
*
* @param ct the class type to get methods from.
* @param name the name of the methods in question.
* @param ct the class type to get methods from.
* @param name the name of the methods in question.
* @param signature the statical type signature of a callee.
* @return the IProgramMethods, if one is found,
* null if none or more than one IProgramMethod is found (in this case
* a debug output is written to console).
* null if none or more than one IProgramMethod is found (in this case
* a debug output is written to console).
*/
@Nullable
public IProgramMethod getProgramMethod(@Nonnull KeYJavaType ct, String name,
Iterable<KeYJavaType> signature) {
Iterable<KeYJavaType> signature) {
if (ct.getJavaType() instanceof ArrayType) {
return getImplicitMethod(ct, name);
}
Expand All @@ -312,7 +337,7 @@ public IProgramMethod getProgramMethod(@Nonnull KeYJavaType ct, String name,
.map(this::getJavaParserType).toList();
var method = MethodResolutionLogic.solveMethodInType(rct, name, jpSignature);
return method.getDeclaration()
.map(d -> (IProgramMethod) mapping.resolvedDeclarationToKeY(d).orElseThrow())
.map(d -> (IProgramMethod) Objects.requireNonNull(mapping.resolvedDeclarationToKeY(d)))
.orElse(null);
}

Expand All @@ -321,12 +346,12 @@ public IProgramMethod getProgramMethod(@Nonnull KeYJavaType ct, String name,
* in the given type or in a supertype where it is visible for the
* given type, and has a signature that is compatible to the given one.
*
* @param ct the class type to get methods from.
* @param name the name of the methods in question.
* @param ct the class type to get methods from.
* @param name the name of the methods in question.
* @param signature the statical type signature of a callee.
* @return the IProgramMethods, if one is found,
* null if none or more than one IProgramMethod is found (in this case
* a debug output is written to console).
* null if none or more than one IProgramMethod is found (in this case
* a debug output is written to console).
*/
public IProgramMethod getProgramMethod(
@Nonnull KeYJavaType ct, String name,
Expand All @@ -337,8 +362,8 @@ public IProgramMethod getProgramMethod(

private List<Field> asKeYFieldsR(Stream<ResolvedFieldDeclaration> rfl) {
return rfl.flatMap(
it -> ((FieldDeclaration) mapping.resolvedDeclarationToKeY(it).orElseThrow())
.getFieldSpecifications().stream())
it -> ((FieldDeclaration) Objects.requireNonNull(mapping.resolvedDeclarationToKeY(it)))
.getFieldSpecifications().stream())
.collect(Collectors.toList());
}

Expand Down Expand Up @@ -389,12 +414,12 @@ public List<Field> getAllVisibleFields(KeYJavaType ct) {
*/
private List<Field> getVisibleArrayFields(KeYJavaType arrayType) {
final ImmutableArray<MemberDeclaration> members =
((ArrayDeclaration) arrayType.getJavaType()).getMembers();
((ArrayDeclaration) arrayType.getJavaType()).getMembers();
List<Field> result = new ArrayList<>();
for (MemberDeclaration member : members) {
if (member instanceof FieldDeclaration) {
final ImmutableArray<FieldSpecification> specs =
((FieldDeclaration) member).getFieldSpecifications();
((FieldDeclaration) member).getFieldSpecifications();
for (FieldSpecification spec : specs) {
result.add(spec);
}
Expand All @@ -408,7 +433,7 @@ private List<Field> getVisibleArrayFields(KeYJavaType arrayType) {
.getDeclaredFields()
.stream()
.filter(f -> f.accessSpecifier() != AccessSpecifier.PRIVATE)
.map(f -> (Field) mapping.resolvedDeclarationToKeY(f).orElseThrow())
.map(f -> (Field) Objects.requireNonNull(mapping.resolvedDeclarationToKeY(f)))
.toList();
result.addAll(objectFields);

Check notice on line 438 in key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java

View workflow job for this annotation

GitHub Actions / qodana

Constant conditions & exceptions 

Value `objectFields` is always 'null'
return result;
Expand Down Expand Up @@ -461,12 +486,12 @@ private List<ResolvedReferenceType> getAllDeclaredSupertypes(KeYJavaType ct) {
*
* @param rctl the ASTList<ClassType> to be converted
* @return list of KeYJavaTypes representing the given recoder types in
* the same order
* the same order
*/
private List<KeYJavaType> asKeYJavaTypes(
final Stream<ResolvedReferenceTypeDeclaration> rctl) {
return rctl
.map(it -> rec2key().resolvedTypeToKeY(new ReferenceTypeImpl(it)).orElseThrow())
.map(it -> Objects.requireNonNull(rec2key().resolvedTypeToKeY(new ReferenceTypeImpl(it))))
.collect(Collectors.toList());
}

Expand Down Expand Up @@ -497,7 +522,7 @@ public List<KeYJavaType> getAllSubtypes(KeYJavaType ct) {
}

public ImmutableList<KeYJavaType> findImplementations(KeYJavaType ct, String name,
ImmutableList<KeYJavaType> signature) {
ImmutableList<KeYJavaType> signature) {
var type = rec2key().resolveType(ct);
if (!type.isReferenceType()) {
return ImmutableList.of();
Expand Down Expand Up @@ -541,7 +566,7 @@ public ImmutableList<KeYJavaType> findImplementations(KeYJavaType ct, String nam


private ImmutableList<KeYJavaType> recFindImplementations(TypeDeclaration ct,
String name, List<Type> signature, ImmutableList<KeYJavaType> result) {
String name, List<Type> signature, ImmutableList<KeYJavaType> result) {
// TODO weigl does not compile, no idea what this should be
// if (declaresApplicableMethods(ct, name, signature)) {
// KeYJavaType r = (KeYJavaType) mapping.toKeY(ct);
Expand All @@ -568,15 +593,15 @@ private ImmutableList<KeYJavaType> recFindImplementations(TypeDeclaration ct,


private boolean declaresApplicableMethods(MethodResolutionCapability ct, String name,
List<ResolvedType> signature) {
List<ResolvedType> signature) {
var method = ct.solveMethod(name, signature, false);
return method.isSolved();
}

private boolean isDeclaringInterface(/*
* recoder.abstraction.ClassType ct, String name,
* List<recoder.abstraction.Type> signature
*/) {
* recoder.abstraction.ClassType ct, String name,
* List<recoder.abstraction.Type> signature
*/) {
// TODO Weigl does not compile
// Debug.assertTrue(ct.isInterface());
// List<recoder.abstraction.Method> list = si.getMethods(ct);
Expand Down
Loading

0 comments on commit 3da3422

Please sign in to comment.