Skip to content

Commit

Permalink
fix: Don't call _typeDescriptor() on reference types in Java (#321)
Browse files Browse the repository at this point in the history
This is necessary for Dafny 4.3 and higher, as Dafny no longer adds this method on reference types. The explicit construction of the right kind of TypeDescriptor (which works both before and after 4.3) was already implemented for other shapes in typeDescriptor(ShapeId), so I just tweaked the case identification, and scoped the default case more explicitly to shapes we know it works for, and now raise an exception for unrecognized shape types.

Unfortunately not covered by any TestModels (which is why #301 didn't fix this as well), but tested on MPL: #195
  • Loading branch information
robin-aws authored Feb 27, 2024
1 parent 61d382e commit 91b0908
Showing 1 changed file with 9 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -343,7 +343,7 @@ public CodeBlock typeDescriptor(ShapeId shapeId) {
return CodeBlock.of("$L()",
new MethodReference(abstractClassForError(), "_typeDescriptor").asNormalReference());
}
if (shape.hasTrait(ReferenceTrait.class) || shape.isServiceShape()) {
if (shape.hasTrait(ReferenceTrait.class) || shape.isServiceShape() || shape.isResourceShape()) {
// It is safe to use typeForShape here, as ReferenceTrait will always turn into a Resource or Service
TypeName interfaceClassName = typeForShape(shapeId);
return CodeBlock.of("$T.reference($T.class)", Constants.DAFNY_TYPE_DESCRIPTOR_CLASS_NAME, interfaceClassName);
Expand Down Expand Up @@ -376,8 +376,14 @@ public CodeBlock typeDescriptor(ShapeId shapeId) {
CodeBlock valueTypeDescriptor = typeDescriptor(shape.asMapShape().get().getValue().getTarget());
return CodeBlock.of("$T._typeDescriptor($L, $L)", Constants.DAFNY_MAP_CLASS_NAME, keyTypeDescriptor, valueTypeDescriptor);
}
return CodeBlock.of("$L()",
new MethodReference(classForNotErrorNotUnitShape(shape), "_typeDescriptor").asNormalReference());
if (shape.getType().isShapeType(ShapeType.STRUCTURE)
|| shape.getType().isShapeType(ShapeType.UNION)
|| shape.getType().isShapeType(ShapeType.DOUBLE)
|| shape.hasTrait(EnumTrait.class)) {
return CodeBlock.of("$L()",
new MethodReference(classForNotErrorNotUnitShape(shape), "_typeDescriptor").asNormalReference());
}
throw new IllegalArgumentException("Don't know how to create a type descriptor for this shape: %s".formatted(shape));
}

/*
Expand Down

0 comments on commit 91b0908

Please sign in to comment.