Skip to content

Commit

Permalink
Fix unit tests and local service
Browse files Browse the repository at this point in the history
  • Loading branch information
@robin-aws
robin-aws committed Oct 30, 2023
1 parent ae8d542 commit 9e2cb47
Show file tree
Hide file tree
Showing 6 changed files with 196 additions and 41 deletions.
2 changes: 1 addition & 1 deletion ...vice/runtimes/java/src/test/java/simple/localservice/internaldafny/wrapped/__default.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ public static Result<ISimpleLocalServiceClient, Error> WrappedSimpleLocalService
simple.localservice.SimpleLocalService impl = SimpleLocalService.builder().SimpleLocalServiceConfig(wrappedConfig).build();
TestToNativeAndToDafnyLocalService(impl);
TestSimpleLocalService wrappedClient = TestSimpleLocalService.builder().impl(impl).build();
return Result.create_Success(dafny.TypeDescriptor.reference(ISimpleLocalServiceClient.class), Error._typeDescriptor(), wrappedClient);
return TestSimpleLocalService.createSuccessOfClient(wrappedClient);
}

// TODO: Determine how to replace this test with Dafny Source Code
Expand Down
6 changes: 5 additions & 1 deletion ...-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,11 +96,15 @@ public static String datatypeConstructorCreate(String name, boolean isRecordType
return "create_" + DafnyNameResolverHelpers.dafnyCompilesExtra_(name);
}

private boolean datatypeConstructorsNeedTypeDescriptors() {
public static boolean datatypeConstructorsNeedTypeDescriptors(String dafnyVersion) {
// TODO: proper version comparison
return dafnyVersion.compareTo("4.2") >= 0;
}

private boolean datatypeConstructorsNeedTypeDescriptors() {
return datatypeConstructorsNeedTypeDescriptors(dafnyVersion);
}

public CodeBlock createNone(CodeBlock typeDescriptor) {
if (datatypeConstructorsNeedTypeDescriptors()) {
return CodeBlock.of(
Expand Down
196 changes: 164 additions & 32 deletions ...gen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/Constants.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@
// SPDX-License-Identifier: Apache-2.0
package software.amazon.polymorph.smithyjava.generator.awssdk.v2;

import software.amazon.polymorph.smithyjava.nameresolver.Dafny;

public class Constants {
static String DoSomethingOperation = """
@Override
Expand All @@ -19,6 +21,27 @@ public Result<DoSomethingResponse, Error> DoSomething(DoSomethingRequest input)
}
""";

static String DoSomethingOperationWithTypeDescriptors = """
@Override
public Result<DoSomethingResponse, Error> DoSomething(DoSomethingRequest input) {
software.amazon.awssdk.services.kms.model.DoSomethingRequest converted = ToNative.DoSomethingRequest(input);
try {
software.amazon.awssdk.services.kms.model.DoSomethingResponse result = _impl.doSomething(converted);
DoSomethingResponse dafnyResponse = ToDafny.DoSomethingResponse(result);
return Result.create_Success(DoSomethingResponse._typeDescriptor(), Error._typeDescriptor(), dafnyResponse);
} catch (DependencyTimeoutException ex) {
return Result.create_Failure(DoSomethingResponse._typeDescriptor(), Error._typeDescriptor(), ToDafny.Error(ex));
} catch (KmsException ex) {
return Result.create_Failure(DoSomethingResponse._typeDescriptor(), Error._typeDescriptor(), ToDafny.Error(ex));
}
}
""";

static String DoSomethingOperation(String dafnyVersion) {
return Dafny.datatypeConstructorsNeedTypeDescriptors(dafnyVersion) ?
DoSomethingOperationWithTypeDescriptors : DoSomethingOperation;
}

static String DoVoidOperation = """
@Override
public Result<Tuple0, Error> DoVoid(DoVoidRequest input) {
Expand All @@ -34,43 +57,152 @@ public Result<Tuple0, Error> DoVoid(DoVoidRequest input) {
}
""";

static String DoVoidOperationWithTypeDescriptors = """
@Override
public Result<Tuple0, Error> DoVoid(DoVoidRequest input) {
software.amazon.awssdk.services.kms.model.DoVoidRequest converted = ToNative.DoVoidRequest(input);
try {
_impl.doVoid(converted);
return Result.create_Success(dafny.Tuple0._typeDescriptor(), Error._typeDescriptor(), Tuple0.create());
} catch (DependencyTimeoutException ex) {
return Result.create_Failure(dafny.Tuple0._typeDescriptor(), Error._typeDescriptor(), ToDafny.Error(ex));
} catch (KmsException ex) {
return Result.create_Failure(dafny.Tuple0._typeDescriptor(), Error._typeDescriptor(), ToDafny.Error(ex));
}
}
""";

static String DoVoidOperation(String dafnyVersion) {
return Dafny.datatypeConstructorsNeedTypeDescriptors(dafnyVersion) ?
DoVoidOperationWithTypeDescriptors : DoVoidOperation;
}

static String MockKmsShim = """
package software.amazon.cryptography.services.kms.internaldafny;
import Wrappers_Compile.Result;
import dafny.Tuple0;
import java.lang.Override;
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.KmsException;
import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingRequest;
import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingResponse;
import software.amazon.cryptography.services.kms.internaldafny.types.DoVoidRequest;
import software.amazon.cryptography.services.kms.internaldafny.types.Error;
import software.amazon.cryptography.services.kms.internaldafny.types.IKeyManagementServiceClient;
public class Shim implements IKeyManagementServiceClient {
private final KmsClient _impl;
package software.amazon.cryptography.services.kms.internaldafny;
import Wrappers_Compile.Option;
import Wrappers_Compile.Result;
import dafny.Tuple0;
import java.lang.Boolean;
import java.lang.Exception;
import java.lang.Override;
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.KmsException;
import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingRequest;
import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingResponse;
import software.amazon.cryptography.services.kms.internaldafny.types.DoVoidRequest;
import software.amazon.cryptography.services.kms.internaldafny.types.Error;
import software.amazon.cryptography.services.kms.internaldafny.types.IKeyManagementServiceClient;
public class Shim implements IKeyManagementServiceClient {
private final KmsClient _impl;
private final String region;
public Shim(final KmsClient impl, final String region) {
this._impl = impl;
this.region = region;
}
public static Result<IKeyManagementServiceClient, Error> createSuccessOfClient(
IKeyManagementServiceClient client) {
return Result.create_Success(client);
}
private final String region;
public static Result<IKeyManagementServiceClient, Error> createFailureOfException(
Exception exception) {
Error dafny_error = Error.create_InternalServerError(Option.create_Some(CharacterSequence(exception.getMessage())));
return Result.create_Failure(dafny_error);
}
public Shim(final KmsClient impl, final String region) {
this._impl = impl;
this.region = region;
}
public static Option<Boolean> createBooleanSome(Boolean b) {
return Option.create_Some(b);
}
public KmsClient impl() {
return this._impl;
}
public static Option<Boolean> createBooleanNone() {
return Option.create_None();
}
public KmsClient impl() {
return this._impl;
}
public String region() {
return this.region;
}
%s
%s
}
""".formatted(DoSomethingOperation, DoVoidOperation);

static String MockKmsShimWithTypeDescriptors = """
package software.amazon.cryptography.services.kms.internaldafny;
import Wrappers_Compile.Option;
import Wrappers_Compile.Result;
import dafny.DafnySequence;
import dafny.Tuple0;
import dafny.TypeDescriptor;
import java.lang.Boolean;
import java.lang.Exception;
import java.lang.Override;
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.KmsException;
import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingRequest;
import software.amazon.cryptography.services.kms.internaldafny.types.DoSomethingResponse;
import software.amazon.cryptography.services.kms.internaldafny.types.DoVoidRequest;
import software.amazon.cryptography.services.kms.internaldafny.types.Error;
import software.amazon.cryptography.services.kms.internaldafny.types.IKeyManagementServiceClient;
public class Shim implements IKeyManagementServiceClient {
private final KmsClient _impl;
private final String region;
public Shim(final KmsClient impl, final String region) {
this._impl = impl;
this.region = region;
}
public static Result<IKeyManagementServiceClient, Error> createSuccessOfClient(
IKeyManagementServiceClient client) {
return Result.create_Success(TypeDescriptor.reference(IKeyManagementServiceClient.class), Error._typeDescriptor(), client);
}
public String region() {
return this.region;
}
public static Result<IKeyManagementServiceClient, Error> createFailureOfException(
Exception exception) {
Error dafny_error = Error.create_InternalServerError(Option.create_Some(DafnySequence._typeDescriptor(TypeDescriptor.CHAR), CharacterSequence(exception.getMessage())));
return Result.create_Failure(TypeDescriptor.reference(IKeyManagementServiceClient.class), Error._typeDescriptor(), dafny_error);
}
%s
%s
}
""".formatted(DoSomethingOperation, DoVoidOperation);
public static Option<Boolean> createBooleanSome(Boolean b) {
return Option.create_Some(TypeDescriptor.BOOLEAN, b);
}
public static Option<Boolean> createBooleanNone() {
return Option.create_None(TypeDescriptor.BOOLEAN);
}
public KmsClient impl() {
return this._impl;
}
public String region() {
return this.region;
}
%s
%s
}
""".formatted(DoSomethingOperationWithTypeDescriptors, DoVoidOperationWithTypeDescriptors);

static String MockKmsShim(String dafnyVersion) {
return Dafny.datatypeConstructorsNeedTypeDescriptors(dafnyVersion) ?
MockKmsShimWithTypeDescriptors : MockKmsShim;
}
}
15 changes: 9 additions & 6 deletions ...egen/src/test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,10 @@ public class ShimTest extends ForEachDafnyTest {
protected ShimV2 underTest;
protected Model model;
protected JavaAwsSdkV2 subject;
protected final String dafnyVersion;

public ShimTest(String dafnyVersion) {
this.dafnyVersion = dafnyVersion;
model = TestSetupUtils.setupLocalModel(ModelConstants.MOCK_KMS);
subject = TestSetupUtils.setupAwsSdkV2(model, "kms", dafnyVersion);
underTest = new ShimV2(subject);
Expand Down Expand Up @@ -69,9 +71,9 @@ public void operation() {
Expected:
%s""").formatted(
actualString, DoSomethingOperation
actualString, DoSomethingOperation(dafnyVersion)
),
actualString.contains(DoSomethingOperation)
actualString.contains(DoSomethingOperation(dafnyVersion))
);
}

Expand Down Expand Up @@ -103,9 +105,9 @@ public void operationVoid() {
Expected:
%s""").formatted(
actualString, DoVoidOperation
actualString, DoVoidOperation(dafnyVersion)
),
actualString.contains(DoVoidOperation)
actualString.contains(DoVoidOperation(dafnyVersion))
);
}

Expand All @@ -119,8 +121,9 @@ public void generate() {
final Path actualPath = actual.keySet().toArray(temp)[0];
assertEquals(expectedPath, actualPath);
final String actualSource = actual.get(actualPath).toString();
final String mockKmsShim = MockKmsShim(dafnyVersion);
System.out.println(actualSource);
System.out.print(MockKmsShim);
Tokenizer.tokenizeAndAssertEqual(MockKmsShim, actualSource);
System.out.print(mockKmsShim);
Tokenizer.tokenizeAndAssertEqual(mockKmsShim, actualSource);
}
}
12 changes: 12 additions & 0 deletions .../java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Constants.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,18 @@ public static software.amazon.cryptography.services.kms.internaldafny.types.Erro
}
""";

protected static String GENERATE_CONVERT_OPAQUE_ERROR_WITH_TYPE_DESCRIPTORS = """
public static software.amazon.cryptography.services.kms.internaldafny.types.Error Error(
software.amazon.awssdk.services.kms.model.KmsException nativeValue
) {
Wrappers_Compile.Option<dafny.DafnySequence<? extends java.lang.Character>> message;
message = java.util.Objects.nonNull(nativeValue.getMessage()) ?
Wrappers_Compile.Option.create_Some(dafny.DafnySequence._typeDescriptor(dafny.TypeDescriptor.CHAR), software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.getMessage()))
: Wrappers_Compile.Option.create_None(dafny.DafnySequence._typeDescriptor(dafny.TypeDescriptor.CHAR));
return new software.amazon.cryptography.services.kms.internaldafny.types.Error_Opaque(message);
}
""";

protected static final String KMS_A_STRING_OPERATION_JAVA_FILE = """
package software.amazon.cryptography.services.kms.internaldafny;
Expand Down
6 changes: 5 additions & 1 deletion .../test/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2Test.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
import software.amazon.polymorph.smithyjava.ForEachDafnyTest;
import software.amazon.polymorph.smithyjava.ModelConstants;
import software.amazon.polymorph.smithyjava.generator.awssdk.TestSetupUtils;
import software.amazon.polymorph.smithyjava.nameresolver.Dafny;
import software.amazon.polymorph.utils.TokenTree;
import software.amazon.smithy.model.Model;
import software.amazon.smithy.model.shapes.ShapeId;
Expand Down Expand Up @@ -76,7 +77,10 @@ public void generateConvert() {

@Test
public void generateConvertOpaqueError() {
tokenizeAndAssertEqual(ToDafnyAwsV2Constants.GENERATE_CONVERT_OPAQUE_ERROR, underTest.generateConvertOpaqueError().toString());
final String expected = Dafny.datatypeConstructorsNeedTypeDescriptors(dafnyVersion) ?
ToDafnyAwsV2Constants.GENERATE_CONVERT_OPAQUE_ERROR_WITH_TYPE_DESCRIPTORS
: ToDafnyAwsV2Constants.GENERATE_CONVERT_OPAQUE_ERROR;
tokenizeAndAssertEqual(expected, underTest.generateConvertOpaqueError().toString());
}

@Test
Expand Down

0 comments on commit 9e2cb47

Please sign in to comment.