Skip to content

Commit

Permalink
chore: repolymorph with latest smithy-dafny (aws#968)
Browse files Browse the repository at this point in the history
* chore: repolymorph for latest smithy-dafny
  • Loading branch information
ajewellamz authored Nov 8, 2024
1 parent f9fb3ef commit 1312493
Show file tree
Hide file tree
Showing 15 changed files with 119 additions and 416 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -1714,6 +1714,13 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object)
type OpaqueError = e: Error | e.Opaque? 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
predicate method IsDummySubsetType(x: int) {
0 < x
}

}
abstract module AbstractAwsCryptographyMaterialProvidersService
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -284,6 +284,13 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object)
type OpaqueError = e: Error | e.Opaque? 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
predicate method IsDummySubsetType(x: int) {
0 < x
}

}
abstract module AbstractAwsCryptographyKeyStoreService
{
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package software.amazon.cryptography.keystore.internaldafny.types;

public class __default
extends software.amazon.cryptography.keystore.internaldafny._ExternBase___default {}
extends software.amazon.cryptography.keystore.internaldafny.types._ExternBase___default {}
Original file line number Diff line number Diff line change
Expand Up @@ -691,6 +691,13 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny.types" }
// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object)
type OpaqueError = e: Error | e.Opaque? 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
predicate method IsDummySubsetType(x: int) {
0 < x
}

}
abstract module AbstractAwsCryptographyPrimitivesService
{
Expand Down
7 changes: 7 additions & 0 deletions ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -2905,6 +2905,13 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty
// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object)
type OpaqueError = e: Error | e.Opaque? 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
predicate method IsDummySubsetType(x: int) {
0 < x
}

}
abstract module AbstractComAmazonawsDynamodbService {
import opened Wrappers
Expand Down
131 changes: 0 additions & 131 deletions ComAmazonawsDynamodb/codegen-patches/java/dafny-4.2.0.patch

This file was deleted.

14 changes: 14 additions & 0 deletions ComAmazonawsDynamodb/codegen-patches/java/dafny-4.8.0.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
diff --git b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
index 5c6364b2..7feacebc 100644
--- b/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
+++ a/ComAmazonawsDynamodb/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/services/dynamodb/internaldafny/ToNative.java
@@ -8670,9 +8670,6 @@ public class ToNative {
if (dafnyValue.is_InternalServerError()) {
return ToNative.Error((Error_InternalServerError) dafnyValue);
}
- if (dafnyValue.is_InvalidEndpointException()) {
- return ToNative.Error((Error_InvalidEndpointException) dafnyValue);
- }
if (dafnyValue.is_InvalidExportTimeException()) {
return ToNative.Error((Error_InvalidExportTimeException) dafnyValue);
}
Original file line number Diff line number Diff line change
Expand Up @@ -354,6 +354,7 @@
import software.amazon.cryptography.services.dynamodb.internaldafny.types.DisableKinesisStreamingDestinationOutput;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.EnableKinesisStreamingDestinationInput;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.EnableKinesisStreamingDestinationOutput;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_BackupInUseException;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_BackupNotFoundException;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ConditionalCheckFailedException;
Expand All @@ -368,6 +369,7 @@
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ImportNotFoundException;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_IndexNotFoundException;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InternalServerError;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidEndpointException;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidExportTimeException;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_InvalidRestoreTimeException;
import software.amazon.cryptography.services.dynamodb.internaldafny.types.Error_ItemCollectionSizeLimitExceededException;
Expand Down Expand Up @@ -8596,10 +8598,30 @@ public static TransactionInProgressException Error(
return builder.build();
}

// BEGIN MANUAL EDIT
public static RuntimeException Error(
software.amazon.cryptography.services.dynamodb.internaldafny.types.Error dafnyValue
) {
public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) {
return ((Shim) dafnyValue).impl();
}

public static RuntimeException Error(Error_Opaque dafnyValue) {
// While the first two cases are logically identical,
// there is a semantic distinction.
// An un-modeled Service Error is different from a Java Heap Exhaustion error.
// In the future, Smithy-Dafny MAY allow for this distinction.
// Which would allow Dafny developers to treat the two differently.
if (dafnyValue.dtor_obj() instanceof DynamoDbException) {
return (DynamoDbException) dafnyValue.dtor_obj();
} else if (dafnyValue.dtor_obj() instanceof Exception) {
return (RuntimeException) dafnyValue.dtor_obj();
}
return new IllegalStateException(
String.format(
"Unknown error thrown while calling Amazon DynamoDB. %s",
dafnyValue
)
);
}

public static RuntimeException Error(Error dafnyValue) {
if (dafnyValue.is_BackupInUseException()) {
return ToNative.Error((Error_BackupInUseException) dafnyValue);
}
Expand Down Expand Up @@ -8667,6 +8689,9 @@ public static RuntimeException Error(
(Error_PointInTimeRecoveryUnavailableException) dafnyValue
);
}
if (dafnyValue.is_PolicyNotFoundException()) {
return ToNative.Error((Error_PolicyNotFoundException) dafnyValue);
}
if (dafnyValue.is_ProvisionedThroughputExceededException()) {
return ToNative.Error(
(Error_ProvisionedThroughputExceededException) dafnyValue
Expand Down Expand Up @@ -8708,32 +8733,10 @@ public static RuntimeException Error(
if (dafnyValue.is_Opaque()) {
return ToNative.Error((Error_Opaque) dafnyValue);
}
// TODO This should indicate a codegen bug
return new IllegalStateException(
String.format("Unknown error thrown while calling DDB. %s", dafnyValue)
);
}

// END MANUAL EDIT

public static DynamoDbClient DynamoDB_20120810(IDynamoDBClient dafnyValue) {
return ((Shim) dafnyValue).impl();
}

public static RuntimeException Error(Error_Opaque dafnyValue) {
// While the first two cases are logically identical,
// there is a semantic distinction.
// An un-modeled Service Error is different from a Java Heap Exhaustion error.
// In the future, Smithy-Dafny MAY allow for this distinction.
// Which would allow Dafny developers to treat the two differently.
if (dafnyValue.dtor_obj() instanceof DynamoDbException) {
return (DynamoDbException) dafnyValue.dtor_obj();
} else if (dafnyValue.dtor_obj() instanceof Exception) {
return (RuntimeException) dafnyValue.dtor_obj();
}
// TODO This should indicate a codegen bug; every error Should have been taken care of.
return new IllegalStateException(
String.format(
"Unknown error thrown while calling Amazon DynamoDB. %s",
"Unknown error thrown while calling service. %s",
dafnyValue
)
);
Expand Down
7 changes: 7 additions & 0 deletions ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -1978,6 +1978,13 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types"
// The Opaque error, used for native, extern, wrapped or unknown errors
| Opaque(obj: object)
type OpaqueError = e: Error | e.Opaque? 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
predicate method IsDummySubsetType(x: int) {
0 < x
}

}
abstract module AbstractComAmazonawsKmsService {
import opened Wrappers
Expand Down
Loading

0 comments on commit 1312493

Please sign in to comment.