Merge branch 'lucmcdon/python-poc' of github.com:smithy-lang/smithy-d…

…afny into lucmcdon/python-poc
smithy-lang · Aug 15, 2023 · 45ada5b · 45ada5b
2 parents 85a98c8 + 52c5c04
commit 45ada5b
Show file tree

Hide file tree

Showing 9 changed files with 49 additions and 18 deletions.
diff --git a/TestModels/SharedMakefile.mk b/TestModels/SharedMakefile.mk
@@ -29,6 +29,18 @@ PROJECT_RELATIVE_ROOT := $(dir $(lastword $(MAKEFILE_LIST)))
 # i.e. The specific library under consideration.
 LIBRARY_ROOT = $(PWD)
 
+# Later versions of Dafny no longer default to adding "_Compile"
+# to the names of modules when translating.
+# Our target language code still assumes it does,
+# so IF the /compileSuffix option is available in our verion of Dafny
+# we need to provide it.
+COMPILE_SUFFIX_OPTION_CHECK_EXIT_CODE := $(shell dafny /help | grep -q /compileSuffix; echo $$?)
+ifeq ($(COMPILE_SUFFIX_OPTION_CHECK_EXIT_CODE), 0)
+	COMPILE_SUFFIX_OPTION := -compileSuffix:1
+else
+	COMPILE_SUFFIX_OPTION :=
+endif
+
 STANDARD_LIBRARY_PATH := $(PROJECT_ROOT)/dafny-dependencies/StandardLibrary
 CODEGEN_CLI_ROOT := $(PROJECT_ROOT)/../codegen/smithy-dafny-codegen-cli
 GRADLEW := $(PROJECT_ROOT)/../codegen/gradlew
@@ -127,6 +139,7 @@ transpile_implementation:
 		-spillTargetCode:3 \
 		-compile:0 \
 		-optimizeErasableDatatypeWrapper:0 \
+		$(COMPILE_SUFFIX_OPTION) \
 		-quantifierSyntax:3 \
 		-unicodeChar:0 \
 		-functionSyntax:3 \
@@ -144,6 +157,7 @@ transpile_test:
 		-runAllTests:1 \
 		-compile:0 \
 		-optimizeErasableDatatypeWrapper:0 \
+		$(COMPILE_SUFFIX_OPTION) \
 		-quantifierSyntax:3 \
 		-unicodeChar:0 \
 		-functionSyntax:3 \

diff --git a/TestModels/SimpleTypes/SimpleEnumV2/Makefile b/TestModels/SimpleTypes/SimpleEnumV2/Makefile
@@ -67,6 +67,7 @@ transpile_implementation_net:
 		-runAllTests:1 \
 		-compile:0 \
 		-optimizeErasableDatatypeWrapper:0 \
+		$(COMPILE_SUFFIX_OPTION) \
 		-useRuntimeLib \
 		-out runtimes/net/ImplementationFromDafny \
 		./src/Index.dfy \
@@ -81,6 +82,7 @@ transpile_test_net:
 		-runAllTests:1 \
 		-compile:0 \
 		-optimizeErasableDatatypeWrapper:0 \
+		$(COMPILE_SUFFIX_OPTION) \
 		-useRuntimeLib \
 		-out runtimes/net/tests/TestsFromDafny \
 		`find ./test -name '*.dfy'` \

diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile
@@ -67,6 +67,7 @@ transpile_implementation:
 		-spillTargetCode:3 \
 		-compile:0 \
 		-optimizeErasableDatatypeWrapper:0 \
+		$(COMPILE_SUFFIX_OPTION) \
 		-quantifierSyntax:3 \
 		-unicodeChar:0 \
 		-functionSyntax:3 \

diff --git a/codegen/smithy-dafny-codegen/README.md b/codegen/smithy-dafny-codegen/README.md
@@ -89,7 +89,7 @@ are as follows:
                 "edition": "2023",
                 "service": "smithy.example#ExampleService",
                 "targetLanguages": ["dotnet"],
-                "includeDafnyPath": "[relative]/[path]/[to]/StandardLibrary/src/Index.dfy"
+                "includeDafnyFile": "[relative]/[path]/[to]/StandardLibrary/src/Index.dfy"
             }
         }
     }

diff --git a/...dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegen.java b/...dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegen.java
@@ -112,11 +112,10 @@ public TokenTree generateOperationShim(final ShapeId operationShapeId) {
 
         final String baseExceptionForService = nameResolver.qualifiedClassForBaseServiceException();
         final TokenTree catchBlock = Token.of("""
-                catch (System.AggregateException aggregate) when (aggregate.InnerException is %s ex) {
-                    return %s.create_Failure(TypeConversion.ToDafny_CommonError(ex));
+                catch (System.AggregateException aggregate) {
+                    return %s.create_Failure(TypeConversion.ToDafny_CommonError(aggregate.InnerException));
                 }
                 """.formatted(
-                        baseExceptionForService,
                         dafnyOutputType));
 
         final TokenTree methodSignature = generateOperationShimSignature(operationShape);

diff --git a/...hy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/ServiceCodegen.java b/...hy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/ServiceCodegen.java
@@ -225,7 +225,9 @@ public TokenTree generateSpecificExceptionClass(final StructureShape structureSh
         // TODO Need to extend for a common class for this namespace
         final TokenTree classHeader = Token.of("public class %s : Exception".formatted(exceptionName));
         // TODO need to model _all_ possible members here...
-        final TokenTree messageCtor = Token.of("public %s(string message) : base(message) {}".formatted(exceptionName));
+        final TokenTree messageCtor = Token.of("""
+                                                public %s(string message) : base(message) {}
+                                                public string getMessage() { return this.Message; }""".formatted(exceptionName));
         return TokenTree.of(classHeader, messageCtor.braced()).namespaced(Token.of(nameResolver.namespaceForService()));
     }
 

diff --git a/...y-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java b/...y-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java
@@ -6,14 +6,7 @@
 import com.google.common.annotations.VisibleForTesting;
 
 import java.nio.file.Path;
-import java.util.ArrayList;
-import java.util.Collections;
-import java.util.HashSet;
-import java.util.List;
-import java.util.Map;
-import java.util.Optional;
-import java.util.Set;
-import java.util.TreeSet;
+import java.util.*;
 import java.util.function.Function;
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
@@ -47,6 +40,21 @@
  */
 public class TypeConversionCodegen {
     public static final String C_SHARP_SYSTEM_EXCEPTION = "System.Exception";
+    // Edge case for constructors of Exceptions that extend the base Exception class.
+    public static final List<String> ERROR_CTOR = Arrays.asList(
+            "AwsCryptographicMaterialProvidersException",
+            "EntryAlreadyExists",
+            "EntryDoesNotExist",
+            "InvalidAlgorithmSuiteInfo",
+            "InvalidAlgorithmSuiteInfoOnDecrypt",
+            "InvalidAlgorithmSuiteInfoOnEncrypt",
+            "InvalidDecryptionMaterials",
+            "InvalidDecryptionMaterialsTransition",
+            "InvalidEncryptionMaterials",
+            "InvalidEncryptionMaterialsTransition",
+            "KeyStoreException",
+            "KeyVectorException"
+    );
 
     /**
      * A pair of type converter methods that converts between the compiled Dafny representation and the idiomatic C#
@@ -461,6 +469,10 @@ private String generateConstructorArg(final MemberShape memberShape) {
                     typeConverterForShape(memberShape.getId(), TO_DAFNY),
                     nameResolver.classPropertyForStructureMember(memberShape));
         }
+        if (ERROR_CTOR.contains(memberShape.getContainer().getName()) || memberShape.getContainer().getName().endsWith("Error"))  {
+            return "%s(value.getMessage())".formatted(
+                     typeConverterForShape(memberShape.getId(), TO_DAFNY));
+        }
         return "%s(value.%s)".formatted(
                 typeConverterForShape(memberShape.getId(), TO_DAFNY),
                 nameResolver.classPropertyForStructureMember(memberShape));
@@ -546,6 +558,7 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) {
             .of(defNames
                 .stream()
                 .map(memberShape -> {
+                    final String propertyNameEdgeCase = StringUtils.equals(nameResolver.classPropertyForStructureMember(memberShape), "KmsKeyArn") ? "kmsKeyArn" : nameResolver.classPropertyForStructureMember(memberShape);
                     final String propertyName = nameResolver.classPropertyForStructureMember(memberShape);
                     final String memberFromDafnyConverterName = typeConverterForShape(
                             memberShape.getId(), FROM_DAFNY);
@@ -556,7 +569,7 @@ public TypeConverter generateUnionConverter(final UnionShape unionShape) {
                         destructorValue = DafnyNameResolverHelpers.dafnyCompilesExtra_(memberShape.getMemberName());
                     }
                     return TokenTree
-                            .of("if (value.is_%s)".formatted(propertyName))
+                            .of("if (value.is_%s)".formatted(propertyNameEdgeCase))
                             .append(TokenTree
                                     .of(
                                             "converted.%s = %s(concrete.dtor_%s);"
@@ -1136,7 +1149,7 @@ public TypeConverter generateSpecificExceptionConverter(final StructureShape err
         assert errorShape.getMember("message").isPresent();
         final ShapeId messageShapeId = errorShape.getId().withMember("message");
 
-        final Token fromDafnyBody = Token.of("return new %s(%s(value.message));".formatted(
+        final Token fromDafnyBody = Token.of("return new %s(%s(value.Message));".formatted(
                 nameResolver.baseTypeForShape(errorShape.getId()),
                 typeConverterForShape(messageShapeId, FROM_DAFNY)
         ));

diff --git a/...y-codegen/src/test/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegenTest.java b/...y-codegen/src/test/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegenTest.java
@@ -147,9 +147,8 @@ public void testGenerateOperationShim() {
                             this._impl.GoAsync(sdkRequest).Result;
                         return Wrappers_Compile.Result<%1$s>.create_Success(%3$s(sdkResponse));
                     }
-                    catch (System.AggregateException aggregate)
-                        when (aggregate.InnerException is Amazon.FoobarService.AmazonFoobarServiceException ex) {
-                        return Wrappers_Compile.Result<%1$s>.create_Failure(TypeConversion.ToDafny_CommonError(ex));
+                    catch (System.AggregateException aggregate) {
+                        return Wrappers_Compile.Result<%1$s>.create_Failure(TypeConversion.ToDafny_CommonError(aggregate.InnerException));
                     }
                 }
                 """.formatted(resultTypeParams, requestFromDafnyConverter, responseToDafnyConverter));

diff --git a/...afny-codegen/src/test/java/software/amazon/polymorph/smithydotnet/ServiceCodegenTest.java b/...afny-codegen/src/test/java/software/amazon/polymorph/smithydotnet/ServiceCodegenTest.java
@@ -563,6 +563,7 @@ public void testGenerateSpecificExceptionClass() {
                 namespace Test.Foobar {
                     public class UnfortunateException : Exception {
                         public UnfortunateException(string message) : base(message) {}
+                        public string getMessage() { return this.Message;}
                     }
                 }
                 """);