Skip to content

Commit a199acc

Browse files
authored
Merge branch 'main-1.x' into robin-aws/dafny-stdlibs-doo-makefile-fix
2 parents 2ae8391 + fe7f3f4 commit a199acc

File tree

7 files changed

+63
-50
lines changed

7 files changed

+63
-50
lines changed

TestModels/Constraints/Model/Constraints.smithy

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ structure SimpleConstraintsConfig {
2222

2323
// This is just a sanity check on the smokeTests support.
2424
// We need to actually convert all the tests in test/WrappedSimpleConstraintsImplTest.dfy
25-
// to smoke tests once https://github.com/smithy-lang/smithy-dafny/issues/278
25+
// to smoke tests now that https://github.com/smithy-lang/smithy-dafny/issues/278
2626
// is fixed.
2727
@smithy.test#smokeTests([
2828
{
@@ -44,17 +44,22 @@ structure SimpleConstraintsConfig {
4444
success: {}
4545
}
4646
},
47+
{
48+
id: "GetConstraintsSuccessNoParams"
49+
vendorParams: {
50+
RequiredString: "foobar",
51+
}
52+
params: {}
53+
expect: {
54+
success: {}
55+
}
56+
},
4757
{
4858
id: "GetConstraintsFailure"
4959
vendorParams: {
5060
RequiredString: "foobar",
5161
}
5262
params: {
53-
// These two always have to be present because of https://github.com/smithy-lang/smithy-dafny/issues/278,
54-
// because otherwise they are interpreted as 0.
55-
OneToTen: 5,
56-
GreaterThanOne: 2,
57-
// This is the member that's actually invalid
5863
NonEmptyBlob: ""
5964
}
6065
expect: {

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkDotNetNameResolver.java

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,13 @@ private boolean isGeneratedInSdk(final ShapeId shapeId) {
4646
}
4747

4848
@Override
49+
protected String baseTypeForMember(final MemberShape memberShape) {
50+
// The AWS SDK uses primitive types for required members.
51+
return memberShapeIsOptional(memberShape)
52+
? super.baseTypeForMember(memberShape)
53+
: baseTypeForShape(memberShape.getTarget());
54+
}
55+
4956
protected String baseTypeForEnum(final EnumShape enumShape) {
5057
if (isGeneratedInSdk(enumShape.getId())) {
5158
return "%s.%s".formatted(

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkTypeConversionCodegen.java

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,11 @@ public TokenTree generateExtractOptionalMember(MemberShape memberShape) {
8282
final String propertyName = nameResolver.classPropertyForStructureMember(
8383
memberShape
8484
);
85-
return TokenTree.of(type, varName, "= value.%s;".formatted(propertyName));
85+
return TokenTree.of(
86+
type,
87+
varName,
88+
"= (%s)value.%s;".formatted(type, propertyName)
89+
);
8690
}
8791

8892
@Override

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -412,9 +412,8 @@ protected String baseTypeForUnion(final UnionShape unionShape) {
412412
}
413413

414414
protected String baseTypeForMember(final MemberShape memberShape) {
415-
final String baseType = baseTypeForShape(memberShape.getTarget());
416-
final boolean isOptional = memberShapeIsOptional(memberShape);
417-
return isOptional ? baseTypeForOptionalMember(memberShape) : baseType;
415+
// We always use nullable types for safety.
416+
return baseTypeForOptionalMember(memberShape);
418417
}
419418

420419
protected String baseTypeForOptionalMember(final MemberShape memberShape) {

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -797,20 +797,6 @@ public TypeConverter generateMemberConverter(final MemberShape memberShape) {
797797
TO_DAFNY
798798
);
799799

800-
if (!nameResolver.memberShapeIsOptional(memberShape)) {
801-
final TokenTree fromDafnyBody = Token.of(
802-
"return %s(value);".formatted(targetFromDafnyConverterName)
803-
);
804-
final TokenTree toDafnyBody = Token.of(
805-
"return %s(value);".formatted(targetToDafnyConverterName)
806-
);
807-
return buildConverterFromMethodBodies(
808-
memberShape,
809-
fromDafnyBody,
810-
toDafnyBody
811-
);
812-
}
813-
814800
String cSharpTypeUnModified;
815801
if (
816802
StringUtils.equals(
@@ -828,6 +814,23 @@ public TypeConverter generateMemberConverter(final MemberShape memberShape) {
828814
cSharpTypeUnModified.substring(0, (cSharpTypeUnModified.length() - 1));
829815
}
830816

817+
if (!nameResolver.memberShapeIsOptional(memberShape)) {
818+
final TokenTree fromDafnyBody = Token.of(
819+
"return %s(value);".formatted(targetFromDafnyConverterName)
820+
);
821+
final TokenTree toDafnyBody = Token.of(
822+
"return %s((%s)value);".formatted(
823+
targetToDafnyConverterName,
824+
cSharpTypeUnModified
825+
)
826+
);
827+
return buildConverterFromMethodBodies(
828+
memberShape,
829+
fromDafnyBody,
830+
toDafnyBody
831+
);
832+
}
833+
831834
final String cSharpType = cSharpTypeUnModified;
832835
final String cSharpOptionType;
833836
if (
@@ -900,6 +903,8 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) {
900903
.map(memberShape -> {
901904
final String propertyName =
902905
nameResolver.classPropertyForStructureMember(memberShape);
906+
final String propertyType =
907+
nameResolver.classPropertyTypeForStructureMember(memberShape);
903908
final String memberFromDafnyConverterName = typeConverterForShape(
904909
memberShape.getId(),
905910
FROM_DAFNY
@@ -930,8 +935,9 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) {
930935
.append(
931936
TokenTree
932937
.of(
933-
"converted.%s = %s(concrete.dtor_%s);".formatted(
938+
"converted.%s = (%s)(%s(concrete.dtor_%s));".formatted(
934939
propertyName,
940+
propertyType,
935941
memberFromDafnyConverterName,
936942
destructorValue
937943
),

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Native.java

Lines changed: 15 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@
3232
import software.amazon.smithy.model.shapes.Shape;
3333
import software.amazon.smithy.model.shapes.ShapeId;
3434
import software.amazon.smithy.model.shapes.ShapeType;
35-
import software.amazon.smithy.model.traits.BoxTrait;
3635
import software.amazon.smithy.model.traits.EnumTrait;
3736
import software.amazon.smithy.model.traits.StreamingTrait;
3837

@@ -76,13 +75,13 @@ public class Native extends NameResolver {
7675
NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE =
7776
Map.ofEntries(
7877
Map.entry(ShapeType.BLOB, ClassName.get(ByteBuffer.class)),
79-
Map.entry(ShapeType.BOOLEAN, TypeName.BOOLEAN),
80-
Map.entry(ShapeType.BYTE, TypeName.BYTE),
81-
Map.entry(ShapeType.SHORT, TypeName.SHORT),
82-
Map.entry(ShapeType.INTEGER, TypeName.INT),
83-
Map.entry(ShapeType.LONG, TypeName.LONG),
84-
Map.entry(ShapeType.FLOAT, TypeName.FLOAT),
85-
Map.entry(ShapeType.DOUBLE, TypeName.DOUBLE),
78+
Map.entry(ShapeType.BOOLEAN, TypeName.BOOLEAN.box()),
79+
Map.entry(ShapeType.BYTE, TypeName.BYTE.box()),
80+
Map.entry(ShapeType.SHORT, TypeName.SHORT.box()),
81+
Map.entry(ShapeType.INTEGER, TypeName.INT.box()),
82+
Map.entry(ShapeType.LONG, TypeName.LONG.box()),
83+
Map.entry(ShapeType.FLOAT, TypeName.FLOAT.box()),
84+
Map.entry(ShapeType.DOUBLE, TypeName.DOUBLE.box()),
8685
// TODO: AWS SDK V2 uses Instant, not Date
8786
Map.entry(ShapeType.TIMESTAMP, ClassName.get(Date.class)),
8887
Map.entry(ShapeType.BIG_DECIMAL, ClassName.get(BigDecimal.class)),
@@ -144,21 +143,14 @@ public TypeName typeForShape(final ShapeId shapeId) {
144143
}
145144

146145
return switch (shape.getType()) {
147-
case BOOLEAN, BYTE, SHORT, INTEGER, LONG, FLOAT, DOUBLE -> {
148-
/* From the Smithy Docs:
149-
* "Boolean, byte, short, integer, long, float, and double shapes
150-
* are only considered boxed if they are marked with the box trait.
151-
* All other shapes are always considered boxed."
152-
* https://smithy.io/1.0/spec/core/type-refinement-traits.html#box-trait
153-
* While Smithy Models SHOULD use Smithy Prelude shapes to avoid this confusion,
154-
* they do not have to.
155-
* Hence, the need to check if these shapes have the box trait
156-
*/
157-
final TypeName typeName = NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE.get(
158-
shape.getType()
159-
);
160-
yield shape.hasTrait(BoxTrait.class) ? typeName.box() : typeName;
161-
}
146+
// All primitives are boxed for safety, even if @required
147+
case BOOLEAN,
148+
BYTE,
149+
SHORT,
150+
INTEGER,
151+
LONG,
152+
FLOAT,
153+
DOUBLE -> NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE.get(shape.getType());
162154
// For supported simple shapes, just map to native types
163155
case BLOB,
164156
TIMESTAMP,

codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/Constants.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,10 @@ class Constants {
1111
static String RANGE_TRAIT_INTEGER_BUILD_EXPECTED =
1212
"""
1313
%s {
14-
if (this._zeroToTenSet && this.zeroToTen() < 0) {
14+
if (Objects.nonNull(this.zeroToTen()) && this.zeroToTen() < 0) {
1515
throw new IllegalArgumentException("`zeroToTen` must be greater than or equal to 0");
1616
}
17-
if (this._zeroToTenSet && this.zeroToTen() > 10) {
17+
if (Objects.nonNull(this.zeroToTen()) && this.zeroToTen() > 10) {
1818
throw new IllegalArgumentException("`zeroToTen` must be less than or equal to 10.");
1919
}
2020
%s

0 commit comments

Comments
 (0)