Skip to content

Commit

Permalink
chore: re-polymorph to gain OpaqueWithText (aws#970)
Browse files Browse the repository at this point in the history
* chore: re-polymorph to gain OpaqueWithText
  • Loading branch information
ajewellamz authored Nov 11, 2024
1 parent 1312493 commit 697b110
Show file tree
Hide file tree
Showing 46 changed files with 1,276 additions and 22 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -1713,7 +1713,9 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object)
type OpaqueError = e: Error | e.Opaque? witness *
// A better Opaque, with a visible string representation.
| OpaqueWithText(obj: object, objMessage : string)
type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *
// This dummy subset type is included to make sure Dafny
// always generates a _ExternBase___default.java class.
type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -283,7 +283,9 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object)
type OpaqueError = e: Error | e.Opaque? witness *
// A better Opaque, with a visible string representation.
| OpaqueWithText(obj: object, objMessage : string)
type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *
// This dummy subset type is included to make sure Dafny
// always generates a _ExternBase___default.java class.
type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ module TestGetKeys {
Types.GetActiveBranchKeyInput(branchKeyIdentifier := WestBranchKey));
expect badResult.Failure?;
expect badResult.error.ComAmazonawsKms?;
expect badResult.error.ComAmazonawsKms.Opaque?;
expect badResult.error.ComAmazonawsKms.OpaqueWithText?;
// it's an opaque error, so I can't test its contents
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@
import software.amazon.cryptography.keystore.model.CollectionOfErrors;
import software.amazon.cryptography.keystore.model.KeyStoreException;
import software.amazon.cryptography.keystore.model.OpaqueError;
import software.amazon.cryptography.keystore.model.OpaqueWithTextError;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.IDynamoDBClient;
import software.amazon.cryptography.services.kms.internaldafny.types.IKMSClient;

Expand All @@ -53,6 +54,9 @@ public static Error Error(RuntimeException nativeValue) {
if (nativeValue instanceof OpaqueError) {
return ToDafny.Error((OpaqueError) nativeValue);
}
if (nativeValue instanceof OpaqueWithTextError) {
return ToDafny.Error((OpaqueWithTextError) nativeValue);
}
if (nativeValue instanceof CollectionOfErrors) {
return ToDafny.Error((CollectionOfErrors) nativeValue);
}
Expand All @@ -63,6 +67,13 @@ public static Error Error(OpaqueError nativeValue) {
return Error.create_Opaque(nativeValue.obj());
}

public static Error Error(OpaqueWithTextError nativeValue) {
return Error.create_OpaqueWithText(
nativeValue.obj(),
dafny.DafnySequence.asString(nativeValue.objMessage())
);
}

public static Error Error(CollectionOfErrors nativeValue) {
DafnySequence<? extends Error> list =
software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
import software.amazon.cryptography.keystore.internaldafny.types.Error_CollectionOfErrors;
import software.amazon.cryptography.keystore.internaldafny.types.Error_KeyStoreException;
import software.amazon.cryptography.keystore.internaldafny.types.Error_Opaque;
import software.amazon.cryptography.keystore.internaldafny.types.Error_OpaqueWithText;
import software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient;
import software.amazon.cryptography.keystore.model.BeaconKeyMaterials;
import software.amazon.cryptography.keystore.model.BranchKeyMaterials;
Expand All @@ -37,6 +38,7 @@
import software.amazon.cryptography.keystore.model.KeyStoreException;
import software.amazon.cryptography.keystore.model.MRDiscovery;
import software.amazon.cryptography.keystore.model.OpaqueError;
import software.amazon.cryptography.keystore.model.OpaqueWithTextError;
import software.amazon.cryptography.keystore.model.VersionKeyInput;
import software.amazon.cryptography.keystore.model.VersionKeyOutput;

Expand All @@ -48,6 +50,17 @@ public static OpaqueError Error(Error_Opaque dafnyValue) {
return nativeBuilder.build();
}

public static OpaqueWithTextError Error(Error_OpaqueWithText dafnyValue) {
OpaqueWithTextError.Builder nativeBuilder = OpaqueWithTextError.builder();
nativeBuilder.obj(dafnyValue.dtor_obj());
nativeBuilder.objMessage(
software.amazon.smithy.dafny.conversion.ToNative.Simple.String(
dafnyValue.dtor_objMessage()
)
);
return nativeBuilder.build();
}

public static CollectionOfErrors Error(Error_CollectionOfErrors dafnyValue) {
CollectionOfErrors.Builder nativeBuilder = CollectionOfErrors.builder();
nativeBuilder.list(
Expand Down Expand Up @@ -81,6 +94,9 @@ public static RuntimeException Error(Error dafnyValue) {
if (dafnyValue.is_Opaque()) {
return ToNative.Error((Error_Opaque) dafnyValue);
}
if (dafnyValue.is_OpaqueWithText()) {
return ToNative.Error((Error_OpaqueWithText) dafnyValue);
}
if (dafnyValue.is_CollectionOfErrors()) {
return ToNative.Error((Error_CollectionOfErrors) dafnyValue);
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,180 @@
// 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.
package software.amazon.cryptography.keystore.model;

public class OpaqueWithTextError extends RuntimeException {

/**
* The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed.
*/
private final Object obj;

/**
* The text equivalent of obj.
*/
private final String objMessage;

protected OpaqueWithTextError(BuilderImpl builder) {
super(messageFromBuilder(builder), builder.cause());
this.obj = builder.obj();
this.objMessage = builder.objMessage();
}

private static String messageFromBuilder(Builder builder) {
if (builder.message() != null) {
return builder.message();
}
if (builder.cause() != null) {
return builder.cause().getMessage();
}
return null;
}

/**
* See {@link Throwable#getMessage()}.
*/
public String message() {
return this.getMessage();
}

/**
* See {@link Throwable#getCause()}.
*/
public Throwable cause() {
return this.getCause();
}

/**
* @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed.
*/
public Object obj() {
return this.obj;
}

/**
* @return The text equivalent of obj.
*/
public String objMessage() {
return this.objMessage;
}

public Builder toBuilder() {
return new BuilderImpl(this);
}

public static Builder builder() {
return new BuilderImpl();
}

public interface Builder {
/**
* @param message The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method.
*/
Builder message(String message);

/**
* @return The detailed message. The detail message is saved for later retrieval by the {@link #getMessage()} method.
*/
String message();

/**
* @param cause The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.)
*/
Builder cause(Throwable cause);

/**
* @return The cause (which is saved for later retrieval by the {@link #getCause()} method). (A {@code null} value is permitted, and indicates that the cause is nonexistent or unknown.)
*/
Throwable cause();

/**
* @param obj The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed.
*/
Builder obj(Object obj);

/**
* @return The unexpected object encountered. It MIGHT BE an Exception, but that is not guaranteed.
*/
Object obj();

/**
* @param objMessage The text equivalent of obj.
*/
Builder objMessage(String objMessage);

/**
* @return The text equivalent of obj.
*/
String objMessage();

OpaqueWithTextError build();
}

static class BuilderImpl implements Builder {

protected String message;

protected Throwable cause;

protected Object obj;

protected String objMessage;

protected BuilderImpl() {}

protected BuilderImpl(OpaqueWithTextError model) {
this.cause = model.getCause();
this.message = model.getMessage();
this.obj = model.obj();
this.objMessage = model.objMessage();
}

public Builder message(String message) {
this.message = message;
return this;
}

public String message() {
return this.message;
}

public Builder cause(Throwable cause) {
this.cause = cause;
return this;
}

public Throwable cause() {
return this.cause;
}

public Builder obj(Object obj) {
this.obj = obj;
return this;
}

public Object obj() {
return this.obj;
}

public Builder objMessage(String objMessage) {
this.objMessage = objMessage;
return this;
}

public String objMessage() {
return this.objMessage;
}

public OpaqueWithTextError build() {
if (
this.obj != null && this.cause == null && this.obj instanceof Throwable
) {
this.cause = (Throwable) this.obj;
} else if (this.obj == null && this.cause != null) {
this.obj = this.cause;
}
return new OpaqueWithTextError(this);
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -126,6 +126,7 @@
import software.amazon.cryptography.materialproviders.model.InvalidEncryptionMaterials;
import software.amazon.cryptography.materialproviders.model.InvalidEncryptionMaterialsTransition;
import software.amazon.cryptography.materialproviders.model.OpaqueError;
import software.amazon.cryptography.materialproviders.model.OpaqueWithTextError;
import software.amazon.cryptography.primitives.internaldafny.types.DigestAlgorithm;
import software.amazon.cryptography.primitives.internaldafny.types.ECDHCurveSpec;
import software.amazon.cryptography.primitives.internaldafny.types.ECDSASignatureAlgorithm;
Expand Down Expand Up @@ -170,6 +171,9 @@ public static Error Error(RuntimeException nativeValue) {
if (nativeValue instanceof OpaqueError) {
return ToDafny.Error((OpaqueError) nativeValue);
}
if (nativeValue instanceof OpaqueWithTextError) {
return ToDafny.Error((OpaqueWithTextError) nativeValue);
}
if (nativeValue instanceof CollectionOfErrors) {
return ToDafny.Error((CollectionOfErrors) nativeValue);
}
Expand All @@ -180,6 +184,13 @@ public static Error Error(OpaqueError nativeValue) {
return Error.create_Opaque(nativeValue.obj());
}

public static Error Error(OpaqueWithTextError nativeValue) {
return Error.create_OpaqueWithText(
nativeValue.obj(),
dafny.DafnySequence.asString(nativeValue.objMessage())
);
}

public static Error Error(CollectionOfErrors nativeValue) {
DafnySequence<? extends Error> list =
software.amazon.smithy.dafny.conversion.ToDafny.Aggregate.GenericToSequence(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
import software.amazon.cryptography.materialproviders.internaldafny.types.Error_InvalidEncryptionMaterials;
import software.amazon.cryptography.materialproviders.internaldafny.types.Error_InvalidEncryptionMaterialsTransition;
import software.amazon.cryptography.materialproviders.internaldafny.types.Error_Opaque;
import software.amazon.cryptography.materialproviders.internaldafny.types.Error_OpaqueWithText;
import software.amazon.cryptography.materialproviders.internaldafny.types.IAwsCryptographicMaterialProvidersClient;
import software.amazon.cryptography.materialproviders.model.AesWrappingAlg;
import software.amazon.cryptography.materialproviders.model.AlgorithmSuiteId;
Expand Down Expand Up @@ -107,6 +108,7 @@
import software.amazon.cryptography.materialproviders.model.OnEncryptInput;
import software.amazon.cryptography.materialproviders.model.OnEncryptOutput;
import software.amazon.cryptography.materialproviders.model.OpaqueError;
import software.amazon.cryptography.materialproviders.model.OpaqueWithTextError;
import software.amazon.cryptography.materialproviders.model.PaddingScheme;
import software.amazon.cryptography.materialproviders.model.PublicKeyDiscoveryInput;
import software.amazon.cryptography.materialproviders.model.PutCacheEntryInput;
Expand All @@ -131,6 +133,17 @@ public static OpaqueError Error(Error_Opaque dafnyValue) {
return nativeBuilder.build();
}

public static OpaqueWithTextError Error(Error_OpaqueWithText dafnyValue) {
OpaqueWithTextError.Builder nativeBuilder = OpaqueWithTextError.builder();
nativeBuilder.obj(dafnyValue.dtor_obj());
nativeBuilder.objMessage(
software.amazon.smithy.dafny.conversion.ToNative.Simple.String(
dafnyValue.dtor_objMessage()
)
);
return nativeBuilder.build();
}

public static CollectionOfErrors Error(Error_CollectionOfErrors dafnyValue) {
CollectionOfErrors.Builder nativeBuilder = CollectionOfErrors.builder();
nativeBuilder.list(
Expand Down Expand Up @@ -315,6 +328,9 @@ public static RuntimeException Error(Error dafnyValue) {
if (dafnyValue.is_Opaque()) {
return ToNative.Error((Error_Opaque) dafnyValue);
}
if (dafnyValue.is_OpaqueWithText()) {
return ToNative.Error((Error_OpaqueWithText) dafnyValue);
}
if (dafnyValue.is_CollectionOfErrors()) {
return ToNative.Error((Error_CollectionOfErrors) dafnyValue);
}
Expand Down
Loading

0 comments on commit 697b110

Please sign in to comment.