Skip to content

Commit

Permalink
fix(Java-SDK): dtor_message is never safe for Opaque (#470)
Browse files Browse the repository at this point in the history
  • Loading branch information
texastony authored Jul 3, 2024
1 parent 2baebfb commit a20908b
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 34 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -553,33 +553,6 @@ protected MethodSpec errorOpaque() {
VAR_INPUT,
Dafny.datatypeDeconstructor("obj")
)
// If String is set
.nextControlFlow(
"else if ($L.$L.$L())",
VAR_INPUT,
Dafny.datatypeDeconstructor("message"),
Dafny.datatypeConstructorIs("Some")
)
// if not null, stringify the object
.addStatement(
"final String suffix = $L.dtor_obj() != null ? String.format($S, $L.dtor_obj()) : $S;",
VAR_INPUT,
" Unknown Object: %s",
VAR_INPUT,
""
)
// Convert String from Dafny
.addStatement(
"final $T message = $L($L.$L.$L) + suffix",
String.class,
SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE
.get(ShapeType.STRING)
.asNormalReference(),
VAR_INPUT,
Dafny.datatypeDeconstructor("message"),
Dafny.datatypeDeconstructor("value")
)
.addStatement("return new $T(message)", RuntimeException.class)
.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 @@ -100,7 +100,6 @@ public static software.amazon.awssdk.services.kms.model.RequiredListEnum Require
import java.lang.Exception;
import java.lang.IllegalStateException;
import java.lang.RuntimeException;
import java.lang.String;
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 @@ -149,10 +148,6 @@ public static RuntimeException Error(Error_Opaque dafnyValue) {
return (KmsException) dafnyValue.dtor_obj();
} else if (dafnyValue.dtor_obj() instanceof Exception) {
return (RuntimeException) dafnyValue.dtor_obj();
} else if (dafnyValue.dtor_message().is_Some()) {
final String suffix = dafnyValue.dtor_obj() != null ? String.format(%s, dafnyValue.dtor_obj()) : %s;;
final String message = software.amazon.smithy.dafny.conversion.ToNative.Simple.String(dafnyValue.dtor_message().dtor_value()) + suffix;
return new RuntimeException(message);
}
return new IllegalStateException(String.format(%s, dafnyValue));
}
Expand All @@ -161,8 +156,6 @@ public static RuntimeException Error(Error_Opaque dafnyValue) {
STRING_CONVERSION,
STRING_CONVERSION,
STRING_CONVERSION,
"\" Unknown Object: %s\"",
"\"\"",
"\"Unknown error thrown while calling AWS. %s\""
);
}

0 comments on commit a20908b

Please sign in to comment.