chore: add new error type OpaqueWithText (#677)

* chore: add new error type OpaqueWithString

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java

@@ -1879,8 +1879,12 @@ public TokenTree generateModeledErrorDataType() {
           "// The Opaque error, used for native, extern, wrapped or unknown errors"
         ),
         Token.of("| Opaque(obj: object)"),
+        Token.of("// A better Opaque, with a visible string representation."),
+        Token.of("| OpaqueWithText(obj: object, objMessage : string)"),
         // Helper error for use with `extern`
-        Token.of("type OpaqueError = e: Error | e.Opaque? witness *")
+        Token.of(
+          "type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *"
+        )
       )
       .lineSeparated();
   }

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/AwsSdkTypeConversionCodegen.java

@@ -151,7 +151,7 @@ protected TokenTree errorToDafnyBody(
     final TreeSet<StructureShape> errorShapes
   ) {
     final String dafnyUnknownErrorType =
-      "%s.Error_Opaque".formatted(
+      "%s.Error_OpaqueWithText".formatted(
           DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId(
             serviceShape.getId()
           )
@@ -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
@@ -230,7 +230,7 @@ protected TokenTree errorFromDanyBody(
     final TokenTree handleBaseFromDafny = TokenTree
       .of(
         "case %1$s dafnyVal:".formatted(
-            DotNetNameResolver.dafnyUnknownErrorTypeForServiceShape(
+            DotNetNameResolver.dafnyUnknownWithTextErrorTypeForServiceShape(
               serviceShape
             )
           ),

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java

@@ -611,6 +611,10 @@ public static String baseClassForUnknownError() {
     return "OpaqueError";
   }
 
+  public static String baseClassForUnknownWithTextError() {
+    return "OpaqueWithTextError";
+  }
+
   /**
    * Implements {@code DafnyAst.NonglobalVariable.CompilerizeName} for strings which are valid enum definition names
    * according to {@link ModelUtils#isValidEnumDefinitionName(String)}.
@@ -981,6 +985,16 @@ public static String dafnyUnknownErrorTypeForServiceShape(
       );
   }
 
+  public static String dafnyUnknownWithTextErrorTypeForServiceShape(
+    final ServiceShape serviceShape
+  ) {
+    return "%s.Error_OpaqueWithText".formatted(
+        DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId(
+          serviceShape.getId()
+        )
+      );
+  }
+
   /**
    * Returns this service name, without the trailing "Factory" if it's present.
    */

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/ServiceCodegen.java

@@ -104,6 +104,15 @@ public Map<Path, TokenTree> generate() {
       opaqueExceptionPathCode.prepend(prelude)
     );
 
+    // OpaqueWithText exception class
+    final Path opaqueWithTextExceptionPath = Path.of("OpaqueWithTextError.cs");
+    final TokenTree opaqueWithTextExceptionPathCode =
+      generateOpaqueWithTextExceptionClass();
+    codeByPath.put(
+      opaqueWithTextExceptionPath,
+      opaqueWithTextExceptionPathCode.prepend(prelude)
+    );
+
     // Specific exception classes
     model
       .getStructureShapes()
@@ -348,6 +357,26 @@ public OpaqueError() : base("Unknown Unexpected Error") { }
       .namespaced(Token.of(nameResolver.namespaceForService()));
   }
 
+  /**
+   * @return an OpaqueWithText exception class that can wrap any given System.Exception,
+   * which extends from System.Exception
+   */
+  public TokenTree generateOpaqueWithTextExceptionClass() {
+    return TokenTree
+      .of(
+        """
+        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;}
+        }
+          """
+      )
+      .namespaced(Token.of(nameResolver.namespaceForService()));
+  }
+
   /**
    * @return a data class for the given structure shape
    */

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/TypeConversionCodegen.java

@@ -1606,6 +1606,14 @@ protected TokenTree errorFromDanyBody(
         "return new %1$s(dafnyVal._obj);".formatted(
             DotNetNameResolver.baseClassForUnknownError()
           ),
+        "case %1$s dafnyVal:".formatted(
+            DotNetNameResolver.dafnyUnknownWithTextErrorTypeForServiceShape(
+              serviceShape
+            )
+          ),
+        "return new %1$s(dafnyVal._obj, dafnyVal._obj.ToString());".formatted(
+            DotNetNameResolver.baseClassForUnknownWithTextError()
+          ),
         "default:",
         "// The switch MUST be complete for _IError, so `value` MUST NOT be an _IError. (How did you get here?)",
         "return new %1$s();".formatted(

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/BuilderMemberSpec.java

@@ -59,6 +59,21 @@ public class BuilderMemberSpec {
       " but that is not guaranteed."
     )
   );
+  public static final List<BuilderMemberSpec> OPAQUE_WITH_TEXT_ARGS = List.of(
+    _MESSAGE,
+    _CAUSE,
+    new BuilderMemberSpec(
+      TypeName.get(Object.class),
+      "obj",
+      "The unexpected object encountered. It MIGHT BE an Exception," +
+      " but that is not guaranteed."
+    ),
+    new BuilderMemberSpec(
+      TypeName.get(String.class),
+      "objMessage",
+      "The text equivalent of obj."
+    )
+  );
   public static final List<BuilderMemberSpec> COLLECTION_ARGS = List.of(
     _MESSAGE,
     _CAUSE,

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_OpaqueWithText(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_OpaqueWithText(nativeValue, dafny.DafnySequence.asString(nativeValue.getMessage()))",
         subject.dafnyNameResolver.abstractClassForError()
       )
       .build();

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToNativeAwsV2.java

@@ -30,6 +30,7 @@
 import software.amazon.polymorph.smithyjava.nameresolver.AwsSdkNativeV2;
 import software.amazon.polymorph.smithyjava.nameresolver.Dafny;
 import software.amazon.polymorph.smithyjava.unmodeled.OpaqueError;
+import software.amazon.polymorph.smithyjava.unmodeled.OpaqueWithTextError;
 import software.amazon.polymorph.traits.LocalServiceTrait;
 import software.amazon.polymorph.utils.AwsSdkNameResolverHelpers;
 import software.amazon.polymorph.utils.DafnyNameResolverHelpers;
@@ -183,6 +184,7 @@ TypeSpec toNative() {
       .addMethods(convertServiceErrors)
       .addMethod(modeledService(subject.serviceShape))
       .addMethod(errorOpaque())
+      .addMethod(errorOpaqueWithText())
       .addMethod(dafnyError())
       .build();
   }
@@ -578,6 +580,60 @@ protected MethodSpec errorOpaque() {
       .build();
   }
 
+  protected MethodSpec errorOpaqueWithText() {
+    final String methodName = "Error";
+    final TypeName inputType =
+      subject.dafnyNameResolver.classForOpaqueWithTextError();
+    final ClassName returnType = ClassName.get(RuntimeException.class);
+    return initializeMethodSpec(methodName, inputType, returnType)
+      .addComment("While the first two cases are logically identical,")
+      .addComment("there is a semantic distinction.")
+      .addComment(
+        "An un-modeled Service Error is different from a Java Heap Exhaustion error."
+      )
+      .addComment("In the future, Smithy-Dafny MAY allow for this distinction.")
+      .addComment(
+        "Which would allow Dafny developers to treat the two differently."
+      )
+      // If obj is an instance of the Service's Base Exception
+      .beginControlFlow(
+        "if ($L.$L instanceof $T)",
+        VAR_INPUT,
+        Dafny.datatypeDeconstructor("obj"),
+        subject.nativeNameResolver.baseErrorForService()
+      )
+      .addStatement(
+        "return ($T) $L.$L",
+        subject.nativeNameResolver.baseErrorForService(),
+        VAR_INPUT,
+        Dafny.datatypeDeconstructor("obj")
+      )
+      // If obj is ANY Exception
+      .nextControlFlow(
+        "else if ($L.$L instanceof $T)",
+        VAR_INPUT,
+        Dafny.datatypeDeconstructor("obj"),
+        Exception.class
+      )
+      .addStatement(
+        "return ($T) $L.$L",
+        RuntimeException.class,
+        VAR_INPUT,
+        Dafny.datatypeDeconstructor("obj")
+      )
+      .endControlFlow()
+      // If obj is not ANY exception and String is not set, Give Up with IllegalStateException
+      .addStatement(
+        "return new $T(String.format($S, $L))",
+        IllegalStateException.class,
+        "Unknown error thrown while calling " +
+        AwsSdkNativeV2.titleForService(subject.serviceShape) +
+        ". %s",
+        VAR_INPUT
+      )
+      .build();
+  }
+
   MethodSpec dafnyError() {
     ClassName inputType = subject.dafnyNameResolver.abstractClassForError();
     ClassName returnType = ClassName.get(RuntimeException.class);
@@ -597,6 +653,7 @@ MethodSpec dafnyError() {
       .map(simpleName -> simpleName.replaceFirst("Error_", ""))
       .collect(Collectors.toCollection(ArrayList::new)); // We need a mutable list, so we can't use stream().toList()
     allDafnyErrorConstructors.add("Opaque");
+    allDafnyErrorConstructors.add("OpaqueWithText");
     allDafnyErrorConstructors.forEach(constructorName ->
       method
         .beginControlFlow(

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ModelCodegen.java

@@ -11,6 +11,7 @@
 import software.amazon.polymorph.smithyjava.modeled.ModeledUnion;
 import software.amazon.polymorph.smithyjava.unmodeled.CollectionOfErrors;
 import software.amazon.polymorph.smithyjava.unmodeled.OpaqueError;
+import software.amazon.polymorph.smithyjava.unmodeled.OpaqueWithTextError;
 import software.amazon.smithy.model.shapes.Shape;
 import software.amazon.smithy.model.shapes.StructureShape;
 import software.amazon.smithy.model.shapes.UnionShape;
@@ -50,6 +51,7 @@ public LinkedHashSet<JavaFile> javaFiles() {
     LinkedHashSet<JavaFile> rtn = new LinkedHashSet<>();
     // Opaque Exception Class
     rtn.add(OpaqueError.javaFile(modelPackageName));
+    rtn.add(OpaqueWithTextError.javaFile(modelPackageName));
     // Collection of Errors class
     rtn.add(CollectionOfErrors.javaFile(modelPackageName));
     // Modeled exception classes

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToDafnyLibrary.java

@@ -25,6 +25,7 @@
 import software.amazon.polymorph.smithyjava.nameresolver.Native;
 import software.amazon.polymorph.smithyjava.unmodeled.CollectionOfErrors;
 import software.amazon.polymorph.smithyjava.unmodeled.OpaqueError;
+import software.amazon.polymorph.smithyjava.unmodeled.OpaqueWithTextError;
 import software.amazon.polymorph.traits.DafnyUtf8BytesTrait;
 import software.amazon.polymorph.traits.PositionalTrait;
 import software.amazon.polymorph.utils.ModelUtils;
@@ -83,6 +84,7 @@ TypeSpec toDafny() {
     toDafnyMethods.add(runtimeException());
     // OpaqueError
     toDafnyMethods.add(opaqueError());
+    toDafnyMethods.add(opaqueWithTextError());
     // CollectionError
     toDafnyMethods.add(collectionError());
     // Structures
@@ -160,6 +162,11 @@ MethodSpec runtimeException() {
     allNativeErrors.add(
       OpaqueError.nativeClassName(subject.nativeNameResolver.modelPackage)
     );
+    allNativeErrors.add(
+      OpaqueWithTextError.nativeClassName(
+        subject.nativeNameResolver.modelPackage
+      )
+    );
     allNativeErrors.add(
       CollectionOfErrors.nativeClassName(
         subject.nativeNameResolver.modelPackage
@@ -195,6 +202,25 @@ MethodSpec opaqueError() {
       .build();
   }
 
+  MethodSpec opaqueWithTextError() {
+    TypeName dafnyError = subject.dafnyNameResolver.abstractClassForError();
+    ClassName opaqueWithTextError = OpaqueWithTextError.nativeClassName(
+      subject.nativeNameResolver.modelPackage
+    );
+    return MethodSpec
+      .methodBuilder("Error")
+      .returns(dafnyError)
+      .addModifiers(PUBLIC_STATIC)
+      .addParameter(opaqueWithTextError, VAR_INPUT)
+      .addStatement(
+        "return $T.create_OpaqueWithText($L.obj(), dafny.DafnySequence.asString($L.objMessage()))",
+        dafnyError,
+        VAR_INPUT,
+        VAR_INPUT
+      )
+      .build();
+  }
+
   MethodSpec collectionError() {
     ClassName dafnyError = subject.dafnyNameResolver.abstractClassForError();
     ClassName nativeError = CollectionOfErrors.nativeClassName(

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/ToNativeLibrary.java

@@ -26,6 +26,7 @@
 import software.amazon.polymorph.smithyjava.nameresolver.Native;
 import software.amazon.polymorph.smithyjava.unmodeled.CollectionOfErrors;
 import software.amazon.polymorph.smithyjava.unmodeled.OpaqueError;
+import software.amazon.polymorph.smithyjava.unmodeled.OpaqueWithTextError;
 import software.amazon.polymorph.traits.DafnyUtf8BytesTrait;
 import software.amazon.polymorph.traits.ExtendableTrait;
 import software.amazon.polymorph.traits.LocalServiceTrait;
@@ -84,6 +85,7 @@ TypeSpec toNative() {
     ArrayList<MethodSpec> toNativeMethods = new ArrayList<>();
     // OpaqueError
     toNativeMethods.add(opaqueError());
+    toNativeMethods.add(opaqueWithTextError());
     // CollectionError
     toNativeMethods.add(collectionError());
     // Modeled exception classes
@@ -169,6 +171,36 @@ MethodSpec opaqueError() {
     return super.buildAndReturn(method);
   }
 
+  MethodSpec opaqueWithTextError() {
+    ClassName inputType = subject.dafnyNameResolver.classForDatatypeConstructor(
+      "Error",
+      "OpaqueWithText"
+    );
+    ClassName returnType = OpaqueWithTextError.nativeClassName(
+      subject.modelPackageName
+    );
+    MethodSpec.Builder method = super.initializeErrorMethodSpec(
+      inputType,
+      returnType
+    );
+    method = super.createNativeBuilder(method, returnType);
+    // Set Value
+    method.addStatement(
+      "$L.obj($L.$L)",
+      NATIVE_BUILDER,
+      VAR_INPUT,
+      datatypeDeconstructor("obj")
+    );
+    method.addStatement(
+      "$L.objMessage(software.amazon.smithy.dafny.conversion.ToNative.Simple.String($L.$L))",
+      NATIVE_BUILDER,
+      VAR_INPUT,
+      datatypeDeconstructor("objMessage")
+    );
+    // Build and Return
+    return super.buildAndReturn(method);
+  }
+
   MethodSpec collectionError() {
     ClassName inputType = subject.dafnyNameResolver.classForDatatypeConstructor(
       "Error",
@@ -229,6 +261,7 @@ MethodSpec dafnyError() {
       .map(simpleName -> simpleName.replaceFirst("Error_", ""))
       .collect(Collectors.toCollection(ArrayList::new)); // We need a mutable list, so we can't use stream().toList()
     allDafnyErrorConstructors.add("Opaque");
+    allDafnyErrorConstructors.add("OpaqueWithText");
     allDafnyErrorConstructors.add("CollectionOfErrors");
     allDafnyErrorConstructors.forEach(constructorName ->
       method

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java

@@ -425,6 +425,10 @@ public ClassName classForOpaqueError() {
     return classForDatatypeConstructor("Error", "Opaque");
   }
 
+  public ClassName classForOpaqueWithTextError() {
+    return classForDatatypeConstructor("Error", "OpaqueWithText");
+  }
+
   public CodeBlock typeDescriptor(ShapeId shapeId) {
     Shape shape = model
       .getShape(shapeId)