diff --git a/.github/workflows/format.yml b/.github/workflows/format.yml index b8374276c1..964db888b3 100644 --- a/.github/workflows/format.yml +++ b/.github/workflows/format.yml @@ -6,7 +6,7 @@ on: jobs: check-java: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Support longpaths run: | diff --git a/.github/workflows/nightly_dafny.yml b/.github/workflows/nightly_dafny.yml index 5d14390a4c..fdc1d41ff5 100644 --- a/.github/workflows/nightly_dafny.yml +++ b/.github/workflows/nightly_dafny.yml @@ -42,7 +42,7 @@ jobs: dafny: "nightly-latest" cut-issue-on-failure: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 needs: [ dafny-nightly-verification, diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 289a31d9b0..cb26671d21 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -6,7 +6,7 @@ on: jobs: pr-populate-dafny-versions: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Populate Dafny versions list id: populate-dafny-versions-list @@ -85,7 +85,7 @@ jobs: - pr-ci-rust - pr-ci-python - pr-ci-go - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Verify all required jobs passed uses: re-actors/alls-green@release/v1 diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 247dfef2b8..f317e58f76 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -8,7 +8,7 @@ on: jobs: pr-populate-dafny-versions: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Populate Dafny versions list id: populate-dafny-versions-list diff --git a/.github/workflows/smithy-dafny-conversion.yml b/.github/workflows/smithy-dafny-conversion.yml index 3d89cc932b..84c2a54365 100644 --- a/.github/workflows/smithy-dafny-conversion.yml +++ b/.github/workflows/smithy-dafny-conversion.yml @@ -8,7 +8,7 @@ on: jobs: gradle-build-smithy-dafny-conversion: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - uses: actions/checkout@v3 with: diff --git a/.github/workflows/smithy-polymorph.yml b/.github/workflows/smithy-polymorph.yml index 002bd09a1b..d15b18dfa4 100644 --- a/.github/workflows/smithy-polymorph.yml +++ b/.github/workflows/smithy-polymorph.yml @@ -11,7 +11,7 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-latest, windows-latest, macos-13] + os: [ubuntu-22.04, windows-latest, macos-13] runs-on: ${{matrix.os}} steps: - uses: actions/checkout@v3 @@ -47,5 +47,5 @@ jobs: run: make polymorph_dafny - name: not-grep - if: matrix.os == 'ubuntu-latest' + if: matrix.os == 'ubuntu-22.04' uses: mattsb42-meta/not-grep@1.0.0 diff --git a/.github/workflows/test_models_dafny_verification.yml b/.github/workflows/test_models_dafny_verification.yml index d53eefb1f4..0d3910ee5e 100644 --- a/.github/workflows/test_models_dafny_verification.yml +++ b/.github/workflows/test_models_dafny_verification.yml @@ -15,7 +15,7 @@ on: jobs: populate-matrix-dimensions: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Populate shard list id: populate-shard-list @@ -30,7 +30,7 @@ jobs: dafny-version: - ${{ inputs.dafny }} shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }} - os: [ubuntu-latest] + os: [ubuntu-22.04] runs-on: ${{ matrix.os }} defaults: run: diff --git a/.github/workflows/test_models_go_tests.yml b/.github/workflows/test_models_go_tests.yml index e77e994bcd..51c6984d2c 100644 --- a/.github/workflows/test_models_go_tests.yml +++ b/.github/workflows/test_models_go_tests.yml @@ -14,7 +14,7 @@ on: jobs: populate-matrix-dimensions: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Populate shard list id: populate-shard-list @@ -27,7 +27,7 @@ jobs: fail-fast: false # at least for development; see all errors matrix: shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }} - runs-on: "ubuntu-latest" + runs-on: "ubuntu-22.04" permissions: id-token: write contents: read diff --git a/.github/workflows/test_models_java_tests.yml b/.github/workflows/test_models_java_tests.yml index a00b4ac432..29f027c83d 100644 --- a/.github/workflows/test_models_java_tests.yml +++ b/.github/workflows/test_models_java_tests.yml @@ -15,7 +15,7 @@ on: jobs: populate-matrix-dimensions: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Populate shard list id: populate-shard-list @@ -28,7 +28,7 @@ jobs: fail-fast: false matrix: shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }} - runs-on: "ubuntu-latest" + runs-on: "ubuntu-22.04" permissions: id-token: write contents: read diff --git a/.github/workflows/test_models_net_tests.yml b/.github/workflows/test_models_net_tests.yml index 34858b5f93..daa47e263f 100644 --- a/.github/workflows/test_models_net_tests.yml +++ b/.github/workflows/test_models_net_tests.yml @@ -15,7 +15,7 @@ on: jobs: populate-matrix-dimensions: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Populate shard list id: populate-shard-list @@ -31,7 +31,7 @@ jobs: - ${{ inputs.dafny }} shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }} dotnet-version: ["6.0.x"] - os: [ubuntu-latest] + os: [ubuntu-22.04] runs-on: ${{ matrix.os }} permissions: id-token: write diff --git a/.github/workflows/test_models_python_tests.yml b/.github/workflows/test_models_python_tests.yml index 65456fda73..7291d9a195 100644 --- a/.github/workflows/test_models_python_tests.yml +++ b/.github/workflows/test_models_python_tests.yml @@ -15,7 +15,7 @@ on: jobs: populate-matrix-dimensions: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Populate shard list id: populate-shard-list @@ -29,7 +29,7 @@ jobs: fail-fast: false # at least for development; see all errors matrix: shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }} - runs-on: "ubuntu-latest" + runs-on: "ubuntu-22.04" permissions: id-token: write contents: read diff --git a/.github/workflows/test_models_rust_tests.yml b/.github/workflows/test_models_rust_tests.yml index 7ab616a589..40374706a4 100644 --- a/.github/workflows/test_models_rust_tests.yml +++ b/.github/workflows/test_models_rust_tests.yml @@ -15,7 +15,7 @@ on: jobs: populate-matrix-dimensions: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 steps: - name: Populate shard list id: populate-shard-list @@ -28,7 +28,7 @@ jobs: fail-fast: false matrix: shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }} - runs-on: "ubuntu-latest" + runs-on: "ubuntu-22.04" permissions: id-token: write contents: read diff --git a/TestModels/.gitignore b/TestModels/.gitignore index 370617fd88..8815c7af98 100644 --- a/TestModels/.gitignore +++ b/TestModels/.gitignore @@ -34,6 +34,23 @@ # Polymorph Generated Python **/runtimes/python/src/**/smithygenerated/ +# Polymorph Generated Rust +**/src/client.rs +**/src/client +**/src/conversions.rs +**/src/conversions +**/src/deps.rs +**/src/deps +**/src/error.rs +**/src/error +**/src/operation.rs +**/src/operation +**/src/standard_library_conversions.rs +**/src/standard_library_externs.rs +**/src/types.rs +**/src/types +**/target + # .NET Artifacts **/bin **/obj diff --git a/TestModels/OrphanedShapes/Makefile b/TestModels/OrphanedShapes/Makefile new file mode 100644 index 0000000000..1868f402e0 --- /dev/null +++ b/TestModels/OrphanedShapes/Makefile @@ -0,0 +1,55 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +CORES=2 + +ENABLE_EXTERN_PROCESSING=1 +TRANSPILE_TESTS_IN_RUST=1 + +include ../SharedMakefile.mk + +NAMESPACE=simple.orphaned + +PROJECT_SERVICES := \ + SimpleOrphaned + +MAIN_SERVICE_FOR_RUST := SimpleOrphaned + +SERVICE_NAMESPACE_SimpleOrphaned=simple.orphaned + +SERVICE_DEPS_SimpleOrphaned := + +SMITHY_DEPS=dafny-dependencies/Model/traits.smithy + +# This project has no dependencies +# DEPENDENT-MODELS:= + +POLYMORPH_OPTIONS=--generate project-files,client-constructors\ + +# Go + +GO_MODULE_NAME="github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes" + +TRANSLATION_RECORD_GO := \ + dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr + +# Python + +PYTHON_MODULE_NAME=simple_orphaned + +TRANSLATION_RECORD_PYTHON := \ + --translation-record ../dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/generated/dafny_src-py.dtr + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleOrphanedTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.orphaned.internaldafny.types\" } SimpleOrphanedTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleOrphanedTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.orphaned.internaldafny\" } SimpleOrphaned refines AbstractSimpleOrphanedService {" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleOrphaned refines AbstractSimpleOrphanedService {" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleOrphanedImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:options \"--function-syntax:4\"} {:extern \"simple.orphaned.internaldafny.wrapped\"} WrappedSimpleOrphanedService refines WrappedAbstractSimpleOrphanedService {" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module {:options \"--function-syntax:4\"} WrappedSimpleOrphanedService refines WrappedAbstractSimpleOrphanedService {" diff --git a/TestModels/OrphanedShapes/Model/OrphanedShapes.smithy b/TestModels/OrphanedShapes/Model/OrphanedShapes.smithy new file mode 100644 index 0000000000..e04cd63751 --- /dev/null +++ b/TestModels/OrphanedShapes/Model/OrphanedShapes.smithy @@ -0,0 +1,130 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +$version: "2" +namespace simple.orphaned + +@aws.polymorph#localService( + sdkId: "SimpleOrphaned", + config: SimpleOrphanedConfig, +) +service SimpleOrphaned { + version: "2021-11-01", + resources: [], + operations: [], +} + +structure SimpleOrphanedConfig { + structureMember: OrphanedConfigShape +} + +structure OrphanedConfigShape { + stringMember: String +} + +blob OrphanedBlob + +boolean OrphanedBoolean + +string OrphanedString + +// TODO: Once SimpleTypes for commented-out shapes are completed, +// uncomment these and add as members to OrphanedStructure +// byte OrphanedByte + +// short OrphanedShort + +integer OrphanedInteger + +long OrphanedLong + +// float OrphanedFloat + +// double OrphanedDouble + +// bigInteger OrphanedBigInteger + +// bigDecimal OrphanedBigDecimal + +// timestamp OrphanedTimestamp + +// document OrphanedDocument + +// This is a smithy V1 Enum +@enum([ + { + name: "FIRST", + value: "0x0014", + }, + { + name: "SECOND", + value: "0x0046", + }, + { + name: "THIRD", + value: "0x0078", + }, +]) +string OrphanedV1Enum + +list OrphanedList { + member: String +} + +map OrphanedMap { + key: String + value: String +} + +structure OrphanedStructure { + blobValue: OrphanedBlob, + booleanValue: OrphanedBoolean, + stringValue: OrphanedString, + // byteValue: OrphanedByte, + // shortValue: OrphanedShort, + integerValue: OrphanedInteger, + longValue: OrphanedLong, + // floatValue: OrphanedFloat, + // doubleValue: OrphanedDouble, + // bigIntegerValue: OrphanedBigInteger, + // bigDecimalValue: OrphanedBigDecimal, + // timestampValue: OrphanedTimestamp, + unionValue: OrphanedUnion, + enumValue: OrphanedV1Enum, + mapValue: OrphanedMap, + listValue: OrphanedList +} + +union OrphanedUnion { + integerValue: Integer + stringValue: String +} + +@error("client") +structure OrphanedError { + @required + message: String, +} + +@aws.polymorph#reference(resource: OrphanedResource) +structure OrphanedResourceReference {} + +@aws.polymorph#extendable +resource OrphanedResource { + operations: [ + OrphanedResourceOperation + ] +} + +operation OrphanedResourceOperation { + input: OrphanedResourceOperationInput + output: OrphanedResourceOperationOutput +} + +structure OrphanedResourceOperationInput { + someString: String +} + +structure OrphanedResourceOperationOutput { + someString: String +} diff --git a/TestModels/OrphanedShapes/README.md b/TestModels/OrphanedShapes/README.md new file mode 100644 index 0000000000..d80119f35c --- /dev/null +++ b/TestModels/OrphanedShapes/README.md @@ -0,0 +1,57 @@ +# OrphanedShapes + +## Background + +This project tests for support of "orphaned" shapes. + +An "orphaned" is a shape that exists in a Smithy model, but is not discovered by Smithy-Core's shape discovery logic. + +Smithy-Core will only discover and generate code for shapes that are attached to a service via the service's + +1. Operations +2. Mixins +3. Errors + +and recursive traversals of the connected shapes. + +If a shape is defined in a Smithy model, +but not declared in a LocalService's operations or errors +(or recursive traversals of these), +codegens that use Smithy-Core's shape discovery will not generate code for the shape. +(Similar for mixins, but Polymorph doesn't have any usage of these at the moment.) + +Smithy-Dafny .NET and Java generate code for orphaned shapes because these codegens don't use Smithy-Core's shape discovery logic. + +By default, any language extending a "real" Smithy code generator use Smithy-Core's shape discovery logic, and do not support orphaned shapes. + +The expectation is that code is generated for orphaned shapes. +The generated code must include any class definitions and Dafny/native conversions. + +## Prerequisites + +This TestModel assumes these other TestModels are passing: + +- Extern +- Extendable +- Errors +- LocalService +- Union +- Aggregate +- Enum + +and these TestModels' prerequisite TestModels. + +## Coverage + +This TestModel tests some instances of orphaned shapes + +- LocalService Config shapes. (Config shapes are "orphaned", but are likely already handled as one-offs by any codegen that's this TestModels' prerequisites) +- Errors +- Resources (with @aws.polymorph#reference trait) and their operations +- Structures (and structures' members) + +The bar this TestModel establishes is "if a shape is defined in a Smithy model, its native/Dafny shapes and their conversions are defined in a runtime." + +This TestModel asserts this by requiring externs to pass orphaned shapes across the Dafny layer. +The extern implementations MUST call Polymorph-generated native shapes and Dafny/native conversions for these orphaned shapes. +Polymorph will only generate these shapes and conversions if the language's codegen supports orphaned shapes. diff --git a/TestModels/OrphanedShapes/runtimes/go/ImplementationFromDafny-go/go.mod b/TestModels/OrphanedShapes/runtimes/go/ImplementationFromDafny-go/go.mod new file mode 100644 index 0000000000..7b5f8db98d --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/go/ImplementationFromDafny-go/go.mod @@ -0,0 +1,10 @@ +module github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes + +go 1.23.0 + +require ( + github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1 + github.com/dafny-lang/DafnyStandardLibGo v0.0.0 +) + +replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ diff --git a/TestModels/OrphanedShapes/runtimes/go/TestsFromDafny-go/ExternDefinitions/extern.go b/TestModels/OrphanedShapes/runtimes/go/TestsFromDafny-go/ExternDefinitions/extern.go new file mode 100644 index 0000000000..6b1a3bbda4 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/go/TestsFromDafny-go/ExternDefinitions/extern.go @@ -0,0 +1,39 @@ +package ExternDefinitions + +import ( + "fmt" + + Wrappers "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" + OrphanedResource "github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes/OrphanedResource" + SimpleOrphanedTypes "github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes/SimpleOrphanedTypes" + simpleorphanedsmithygenerated "github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes/simpleorphanedsmithygenerated" + simpleorphanedsmithygeneratedtypes "github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes/simpleorphanedsmithygeneratedtypes" +) + +var _ Wrappers.Dummy__ + +// TODO: Finish implementation. +// This is missing structure converter. + +func (CompanionStruct_Default___) InitializeOrphanedStructure(input SimpleOrphanedTypes.OrphanedStructure) SimpleOrphanedTypes.OrphanedStructure { + // Missing Structure converter + return input +} + +func (CompanionStruct_Default___) CallNativeOrphanedResource(input *OrphanedResource.OrphanedResource) Wrappers.Result { + native_resource := simpleorphanedsmithygenerated.OrphanedResource_FromDafny(input) + someString := "the extern MUST provide this string to the native resource's operation" + native_output, err := native_resource.OrphanedResourceOperation(simpleorphanedsmithygeneratedtypes.OrphanedResourceOperationInput{SomeString: &someString}) + if err != nil { + return Wrappers.Companion_Result_.Create_Failure_(err) + } + dafny_output := simpleorphanedsmithygenerated.OrphanedResourceOperationOutput_ToDafny(*native_output) + return Wrappers.Companion_Result_.Create_Success_(dafny_output) +} + +func (CompanionStruct_Default___) CallNativeOrphanedError(input SimpleOrphanedTypes.Error) SimpleOrphanedTypes.Error { + native_error := simpleorphanedsmithygenerated.Error_FromDafny(input) + native_error.Message = "the extern MUST set this string using the catch-all error converter, NOT the orphaned error-specific converter" + dafny_error_again := simpleorphanedsmithygenerated.Error_ToDafny(native_error) + return dafny_error_again +} diff --git a/TestModels/OrphanedShapes/runtimes/go/TestsFromDafny-go/go.mod b/TestModels/OrphanedShapes/runtimes/go/TestsFromDafny-go/go.mod new file mode 100644 index 0000000000..349df89cc9 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/go/TestsFromDafny-go/go.mod @@ -0,0 +1,14 @@ +module github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes/test + +go 1.23.0 + +require github.com/dafny-lang/DafnyStandardLibGo v0.0.0 + +require ( + github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1 + github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes v0.0.0 +) + +replace github.com/smithy-lang/smithy-dafny/TestModels/OrphanedShapes v0.0.0 => ../ImplementationFromDafny-go + +replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ diff --git a/TestModels/OrphanedShapes/runtimes/java/build.gradle.kts b/TestModels/OrphanedShapes/runtimes/java/build.gradle.kts new file mode 100644 index 0000000000..09b66fb38a --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/java/build.gradle.kts @@ -0,0 +1,80 @@ +// 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 +import java.net.URI +import javax.annotation.Nullable + +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.orphaned" +version = "1.0-SNAPSHOT" +description = "SimpleOrphaned" + +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("mavenLocal") { + groupId = group as String? + artifactId = description + from(components["java"]) + } + publications.create("maven") { + groupId = group as String? + artifactId = description + 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() +} diff --git a/TestModels/OrphanedShapes/runtimes/java/src/main/java/Dafny/simple/orphaned/__default.java b/TestModels/OrphanedShapes/runtimes/java/src/main/java/Dafny/simple/orphaned/__default.java new file mode 100644 index 0000000000..9b96a60104 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/java/src/main/java/Dafny/simple/orphaned/__default.java @@ -0,0 +1,5 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package simple.orphaned.internaldafny; + +public class __default extends _ExternBase___default {} diff --git a/TestModels/OrphanedShapes/runtimes/java/src/main/java/Dafny/simple/orphaned/types/__default.java b/TestModels/OrphanedShapes/runtimes/java/src/main/java/Dafny/simple/orphaned/types/__default.java new file mode 100644 index 0000000000..846935f550 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/java/src/main/java/Dafny/simple/orphaned/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.orphaned.internaldafny.types; + +public class __default extends _ExternBase___default {} diff --git a/TestModels/OrphanedShapes/runtimes/java/src/test/java/ExternDefinitions_Compile/__default.java b/TestModels/OrphanedShapes/runtimes/java/src/test/java/ExternDefinitions_Compile/__default.java new file mode 100644 index 0000000000..29c7a4ad28 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/java/src/test/java/ExternDefinitions_Compile/__default.java @@ -0,0 +1,45 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package ExternDefinitions_Compile; + +import simple.orphaned.internaldafny.types.*; +import OrphanedResource_Compile.*; +import simple.orphaned.ToDafny; +import simple.orphaned.ToNative; +import Wrappers_Compile.*; + +@SuppressWarnings({"unchecked", "deprecation"}) +public class __default extends _ExternBase___default { + public static simple.orphaned.internaldafny.types.OrphanedStructure InitializeOrphanedStructure(simple.orphaned.internaldafny.types.OrphanedStructure input) { + simple.orphaned.model.OrphanedStructure nativeStructure = ToNative.OrphanedStructure(input); + simple.orphaned.model.OrphanedStructure newNativeStructure = nativeStructure.toBuilder().stringValue( + "the extern MUST use Smithy-generated conversions to set this value in the native structure" + ).build(); + simple.orphaned.internaldafny.types.OrphanedStructure newDafnyStructure = ToDafny.OrphanedStructure(newNativeStructure); + return newDafnyStructure; + } + + public static Result CallNativeOrphanedResource(OrphanedResource_Compile.OrphanedResource input) { + simple.orphaned.IOrphanedResource nativeResource = ToNative.OrphanedResource(input); + simple.orphaned.model.OrphanedResourceOperationOutput output = nativeResource.OrphanedResourceOperation( + simple.orphaned.model.OrphanedResourceOperationInput.builder() + .someString("the extern MUST provide this string to the native resource's operation") + .build() + ); + simple.orphaned.internaldafny.types.OrphanedResourceOperationOutput dafnyOutput = ToDafny.OrphanedResourceOperationOutput(output); + return Result.create_Success( + simple.orphaned.internaldafny.types.OrphanedResourceOperationOutput._typeDescriptor(), + simple.orphaned.internaldafny.types.Error._typeDescriptor(), + dafnyOutput + ); + } + + public static simple.orphaned.internaldafny.types.Error CallNativeOrphanedError(simple.orphaned.internaldafny.types.Error input) { + simple.orphaned.model.OrphanedError nativeError = ToNative.Error((simple.orphaned.internaldafny.types.Error_OrphanedError) input); + simple.orphaned.model.OrphanedError updatedNativeError = nativeError.toBuilder() + .message("the extern MUST set this string using the catch-all error converter, NOT the orphaned error-specific converter") + .build(); + simple.orphaned.internaldafny.types.Error dafnyErrorAgain = ToDafny.Error(updatedNativeError); + return dafnyErrorAgain; + } +} diff --git a/TestModels/OrphanedShapes/runtimes/java/src/test/java/simple/orphaned/internaldafny/wrapped/__default.java b/TestModels/OrphanedShapes/runtimes/java/src/test/java/simple/orphaned/internaldafny/wrapped/__default.java new file mode 100644 index 0000000000..9a8feca64e --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/java/src/test/java/simple/orphaned/internaldafny/wrapped/__default.java @@ -0,0 +1,32 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package simple.orphaned.internaldafny.wrapped; + +import Wrappers_Compile.Result; +import simple.orphaned.SimpleOrphaned; +import simple.orphaned.ToNative; +import simple.orphaned.internaldafny.types.Error; +import simple.orphaned.internaldafny.types.ISimpleOrphanedClient; +import simple.orphaned.internaldafny.types.SimpleOrphanedConfig; +import simple.orphaned.wrapped.TestSimpleOrphaned; + +public class __default extends _ExternBase___default { + + public static Result WrappedSimpleOrphaned( + SimpleOrphanedConfig config + ) { + simple.orphaned.model.SimpleOrphanedConfig wrappedConfig = + ToNative.SimpleOrphanedConfig(config); + simple.orphaned.SimpleOrphaned impl = SimpleOrphaned + .builder() + .SimpleOrphanedConfig(wrappedConfig) + .build(); + TestSimpleOrphaned wrappedClient = TestSimpleOrphaned + .builder() + .impl(impl) + .build(); + return simple.orphaned.internaldafny.__default.CreateSuccessOfClient( + wrappedClient + ); + } +} diff --git a/TestModels/OrphanedShapes/runtimes/python/pyproject.toml b/TestModels/OrphanedShapes/runtimes/python/pyproject.toml new file mode 100644 index 0000000000..e5bb36f547 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/python/pyproject.toml @@ -0,0 +1,26 @@ +[tool.poetry] +name = "simple-orphaned-shapes" +version = "0.1.0" +description = "" +authors = ["AWS "] +packages = [ + { include = "simple_orphaned", from = "src" } +] +# Include all of the following .gitignored files in package distributions, +# even though it is not included in version control +include = ["**/smithygenerated/**/*.py", "**/internaldafny/generated/*.py"] + +[tool.poetry.dependencies] +python = "^3.11.0" +# TODO: Depend on PyPi once Smithy-Python publishes their Python package there +smithy-python = { path = "../../../../codegen/smithy-dafny-codegen-modules/smithy-python/python-packages/smithy-python", develop = false} + +smithy-dafny-standard-library = {path = "../../../dafny-dependencies/StandardLibrary/runtimes/python", develop = false} +DafnyRuntimePython = "^4.7.0" + +[tool.poetry.group.test.dependencies] +pytest = "^7.4.0" + +[build-system] +requires = ["poetry-core"] +build-backend = "poetry.core.masonry.api" diff --git a/TestModels/OrphanedShapes/runtimes/python/src/simple_orphaned/__init__.py b/TestModels/OrphanedShapes/runtimes/python/src/simple_orphaned/__init__.py new file mode 100644 index 0000000000..67a3d57bd7 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/python/src/simple_orphaned/__init__.py @@ -0,0 +1,5 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# Initialize generated Dafny +from .internaldafny.generated import module_ diff --git a/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/__init__.py b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/__init__.py new file mode 100644 index 0000000000..76a5b798a2 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/__init__.py @@ -0,0 +1,2 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 \ No newline at end of file diff --git a/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/__init__.py b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/__init__.py new file mode 100644 index 0000000000..f94fd12a2e --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/__init__.py @@ -0,0 +1,2 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 diff --git a/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/test_externs.py b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/test_externs.py new file mode 100644 index 0000000000..11575cb399 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/test_externs.py @@ -0,0 +1,36 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +import ExternDefinitions +import simple_orphaned +import simple_orphaned.smithygenerated.simple_orphaned.deserialize +import smithy_dafny_standard_library.internaldafny.generated.Wrappers as Wrappers + +class default__(ExternDefinitions.default__): + + @staticmethod + def InitializeOrphanedStructure(dafny_uninitialized_structure): + native_structure = simple_orphaned.smithygenerated.simple_orphaned.dafny_to_smithy.simple_orphaned_OrphanedStructure(dafny_uninitialized_structure) + native_structure.string_value = "the extern MUST use Smithy-generated conversions to set this value in the native structure" + dafny_initialized_structure = simple_orphaned.smithygenerated.simple_orphaned.smithy_to_dafny.simple_orphaned_OrphanedStructure(native_structure) + return dafny_initialized_structure + + @staticmethod + def CallNativeOrphanedResource(dafny_resource): + native_resource = simple_orphaned.smithygenerated.simple_orphaned.dafny_to_smithy.simple_orphaned_OrphanedResourceReference(dafny_resource) + native_output = native_resource.orphaned_resource_operation( + simple_orphaned.smithygenerated.simple_orphaned.models.OrphanedResourceOperationInput( + some_string = "the extern MUST provide this string to the native resource's operation" + ) + ) + dafny_output = simple_orphaned.smithygenerated.simple_orphaned.smithy_to_dafny.simple_orphaned_OrphanedResourceOperationOutput(native_output) + return Wrappers.Result_Success(dafny_output) + + @staticmethod + def CallNativeOrphanedError(dafny_error): + native_error = simple_orphaned.smithygenerated.simple_orphaned.deserialize._deserialize_error(dafny_error) + native_error.message = "the extern MUST set this string using the catch-all error converter, NOT the orphaned error-specific converter" + dafny_error_again = simple_orphaned.smithygenerated.simple_orphaned.errors._smithy_error_to_dafny_error(native_error) + return dafny_error_again + +ExternDefinitions.default__ = default__ diff --git a/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/wrapped_simple_orphaned.py b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/wrapped_simple_orphaned.py new file mode 100644 index 0000000000..e5b1ac961c --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/extern/wrapped_simple_orphaned.py @@ -0,0 +1,22 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# src imports +from simple_orphaned.smithygenerated.simple_orphaned.client import SimpleOrphaned +from simple_orphaned.smithygenerated.simple_orphaned.shim import SimpleOrphanedShim +from simple_orphaned.smithygenerated.simple_orphaned.config import dafny_config_to_smithy_config +import smithy_dafny_standard_library.internaldafny.generated.Wrappers as Wrappers + +# test imports, not qualified since this isn't in a package +import WrappedSimpleOrphanedService + +class default__(WrappedSimpleOrphanedService.default__): + + @staticmethod + def WrappedSimpleOrphaned(config): + wrapped_config = dafny_config_to_smithy_config(config) + impl = SimpleOrphaned(wrapped_config) + wrapped_client = SimpleOrphanedShim(impl) + return Wrappers.Result_Success(wrapped_client) + +WrappedSimpleOrphanedService.default__ = default__ \ No newline at end of file diff --git a/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/test_dafny_wrapper.py b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/test_dafny_wrapper.py new file mode 100644 index 0000000000..ec829826cb --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/python/test/internaldafny/test_dafny_wrapper.py @@ -0,0 +1,27 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +""" +Wrapper file for executing Dafny tests from pytest. +This allows us to import modules required by Dafny-generated tests +before executing Dafny-generated tests. +pytest will find and execute the `test_dafny` method below, +which will execute the `__main__.py` file in the `dafny` directory. +""" + +import sys + +# Dafny-generated tests are not compiled as a package +# and require adding Dafny-generated test code to PYTHONPATH. +# These files are only on PYTHONPATH for tests executed from this file. + +internaldafny_dir = '/'.join(__file__.split("/")[:-1]) + +sys.path.append(internaldafny_dir + "/extern") +sys.path.append(internaldafny_dir + "/generated") + +# Initialize extern for test +from .extern import wrapped_simple_orphaned + +def test_dafny(): + from .generated import __main__ \ No newline at end of file diff --git a/TestModels/OrphanedShapes/runtimes/python/tox.ini b/TestModels/OrphanedShapes/runtimes/python/tox.ini new file mode 100644 index 0000000000..b626d2496c --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/python/tox.ini @@ -0,0 +1,13 @@ +[tox] +isolated_build = True +envlist = + py{311,312} + +[testenv] +skip_install = true +allowlist_externals = poetry +commands_pre = + poetry lock + poetry install +commands = + poetry run pytest -s -v test/ \ No newline at end of file diff --git a/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml b/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml new file mode 100644 index 0000000000..45c7f4805a --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/rust/Cargo.toml @@ -0,0 +1,22 @@ +[package] +name = "simple_orphaned" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[features] +wrapped-client = [] + +[dependencies] +aws-smithy-runtime = {version = "1.6.0", features = ["client"] } +aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] } +aws-smithy-types = "1.2.0" +dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"} + +[dev-dependencies] +simple_orphaned = { path = ".", features = ["wrapped-client"] } + +[dependencies.tokio] +version = "1.26.0" +features = ["full"] diff --git a/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs b/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs new file mode 100644 index 0000000000..0349a2b625 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/rust/src/extern_definitions.rs @@ -0,0 +1,77 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +use crate::r#_Wrappers_Compile::Result; +use dafny_runtime::rcmut; +use std::cell::UnsafeCell; +use std::rc::Rc; + +pub mod internal_ExternDefinitions_Compile { + + use crate::conversions::*; + use crate::implementation_from_dafny::_ExternDefinitions_Compile::_default; + use crate::implementation_from_dafny::_OrphanedResource_Compile::*; + use crate::simple::orphaned::internaldafny::types as internaldafny_types; + use crate::simple::orphaned::internaldafny::types::*; + use crate::types::*; + + impl _default { + pub fn InitializeOrphanedStructure( + uninitialized_structure: &Rc, + ) -> Rc { + let native_structure = orphaned_structure::from_dafny(uninitialized_structure.clone()); + // I don't think generated Rust objects have a "toBuilder" method. + // Ideally, this extern would convert the Dafny structure to native, + // then set this property on the converted native structure. + // But that is sort of outside the scope of this TestModel. + // The important fact is that the from/to_dafny conversions above and below exist. + let native_structure_new = crate::types::OrphanedStructure::builder().set_string_value(Some( + "the extern MUST use Smithy-generated conversions to set this value in the native structure".to_string() + )).build().unwrap(); + return orphaned_structure::to_dafny(&native_structure_new); + } + + pub fn CallNativeOrphanedResource( + dafny_resource: &Object, + ) -> Rc, Rc>> + { + let native_resource_ref = + crate::conversions::orphaned_resource::from_dafny(dafny_resource.clone()); + let native_resource = native_resource_ref.inner.borrow(); + let native_output = native_resource.orphaned_resource_operation( + crate::operation::orphaned_resource_operation::OrphanedResourceOperationInput { + some_string: std::option::Option::Some( + "the extern MUST provide this string to the native resource's operation" + .to_string(), + ), + }, + ); + + let dafny_output = + orphaned_resource_operation::_orphaned_resource_operation_output::to_dafny( + native_output.unwrap(), + ); + + ::std::rc::Rc::new(Result::< + Rc, + Rc, + >::Success { + value: dafny_output, + }) + } + + pub fn CallNativeOrphanedError(dafny_error: &Rc) -> Rc { + let native_error = crate::conversions::error::from_dafny(dafny_error.clone()); + // I don't think generated Rust objects have a way for me to update the message + // on a pre-existing object (i.e. public fields or a .toBuilder). + // Ideally, this extern would convert the Dafny structure to native, + // then set this property on the converted native structure. + // But that is sort of outside the scope of this TestModel. + // The fact that the from/to_dafny conversions above and below exist are the important things. + let native_error_new = crate::types::error::Error::OrphanedError { + message : "the extern MUST set this string using the catch-all error converter, NOT the orphaned error-specific converter".to_string() + }; + return crate::conversions::error::to_dafny(native_error_new); + } + } +} diff --git a/TestModels/OrphanedShapes/runtimes/rust/src/lib.rs b/TestModels/OrphanedShapes/runtimes/rust/src/lib.rs new file mode 100644 index 0000000000..3d089722f7 --- /dev/null +++ b/TestModels/OrphanedShapes/runtimes/rust/src/lib.rs @@ -0,0 +1,26 @@ +#![allow( + deprecated, + non_upper_case_globals, + unused, + non_snake_case, + non_camel_case_types +)] + +pub mod client; +pub mod conversions; +pub mod deps; +/// Common errors and error handling utilities. +pub mod error; +pub mod extern_definitions; +pub(crate) mod implementation_from_dafny; +/// All operations that this crate can perform. +pub mod operation; +mod standard_library_conversions; +mod standard_library_externs; +pub mod types; +pub mod validation; +pub mod wrapped; +pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile; +pub(crate) use crate::implementation_from_dafny::simple; +pub use crate::types::simple_orphaned_config::SimpleOrphanedConfig; +pub use client::Client; diff --git a/TestModels/OrphanedShapes/src/Index.dfy b/TestModels/OrphanedShapes/src/Index.dfy new file mode 100644 index 0000000000..2fe489ca2f --- /dev/null +++ b/TestModels/OrphanedShapes/src/Index.dfy @@ -0,0 +1,31 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "SimpleOrphanedImpl.dfy" + +module {:extern "simple.orphaned.internaldafny" } SimpleOrphaned refines AbstractSimpleOrphanedService { + import Operations = SimpleOrphanedImpl + + function method DefaultSimpleOrphanedConfig(): SimpleOrphanedConfig { + SimpleOrphanedConfig + } + + method SimpleOrphaned(config: SimpleOrphanedConfig) + returns (res: Result) + { + var client := new SimpleOrphanedClient(Operations.Config); + return Success(client); + } + + class SimpleOrphanedClient... { + predicate ValidState() { + && Operations.ValidInternalConfig?(config) + && Modifies == Operations.ModifiesInternalConfig(config) + {History} + } + + constructor(config: Operations.InternalConfig) { + this.config := config; + History := new ISimpleOrphanedClientCallHistory(); + Modifies := Operations.ModifiesInternalConfig(config) + {History}; + } + } +} diff --git a/TestModels/OrphanedShapes/src/OrphanedResource.dfy b/TestModels/OrphanedShapes/src/OrphanedResource.dfy new file mode 100644 index 0000000000..6a7e123bcf --- /dev/null +++ b/TestModels/OrphanedShapes/src/OrphanedResource.dfy @@ -0,0 +1,54 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../Model/SimpleOrphanedTypes.dfy" + +// This resource is orphaned in the Smithy model. +module OrphanedResource { + import opened StandardLibrary + import opened Wrappers + import Types = SimpleOrphanedTypes + + class OrphanedResource extends Types.IOrphanedResource + { + predicate ValidState() + ensures ValidState() ==> History in Modifies + { + && History in Modifies + } + + constructor ( + ) + { + History := new Types.IOrphanedResourceCallHistory(); + Modifies := {History}; + } + + predicate OrphanedResourceOperationEnsuresPublicly( + input: Types.OrphanedResourceOperationInput, + output: Result + ) {true} + + method OrphanedResourceOperation'( + input: Types.OrphanedResourceOperationInput + ) returns ( + output: Result + ) + requires ValidState() + modifies Modifies - {History} + decreases Modifies - {History} + ensures && ValidState() + ensures OrphanedResourceOperationEnsuresPublicly(input, output) + ensures unchanged(History) + { + if ( + && input.someString.Some? + && input.someString.value == "the extern MUST provide this string to the native resource's operation" + ) { + return Success(Types.OrphanedResourceOperationOutput(someString := Some("correct string"))); + } else { + return Failure(Types.Error.OrphanedError(message := "incorrect string")); + } + } + } +} diff --git a/TestModels/OrphanedShapes/src/SimpleOrphanedImpl.dfy b/TestModels/OrphanedShapes/src/SimpleOrphanedImpl.dfy new file mode 100644 index 0000000000..c8e2fd85b1 --- /dev/null +++ b/TestModels/OrphanedShapes/src/SimpleOrphanedImpl.dfy @@ -0,0 +1,15 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../Model/SimpleOrphanedTypes.dfy" +include "OrphanedResource.dfy" + +module SimpleOrphanedImpl refines AbstractSimpleOrphanedOperations { + + datatype Config = Config + type InternalConfig = Config + predicate ValidInternalConfig?(config: InternalConfig) + {true} + function ModifiesInternalConfig(config: InternalConfig) : set + {{}} +} \ No newline at end of file diff --git a/TestModels/OrphanedShapes/src/WrappedSimpleOrphanedImpl.dfy b/TestModels/OrphanedShapes/src/WrappedSimpleOrphanedImpl.dfy new file mode 100644 index 0000000000..db9896c073 --- /dev/null +++ b/TestModels/OrphanedShapes/src/WrappedSimpleOrphanedImpl.dfy @@ -0,0 +1,10 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../Model/SimpleOrphanedTypesWrapped.dfy" + +module {:options "--function-syntax:4"} {:extern "simple.orphaned.internaldafny.wrapped"} WrappedSimpleOrphanedService refines WrappedAbstractSimpleOrphanedService { + import WrappedService = SimpleOrphaned + function WrappedDefaultSimpleOrphanedConfig(): SimpleOrphanedConfig { + SimpleOrphanedConfig + } +} diff --git a/TestModels/OrphanedShapes/test/ExternDefinitions.dfy b/TestModels/OrphanedShapes/test/ExternDefinitions.dfy new file mode 100644 index 0000000000..6d91d33919 --- /dev/null +++ b/TestModels/OrphanedShapes/test/ExternDefinitions.dfy @@ -0,0 +1,68 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../Model/SimpleOrphanedTypes.dfy" +include "../src/OrphanedResource.dfy" + +module {:extern} ExternDefinitions { + + import opened Wrappers + import Types = SimpleOrphanedTypes + import OrphanedResource + + method TestOrphanedStructure () + { + var uninitializedStructure := Types.OrphanedStructure(); + var initializedStructure := InitializeOrphanedStructure(uninitializedStructure); + + expect initializedStructure.stringValue.Some?; + expect initializedStructure.stringValue.value == "the extern MUST use Smithy-generated conversions to set this value in the native structure"; + } + + method TestOrphanedResource () + { + var resource := new OrphanedResource.OrphanedResource(); + var ret := CallNativeOrphanedResource(resource); + + expect ret.Success?; + expect ret.value.someString.Some?; + expect ret.value.someString.value == "correct string"; + } + + method TestOrphanedError () + { + var error := Types.Error.OrphanedError(message := "TBD"); + var out_error := CallNativeOrphanedError(error); + + expect out_error.OrphanedError?; + expect out_error.message == "the extern MUST set this string using the catch-all error converter, NOT the orphaned error-specific converter"; + } + + // This extern MUST use Smithy-generated type conversions to initialize the input in the native OrphanedStructure. + // This will ensure that OrphanedStructure and its conversions are generated, + // even though OrphanedStructure is "orphaned". + + // OrphanedStructure is orphaned because InitializeOrphanedStructure is not a modelled operation. + // The Smithy model does not know about this operation, + // so it doesn't register OrphanedStructure as an operation shape. + // If this operation were on the Smithy model, + // both the operation and OrphanedStructure would no longer be orphaned, + // and wouldn't be useful in an "orphaned shapes" TestModel. + // Putting all usage of the orphaned shape outside the model's knowledge + // lets us test orphaned shape model/conversion generation. + method {:extern} InitializeOrphanedStructure( input: Types.OrphanedStructure ) + returns (output: Types.OrphanedStructure) + + // This extern MUST use Smithy-generated type conversions to call the operation on the native OrphanedResource. + // This will ensure that OrphanedResource and its conversions are generated, + // even though OrphanedResource is "orphaned". + method {:extern} CallNativeOrphanedResource( input: Types.IOrphanedResource ) + returns (output: Result) + + // This extern MUST use Smithy-generated type conversions to convert the Dafny error to/from native. + // In particular, the extern MUST use the catch-all/common error handler for this conversion. + // The extern MUST NOT use some error handler specific to OrphanedError. + // This will ensure that orphaned errors are handled in the catch-all/common error handler. + method {:extern} CallNativeOrphanedError( input: Types.Error ) + returns (output: Types.Error ) +} \ No newline at end of file diff --git a/TestModels/OrphanedShapes/test/WrappedTest.dfy b/TestModels/OrphanedShapes/test/WrappedTest.dfy new file mode 100644 index 0000000000..ded4b88f01 --- /dev/null +++ b/TestModels/OrphanedShapes/test/WrappedTest.dfy @@ -0,0 +1,27 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../src/WrappedSimpleOrphanedImpl.dfy" +include "ExternDefinitions.dfy" + +// There are no non-wrapped tests for this TestModel. +// This TestModel requires implementing externs that use Polymorph-generated code. +// Polymorph must be in the mix, so it is reasonable to only have wrapped tests. + +module WrappedTest { + import WrappedSimpleOrphanedService + import opened Types = SimpleOrphanedTypes + import ExternDefinitions + + method {:test} TestOrphanedStructure() { + ExternDefinitions.TestOrphanedStructure(); + } + + method {:test} TestOrphanedResource() { + ExternDefinitions.TestOrphanedResource(); + } + + method {:test} TestOrphanedError() { + ExternDefinitions.TestOrphanedError(); + } +} diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydotnet/DotnetTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydotnet/DotnetTestModels.java index 194bb3f234..da8f77119e 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydotnet/DotnetTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydotnet/DotnetTestModels.java @@ -23,6 +23,8 @@ class DotnetTestModels extends TestModelTest { DISABLED_TESTS.add("Documentation"); DISABLED_TESTS.add("LanguageSpecificLogic"); DISABLED_TESTS.add("LocalService"); + // Needs work to generate some missing orphaned shape conversion methods + DISABLED_TESTS.add("OrphanedShapes"); DISABLED_TESTS.add("SimpleTypes/BigDecimal"); DISABLED_TESTS.add("SimpleTypes/BigInteger"); DISABLED_TESTS.add("SimpleTypes/SimpleByte"); diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithygo/GoTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithygo/GoTestModels.java index 2bb352aa83..47bb0fecdc 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithygo/GoTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithygo/GoTestModels.java @@ -21,6 +21,8 @@ class GoTestModels extends TestModelTest { DISABLED_TESTS.add("AggregateReferences"); DISABLED_TESTS.add("Documentation"); DISABLED_TESTS.add("LanguageSpecificLogic"); + // Needs work to generate some missing orphaned shape conversion methods + DISABLED_TESTS.add("OrphanedShapes"); DISABLED_TESTS.add("SimpleTypes/BigDecimal"); DISABLED_TESTS.add("SimpleTypes/BigInteger"); DISABLED_TESTS.add("SimpleTypes/SimpleByte"); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/common/shapevisitor/conversionwriter/BaseConversionWriter.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/common/shapevisitor/conversionwriter/BaseConversionWriter.java index 4f2317929e..c467850e23 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/common/shapevisitor/conversionwriter/BaseConversionWriter.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/common/shapevisitor/conversionwriter/BaseConversionWriter.java @@ -7,12 +7,14 @@ import java.util.HashSet; import java.util.List; import java.util.Set; +import software.amazon.polymorph.smithypython.awssdk.nameresolver.AwsSdkNameResolver; import software.amazon.polymorph.smithypython.wrappedlocalservice.DafnyPythonWrappedLocalServiceProtocolGenerator; import software.amazon.smithy.model.shapes.Shape; import software.amazon.smithy.model.shapes.StringShape; import software.amazon.smithy.model.shapes.StructureShape; import software.amazon.smithy.model.shapes.UnionShape; import software.amazon.smithy.model.traits.EnumTrait; +import software.amazon.smithy.model.traits.ErrorTrait; import software.amazon.smithy.python.codegen.GenerationContext; import software.amazon.smithy.python.codegen.PythonWriter; @@ -95,6 +97,12 @@ public void baseWriteConverterForShapeAndMembers( Shape toGenerate = shapesToGenerate.remove(0); generatedShapes.add(toGenerate); + if (!shapeShouldHaveConversionFunction(toGenerate)) { + throw new IllegalArgumentException( + "Unsupported shape passed to ConversionWriter: " + toGenerate + ); + } + if (toGenerate.isStructureShape()) { writeStructureShapeConverter(toGenerate.asStructureShape().get()); } else if (toGenerate.isUnionShape()) { @@ -121,4 +129,34 @@ protected abstract void writeStructureShapeConverter( protected abstract void writeStringEnumShapeConverter( StringShape stringShapeWithEnumTrait ); + + /** + * Returns true if a conversion function should be written for the shape, false otherwise. + * Conversion functions are only written for "complex" shapes: + * - StructureShapes ("complex" because StructureShapes can be recursive) + * - except for non-AWS SDK StructureShapes with ErrorTrait; these aren't "complex" + * - UnionShapes ("complex" because the conversion is not a one-liner) + * - EnumShapes or StringShapes with EnumTrait ("complex" because the conversion is not a one-liner) + * @param shape + * @return + */ + public static boolean shapeShouldHaveConversionFunction(Shape shape) { + if (shape.isStructureShape()) { + if ( + !AwsSdkNameResolver.isAwsSdkShape(shape) && + shape.hasTrait(ErrorTrait.class) + ) { + return false; + } + return true; + } else if (shape.isUnionShape()) { + return true; + } else if ( + (shape.isStringShape() && shape.hasTrait(EnumTrait.class)) || + shape.isEnumShape() + ) { + return true; + } + return false; + } } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/extensions/DirectedDafnyPythonLocalServiceCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/extensions/DirectedDafnyPythonLocalServiceCodegen.java index 4e3dadf6d7..f761c50305 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/extensions/DirectedDafnyPythonLocalServiceCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/extensions/DirectedDafnyPythonLocalServiceCodegen.java @@ -4,6 +4,7 @@ package software.amazon.polymorph.smithypython.localservice.extensions; import static java.lang.String.format; +import static software.amazon.polymorph.smithypython.common.shapevisitor.conversionwriter.BaseConversionWriter.shapeShouldHaveConversionFunction; import static software.amazon.polymorph.utils.ModelUtils.getTopologicallyOrderedOrphanedShapesForService; import java.nio.file.Path; @@ -12,10 +13,13 @@ import software.amazon.polymorph.smithypython.common.nameresolver.SmithyNameResolver; import software.amazon.polymorph.smithypython.localservice.DafnyLocalServiceCodegenConstants; import software.amazon.polymorph.smithypython.localservice.customize.ReferencesFileWriter; +import software.amazon.polymorph.smithypython.localservice.shapevisitor.conversionwriter.DafnyToLocalServiceConversionFunctionWriter; +import software.amazon.polymorph.smithypython.localservice.shapevisitor.conversionwriter.LocalServiceToDafnyConversionFunctionWriter; import software.amazon.smithy.build.FileManifest; import software.amazon.smithy.codegen.core.*; import software.amazon.smithy.codegen.core.directed.*; import software.amazon.smithy.model.shapes.*; +import software.amazon.smithy.model.traits.EnumTrait; import software.amazon.smithy.model.traits.ErrorTrait; import software.amazon.smithy.python.codegen.*; @@ -492,6 +496,10 @@ protected void generateOrphanedShapesForService( structureShape, directive.context() ); + // Errors don't get explicit conversion functions; + // Conversions are done in a catch-all function + // (This could be changed in the future) + continue; } else { writeStructureShape(structureShape, directive.context()); } @@ -506,15 +514,19 @@ protected void generateOrphanedShapesForService( directive.context() ); } else if (shapeToGenerate.isStringShape()) { - // Classes are not generated for strings + // Neither classes nor converisons are generated for strings } else if (shapeToGenerate.isIntegerShape()) { - // Classes are not generated for ints + // Neither classes nor converisons are generated for ints } else if (shapeToGenerate.isListShape()) { - // Classes are not generated for lists + // Neither classes nor converisons are generated for lists } else if (shapeToGenerate.isMapShape()) { - // Classes are not generated for maps + // Neither classes nor converisons are generated for maps } else if (shapeToGenerate.isLongShape()) { - // Classes are not generated for longs + // Neither classes nor converisons are generated for longs + } else if (shapeToGenerate.isBlobShape()) { + // Neither classes nor converisons are generated for blobs + } else if (shapeToGenerate.isBooleanShape()) { + // Neither classes nor converisons are generated for blobs } else { // Add more as needed... throw new ClassCastException( @@ -525,6 +537,57 @@ protected void generateOrphanedShapesForService( } } + /** + * This MUST run after code generation for non-orphaned shapes. + * Orphaned shapes may topologically depend on non-orphaned shapes, but not vice versa. + * + * @param directive + */ + protected void generateOrphanedShapeConversionMethods( + GenerateServiceDirective directive + ) { + List orderedShapes = getTopologicallyOrderedOrphanedShapesForService( + directive.shape(), + directive.model() + ); + + for (Shape shapeToGenerate : orderedShapes) { + if (shapeShouldHaveConversionFunction(shapeToGenerate)) { + final WriterDelegator delegator = directive + .context() + .writerDelegator(); + final String moduleName = + SmithyNameResolver.getServiceSmithygeneratedDirectoryNameForNamespace( + directive.context().settings().getService().getNamespace() + ); + + delegator.useFileWriter( + moduleName + "/dafny_to_smithy.py", + "", + conversionWriter -> { + DafnyToLocalServiceConversionFunctionWriter.writeConverterForShapeAndMembers( + shapeToGenerate, + directive.context(), + conversionWriter + ); + } + ); + + delegator.useFileWriter( + moduleName + "/smithy_to_dafny.py", + "", + conversionWriter -> { + LocalServiceToDafnyConversionFunctionWriter.writeConverterForShapeAndMembers( + shapeToGenerate, + directive.context(), + conversionWriter + ); + } + ); + } + } + } + /** * Override Smithy-Python's generateService to generate a synchronous client. * Smithy-Python-generated clients' methods are all async. @@ -560,6 +623,16 @@ public void generateService( protocolGenerator.generateSharedDeserializerComponents(directive.context()); protocolGenerator.generateResponseDeserializers(directive.context()); + // Generate any missing conversion. + // This SHOULD run after generateRequestSerializers and generateResponseDeserializers + // to preserve topological ordering of generated functions. + // I don't think that topological ordering is required here + // (no function's top-level definition depends on another function in this file) + // but this could change in the future, so best to preserve the correct ordering. + // (An orphaned conversion function MAY depend on a non-orphaned conversion function, + // but never the other way around.) + generateOrphanedShapeConversionMethods(directive); + protocolGenerator.generateProtocolTests(directive.context()); } }