chore: Add string to opaque type (#617)

* chore: Add string to opaque type

TestModels/Dependencies/src/SimpleDependenciesImpl.dfy

@@ -160,7 +160,7 @@ module SimpleDependenciesImpl refines AbstractSimpleDependenciesOperations {
  returns (output: Result<SimpleExtendableResourcesTypes.GetExtendableResourceErrorsOutput, Error>)
  {
  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);
  }

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"),
  },
  }

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);
  }

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"));
  }
  }
 }

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<char>.FromString(exception.ToString())));
  }
  }
 }
@@ -58,7 +58,7 @@ public static _IResult<ExternConstructorClass, _IError> Build(ISequence<char> in
  }
  catch (Exception ex)
  {
- return Result<ExternConstructorClass, _IError>.create_Failure(Error.create_Opaque(ex));
+ return Result<ExternConstructorClass, _IError>.create_Failure(Error.create_Opaque(ex, Dafny.Sequence<char>.FromString(ex.ToString())));
  }
  }
 

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<types.ISimpleExternClient, types._IError> WrappedSimpleExtern(types._ISimpleExternConfig config) {
+ public partial class __default
+ {
+ public static _IResult<types.ISimpleExternClient, types._IError> 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);

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
+simple_dafnyextern.internaldafny.generated.ExternConstructor.ExternConstructorClass = ExternConstructorClass

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
+default__.ExternMustError = ExternMustError

TestModels/LanguageSpecificLogic/runtimes/rust/src/conversions/error.rs

@@ -8,7 +8,7 @@ pub fn to_opaque_error<E: std::error::Error + 'static>(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")
  },
  )
 }

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") })
  }
 }
 

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.
+// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.

TestModels/Refinement/runtimes/rust/src/conversions/get_refinement.rs

@@ -8,7 +8,7 @@ pub fn to_dafny_error(
 ) -> ::std::rc::Rc<crate::r#simple::refinement::internaldafny::types::Error> {
  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") })
  }
 }
 

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")
  },
  ),
  }

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")
  },
  ),
  }

TestModels/Refinement/runtimes/rust/src/conversions/readonly_operation.rs

@@ -8,7 +8,7 @@ pub fn to_dafny_error(
 ) -> ::std::rc::Rc<crate::r#simple::refinement::internaldafny::types::Error> {
  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") })
  }
 }
 

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.
+// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.

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 {

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 {

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 *")
  )

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<char>.FromString(value.ToString()));
  """.formatted(dafnyUnknownErrorType)
  );
  final TokenTree cases = TokenTree

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<char>.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<char>.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<char>.FromString(value.ToString()));".formatted(
  DotNetNameResolver.dafnyUnknownErrorTypeForServiceShape(
  serviceShape
  )

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<char>.FromString(error.ToString()));
  """.formatted(dafnyUnknownErrorType)
  );
 

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<BuilderMemberSpec> COLLECTION_ARGS = List.of(

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();

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();
  }
 

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();
  }

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,30 +160,33 @@ 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,
  // and this function should only cast to Opaque error via `else`
  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
  );
  }
  }

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))"""
  );
  }
  );