From 183c4b3ea1469e46bb87530356f862157deb9b56 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 2 Jul 2024 15:40:44 -0700 Subject: [PATCH 1/5] cleanup --- TestModels/Constraints/Makefile | 21 +++ .../internaldafny/types/__default.java | 6 +- .../__default.java | 33 ++++ .../Extern/WrappedSimpleConstraintsService.cs | 17 ++- TestModels/Constraints/src/Index.dfy | 2 +- .../src/WrappedSimpleConstraintsImpl.dfy | 2 +- .../StandardLibrary/Makefile | 51 +++++-- .../java/src/main/java/UTF8/__default.java | 6 +- .../runtimes/net/Extern/UTF8.cs | 4 +- .../smithydafny/DafnyApiCodegen.java | 141 +++--------------- .../smithydotnet/DotNetNameResolver.java | 4 +- .../LocalServiceWrappedCodegen.java | 7 +- .../nativeWrapper/NativeWrapperCodegen.java | 2 +- .../smithyjava/BuilderMemberSpec.java | 27 ++-- .../smithyjava/OperationJavaDoc.java | 23 +-- .../smithyjava/generator/ToDafny.java | 2 +- .../generator/awssdk/v1/JavaAwsSdkV1.java | 4 +- .../generator/awssdk/v1/ToDafnyAwsV1.java | 7 +- .../generator/awssdk/v2/ShimV2.java | 1 + .../generator/awssdk/v2/ToDafnyAwsV2.java | 2 +- .../generator/library/ShimLibrary.java | 1 + .../generator/library/shims/ResourceShim.java | 6 +- .../generator/library/shims/ServiceShim.java | 8 +- .../smithyjava/modeled/ModeledEnum.java | 6 +- .../smithyjava/modeled/ModeledError.java | 6 +- .../smithyjava/modeled/ModeledStructure.java | 6 +- .../smithyjava/nameresolver/Constants.java | 4 +- .../smithyjava/nameresolver/Dafny.java | 13 +- 28 files changed, 216 insertions(+), 196 deletions(-) create mode 100644 TestModels/Constraints/runtimes/java/src/test/java/WrappedSimpleConstraintsService/__default.java diff --git a/TestModels/Constraints/Makefile b/TestModels/Constraints/Makefile index fa31cc5419..3826dd3ef8 100644 --- a/TestModels/Constraints/Makefile +++ b/TestModels/Constraints/Makefile @@ -24,3 +24,24 @@ polymorph: make polymorph_dafny make polymorph_java make polymorph_dotnet + +# Python + +PYTHON_MODULE_NAME=simple_constraints + +TRANSLATION_RECORD_PYTHON := \ + --translation-record ../dafny-dependencies/StandardLibrary/runtimes/python/src/standard_library/internaldafny/generated/dafny_src-py.dtr + +# Java + +JAVA_PACKAGE_NAME=simple.constraints + +TRANSLATION_RECORD_JAVA:= \ + --translation-record ../dafny-dependencies/StandardLibrary/runtimes/java/src/main/dafny-generated/ImplementationFromDafny-java.dtr + +# NET + +NET_NAMESPACE_NAME=simple.constraints + +TRANSLATION_RECORD_NET:= \ + --translation-record ../dafny-dependencies/StandardLibrary/runtimes/net/ImplementationFromDafny-cs.dtr diff --git a/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java b/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java index 1100632e4b..147f02dbb5 100644 --- a/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java +++ b/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java @@ -1,5 +1,5 @@ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 +// Class _ExternBase___default +// Dafny class __default compiled into Java package simple.constraints.internaldafny.types; -public class __default extends _ExternBase___default {} +public abstract class __default extends _ExternBase___default { } diff --git a/TestModels/Constraints/runtimes/java/src/test/java/WrappedSimpleConstraintsService/__default.java b/TestModels/Constraints/runtimes/java/src/test/java/WrappedSimpleConstraintsService/__default.java new file mode 100644 index 0000000000..70a47cb527 --- /dev/null +++ b/TestModels/Constraints/runtimes/java/src/test/java/WrappedSimpleConstraintsService/__default.java @@ -0,0 +1,33 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package WrappedSimpleConstraintsService; + +import software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.Result; +import simple.constraints.SimpleConstraints; +import simple.constraints.ToNative; +import simple.constraints.internaldafny.types.Error; +import simple.constraints.internaldafny.types.ISimpleConstraintsClient; +import simple.constraints.internaldafny.types.SimpleConstraintsConfig; +import simple.constraints.wrapped.TestSimpleConstraints; + +public class __default extends _ExternBase___default { + + public static Result< + ISimpleConstraintsClient, + Error + > WrappedSimpleConstraints(SimpleConstraintsConfig config) { + simple.constraints.model.SimpleConstraintsConfig wrappedConfig = + ToNative.SimpleConstraintsConfig(config); + simple.constraints.SimpleConstraints impl = SimpleConstraints + .builder() + .SimpleConstraintsConfig(wrappedConfig) + .build(); + TestSimpleConstraints wrappedClient = TestSimpleConstraints + .builder() + .impl(impl) + .build(); + return simple.constraints.internaldafny.SimpleConstraints.__default.CreateSuccessOfClient( + wrappedClient + ); + } +} diff --git a/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs b/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs index ef1e400b04..2ddd218057 100644 --- a/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs +++ b/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs @@ -1,17 +1,20 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 -using Wrappers_Compile; +using software.amazon.cryptography.standardlibrary.internaldafny.Wrappers; +using simple.constraints.internaldafny.types; using Simple.Constraints; using Simple.Constraints.Wrapped; -using TypeConversion = Simple.Constraints.TypeConversion ; -namespace simple.constraints.internaldafny.wrapped +using TypeConversion = Simple.Constraints.TypeConversion; +namespace WrappedSimpleConstraintsService { - public partial class __default { - public static _IResult WrappedSimpleConstraints(types._ISimpleConstraintsConfig config) { + public partial class __default + { + public static _IResult WrappedSimpleConstraints(simple.constraints.internaldafny.types._ISimpleConstraintsConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N11_constraints__S23_SimpleConstraintsConfig(config); - var impl = new SimpleConstraints(wrappedConfig); + var impl = new Simple.Constraints.SimpleConstraints(wrappedConfig); var wrappedClient = new SimpleConstraintsShim(impl); - return Result.create_Success(wrappedClient); + return Result.create_Success(wrappedClient); } } } diff --git a/TestModels/Constraints/src/Index.dfy b/TestModels/Constraints/src/Index.dfy index f8979e553a..2ac9079d68 100644 --- a/TestModels/Constraints/src/Index.dfy +++ b/TestModels/Constraints/src/Index.dfy @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 include "SimpleConstraintsImpl.dfy" -module {:extern "simple.constraints.internaldafny" } SimpleConstraints refines AbstractSimpleConstraintsService { +module SimpleConstraints refines AbstractSimpleConstraintsService { import Operations = SimpleConstraintsImpl function method DefaultSimpleConstraintsConfig(): SimpleConstraintsConfig { diff --git a/TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy b/TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy index 2d2f19bf2c..9909aef606 100644 --- a/TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy +++ b/TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 include "../Model/SimpleConstraintsTypesWrapped.dfy" -module {:extern "simple.constraints.internaldafny.wrapped"} WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService { +module {:extern "WrappedSimpleConstraintsService"} WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService { import WrappedService = SimpleConstraints function method WrappedDefaultSimpleConstraintsConfig(): SimpleConstraintsConfig { SimpleConstraintsConfig diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile index 3dcd26f9c1..f95b6af882 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -6,6 +6,10 @@ CORES=2 include ../../SharedMakefile.mk MAX_RESOURCE_COUNT=500000000 +PYTHON_MODULE_NAME=standard_library +JAVA_PACKAGE_NAME=software.amazon.cryptography.standardlibrary +NET_NAMESPACE_NAME=software.amazon.cryptography.standardlibrary +LIBRARIES := # define standard colors ifneq (,$(findstring xterm,${TERM})) @@ -36,6 +40,9 @@ polymorph_dotnet : polymorph_java : echo "Skipping polymorph_java for StandardLibrary" +polymorph_python : + echo "Skipping polymorph_python for StandardLibrary" + # Using this target for the side-effect of maintaining patches, # Since Dafny Rust code generation is incomplete and also needs to be patched. # That only works if you run transpile_rust first. @@ -63,6 +70,26 @@ transpile_net: | transpile_implementation_net transpile_test_net # StandardLibrary as a dependency transpile_java: | transpile_implementation_java transpile_test_java +# Override SharedMakefile's transpile_python to not transpile +# StandardLibrary as a dependency +transpile_python: | transpile_implementation_python transpile_test_python + +# Hacky workaround until Dafny supports per-language extern names. +# Replaces `.`s with `_`s in strings like `{:extern ".*"}`. +# This is flawed logic and should be removed, but is a reasonable band-aid for now. +# TODO: Once Dafny supports per-language extern names, remove and replace with Pythonic extern names. +# This may require new Smithy-Dafny logic to generate Pythonic extern names. +_python_underscore_extern_names: + find src -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/module {:extern \".*\"/s/\./_/g' {} \; + echo "Skipping Model modification for StandardLibrary" + find test -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/module {:extern \".*\"/s/\./_/g' {} \; + +_python_revert_underscore_extern_names: + find src -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/module {:extern \".*\"/s/_/\./g' {} \; + echo "Skipping Model modification for StandardLibrary" + find test -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/module {:extern \".*\"/s/_/\./g' {} \; + +########################## Rust targets # Override SharedMakefile's transpile_java to not transpile # StandardLibrary as a dependency transpile_rust: | transpile_implementation_rust @@ -86,21 +113,19 @@ transpile_dependencies: # Override SharedMakefile's transpile_implementation to not reference # StandardLibrary as a Library +transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src) transpile_implementation: find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \ - -stdin \ - -noVerify \ - -vcsCores:$(CORES) \ - -compileTarget:$(TARGET) \ - -spillTargetCode:3 \ - -compile:0 \ - -optimizeErasableDatatypeWrapper:0 \ - -compileSuffix:1 \ - -unicodeChar:0 \ - -functionSyntax:3 \ - -useRuntimeLib \ - $(DAFNY_OPTIONS) \ - -out $(OUT) + translate $(TARGET) \ + --stdin \ + --no-verify \ + --cores:$(CORES) \ + --optimize-erasable-datatype-wrapper:false \ + --unicode-char:false \ + --function-syntax:3 \ + --allow-warnings \ + --output $(OUT) \ + $(TRANSPILE_MODULE_NAME) # Override SharedMakefile's build_java to not install # StandardLibrary as a dependency diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java b/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java index 010dbed431..32de956315 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java @@ -1,13 +1,13 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 -package UTF8; +package software.amazon.cryptography.standardlibrary.internaldafny.UTF8; import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence; import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence; import static software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer; import static software.amazon.smithy.dafny.conversion.ToNative.Simple.String; -import Wrappers_Compile.Result; +import software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.Result; import dafny.DafnySequence; import java.nio.ByteBuffer; import java.nio.CharBuffer; @@ -22,7 +22,7 @@ // If we wanted to increase performance, // we could declare this NOT thread/concurrent safe, // and reset the coder everytime. -public class __default extends UTF8._ExternBase___default { +public class __default extends _ExternBase___default { // This is largely copied from Polymorph's dafny-java-conversion: // software.amazon.smithy.dafny.conversion.ToDafny.Simple.DafnyUtf8Bytes diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs index b9ba40f833..3f4452abac 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs @@ -4,13 +4,13 @@ using System; using System.Text; -using Wrappers_Compile; +using software.amazon.cryptography.standardlibrary.internaldafny.Wrappers; using ibyteseq = Dafny.ISequence; using byteseq = Dafny.Sequence; using icharseq = Dafny.ISequence; using charseq = Dafny.Sequence; -namespace UTF8 { +namespace software.amazon.cryptography.standardlibrary.internaldafny.UTF8 { public partial class __default { public static _IResult Encode(icharseq str) { UTF8Encoding utf8 = new UTF8Encoding(false, true); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java index 4656098f54..cf8878b7d3 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java @@ -129,10 +129,7 @@ public Map generate() { namespace ); final TokenTree typesModuleHeader = Token.of( - "module {:extern \"%s\" } %s".formatted( - DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId( - serviceShape.getId() - ), + "module {:extern \"types\"} %s".formatted( typesModuleName ) ); @@ -856,26 +853,24 @@ private TokenTree generateBodilessOperationMethodThatEnsuresCallEvents( .parenthesized() ), generateOperationReturnsClause(serviceShape, operationShape), - implementationType.equals(ImplementationType.DEVELOPER) - ? TokenTree.empty() - : isFunction - ? TokenTree.of( - "// Functions that are transparent do not need ensures" + isFunction + ? TokenTree.of( + "// Functions that are transparent do not need ensures" + ) + : TokenTree + .of( + generateMutableInvariantForMethod( + serviceShape, + operationShapeId, + implementationType + ), + generateEnsuresForEnsuresPubliclyPredicate(operationShapeId), + !implementationType.equals(ImplementationType.ABSTRACT) + ? generateEnsuresHistoricalCallEvents(operationShapeId) + : TokenTree.empty() ) - : TokenTree - .of( - generateMutableInvariantForMethod( - serviceShape, - operationShapeId, - implementationType - ), - generateEnsuresForEnsuresPubliclyPredicate(operationShapeId), - !implementationType.equals(ImplementationType.ABSTRACT) - ? generateEnsuresHistoricalCallEvents(operationShapeId) - : TokenTree.empty() - ) - .dropEmpty() - .lineSeparated() + .dropEmpty() + .lineSeparated() ) .lineSeparated(); return TokenTree @@ -885,15 +880,9 @@ private TokenTree generateBodilessOperationMethodThatEnsuresCallEvents( // so that other callers can compose // and add bodies. TokenTree.of( - switch (implementationType) { - case CODEGEN -> TokenTree.of( - "// The public method to be called by library consumers" - ); - case ABSTRACT -> TokenTree.of( - "// The private method to be refined by the library developer" - ); - case DEVELOPER -> TokenTree.empty(); - } + !implementationType.equals(ImplementationType.ABSTRACT) + ? "// The public method to be called by library consumers" + : "// The private method to be refined by the library developer" ), operationMethod ) @@ -2771,92 +2760,4 @@ private TokenTree generateAbstractOperationsModule( return TokenTree.of(header, body); } - - public Map generateSkeleton() { - final String namespace = serviceShape.getId().getNamespace(); - final String sdkID = serviceShape - .expectTrait(LocalServiceTrait.class) - .getSdkId(); - final String typesModuleName = DafnyNameResolver.dafnyTypesModuleName( - namespace - ); - final Path path = Path.of("%sImpl.dfy".formatted(sdkID)); - TokenTree includeDirectives = TokenTree.of( - "include \"../Model/%s.dfy\"".formatted(typesModuleName) - ); - TokenTree concreteModuleTemplate = generateTemplateOperationsModule( - serviceShape - ); - final TokenTree fullCode = TokenTree - .of(includeDirectives, concreteModuleTemplate) - .lineSeparated(); - return Map.of(path, fullCode); - } - - private TokenTree generateTemplateOperationsModule( - final ServiceShape serviceShape - ) { - final String baseModuleName = DafnyNameResolver.dafnyBaseModuleName( - serviceShape.getId().getNamespace() - ); - final TokenTree header = TokenTree.of( - "module %sImpl refines Abstract%sOperations".formatted( - baseModuleName, - baseModuleName - ) - ); - - final String internalConfigType = DafnyNameResolver.internalConfigType(); - - final TokenTree body = TokenTree - .of( - TokenTree.of("datatype Config = Config"), - TokenTree.of("type %s = Config".formatted(internalConfigType)), - TokenTree.of( - "predicate %s(config: %s)".formatted( - DafnyNameResolver.validConfigPredicate(), - internalConfigType - ) - ), - TokenTree.of("{true}"), - TokenTree.of( - "function %s(config: %s): set".formatted( - DafnyNameResolver.modifiesInternalConfig(), - internalConfigType - ) - ), - TokenTree.of("{{}}"), - TokenTree - .of( - serviceShape - .getAllOperations() - .stream() - .map(operation -> - TokenTree - .of( - generateEnsuresPubliclyPredicate(serviceShape, operation), - TokenTree.of("{true}"), - generateBodilessOperationMethodThatEnsuresCallEvents( - serviceShape, - operation, - ImplementationType.DEVELOPER - ), - TokenTree.of("{"), - TokenTree.of( - " expect false, \"...that you'll fill this in\";" - ), - TokenTree.of("}") - ) - .flatten() - .lineSeparated() - ) - ) - .lineSeparated() - ) - .flatten() - .lineSeparated() - .braced(); - - return TokenTree.of(header, body); - } } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java index 572e2d6be5..a30ebce5d3 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java @@ -881,7 +881,7 @@ private String dafnyTypeForOptionalMember( final String baseType = dafnyTypeForShape(memberShape.getTarget()); final String prefix = concrete ? "" : "_I"; - return "Wrappers_Compile.%sOption<%s>".formatted(prefix, baseType); + return "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.%sOption<%s>".formatted(prefix, baseType); } private String dafnyTypeForService(final ServiceShape serviceShape) { @@ -1060,7 +1060,7 @@ private String dafnyTypeForResult( final boolean concrete ) { final String resultType = concrete ? "Result" : "_IResult"; - return "Wrappers_Compile.%s<%s, %s>".formatted( + return "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.%s<%s, %s>".formatted( resultType, valueType, errorType diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java index 8882fde757..08ef019557 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java @@ -15,6 +15,8 @@ import software.amazon.smithy.model.shapes.ResourceShape; import software.amazon.smithy.model.shapes.ServiceShape; +import static software.amazon.polymorph.smithyjava.nameresolver.Dafny.convertNamespaceToPascalCase; + public class LocalServiceWrappedCodegen extends ServiceCodegen { public LocalServiceWrappedCodegen( @@ -88,7 +90,7 @@ public TokenTree generateWrappedServiceExtern( .of( "public static", // TODO fix the Error and don't hard code it :( - "Wrappers_Compile._IResult".formatted( + "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers._IResult".formatted( nameResolver.dafnyTypeForShape(serviceShape.getId()) ), "Wrapped%s(Types.%s config)".formatted( @@ -108,7 +110,7 @@ public TokenTree generateWrappedServiceExtern( ((LocalServiceWrappedNameResolver) nameResolver).shimClassForService() ), // TODO fix the Error and don't hard code it :( - "return Wrappers_Compile.Result.create_Success(wrappedClient);".formatted( + "return software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.Result.create_Success(wrappedClient);".formatted( nameResolver.dafnyTypeForShape(serviceShape.getId()) ) ) @@ -123,4 +125,5 @@ public TokenTree generateWrappedServiceExtern( ".Wrapped" ); } + } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/nativeWrapper/NativeWrapperCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/nativeWrapper/NativeWrapperCodegen.java index 099d84d084..ff1d11df30 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/nativeWrapper/NativeWrapperCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/nativeWrapper/NativeWrapperCodegen.java @@ -54,7 +54,7 @@ public class NativeWrapperCodegen { protected static final List UNCONDITIONAL_IMPORTS = List.of( "System", "_System", - "Wrappers_Compile" + "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers" ); public NativeWrapperCodegen( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java index ccba829424..f09dca461a 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java @@ -18,12 +18,13 @@ import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; import software.amazon.polymorph.smithyjava.nameresolver.Native; import software.amazon.polymorph.smithyjava.unmodeled.CollectionOfErrors; +import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.polymorph.traits.LocalServiceTrait; -import software.amazon.polymorph.utils.ModelUtils; import software.amazon.polymorph.utils.ModelUtils.ResolvedShapeId; import software.amazon.smithy.model.shapes.MemberShape; import software.amazon.smithy.model.shapes.Shape; import software.amazon.smithy.model.shapes.StructureShape; +import software.amazon.smithy.model.traits.StringTrait; // TODO: We can shrink our code base by combining // BuilderMemberSpec w/ PolymorphFieldSpec. @@ -116,11 +117,11 @@ public BuilderMemberSpec(MemberShape memberShape, JavaLibrary subject) { this.interfaceType = null; this.wrapCall = null; } - this.javaDoc = - ModelUtils - .getDocumentationOrJavadoc(memberShape) - .or(() -> ModelUtils.getDocumentationOrJavadoc(resolvedShape)) - .orElse(null); + Optional maybeJavaDoc = memberShape.getMemberTrait( + subject.model, + JavaDocTrait.class + ); + this.javaDoc = maybeJavaDoc.map(StringTrait::getValue).orElse(null); } /** Private Method for handling Edge Cases or cases where @@ -152,9 +153,10 @@ public static BuilderMemberSpec localServiceConfigMemberSpec( trait.getConfigId(), StructureShape.class ); - String javaDoc = ModelUtils - .getDocumentationOrJavadoc(structureShape) - .orElse(null); + Optional maybeJavaDoc = structureShape.getTrait( + JavaDocTrait.class + ); + String javaDoc = maybeJavaDoc.map(StringTrait::getValue).orElse(null); return new BuilderMemberSpec(type, name, javaDoc); } @@ -165,9 +167,10 @@ public static BuilderMemberSpec localServiceAsMemberSpec( subject.serviceShape ); String name = INTERFACE_VAR; - String javaDoc = ModelUtils - .getDocumentationOrJavadoc(subject.serviceShape) - .orElse(null); + Optional maybeJavaDoc = subject.serviceShape.getTrait( + JavaDocTrait.class + ); + String javaDoc = maybeJavaDoc.map(StringTrait::getValue).orElse(null); return new BuilderMemberSpec(type, name, javaDoc); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/OperationJavaDoc.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/OperationJavaDoc.java index e2fcd0c597..173212f724 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/OperationJavaDoc.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/OperationJavaDoc.java @@ -10,10 +10,10 @@ import javax.annotation.Nullable; import software.amazon.awssdk.utils.Pair; import software.amazon.awssdk.utils.StringUtils; -import software.amazon.polymorph.utils.ModelUtils; +import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.smithy.model.Model; import software.amazon.smithy.model.shapes.OperationShape; -import software.amazon.smithy.model.shapes.Shape; +import software.amazon.smithy.model.traits.StringTrait; /** * @param desc JavaDoc Body content @@ -66,20 +66,25 @@ public static OperationJavaDoc fromOperationShape( Model model, OperationShape shape ) { - Shape inputShape = model.expectShape(shape.getInputShape()); @Nullable - String paramDoc = ModelUtils - .getDocumentationOrJavadoc(inputShape) + String paramDoc = model + .expectShape(shape.getInputShape()) + .getMemberTrait(model, JavaDocTrait.class) + .map(StringTrait::getValue) .orElse(null); @Nonnull String paramName = NATIVE_VAR; - Shape outputShape = model.expectShape(shape.getOutputShape()); @Nullable - String returns = ModelUtils - .getDocumentationOrJavadoc(outputShape) + String returns = model + .expectShape(shape.getOutputShape()) + .getMemberTrait(model, JavaDocTrait.class) + .map(StringTrait::getValue) .orElse(null); @Nullable - String desc = ModelUtils.getDocumentationOrJavadoc(shape).orElse(null); + String desc = shape + .getTrait(JavaDocTrait.class) + .map(StringTrait::getValue) + .orElse(null); List> params = StringUtils.isNotBlank(paramDoc) ? List.of(Pair.of(paramName, paramDoc)) : null; diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java index 9ec737662a..e4c67b0138 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java @@ -225,7 +225,7 @@ protected CodeBlock memberDeclaration( return CodeBlock.of( "$T $L", ParameterizedTypeName.get( - ClassName.get("Wrappers_Compile", "Option"), + ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"), subject.dafnyNameResolver.typeForShape(memberShape.getId()) ), variable diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/JavaAwsSdkV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/JavaAwsSdkV1.java index 1b577d1b78..d97bbc10d2 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/JavaAwsSdkV1.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/JavaAwsSdkV1.java @@ -13,6 +13,8 @@ import software.amazon.smithy.model.Model; import software.amazon.smithy.model.shapes.ServiceShape; +import static software.amazon.polymorph.smithyjava.nameresolver.Dafny.convertNamespaceToPascalCase; + /** * Generates all the Java Classes needed for * Dafny Generated Java to call AWS Services via @@ -46,7 +48,7 @@ private JavaAwsSdkV1( this.packageName = DafnyNameResolverHelpers.packageNameForNamespace( serviceShape.getId().getNamespace() - ); + ) + "." + convertNamespaceToPascalCase(serviceShape.getId().getNamespace()); } public static JavaAwsSdkV1 createJavaAwsSdkV1( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java index 23c8a8edb0..985f79695b 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 package software.amazon.polymorph.smithyjava.generator.awssdk.v1; +import static software.amazon.polymorph.smithyjava.nameresolver.Dafny.convertNamespaceToPascalCase; import static software.amazon.smithy.utils.StringUtils.capitalize; import com.squareup.javapoet.ClassName; @@ -454,7 +455,7 @@ MethodSpec generateConvertOpaqueError() { CodeBlock memberDeclaration = CodeBlock.of( "$T $L", ParameterizedTypeName.get( - ClassName.get("Wrappers_Compile", "Option"), + ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"), ParameterizedTypeName.get( software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_SEQUENCE_CLASS_NAME, WildcardTypeName.subtypeOf(Character.class) @@ -472,14 +473,14 @@ MethodSpec generateConvertOpaqueError() { "message", ClassName.get(Objects.class), "nativeValue.getMessage()", - ClassName.get("Wrappers_Compile", "Option"), + ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"), stringTypeDescriptor, COMMON_TO_DAFNY_SIMPLE, SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE .get(ShapeType.STRING) .methodName(), "nativeValue.getMessage()", - ClassName.get("Wrappers_Compile", "Option"), + ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"), stringTypeDescriptor ); return MethodSpec diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java index 5cc3b64063..e06b622441 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java @@ -4,6 +4,7 @@ import static software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_TUPLE0_CLASS_NAME; import static software.amazon.polymorph.smithyjava.nameresolver.Constants.SMITHY_API_UNIT; +import static software.amazon.polymorph.smithyjava.nameresolver.Dafny.convertNamespaceToPascalCase; import com.squareup.javapoet.ClassName; import com.squareup.javapoet.CodeBlock; diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java index 0b9185dbe5..3a19a4a4ac 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java @@ -688,7 +688,7 @@ MethodSpec generateConvertOpaqueError() { CodeBlock memberDeclaration = CodeBlock.of( "$T $L", ParameterizedTypeName.get( - ClassName.get("Wrappers_Compile", "Option"), + ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"), ParameterizedTypeName.get( software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_SEQUENCE_CLASS_NAME, WildcardTypeName.subtypeOf(Character.class) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ShimLibrary.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ShimLibrary.java index b21b68755d..b1228943e8 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ShimLibrary.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ShimLibrary.java @@ -18,6 +18,7 @@ import software.amazon.polymorph.smithyjava.generator.Generator; import software.amazon.polymorph.smithyjava.modeled.Operation; import software.amazon.polymorph.smithyjava.nameresolver.Dafny; +import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.polymorph.utils.AwsSdkNameResolverHelpers; import software.amazon.polymorph.utils.ModelUtils; import software.amazon.polymorph.utils.ModelUtils.ResolvedShapeId; diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ResourceShim.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ResourceShim.java index 7113e91f91..724dad3641 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ResourceShim.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ResourceShim.java @@ -27,7 +27,7 @@ import software.amazon.polymorph.smithyjava.nameresolver.Dafny; import software.amazon.polymorph.smithyjava.nameresolver.Native; import software.amazon.polymorph.traits.ExtendableTrait; -import software.amazon.polymorph.utils.ModelUtils; +import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.smithy.model.shapes.OperationShape; import software.amazon.smithy.model.shapes.ResourceShape; @@ -89,7 +89,9 @@ TypeSpec shim() { .addMethod(resourceAsDafny()) .addMethod(resourceAsNativeInterface()) .addMethod(impl()); - ModelUtils.getDocumentationOrJavadoc(targetShape).map(spec::addJavadoc); + targetShape + .getTrait(JavaDocTrait.class) + .map(docTrait -> spec.addJavadoc(docTrait.getValue())); spec.addMethods( getOperationsForTarget() .stream() diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java index 063a9acff0..724866a5f2 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java @@ -13,6 +13,8 @@ import com.squareup.javapoet.TypeSpec; import java.util.Collections; import java.util.List; +import java.util.Objects; +import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; import software.amazon.polymorph.smithyjava.BuildMethod; @@ -21,8 +23,8 @@ import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; import software.amazon.polymorph.smithyjava.generator.library.ShimLibrary; import software.amazon.polymorph.smithyjava.nameresolver.Dafny; +import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.polymorph.traits.LocalServiceTrait; -import software.amazon.polymorph.utils.ModelUtils; import software.amazon.smithy.model.shapes.ServiceShape; public class ServiceShim extends ShimLibrary { @@ -60,7 +62,9 @@ protected TypeSpec shim() { shimArgs, Collections.emptyList() ); - ModelUtils.getDocumentationOrJavadoc(targetShape).map(spec::addJavadoc); + targetShape + .getTrait(JavaDocTrait.class) + .map(docTrait -> spec.addJavadoc(docTrait.getValue())); spec .addType(builderSpecs.builderInterface()) .addType( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledEnum.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledEnum.java index 73f20c3804..4ea6bd6db2 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledEnum.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledEnum.java @@ -11,7 +11,7 @@ import com.squareup.javapoet.JavaFile; import com.squareup.javapoet.MethodSpec; import com.squareup.javapoet.TypeSpec; -import software.amazon.polymorph.utils.ModelUtils; +import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.smithy.model.shapes.Shape; import software.amazon.smithy.model.traits.EnumDefinition; import software.amazon.smithy.model.traits.EnumTrait; @@ -44,7 +44,9 @@ public static JavaFile javaFile(String packageName, Shape shape) { enumSpec.addField(ENUM_VALUE_FIELD); enumSpec.addMethod(constructor()); enumSpec.addMethod(toStringMethod()); - ModelUtils.getDocumentationOrJavadoc(shape).map(enumSpec::addJavadoc); + shape + .getTrait(JavaDocTrait.class) + .map(docTrait -> enumSpec.addJavadoc(docTrait.getValue())); return JavaFile .builder(packageName, enumSpec.build()) .skipJavaLangImports(true) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledError.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledError.java index a95f699065..d69e73b1d8 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledError.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledError.java @@ -19,7 +19,7 @@ import software.amazon.polymorph.smithyjava.BuilderSpecs; import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; import software.amazon.polymorph.smithyjava.unmodeled.ErrorHelpers; -import software.amazon.polymorph.utils.ModelUtils; +import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.smithy.model.shapes.StructureShape; public class ModeledError { @@ -55,7 +55,9 @@ public static JavaFile javaFile( .classBuilder(className) .addModifiers(Modifier.PUBLIC) .superclass(superName); - ModelUtils.getDocumentationOrJavadoc(shape).map(spec::addJavadoc); + shape + .getTrait(JavaDocTrait.class) + .map(docTrait -> spec.addJavadoc(docTrait.getValue())); localOnlyFields.forEach(field -> { // Add local fields spec.addField(field.toFieldSpec(PRIVATE, FINAL)); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledStructure.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledStructure.java index feddd40647..a639db1330 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledStructure.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledStructure.java @@ -19,7 +19,7 @@ import software.amazon.polymorph.smithyjava.BuilderMemberSpec; import software.amazon.polymorph.smithyjava.BuilderSpecs; import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; -import software.amazon.polymorph.utils.ModelUtils; +import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.smithy.model.shapes.Shape; public class ModeledStructure { @@ -77,7 +77,9 @@ public static JavaFile javaFile( .addModifiers(Modifier.PUBLIC) .addType(builderInterface) .addType(builderImpl); - ModelUtils.getDocumentationOrJavadoc(shape).map(spec::addJavadoc); + shape + .getTrait(JavaDocTrait.class) + .map(docTrait -> spec.addJavadoc(docTrait.getValue())); modelFields.forEach(field -> { // Add fields spec.addField(field.toFieldSpec(PRIVATE, FINAL)); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java index ab2d8264f9..397ab92f7d 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java @@ -16,11 +16,11 @@ public class Constants { "Unit" ); public static final ClassName DAFNY_OPTION_CLASS_NAME = ClassName.get( - "Wrappers_Compile", + "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option" ); public static final ClassName DAFNY_RESULT_CLASS_NAME = ClassName.get( - "Wrappers_Compile", + "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Result" ); public static final ClassName DAFNY_TUPLE0_CLASS_NAME = ClassName.get( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java index 64f53a3d74..c9692067ee 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java @@ -11,8 +11,10 @@ import com.squareup.javapoet.WildcardTypeName; import java.math.BigDecimal; import java.math.BigInteger; +import java.util.Arrays; import java.util.Map; import java.util.Objects; +import java.util.stream.Collectors; import javax.annotation.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -174,13 +176,13 @@ public CodeBlock createNone(CodeBlock typeDescriptor) { if (datatypeConstructorsNeedTypeDescriptors()) { return CodeBlock.of( "$T.create_None($L)", - ClassName.get("Wrappers_Compile", "Option"), + ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"), typeDescriptor ); } else { return CodeBlock.of( "$T.create_None()", - ClassName.get("Wrappers_Compile", "Option") + ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option") ); } } @@ -277,6 +279,13 @@ public static String aggregateSizeMethod(ShapeType shapeType) { }; } + public static String convertNamespaceToPascalCase(final String namespace) { + String camelCase = Arrays.stream(namespace.split("\\.")) + .map(part -> Character.toUpperCase(part.charAt(0)) + part.substring(1).toLowerCase()) + .collect(Collectors.joining()); + return camelCase; + } + static String modelPackageNameForNamespace(final String namespace) { return DafnyNameResolverHelpers.dafnyExternNamespaceForNamespace(namespace); } From 5b9d395fa78a75bccc3612112f6da4b70a166803 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 2 Jul 2024 16:02:32 -0700 Subject: [PATCH 2/5] cleanup --- .../smithydafny/DafnyApiCodegen.java | 141 +++++++++++++++--- .../smithyjava/BuilderMemberSpec.java | 27 ++-- .../smithyjava/OperationJavaDoc.java | 23 ++- .../generator/library/shims/ResourceShim.java | 6 +- .../generator/library/shims/ServiceShim.java | 8 +- .../smithyjava/modeled/ModeledEnum.java | 6 +- .../smithyjava/modeled/ModeledError.java | 6 +- .../smithyjava/modeled/ModeledStructure.java | 6 +- 8 files changed, 151 insertions(+), 72 deletions(-) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java index cf8878b7d3..4656098f54 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java @@ -129,7 +129,10 @@ public Map generate() { namespace ); final TokenTree typesModuleHeader = Token.of( - "module {:extern \"types\"} %s".formatted( + "module {:extern \"%s\" } %s".formatted( + DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId( + serviceShape.getId() + ), typesModuleName ) ); @@ -853,24 +856,26 @@ private TokenTree generateBodilessOperationMethodThatEnsuresCallEvents( .parenthesized() ), generateOperationReturnsClause(serviceShape, operationShape), - isFunction - ? TokenTree.of( - "// Functions that are transparent do not need ensures" - ) - : TokenTree - .of( - generateMutableInvariantForMethod( - serviceShape, - operationShapeId, - implementationType - ), - generateEnsuresForEnsuresPubliclyPredicate(operationShapeId), - !implementationType.equals(ImplementationType.ABSTRACT) - ? generateEnsuresHistoricalCallEvents(operationShapeId) - : TokenTree.empty() + implementationType.equals(ImplementationType.DEVELOPER) + ? TokenTree.empty() + : isFunction + ? TokenTree.of( + "// Functions that are transparent do not need ensures" ) - .dropEmpty() - .lineSeparated() + : TokenTree + .of( + generateMutableInvariantForMethod( + serviceShape, + operationShapeId, + implementationType + ), + generateEnsuresForEnsuresPubliclyPredicate(operationShapeId), + !implementationType.equals(ImplementationType.ABSTRACT) + ? generateEnsuresHistoricalCallEvents(operationShapeId) + : TokenTree.empty() + ) + .dropEmpty() + .lineSeparated() ) .lineSeparated(); return TokenTree @@ -880,9 +885,15 @@ private TokenTree generateBodilessOperationMethodThatEnsuresCallEvents( // so that other callers can compose // and add bodies. TokenTree.of( - !implementationType.equals(ImplementationType.ABSTRACT) - ? "// The public method to be called by library consumers" - : "// The private method to be refined by the library developer" + switch (implementationType) { + case CODEGEN -> TokenTree.of( + "// The public method to be called by library consumers" + ); + case ABSTRACT -> TokenTree.of( + "// The private method to be refined by the library developer" + ); + case DEVELOPER -> TokenTree.empty(); + } ), operationMethod ) @@ -2760,4 +2771,92 @@ private TokenTree generateAbstractOperationsModule( return TokenTree.of(header, body); } + + public Map generateSkeleton() { + final String namespace = serviceShape.getId().getNamespace(); + final String sdkID = serviceShape + .expectTrait(LocalServiceTrait.class) + .getSdkId(); + final String typesModuleName = DafnyNameResolver.dafnyTypesModuleName( + namespace + ); + final Path path = Path.of("%sImpl.dfy".formatted(sdkID)); + TokenTree includeDirectives = TokenTree.of( + "include \"../Model/%s.dfy\"".formatted(typesModuleName) + ); + TokenTree concreteModuleTemplate = generateTemplateOperationsModule( + serviceShape + ); + final TokenTree fullCode = TokenTree + .of(includeDirectives, concreteModuleTemplate) + .lineSeparated(); + return Map.of(path, fullCode); + } + + private TokenTree generateTemplateOperationsModule( + final ServiceShape serviceShape + ) { + final String baseModuleName = DafnyNameResolver.dafnyBaseModuleName( + serviceShape.getId().getNamespace() + ); + final TokenTree header = TokenTree.of( + "module %sImpl refines Abstract%sOperations".formatted( + baseModuleName, + baseModuleName + ) + ); + + final String internalConfigType = DafnyNameResolver.internalConfigType(); + + final TokenTree body = TokenTree + .of( + TokenTree.of("datatype Config = Config"), + TokenTree.of("type %s = Config".formatted(internalConfigType)), + TokenTree.of( + "predicate %s(config: %s)".formatted( + DafnyNameResolver.validConfigPredicate(), + internalConfigType + ) + ), + TokenTree.of("{true}"), + TokenTree.of( + "function %s(config: %s): set".formatted( + DafnyNameResolver.modifiesInternalConfig(), + internalConfigType + ) + ), + TokenTree.of("{{}}"), + TokenTree + .of( + serviceShape + .getAllOperations() + .stream() + .map(operation -> + TokenTree + .of( + generateEnsuresPubliclyPredicate(serviceShape, operation), + TokenTree.of("{true}"), + generateBodilessOperationMethodThatEnsuresCallEvents( + serviceShape, + operation, + ImplementationType.DEVELOPER + ), + TokenTree.of("{"), + TokenTree.of( + " expect false, \"...that you'll fill this in\";" + ), + TokenTree.of("}") + ) + .flatten() + .lineSeparated() + ) + ) + .lineSeparated() + ) + .flatten() + .lineSeparated() + .braced(); + + return TokenTree.of(header, body); + } } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java index f09dca461a..ccba829424 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java @@ -18,13 +18,12 @@ import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; import software.amazon.polymorph.smithyjava.nameresolver.Native; import software.amazon.polymorph.smithyjava.unmodeled.CollectionOfErrors; -import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.polymorph.traits.LocalServiceTrait; +import software.amazon.polymorph.utils.ModelUtils; import software.amazon.polymorph.utils.ModelUtils.ResolvedShapeId; import software.amazon.smithy.model.shapes.MemberShape; import software.amazon.smithy.model.shapes.Shape; import software.amazon.smithy.model.shapes.StructureShape; -import software.amazon.smithy.model.traits.StringTrait; // TODO: We can shrink our code base by combining // BuilderMemberSpec w/ PolymorphFieldSpec. @@ -117,11 +116,11 @@ public BuilderMemberSpec(MemberShape memberShape, JavaLibrary subject) { this.interfaceType = null; this.wrapCall = null; } - Optional maybeJavaDoc = memberShape.getMemberTrait( - subject.model, - JavaDocTrait.class - ); - this.javaDoc = maybeJavaDoc.map(StringTrait::getValue).orElse(null); + this.javaDoc = + ModelUtils + .getDocumentationOrJavadoc(memberShape) + .or(() -> ModelUtils.getDocumentationOrJavadoc(resolvedShape)) + .orElse(null); } /** Private Method for handling Edge Cases or cases where @@ -153,10 +152,9 @@ public static BuilderMemberSpec localServiceConfigMemberSpec( trait.getConfigId(), StructureShape.class ); - Optional maybeJavaDoc = structureShape.getTrait( - JavaDocTrait.class - ); - String javaDoc = maybeJavaDoc.map(StringTrait::getValue).orElse(null); + String javaDoc = ModelUtils + .getDocumentationOrJavadoc(structureShape) + .orElse(null); return new BuilderMemberSpec(type, name, javaDoc); } @@ -167,10 +165,9 @@ public static BuilderMemberSpec localServiceAsMemberSpec( subject.serviceShape ); String name = INTERFACE_VAR; - Optional maybeJavaDoc = subject.serviceShape.getTrait( - JavaDocTrait.class - ); - String javaDoc = maybeJavaDoc.map(StringTrait::getValue).orElse(null); + String javaDoc = ModelUtils + .getDocumentationOrJavadoc(subject.serviceShape) + .orElse(null); return new BuilderMemberSpec(type, name, javaDoc); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/OperationJavaDoc.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/OperationJavaDoc.java index 173212f724..e2fcd0c597 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/OperationJavaDoc.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/OperationJavaDoc.java @@ -10,10 +10,10 @@ import javax.annotation.Nullable; import software.amazon.awssdk.utils.Pair; import software.amazon.awssdk.utils.StringUtils; -import software.amazon.polymorph.traits.JavaDocTrait; +import software.amazon.polymorph.utils.ModelUtils; import software.amazon.smithy.model.Model; import software.amazon.smithy.model.shapes.OperationShape; -import software.amazon.smithy.model.traits.StringTrait; +import software.amazon.smithy.model.shapes.Shape; /** * @param desc JavaDoc Body content @@ -66,25 +66,20 @@ public static OperationJavaDoc fromOperationShape( Model model, OperationShape shape ) { + Shape inputShape = model.expectShape(shape.getInputShape()); @Nullable - String paramDoc = model - .expectShape(shape.getInputShape()) - .getMemberTrait(model, JavaDocTrait.class) - .map(StringTrait::getValue) + String paramDoc = ModelUtils + .getDocumentationOrJavadoc(inputShape) .orElse(null); @Nonnull String paramName = NATIVE_VAR; + Shape outputShape = model.expectShape(shape.getOutputShape()); @Nullable - String returns = model - .expectShape(shape.getOutputShape()) - .getMemberTrait(model, JavaDocTrait.class) - .map(StringTrait::getValue) + String returns = ModelUtils + .getDocumentationOrJavadoc(outputShape) .orElse(null); @Nullable - String desc = shape - .getTrait(JavaDocTrait.class) - .map(StringTrait::getValue) - .orElse(null); + String desc = ModelUtils.getDocumentationOrJavadoc(shape).orElse(null); List> params = StringUtils.isNotBlank(paramDoc) ? List.of(Pair.of(paramName, paramDoc)) : null; diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ResourceShim.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ResourceShim.java index 724dad3641..7113e91f91 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ResourceShim.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ResourceShim.java @@ -27,7 +27,7 @@ import software.amazon.polymorph.smithyjava.nameresolver.Dafny; import software.amazon.polymorph.smithyjava.nameresolver.Native; import software.amazon.polymorph.traits.ExtendableTrait; -import software.amazon.polymorph.traits.JavaDocTrait; +import software.amazon.polymorph.utils.ModelUtils; import software.amazon.smithy.model.shapes.OperationShape; import software.amazon.smithy.model.shapes.ResourceShape; @@ -89,9 +89,7 @@ TypeSpec shim() { .addMethod(resourceAsDafny()) .addMethod(resourceAsNativeInterface()) .addMethod(impl()); - targetShape - .getTrait(JavaDocTrait.class) - .map(docTrait -> spec.addJavadoc(docTrait.getValue())); + ModelUtils.getDocumentationOrJavadoc(targetShape).map(spec::addJavadoc); spec.addMethods( getOperationsForTarget() .stream() diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java index 724866a5f2..063a9acff0 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/shims/ServiceShim.java @@ -13,8 +13,6 @@ import com.squareup.javapoet.TypeSpec; import java.util.Collections; import java.util.List; -import java.util.Objects; -import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; import software.amazon.polymorph.smithyjava.BuildMethod; @@ -23,8 +21,8 @@ import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; import software.amazon.polymorph.smithyjava.generator.library.ShimLibrary; import software.amazon.polymorph.smithyjava.nameresolver.Dafny; -import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.polymorph.traits.LocalServiceTrait; +import software.amazon.polymorph.utils.ModelUtils; import software.amazon.smithy.model.shapes.ServiceShape; public class ServiceShim extends ShimLibrary { @@ -62,9 +60,7 @@ protected TypeSpec shim() { shimArgs, Collections.emptyList() ); - targetShape - .getTrait(JavaDocTrait.class) - .map(docTrait -> spec.addJavadoc(docTrait.getValue())); + ModelUtils.getDocumentationOrJavadoc(targetShape).map(spec::addJavadoc); spec .addType(builderSpecs.builderInterface()) .addType( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledEnum.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledEnum.java index 4ea6bd6db2..73f20c3804 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledEnum.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledEnum.java @@ -11,7 +11,7 @@ import com.squareup.javapoet.JavaFile; import com.squareup.javapoet.MethodSpec; import com.squareup.javapoet.TypeSpec; -import software.amazon.polymorph.traits.JavaDocTrait; +import software.amazon.polymorph.utils.ModelUtils; import software.amazon.smithy.model.shapes.Shape; import software.amazon.smithy.model.traits.EnumDefinition; import software.amazon.smithy.model.traits.EnumTrait; @@ -44,9 +44,7 @@ public static JavaFile javaFile(String packageName, Shape shape) { enumSpec.addField(ENUM_VALUE_FIELD); enumSpec.addMethod(constructor()); enumSpec.addMethod(toStringMethod()); - shape - .getTrait(JavaDocTrait.class) - .map(docTrait -> enumSpec.addJavadoc(docTrait.getValue())); + ModelUtils.getDocumentationOrJavadoc(shape).map(enumSpec::addJavadoc); return JavaFile .builder(packageName, enumSpec.build()) .skipJavaLangImports(true) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledError.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledError.java index d69e73b1d8..a95f699065 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledError.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledError.java @@ -19,7 +19,7 @@ import software.amazon.polymorph.smithyjava.BuilderSpecs; import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; import software.amazon.polymorph.smithyjava.unmodeled.ErrorHelpers; -import software.amazon.polymorph.traits.JavaDocTrait; +import software.amazon.polymorph.utils.ModelUtils; import software.amazon.smithy.model.shapes.StructureShape; public class ModeledError { @@ -55,9 +55,7 @@ public static JavaFile javaFile( .classBuilder(className) .addModifiers(Modifier.PUBLIC) .superclass(superName); - shape - .getTrait(JavaDocTrait.class) - .map(docTrait -> spec.addJavadoc(docTrait.getValue())); + ModelUtils.getDocumentationOrJavadoc(shape).map(spec::addJavadoc); localOnlyFields.forEach(field -> { // Add local fields spec.addField(field.toFieldSpec(PRIVATE, FINAL)); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledStructure.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledStructure.java index a639db1330..feddd40647 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledStructure.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/ModeledStructure.java @@ -19,7 +19,7 @@ import software.amazon.polymorph.smithyjava.BuilderMemberSpec; import software.amazon.polymorph.smithyjava.BuilderSpecs; import software.amazon.polymorph.smithyjava.generator.library.JavaLibrary; -import software.amazon.polymorph.traits.JavaDocTrait; +import software.amazon.polymorph.utils.ModelUtils; import software.amazon.smithy.model.shapes.Shape; public class ModeledStructure { @@ -77,9 +77,7 @@ public static JavaFile javaFile( .addModifiers(Modifier.PUBLIC) .addType(builderInterface) .addType(builderImpl); - shape - .getTrait(JavaDocTrait.class) - .map(docTrait -> spec.addJavadoc(docTrait.getValue())); + ModelUtils.getDocumentationOrJavadoc(shape).map(spec::addJavadoc); modelFields.forEach(field -> { // Add fields spec.addField(field.toFieldSpec(PRIVATE, FINAL)); From 2408436aba3d6b10194c972020c7e31d512f3fab Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 2 Jul 2024 16:03:16 -0700 Subject: [PATCH 3/5] cleanup --- Makefile | 3 +++ TestModels/Constraints/Makefile | 7 ------ .../internaldafny/types/__default.java | 6 ++--- TestModels/Constraints/src/Index.dfy | 2 +- .../StandardLibrary/Makefile | 23 ------------------- .../smithydafny/DafnyApiCodegen.java | 5 +--- .../LocalServiceWrappedCodegen.java | 2 -- .../generator/awssdk/v1/ToDafnyAwsV1.java | 1 - .../generator/awssdk/v2/ShimV2.java | 1 - .../generator/library/ShimLibrary.java | 1 - 10 files changed, 8 insertions(+), 43 deletions(-) diff --git a/Makefile b/Makefile index 58972c4b7e..a049701984 100644 --- a/Makefile +++ b/Makefile @@ -9,3 +9,6 @@ format_java_misc-check: setup_prettier setup_prettier: npm i --no-save prettier@3 prettier-plugin-java@2.5 + + +TestModels/dafny-dependencies/StandardLibrary/runtimes/java TestModels/dafny-dependencies/StandardLibrary/runtimes/net TestModels/dafny-dependencies/StandardLibrary/Makefile TestModels/dafny-dependencies/StandardLibrary/src \ No newline at end of file diff --git a/TestModels/Constraints/Makefile b/TestModels/Constraints/Makefile index 3826dd3ef8..90cbc5e579 100644 --- a/TestModels/Constraints/Makefile +++ b/TestModels/Constraints/Makefile @@ -25,13 +25,6 @@ polymorph: make polymorph_java make polymorph_dotnet -# Python - -PYTHON_MODULE_NAME=simple_constraints - -TRANSLATION_RECORD_PYTHON := \ - --translation-record ../dafny-dependencies/StandardLibrary/runtimes/python/src/standard_library/internaldafny/generated/dafny_src-py.dtr - # Java JAVA_PACKAGE_NAME=simple.constraints diff --git a/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java b/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java index 147f02dbb5..c38f39a7b1 100644 --- a/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java +++ b/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java @@ -1,5 +1,5 @@ -// Class _ExternBase___default -// Dafny class __default compiled into Java +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 package simple.constraints.internaldafny.types; -public abstract class __default extends _ExternBase___default { } +public class __default extends _ExternBase___default { } diff --git a/TestModels/Constraints/src/Index.dfy b/TestModels/Constraints/src/Index.dfy index 2ac9079d68..d3515f35e6 100644 --- a/TestModels/Constraints/src/Index.dfy +++ b/TestModels/Constraints/src/Index.dfy @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 include "SimpleConstraintsImpl.dfy" -module SimpleConstraints refines AbstractSimpleConstraintsService { +module {:extern "SimpleConstraints" } SimpleConstraints refines AbstractSimpleConstraintsService { import Operations = SimpleConstraintsImpl function method DefaultSimpleConstraintsConfig(): SimpleConstraintsConfig { diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile index f95b6af882..c1f5581e63 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -9,7 +9,6 @@ MAX_RESOURCE_COUNT=500000000 PYTHON_MODULE_NAME=standard_library JAVA_PACKAGE_NAME=software.amazon.cryptography.standardlibrary NET_NAMESPACE_NAME=software.amazon.cryptography.standardlibrary -LIBRARIES := # define standard colors ifneq (,$(findstring xterm,${TERM})) @@ -40,9 +39,6 @@ polymorph_dotnet : polymorph_java : echo "Skipping polymorph_java for StandardLibrary" -polymorph_python : - echo "Skipping polymorph_python for StandardLibrary" - # Using this target for the side-effect of maintaining patches, # Since Dafny Rust code generation is incomplete and also needs to be patched. # That only works if you run transpile_rust first. @@ -70,25 +66,6 @@ transpile_net: | transpile_implementation_net transpile_test_net # StandardLibrary as a dependency transpile_java: | transpile_implementation_java transpile_test_java -# Override SharedMakefile's transpile_python to not transpile -# StandardLibrary as a dependency -transpile_python: | transpile_implementation_python transpile_test_python - -# Hacky workaround until Dafny supports per-language extern names. -# Replaces `.`s with `_`s in strings like `{:extern ".*"}`. -# This is flawed logic and should be removed, but is a reasonable band-aid for now. -# TODO: Once Dafny supports per-language extern names, remove and replace with Pythonic extern names. -# This may require new Smithy-Dafny logic to generate Pythonic extern names. -_python_underscore_extern_names: - find src -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/module {:extern \".*\"/s/\./_/g' {} \; - echo "Skipping Model modification for StandardLibrary" - find test -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/module {:extern \".*\"/s/\./_/g' {} \; - -_python_revert_underscore_extern_names: - find src -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/module {:extern \".*\"/s/_/\./g' {} \; - echo "Skipping Model modification for StandardLibrary" - find test -regex ".*\.dfy" -type f -exec sed -i $(SED_PARAMETER) '/module {:extern \".*\"/s/_/\./g' {} \; - ########################## Rust targets # Override SharedMakefile's transpile_java to not transpile # StandardLibrary as a dependency diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java index 4656098f54..002427868b 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java @@ -129,10 +129,7 @@ public Map generate() { namespace ); final TokenTree typesModuleHeader = Token.of( - "module {:extern \"%s\" } %s".formatted( - DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId( - serviceShape.getId() - ), + "module {:extern \"types\"} %s".formatted( typesModuleName ) ); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java index 08ef019557..26b6d75114 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java @@ -15,8 +15,6 @@ import software.amazon.smithy.model.shapes.ResourceShape; import software.amazon.smithy.model.shapes.ServiceShape; -import static software.amazon.polymorph.smithyjava.nameresolver.Dafny.convertNamespaceToPascalCase; - public class LocalServiceWrappedCodegen extends ServiceCodegen { public LocalServiceWrappedCodegen( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java index 985f79695b..a8ba2a2bcc 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 package software.amazon.polymorph.smithyjava.generator.awssdk.v1; -import static software.amazon.polymorph.smithyjava.nameresolver.Dafny.convertNamespaceToPascalCase; import static software.amazon.smithy.utils.StringUtils.capitalize; import com.squareup.javapoet.ClassName; diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java index e06b622441..5cc3b64063 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java @@ -4,7 +4,6 @@ import static software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_TUPLE0_CLASS_NAME; import static software.amazon.polymorph.smithyjava.nameresolver.Constants.SMITHY_API_UNIT; -import static software.amazon.polymorph.smithyjava.nameresolver.Dafny.convertNamespaceToPascalCase; import com.squareup.javapoet.ClassName; import com.squareup.javapoet.CodeBlock; diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ShimLibrary.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ShimLibrary.java index b1228943e8..b21b68755d 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ShimLibrary.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ShimLibrary.java @@ -18,7 +18,6 @@ import software.amazon.polymorph.smithyjava.generator.Generator; import software.amazon.polymorph.smithyjava.modeled.Operation; import software.amazon.polymorph.smithyjava.nameresolver.Dafny; -import software.amazon.polymorph.traits.JavaDocTrait; import software.amazon.polymorph.utils.AwsSdkNameResolverHelpers; import software.amazon.polymorph.utils.ModelUtils; import software.amazon.polymorph.utils.ModelUtils.ResolvedShapeId; From 3f0858c3acb759aa02f71cb6f4661d0af38d231d Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 2 Jul 2024 16:06:21 -0700 Subject: [PATCH 4/5] clenau-p --- Makefile | 5 +- SmithyDafnyMakefile.mk | 79 ++++++++++--------- .../internaldafny/types/__default.java | 2 +- .../StandardLibrary/Makefile | 2 - 4 files changed, 44 insertions(+), 44 deletions(-) diff --git a/Makefile b/Makefile index a049701984..4545a932df 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,4 @@ format_java_misc-check: setup_prettier npx prettier --plugin=prettier-plugin-java . --check setup_prettier: - npm i --no-save prettier@3 prettier-plugin-java@2.5 - - -TestModels/dafny-dependencies/StandardLibrary/runtimes/java TestModels/dafny-dependencies/StandardLibrary/runtimes/net TestModels/dafny-dependencies/StandardLibrary/Makefile TestModels/dafny-dependencies/StandardLibrary/src \ No newline at end of file + npm i --no-save prettier@3 prettier-plugin-java@2.5 \ No newline at end of file diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 6c869e119e..050f03529d 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -39,7 +39,7 @@ VERIFY_TIMEOUT := 100 # This evaluates to the path of the current working directory. # i.e. The specific library under consideration. -LIBRARY_ROOT := $(shell pwd) +LIBRARY_ROOT := $(PWD) # Smithy Dafny code gen needs to know # where the smithy model is. # This is generally in the same directory as the library. @@ -154,7 +154,7 @@ clean-dafny-report: # Transpile the entire project's impl # For each index file listed in the project Makefile's PROJECT_INDEX variable, # append a `-library:TestModels/$(PROJECT_INDEX) to the transpiliation target -_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX)) +_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, --library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX)) _transpile_implementation_all: transpile_implementation # The `$(OUT)` and $(TARGET) variables are problematic. @@ -189,22 +189,21 @@ transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src # `find` looks for `Index.dfy` files in either V1 or V2-styled project directories (single vs. multiple model files). transpile_implementation: find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \ - -stdin \ - -noVerify \ - -vcsCores:$(CORES) \ - -compileTarget:$(TARGET) \ - -spillTargetCode:3 \ - -compile:0 \ - -optimizeErasableDatatypeWrapper:0 \ - -compileSuffix:1 \ - -unicodeChar:0 \ - -functionSyntax:3 \ - -useRuntimeLib \ - -out $(OUT) \ - $(DAFNY_OPTIONS) \ - $(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ + translate $(TARGET) \ + --stdin \ + --no-verify \ + --cores:$(CORES) \ + --optimize-erasable-datatype-wrapper:false \ + --unicode-char:false \ + --function-syntax:3 \ + --allow-warnings \ + --output $(OUT) \ + $(TRANSPILE_MODULE_NAME) \ + $(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ + $(TRANSLATION_RECORD) \ $(TRANSPILE_DEPENDENCIES) + # If the project under transpilation uses `replaceable` modules, # it MUST define a SRC_INDEX variable per language. # The purpose and usage of this is described in the `transpile_implementation` comments. @@ -222,27 +221,26 @@ _transpile_test_all: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),test) # append `-library:/path/to/Index.dfy` to the transpile target # Else: (i.e. single model/service in project), then: # append `-library:/path/to/Index.dfy` to the transpile target -_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, -library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), -library:$(SRC_INDEX_TRANSPILE)/Index.dfy) +_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, --library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), --library:$(SRC_INDEX_TRANSPILE)/Index.dfy) # Transpile the entire project's tests _transpile_test_all: transpile_test # `find` looks for tests in either V1 or V2-styled project directories (single vs. multiple model files). transpile_test: find ./dafny/**/$(TEST_INDEX_TRANSPILE) ./$(TEST_INDEX_TRANSPILE) -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \ - -stdin \ - -noVerify \ - -vcsCores:$(CORES) \ - -compileTarget:$(TARGET) \ - -spillTargetCode:3 \ - -runAllTests:1 \ - -compile:0 \ - -optimizeErasableDatatypeWrapper:0 \ - -compileSuffix:1 \ - -unicodeChar:0 \ - -functionSyntax:3 \ - -useRuntimeLib \ - -out $(OUT) \ - $(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ + translate $(TARGET) \ + --stdin \ + --no-verify \ + --cores:$(CORES) \ + --include-test-runner \ + --optimize-erasable-datatype-wrapper:false \ + --unicode-char:false \ + --function-syntax:3 \ + --allow-warnings \ + --output $(OUT) \ + $(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ + $(TRANSLATION_RECORD) \ + $(SOURCE_TRANSLATION_RECORD) \ $(TRANSPILE_DEPENDENCIES) \ # If we are not the StandardLibrary, transpile the StandardLibrary. @@ -275,10 +273,12 @@ _polymorph: $(OUTPUT_JAVA) \ $(OUTPUT_JAVA_TEST) \ $(OUTPUT_DOTNET) \ + $(MODULE_NAME) \ $(OUTPUT_RUST) \ --model $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(SMITHY_MODEL_ROOT)) \ --dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \ $(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \ + $(DEPENDENCY_MODULE_NAMES) \ --namespace $($(namespace_var)) \ $(OUTPUT_LOCAL_SERVICE_$(SERVICE)) \ $(AWS_SDK_CMD) \ @@ -292,13 +292,14 @@ _polymorph_wrapped: --dafny-version $(DAFNY_VERSION) \ --library-root $(LIBRARY_ROOT) \ --properties-file $(LIBRARY_ROOT)/project.properties \ - $(INPUT_DAFNY) \ $(OUTPUT_DAFNY_WRAPPED) \ $(OUTPUT_DOTNET_WRAPPED) \ $(OUTPUT_JAVA_WRAPPED) \ + $(MODULE_NAME) \ --model $(if $(DIR_STRUCTURE_V2),$(LIBRARY_ROOT)/dafny/$(SERVICE)/Model,$(LIBRARY_ROOT)/Model) \ --dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \ $(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \ + $(DEPENDENCY_MODULE_NAMES) \ --namespace $($(namespace_var)) \ --local-service-test \ $(AWS_SDK_CMD) \ @@ -369,8 +370,6 @@ polymorph_dotnet: _polymorph_dotnet: OUTPUT_DOTNET=\ $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/) -_polymorph_dotnet: INPUT_DAFNY=\ - --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy _polymorph_dotnet: _polymorph # Generates java code for all namespaces in this project @@ -387,8 +386,6 @@ polymorph_java: _polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated _polymorph_java: OUTPUT_JAVA_TEST=--output-java-test $(LIBRARY_ROOT)/runtimes/java/src/test/smithy-generated -_polymorph_java: INPUT_DAFNY=\ - --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy _polymorph_java: _polymorph # Dependency for formatting generating Java code @@ -419,6 +416,8 @@ transpile_net: | transpile_implementation_net transpile_test_net transpile_depen transpile_implementation_net: TARGET=cs transpile_implementation_net: OUT=runtimes/net/ImplementationFromDafny +transpile_implementation_net: TRANSPILE_MODULE_NAME=$(if $(NET_NAMESPACE_NAME),--dotnet-namespace=$(NET_NAMESPACE_NAME).internaldafny,) +transpile_implementation_net: TRANSLATION_RECORD=$(TRANSLATION_RECORD_NET) transpile_implementation_net: SRC_INDEX=$(NET_SRC_INDEX) transpile_implementation_net: _transpile_implementation_all @@ -426,6 +425,8 @@ transpile_test_net: SRC_INDEX=$(NET_SRC_INDEX) transpile_test_net: TEST_INDEX=$(NET_TEST_INDEX) transpile_test_net: TARGET=cs transpile_test_net: OUT=runtimes/net/tests/TestsFromDafny +transpile_test_net: TRANSLATION_RECORD=$(TRANSLATION_RECORD_NET) +transpile_test_net: SOURCE_TRANSLATION_RECORD= --translation-record runtimes/net/ImplementationFromDafny-cs.dtr transpile_test_net: _transpile_test_all transpile_dependencies_net: LANG=net @@ -467,10 +468,14 @@ transpile_java: | transpile_implementation_java transpile_test_java transpile_de transpile_implementation_java: TARGET=java transpile_implementation_java: OUT=runtimes/java/ImplementationFromDafny +transpile_implementation_java: TRANSPILE_MODULE_NAME=$(if $(JAVA_PACKAGE_NAME),--java-package-name=$(JAVA_PACKAGE_NAME).internaldafny,) +transpile_implementation_java: TRANSLATION_RECORD=$(TRANSLATION_RECORD_JAVA) transpile_implementation_java: _transpile_implementation_all _mv_implementation_java transpile_test_java: TARGET=java transpile_test_java: OUT=runtimes/java/TestsFromDafny +transpile_test_java: TRANSLATION_RECORD=$(TRANSLATION_RECORD_JAVA) +transpile_test_java: SOURCE_TRANSLATION_RECORD= --translation-record runtimes/java/src/main/dafny-generated/ImplementationFromDafny-java.dtr transpile_test_java: _transpile_test_all _mv_test_java # Currently Dafny compiles to Java by changing the directory name. @@ -556,7 +561,7 @@ build_rust: test_rust: cd runtimes/rust; \ - cargo test -- --nocapture + cargo test ########################## Cleanup targets diff --git a/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java b/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java index c38f39a7b1..1100632e4b 100644 --- a/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java +++ b/TestModels/Constraints/runtimes/java/src/main/java/simple/constraints/internaldafny/types/__default.java @@ -2,4 +2,4 @@ // SPDX-License-Identifier: Apache-2.0 package simple.constraints.internaldafny.types; -public class __default extends _ExternBase___default { } +public class __default extends _ExternBase___default {} diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile index c1f5581e63..b8f4342e38 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -6,7 +6,6 @@ CORES=2 include ../../SharedMakefile.mk MAX_RESOURCE_COUNT=500000000 -PYTHON_MODULE_NAME=standard_library JAVA_PACKAGE_NAME=software.amazon.cryptography.standardlibrary NET_NAMESPACE_NAME=software.amazon.cryptography.standardlibrary @@ -66,7 +65,6 @@ transpile_net: | transpile_implementation_net transpile_test_net # StandardLibrary as a dependency transpile_java: | transpile_implementation_java transpile_test_java -########################## Rust targets # Override SharedMakefile's transpile_java to not transpile # StandardLibrary as a dependency transpile_rust: | transpile_implementation_rust From 49d8524478e4921fd1b436692fc454af34905b46 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Tue, 2 Jul 2024 16:08:12 -0700 Subject: [PATCH 5/5] cleanup --- Makefile | 2 +- SmithyDafnyMakefile.mk | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 4545a932df..58972c4b7e 100644 --- a/Makefile +++ b/Makefile @@ -8,4 +8,4 @@ format_java_misc-check: setup_prettier npx prettier --plugin=prettier-plugin-java . --check setup_prettier: - npm i --no-save prettier@3 prettier-plugin-java@2.5 \ No newline at end of file + npm i --no-save prettier@3 prettier-plugin-java@2.5 diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 050f03529d..376641d0af 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -39,7 +39,7 @@ VERIFY_TIMEOUT := 100 # This evaluates to the path of the current working directory. # i.e. The specific library under consideration. -LIBRARY_ROOT := $(PWD) +LIBRARY_ROOT := $(shell pwd) # Smithy Dafny code gen needs to know # where the smithy model is. # This is generally in the same directory as the library. @@ -561,7 +561,7 @@ build_rust: test_rust: cd runtimes/rust; \ - cargo test + cargo test -- --nocapture ########################## Cleanup targets