From 78ee43abe82caff554c1f72e758d9918db520e88 Mon Sep 17 00:00:00 2001 From: seebees Date: Mon, 10 Mar 2025 15:11:46 -0700 Subject: [PATCH 1/2] fix(java): empty nullable lists convert to optional empty lists `null` and `.isPresent()` of empty are not the same. The AWS SKD has a specific way it handles these cases, and we are not adjusting that. This converts java `null` => `None`, and `[]` => `Some([])`. This means that for smithy-dafny Java <=> Dafny conversions are lossless. --- .../Aggregate/runtimes/java/build.gradle.kts | 73 +++++++++++++++++++ .../aggregate/internaldafny/__default.java | 5 ++ .../internaldafny/types/__default.java | 5 ++ .../internaldafny/wrapped/__default.java | 33 +++++++++ .../test/SimpleAggregateImplTest.dfy | 64 +++++++++++++++- .../test/WrappedSimpleAggregateImplTest.dfy | 3 +- .../smithyjava/generator/ToDafny.java | 5 +- 7 files changed, 181 insertions(+), 7 deletions(-) create mode 100644 TestModels/Aggregate/runtimes/java/build.gradle.kts create mode 100644 TestModels/Aggregate/runtimes/java/src/main/java/simple/aggregate/internaldafny/__default.java create mode 100644 TestModels/Aggregate/runtimes/java/src/main/java/simple/aggregate/internaldafny/types/__default.java create mode 100644 TestModels/Aggregate/runtimes/java/src/test/java/simple/aggregate/internaldafny/wrapped/__default.java diff --git a/TestModels/Aggregate/runtimes/java/build.gradle.kts b/TestModels/Aggregate/runtimes/java/build.gradle.kts new file mode 100644 index 0000000000..5148ab42b5 --- /dev/null +++ b/TestModels/Aggregate/runtimes/java/build.gradle.kts @@ -0,0 +1,73 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +import java.io.File +import java.io.FileInputStream +import java.util.Properties + +tasks.wrapper { + gradleVersion = "7.6" +} + +plugins { + `java-library` + `maven-publish` +} + +var props = Properties().apply { + load(FileInputStream(File(rootProject.rootDir, "../../project.properties"))) +} +var dafnyVersion = props.getProperty("dafnyVersion") + +group = "simple" +version = "1.0-SNAPSHOT" +description = "Constraints" + +java { + toolchain.languageVersion.set(JavaLanguageVersion.of(8)) + sourceSets["main"].java { + srcDir("src/main/java") + srcDir("src/main/dafny-generated") + srcDir("src/main/smithy-generated") + } + sourceSets["test"].java { + srcDir("src/test/java") + srcDir("src/test/dafny-generated") + srcDir("src/test/smithy-generated") + } +} + +repositories { + mavenCentral() + mavenLocal() +} + +dependencies { + implementation("org.dafny:DafnyRuntime:${dafnyVersion}") + implementation("software.amazon.smithy.dafny:conversion:0.1.1") + implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT") + testImplementation("org.testng:testng:7.5") +} + +publishing { + publications.create("maven") { + groupId = "simple" + artifactId = "Constraints" + from(components["java"]) + } + repositories { mavenLocal() } +} + +tasks.withType() { + options.encoding = "UTF-8" +} + +tasks { + register("runTests", JavaExec::class.java) { + mainClass.set("TestsFromDafny") + classpath = sourceSets["test"].runtimeClasspath + } +} + +tasks.named("test") { + useTestNG() +} \ No newline at end of file diff --git a/TestModels/Aggregate/runtimes/java/src/main/java/simple/aggregate/internaldafny/__default.java b/TestModels/Aggregate/runtimes/java/src/main/java/simple/aggregate/internaldafny/__default.java new file mode 100644 index 0000000000..396bfd8d55 --- /dev/null +++ b/TestModels/Aggregate/runtimes/java/src/main/java/simple/aggregate/internaldafny/__default.java @@ -0,0 +1,5 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package simple.aggregate.internaldafny; + +public class __default extends _ExternBase___default {} diff --git a/TestModels/Aggregate/runtimes/java/src/main/java/simple/aggregate/internaldafny/types/__default.java b/TestModels/Aggregate/runtimes/java/src/main/java/simple/aggregate/internaldafny/types/__default.java new file mode 100644 index 0000000000..6e3d20eb35 --- /dev/null +++ b/TestModels/Aggregate/runtimes/java/src/main/java/simple/aggregate/internaldafny/types/__default.java @@ -0,0 +1,5 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package simple.aggregate.internaldafny.types; + +public class __default extends _ExternBase___default {} diff --git a/TestModels/Aggregate/runtimes/java/src/test/java/simple/aggregate/internaldafny/wrapped/__default.java b/TestModels/Aggregate/runtimes/java/src/test/java/simple/aggregate/internaldafny/wrapped/__default.java new file mode 100644 index 0000000000..ae10b2ab9d --- /dev/null +++ b/TestModels/Aggregate/runtimes/java/src/test/java/simple/aggregate/internaldafny/wrapped/__default.java @@ -0,0 +1,33 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package simple.aggregate.internaldafny.wrapped; + +import Wrappers_Compile.Result; +import simple.aggregate.SimpleAggregate; +import simple.aggregate.ToNative; +import simple.aggregate.internaldafny.types.Error; +import simple.aggregate.internaldafny.types.ISimpleAggregateClient; +import simple.aggregate.internaldafny.types.SimpleAggregateConfig; +import simple.aggregate.wrapped.TestSimpleAggregate; + +public class __default extends _ExternBase___default { + + public static Result< + ISimpleAggregateClient, + Error + > WrappedSimpleAggregate(SimpleAggregateConfig config) { + simple.aggregate.model.SimpleAggregateConfig wrappedConfig = + ToNative.SimpleAggregateConfig(config); + simple.aggregate.SimpleAggregate impl = SimpleAggregate + .builder() + .SimpleAggregateConfig(wrappedConfig) + .build(); + TestSimpleAggregate wrappedClient = TestSimpleAggregate + .builder() + .impl(impl) + .build(); + return simple.aggregate.internaldafny.__default.CreateSuccessOfClient( + wrappedClient + ); + } +} diff --git a/TestModels/Aggregate/test/SimpleAggregateImplTest.dfy b/TestModels/Aggregate/test/SimpleAggregateImplTest.dfy index 296ec2d447..d6d8899047 100644 --- a/TestModels/Aggregate/test/SimpleAggregateImplTest.dfy +++ b/TestModels/Aggregate/test/SimpleAggregateImplTest.dfy @@ -7,9 +7,19 @@ module SimpleAggregateImplTest { import opened SimpleAggregateTypes import opened Wrappers method{:test} GetAggregate(){ - var client :- expect SimpleAggregate.SimpleAggregate(); - TestGetAggregate(client); - TestGetAggregateKnownValue(client); + var client :- expect SimpleAggregate.SimpleAggregate(); + TestAggregate(client); + } + + method TestAggregate(client: ISimpleAggregateClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + TestGetAggregate(client); + TestGetAggregateKnownValue(client); + TestEmptyAggregate(client); + TestNoneAggregate(client); } method TestGetAggregate(client: ISimpleAggregateClient) @@ -37,7 +47,7 @@ module SimpleAggregateImplTest { } method TestGetAggregateKnownValue(client: ISimpleAggregateClient) - requires client.ValidState() + requires client.ValidState() modifies client.Modifies ensures client.ValidState() { @@ -59,4 +69,50 @@ module SimpleAggregateImplTest { expect ret.nestedStructure.UnwrapOr(NestedStructure(stringStructure := Some(StringStructure(value := Some(""))))) == nestedStructure; print ret; } + + method TestEmptyAggregate(client: ISimpleAggregateClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var stringList := []; + var simpleStringMap := map[]; + var structureList :=[]; + var simpleIntegerMap := map[]; + var nestedStructure := NestedStructure(stringStructure := Some(StringStructure(value := Some("Nested")))); + var ret :- expect client.GetAggregate(GetAggregateInput(simpleIntegerMap := Some(simpleIntegerMap), + simpleStringMap := Some(simpleStringMap), + simpleStringList := Some(stringList), + structureList := Some(structureList), + nestedStructure := Some(nestedStructure)) + ); + expect ret.simpleStringList == Some(stringList); + expect ret.structureList == Some(structureList); + expect ret.simpleStringMap == Some(simpleStringMap); + expect ret.simpleIntegerMap == Some(simpleIntegerMap); + expect ret.nestedStructure.UnwrapOr(NestedStructure(stringStructure := Some(StringStructure(value := Some(""))))) == nestedStructure; + print ret; + } + + method TestNoneAggregate(client: ISimpleAggregateClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + + var ret :- expect client.GetAggregate( + GetAggregateInput( + simpleIntegerMap := None, + simpleStringMap := None, + simpleStringList := None, + structureList := None, + nestedStructure := None) + ); + expect ret.simpleStringList == None; + expect ret.structureList == None; + expect ret.simpleStringMap == None; + expect ret.simpleIntegerMap == None; + expect ret.nestedStructure == None; + print ret; + } } \ No newline at end of file diff --git a/TestModels/Aggregate/test/WrappedSimpleAggregateImplTest.dfy b/TestModels/Aggregate/test/WrappedSimpleAggregateImplTest.dfy index 803a29f6a7..b17abd7bd4 100644 --- a/TestModels/Aggregate/test/WrappedSimpleAggregateImplTest.dfy +++ b/TestModels/Aggregate/test/WrappedSimpleAggregateImplTest.dfy @@ -9,7 +9,6 @@ module WrappedSimpleTypesStringTest { import opened Wrappers method{:test} GetAggregate() { var client :- expect WrappedSimpleAggregateService.WrappedSimpleAggregate(); - SimpleAggregateImplTest.TestGetAggregate(client); - SimpleAggregateImplTest.TestGetAggregateKnownValue(client); + SimpleAggregateImplTest.TestAggregate(client); } } \ No newline at end of file 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..5a44a3e8eb 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 @@ -263,7 +263,10 @@ protected CodeBlock memberAssign( ); CodeBlock isSetCheck = isNullCheck; Shape targetShape = subject.model.expectShape(memberShape.getTarget()); - if (Constants.LIST_MAP_SET_SHAPE_TYPES.contains(targetShape.getType())) { + if ( + Constants.LIST_MAP_SET_SHAPE_TYPES.contains(targetShape.getType()) + && AwsSdkNameResolverHelpers.isInAwsSdkNamespace(memberShape.getTarget()) + ) { isSetCheck = CodeBlock.of("($L && $L.size() > 0)", isNullCheck, inputVar); } CodeBlock typeDescriptor = subject.dafnyNameResolver.typeDescriptor( From 8eb825a3219d26d9cd13921c20184d0945fbb1cf Mon Sep 17 00:00:00 2001 From: seebees Date: Mon, 10 Mar 2025 15:25:01 -0700 Subject: [PATCH 2/2] updates --- .../software/amazon/polymorph/smithyjava/JavaTestModels.java | 1 - .../software/amazon/polymorph/smithyjava/generator/ToDafny.java | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyjava/JavaTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyjava/JavaTestModels.java index 8cf0ec9952..bc6c132297 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyjava/JavaTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyjava/JavaTestModels.java @@ -20,7 +20,6 @@ class JavaTestModels extends TestModelTest { private static final Set DISABLED_TESTS = new HashSet<>(); static { - DISABLED_TESTS.add("Aggregate"); DISABLED_TESTS.add("AggregateReferences"); DISABLED_TESTS.add("CallingAWSSDKFromLocalService"); DISABLED_TESTS.add("Constructor"); 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 5a44a3e8eb..2c9a51eda9 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 @@ -265,7 +265,7 @@ protected CodeBlock memberAssign( Shape targetShape = subject.model.expectShape(memberShape.getTarget()); if ( Constants.LIST_MAP_SET_SHAPE_TYPES.contains(targetShape.getType()) - && AwsSdkNameResolverHelpers.isInAwsSdkNamespace(memberShape.getTarget()) + && AwsSdkNameResolverHelpers.isInAwsSdkNamespace(memberShape.getTarget()) ) { isSetCheck = CodeBlock.of("($L && $L.size() > 0)", isNullCheck, inputVar); }