From 697b110eec8582fbac79f8912f8e57c2637d3d68 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Mon, 11 Nov 2024 09:56:33 -0500 Subject: [PATCH] chore: re-polymorph to gain OpaqueWithText (#970) * chore: re-polymorph to gain OpaqueWithText --- .../AwsCryptographyMaterialProvidersTypes.dfy | 4 +- .../Model/AwsCryptographyKeyStoreTypes.dfy | 4 +- .../test/TestGetKeys.dfy | 2 +- .../amazon/cryptography/keystore/ToDafny.java | 11 ++ .../cryptography/keystore/ToNative.java | 16 ++ .../keystore/model/OpaqueWithTextError.java | 180 ++++++++++++++++++ .../materialproviders/ToDafny.java | 11 ++ .../materialproviders/ToNative.java | 16 ++ .../model/OpaqueWithTextError.java | 180 ++++++++++++++++++ .../OpaqueWithTextError.cs | 17 ++ .../TypeConversion.cs | 2 + .../OpaqueWithTextError.cs | 17 ++ .../AwsCryptographyKeyStore/TypeConversion.cs | 2 + .../aws_cryptography_keystore/deserialize.py | 2 + .../aws_cryptography_keystore/errors.py | 63 ++++++ .../deserialize.py | 2 + .../errors.py | 63 ++++++ .../Model/AwsCryptographyPrimitivesTypes.dfy | 4 +- .../cryptography/primitives/ToDafny.java | 11 ++ .../cryptography/primitives/ToNative.java | 16 ++ .../primitives/model/OpaqueWithTextError.java | 180 ++++++++++++++++++ .../net/Generated/OpaqueWithTextError.cs | 17 ++ .../runtimes/net/Generated/TypeConversion.cs | 2 + .../deserialize.py | 2 + .../aws_cryptography_primitives/errors.py | 63 ++++++ .../Model/ComAmazonawsDynamodbTypes.dfy | 4 +- .../dynamodb/internaldafny/ToDafny.java | 10 +- .../dynamodb/internaldafny/ToNative.java | 23 +++ .../runtimes/net/Generated/TypeConversion.cs | 4 +- .../com_amazonaws_dynamodb/shim.py | 13 +- .../Model/ComAmazonawsKmsTypes.dfy | 4 +- .../services/kms/internaldafny/ToDafny.java | 10 +- .../services/kms/internaldafny/ToNative.java | 23 +++ .../runtimes/net/Generated/TypeConversion.cs | 4 +- .../smithygenerated/com_amazonaws_kms/shim.py | 13 +- ComAmazonawsKms/test/TestComAmazonawsKms.dfy | 4 +- ...hyMaterialProvidersTestVectorKeysTypes.dfy | 4 +- .../ToDafny.java | 11 ++ .../ToNative.java | 16 ++ .../model/OpaqueWithTextError.java | 180 ++++++++++++++++++ .../KeyVectors/OpaqueWithTextError.cs | 17 ++ .../Generated/KeyVectors/TypeConversion.cs | 2 + .../TypeConversion.cs | 2 + .../deserialize.py | 2 + .../errors.py | 63 ++++++ smithy-dafny | 2 +- 46 files changed, 1276 insertions(+), 22 deletions(-) create mode 100644 AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/OpaqueWithTextError.java create mode 100644 AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/OpaqueWithTextError.java create mode 100644 AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/OpaqueWithTextError.cs create mode 100644 AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/OpaqueWithTextError.cs create mode 100644 AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/model/OpaqueWithTextError.java create mode 100644 AwsCryptographyPrimitives/runtimes/net/Generated/OpaqueWithTextError.cs create mode 100644 TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/model/OpaqueWithTextError.java create mode 100644 TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/OpaqueWithTextError.cs diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy index 0790e276f..a32d3987f 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy @@ -1713,7 +1713,9 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty | CollectionOfErrors(list: seq, nameonly message: string) // The Opaque error, used for native, extern, wrapped or unknown errors | Opaque(obj: object) - type OpaqueError = e: Error | e.Opaque? witness * + // A better Opaque, with a visible string representation. + | OpaqueWithText(obj: object, objMessage : string) + type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness * // This dummy subset type is included to make sure Dafny // always generates a _ExternBase___default.java class. type DummySubsetType = x: int | IsDummySubsetType(x) witness 1 diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy index b16e75d07..a37104579 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy @@ -283,7 +283,9 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw | CollectionOfErrors(list: seq, nameonly message: string) // The Opaque error, used for native, extern, wrapped or unknown errors | Opaque(obj: object) - type OpaqueError = e: Error | e.Opaque? witness * + // A better Opaque, with a visible string representation. + | OpaqueWithText(obj: object, objMessage : string) + type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness * // This dummy subset type is included to make sure Dafny // always generates a _ExternBase___default.java class. type DummySubsetType = x: int | IsDummySubsetType(x) witness 1 diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy index 23cda9e28..7efc428c4 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy @@ -182,7 +182,7 @@ module TestGetKeys { Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey)); expect badResult.Failure?; expect badResult.error.ComAmazonawsKms?; - expect badResult.error.ComAmazonawsKms.Opaque?; + expect badResult.error.ComAmazonawsKms.OpaqueWithText?; // it's an opaque error, so I can't test its contents } diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToDafny.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToDafny.java index 9a949c149..0788d384f 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToDafny.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToDafny.java @@ -41,6 +41,7 @@ import software.amazon.cryptography.keystore.model.CollectionOfErrors; import software.amazon.cryptography.keystore.model.KeyStoreException; import software.amazon.cryptography.keystore.model.OpaqueError; +import software.amazon.cryptography.keystore.model.OpaqueWithTextError; import software.amazon.cryptography.services.dynamodb.internaldafny.types.IDynamoDBClient; import software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient; @@ -53,6 +54,9 @@ public static Error Error(RuntimeException nativeValue) { if (nativeValue instanceof OpaqueError) { return ToDafny.Error((OpaqueError) nativeValue); } + if (nativeValue instanceof OpaqueWithTextError) { + return ToDafny.Error((OpaqueWithTextError) nativeValue); + } if (nativeValue instanceof CollectionOfErrors) { return ToDafny.Error((CollectionOfErrors) nativeValue); } @@ -63,6 +67,13 @@ public static Error Error(OpaqueError nativeValue) { return Error.create_Opaque(nativeValue.obj()); } + public static Error Error(OpaqueWithTextError nativeValue) { + return Error.create_OpaqueWithText( + nativeValue.obj(), + dafny.DafnySequence.asString(nativeValue.objMessage()) + ); + } + public static Error Error(CollectionOfErrors nativeValue) { DafnySequence list = software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence( diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToNative.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToNative.java index e2ac0de8f..2171f5406 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToNative.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToNative.java @@ -16,6 +16,7 @@ import software.amazon.cryptography.keystore.internaldafny.types.Error_CollectionOfErrors; import software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException; import software.amazon.cryptography.keystore.internaldafny.types.Error_Opaque; +import software.amazon.cryptography.keystore.internaldafny.types.Error_OpaqueWithText; import software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient; import software.amazon.cryptography.keystore.model.BeaconKeyMaterials; import software.amazon.cryptography.keystore.model.BranchKeyMaterials; @@ -37,6 +38,7 @@ import software.amazon.cryptography.keystore.model.KeyStoreException; import software.amazon.cryptography.keystore.model.MRDiscovery; import software.amazon.cryptography.keystore.model.OpaqueError; +import software.amazon.cryptography.keystore.model.OpaqueWithTextError; import software.amazon.cryptography.keystore.model.VersionKeyInput; import software.amazon.cryptography.keystore.model.VersionKeyOutput; @@ -48,6 +50,17 @@ public static OpaqueError Error(Error_Opaque dafnyValue) { return nativeBuilder.build(); } + public static OpaqueWithTextError Error(Error_OpaqueWithText dafnyValue) { + OpaqueWithTextError.Builder nativeBuilder = OpaqueWithTextError.builder(); + nativeBuilder.obj(dafnyValue.dtor_obj()); + nativeBuilder.objMessage( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_objMessage() + ) + ); + return nativeBuilder.build(); + } + public static CollectionOfErrors Error(Error_CollectionOfErrors dafnyValue) { CollectionOfErrors.Builder nativeBuilder = CollectionOfErrors.builder(); nativeBuilder.list( @@ -81,6 +94,9 @@ public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_Opaque()) { return ToNative.Error((Error_Opaque) dafnyValue); } + if (dafnyValue.is_OpaqueWithText()) { + return ToNative.Error((Error_OpaqueWithText) dafnyValue); + } if (dafnyValue.is_CollectionOfErrors()) { return ToNative.Error((Error_CollectionOfErrors) dafnyValue); } diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/OpaqueWithTextError.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/OpaqueWithTextError.java new file mode 100644 index 000000000..3c4bd3aa2 --- /dev/null +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/model/OpaqueWithTextError.java @@ -0,0 +1,180 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.keystore.model; + +public class OpaqueWithTextError extends RuntimeException { + + /** + * The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + private final Object obj; + + /** + * The text equivalent of obj. + */ + private final String objMessage; + + protected OpaqueWithTextError(BuilderImpl builder) { + super(messageFromBuilder(builder), builder.cause()); + this.obj = builder.obj(); + this.objMessage = builder.objMessage(); + } + + private static String messageFromBuilder(Builder builder) { + if (builder.message() != null) { + return builder.message(); + } + if (builder.cause() != null) { + return builder.cause().getMessage(); + } + return null; + } + + /** + * See {@link Throwable#getMessage()}. + */ + public String message() { + return this.getMessage(); + } + + /** + * See {@link Throwable#getCause()}. + */ + public Throwable cause() { + return this.getCause(); + } + + /** + * @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + public Object obj() { + return this.obj; + } + + /** + * @return The text equivalent of obj. + */ + public String objMessage() { + return this.objMessage; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param message The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method. + */ + Builder message(String message); + + /** + * @return The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method. + */ + String message(); + + /** + * @param cause The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.) + */ + Builder cause(Throwable cause); + + /** + * @return The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.) + */ + Throwable cause(); + + /** + * @param obj The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + Builder obj(Object obj); + + /** + * @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + Object obj(); + + /** + * @param objMessage The text equivalent of obj. + */ + Builder objMessage(String objMessage); + + /** + * @return The text equivalent of obj. + */ + String objMessage(); + + OpaqueWithTextError build(); + } + + static class BuilderImpl implements Builder { + + protected String message; + + protected Throwable cause; + + protected Object obj; + + protected String objMessage; + + protected BuilderImpl() {} + + protected BuilderImpl(OpaqueWithTextError model) { + this.cause = model.getCause(); + this.message = model.getMessage(); + this.obj = model.obj(); + this.objMessage = model.objMessage(); + } + + public Builder message(String message) { + this.message = message; + return this; + } + + public String message() { + return this.message; + } + + public Builder cause(Throwable cause) { + this.cause = cause; + return this; + } + + public Throwable cause() { + return this.cause; + } + + public Builder obj(Object obj) { + this.obj = obj; + return this; + } + + public Object obj() { + return this.obj; + } + + public Builder objMessage(String objMessage) { + this.objMessage = objMessage; + return this; + } + + public String objMessage() { + return this.objMessage; + } + + public OpaqueWithTextError build() { + if ( + this.obj != null && this.cause == null && this.obj instanceof Throwable + ) { + this.cause = (Throwable) this.obj; + } else if (this.obj == null && this.cause != null) { + this.obj = this.cause; + } + return new OpaqueWithTextError(this); + } + } +} diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToDafny.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToDafny.java index d2efbf511..469094c39 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToDafny.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToDafny.java @@ -126,6 +126,7 @@ import software.amazon.cryptography.materialproviders.model.InvalidEncryptionMaterials; import software.amazon.cryptography.materialproviders.model.InvalidEncryptionMaterialsTransition; import software.amazon.cryptography.materialproviders.model.OpaqueError; +import software.amazon.cryptography.materialproviders.model.OpaqueWithTextError; import software.amazon.cryptography.primitives.internaldafny.types.DigestAlgorithm; import software.amazon.cryptography.primitives.internaldafny.types.ECDHCurveSpec; import software.amazon.cryptography.primitives.internaldafny.types.ECDSASignatureAlgorithm; @@ -170,6 +171,9 @@ public static Error Error(RuntimeException nativeValue) { if (nativeValue instanceof OpaqueError) { return ToDafny.Error((OpaqueError) nativeValue); } + if (nativeValue instanceof OpaqueWithTextError) { + return ToDafny.Error((OpaqueWithTextError) nativeValue); + } if (nativeValue instanceof CollectionOfErrors) { return ToDafny.Error((CollectionOfErrors) nativeValue); } @@ -180,6 +184,13 @@ public static Error Error(OpaqueError nativeValue) { return Error.create_Opaque(nativeValue.obj()); } + public static Error Error(OpaqueWithTextError nativeValue) { + return Error.create_OpaqueWithText( + nativeValue.obj(), + dafny.DafnySequence.asString(nativeValue.objMessage()) + ); + } + public static Error Error(CollectionOfErrors nativeValue) { DafnySequence list = software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence( diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToNative.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToNative.java index 9bd2cbf7c..50092ec55 100644 --- a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToNative.java +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/ToNative.java @@ -27,6 +27,7 @@ import software.amazon.cryptography.materialproviders.internaldafny.types.Error_InvalidEncryptionMaterials; import software.amazon.cryptography.materialproviders.internaldafny.types.Error_InvalidEncryptionMaterialsTransition; import software.amazon.cryptography.materialproviders.internaldafny.types.Error_Opaque; +import software.amazon.cryptography.materialproviders.internaldafny.types.Error_OpaqueWithText; import software.amazon.cryptography.materialproviders.internaldafny.types.IAwsCryptographicMaterialProvidersClient; import software.amazon.cryptography.materialproviders.model.AesWrappingAlg; import software.amazon.cryptography.materialproviders.model.AlgorithmSuiteId; @@ -107,6 +108,7 @@ import software.amazon.cryptography.materialproviders.model.OnEncryptInput; import software.amazon.cryptography.materialproviders.model.OnEncryptOutput; import software.amazon.cryptography.materialproviders.model.OpaqueError; +import software.amazon.cryptography.materialproviders.model.OpaqueWithTextError; import software.amazon.cryptography.materialproviders.model.PaddingScheme; import software.amazon.cryptography.materialproviders.model.PublicKeyDiscoveryInput; import software.amazon.cryptography.materialproviders.model.PutCacheEntryInput; @@ -131,6 +133,17 @@ public static OpaqueError Error(Error_Opaque dafnyValue) { return nativeBuilder.build(); } + public static OpaqueWithTextError Error(Error_OpaqueWithText dafnyValue) { + OpaqueWithTextError.Builder nativeBuilder = OpaqueWithTextError.builder(); + nativeBuilder.obj(dafnyValue.dtor_obj()); + nativeBuilder.objMessage( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_objMessage() + ) + ); + return nativeBuilder.build(); + } + public static CollectionOfErrors Error(Error_CollectionOfErrors dafnyValue) { CollectionOfErrors.Builder nativeBuilder = CollectionOfErrors.builder(); nativeBuilder.list( @@ -315,6 +328,9 @@ public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_Opaque()) { return ToNative.Error((Error_Opaque) dafnyValue); } + if (dafnyValue.is_OpaqueWithText()) { + return ToNative.Error((Error_OpaqueWithText) dafnyValue); + } if (dafnyValue.is_CollectionOfErrors()) { return ToNative.Error((Error_CollectionOfErrors) dafnyValue); } diff --git a/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/OpaqueWithTextError.java b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/OpaqueWithTextError.java new file mode 100644 index 000000000..53ba43a7b --- /dev/null +++ b/AwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviders/model/OpaqueWithTextError.java @@ -0,0 +1,180 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.materialproviders.model; + +public class OpaqueWithTextError extends RuntimeException { + + /** + * The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + private final Object obj; + + /** + * The text equivalent of obj. + */ + private final String objMessage; + + protected OpaqueWithTextError(BuilderImpl builder) { + super(messageFromBuilder(builder), builder.cause()); + this.obj = builder.obj(); + this.objMessage = builder.objMessage(); + } + + private static String messageFromBuilder(Builder builder) { + if (builder.message() != null) { + return builder.message(); + } + if (builder.cause() != null) { + return builder.cause().getMessage(); + } + return null; + } + + /** + * See {@link Throwable#getMessage()}. + */ + public String message() { + return this.getMessage(); + } + + /** + * See {@link Throwable#getCause()}. + */ + public Throwable cause() { + return this.getCause(); + } + + /** + * @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + public Object obj() { + return this.obj; + } + + /** + * @return The text equivalent of obj. + */ + public String objMessage() { + return this.objMessage; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param message The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method. + */ + Builder message(String message); + + /** + * @return The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method. + */ + String message(); + + /** + * @param cause The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.) + */ + Builder cause(Throwable cause); + + /** + * @return The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.) + */ + Throwable cause(); + + /** + * @param obj The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + Builder obj(Object obj); + + /** + * @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + Object obj(); + + /** + * @param objMessage The text equivalent of obj. + */ + Builder objMessage(String objMessage); + + /** + * @return The text equivalent of obj. + */ + String objMessage(); + + OpaqueWithTextError build(); + } + + static class BuilderImpl implements Builder { + + protected String message; + + protected Throwable cause; + + protected Object obj; + + protected String objMessage; + + protected BuilderImpl() {} + + protected BuilderImpl(OpaqueWithTextError model) { + this.cause = model.getCause(); + this.message = model.getMessage(); + this.obj = model.obj(); + this.objMessage = model.objMessage(); + } + + public Builder message(String message) { + this.message = message; + return this; + } + + public String message() { + return this.message; + } + + public Builder cause(Throwable cause) { + this.cause = cause; + return this; + } + + public Throwable cause() { + return this.cause; + } + + public Builder obj(Object obj) { + this.obj = obj; + return this; + } + + public Object obj() { + return this.obj; + } + + public Builder objMessage(String objMessage) { + this.objMessage = objMessage; + return this; + } + + public String objMessage() { + return this.objMessage; + } + + public OpaqueWithTextError build() { + if ( + this.obj != null && this.cause == null && this.obj instanceof Throwable + ) { + this.cause = (Throwable) this.obj; + } else if (this.obj == null && this.cause != null) { + this.obj = this.cause; + } + return new OpaqueWithTextError(this); + } + } +} diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/OpaqueWithTextError.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/OpaqueWithTextError.cs new file mode 100644 index 000000000..55fff5741 --- /dev/null +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/OpaqueWithTextError.cs @@ -0,0 +1,17 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +using System; +using AWS.Cryptography.MaterialProviders; +namespace AWS.Cryptography.MaterialProviders +{ + public class OpaqueWithTextError : Exception + { + public readonly object obj; + public readonly string objMessage; + public OpaqueWithTextError(Exception ex) : base("OpaqueError:", ex) { this.obj = ex; this.objMessage = obj.ToString(); } + public OpaqueWithTextError() : base("Unknown Unexpected Error") { } + public OpaqueWithTextError(object obj, string objMessage) : base(obj is Exception ? "OpaqueWithTextError:" : "Opaque obj is not an Exception.", obj as Exception) { this.obj = obj; this.objMessage = objMessage; } + } + +} diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs index 56aef9ec6..315ad15e7 100644 --- a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographicMaterialProviders/TypeConversion.cs @@ -3935,6 +3935,8 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph new string(dafnyVal.dtor_message.Elements)); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_Opaque dafnyVal: return new OpaqueError(dafnyVal._obj); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_OpaqueWithText dafnyVal: + return new OpaqueWithTextError(dafnyVal._obj, dafnyVal._obj.ToString()); default: // The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?) return new OpaqueError(); diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/OpaqueWithTextError.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/OpaqueWithTextError.cs new file mode 100644 index 000000000..30923009f --- /dev/null +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/OpaqueWithTextError.cs @@ -0,0 +1,17 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +using System; +using AWS.Cryptography.KeyStore; +namespace AWS.Cryptography.KeyStore +{ + public class OpaqueWithTextError : Exception + { + public readonly object obj; + public readonly string objMessage; + public OpaqueWithTextError(Exception ex) : base("OpaqueError:", ex) { this.obj = ex; this.objMessage = obj.ToString(); } + public OpaqueWithTextError() : base("Unknown Unexpected Error") { } + public OpaqueWithTextError(object obj, string objMessage) : base(obj is Exception ? "OpaqueWithTextError:" : "Opaque obj is not an Exception.", obj as Exception) { this.obj = obj; this.objMessage = objMessage; } + } + +} diff --git a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs index 832e525e5..9c9b351d5 100644 --- a/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs +++ b/AwsCryptographicMaterialProviders/runtimes/net/Generated/AwsCryptographyKeyStore/TypeConversion.cs @@ -750,6 +750,8 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph new string(dafnyVal.dtor_message.Elements)); case software.amazon.cryptography.keystore.internaldafny.types.Error_Opaque dafnyVal: return new OpaqueError(dafnyVal._obj); + case software.amazon.cryptography.keystore.internaldafny.types.Error_OpaqueWithText dafnyVal: + return new OpaqueWithTextError(dafnyVal._obj, dafnyVal._obj.ToString()); default: // The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?) return new OpaqueError(); diff --git a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/deserialize.py b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/deserialize.py index 213c9a6d9..874cead29 100644 --- a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/deserialize.py +++ b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/deserialize.py @@ -103,6 +103,8 @@ def _deserialize_get_beacon_key(input: DafnyResponse, config: Config): def _deserialize_error(error: Error) -> ServiceError: if error.is_Opaque: return OpaqueError(obj=error.obj) + elif error.is_OpaqueWithText: + return OpaqueErrorWithText(obj=error.obj, obj_message=error.objMessage) elif error.is_CollectionOfErrors: return CollectionOfErrors( message=_dafny.string_of(error.message), diff --git a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/errors.py b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/errors.py index 134fbbba1..1826a7ef9 100644 --- a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/errors.py +++ b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_keystore/errors.py @@ -198,6 +198,64 @@ def __eq__(self, other: Any) -> bool: return all(getattr(self, a) == getattr(other, a) for a in attributes) +class OpaqueWithTextError(ApiError[Literal["OpaqueWithTextError"]]): + code: Literal["OpaqueWithTextError"] = "OpaqueWithTextError" + obj: Any # As an OpaqueWithTextError, type of obj is unknown + obj_message: str # obj_message is a message representing the details of obj + + def __init__(self, *, obj, obj_message): + super().__init__("") + self.obj = obj + self.obj_message = obj_message + + def as_dict(self) -> Dict[str, Any]: + """Converts the OpaqueWithTextError to a dictionary. + + The dictionary uses the modeled shape names rather than the + parameter names as keys to be mostly compatible with boto3. + """ + return { + "message": self.message, + "code": self.code, + "obj": self.obj, + "obj_message": self.obj_message, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "OpaqueWithTextError": + """Creates a OpaqueWithTextError from a dictionary. + + The dictionary is expected to use the modeled shape names rather + than the parameter names as keys to be mostly compatible with + boto3. + """ + kwargs: Dict[str, Any] = { + "message": d["message"], + "obj": d["obj"], + "obj_message": d["obj_message"], + } + + return OpaqueWithTextError(**kwargs) + + def __repr__(self) -> str: + result = "OpaqueWithTextError(" + result += f"message={self.message}," + if self.message is not None: + result += f"message={repr(self.message)}" + result += f"obj={self.obj}" + result += f"obj_message={self.obj_message}" + result += ")" + return result + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, OpaqueWithTextError): + return False + if not (self.obj == other.obj): + return False + attributes: list[str] = ["message", "message"] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + def _smithy_error_to_dafny_error(e: ServiceError): """Converts the provided native Smithy-modeled error into the corresponding Dafny error.""" @@ -232,6 +290,11 @@ def _smithy_error_to_dafny_error(e: ServiceError): obj=e.obj ) + if isinstance(e, OpaqueWithTextError): + return aws_cryptographic_material_providers.internaldafny.generated.AwsCryptographyKeyStoreTypes.Error_OpaqueWithText( + obj=e.obj, objMessage=e.obj_message + ) + else: return aws_cryptographic_material_providers.internaldafny.generated.AwsCryptographyKeyStoreTypes.Error_Opaque( obj=e diff --git a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/deserialize.py b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/deserialize.py index d3cbc6185..eca1565bf 100644 --- a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/deserialize.py +++ b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/deserialize.py @@ -320,6 +320,8 @@ def _deserialize_validate_commitment_policy_on_decrypt( def _deserialize_error(error: Error) -> ServiceError: if error.is_Opaque: return OpaqueError(obj=error.obj) + elif error.is_OpaqueWithText: + return OpaqueErrorWithText(obj=error.obj, obj_message=error.objMessage) elif error.is_CollectionOfErrors: return CollectionOfErrors( message=_dafny.string_of(error.message), diff --git a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/errors.py b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/errors.py index 2b6ca2e95..77c63d0b9 100644 --- a/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/errors.py +++ b/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_material_providers/smithygenerated/aws_cryptography_materialproviders/errors.py @@ -697,6 +697,64 @@ def __eq__(self, other: Any) -> bool: return all(getattr(self, a) == getattr(other, a) for a in attributes) +class OpaqueWithTextError(ApiError[Literal["OpaqueWithTextError"]]): + code: Literal["OpaqueWithTextError"] = "OpaqueWithTextError" + obj: Any # As an OpaqueWithTextError, type of obj is unknown + obj_message: str # obj_message is a message representing the details of obj + + def __init__(self, *, obj, obj_message): + super().__init__("") + self.obj = obj + self.obj_message = obj_message + + def as_dict(self) -> Dict[str, Any]: + """Converts the OpaqueWithTextError to a dictionary. + + The dictionary uses the modeled shape names rather than the + parameter names as keys to be mostly compatible with boto3. + """ + return { + "message": self.message, + "code": self.code, + "obj": self.obj, + "obj_message": self.obj_message, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "OpaqueWithTextError": + """Creates a OpaqueWithTextError from a dictionary. + + The dictionary is expected to use the modeled shape names rather + than the parameter names as keys to be mostly compatible with + boto3. + """ + kwargs: Dict[str, Any] = { + "message": d["message"], + "obj": d["obj"], + "obj_message": d["obj_message"], + } + + return OpaqueWithTextError(**kwargs) + + def __repr__(self) -> str: + result = "OpaqueWithTextError(" + result += f"message={self.message}," + if self.message is not None: + result += f"message={repr(self.message)}" + result += f"obj={self.obj}" + result += f"obj_message={self.obj_message}" + result += ")" + return result + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, OpaqueWithTextError): + return False + if not (self.obj == other.obj): + return False + attributes: list[str] = ["message", "message"] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + def _smithy_error_to_dafny_error(e: ServiceError): """Converts the provided native Smithy-modeled error into the corresponding Dafny error.""" @@ -813,6 +871,11 @@ def _smithy_error_to_dafny_error(e: ServiceError): obj=e.obj ) + if isinstance(e, OpaqueWithTextError): + return aws_cryptographic_material_providers.internaldafny.generated.AwsCryptographyMaterialProvidersTypes.Error_OpaqueWithText( + obj=e.obj, objMessage=e.obj_message + ) + else: return aws_cryptographic_material_providers.internaldafny.generated.AwsCryptographyMaterialProvidersTypes.Error_Opaque( obj=e diff --git a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy index 485871afc..7714244df 100644 --- a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy +++ b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy @@ -690,7 +690,9 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny.types" } | CollectionOfErrors(list: seq, nameonly message: string) // The Opaque error, used for native, extern, wrapped or unknown errors | Opaque(obj: object) - type OpaqueError = e: Error | e.Opaque? witness * + // A better Opaque, with a visible string representation. + | OpaqueWithText(obj: object, objMessage : string) + type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness * // This dummy subset type is included to make sure Dafny // always generates a _ExternBase___default.java class. type DummySubsetType = x: int | IsDummySubsetType(x) witness 1 diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/ToDafny.java b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/ToDafny.java index 3ba9bace3..06ef1d008 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/ToDafny.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/ToDafny.java @@ -67,6 +67,7 @@ import software.amazon.cryptography.primitives.model.AwsCryptographicPrimitivesError; import software.amazon.cryptography.primitives.model.CollectionOfErrors; import software.amazon.cryptography.primitives.model.OpaqueError; +import software.amazon.cryptography.primitives.model.OpaqueWithTextError; public class ToDafny { @@ -77,6 +78,9 @@ public static Error Error(RuntimeException nativeValue) { if (nativeValue instanceof OpaqueError) { return ToDafny.Error((OpaqueError) nativeValue); } + if (nativeValue instanceof OpaqueWithTextError) { + return ToDafny.Error((OpaqueWithTextError) nativeValue); + } if (nativeValue instanceof CollectionOfErrors) { return ToDafny.Error((CollectionOfErrors) nativeValue); } @@ -87,6 +91,13 @@ public static Error Error(OpaqueError nativeValue) { return Error.create_Opaque(nativeValue.obj()); } + public static Error Error(OpaqueWithTextError nativeValue) { + return Error.create_OpaqueWithText( + nativeValue.obj(), + dafny.DafnySequence.asString(nativeValue.objMessage()) + ); + } + public static Error Error(CollectionOfErrors nativeValue) { DafnySequence list = software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence( diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/ToNative.java b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/ToNative.java index 94bd292df..f2bec6291 100644 --- a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/ToNative.java +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/ToNative.java @@ -15,6 +15,7 @@ import software.amazon.cryptography.primitives.internaldafny.types.Error_AwsCryptographicPrimitivesError; import software.amazon.cryptography.primitives.internaldafny.types.Error_CollectionOfErrors; import software.amazon.cryptography.primitives.internaldafny.types.Error_Opaque; +import software.amazon.cryptography.primitives.internaldafny.types.Error_OpaqueWithText; import software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient; import software.amazon.cryptography.primitives.model.AESDecryptInput; import software.amazon.cryptography.primitives.model.AESEncryptInput; @@ -56,6 +57,7 @@ import software.amazon.cryptography.primitives.model.HkdfInput; import software.amazon.cryptography.primitives.model.KdfCtrInput; import software.amazon.cryptography.primitives.model.OpaqueError; +import software.amazon.cryptography.primitives.model.OpaqueWithTextError; import software.amazon.cryptography.primitives.model.ParsePublicKeyInput; import software.amazon.cryptography.primitives.model.ParsePublicKeyOutput; import software.amazon.cryptography.primitives.model.RSADecryptInput; @@ -74,6 +76,17 @@ public static OpaqueError Error(Error_Opaque dafnyValue) { return nativeBuilder.build(); } + public static OpaqueWithTextError Error(Error_OpaqueWithText dafnyValue) { + OpaqueWithTextError.Builder nativeBuilder = OpaqueWithTextError.builder(); + nativeBuilder.obj(dafnyValue.dtor_obj()); + nativeBuilder.objMessage( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_objMessage() + ) + ); + return nativeBuilder.build(); + } + public static CollectionOfErrors Error(Error_CollectionOfErrors dafnyValue) { CollectionOfErrors.Builder nativeBuilder = CollectionOfErrors.builder(); nativeBuilder.list( @@ -110,6 +123,9 @@ public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_Opaque()) { return ToNative.Error((Error_Opaque) dafnyValue); } + if (dafnyValue.is_OpaqueWithText()) { + return ToNative.Error((Error_OpaqueWithText) dafnyValue); + } if (dafnyValue.is_CollectionOfErrors()) { return ToNative.Error((Error_CollectionOfErrors) dafnyValue); } diff --git a/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/model/OpaqueWithTextError.java b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/model/OpaqueWithTextError.java new file mode 100644 index 000000000..60d0de43f --- /dev/null +++ b/AwsCryptographyPrimitives/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/primitives/model/OpaqueWithTextError.java @@ -0,0 +1,180 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.primitives.model; + +public class OpaqueWithTextError extends RuntimeException { + + /** + * The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + private final Object obj; + + /** + * The text equivalent of obj. + */ + private final String objMessage; + + protected OpaqueWithTextError(BuilderImpl builder) { + super(messageFromBuilder(builder), builder.cause()); + this.obj = builder.obj(); + this.objMessage = builder.objMessage(); + } + + private static String messageFromBuilder(Builder builder) { + if (builder.message() != null) { + return builder.message(); + } + if (builder.cause() != null) { + return builder.cause().getMessage(); + } + return null; + } + + /** + * See {@link Throwable#getMessage()}. + */ + public String message() { + return this.getMessage(); + } + + /** + * See {@link Throwable#getCause()}. + */ + public Throwable cause() { + return this.getCause(); + } + + /** + * @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + public Object obj() { + return this.obj; + } + + /** + * @return The text equivalent of obj. + */ + public String objMessage() { + return this.objMessage; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param message The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method. + */ + Builder message(String message); + + /** + * @return The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method. + */ + String message(); + + /** + * @param cause The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.) + */ + Builder cause(Throwable cause); + + /** + * @return The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.) + */ + Throwable cause(); + + /** + * @param obj The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + Builder obj(Object obj); + + /** + * @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + Object obj(); + + /** + * @param objMessage The text equivalent of obj. + */ + Builder objMessage(String objMessage); + + /** + * @return The text equivalent of obj. + */ + String objMessage(); + + OpaqueWithTextError build(); + } + + static class BuilderImpl implements Builder { + + protected String message; + + protected Throwable cause; + + protected Object obj; + + protected String objMessage; + + protected BuilderImpl() {} + + protected BuilderImpl(OpaqueWithTextError model) { + this.cause = model.getCause(); + this.message = model.getMessage(); + this.obj = model.obj(); + this.objMessage = model.objMessage(); + } + + public Builder message(String message) { + this.message = message; + return this; + } + + public String message() { + return this.message; + } + + public Builder cause(Throwable cause) { + this.cause = cause; + return this; + } + + public Throwable cause() { + return this.cause; + } + + public Builder obj(Object obj) { + this.obj = obj; + return this; + } + + public Object obj() { + return this.obj; + } + + public Builder objMessage(String objMessage) { + this.objMessage = objMessage; + return this; + } + + public String objMessage() { + return this.objMessage; + } + + public OpaqueWithTextError build() { + if ( + this.obj != null && this.cause == null && this.obj instanceof Throwable + ) { + this.cause = (Throwable) this.obj; + } else if (this.obj == null && this.cause != null) { + this.obj = this.cause; + } + return new OpaqueWithTextError(this); + } + } +} diff --git a/AwsCryptographyPrimitives/runtimes/net/Generated/OpaqueWithTextError.cs b/AwsCryptographyPrimitives/runtimes/net/Generated/OpaqueWithTextError.cs new file mode 100644 index 000000000..8451beb57 --- /dev/null +++ b/AwsCryptographyPrimitives/runtimes/net/Generated/OpaqueWithTextError.cs @@ -0,0 +1,17 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +using System; +using AWS.Cryptography.Primitives; +namespace AWS.Cryptography.Primitives +{ + public class OpaqueWithTextError : Exception + { + public readonly object obj; + public readonly string objMessage; + public OpaqueWithTextError(Exception ex) : base("OpaqueError:", ex) { this.obj = ex; this.objMessage = obj.ToString(); } + public OpaqueWithTextError() : base("Unknown Unexpected Error") { } + public OpaqueWithTextError(object obj, string objMessage) : base(obj is Exception ? "OpaqueWithTextError:" : "Opaque obj is not an Exception.", obj as Exception) { this.obj = obj; this.objMessage = objMessage; } + } + +} diff --git a/AwsCryptographyPrimitives/runtimes/net/Generated/TypeConversion.cs b/AwsCryptographyPrimitives/runtimes/net/Generated/TypeConversion.cs index 93391f904..83071c6b6 100644 --- a/AwsCryptographyPrimitives/runtimes/net/Generated/TypeConversion.cs +++ b/AwsCryptographyPrimitives/runtimes/net/Generated/TypeConversion.cs @@ -1608,6 +1608,8 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph new string(dafnyVal.dtor_message.Elements)); case software.amazon.cryptography.primitives.internaldafny.types.Error_Opaque dafnyVal: return new OpaqueError(dafnyVal._obj); + case software.amazon.cryptography.primitives.internaldafny.types.Error_OpaqueWithText dafnyVal: + return new OpaqueWithTextError(dafnyVal._obj, dafnyVal._obj.ToString()); default: // The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?) return new OpaqueError(); diff --git a/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/smithygenerated/aws_cryptography_primitives/deserialize.py b/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/smithygenerated/aws_cryptography_primitives/deserialize.py index 2556ced3a..743c02a04 100644 --- a/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/smithygenerated/aws_cryptography_primitives/deserialize.py +++ b/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/smithygenerated/aws_cryptography_primitives/deserialize.py @@ -252,6 +252,8 @@ def _deserialize_parse_public_key(input: DafnyResponse, config: Config): def _deserialize_error(error: Error) -> ServiceError: if error.is_Opaque: return OpaqueError(obj=error.obj) + elif error.is_OpaqueWithText: + return OpaqueErrorWithText(obj=error.obj, obj_message=error.objMessage) elif error.is_CollectionOfErrors: return CollectionOfErrors( message=_dafny.string_of(error.message), diff --git a/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/smithygenerated/aws_cryptography_primitives/errors.py b/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/smithygenerated/aws_cryptography_primitives/errors.py index 59b8ea560..b9a1d39ec 100644 --- a/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/smithygenerated/aws_cryptography_primitives/errors.py +++ b/AwsCryptographyPrimitives/runtimes/python/src/aws_cryptography_primitives/smithygenerated/aws_cryptography_primitives/errors.py @@ -188,6 +188,64 @@ def __eq__(self, other: Any) -> bool: return all(getattr(self, a) == getattr(other, a) for a in attributes) +class OpaqueWithTextError(ApiError[Literal["OpaqueWithTextError"]]): + code: Literal["OpaqueWithTextError"] = "OpaqueWithTextError" + obj: Any # As an OpaqueWithTextError, type of obj is unknown + obj_message: str # obj_message is a message representing the details of obj + + def __init__(self, *, obj, obj_message): + super().__init__("") + self.obj = obj + self.obj_message = obj_message + + def as_dict(self) -> Dict[str, Any]: + """Converts the OpaqueWithTextError to a dictionary. + + The dictionary uses the modeled shape names rather than the + parameter names as keys to be mostly compatible with boto3. + """ + return { + "message": self.message, + "code": self.code, + "obj": self.obj, + "obj_message": self.obj_message, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "OpaqueWithTextError": + """Creates a OpaqueWithTextError from a dictionary. + + The dictionary is expected to use the modeled shape names rather + than the parameter names as keys to be mostly compatible with + boto3. + """ + kwargs: Dict[str, Any] = { + "message": d["message"], + "obj": d["obj"], + "obj_message": d["obj_message"], + } + + return OpaqueWithTextError(**kwargs) + + def __repr__(self) -> str: + result = "OpaqueWithTextError(" + result += f"message={self.message}," + if self.message is not None: + result += f"message={repr(self.message)}" + result += f"obj={self.obj}" + result += f"obj_message={self.obj_message}" + result += ")" + return result + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, OpaqueWithTextError): + return False + if not (self.obj == other.obj): + return False + attributes: list[str] = ["message", "message"] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + def _smithy_error_to_dafny_error(e: ServiceError): """Converts the provided native Smithy-modeled error into the corresponding Dafny error.""" @@ -212,6 +270,11 @@ def _smithy_error_to_dafny_error(e: ServiceError): obj=e.obj ) + if isinstance(e, OpaqueWithTextError): + return aws_cryptography_primitives.internaldafny.generated.AwsCryptographyPrimitivesTypes.Error_OpaqueWithText( + obj=e.obj, objMessage=e.obj_message + ) + else: return aws_cryptography_primitives.internaldafny.generated.AwsCryptographyPrimitivesTypes.Error_Opaque( obj=e diff --git a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy index 8c808cfd6..8dd9372b2 100644 --- a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy +++ b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy @@ -2904,7 +2904,9 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty // The Opaque error, used for native, extern, wrapped or unknown errors | Opaque(obj: object) - type OpaqueError = e: Error | e.Opaque? witness * + // A better Opaque, with a visible string representation. + | OpaqueWithText(obj: object, objMessage : string) + type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness * // This dummy subset type is included to make sure Dafny // always generates a _ExternBase___default.java class. type DummySubsetType = x: int | IsDummySubsetType(x) witness 1 diff --git a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java index f6e1352aa..abc8e618c 100644 --- a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java +++ b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToDafny.java @@ -13425,7 +13425,10 @@ public static Error Error(DynamoDbException nativeValue) { // An un-modeled Service Error is different from a Java Heap Exhaustion error. // In the future, Smithy-Dafny MAY allow for this distinction. // Which would allow Dafny developers to treat the two differently. - return Error.create_Opaque(nativeValue); + return Error.create_OpaqueWithText( + nativeValue, + dafny.DafnySequence.asString(nativeValue.getMessage()) + ); } public static Error Error(Exception nativeValue) { @@ -13434,7 +13437,10 @@ public static Error Error(Exception nativeValue) { // An un-modeled Service Error is different from a Java Heap Exhaustion error. // In the future, Smithy-Dafny MAY allow for this distinction. // Which would allow Dafny developers to treat the two differently. - return Error.create_Opaque(nativeValue); + return Error.create_OpaqueWithText( + nativeValue, + dafny.DafnySequence.asString(nativeValue.getMessage()) + ); } public static IDynamoDBClient DynamoDB_20120810(DynamoDbClient nativeValue) { diff --git a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java index 7feacebc6..7820211dc 100644 --- a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java +++ b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java @@ -375,6 +375,7 @@ import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ItemCollectionSizeLimitExceededException; import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_LimitExceededException; import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_Opaque; +import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_OpaqueWithText; import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_PointInTimeRecoveryUnavailableException; import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_PolicyNotFoundException; import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ProvisionedThroughputExceededException; @@ -8621,6 +8622,25 @@ public static RuntimeException Error(Error_Opaque dafnyValue) { ); } + public static RuntimeException Error(Error_OpaqueWithText dafnyValue) { + // While the first two cases are logically identical, + // there is a semantic distinction. + // An un-modeled Service Error is different from a Java Heap Exhaustion error. + // In the future, Smithy-Dafny MAY allow for this distinction. + // Which would allow Dafny developers to treat the two differently. + if (dafnyValue.dtor_obj() instanceof DynamoDbException) { + return (DynamoDbException) dafnyValue.dtor_obj(); + } else if (dafnyValue.dtor_obj() instanceof Exception) { + return (RuntimeException) dafnyValue.dtor_obj(); + } + return new IllegalStateException( + String.format( + "Unknown error thrown while calling Amazon DynamoDB. %s", + dafnyValue + ) + ); + } + public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_BackupInUseException()) { return ToNative.Error((Error_BackupInUseException) dafnyValue); @@ -8733,6 +8753,9 @@ public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_Opaque()) { return ToNative.Error((Error_Opaque) dafnyValue); } + if (dafnyValue.is_OpaqueWithText()) { + return ToNative.Error((Error_OpaqueWithText) dafnyValue); + } // TODO This should indicate a codegen bug; every error Should have been taken care of. return new IllegalStateException( String.format( diff --git a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs index 3ba9829a4..b133fcd49 100644 --- a/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs +++ b/ComAmazonawsDynamodb/runtimes/net/Generated/TypeConversion.cs @@ -13135,7 +13135,7 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S28_TransactionConflictException(dafnyVal); case software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_TransactionInProgressException dafnyVal: return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S30_TransactionInProgressException(dafnyVal); - case software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_Opaque dafnyVal: + case software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_OpaqueWithText dafnyVal: return new SystemException(dafnyVal._obj.ToString()); default: // The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?) @@ -13244,7 +13244,7 @@ public static software.amazon.cryptography.services.dynamodb.internaldafny.types return TypeConversion.ToDafny_N3_com__N9_amazonaws__N8_dynamodb__S30_TransactionInProgressException(e); default: - return new software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_Opaque(value); + return new software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_OpaqueWithText(value, Dafny.Sequence.FromString(value.ToString())); } } diff --git a/ComAmazonawsDynamodb/runtimes/python/src/aws_cryptography_internal_dynamodb/smithygenerated/com_amazonaws_dynamodb/shim.py b/ComAmazonawsDynamodb/runtimes/python/src/aws_cryptography_internal_dynamodb/smithygenerated/com_amazonaws_dynamodb/shim.py index defd47c9f..9f62a2697 100644 --- a/ComAmazonawsDynamodb/runtimes/python/src/aws_cryptography_internal_dynamodb/smithygenerated/com_amazonaws_dynamodb/shim.py +++ b/ComAmazonawsDynamodb/runtimes/python/src/aws_cryptography_internal_dynamodb/smithygenerated/com_amazonaws_dynamodb/shim.py @@ -2,6 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 # Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +import _dafny from aws_cryptography_internal_dynamodb.internaldafny.generated.ComAmazonawsDynamodbTypes import ( BatchExecuteStatementInput_BatchExecuteStatementInput as DafnyBatchExecuteStatementInput, BatchExecuteStatementOutput_BatchExecuteStatementOutput as DafnyBatchExecuteStatementOutput, @@ -296,8 +297,16 @@ def _sdk_error_to_dafny_error(e: ClientError): e.response ) - return aws_cryptography_internal_dynamodb.internaldafny.generated.ComAmazonawsDynamodbTypes.Error_Opaque( - obj=e + return aws_cryptography_internal_dynamodb.internaldafny.generated.ComAmazonawsDynamodbTypes.Error_OpaqueWithText( + obj=e, + objMessage=_dafny.Seq( + "".join( + [ + chr(int.from_bytes(pair, "big")) + for pair in zip(*[iter(repr(e).encode("utf-16-be"))] * 2) + ] + ) + ), ) diff --git a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy index 54f8f6bde..ff5520a28 100644 --- a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy +++ b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy @@ -1977,7 +1977,9 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types" // The Opaque error, used for native, extern, wrapped or unknown errors | Opaque(obj: object) - type OpaqueError = e: Error | e.Opaque? witness * + // A better Opaque, with a visible string representation. + | OpaqueWithText(obj: object, objMessage : string) + type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness * // This dummy subset type is included to make sure Dafny // always generates a _ExternBase___default.java class. type DummySubsetType = x: int | IsDummySubsetType(x) witness 1 diff --git a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java index d8767cd0f..3a7a97f73 100644 --- a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java +++ b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToDafny.java @@ -5727,7 +5727,10 @@ public static Error Error(KmsException nativeValue) { // An un-modeled Service Error is different from a Java Heap Exhaustion error. // In the future, Smithy-Dafny MAY allow for this distinction. // Which would allow Dafny developers to treat the two differently. - return Error.create_Opaque(nativeValue); + return Error.create_OpaqueWithText( + nativeValue, + dafny.DafnySequence.asString(nativeValue.getMessage()) + ); } public static Error Error(Exception nativeValue) { @@ -5736,7 +5739,10 @@ public static Error Error(Exception nativeValue) { // An un-modeled Service Error is different from a Java Heap Exhaustion error. // In the future, Smithy-Dafny MAY allow for this distinction. // Which would allow Dafny developers to treat the two differently. - return Error.create_Opaque(nativeValue); + return Error.create_OpaqueWithText( + nativeValue, + dafny.DafnySequence.asString(nativeValue.getMessage()) + ); } public static IKMSClient TrentService(KmsClient nativeValue) { diff --git a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java index d4e598f82..314a2de75 100644 --- a/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java +++ b/ComAmazonawsKms/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/kms/internaldafny/ToNative.java @@ -226,6 +226,7 @@ import software.amazon.cryptography.services.kms.internaldafny.types.Error_MalformedPolicyDocumentException; import software.amazon.cryptography.services.kms.internaldafny.types.Error_NotFoundException; import software.amazon.cryptography.services.kms.internaldafny.types.Error_Opaque; +import software.amazon.cryptography.services.kms.internaldafny.types.Error_OpaqueWithText; import software.amazon.cryptography.services.kms.internaldafny.types.Error_TagException; import software.amazon.cryptography.services.kms.internaldafny.types.Error_UnsupportedOperationException; import software.amazon.cryptography.services.kms.internaldafny.types.Error_XksKeyAlreadyInUseException; @@ -4566,6 +4567,25 @@ public static RuntimeException Error(Error_Opaque dafnyValue) { ); } + public static RuntimeException Error(Error_OpaqueWithText dafnyValue) { + // While the first two cases are logically identical, + // there is a semantic distinction. + // An un-modeled Service Error is different from a Java Heap Exhaustion error. + // In the future, Smithy-Dafny MAY allow for this distinction. + // Which would allow Dafny developers to treat the two differently. + if (dafnyValue.dtor_obj() instanceof KmsException) { + return (KmsException) dafnyValue.dtor_obj(); + } else if (dafnyValue.dtor_obj() instanceof Exception) { + return (RuntimeException) dafnyValue.dtor_obj(); + } + return new IllegalStateException( + String.format( + "Unknown error thrown while calling AWS Key Management Service. %s", + dafnyValue + ) + ); + } + public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_AlreadyExistsException()) { return ToNative.Error((Error_AlreadyExistsException) dafnyValue); @@ -4746,6 +4766,9 @@ public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_Opaque()) { return ToNative.Error((Error_Opaque) dafnyValue); } + if (dafnyValue.is_OpaqueWithText()) { + return ToNative.Error((Error_OpaqueWithText) dafnyValue); + } // TODO This should indicate a codegen bug; every error Should have been taken care of. return new IllegalStateException( String.format( diff --git a/ComAmazonawsKms/runtimes/net/Generated/TypeConversion.cs b/ComAmazonawsKms/runtimes/net/Generated/TypeConversion.cs index 46aff0c76..0752a1dbb 100644 --- a/ComAmazonawsKms/runtimes/net/Generated/TypeConversion.cs +++ b/ComAmazonawsKms/runtimes/net/Generated/TypeConversion.cs @@ -6681,7 +6681,7 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph return FromDafny_N3_com__N9_amazonaws__N3_kms__S55_XksProxyVpcEndpointServiceInvalidConfigurationException(dafnyVal); case software.amazon.cryptography.services.kms.internaldafny.types.Error_XksProxyVpcEndpointServiceNotFoundException dafnyVal: return FromDafny_N3_com__N9_amazonaws__N3_kms__S43_XksProxyVpcEndpointServiceNotFoundException(dafnyVal); - case software.amazon.cryptography.services.kms.internaldafny.types.Error_Opaque dafnyVal: + case software.amazon.cryptography.services.kms.internaldafny.types.Error_OpaqueWithText dafnyVal: return new SystemException(dafnyVal._obj.ToString()); default: // The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?) @@ -6837,7 +6837,7 @@ public static software.amazon.cryptography.services.kms.internaldafny.types._IEr return TypeConversion.ToDafny_N3_com__N9_amazonaws__N3_kms__S43_XksProxyVpcEndpointServiceNotFoundException(e); default: - return new software.amazon.cryptography.services.kms.internaldafny.types.Error_Opaque(value); + return new software.amazon.cryptography.services.kms.internaldafny.types.Error_OpaqueWithText(value, Dafny.Sequence.FromString(value.ToString())); } } diff --git a/ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/smithygenerated/com_amazonaws_kms/shim.py b/ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/smithygenerated/com_amazonaws_kms/shim.py index 8bf832b48..79a83136c 100644 --- a/ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/smithygenerated/com_amazonaws_kms/shim.py +++ b/ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/smithygenerated/com_amazonaws_kms/shim.py @@ -2,6 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 # Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +import _dafny from aws_cryptography_internal_kms.internaldafny.generated.ComAmazonawsKmsTypes import ( CancelKeyDeletionRequest_CancelKeyDeletionRequest as DafnyCancelKeyDeletionRequest, CancelKeyDeletionResponse_CancelKeyDeletionResponse as DafnyCancelKeyDeletionResponse, @@ -354,8 +355,16 @@ def _sdk_error_to_dafny_error(e: ClientError): e.response ) - return aws_cryptography_internal_kms.internaldafny.generated.ComAmazonawsKmsTypes.Error_Opaque( - obj=e + return aws_cryptography_internal_kms.internaldafny.generated.ComAmazonawsKmsTypes.Error_OpaqueWithText( + obj=e, + objMessage=_dafny.Seq( + "".join( + [ + chr(int.from_bytes(pair, "big")) + for pair in zip(*[iter(repr(e).encode("utf-16-be"))] * 2) + ] + ) + ), ) diff --git a/ComAmazonawsKms/test/TestComAmazonawsKms.dfy b/ComAmazonawsKms/test/TestComAmazonawsKms.dfy index 3cbd71aa3..e07ec4765 100644 --- a/ComAmazonawsKms/test/TestComAmazonawsKms.dfy +++ b/ComAmazonawsKms/test/TestComAmazonawsKms.dfy @@ -118,9 +118,9 @@ module TestComAmazonawsKms { var ret := client.GenerateDataKeyWithoutPlaintext(failingInput); expect ret.Failure?; var err: Kms.Types.Error := ret.error; - expect err.Opaque?; + expect err.OpaqueWithText?; match err { - case Opaque(obj) => expect true; + case OpaqueWithText(obj, objMessage) => expect true; case _ => expect false, "Failing KMS Key MUST cause an OpaqueError that can later be unwrapped to a proper but generic KMS Exception."; } } diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy index 26615f621..201cf7476 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy @@ -261,7 +261,9 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in | CollectionOfErrors(list: seq, nameonly message: string) // The Opaque error, used for native, extern, wrapped or unknown errors | Opaque(obj: object) - type OpaqueError = e: Error | e.Opaque? witness * + // A better Opaque, with a visible string representation. + | OpaqueWithText(obj: object, objMessage : string) + type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness * // This dummy subset type is included to make sure Dafny // always generates a _ExternBase___default.java class. type DummySubsetType = x: int | IsDummySubsetType(x) witness 1 diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/ToDafny.java b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/ToDafny.java index 429283097..3b3651b23 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/ToDafny.java +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/ToDafny.java @@ -40,6 +40,7 @@ import software.amazon.cryptography.materialproviderstestvectorkeys.model.CollectionOfErrors; import software.amazon.cryptography.materialproviderstestvectorkeys.model.KeyVectorException; import software.amazon.cryptography.materialproviderstestvectorkeys.model.OpaqueError; +import software.amazon.cryptography.materialproviderstestvectorkeys.model.OpaqueWithTextError; import software.amazon.cryptography.services.kms.internaldafny.types.EncryptionAlgorithmSpec; public class ToDafny { @@ -51,6 +52,9 @@ public static Error Error(RuntimeException nativeValue) { if (nativeValue instanceof OpaqueError) { return ToDafny.Error((OpaqueError) nativeValue); } + if (nativeValue instanceof OpaqueWithTextError) { + return ToDafny.Error((OpaqueWithTextError) nativeValue); + } if (nativeValue instanceof CollectionOfErrors) { return ToDafny.Error((CollectionOfErrors) nativeValue); } @@ -61,6 +65,13 @@ public static Error Error(OpaqueError nativeValue) { return Error.create_Opaque(nativeValue.obj()); } + public static Error Error(OpaqueWithTextError nativeValue) { + return Error.create_OpaqueWithText( + nativeValue.obj(), + dafny.DafnySequence.asString(nativeValue.objMessage()) + ); + } + public static Error Error(CollectionOfErrors nativeValue) { DafnySequence list = software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence( diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/ToNative.java b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/ToNative.java index 60a342464..f322900ea 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/ToNative.java +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/ToNative.java @@ -11,6 +11,7 @@ import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.Error_CollectionOfErrors; import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.Error_KeyVectorException; import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.Error_Opaque; +import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.Error_OpaqueWithText; import software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.IKeyVectorsClient; import software.amazon.cryptography.materialproviderstestvectorkeys.model.CmmOperation; import software.amazon.cryptography.materialproviderstestvectorkeys.model.CollectionOfErrors; @@ -27,6 +28,7 @@ import software.amazon.cryptography.materialproviderstestvectorkeys.model.KmsRsaKeyring; import software.amazon.cryptography.materialproviderstestvectorkeys.model.MultiKeyring; import software.amazon.cryptography.materialproviderstestvectorkeys.model.OpaqueError; +import software.amazon.cryptography.materialproviderstestvectorkeys.model.OpaqueWithTextError; import software.amazon.cryptography.materialproviderstestvectorkeys.model.RawAES; import software.amazon.cryptography.materialproviderstestvectorkeys.model.RawEcdh; import software.amazon.cryptography.materialproviderstestvectorkeys.model.RawRSA; @@ -45,6 +47,17 @@ public static OpaqueError Error(Error_Opaque dafnyValue) { return nativeBuilder.build(); } + public static OpaqueWithTextError Error(Error_OpaqueWithText dafnyValue) { + OpaqueWithTextError.Builder nativeBuilder = OpaqueWithTextError.builder(); + nativeBuilder.obj(dafnyValue.dtor_obj()); + nativeBuilder.objMessage( + software.amazon.smithy.dafny.conversion.ToNative.Simple.String( + dafnyValue.dtor_objMessage() + ) + ); + return nativeBuilder.build(); + } + public static CollectionOfErrors Error(Error_CollectionOfErrors dafnyValue) { CollectionOfErrors.Builder nativeBuilder = CollectionOfErrors.builder(); nativeBuilder.list( @@ -78,6 +91,9 @@ public static RuntimeException Error(Error dafnyValue) { if (dafnyValue.is_Opaque()) { return ToNative.Error((Error_Opaque) dafnyValue); } + if (dafnyValue.is_OpaqueWithText()) { + return ToNative.Error((Error_OpaqueWithText) dafnyValue); + } if (dafnyValue.is_CollectionOfErrors()) { return ToNative.Error((Error_CollectionOfErrors) dafnyValue); } diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/model/OpaqueWithTextError.java b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/model/OpaqueWithTextError.java new file mode 100644 index 000000000..5997b10b0 --- /dev/null +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/materialproviderstestvectorkeys/model/OpaqueWithTextError.java @@ -0,0 +1,180 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +package software.amazon.cryptography.materialproviderstestvectorkeys.model; + +public class OpaqueWithTextError extends RuntimeException { + + /** + * The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + private final Object obj; + + /** + * The text equivalent of obj. + */ + private final String objMessage; + + protected OpaqueWithTextError(BuilderImpl builder) { + super(messageFromBuilder(builder), builder.cause()); + this.obj = builder.obj(); + this.objMessage = builder.objMessage(); + } + + private static String messageFromBuilder(Builder builder) { + if (builder.message() != null) { + return builder.message(); + } + if (builder.cause() != null) { + return builder.cause().getMessage(); + } + return null; + } + + /** + * See {@link Throwable#getMessage()}. + */ + public String message() { + return this.getMessage(); + } + + /** + * See {@link Throwable#getCause()}. + */ + public Throwable cause() { + return this.getCause(); + } + + /** + * @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + public Object obj() { + return this.obj; + } + + /** + * @return The text equivalent of obj. + */ + public String objMessage() { + return this.objMessage; + } + + public Builder toBuilder() { + return new BuilderImpl(this); + } + + public static Builder builder() { + return new BuilderImpl(); + } + + public interface Builder { + /** + * @param message The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method. + */ + Builder message(String message); + + /** + * @return The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method. + */ + String message(); + + /** + * @param cause The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.) + */ + Builder cause(Throwable cause); + + /** + * @return The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.) + */ + Throwable cause(); + + /** + * @param obj The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + Builder obj(Object obj); + + /** + * @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed. + */ + Object obj(); + + /** + * @param objMessage The text equivalent of obj. + */ + Builder objMessage(String objMessage); + + /** + * @return The text equivalent of obj. + */ + String objMessage(); + + OpaqueWithTextError build(); + } + + static class BuilderImpl implements Builder { + + protected String message; + + protected Throwable cause; + + protected Object obj; + + protected String objMessage; + + protected BuilderImpl() {} + + protected BuilderImpl(OpaqueWithTextError model) { + this.cause = model.getCause(); + this.message = model.getMessage(); + this.obj = model.obj(); + this.objMessage = model.objMessage(); + } + + public Builder message(String message) { + this.message = message; + return this; + } + + public String message() { + return this.message; + } + + public Builder cause(Throwable cause) { + this.cause = cause; + return this; + } + + public Throwable cause() { + return this.cause; + } + + public Builder obj(Object obj) { + this.obj = obj; + return this; + } + + public Object obj() { + return this.obj; + } + + public Builder objMessage(String objMessage) { + this.objMessage = objMessage; + return this; + } + + public String objMessage() { + return this.objMessage; + } + + public OpaqueWithTextError build() { + if ( + this.obj != null && this.cause == null && this.obj instanceof Throwable + ) { + this.cause = (Throwable) this.obj; + } else if (this.obj == null && this.cause != null) { + this.obj = this.cause; + } + return new OpaqueWithTextError(this); + } + } +} diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/OpaqueWithTextError.cs b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/OpaqueWithTextError.cs new file mode 100644 index 000000000..be8759d84 --- /dev/null +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/OpaqueWithTextError.cs @@ -0,0 +1,17 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +using System; +using AWS.Cryptography.MaterialProvidersTestVectorKeys; +namespace AWS.Cryptography.MaterialProvidersTestVectorKeys +{ + public class OpaqueWithTextError : Exception + { + public readonly object obj; + public readonly string objMessage; + public OpaqueWithTextError(Exception ex) : base("OpaqueError:", ex) { this.obj = ex; this.objMessage = obj.ToString(); } + public OpaqueWithTextError() : base("Unknown Unexpected Error") { } + public OpaqueWithTextError(object obj, string objMessage) : base(obj is Exception ? "OpaqueWithTextError:" : "Opaque obj is not an Exception.", obj as Exception) { this.obj = obj; this.objMessage = objMessage; } + } + +} diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/TypeConversion.cs b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/TypeConversion.cs index 6e78de744..d37b12d1e 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/TypeConversion.cs +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/KeyVectors/TypeConversion.cs @@ -995,6 +995,8 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph new string(dafnyVal.dtor_message.Elements)); case software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.Error_Opaque dafnyVal: return new OpaqueError(dafnyVal._obj); + case software.amazon.cryptography.materialproviderstestvectorkeys.internaldafny.types.Error_OpaqueWithText dafnyVal: + return new OpaqueWithTextError(dafnyVal._obj, dafnyVal._obj.ToString()); default: // The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?) return new OpaqueError(); diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs index e477a7882..0fa25a68c 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/Generated/TestVectorsAwsCryptographicMaterialProviders/TypeConversion.cs @@ -3898,6 +3898,8 @@ public static System.Exception FromDafny_CommonError(software.amazon.cryptograph new string(dafnyVal.dtor_message.Elements)); case software.amazon.cryptography.materialproviders.internaldafny.types.Error_Opaque dafnyVal: return new OpaqueError(dafnyVal._obj); + case software.amazon.cryptography.materialproviders.internaldafny.types.Error_OpaqueWithText dafnyVal: + return new OpaqueWithTextError(dafnyVal._obj, dafnyVal._obj.ToString()); default: // The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?) return new OpaqueError(); diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/smithygenerated/aws_cryptography_materialproviderstestvectorkeys/deserialize.py b/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/smithygenerated/aws_cryptography_materialproviderstestvectorkeys/deserialize.py index 42b5a9f6d..57535e298 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/smithygenerated/aws_cryptography_materialproviderstestvectorkeys/deserialize.py +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/smithygenerated/aws_cryptography_materialproviderstestvectorkeys/deserialize.py @@ -70,6 +70,8 @@ def _deserialize_serialize_key_description(input: DafnyResponse, config: Config) def _deserialize_error(error: Error) -> ServiceError: if error.is_Opaque: return OpaqueError(obj=error.obj) + elif error.is_OpaqueWithText: + return OpaqueErrorWithText(obj=error.obj, obj_message=error.objMessage) elif error.is_CollectionOfErrors: return CollectionOfErrors( message=_dafny.string_of(error.message), diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/smithygenerated/aws_cryptography_materialproviderstestvectorkeys/errors.py b/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/smithygenerated/aws_cryptography_materialproviderstestvectorkeys/errors.py index d06847e71..1dcd143df 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/smithygenerated/aws_cryptography_materialproviderstestvectorkeys/errors.py +++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptography_materialproviders_test_vectors/smithygenerated/aws_cryptography_materialproviderstestvectorkeys/errors.py @@ -184,6 +184,64 @@ def __eq__(self, other: Any) -> bool: return all(getattr(self, a) == getattr(other, a) for a in attributes) +class OpaqueWithTextError(ApiError[Literal["OpaqueWithTextError"]]): + code: Literal["OpaqueWithTextError"] = "OpaqueWithTextError" + obj: Any # As an OpaqueWithTextError, type of obj is unknown + obj_message: str # obj_message is a message representing the details of obj + + def __init__(self, *, obj, obj_message): + super().__init__("") + self.obj = obj + self.obj_message = obj_message + + def as_dict(self) -> Dict[str, Any]: + """Converts the OpaqueWithTextError to a dictionary. + + The dictionary uses the modeled shape names rather than the + parameter names as keys to be mostly compatible with boto3. + """ + return { + "message": self.message, + "code": self.code, + "obj": self.obj, + "obj_message": self.obj_message, + } + + @staticmethod + def from_dict(d: Dict[str, Any]) -> "OpaqueWithTextError": + """Creates a OpaqueWithTextError from a dictionary. + + The dictionary is expected to use the modeled shape names rather + than the parameter names as keys to be mostly compatible with + boto3. + """ + kwargs: Dict[str, Any] = { + "message": d["message"], + "obj": d["obj"], + "obj_message": d["obj_message"], + } + + return OpaqueWithTextError(**kwargs) + + def __repr__(self) -> str: + result = "OpaqueWithTextError(" + result += f"message={self.message}," + if self.message is not None: + result += f"message={repr(self.message)}" + result += f"obj={self.obj}" + result += f"obj_message={self.obj_message}" + result += ")" + return result + + def __eq__(self, other: Any) -> bool: + if not isinstance(other, OpaqueWithTextError): + return False + if not (self.obj == other.obj): + return False + attributes: list[str] = ["message", "message"] + return all(getattr(self, a) == getattr(other, a) for a in attributes) + + def _smithy_error_to_dafny_error(e: ServiceError): """Converts the provided native Smithy-modeled error into the corresponding Dafny error.""" @@ -208,6 +266,11 @@ def _smithy_error_to_dafny_error(e: ServiceError): obj=e.obj ) + if isinstance(e, OpaqueWithTextError): + return aws_cryptography_materialproviders_test_vectors.internaldafny.generated.AwsCryptographyMaterialProvidersTestVectorKeysTypes.Error_OpaqueWithText( + obj=e.obj, objMessage=e.obj_message + ) + else: return aws_cryptography_materialproviders_test_vectors.internaldafny.generated.AwsCryptographyMaterialProvidersTestVectorKeysTypes.Error_Opaque( obj=e diff --git a/smithy-dafny b/smithy-dafny index 465b91697..fe4809863 160000 --- a/smithy-dafny +++ b/smithy-dafny @@ -1 +1 @@ -Subproject commit 465b916975ac71938774a47069cdbcc478f403f4 +Subproject commit fe4809863bafd6ca8641c352bc0258026bcc0524