-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Shubham Chaturvedi
committed
Oct 24, 2024
1 parent
e602cbf
commit 5a5a5cc
Showing
19 changed files
with
551 additions
and
22 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
20 changes: 20 additions & 0 deletions
20
TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.5.0.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) | ||
| { |
20 changes: 20 additions & 0 deletions
20
TestModels/aws-sdks/ddbv2/codegen-patches/dotnet/dafny-4.8.0.patch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) | ||
| { |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<MavenPublication>("maven") { | ||
| groupId = "software.amazon.cryptography" | ||
| artifactId = "ComAmazonawsDynamodb" | ||
| from(components["java"]) | ||
| } | ||
| repositories { mavenLocal() } | ||
| } | ||
|
|
||
| tasks.withType<JavaCompile>() { | ||
| options.encoding = "UTF-8" | ||
| } | ||
|
|
||
| tasks.withType<Wrapper>() { | ||
| gradleVersion = "7.6" | ||
| } | ||
|
|
||
| tasks { | ||
| register("runTests", JavaExec::class.java) { | ||
| mainClass.set("TestsFromDafny") | ||
| classpath = sourceSets["test"].runtimeClasspath | ||
| } | ||
| } |
39 changes: 39 additions & 0 deletions
39
...src/main/java/software/amazon/cryptography/services/dynamodb/internaldafny/__default.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<IDynamoDBClient, Error> 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); | ||
| } | ||
| } | ||
| } |
6 changes: 6 additions & 0 deletions
6
...in/java/software/amazon/cryptography/services/dynamodb/internaldafny/types/__default.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 {} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,34 @@ | ||
| <Project Sdk="Microsoft.NET.Sdk"> | ||
|
|
||
| <PropertyGroup> | ||
| <RootNamespace>DDBv2</RootNamespace> | ||
| <ImplicitUsings>disable</ImplicitUsings> | ||
| <Nullable>disable</Nullable> | ||
| <TargetFrameworks>net6.0</TargetFrameworks> | ||
| <LangVersion>10</LangVersion> | ||
| <EnableDefaultCompileItems>false</EnableDefaultCompileItems> | ||
| </PropertyGroup> | ||
|
|
||
| <ItemGroup> | ||
| <PackageReference Include="DafnyRuntime" Version="4.8.1" /> | ||
| <PackageReference Include="AWSSDK.Core" Version="3.7.400.38" /> | ||
| <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.402.2" /> | ||
| <PackageReference Include="ObjectDumper.NET" Version="3.5.6" /> | ||
| <!-- | ||
| System.Collections.Immutable can be removed once dafny.msbuild is updated with | ||
| https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned | ||
| --> | ||
| <PackageReference Include="System.Collections.Immutable" Version="1.7.0" /> | ||
| <!-- Work around for dafny-lang/dafny/issues/1951; remove once resolved --> | ||
| <PackageReference Include="System.ValueTuple" Version="4.5.0" /> | ||
|
|
||
| <Compile Include="Extern/**/*.cs" /> | ||
| <Compile Include="Generated/**/*.cs" /> | ||
| <Compile Include="ImplementationFromDafny.cs" /> | ||
| </ItemGroup> | ||
|
|
||
| <ItemGroup> | ||
| <ProjectReference Include="../../../../dafny-dependencies/StandardLibrary/runtimes/net/STD.csproj" /> | ||
| </ItemGroup> | ||
|
|
||
| </Project> |
Oops, something went wrong.