From a1160408ab984ba6c03475bfad4a2f4cca9ce753 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 28 Oct 2023 14:43:41 -0700 Subject: [PATCH] Add dafnyVersion parameter, make type descriptors conditional --- .../amazon/polymorph/CodegenEngine.java | 23 ++++++- .../smithyjava/generator/ToDafny.java | 9 +-- .../generator/awssdk/v1/ShimV1.java | 29 ++++---- .../generator/awssdk/v2/JavaAwsSdkV2.java | 4 +- .../generator/awssdk/v2/ShimV2.java | 29 ++++---- .../generator/awssdk/v2/ToDafnyAwsV2.java | 15 ++-- .../generator/library/JavaLibrary.java | 8 +-- .../generator/library/TestJavaLibrary.java | 4 +- .../smithyjava/modeled/Operation.java | 22 +++--- .../nameresolver/AwsSdkDafnyV1.java | 4 +- .../nameresolver/AwsSdkDafnyV2.java | 4 +- .../smithyjava/nameresolver/Constants.java | 1 + .../smithyjava/nameresolver/Dafny.java | 69 ++++++++++++++++++- .../DafnyClientCodegenPluginSettings.java | 17 ++++- .../smithyjava/ForEachDafnyTest.java | 19 +++++ .../generator/awssdk/TestSetupUtils.java | 8 +-- .../generator/awssdk/v2/ShimTest.java | 10 +-- .../generator/awssdk/v2/ToDafnyAwsV2Test.java | 16 +++-- .../generator/awssdk/v2/ToNativeTest.java | 18 +++-- .../generator/library/ModelCodegenTest.java | 8 +-- .../smithyjava/nameresolver/DafnyTest.java | 13 ++-- 21 files changed, 233 insertions(+), 97 deletions(-) create mode 100644 codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/ForEachDafnyTest.java diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java index 556d075111..4785710f60 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java @@ -41,6 +41,7 @@ public class CodegenEngine { private final Path[] dependentModelPaths; private final String namespace; private final Map targetLangOutputDirs; + private final String dafnyVersion; // refactor this to only be required if generating Java private final AwsSdkVersion javaAwsSdkVersion; private final Optional includeDafnyFile; @@ -62,6 +63,7 @@ private CodegenEngine( final Path[] dependentModelPaths, final String namespace, final Map targetLangOutputDirs, + final String dafnyVersion, final AwsSdkVersion javaAwsSdkVersion, final Optional includeDafnyFile, final boolean awsSdkStyle, @@ -72,6 +74,7 @@ private CodegenEngine( this.dependentModelPaths = dependentModelPaths; this.namespace = namespace; this.targetLangOutputDirs = targetLangOutputDirs; + this.dafnyVersion = dafnyVersion; this.javaAwsSdkVersion = javaAwsSdkVersion; this.includeDafnyFile = includeDafnyFile; this.awsSdkStyle = awsSdkStyle; @@ -150,13 +153,13 @@ private void generateJava(final Path outputDir) { } private void javaLocalService(final Path outputDir) { - final JavaLibrary javaLibrary = new JavaLibrary(this.model, this.serviceShape, this.javaAwsSdkVersion); + final JavaLibrary javaLibrary = new JavaLibrary(this.model, this.serviceShape, this.javaAwsSdkVersion, this.dafnyVersion); IOUtils.writeTokenTreesIntoDir(javaLibrary.generate(), outputDir); LOGGER.info("Java code generated in {}", outputDir); } private void javaWrappedLocalService(final Path outputDir) { - final TestJavaLibrary testJavaLibrary = new TestJavaLibrary(model, serviceShape, this.javaAwsSdkVersion); + final TestJavaLibrary testJavaLibrary = new TestJavaLibrary(model, serviceShape, this.javaAwsSdkVersion, this.dafnyVersion); IOUtils.writeTokenTreesIntoDir(testJavaLibrary.generate(), outputDir); LOGGER.info("Java that tests a local service generated in {}", outputDir); } @@ -168,7 +171,7 @@ private void javaAwsSdkV1(Path outputDir) { } private void javaAwsSdkV2(final Path outputDir) { - final JavaAwsSdkV2 javaV2ShimCodegen = JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, model); + final JavaAwsSdkV2 javaV2ShimCodegen = JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, model, dafnyVersion); IOUtils.writeTokenTreesIntoDir(javaV2ShimCodegen.generate(), outputDir); LOGGER.info("Java V2 code generated in {}", outputDir); } @@ -245,6 +248,7 @@ public static class Builder { private Path[] dependentModelPaths; private String namespace; private Map targetLangOutputDirs; + private String dafnyVersion = "4.1.0"; private AwsSdkVersion javaAwsSdkVersion = AwsSdkVersion.V2; private Path includeDafnyFile; private boolean awsSdkStyle = false; @@ -286,6 +290,17 @@ public Builder withTargetLangOutputDirs(final Map targetLa return this; } + /** + * Sets the Dafny version for which generated code should be compatible. + * This is used to ensure both Dafny source compatibility + * and compatibility with the Dafny compiler and runtime internals, + * which shim code generation currently depends on. + */ + public Builder withDafnyVersion(final String dafnyVersion) { + this.dafnyVersion = dafnyVersion; + return this; + } + /** * Sets the version of the AWS SDK for Java for which generated code should be compatible. * This has no effect unless the engine is configured to generate Java code. @@ -341,6 +356,7 @@ public CodegenEngine build() { targetLangOutputDirsRaw.replaceAll((_lang, path) -> path.toAbsolutePath().normalize()); final Map targetLangOutputDirs = ImmutableMap.copyOf(targetLangOutputDirsRaw); + final String dafnyVersion = Objects.requireNonNull(this.dafnyVersion); final AwsSdkVersion javaAwsSdkVersion = Objects.requireNonNull(this.javaAwsSdkVersion); if (targetLangOutputDirs.containsKey(TargetLanguage.DAFNY) @@ -360,6 +376,7 @@ public CodegenEngine build() { dependentModelPaths, this.namespace, targetLangOutputDirs, + dafnyVersion, javaAwsSdkVersion, includeDafnyFile, this.awsSdkStyle, 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 c8af80d9a1..18908b869d 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 @@ -196,14 +196,11 @@ protected CodeBlock memberAssign( } CodeBlock typeDescriptor = subject.dafnyNameResolver.typeDescriptor(memberShape.getTarget()); return CodeBlock.of( - "$L = $L ?\n$T.create_Some($L, $L)\n: $T.create_None($L)", + "$L = $L ?\n$L\n: $L", outputVar, isSetCheck, - ClassName.get("Wrappers_Compile", "Option"), - typeDescriptor, - memberConversion, - ClassName.get("Wrappers_Compile", "Option"), - typeDescriptor + subject.dafnyNameResolver.createSome(typeDescriptor, memberConversion), + subject.dafnyNameResolver.createNone(typeDescriptor) ); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java index 8d36456b7f..6fa12edf57 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java @@ -144,10 +144,10 @@ Optional operation(final ShapeId operationShapeId) { successTypeDescriptor = CodeBlock.of(DAFNY_TUPLE0_CLASS_NAME + "._typeDescriptor()"); builder.addStatement("_impl.$L(converted)", StringUtils.uncapitalize(operationName)) - .addStatement("return $T.create_Success($L, Error._typeDescriptor(), $T.create())", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor, - DAFNY_TUPLE0_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME))); } else { successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputShapeId); builder.addStatement("$T result = _impl.$L(converted)", @@ -156,23 +156,26 @@ Optional operation(final ShapeId operationShapeId) { .addStatement("$T dafnyResponse = ToDafny.$L(result)", dafnyOutput, StringUtils.capitalize(outputShapeId.getName())) - .addStatement("return $T.create_Success($L, Error._typeDescriptor(), dafnyResponse)", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("dafnyResponse"))); } operationShape.getErrors().stream().sorted().forEach(shapeId -> builder .nextControlFlow("catch ($T ex)", subject.nativeNameResolver.typeForShape(shapeId)) - .addStatement("return $T.create_Failure($L, Error._typeDescriptor(), ToDafny.Error(ex))", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor) + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("ToDafny.Error(ex)"))) ); return Optional.of(builder .nextControlFlow("catch ($T ex)", subject.nativeNameResolver.baseErrorForService()) - .addStatement("return $T.create_Failure($L, Error._typeDescriptor(), ToDafny.Error(ex))", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor) + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("ToDafny.Error(ex)"))) .endControlFlow() .build()); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java index 28e45b6a28..4651bda803 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java @@ -47,8 +47,8 @@ private JavaAwsSdkV2( this.packageName = dafnyNameResolver.packageName(); } - public static JavaAwsSdkV2 createJavaAwsSdkV2(ServiceShape serviceShape, Model model) { - final AwsSdkDafnyV2 dafnyNameResolver = new AwsSdkDafnyV2(serviceShape, model); + public static JavaAwsSdkV2 createJavaAwsSdkV2(ServiceShape serviceShape, Model model, String dafnyVersion) { + final AwsSdkDafnyV2 dafnyNameResolver = new AwsSdkDafnyV2(serviceShape, model, dafnyVersion); final AwsSdkNativeV2 nativeNameResolver = new AwsSdkNativeV2(serviceShape, model); return new JavaAwsSdkV2(serviceShape, model, dafnyNameResolver, nativeNameResolver); } 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 a17c8d6395..e36eb3ee03 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 @@ -144,10 +144,10 @@ Optional operation(final ShapeId operationShapeId) { successTypeDescriptor = CodeBlock.of(DAFNY_TUPLE0_CLASS_NAME + "._typeDescriptor()"); builder.addStatement("_impl.$L(converted)", StringUtils.uncapitalize(operationName)) - .addStatement("return $T.create_Success($L, Error._typeDescriptor(), $T.create())", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor, - DAFNY_TUPLE0_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME))); } else { successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputShapeId); builder.addStatement("$T result = _impl.$L(converted)", @@ -156,9 +156,10 @@ Optional operation(final ShapeId operationShapeId) { .addStatement("$T dafnyResponse = ToDafny.$L(result)", dafnyOutput, StringUtils.capitalize(outputShapeId.getName())) - .addStatement("return $T.create_Success($L, Error._typeDescriptor(), dafnyResponse)", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("dafnyResponse"))); } operationShape.getErrors().stream().sorted().forEach(shapeId -> { @@ -171,15 +172,17 @@ Optional operation(final ShapeId operationShapeId) { builder .nextControlFlow("catch ($T ex)", subject.nativeNameResolver.typeForShape(shapeId)) - .addStatement("return $T.create_Failure($L, Error._typeDescriptor(), ToDafny.Error(ex))", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor); + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("ToDafny.Error(ex)"))); }); return Optional.of(builder .nextControlFlow("catch ($T ex)", subject.nativeNameResolver.baseErrorForService()) - .addStatement("return $T.create_Failure($L, Error._typeDescriptor(), ToDafny.Error(ex))", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor) + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("ToDafny.Error(ex)"))) .endControlFlow() .build()); } 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 4416cb78a5..1d830b5d4e 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 @@ -522,17 +522,16 @@ MethodSpec generateConvertOpaqueError() { // but with calls to dafnyNameResolver replaced with their expected response. CodeBlock stringTypeDescriptor = Dafny.TYPE_DESCRIPTOR_BY_SHAPE_TYPE.get(ShapeType.STRING); CodeBlock memberAssignment = CodeBlock.of( - "$L = $T.nonNull($L) ?\n$T.create_Some($L, $T.$L($L))\n: $T.create_None($L)", + "$L = $T.nonNull($L) ?\n$L\n: $L", "message", ClassName.get(Objects.class), "nativeValue.getMessage()", - ClassName.get("Wrappers_Compile", "Option"), - stringTypeDescriptor, - COMMON_TO_DAFNY_SIMPLE, - SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE.get(ShapeType.STRING).methodName(), - "nativeValue.getMessage()", - ClassName.get("Wrappers_Compile", "Option"), - stringTypeDescriptor + subject.dafnyNameResolver.createSome(stringTypeDescriptor, + CodeBlock.of("$T.$L($L)", + COMMON_TO_DAFNY_SIMPLE, + SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE.get(ShapeType.STRING).methodName(), + "nativeValue.getMessage()")), + subject.dafnyNameResolver.createNone(stringTypeDescriptor) ); return MethodSpec.methodBuilder("Error") .addModifiers(Modifier.PUBLIC, Modifier.STATIC) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java index 4c29f856fd..4b8c332d6a 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java @@ -61,8 +61,8 @@ public class JavaLibrary extends CodegenSubject { public final ToDafnyLibrary toDafnyLibrary; public final ToNativeLibrary toNativeLibrary; - public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion) { - super(model, serviceShape, initDafny(model, serviceShape, sdkVersion), initNative(model, serviceShape, sdkVersion), sdkVersion); + public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion, String dafnyVersion) { + super(model, serviceShape, initDafny(model, serviceShape, sdkVersion, dafnyVersion), initNative(model, serviceShape, sdkVersion), sdkVersion); packageName = NamespaceHelper.standardize(serviceShape.getId().getNamespace()); modelPackageName = packageName + ".model"; try { @@ -77,9 +77,9 @@ public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVers toNativeLibrary = new ToNativeLibrary(this); } - static Dafny initDafny(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion) { + static Dafny initDafny(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion, String dafnyVersion) { String packageName = DafnyNameResolverHelpers.packageNameForNamespace(serviceShape.getId().getNamespace()); - return new Dafny(packageName, model, serviceShape, awsSdkVersion); + return new Dafny(packageName, model, serviceShape, awsSdkVersion, dafnyVersion); } static Native initNative(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion) { diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java index d2926fc389..34b06c7d8c 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java @@ -19,8 +19,8 @@ public class TestJavaLibrary extends JavaLibrary { @SuppressWarnings("unused") private static final Logger LOGGER = LoggerFactory.getLogger(TestJavaLibrary.class); - public TestJavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion) { - super(model, serviceShape, sdkVersion); + public TestJavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion, String dafnyVersion) { + super(model, serviceShape, sdkVersion, dafnyVersion); } @Override diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java index e58a880284..ef75c12832 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java @@ -63,10 +63,10 @@ public static MethodSpec operation( successTypeDescriptor = CodeBlock.of("dafny.Tuple0._typeDescriptor()"); method .addStatement(invoke(operationName)) - .addStatement("return $T.create_Success($L, Error._typeDescriptor(), $T.create())", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor, - DAFNY_TUPLE0_CLASS_NAME); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME))); } else { // operation is not void successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputResolved.resolvedId()); @@ -74,17 +74,19 @@ public static MethodSpec operation( method .addStatement(declareNativeOutputAndInvoke(operationName, nativeOutputType)) .addStatement(declareDafnyOutputAndConvert(outputResolved, subject)) - .addStatement("return $T.create_Success($L, Error._typeDescriptor(), $L)", - DAFNY_RESULT_CLASS_NAME, - successTypeDescriptor, - DAFNY_OUTPUT); + .addStatement("return $L", + subject.dafnyNameResolver.createSuccess( + successTypeDescriptor, + CodeBlock.of(DAFNY_OUTPUT))); } // catch Errors in this Namespace method .nextControlFlow("catch ($T ex)", ClassName.get(RuntimeException.class)) - .addStatement("return $T.create_Failure($L, Error._typeDescriptor(), $T.Error(ex))", - DAFNY_RESULT_CLASS_NAME, successTypeDescriptor, shimLibrary.toDafnyClassName) + .addStatement("return $L", + subject.dafnyNameResolver.createFailure( + successTypeDescriptor, + CodeBlock.of("$T.Error(ex)", shimLibrary.toDafnyClassName))) .endControlFlow(); return method.build(); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java index e1bdfa7908..a2b3bbfc9d 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java @@ -18,8 +18,8 @@ public class AwsSdkDafnyV1 extends Dafny { - public AwsSdkDafnyV1(ServiceShape serviceShape, Model model) { - super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V1); + public AwsSdkDafnyV1(ServiceShape serviceShape, Model model, String dafnyVersion) { + super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V1, dafnyVersion); } @Override diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java index 496ddbc16d..f735a51853 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java @@ -25,8 +25,8 @@ public class AwsSdkDafnyV2 extends Dafny { - public AwsSdkDafnyV2(ServiceShape serviceShape, Model model) { - super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V2); + public AwsSdkDafnyV2(ServiceShape serviceShape, Model model, String dafnyVersion) { + super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V2, dafnyVersion); } @Override 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 de79b77c8b..9739abe8ef 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 @@ -11,6 +11,7 @@ public class Constants { public static final ShapeId SMITHY_API_UNIT = ShapeId.fromParts("smithy.api", "Unit"); + public static final ClassName DAFNY_OPTION_CLASS_NAME = ClassName.get("Wrappers_Compile", "Option"); public static final ClassName DAFNY_RESULT_CLASS_NAME = ClassName.get("Wrappers_Compile", "Result"); public static final ClassName DAFNY_TUPLE0_CLASS_NAME = ClassName.get("dafny", "Tuple0"); public static final ClassName DAFNY_TYPE_DESCRIPTOR_CLASS_NAME = ClassName.get("dafny", "TypeDescriptor"); 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 6c7bc51c78..3f337f552b 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 @@ -65,17 +65,21 @@ public class Dafny extends NameResolver { ); } + private final String dafnyVersion; + public Dafny( final String packageName, final Model model, final ServiceShape serviceShape, - CodegenSubject.AwsSdkVersion awsSdkVersion) { + CodegenSubject.AwsSdkVersion awsSdkVersion, + final String dafnyVersion) { super( packageName, serviceShape, model, modelPackageNameForServiceShape(serviceShape), awsSdkVersion); + this.dafnyVersion = dafnyVersion; } /** @@ -92,6 +96,69 @@ public static String datatypeConstructorCreate(String name, boolean isRecordType return "create_" + DafnyNameResolverHelpers.dafnyCompilesExtra_(name); } + private boolean datatypeConstructorsNeedTypeDescriptors() { + // TODO: proper version comparison + return dafnyVersion.compareTo("4.2") >= 0; + } + + public CodeBlock createNone(CodeBlock typeDescriptor) { + if (datatypeConstructorsNeedTypeDescriptors()) { + return CodeBlock.of( + "$T.create_None($L)", + ClassName.get("Wrappers_Compile", "Option"), + typeDescriptor); + } else { + return CodeBlock.of( + "$T.create_None()", + ClassName.get("Wrappers_Compile", "Option")); + } + } + + public CodeBlock createSome(CodeBlock typeDescriptor, CodeBlock value) { + if (datatypeConstructorsNeedTypeDescriptors()) { + return CodeBlock.of( + "$T.create_Some($L, $L)", + Constants.DAFNY_OPTION_CLASS_NAME, + typeDescriptor, + value); + } else { + return CodeBlock.of( + "$T.create_Some($L)", + Constants.DAFNY_OPTION_CLASS_NAME, + value); + } + } + + public CodeBlock createSuccess(CodeBlock valueTypeDescriptor, CodeBlock value) { + if (datatypeConstructorsNeedTypeDescriptors()) { + return CodeBlock.of( + "$T.create_Success($L, Error._typeDescriptor(), $L)", + Constants.DAFNY_RESULT_CLASS_NAME, + valueTypeDescriptor, + value); + } else { + return CodeBlock.of( + "$T.create_Success($L)", + Constants.DAFNY_RESULT_CLASS_NAME, + value); + } + } + + public CodeBlock createFailure(CodeBlock typeDescriptor, CodeBlock error) { + if (datatypeConstructorsNeedTypeDescriptors()) { + return CodeBlock.of( + "$T.create_Failure($L, Error._typeDescriptor(), $L)", + Constants.DAFNY_RESULT_CLASS_NAME, + typeDescriptor, + error); + } else { + return CodeBlock.of( + "$T.create_Failure($L)", + Constants.DAFNY_RESULT_CLASS_NAME, + error); + } + } + public static String datatypeConstructorIs(String name) { String dafnyEnumName = DafnyNameResolverHelpers.dafnyCompilesExtra_(name); return "is_" + dafnyEnumName; diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java index 92b85a11bc..9c1a717c9a 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginSettings.java @@ -52,16 +52,26 @@ class DafnyClientCodegenPluginSettings { */ public final Path includeDafnyFile; + /** + * The Dafny version to generate code compatible with. + * This is used to ensure both Dafny source compatibility + * and compatibility with the Dafny compiler and runtime internals, + * which shim code generation currently depends on. + */ + public final String dafnyVersion; + private DafnyClientCodegenPluginSettings( final DafnyClientCodegenEdition edition, final ShapeId serviceId, final Set targetLanguages, - final Path includeDafnyFile + final Path includeDafnyFile, + final String dafnyVersion ) { this.edition = edition; this.serviceId = serviceId; this.targetLanguages = targetLanguages; this.includeDafnyFile = includeDafnyFile; + this.dafnyVersion = dafnyVersion; } static Optional fromObject(final ObjectNode node, final FileManifest manifest) { @@ -107,8 +117,11 @@ static Optional fromObject(final ObjectNode no includeDafnyFileNormalized); } + final String dafnyVersion = node.expectStringMember("dafnyVersion").getValue(); + return Optional.of( - new DafnyClientCodegenPluginSettings(edition, serviceId, targetLanguages, includeDafnyFileNormalized)); + new DafnyClientCodegenPluginSettings(edition, serviceId, targetLanguages, includeDafnyFileNormalized, + dafnyVersion)); } /** diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/ForEachDafnyTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/ForEachDafnyTest.java new file mode 100644 index 0000000000..493c2a72e0 --- /dev/null +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/ForEachDafnyTest.java @@ -0,0 +1,19 @@ +package software.amazon.polymorph.smithyjava; + +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.util.Arrays; +import java.util.Collection; + +@RunWith(Parameterized.class) +public abstract class ForEachDafnyTest { + + @Parameterized.Parameters(name = "dafnyVersion = {0}") + public static Collection dafnies() { + return Arrays.asList(new Object[][] { + { "4.1" }, + { "4.3" }, + }); + } +} diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/TestSetupUtils.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/TestSetupUtils.java index a9f1a06325..793d5ff529 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/TestSetupUtils.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/TestSetupUtils.java @@ -32,13 +32,13 @@ public static JavaAwsSdkV1 setupAwsSdkV1(Model localModel, String awsName) { localModel, namespaceForService(awsName)); return JavaAwsSdkV1.createJavaAwsSdkV1(serviceShape, localModel); } - public static JavaAwsSdkV2 setupAwsSdkV2(Model localModel, String awsName) { + public static JavaAwsSdkV2 setupAwsSdkV2(Model localModel, String awsName, String dafnyVersion) { ServiceShape serviceShape = serviceFromNamespace( localModel, namespaceForService(awsName)); - return JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, localModel); + return JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, localModel, dafnyVersion); } - public static JavaLibrary setupLibrary(Model localModel, String namespace) { + public static JavaLibrary setupLibrary(Model localModel, String namespace, String dafnyVersion) { ServiceShape serviceShape = serviceFromNamespace(localModel, namespace); - return new JavaLibrary(localModel, serviceShape, CodegenSubject.AwsSdkVersion.V1); + return new JavaLibrary(localModel, serviceShape, CodegenSubject.AwsSdkVersion.V1, dafnyVersion); } } diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java index 2b674170ee..153e2d6d42 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java @@ -14,6 +14,9 @@ import javax.lang.model.element.Modifier; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; import software.amazon.polymorph.util.Tokenizer; @@ -27,15 +30,14 @@ import static software.amazon.polymorph.smithyjava.generator.awssdk.v2.Constants.DoVoidOperation; import static software.amazon.polymorph.smithyjava.generator.awssdk.v2.Constants.MockKmsShim; -public class ShimTest { +public class ShimTest extends ForEachDafnyTest { protected ShimV2 underTest; protected Model model; protected JavaAwsSdkV2 subject; - @Before - public void setup() { + public ShimTest(String dafnyVersion) { model = TestSetupUtils.setupLocalModel(ModelConstants.MOCK_KMS); - subject = TestSetupUtils.setupAwsSdkV2(model, "kms"); + subject = TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion); underTest = new ShimV2(subject); } diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java index 63f97ab549..b59d8ea8a1 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java @@ -10,6 +10,7 @@ import java.nio.file.Path; import java.util.Map; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; import software.amazon.polymorph.utils.TokenTree; @@ -21,14 +22,15 @@ import static org.junit.Assert.assertThrows; import static software.amazon.polymorph.util.Tokenizer.tokenizeAndAssertEqual; -public class ToDafnyAwsV2Test { - protected ToDafnyAwsV2 underTest; - protected Model model; +public class ToDafnyAwsV2Test extends ForEachDafnyTest { + protected final ToDafnyAwsV2 underTest; + protected final Model model; + protected final String dafnyVersion; - @Before - public void setup() { + public ToDafnyAwsV2Test(String dafnyVersion) { + this.dafnyVersion = dafnyVersion; model = TestSetupUtils.setupTwoLocalModel(ModelConstants.KMS_KITCHEN, ModelConstants.OTHER_NAMESPACE); - underTest = new ToDafnyAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms")); + underTest = new ToDafnyAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion)); } @Test @@ -80,7 +82,7 @@ public void generateConvertOpaqueError() { @Test public void generate() { Model localModel = TestSetupUtils.setupLocalModel(ModelConstants.KMS_A_STRING_OPERATION); - ToDafnyAwsV2 localUnderTest = new ToDafnyAwsV2(TestSetupUtils.setupAwsSdkV2(localModel, "kms")); + ToDafnyAwsV2 localUnderTest = new ToDafnyAwsV2(TestSetupUtils.setupAwsSdkV2(localModel, "kms", dafnyVersion)); final Map actual = localUnderTest.generate(); final Path expectedPath = Path.of("software/amazon/cryptography/services/kms/internaldafny/ToDafny.java"); Path[] temp = new Path[1]; diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeTest.java index 6d7c3ac1c8..9b1924ff3c 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeTest.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeTest.java @@ -10,9 +10,14 @@ import org.junit.Test; import java.nio.file.Path; +import java.util.Arrays; +import java.util.Collection; import java.util.Map; import java.util.Set; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.MethodReference; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; @@ -35,7 +40,7 @@ import static software.amazon.polymorph.util.Tokenizer.tokenizeAndAssertEqual; @SuppressWarnings("OptionalGetWithoutIsPresent") -public class ToNativeTest { +public class ToNativeTest extends ForEachDafnyTest { // Why two underTests? // As we refactor ToNativeAwsV2 and abstract ToNative, // we are going to bump into permission issues in unit tests @@ -49,6 +54,7 @@ public class ToNativeTest { protected ToNativeAwsV2 underTest; protected ToNativeTestImpl underTestAbstract; protected Model model; + protected final String dafnyVersion; class ToNativeTestImpl extends ToNativeAwsV2 { @@ -93,11 +99,11 @@ protected CodeBlock setWithConversionCall(MemberShape member, CodeBlock getMembe } } - @Before - public void setup() { + public ToNativeTest(String dafnyVersion) { + this.dafnyVersion = dafnyVersion; model = TestSetupUtils.setupTwoLocalModel(ModelConstants.KMS_KITCHEN, ModelConstants.OTHER_NAMESPACE); - underTest = new ToNativeAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms")); - underTestAbstract = new ToNativeTestImpl(TestSetupUtils.setupAwsSdkV2(model, "kms")); + underTest = new ToNativeAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion)); + underTestAbstract = new ToNativeTestImpl(TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion)); } @Test @@ -231,7 +237,7 @@ public void generateConvert() { @Test public void generate() { Model model = TestSetupUtils.setupLocalModel(ModelConstants.KMS_A_STRING_OPERATION); - ToNativeAwsV2 underTest = new ToNativeAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms")); + ToNativeAwsV2 underTest = new ToNativeAwsV2(TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion)); final Map actual = underTest.generate(); final Path expectedPath = Path.of("software/amazon/cryptography/services/kms/internaldafny/ToNative.java"); Path[] temp = new Path[1]; diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegenTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegenTest.java index ac2d029baa..900ccae810 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegenTest.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegenTest.java @@ -7,6 +7,7 @@ import org.junit.Before; import org.junit.Test; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; import software.amazon.smithy.model.Model; @@ -15,14 +16,13 @@ import static software.amazon.polymorph.util.Tokenizer.tokenizeAndAssertEqual; -public class ModelCodegenTest { +public class ModelCodegenTest extends ForEachDafnyTest { protected ModelCodegen underTest; protected Model model; - @Before - public void setup() { + public ModelCodegenTest(String dafnyVersion) { model = TestSetupUtils.setupLocalModel(ModelConstants.CRYPTOGRAPHY_A_STRING_OPERATION); - underTest = new ModelCodegen(TestSetupUtils.setupLibrary(model, "aws.cryptography.test")); + underTest = new ModelCodegen(TestSetupUtils.setupLibrary(model, "aws.cryptography.test", dafnyVersion)); } @Test diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/nameresolver/DafnyTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/nameresolver/DafnyTest.java index da1991ebe4..eabbbf3215 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/nameresolver/DafnyTest.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/nameresolver/DafnyTest.java @@ -8,6 +8,9 @@ import org.junit.Before; import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import software.amazon.polymorph.smithyjava.ForEachDafnyTest; import software.amazon.polymorph.smithyjava.ModelConstants; import software.amazon.polymorph.smithyjava.generator.CodegenSubject; import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils; @@ -19,15 +22,17 @@ import software.amazon.smithy.model.shapes.ShapeId; import software.amazon.smithy.model.shapes.StructureShape; +import java.util.Arrays; +import java.util.Collection; + import static org.junit.Assert.assertEquals; import static software.amazon.polymorph.util.Tokenizer.tokenizeAndAssertEqual; -public class DafnyTest { +public class DafnyTest extends ForEachDafnyTest { Dafny underTest; protected Model model; - @Before - public void setup() { + public DafnyTest(String dafnyVersion) { String rawModel = """ namespace smithy.example service Example {} @@ -40,7 +45,7 @@ public void setup() { (builder, modelAssembler) -> modelAssembler .addUnparsedModel("test.smithy", rawModel)); ServiceShape serviceShape = ModelUtils.serviceFromNamespace(model, "smithy.example"); - underTest = new Dafny("Dafny.Smithy.Example", model, serviceShape, CodegenSubject.AwsSdkVersion.V2); + underTest = new Dafny("Dafny.Smithy.Example", model, serviceShape, CodegenSubject.AwsSdkVersion.V2, dafnyVersion); } @Test