Merge branch 'robin-aws/dafny-stdlibs-doo-makefile-fix' of github.com…

…:smithy-lang/smithy-dafny into robin-aws/dafny-stdlibs-doo-makefile-fix

TestModels/Constraints/Model/Constraints.smithy

@@ -22,7 +22,7 @@ structure SimpleConstraintsConfig {
 
 // This is just a sanity check on the smokeTests support.
 // We need to actually convert all the tests in test/WrappedSimpleConstraintsImplTest.dfy
-// to smoke tests once https://github.com/smithy-lang/smithy-dafny/issues/278
+// to smoke tests now that https://github.com/smithy-lang/smithy-dafny/issues/278
 // is fixed.
 @smithy.test#smokeTests([
   {
@@ -44,17 +44,22 @@ structure SimpleConstraintsConfig {
         success: {}
     }
   },
+  {
+    id: "GetConstraintsSuccessNoParams"
+    vendorParams: {
+      RequiredString: "foobar",
+    }
+    params: {}
+    expect: {
+        success: {}
+    }
+  },
   {
     id: "GetConstraintsFailure"
     vendorParams: {
       RequiredString: "foobar",
     }
     params: {
-      // These two always have to be present because of https://github.com/smithy-lang/smithy-dafny/issues/278,
-      // because otherwise they are interpreted as 0.
-      OneToTen: 5,
-      GreaterThanOne: 2,
-      // This is the member that's actually invalid
       NonEmptyBlob: ""
     }
     expect: {

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

@@ -46,6 +46,13 @@ private boolean isGeneratedInSdk(final ShapeId shapeId) {
   }
 
   @Override
+  protected String baseTypeForMember(final MemberShape memberShape) {
+    // The AWS SDK uses primitive types for required members.
+    return memberShapeIsOptional(memberShape)
+      ? super.baseTypeForMember(memberShape)
+      : baseTypeForShape(memberShape.getTarget());
+  }
+
   protected String baseTypeForEnum(final EnumShape enumShape) {
     if (isGeneratedInSdk(enumShape.getId())) {
       return "%s.%s".formatted(

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

@@ -82,7 +82,11 @@ public TokenTree generateExtractOptionalMember(MemberShape memberShape) {
     final String propertyName = nameResolver.classPropertyForStructureMember(
       memberShape
     );
-    return TokenTree.of(type, varName, "= value.%s;".formatted(propertyName));
+    return TokenTree.of(
+      type,
+      varName,
+      "= (%s)value.%s;".formatted(type, propertyName)
+    );
   }
 
   @Override

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

@@ -412,9 +412,8 @@ protected String baseTypeForUnion(final UnionShape unionShape) {
   }
 
   protected String baseTypeForMember(final MemberShape memberShape) {
-    final String baseType = baseTypeForShape(memberShape.getTarget());
-    final boolean isOptional = memberShapeIsOptional(memberShape);
-    return isOptional ? baseTypeForOptionalMember(memberShape) : baseType;
+    // We always use nullable types for safety.
+    return baseTypeForOptionalMember(memberShape);
   }
 
   protected String baseTypeForOptionalMember(final MemberShape memberShape) {

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

@@ -797,20 +797,6 @@ public TypeConverter generateMemberConverter(final MemberShape memberShape) {
       TO_DAFNY
     );
 
-    if (!nameResolver.memberShapeIsOptional(memberShape)) {
-      final TokenTree fromDafnyBody = Token.of(
-        "return %s(value);".formatted(targetFromDafnyConverterName)
-      );
-      final TokenTree toDafnyBody = Token.of(
-        "return %s(value);".formatted(targetToDafnyConverterName)
-      );
-      return buildConverterFromMethodBodies(
-        memberShape,
-        fromDafnyBody,
-        toDafnyBody
-      );
-    }
-
     String cSharpTypeUnModified;
     if (
       StringUtils.equals(
@@ -828,6 +814,23 @@ public TypeConverter generateMemberConverter(final MemberShape memberShape) {
         cSharpTypeUnModified.substring(0, (cSharpTypeUnModified.length() - 1));
     }
 
+    if (!nameResolver.memberShapeIsOptional(memberShape)) {
+      final TokenTree fromDafnyBody = Token.of(
+        "return %s(value);".formatted(targetFromDafnyConverterName)
+      );
+      final TokenTree toDafnyBody = Token.of(
+        "return %s((%s)value);".formatted(
+            targetToDafnyConverterName,
+            cSharpTypeUnModified
+          )
+      );
+      return buildConverterFromMethodBodies(
+        memberShape,
+        fromDafnyBody,
+        toDafnyBody
+      );
+    }
+
     final String cSharpType = cSharpTypeUnModified;
     final String cSharpOptionType;
     if (
@@ -900,6 +903,8 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) {
           .map(memberShape -> {
             final String propertyName =
               nameResolver.classPropertyForStructureMember(memberShape);
+            final String propertyType =
+              nameResolver.classPropertyTypeForStructureMember(memberShape);
             final String memberFromDafnyConverterName = typeConverterForShape(
               memberShape.getId(),
               FROM_DAFNY
@@ -930,8 +935,9 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) {
               .append(
                 TokenTree
                   .of(
-                    "converted.%s = %s(concrete.dtor_%s);".formatted(
+                    "converted.%s = (%s)(%s(concrete.dtor_%s));".formatted(
                         propertyName,
+                        propertyType,
                         memberFromDafnyConverterName,
                         destructorValue
                       ),

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

@@ -32,7 +32,6 @@
 import software.amazon.smithy.model.shapes.Shape;
 import software.amazon.smithy.model.shapes.ShapeId;
 import software.amazon.smithy.model.shapes.ShapeType;
-import software.amazon.smithy.model.traits.BoxTrait;
 import software.amazon.smithy.model.traits.EnumTrait;
 import software.amazon.smithy.model.traits.StreamingTrait;
 
@@ -76,13 +75,13 @@ public class Native extends NameResolver {
     NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE =
       Map.ofEntries(
         Map.entry(ShapeType.BLOB, ClassName.get(ByteBuffer.class)),
-        Map.entry(ShapeType.BOOLEAN, TypeName.BOOLEAN),
-        Map.entry(ShapeType.BYTE, TypeName.BYTE),
-        Map.entry(ShapeType.SHORT, TypeName.SHORT),
-        Map.entry(ShapeType.INTEGER, TypeName.INT),
-        Map.entry(ShapeType.LONG, TypeName.LONG),
-        Map.entry(ShapeType.FLOAT, TypeName.FLOAT),
-        Map.entry(ShapeType.DOUBLE, TypeName.DOUBLE),
+        Map.entry(ShapeType.BOOLEAN, TypeName.BOOLEAN.box()),
+        Map.entry(ShapeType.BYTE, TypeName.BYTE.box()),
+        Map.entry(ShapeType.SHORT, TypeName.SHORT.box()),
+        Map.entry(ShapeType.INTEGER, TypeName.INT.box()),
+        Map.entry(ShapeType.LONG, TypeName.LONG.box()),
+        Map.entry(ShapeType.FLOAT, TypeName.FLOAT.box()),
+        Map.entry(ShapeType.DOUBLE, TypeName.DOUBLE.box()),
         // TODO: AWS SDK V2 uses Instant, not Date
         Map.entry(ShapeType.TIMESTAMP, ClassName.get(Date.class)),
         Map.entry(ShapeType.BIG_DECIMAL, ClassName.get(BigDecimal.class)),
@@ -144,21 +143,14 @@ public TypeName typeForShape(final ShapeId shapeId) {
     }
 
     return switch (shape.getType()) {
-      case BOOLEAN, BYTE, SHORT, INTEGER, LONG, FLOAT, DOUBLE -> {
-        /* From the Smithy Docs:
-         * "Boolean, byte, short, integer, long, float, and double shapes
-         * are only considered boxed if they are marked with the box trait.
-         * All other shapes are always considered boxed."
-         * https://smithy.io/1.0/spec/core/type-refinement-traits.html#box-trait
-         * While Smithy Models SHOULD use Smithy Prelude shapes to avoid this confusion,
-         * they do not have to.
-         * Hence, the need to check if these shapes have the box trait
-         */
-        final TypeName typeName = NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE.get(
-          shape.getType()
-        );
-        yield shape.hasTrait(BoxTrait.class) ? typeName.box() : typeName;
-      }
+      // All primitives are boxed for safety, even if @required
+      case BOOLEAN,
+        BYTE,
+        SHORT,
+        INTEGER,
+        LONG,
+        FLOAT,
+        DOUBLE -> NATIVE_TYPES_BY_SIMPLE_SHAPE_TYPE.get(shape.getType());
       // For supported simple shapes, just map to native types
       case BLOB,
         TIMESTAMP,

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

@@ -11,10 +11,10 @@ class Constants {
   static String RANGE_TRAIT_INTEGER_BUILD_EXPECTED =
     """
     %s {
-      if (this._zeroToTenSet && this.zeroToTen() < 0) {
+      if (Objects.nonNull(this.zeroToTen()) && this.zeroToTen() < 0) {
         throw new IllegalArgumentException("`zeroToTen` must be greater than or equal to 0");
       }
-      if (this._zeroToTenSet && this.zeroToTen() > 10) {
+      if (Objects.nonNull(this.zeroToTen()) && this.zeroToTen() > 10) {
         throw new IllegalArgumentException("`zeroToTen` must be less than or equal to 10.");
       }
       %s