Skip to content

Commit

Permalink
fix: Opaque to Exception conversion (#710)
Browse files Browse the repository at this point in the history
* fix: Opaque to Exception conversion
  • Loading branch information
ajewellamz authored Nov 11, 2024
1 parent fe48098 commit cb301b9
Show file tree
Hide file tree
Showing 2 changed files with 38 additions and 8 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -554,19 +554,32 @@ protected MethodSpec errorOpaque() {
VAR_INPUT,
Dafny.datatypeDeconstructor("obj")
)
// If obj is ANY Exception
// If obj is A RuntimeException
.nextControlFlow(
"else if ($L.$L instanceof $T)",
VAR_INPUT,
Dafny.datatypeDeconstructor("obj"),
Exception.class
RuntimeException.class
)
.addStatement(
"return ($T) $L.$L",
RuntimeException.class,
VAR_INPUT,
Dafny.datatypeDeconstructor("obj")
)
// If obj is A Throwable
.nextControlFlow(
"else if ($L.$L instanceof $T)",
VAR_INPUT,
Dafny.datatypeDeconstructor("obj"),
Throwable.class
)
.addStatement(
"return new RuntimeException(String.format($S, (Throwable) dafnyValue.dtor_obj()))",
"Unknown error thrown while calling " +
AwsSdkNativeV2.titleForService(subject.serviceShape) +
". %s"
)
.endControlFlow()
// If obj is not ANY exception and String is not set, Give Up with IllegalStateException
.addStatement(
Expand Down Expand Up @@ -608,19 +621,32 @@ protected MethodSpec errorOpaqueWithText() {
VAR_INPUT,
Dafny.datatypeDeconstructor("obj")
)
// If obj is ANY Exception
// If obj is A RuntimeException
.nextControlFlow(
"else if ($L.$L instanceof $T)",
VAR_INPUT,
Dafny.datatypeDeconstructor("obj"),
Exception.class
RuntimeException.class
)
.addStatement(
"return ($T) $L.$L",
RuntimeException.class,
VAR_INPUT,
Dafny.datatypeDeconstructor("obj")
)
// If obj is A Throwable
.nextControlFlow(
"else if ($L.$L instanceof $T)",
VAR_INPUT,
Dafny.datatypeDeconstructor("obj"),
Throwable.class
)
.addStatement(
"return new RuntimeException(String.format($S, (Throwable) dafnyValue.dtor_obj()))",
"Unknown error thrown while calling " +
AwsSdkNativeV2.titleForService(subject.serviceShape) +
". %s"
)
.endControlFlow()
// If obj is not ANY exception and String is not set, Give Up with IllegalStateException
.addStatement(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -97,9 +97,9 @@ public static software.amazon.awssdk.services.kms.model.RequiredListEnum Require
"""
package software.amazon.cryptography.services.kms.internaldafny;
import java.lang.Exception;
import java.lang.IllegalStateException;
import java.lang.RuntimeException;
import java.lang.Throwable;
import software.amazon.awssdk.services.kms.KmsClient;
import software.amazon.awssdk.services.kms.model.DependencyTimeoutException;
import software.amazon.awssdk.services.kms.model.DoSomethingRequest;
Expand Down Expand Up @@ -148,10 +148,12 @@ public static RuntimeException Error(Error_Opaque dafnyValue) {
// 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) {
} else if (dafnyValue.dtor_obj() instanceof RuntimeException) {
return (RuntimeException) dafnyValue.dtor_obj();
} else if (dafnyValue.dtor_obj() instanceof Throwable) {
return new RuntimeException(String.format("Unknown error thrown while calling AWS. %%s", (Throwable) dafnyValue.dtor_obj()));
}
return new IllegalStateException(String.format(%s, dafnyValue));
return new IllegalStateException(String.format(%s, dafnyValue));
}
public static RuntimeException Error(Error_OpaqueWithText dafnyValue) {
Expand All @@ -162,8 +164,10 @@ public static RuntimeException Error(Error_OpaqueWithText dafnyValue) {
// 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) {
} else if (dafnyValue.dtor_obj() instanceof RuntimeException) {
return (RuntimeException) dafnyValue.dtor_obj();
} else if (dafnyValue.dtor_obj() instanceof Throwable) {
return new RuntimeException(String.format("Unknown error thrown while calling AWS. %%s", (Throwable) dafnyValue.dtor_obj()));
}
return new IllegalStateException(String.format(%s, dafnyValue));
}
Expand Down

0 comments on commit cb301b9

Please sign in to comment.