From 5a5a5cc523715b88a86b3b3b70d0f8b52acc166a Mon Sep 17 00:00:00 2001 From: Shubham Chaturvedi Date: Wed, 23 Oct 2024 18:11:03 -0700 Subject: [PATCH] feat: enable ddbv2 support --- TestModels/aws-sdks/ddbv2/Model/model.json | 116 +++++++++++++++++- .../codegen-patches/dotnet/dafny-4.5.0.patch | 20 +++ .../codegen-patches/dotnet/dafny-4.8.0.patch | 20 +++ .../ddbv2/runtimes/java/build.gradle.kts | 94 ++++++++++++++ .../dynamodb/internaldafny/__default.java | 39 ++++++ .../internaldafny/types/__default.java | 6 + .../aws-sdks/ddbv2/runtimes/net/.editorconfig | 29 +++++ .../aws-sdks/ddbv2/runtimes/net/DDBv2.csproj | 34 +++++ .../ddbv2/runtimes/net/Extern/DDBv2Client.cs | 31 +++++ .../ddbv2/runtimes/net/tests/TestDDBv2.csproj | 25 ++++ .../aws-sdks/ddbv2/runtimes/rust/Cargo.toml | 27 ++++ .../aws-sdks/ddbv2/runtimes/rust/src/ddb.rs | 42 +++++++ .../dafny-dependencies/Model/aws.test.smithy | 58 +++++++++ .../smithydotnet/DotnetTestModels.java | 3 - .../polymorph/smithyjava/JavaTestModels.java | 3 - .../polymorph/smithyrust/RustTestModels.java | 3 - .../AwsSdkDotNetNameResolver.java | 21 ++-- .../generator/awssdk/v2/ToNativeAwsV2.java | 1 + .../smithyjava/nameresolver/Dafny.java | 1 + 19 files changed, 551 insertions(+), 22 deletions(-) create mode 100644 TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.5.0.patch create mode 100644 TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.8.0.patch create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/java/build.gradle.kts create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/types/__default.java create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/net/.editorconfig create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/net/DDBv2.csproj create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/net/Extern/DDBv2Client.cs create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/net/tests/TestDDBv2.csproj create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/rust/Cargo.toml create mode 100644 TestModels/aws-sdks/ddbv2/runtimes/rust/src/ddb.rs create mode 100644 TestModels/dafny-dependencies/Model/aws.test.smithy diff --git a/TestModels/aws-sdks/ddbv2/Model/model.json b/TestModels/aws-sdks/ddbv2/Model/model.json index b7ceadec4..6adea74bb 100644 --- a/TestModels/aws-sdks/ddbv2/Model/model.json +++ b/TestModels/aws-sdks/ddbv2/Model/model.json @@ -3604,10 +3604,10 @@ "com.amazonaws.dynamodb#DisableKinesisStreamingDestination": { "type": "operation", "input": { - "target": "com.amazonaws.dynamodb#KinesisStreamingDestinationInput" + "target": "com.amazonaws.dynamodb#DisableKinesisStreamingDestinationInput" }, "output": { - "target": "com.amazonaws.dynamodb#KinesisStreamingDestinationOutput" + "target": "com.amazonaws.dynamodb#DisableKinesisStreamingDestinationOutput" }, "errors": [ { @@ -4944,10 +4944,10 @@ "com.amazonaws.dynamodb#EnableKinesisStreamingDestination": { "type": "operation", "input": { - "target": "com.amazonaws.dynamodb#KinesisStreamingDestinationInput" + "target": "com.amazonaws.dynamodb#EnableKinesisStreamingDestinationInput" }, "output": { - "target": "com.amazonaws.dynamodb#KinesisStreamingDestinationOutput" + "target": "com.amazonaws.dynamodb#EnableKinesisStreamingDestinationOutput" }, "errors": [ { @@ -7260,6 +7260,114 @@ } } }, + "com.amazonaws.dynamodb#DisableKinesisStreamingDestinationInput": { + "type": "structure", + "members": { + "TableName": { + "target": "com.amazonaws.dynamodb#TableArn", + "traits": { + "smithy.api#documentation": "

The name of the DynamoDB table. You can also provide the Amazon Resource Name (ARN) of the\n table in this parameter.

", + "smithy.api#required": {} + } + }, + "StreamArn": { + "target": "com.amazonaws.dynamodb#StreamArn", + "traits": { + "smithy.api#documentation": "

The ARN for a Kinesis data stream.

", + "smithy.api#required": {} + } + }, + "EnableKinesisStreamingConfiguration": { + "target": "com.amazonaws.dynamodb#EnableKinesisStreamingConfiguration", + "traits": { + "smithy.api#documentation": "

The source for the Kinesis streaming information that is being enabled.

" + } + } + } + }, + "com.amazonaws.dynamodb#DisableKinesisStreamingDestinationOutput": { + "type": "structure", + "members": { + "TableName": { + "target": "com.amazonaws.dynamodb#TableName", + "traits": { + "smithy.api#documentation": "

The name of the table being modified.

" + } + }, + "StreamArn": { + "target": "com.amazonaws.dynamodb#StreamArn", + "traits": { + "smithy.api#documentation": "

The ARN for the specific Kinesis data stream.

" + } + }, + "DestinationStatus": { + "target": "com.amazonaws.dynamodb#DestinationStatus", + "traits": { + "smithy.api#documentation": "

The current status of the replication.

" + } + }, + "EnableKinesisStreamingConfiguration": { + "target": "com.amazonaws.dynamodb#EnableKinesisStreamingConfiguration", + "traits": { + "smithy.api#documentation": "

The destination for the Kinesis streaming information that is being enabled.

" + } + } + } + }, + "com.amazonaws.dynamodb#EnableKinesisStreamingDestinationInput": { + "type": "structure", + "members": { + "TableName": { + "target": "com.amazonaws.dynamodb#TableArn", + "traits": { + "smithy.api#documentation": "

The name of the DynamoDB table. You can also provide the Amazon Resource Name (ARN) of the\n table in this parameter.

", + "smithy.api#required": {} + } + }, + "StreamArn": { + "target": "com.amazonaws.dynamodb#StreamArn", + "traits": { + "smithy.api#documentation": "

The ARN for a Kinesis data stream.

", + "smithy.api#required": {} + } + }, + "EnableKinesisStreamingConfiguration": { + "target": "com.amazonaws.dynamodb#EnableKinesisStreamingConfiguration", + "traits": { + "smithy.api#documentation": "

The source for the Kinesis streaming information that is being enabled.

" + } + } + } + }, + "com.amazonaws.dynamodb#EnableKinesisStreamingDestinationOutput": { + "type": "structure", + "members": { + "TableName": { + "target": "com.amazonaws.dynamodb#TableName", + "traits": { + "smithy.api#documentation": "

The name of the table being modified.

" + } + }, + "StreamArn": { + "target": "com.amazonaws.dynamodb#StreamArn", + "traits": { + "smithy.api#documentation": "

The ARN for the specific Kinesis data stream.

" + } + }, + "DestinationStatus": { + "target": "com.amazonaws.dynamodb#DestinationStatus", + "traits": { + "smithy.api#documentation": "

The current status of the replication.

" + } + }, + "EnableKinesisStreamingConfiguration": { + "target": "com.amazonaws.dynamodb#EnableKinesisStreamingConfiguration", + "traits": { + "smithy.api#documentation": "

The destination for the Kinesis streaming information that is being enabled.

" + } + } + } + }, "com.amazonaws.dynamodb#LastUpdateDateTime": { "type": "timestamp" }, diff --git a/TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.5.0.patch b/TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.5.0.patch new file mode 100644 index 000000000..5f6d63818 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.5.0.patch @@ -0,0 +1,20 @@ +diff --git a/TestModels/aws-sdks/ddb/runtimes/net/Generated/TypeConversion.cs b/TestModels/aws-sdks/ddb/runtimes/net/Generated/TypeConversion.cs +index a2b924092..58c542008 100644 +--- a/TestModels/aws-sdks/ddb/runtimes/net/Generated/TypeConversion.cs ++++ b/TestModels/aws-sdks/ddb/runtimes/net/Generated/TypeConversion.cs +@@ -213,11 +213,10 @@ namespace Com.Amazonaws.Dynamodb + } + public static Amazon.DynamoDBv2.Model.ConditionalCheckFailedException FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException(software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ConditionalCheckFailedException value) + { +- return new Amazon.DynamoDBv2.Model.ConditionalCheckFailedException( +- FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M7_message(value._message) +- , +- FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M4_Item(value._Item) +- ); ++ var conditionalCheckFailedException = new Amazon.DynamoDBv2.Model.ConditionalCheckFailedException( ++ FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M7_message(value._message)); ++ conditionalCheckFailedException.Item = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M4_Item(value._Item); ++ return conditionalCheckFailedException; + } + public static software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ConditionalCheckFailedException ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException(Amazon.DynamoDBv2.Model.ConditionalCheckFailedException value) + { diff --git a/TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.8.0.patch b/TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.8.0.patch new file mode 100644 index 000000000..5f6d63818 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.8.0.patch @@ -0,0 +1,20 @@ +diff --git a/TestModels/aws-sdks/ddb/runtimes/net/Generated/TypeConversion.cs b/TestModels/aws-sdks/ddb/runtimes/net/Generated/TypeConversion.cs +index a2b924092..58c542008 100644 +--- a/TestModels/aws-sdks/ddb/runtimes/net/Generated/TypeConversion.cs ++++ b/TestModels/aws-sdks/ddb/runtimes/net/Generated/TypeConversion.cs +@@ -213,11 +213,10 @@ namespace Com.Amazonaws.Dynamodb + } + public static Amazon.DynamoDBv2.Model.ConditionalCheckFailedException FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException(software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ConditionalCheckFailedException value) + { +- return new Amazon.DynamoDBv2.Model.ConditionalCheckFailedException( +- FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M7_message(value._message) +- , +- FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M4_Item(value._Item) +- ); ++ var conditionalCheckFailedException = new Amazon.DynamoDBv2.Model.ConditionalCheckFailedException( ++ FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M7_message(value._message)); ++ conditionalCheckFailedException.Item = FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException__M4_Item(value._Item); ++ return conditionalCheckFailedException; + } + public static software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ConditionalCheckFailedException ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S31_ConditionalCheckFailedException(Amazon.DynamoDBv2.Model.ConditionalCheckFailedException value) + { diff --git a/TestModels/aws-sdks/ddbv2/runtimes/java/build.gradle.kts b/TestModels/aws-sdks/ddbv2/runtimes/java/build.gradle.kts new file mode 100644 index 000000000..7e3ea0d90 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/java/build.gradle.kts @@ -0,0 +1,94 @@ +// 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 + +plugins { + `java-library` + `maven-publish` +} + +var props = Properties().apply { + load(FileInputStream(File(rootProject.rootDir, "../../project.properties"))) +} +var dafnyVersion = props.getProperty("dafnyVersion") + +group = "software.amazon.cryptography" +version = "1.0-SNAPSHOT" +description = "ComAmazonawsDynamodb" + +var caUrl: URI? = null +@Nullable +val caUrlStr: String? = System.getenv("CODEARTIFACT_URL_JAVA_CONVERSION") +if (!caUrlStr.isNullOrBlank()) { + caUrl = URI.create(caUrlStr) +} + +var caPassword: String? = null +@Nullable +val caPasswordString: String? = System.getenv("CODEARTIFACT_AUTH_TOKEN") +if (!caPasswordString.isNullOrBlank()) { + caPassword = caPasswordString +} + +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/dafny-generated") + } +} + +repositories { + mavenCentral() + mavenLocal() + if (caUrl != null && caPassword != null) { + maven { + name = "CodeArtifact" + url = caUrl!! + credentials { + username = "aws" + password = caPassword!! + } + } + } +} + +dependencies { + implementation("org.dafny:DafnyRuntime:${dafnyVersion}") + implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT") + implementation("software.amazon.smithy.dafny:conversion:0.1.1") + implementation(platform("software.amazon.awssdk:bom:2.28.28")) + implementation("software.amazon.awssdk:dynamodb") +} + +publishing { + publications.create("maven") { + groupId = "software.amazon.cryptography" + artifactId = "ComAmazonawsDynamodb" + from(components["java"]) + } + repositories { mavenLocal() } +} + +tasks.withType() { + options.encoding = "UTF-8" +} + +tasks.withType() { + gradleVersion = "7.6" +} + +tasks { + register("runTests", JavaExec::class.java) { + mainClass.set("TestsFromDafny") + classpath = sourceSets["test"].runtimeClasspath + } +} diff --git a/TestModels/aws-sdks/ddbv2/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java b/TestModels/aws-sdks/ddbv2/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java new file mode 100644 index 000000000..45b68cdcc --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java @@ -0,0 +1,39 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package software.amazon.cryptography.services.dynamodb.internaldafny; + +import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence; +import static software.amazon.smithy.dafny.conversion.ToNative.Simple.String; + +import StandardLibraryInterop_Compile.WrappersInterop; +import Wrappers_Compile.Option; +import Wrappers_Compile.Result; +import dafny.DafnySequence; +import software.amazon.awssdk.auth.credentials.ProfileCredentialsProvider; +import software.amazon.awssdk.regions.Region; +import software.amazon.awssdk.regions.providers.DefaultAwsRegionProviderChain; +import software.amazon.awssdk.services.dynamodb.DynamoDbClient; +import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error; +import software.amazon.cryptography.services.dynamodb.internaldafny.types.IDynamoDBClient; + +public class __default + extends software.amazon.cryptography.services.dynamodb.internaldafny._ExternBase___default { + + public static Result DynamoDBClient() { + try { + Region region = new DefaultAwsRegionProviderChain().getRegion(); + final DynamoDbClient ddbClient = DynamoDbClient + .builder() + .region(region) + .build(); + + IDynamoDBClient shim = new Shim(ddbClient, region.toString()); + return CreateSuccessOfClient(shim); + } catch (Exception e) { + Error dafny_error = Error.create_InternalServerError( + WrappersInterop.CreateStringSome(CharacterSequence(e.getMessage())) + ); + return CreateFailureOfError(dafny_error); + } + } +} diff --git a/TestModels/aws-sdks/ddbv2/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/types/__default.java b/TestModels/aws-sdks/ddbv2/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/types/__default.java new file mode 100644 index 000000000..9c8b51b46 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/java/src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/types/__default.java @@ -0,0 +1,6 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package software.amazon.cryptography.services.dynamodb.internaldafny.types; + +public class __default + extends software.amazon.cryptography.services.dynamodb.internaldafny.types._ExternBase___default {} diff --git a/TestModels/aws-sdks/ddbv2/runtimes/net/.editorconfig b/TestModels/aws-sdks/ddbv2/runtimes/net/.editorconfig new file mode 100644 index 000000000..c4091548c --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/net/.editorconfig @@ -0,0 +1,29 @@ +############################### +# Core EditorConfig Options # +# See https://github.com/dotnet/format/blob/main/docs/Supported-.editorconfig-options.md +############################### +root = true +# All files +[*] +indent_style = space + +# XML project files +[*.{csproj,vbproj,vcxproj,vcxproj.filters,proj,projitems,shproj}] +indent_size = 2 + +# XML config files +[*.{props,targets,ruleset,config,nuspec,resx,vsixmanifest,vsct}] +indent_size = 2 + +# Code files +[*.{cs,csx,vb,vbx}] +indent_size = 2 +insert_final_newline = true + +# Rider is wrong, dotnet_diagnostic is supported +# noinspection EditorConfigKeyCorrectness +[*.{cs,vb}] +dotnet_diagnostic.CS0436.severity = none # The type <> ... conflicts with the imported type <> in ... +dotnet_diagnostic.CS0162.severity = none # Unreachable code detected +dotnet_diagnostic.CS0618.severity = none # obsolete +dotnet_diagnostic.CS0168.severity = none # Unused variable diff --git a/TestModels/aws-sdks/ddbv2/runtimes/net/DDBv2.csproj b/TestModels/aws-sdks/ddbv2/runtimes/net/DDBv2.csproj new file mode 100644 index 000000000..a958c96c4 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/net/DDBv2.csproj @@ -0,0 +1,34 @@ + + + + DDBv2 + disable + disable + net6.0 + 10 + false + + + + + + + + + + + + + + + + + + + + + + diff --git a/TestModels/aws-sdks/ddbv2/runtimes/net/Extern/DDBv2Client.cs b/TestModels/aws-sdks/ddbv2/runtimes/net/Extern/DDBv2Client.cs new file mode 100644 index 000000000..6e9b68655 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/net/Extern/DDBv2Client.cs @@ -0,0 +1,31 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +using Amazon; +using Amazon.DynamoDBv2; +using Wrappers_Compile; +using Amazon.Runtime; +using Com.Amazonaws.Dynamodb; + +// This extern is identified in Dafny code +// that refines the AWS SDK DDB Model +namespace software.amazon.cryptography.services.dynamodb.internaldafny +{ + public partial class __default + { + public static + _IResult< + types.IDynamoDBClient, + types._IError + > + DynamoDBClient() + { + var client = new AmazonDynamoDBClient(); + + return Result< + types.IDynamoDBClient, + types._IError + > + .create_Success(new DynamoDBv2Shim(client)); + } + } +} diff --git a/TestModels/aws-sdks/ddbv2/runtimes/net/tests/TestDDBv2.csproj b/TestModels/aws-sdks/ddbv2/runtimes/net/tests/TestDDBv2.csproj new file mode 100644 index 000000000..efe6f8989 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/net/tests/TestDDBv2.csproj @@ -0,0 +1,25 @@ + + + + TestDDBv2 + disable + disable + net6.0 + 10 + Exe + false + + + + + + + + + + + + \ No newline at end of file diff --git a/TestModels/aws-sdks/ddbv2/runtimes/rust/Cargo.toml b/TestModels/aws-sdks/ddbv2/runtimes/rust/Cargo.toml new file mode 100644 index 000000000..d834361e2 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/rust/Cargo.toml @@ -0,0 +1,27 @@ +[package] +name = "aws_sdk_ddb" +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-sdk-dynamodb = "1.45.0" +aws-config = "1.5.4" +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] +aws_sdk_ddb = { path = ".", features = ["wrapped-client"] } + +[dependencies.tokio] +version = "1.26.0" +features = ["full"] + +[lib] +path = "src/implementation_from_dafny.rs" diff --git a/TestModels/aws-sdks/ddbv2/runtimes/rust/src/ddb.rs b/TestModels/aws-sdks/ddbv2/runtimes/rust/src/ddb.rs new file mode 100644 index 000000000..8fd807b65 --- /dev/null +++ b/TestModels/aws-sdks/ddbv2/runtimes/rust/src/ddb.rs @@ -0,0 +1,42 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +#![deny(warnings, unconditional_panic)] +#![deny(nonstandard_style)] +#![deny(clippy::all)] + +use std::sync::LazyLock; + +static DAFNY_TOKIO_RUNTIME: LazyLock = LazyLock::new(|| { + tokio::runtime::Builder::new_multi_thread() + .enable_all() + .build() + .unwrap() +}); + +#[allow(non_snake_case)] +impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny::_default { + pub fn DynamoDBClient() -> ::std::rc::Rc< + crate::r#_Wrappers_Compile::Result< + ::dafny_runtime::Object, + ::std::rc::Rc + > + >{ + let shared_config = match tokio::runtime::Handle::try_current() { + Ok(curr) => tokio::task::block_in_place(|| { + curr.block_on(async { + aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await + }) + }), + Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults( + aws_config::BehaviorVersion::v2024_03_28(), + )), + }; + let inner = aws_sdk_dynamodb::Client::new(&shared_config); + let client = crate::client::Client { inner }; + let dafny_client = ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(client)); + std::rc::Rc::new(crate::r#_Wrappers_Compile::Result::Success { + value: dafny_client, + }) + } +} diff --git a/TestModels/dafny-dependencies/Model/aws.test.smithy b/TestModels/dafny-dependencies/Model/aws.test.smithy new file mode 100644 index 000000000..49b958134 --- /dev/null +++ b/TestModels/dafny-dependencies/Model/aws.test.smithy @@ -0,0 +1,58 @@ +$version: "2.0" + +namespace aws.test + +/// Base vendor params for all aws services. +@mixin +@suppress(["UnreferencedShape"]) +structure BaseAwsVendorParams { + /// The AWS region to sign the request for and to resolve the default + /// endpoint with. + region: String = "us-west-2" + + /// The set of regions to sign a sigv4a request with. + sigv4aRegionSet: NonEmptyStringList + + /// A static endpoint to send the request to. + uri: String + + /// Whether to resolve a FIPS compliant endpoint or not. + useFips: Boolean = false + + /// Whether to resolve a dualstack endpoint or not. + useDualstack: Boolean = false + + /// Whether to use account ID based routing where applicable. + useAccountIdRouting: Boolean = true +} + +@private +@length(min: 1) +@suppress(["UnreferencedShape"]) +list NonEmptyStringList { + member: String +} + +/// Concrete vendor params to apply to AWS services by default. +@suppress(["UnreferencedShape"]) +structure AwsVendorParams with [BaseAwsVendorParams] {} + +/// Vendor params for S3. +@suppress(["UnreferencedShape"]) +structure S3VendorParams with [BaseAwsVendorParams] { + /// Whether to resolve an accelerate endpoint or not. + useAccelerate: Boolean = false + + /// Whether to use the global endpoint for us-east-1. + useGlobalEndpoint: Boolean = false + + /// Whether to force path-style addressing. + forcePathStyle: Boolean = false + + /// Whether to use the region in the bucket arn to override the set + /// region. + useArnRegion: Boolean = true + + /// Whether to use S3's multi-region access points. + useMultiRegionAccessPoints: Boolean = true +} \ No newline at end of file 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 01f918206..3ddf756bc 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 @@ -26,9 +26,6 @@ class DotnetTestModels extends TestModelTest { DISABLED_TESTS.add("SimpleTypes/SimpleByte"); DISABLED_TESTS.add("SimpleTypes/SimpleFloat"); DISABLED_TESTS.add("SimpleTypes/SimpleShort"); - // V2 Models are not yet supported in Net. - DISABLED_TESTS.add("aws-sdks/ddbv2"); - DISABLED_TESTS.add("aws-sdks/kmsv2"); // S3 is not yet supported DISABLED_TESTS.add("aws-sdks/s3"); } 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 4b4eba6cc..47da98fc4 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 @@ -41,9 +41,6 @@ class JavaTestModels extends TestModelTest { DISABLED_TESTS.add("aws-sdks/kms-lite"); DISABLED_TESTS.add("aws-sdks/sqs"); DISABLED_TESTS.add("aws-sdks/sqs-via-cli"); - // V2 Models are not yet supported in Java. - DISABLED_TESTS.add("aws-sdks/ddbv2"); - DISABLED_TESTS.add("aws-sdks/kmsv2"); // S3 is not yet supported DISABLED_TESTS.add("aws-sdks/s3"); } diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java index 609e4724f..2bc2e1b72 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java @@ -29,9 +29,6 @@ class RustTestModels extends TestModelTest { DISABLED_TESTS.add("aws-sdks/lakeformation"); DISABLED_TESTS.add("aws-sdks/sqs"); DISABLED_TESTS.add("aws-sdks/sqs-via-cli"); - // V2 Models are not yet supported in Rust. - DISABLED_TESTS.add("aws-sdks/ddbv2"); - DISABLED_TESTS.add("aws-sdks/kmsv2"); // S3 is not yet supported DISABLED_TESTS.add("aws-sdks/s3"); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkDotNetNameResolver.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkDotNetNameResolver.java index 2cc9bfd44..f85a88bd7 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkDotNetNameResolver.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkDotNetNameResolver.java @@ -9,15 +9,7 @@ import software.amazon.smithy.aws.traits.ServiceTrait; import software.amazon.smithy.model.Model; import software.amazon.smithy.model.knowledge.OperationIndex; -import software.amazon.smithy.model.shapes.ListShape; -import software.amazon.smithy.model.shapes.MapShape; -import software.amazon.smithy.model.shapes.MemberShape; -import software.amazon.smithy.model.shapes.OperationShape; -import software.amazon.smithy.model.shapes.ServiceShape; -import software.amazon.smithy.model.shapes.Shape; -import software.amazon.smithy.model.shapes.ShapeId; -import software.amazon.smithy.model.shapes.StringShape; -import software.amazon.smithy.model.shapes.StructureShape; +import software.amazon.smithy.model.shapes.*; import software.amazon.smithy.model.traits.EnumTrait; import software.amazon.smithy.model.traits.ErrorTrait; import software.amazon.smithy.model.traits.TraitDefinition; @@ -53,6 +45,17 @@ private boolean isGeneratedInSdk(final ShapeId shapeId) { return ModelUtils.isInServiceNamespace(shapeId, getServiceShape()); } + @Override + protected String baseTypeForEnum(final EnumShape enumShape) { + if (isGeneratedInSdk(enumShape.getId())) { + return "%s.%s".formatted( + namespaceForService(), + classForEnum(enumShape.getId()) + ); + } + return super.baseTypeForEnum(enumShape); + } + @Override protected String baseTypeForString(final StringShape stringShape) { if ( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeAwsV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeAwsV2.java index 2fd559028..8cb024a9e 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeAwsV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeAwsV2.java @@ -230,6 +230,7 @@ MethodSpec generateConvert(ShapeId shapeId) { case MAP -> modeledMap(shape.asMapShape().get()); case STRUCTURE -> modeledStructure(shape.asStructureShape().get()); case UNION -> modeledUnion(shape.asUnionShape().get()); + case ENUM -> generateConvertEnum(shapeId); default -> throw new UnsupportedOperationException( "ShapeId %s is of Type %s, which is not yet supported for ToNative".formatted( shapeId, 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 64f53a3d7..c742522c3 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 @@ -356,6 +356,7 @@ public TypeName typeForShape(final ShapeId shapeId) { case RESOURCE -> classNameForResource(shape.asResourceShape().get()); // Unions are identical to Structures (in this context). case UNION -> classForNotErrorNotUnitShape(shape.asUnionShape().get()); + case ENUM -> typeForString(shape.asStringShape().get()); default -> throw new UnsupportedOperationException( "Unsupported shape " + shapeId );