From 73d7de462af6e0262967c2457e4e2abbe4a5ef1b Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 26 Jun 2023 16:19:41 -0700 Subject: [PATCH 1/4] Update README.md (#276) Fix typo in example --- codegen/smithy-dafny-codegen/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/codegen/smithy-dafny-codegen/README.md b/codegen/smithy-dafny-codegen/README.md index 5fe91aac9..467f3a0b3 100644 --- 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" } } } From d7b080a813c9fa3991acf412ed039719a89f917a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Fri, 7 Jul 2023 12:52:36 -0700 Subject: [PATCH 2/4] fix(NET): NET SDK Error Wrapping (#277) --- .../smithydotnet/AwsSdkShimCodegen.java | 5 ++- .../smithydotnet/ServiceCodegen.java | 4 ++- .../smithydotnet/TypeConversionCodegen.java | 33 +++++++++++++------ .../smithydotnet/AwsSdkShimCodegenTest.java | 5 ++- .../smithydotnet/ServiceCodegenTest.java | 1 + 5 files changed, 31 insertions(+), 17 deletions(-) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegen.java index dbdfae0b2..cd05049e1 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegen.java +++ b/codegen/smithy-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/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/ServiceCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/ServiceCodegen.java index 243395477..1224c21bd 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/ServiceCodegen.java +++ b/codegen/smithy-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/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java index 422e85f2c..93ed938ae 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java +++ b/codegen/smithy-dafny-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 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/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegenTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegenTest.java index 7c528c330..927e36b28 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydotnet/AwsSdkShimCodegenTest.java +++ b/codegen/smithy-dafny-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/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydotnet/ServiceCodegenTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydotnet/ServiceCodegenTest.java index 8bbc1e15d..83a45cf47 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithydotnet/ServiceCodegenTest.java +++ b/codegen/smithy-dafny-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;} } } """); From 32b66385da825218b918c2c42dceba91dc9783f6 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 17 Jul 2023 14:01:48 -0700 Subject: [PATCH 3/4] fix: Provide -compileSuffix to dafny when available (#280) --- TestModels/SharedMakefile.mk | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/TestModels/SharedMakefile.mk b/TestModels/SharedMakefile.mk index 14eb06fca..d2cdb7c25 100644 --- 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 @@ -92,6 +104,7 @@ transpile_implementation: -spillTargetCode:3 \ -compile:0 \ -optimizeErasableDatatypeWrapper:0 \ + $(COMPILE_SUFFIX_OPTION) \ -quantifierSyntax:3 \ -unicodeChar:0 \ -functionSyntax:3 \ @@ -109,6 +122,7 @@ transpile_test: -runAllTests:1 \ -compile:0 \ -optimizeErasableDatatypeWrapper:0 \ + $(COMPILE_SUFFIX_OPTION) \ -quantifierSyntax:3 \ -unicodeChar:0 \ -functionSyntax:3 \ From cf4522f804542b51bffd1ec204c69aa0fb1ba7e2 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 17 Jul 2023 16:30:43 -0700 Subject: [PATCH 4/4] chore: Add -compileSuffix:1 to a couple of other Makefiles (#281) --- TestModels/SimpleTypes/SimpleEnumV2/Makefile | 2 ++ TestModels/dafny-dependencies/StandardLibrary/Makefile | 1 + 2 files changed, 3 insertions(+) diff --git a/TestModels/SimpleTypes/SimpleEnumV2/Makefile b/TestModels/SimpleTypes/SimpleEnumV2/Makefile index ebbe747ff..bdb3ad984 100644 --- 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 index 436a4773f..6c029b074 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -48,6 +48,7 @@ transpile_implementation: -spillTargetCode:3 \ -compile:0 \ -optimizeErasableDatatypeWrapper:0 \ + $(COMPILE_SUFFIX_OPTION) \ -quantifierSyntax:3 \ -unicodeChar:0 \ -functionSyntax:3 \