diff --git a/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy b/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy index 6a0a6cabd..bab435818 100644 --- a/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy +++ b/TestModels/Dependencies/src/SimpleDependenciesImpl.dfy @@ -160,7 +160,7 @@ module SimpleDependenciesImpl refines AbstractSimpleDependenciesOperations { returns (output: Result) { var obj: object := new ExtendableResource.OpaqueMessage(); - var extendableResourceError := SimpleExtendableResourcesTypes.Opaque(obj); + var extendableResourceError := SimpleExtendableResourcesTypes.Opaque(obj, "alt text for the message"); var dependenciesError := Error.SimpleExtendableResources(extendableResourceError); return Failure(dependenciesError); } diff --git a/TestModels/Errors/runtimes/rust/tests/simple_errors_test.rs b/TestModels/Errors/runtimes/rust/tests/simple_errors_test.rs index 74b093040..8bb2b82b6 100644 --- a/TestModels/Errors/runtimes/rust/tests/simple_errors_test.rs +++ b/TestModels/Errors/runtimes/rust/tests/simple_errors_test.rs @@ -30,7 +30,7 @@ mod simple_errors_test { match result { Ok(_x) => assert!(false), Err(e) => match e { - Opaque { obj } => assert!(obj.0.is_some()), + Opaque { obj , ..} => assert!(obj.0.is_some()), _ => assert!(false, "always_native_error did not return Opaque"), }, } diff --git a/TestModels/Errors/src/SimpleErrorsImpl.dfy b/TestModels/Errors/src/SimpleErrorsImpl.dfy index 3f8297139..a0e938a6e 100644 --- a/TestModels/Errors/src/SimpleErrorsImpl.dfy +++ b/TestModels/Errors/src/SimpleErrorsImpl.dfy @@ -54,7 +54,7 @@ module SimpleErrorsImpl refines AbstractSimpleErrorsOperations { // TODO: Rewrite this as an actual extern. var opaqueObject := new SomeOpaqueGeneratedTypeForTesting(); - var res := Error.Opaque( obj := opaqueObject ); + var res := Error.Opaque( obj := opaqueObject, alt_text := "Some Generated Test" ); return Failure(res); } diff --git a/TestModels/Extendable/src/ExtendableResource.dfy b/TestModels/Extendable/src/ExtendableResource.dfy index fe5b62a33..841328e89 100644 --- a/TestModels/Extendable/src/ExtendableResource.dfy +++ b/TestModels/Extendable/src/ExtendableResource.dfy @@ -140,7 +140,7 @@ module ExtendableResource { ensures unchanged(History) { var obj: object := new OpaqueMessage(); - return Failure(Types.Opaque(obj)); + return Failure(Types.Opaque(obj, "lost in translation")); } } } diff --git a/TestModels/Extern/runtimes/net/Extern/ExternOperations.cs b/TestModels/Extern/runtimes/net/Extern/ExternOperations.cs index 561034de1..09016df17 100644 --- a/TestModels/Extern/runtimes/net/Extern/ExternOperations.cs +++ b/TestModels/Extern/runtimes/net/Extern/ExternOperations.cs @@ -27,7 +27,7 @@ public static _IResult<_IExternMustErrorOutput, _IError> ExternMustError(_IConfi var exception = new Exception( TypeConversion .FromDafny_N6_simple__N11_dafnyExtern__S20_ExternMustErrorInput__M5_value(input.dtor_value)); - return Result<_IExternMustErrorOutput, _IError>.create_Failure(Error.create_Opaque(exception)); + return Result<_IExternMustErrorOutput, _IError>.create_Failure(Error.create_Opaque(exception, Dafny.Sequence.FromString(exception.ToString()))); } } } @@ -58,7 +58,7 @@ public static _IResult Build(ISequence in } catch (Exception ex) { - return Result.create_Failure(Error.create_Opaque(ex)); + return Result.create_Failure(Error.create_Opaque(ex, Dafny.Sequence.FromString(ex.ToString()))); } } diff --git a/TestModels/Extern/runtimes/net/Extern/WrappedSimpleExternService.cs b/TestModels/Extern/runtimes/net/Extern/WrappedSimpleExternService.cs index 5c4bb7495..023003cb8 100644 --- a/TestModels/Extern/runtimes/net/Extern/WrappedSimpleExternService.cs +++ b/TestModels/Extern/runtimes/net/Extern/WrappedSimpleExternService.cs @@ -3,11 +3,13 @@ using Wrappers_Compile; using Simple.DafnyExtern; using Simple.DafnyExtern.Wrapped; -using TypeConversion = Simple.DafnyExtern.TypeConversion ; +using TypeConversion = Simple.DafnyExtern.TypeConversion; namespace simple.dafnyextern.internaldafny.wrapped { - public partial class __default { - public static _IResult WrappedSimpleExtern(types._ISimpleExternConfig config) { + public partial class __default + { + public static _IResult WrappedSimpleExtern(types._ISimpleExternConfig config) + { var wrappedConfig = TypeConversion.FromDafny_N6_simple__N11_dafnyExtern__S18_SimpleExternConfig(config); var impl = new SimpleExtern(wrappedConfig); var wrappedClient = new SimpleExternShim(impl); diff --git a/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/ExternConstructor.py b/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/ExternConstructor.py index 836ce5dc7..b56281422 100644 --- a/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/ExternConstructor.py +++ b/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/ExternConstructor.py @@ -21,6 +21,6 @@ def Build(input): try: return Wrappers.Result_Success(ExternConstructorClass(input)) except Exception as e: - return Wrappers.Result_Failure(SimpleDafnyExternTypes.Error_Opaque(e)) + return Wrappers.Result_Failure(SimpleDafnyExternTypes.Error_Opaque(e, repr(e))) -simple_dafnyextern.internaldafny.generated.ExternConstructor.ExternConstructorClass = ExternConstructorClass \ No newline at end of file +simple_dafnyextern.internaldafny.generated.ExternConstructor.ExternConstructorClass = ExternConstructorClass diff --git a/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/SimpleExternImpl.py b/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/SimpleExternImpl.py index a719ad2ed..4ccc037a1 100644 --- a/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/SimpleExternImpl.py +++ b/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern/SimpleExternImpl.py @@ -18,7 +18,7 @@ def GetExtern(config, input): @staticmethod def ExternMustError(config, input): exception = Exception(input) - return Wrappers.Result_Failure(SimpleDafnyExternTypes.Error_Opaque(exception)) + return Wrappers.Result_Failure(SimpleDafnyExternTypes.Error_Opaque(exception, repr(input))) default__.GetExtern = GetExtern -default__.ExternMustError = ExternMustError \ No newline at end of file +default__.ExternMustError = ExternMustError diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs index c5d1f5831..bdc253bdb 100644 --- a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs @@ -8,7 +8,7 @@ pub fn to_opaque_error(value: E) -> ))); ::std::rc::Rc::new( crate::r#language::specific::logic::internaldafny::types::Error::Opaque { - obj: error_obj, + obj: error_obj, alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") }, ) } diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information.rs index 9539a2bdc..cc52d073f 100644 --- a/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information.rs +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/get_runtime_information.rs @@ -9,7 +9,7 @@ pub fn to_dafny_error( { match value { crate::operation::get_runtime_information::GetRuntimeInformationError::Unhandled(unhandled) => - ::std::rc::Rc::new(crate::r#language::specific::logic::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) }) + ::std::rc::Rc::new(crate::r#language::specific::logic::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)), alt_text: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") }) } } diff --git a/TestModels/LanguageSpecificLogic/runtimes/rust/src/deps.rs b/TestModels/LanguageSpecificLogic/runtimes/rust/src/deps.rs index a5d3381b0..5fbbbaa0f 100644 --- a/TestModels/LanguageSpecificLogic/runtimes/rust/src/deps.rs +++ b/TestModels/LanguageSpecificLogic/runtimes/rust/src/deps.rs @@ -1,3 +1,3 @@ // 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. \ No newline at end of file +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. diff --git a/TestModels/Refinement/runtimes/rust/src/conversions/get_refinement.rs b/TestModels/Refinement/runtimes/rust/src/conversions/get_refinement.rs index 6586e95d9..57daa0b2c 100644 --- a/TestModels/Refinement/runtimes/rust/src/conversions/get_refinement.rs +++ b/TestModels/Refinement/runtimes/rust/src/conversions/get_refinement.rs @@ -8,7 +8,7 @@ pub fn to_dafny_error( ) -> ::std::rc::Rc { match value { crate::operation::get_refinement::GetRefinementError::Unhandled(unhandled) => - ::std::rc::Rc::new(crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) }) + ::std::rc::Rc::new(crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)), alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") }) } } diff --git a/TestModels/Refinement/runtimes/rust/src/conversions/only_input.rs b/TestModels/Refinement/runtimes/rust/src/conversions/only_input.rs index 460f0edfa..ac740cc46 100644 --- a/TestModels/Refinement/runtimes/rust/src/conversions/only_input.rs +++ b/TestModels/Refinement/runtimes/rust/src/conversions/only_input.rs @@ -11,7 +11,7 @@ pub fn to_dafny_error( crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()( ::dafny_runtime::object::new(unhandled), - ), + ), alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") }, ), } diff --git a/TestModels/Refinement/runtimes/rust/src/conversions/only_output.rs b/TestModels/Refinement/runtimes/rust/src/conversions/only_output.rs index c9a8d2504..cd83be98e 100644 --- a/TestModels/Refinement/runtimes/rust/src/conversions/only_output.rs +++ b/TestModels/Refinement/runtimes/rust/src/conversions/only_output.rs @@ -11,7 +11,7 @@ pub fn to_dafny_error( crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()( ::dafny_runtime::object::new(unhandled), - ), + ), alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") }, ), } diff --git a/TestModels/Refinement/runtimes/rust/src/conversions/readonly_operation.rs b/TestModels/Refinement/runtimes/rust/src/conversions/readonly_operation.rs index cd6ab4756..aaa52ea91 100644 --- a/TestModels/Refinement/runtimes/rust/src/conversions/readonly_operation.rs +++ b/TestModels/Refinement/runtimes/rust/src/conversions/readonly_operation.rs @@ -8,7 +8,7 @@ pub fn to_dafny_error( ) -> ::std::rc::Rc { match value { crate::operation::readonly_operation::ReadonlyOperationError::Unhandled(unhandled) => - ::std::rc::Rc::new(crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)) }) + ::std::rc::Rc::new(crate::r#simple::refinement::internaldafny::types::Error::Opaque { obj: ::dafny_runtime::upcast_object()(::dafny_runtime::object::new(unhandled)), alt_text : ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("foo") }) } } diff --git a/TestModels/Refinement/runtimes/rust/src/deps.rs b/TestModels/Refinement/runtimes/rust/src/deps.rs index a5d3381b0..5fbbbaa0f 100644 --- a/TestModels/Refinement/runtimes/rust/src/deps.rs +++ b/TestModels/Refinement/runtimes/rust/src/deps.rs @@ -1,3 +1,3 @@ // 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. \ No newline at end of file +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. diff --git a/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy b/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy index cdd49100d..83895afa3 100644 --- a/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy +++ b/TestModels/aws-sdks/ddb-lite/model/ComAmazonawsDynamodbTypes.dfy @@ -1122,7 +1122,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object) + | Opaque(obj: object, alt_text : string) type OpaqueError = e: Error | e.Opaque? witness * } abstract module AbstractComAmazonawsDynamodbService { diff --git a/TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy b/TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy index 9d7ab5578..54a1ee107 100644 --- a/TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy +++ b/TestModels/aws-sdks/kms-lite/model/ComAmazonawsKmsTypes.dfy @@ -439,7 +439,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types" // The Opaque error, used for native, extern, wrapped or unknown errors - | Opaque(obj: object) + | Opaque(obj: object, alt_text : string) type OpaqueError = e: Error | e.Opaque? witness * } abstract module AbstractComAmazonawsKmsService { diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java index 4cdcb1a42..727983456 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java @@ -1579,7 +1579,7 @@ public TokenTree generateModeledErrorDataType() { Token.of( "// The Opaque error, used for native, extern, wrapped or unknown errors" ), - Token.of("| Opaque(obj: object)"), + Token.of("| Opaque(obj: object, alt_text : string)"), // Helper error for use with `extern` Token.of("type OpaqueError = e: Error | e.Opaque? witness *") ) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkTypeConversionCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkTypeConversionCodegen.java index 9a50e9b4f..471df37b0 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkTypeConversionCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkTypeConversionCodegen.java @@ -186,7 +186,7 @@ protected TokenTree errorToDafnyBody( final TokenTree unknownErrorCase = Token.of( """ default: - return new %s(value); + return new %s(value, Dafny.Sequence.FromString(value.ToString())); """.formatted(dafnyUnknownErrorType) ); final TokenTree cases = TokenTree diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java index 05494838e..1bb79bc90 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java @@ -1718,20 +1718,20 @@ protected TokenTree errorToDafnyBody( "case %1$s exception:".formatted( DotNetNameResolver.baseClassForUnknownError() ), - "return new %1$s(exception);".formatted( + "return new %1$s(exception, Dafny.Sequence.FromString(exception.ToString()));".formatted( DotNetNameResolver.dafnyUnknownErrorTypeForServiceShape( serviceShape ) ), "case %1$s exception:".formatted(C_SHARP_SYSTEM_EXCEPTION), - "return new %1$s(exception);".formatted( + "return new %1$s(exception, Dafny.Sequence.FromString(exception.ToString()));".formatted( DotNetNameResolver.dafnyUnknownErrorTypeForServiceShape( serviceShape ) ), "default:", "// The switch MUST be complete for System.Exception, so `value` MUST NOT be an System.Exception. (How did you get here?)", - "return new %1$s(value);".formatted( + "return new %1$s(value, Dafny.Sequence.FromString(value.ToString()));".formatted( DotNetNameResolver.dafnyUnknownErrorTypeForServiceShape( serviceShape ) diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedShimCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedShimCodegen.java index 0e724a33f..ac9e65547 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedShimCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedShimCodegen.java @@ -325,7 +325,7 @@ public TokenTree generateErrorTypeShim() { final TokenTree unknownErrorCase = Token.of( """ default: - return new %s(error); + return new %s(error, Dafny.Sequence.FromString(error.ToString())); """.formatted(dafnyUnknownErrorType) ); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java index ccba82942..a25d2e171 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java @@ -57,6 +57,11 @@ public class BuilderMemberSpec { "obj", "The unexpected object encountered. It MIGHT BE an Exception," + " but that is not guaranteed." + ), + new BuilderMemberSpec( + TypeName.get(String.class), + "altText", + "A best effort text representation of obj." ) ); public static final List COLLECTION_ARGS = List.of( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java index 230aa1e15..5a39bc5d5 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java @@ -705,7 +705,7 @@ MethodSpec generateConvertOpaqueServiceError() { "nativeValue" ) .addStatement( - "return $T.create_Opaque(nativeValue)", + "return $T.create_Opaque(nativeValue, dafny.DafnySequence.asString(nativeValue.getMessage()))", subject.dafnyNameResolver.abstractClassForError() ) .build(); @@ -731,7 +731,7 @@ MethodSpec generateConvertOpaqueError() { "Which would allow Dafny developers to treat the two differently." ) .addStatement( - "return $T.create_Opaque(nativeValue)", + "return $T.create_Opaque(nativeValue, dafny.DafnySequence.asString(nativeValue.getMessage()))", subject.dafnyNameResolver.abstractClassForError() ) .build(); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToDafnyLibrary.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToDafnyLibrary.java index cbc0a47cf..4d8e3ccda 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToDafnyLibrary.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToDafnyLibrary.java @@ -177,7 +177,13 @@ MethodSpec runtimeException() { .endControlFlow() ); return method - .addStatement("return $T.create_Opaque($L)", dafnyError, VAR_INPUT) + .addStatement( + "return $T.create_Opaque($L, dafny.DafnySequence.asString(java.util.Objects.nonNull($L.getMessage()) ? $L.getMessage() : \"\"))", + dafnyError, + VAR_INPUT, + VAR_INPUT, + VAR_INPUT + ) .build(); } @@ -191,7 +197,13 @@ MethodSpec opaqueError() { .returns(dafnyError) .addModifiers(PUBLIC_STATIC) .addParameter(opaqueError, VAR_INPUT) - .addStatement("return $T.create_Opaque($L.obj())", dafnyError, VAR_INPUT) + .addStatement( + "return $T.create_Opaque($L.obj(), dafny.DafnySequence.asString(java.util.Objects.nonNull($L.altText()) ? $L.altText() : \"\"))", + dafnyError, + VAR_INPUT, + VAR_INPUT, + VAR_INPUT + ) .build(); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/unmodeled/OpaqueError.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/unmodeled/OpaqueError.java index 0bf762af7..6a3e17963 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/unmodeled/OpaqueError.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/unmodeled/OpaqueError.java @@ -93,6 +93,7 @@ static MethodSpec constructor(BuilderSpecs builderSpecs) { BuilderSpecs.BUILDER_VAR, BuilderSpecs.BUILDER_VAR ) + .addStatement("this.altText = builder.altText()") .addStatement("this.obj = builder.obj()"); return method.build(); } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/customize/AwsSdkShimFileWriter.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/customize/AwsSdkShimFileWriter.java index 26a79c36c..cbf7b01c9 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/customize/AwsSdkShimFileWriter.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/customize/AwsSdkShimFileWriter.java @@ -86,6 +86,20 @@ def __init__(self, _impl, _region): ); } + private static final String DAFNY_STRING_E = + """ + _dafny.Seq( + "".join( + [ + chr(int.from_bytes(pair, "big")) + for pair in zip( + *[iter(repr(e).encode("utf-16-be"))] * 2 + ) + ] + ) + ) + """; + /** * Generate the method body for the `_sdk_error_to_dafny_error` method. This writes out a block to * convert a boto3 ClientError modelled in JSON into a Dafny-modelled error @@ -146,17 +160,19 @@ private void generateAwsSdkErrorToDafnyErrorBlock( hasOpenedIfBlock = true; } + writer.addStdlibImport("_dafny"); if (hasOpenedIfBlock) { // If `hasOpenedIfBlock` is false, then codegen never wrote any errors, // and this function should only cast to Opaque errors writer.write( """ - return $L.Error_Opaque(obj=e) + return $L.Error_Opaque(obj=e, alt__text=$L) """, DafnyNameResolver.getDafnyPythonTypesModuleNameForShape( serviceShape.getId(), codegenContext - ) + ), + DAFNY_STRING_E ); } else { // If `hasOpenedIfBlock` is true, then codegen wrote at least one error, @@ -164,12 +180,13 @@ private void generateAwsSdkErrorToDafnyErrorBlock( writer.write( """ else: - return $L.Error_Opaque(obj=e) + return $L.Error_Opaque(obj=e, alt__text=$L) """, DafnyNameResolver.getDafnyPythonTypesModuleNameForShape( serviceShape.getId(), codegenContext - ) + ), + DAFNY_STRING_E ); } } diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/DafnyPythonLocalServiceProtocolGenerator.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/DafnyPythonLocalServiceProtocolGenerator.java index adb467119..5f3746a42 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/DafnyPythonLocalServiceProtocolGenerator.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/DafnyPythonLocalServiceProtocolGenerator.java @@ -459,7 +459,7 @@ private void generateErrorResponseDeserializerSection( writer.write( """ if error.is_Opaque: - return OpaqueError(obj=error.obj) + return OpaqueError(obj=error.obj, alt_text=error.alt__text) elif error.is_CollectionOfErrors: return CollectionOfErrors( message=_dafny.string_of(error.message), @@ -496,7 +496,7 @@ private void generateErrorResponseDeserializerSection( writer.write( """ else: - return OpaqueError(obj=error)""" + return OpaqueError(obj=error, alt_text=repr(error))""" ); } ); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/customize/ErrorsFileWriter.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/customize/ErrorsFileWriter.java index 46b7439f8..fc7f5912a 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/customize/ErrorsFileWriter.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/customize/ErrorsFileWriter.java @@ -156,10 +156,12 @@ class OpaqueError(ApiError[Literal["OpaqueError"]]): def __init__( self, *, - obj + obj, + alt_text ): super().__init__("") self.obj = obj + self.alt_text = alt_text def as_dict(self) -> Dict[str, Any]: ""\"Converts the OpaqueError to a dictionary. @@ -171,6 +173,7 @@ def as_dict(self) -> Dict[str, Any]: 'message': self.message, 'code': self.code, 'obj': self.obj, + 'alt_text': self.alt_text, } @staticmethod @@ -182,7 +185,8 @@ def from_dict(d: Dict[str, Any]) -> "OpaqueError": ""\" kwargs: Dict[str, Any] = { 'message': d['message'], - 'obj': d['obj'] + 'obj': d['obj'], + 'alt_text': d['alt_text'] } return OpaqueError(**kwargs) @@ -192,7 +196,7 @@ def __repr__(self) -> str: 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={self.alt_text}' result += ")" return result @@ -408,7 +412,7 @@ private void generateSmithyErrorToDafnyErrorBlock( writer.write( """ if isinstance(e, OpaqueError): - return $L.Error_Opaque(obj=e.obj) + return $L.Error_Opaque(obj=e.obj, alt__text=e.alt_text) """, DafnyNameResolver.getDafnyPythonTypesModuleNameForShape( serviceShape.getId(), @@ -420,11 +424,21 @@ private void generateSmithyErrorToDafnyErrorBlock( serviceShape.getId().getNamespace() ) ); + writer.addStdlibImport("_dafny"); // Nothing found, we know nothing about this error. Cast as opaque writer.write( """ else: - return $L.Error_Opaque(obj=e) + return $L.Error_Opaque(obj=e, alt__text=_dafny.Seq( + "".join( + [ + chr(int.from_bytes(pair, "big")) + for pair in zip( + *[iter(repr(e).encode("utf-16-be"))] * 2 + ) + ] + ) + )) """, DafnyNameResolver.getDafnyPythonTypesModuleNameForShape( serviceShape.getId(), diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java index a21889896..93e3f1b12 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyrust/generator/RustAwsSdkShimGenerator.java @@ -667,10 +667,10 @@ pub fn to_dafny_error( match value { $sdkCrate:L::error::SdkError::ServiceError(service_error) => match service_error.err() { $errorCases:L - e => $rustRootModuleName:L::conversions::error::to_opaque_error(e.to_string()), + e => $rustRootModuleName:L::conversions::error::to_opaque_error(format!("{:?}", e)), }, _ => { - $rustRootModuleName:L::conversions::error::to_opaque_error(value.to_string()) + $rustRootModuleName:L::conversions::error::to_opaque_error(format!("{:?}", value)) } } } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/java/src/main/java/$dafnyNamespaceDir;L/__default.java b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/java/src/main/java/$dafnyNamespaceDir;L/__default.java index 735273fd3..99c90cfac 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/java/src/main/java/$dafnyNamespaceDir;L/__default.java +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/java/src/main/java/$dafnyNamespaceDir;L/__default.java @@ -30,7 +30,7 @@ public class __default I$sdkID:LClient shim = new Shim(nativeClient, region.toString()); return CreateSuccessOfClient(shim); } catch (Exception e) { - Error dafny_error = Error.create_Opaque(e); + Error dafny_error = Error.create_Opaque(e, dafny.DafnySequence.asString(e.getMessage())); return CreateFailureOfError(dafny_error); } } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_awssdk.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_awssdk.rs index efd15bc7c..de1366a36 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_awssdk.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_awssdk.rs @@ -4,9 +4,10 @@ pub fn to_dafny( ) -> ::std::rc::Rc { match value { $toDafnyArms:L - $qualifiedRustServiceErrorType:L::Opaque { obj } => + $qualifiedRustServiceErrorType:L::Opaque { obj, alt_text } => ::std::rc::Rc::new(crate::r#$dafnyTypesModuleName:L::Error::Opaque { - obj: ::dafny_runtime::Object(obj.0) + obj: ::dafny_runtime::Object(obj.0), + alt_text: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&alt_text) }), } } @@ -19,9 +20,10 @@ pub fn from_dafny( ) -> $qualifiedRustServiceErrorType:L { match ::std::borrow::Borrow::borrow(&dafny_value) { $fromDafnyArms:L - crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj } => + crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj, alt_text } => $qualifiedRustServiceErrorType:L::Opaque { - obj: obj.clone() + obj: obj.clone(), + alt_text: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&alt_text) }, } -} \ No newline at end of file +} diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_common.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_common.rs index ebdbcb71f..8448b5c06 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_common.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_common.rs @@ -1,19 +1,22 @@ /// Wraps up an arbitrary Rust Error value as a Dafny Error -pub fn to_opaque_error(value: E) -> +pub fn to_opaque_error(value: E) -> ::std::rc::Rc { + let error_str = format!("{:?}", value); + let error_str = ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&error_str); let error_obj: ::dafny_runtime::Object = ::dafny_runtime::Object(Some( ::std::rc::Rc::new(::std::cell::UnsafeCell::new(value)), )); ::std::rc::Rc::new( crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj: error_obj, + alt_text: error_str }, ) } /// Wraps up an arbitrary Rust Error value as a Dafny Result.Failure -pub fn to_opaque_error_result(value: E) -> +pub fn to_opaque_error_result(value: E) -> ::std::rc::Rc< crate::_Wrappers_Compile::Result< T, @@ -24,4 +27,4 @@ pub fn to_opaque_error_result(value: ::std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure { error: to_opaque_error(value), }) -} \ No newline at end of file +} diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_library.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_library.rs index 2f37db65b..84ec6c43f 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_library.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/conversions/error_library.rs @@ -9,7 +9,8 @@ pub fn to_dafny( message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&message), list: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&list, |e| to_dafny(e.clone())) }, - $qualifiedRustServiceErrorType:L::ValidationError(inner) => + $qualifiedRustServiceErrorType:L::ValidationError(inner) => { + let error_str = format!("{:?}", inner); crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj: { let rc = ::std::rc::Rc::new(inner) as ::std::rc::Rc; @@ -18,10 +19,15 @@ pub fn to_dafny( // accepts unsized types (https://github.com/dafny-lang/dafny/pull/5769) unsafe { ::dafny_runtime::Object::from_rc(rc) } }, - }, - $qualifiedRustServiceErrorType:L::Opaque { obj } => + alt_text : { + ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&error_str) + } + } + }, + $qualifiedRustServiceErrorType:L::Opaque { obj, alt_text } => crate::r#$dafnyTypesModuleName:L::Error::Opaque { - obj: ::dafny_runtime::Object(obj.0) + obj: ::dafny_runtime::Object(obj.0), + alt_text: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&alt_text) }, }) } @@ -39,11 +45,12 @@ pub fn from_dafny( message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&message), list: ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(&list, |e| from_dafny(e.clone())) }, - crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj } => + crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj, alt_text } => $qualifiedRustServiceErrorType:L::Opaque { - obj: obj.clone() + obj: obj.clone(), + alt_text: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&alt_text) }, - crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj } => + crate::r#$dafnyTypesModuleName:L::Error::Opaque { obj, alt_text } => { use ::std::any::Any; if ::dafny_runtime::is_object!(obj, $rustErrorModuleName:L::ValidationError) { @@ -56,9 +63,10 @@ pub fn from_dafny( ) } else { $qualifiedRustServiceErrorType:L::Opaque { - obj: obj.clone() + obj: obj.clone(), + alt_text: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&alt_text) } } }, } -} \ No newline at end of file +} diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/operation/builders.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/operation/builders.rs index 90d0e3fc8..22e007c6f 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/operation/builders.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/operation/builders.rs @@ -50,10 +50,11 @@ impl $pascalCaseOperationName:LFluentBuilder { // and smithy-rs seems to not generate a ValidationError case unless there is. // Vanilla smithy-rs uses SdkError::construction_failure, but we aren't using SdkError. .map_err(|mut e| $qualifiedRustServiceErrorType:L::Opaque { - obj: ::dafny_runtime::Object::from_ref(&mut e as &mut dyn ::std::any::Any) + obj: ::dafny_runtime::Object::from_ref(&mut e as &mut dyn ::std::any::Any), + alt_text : format!("{:?}", e) })?; $rustRootModuleName:L::operation::$snakeCaseOperationName:L::$pascalCaseOperationName:L::send(&self.$operationTargetName:L, input).await } $accessors:L -} \ No newline at end of file +} diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error.rs index 931d03303..4b17284b1 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error.rs @@ -8,6 +8,7 @@ pub enum Error { ValidationError(ValidationError), Opaque { obj: ::dafny_runtime::Object, + alt_text : ::std::string::String }, } @@ -17,6 +18,7 @@ impl ::std::fmt::Display for Error { fn fmt(&self, f: &mut ::std::fmt::Formatter) -> ::std::fmt::Result { match self { Self::ValidationError(err) => ::std::fmt::Display::fmt(err, f), + Self::Opaque{obj, alt_text} => ::std::fmt::Debug::fmt(alt_text, f), _ => ::std::fmt::Debug::fmt(self, f), } } diff --git a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error_awssdk.rs b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error_awssdk.rs index ebc4e8f99..82c4319f5 100644 --- a/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error_awssdk.rs +++ b/codegen/smithy-dafny-codegen/src/main/resources/templates/runtimes/rust/types/error_awssdk.rs @@ -3,6 +3,7 @@ pub enum Error { $modeledErrorVariants:L Opaque { obj: ::dafny_runtime::Object, + alt_text : String }, } diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java index 79c281cf8..fb171ef40 100644 --- a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java @@ -107,31 +107,31 @@ public static software.amazon.cryptography.services.kms.internaldafny.types.Simp protected static String GENERATE_CONVERT_OPAQUE_ERROR = """ - public static software.amazon.cryptography.services.kms.internaldafny.types.Error Error( - java.lang.Exception nativeValue - ) { - // While this is logically identical to the other Opaque Error case, - // it is semantically distinct. - // 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 software.amazon.cryptography.services.kms.internaldafny.types.Error.create_Opaque(nativeValue); - } - """; + public static software.amazon.cryptography.services.kms.internaldafny.types.Error Error( + java.lang.Exception nativeValue + ) { + // While this is logically identical to the other Opaque Error case, + // it is semantically distinct. + // 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 software.amazon.cryptography.services.kms.internaldafny.types.Error.create_Opaque(nativeValue, dafny.DafnySequence.asString(nativeValue.getMessage())); + } + """; protected static String GENERATE_CONVERT_OPAQUE_ERROR_WITH_TYPE_DESCRIPTORS = """ - public static software.amazon.cryptography.services.kms.internaldafny.types.Error Error( - java.lang.Exception nativeValue - ) { - // While this is logically identical to the other Opaque Error case, - // it is semantically distinct. - // 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 software.amazon.cryptography.services.kms.internaldafny.types.Error.create_Opaque(nativeValue); - } - """; + public static software.amazon.cryptography.services.kms.internaldafny.types.Error Error( + java.lang.Exception nativeValue + ) { + // While this is logically identical to the other Opaque Error case, + // it is semantically distinct. + // 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 software.amazon.cryptography.services.kms.internaldafny.types.Error.create_Opaque(nativeValue, dafny.DafnySequence.asString(nativeValue.getMessage())); + } + """; protected static final String KMS_A_STRING_OPERATION_JAVA_FILE = """