Skip to content

Commit

Permalink
Add dafnyVersion parameter, make type descriptors conditional
Browse files Browse the repository at this point in the history
  • Loading branch information
@robin-aws
robin-aws committed Oct 28, 2023
1 parent 213da2b commit a116040
Show file tree
Hide file tree
Showing 21 changed files with 233 additions and 97 deletions.
23 changes: 20 additions & 3 deletions codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/CodegenEngine.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ public class CodegenEngine {
private final Path[] dependentModelPaths;
private final String namespace;
private final Map<TargetLanguage, Path> targetLangOutputDirs;
private final String dafnyVersion;
// refactor this to only be required if generating Java
private final AwsSdkVersion javaAwsSdkVersion;
private final Optional<Path> includeDafnyFile;
Expand All @@ -62,6 +63,7 @@ private CodegenEngine(
final Path[] dependentModelPaths,
final String namespace,
final Map<TargetLanguage, Path> targetLangOutputDirs,
final String dafnyVersion,
final AwsSdkVersion javaAwsSdkVersion,
final Optional<Path> includeDafnyFile,
final boolean awsSdkStyle,
Expand All @@ -72,6 +74,7 @@ private CodegenEngine(
this.dependentModelPaths = dependentModelPaths;
this.namespace = namespace;
this.targetLangOutputDirs = targetLangOutputDirs;
this.dafnyVersion = dafnyVersion;
this.javaAwsSdkVersion = javaAwsSdkVersion;
this.includeDafnyFile = includeDafnyFile;
this.awsSdkStyle = awsSdkStyle;
Expand Down Expand Up @@ -150,13 +153,13 @@ private void generateJava(final Path outputDir) {
}

private void javaLocalService(final Path outputDir) {
final JavaLibrary javaLibrary = new JavaLibrary(this.model, this.serviceShape, this.javaAwsSdkVersion);
final JavaLibrary javaLibrary = new JavaLibrary(this.model, this.serviceShape, this.javaAwsSdkVersion, this.dafnyVersion);
IOUtils.writeTokenTreesIntoDir(javaLibrary.generate(), outputDir);
LOGGER.info("Java code generated in {}", outputDir);
}

private void javaWrappedLocalService(final Path outputDir) {
final TestJavaLibrary testJavaLibrary = new TestJavaLibrary(model, serviceShape, this.javaAwsSdkVersion);
final TestJavaLibrary testJavaLibrary = new TestJavaLibrary(model, serviceShape, this.javaAwsSdkVersion, this.dafnyVersion);
IOUtils.writeTokenTreesIntoDir(testJavaLibrary.generate(), outputDir);
LOGGER.info("Java that tests a local service generated in {}", outputDir);
}
Expand All @@ -168,7 +171,7 @@ private void javaAwsSdkV1(Path outputDir) {
}

private void javaAwsSdkV2(final Path outputDir) {
final JavaAwsSdkV2 javaV2ShimCodegen = JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, model);
final JavaAwsSdkV2 javaV2ShimCodegen = JavaAwsSdkV2.createJavaAwsSdkV2(serviceShape, model, dafnyVersion);
IOUtils.writeTokenTreesIntoDir(javaV2ShimCodegen.generate(), outputDir);
LOGGER.info("Java V2 code generated in {}", outputDir);
}
Expand Down Expand Up @@ -245,6 +248,7 @@ public static class Builder {
private Path[] dependentModelPaths;
private String namespace;
private Map<TargetLanguage, Path> targetLangOutputDirs;
private String dafnyVersion = "4.1.0";
private AwsSdkVersion javaAwsSdkVersion = AwsSdkVersion.V2;
private Path includeDafnyFile;
private boolean awsSdkStyle = false;
Expand Down Expand Up @@ -286,6 +290,17 @@ public Builder withTargetLangOutputDirs(final Map<TargetLanguage, Path> targetLa
return this;
}

/**
* Sets the Dafny version for which generated code should be compatible.
* This is used to ensure both Dafny source compatibility
* and compatibility with the Dafny compiler and runtime internals,
* which shim code generation currently depends on.
*/
public Builder withDafnyVersion(final String dafnyVersion) {
this.dafnyVersion = dafnyVersion;
return this;
}

/**
* Sets the version of the AWS SDK for Java for which generated code should be compatible.
* This has no effect unless the engine is configured to generate Java code.
Expand Down Expand Up @@ -341,6 +356,7 @@ public CodegenEngine build() {
targetLangOutputDirsRaw.replaceAll((_lang, path) -> path.toAbsolutePath().normalize());
final Map<TargetLanguage, Path> targetLangOutputDirs = ImmutableMap.copyOf(targetLangOutputDirsRaw);

final String dafnyVersion = Objects.requireNonNull(this.dafnyVersion);
final AwsSdkVersion javaAwsSdkVersion = Objects.requireNonNull(this.javaAwsSdkVersion);

if (targetLangOutputDirs.containsKey(TargetLanguage.DAFNY)
Expand All @@ -360,6 +376,7 @@ public CodegenEngine build() {
dependentModelPaths,
this.namespace,
targetLangOutputDirs,
dafnyVersion,
javaAwsSdkVersion,
includeDafnyFile,
this.awsSdkStyle,
Expand Down
9 changes: 3 additions & 6 deletions ...y-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -196,14 +196,11 @@ protected CodeBlock memberAssign(
}
CodeBlock typeDescriptor = subject.dafnyNameResolver.typeDescriptor(memberShape.getTarget());
return CodeBlock.of(
"$L = $L ?\n$T.create_Some($L, $L)\n: $T.create_None($L)",
"$L = $L ?\n$L\n: $L",
outputVar,
isSetCheck,
ClassName.get("Wrappers_Compile", "Option"),
typeDescriptor,
memberConversion,
ClassName.get("Wrappers_Compile", "Option"),
typeDescriptor
subject.dafnyNameResolver.createSome(typeDescriptor, memberConversion),
subject.dafnyNameResolver.createNone(typeDescriptor)
);
}

Expand Down
29 changes: 16 additions & 13 deletions ...odegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ShimV1.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,10 +144,10 @@ Optional<MethodSpec> operation(final ShapeId operationShapeId) {
successTypeDescriptor = CodeBlock.of(DAFNY_TUPLE0_CLASS_NAME + "._typeDescriptor()");
builder.addStatement("_impl.$L(converted)",
StringUtils.uncapitalize(operationName))
.addStatement("return $T.create_Success($L, Error._typeDescriptor(), $T.create())",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor,
DAFNY_TUPLE0_CLASS_NAME);
.addStatement("return $L",
subject.dafnyNameResolver.createSuccess(
successTypeDescriptor,
CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME)));
} else {
successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputShapeId);
builder.addStatement("$T result = _impl.$L(converted)",
Expand All @@ -156,23 +156,26 @@ Optional<MethodSpec> operation(final ShapeId operationShapeId) {
.addStatement("$T dafnyResponse = ToDafny.$L(result)",
dafnyOutput,
StringUtils.capitalize(outputShapeId.getName()))
.addStatement("return $T.create_Success($L, Error._typeDescriptor(), dafnyResponse)",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor);
.addStatement("return $L",
subject.dafnyNameResolver.createSuccess(
successTypeDescriptor,
CodeBlock.of("dafnyResponse")));
}

operationShape.getErrors().stream().sorted().forEach(shapeId ->
builder
.nextControlFlow("catch ($T ex)", subject.nativeNameResolver.typeForShape(shapeId))
.addStatement("return $T.create_Failure($L, Error._typeDescriptor(), ToDafny.Error(ex))",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor)
.addStatement("return $L",
subject.dafnyNameResolver.createFailure(
successTypeDescriptor,
CodeBlock.of("ToDafny.Error(ex)")))
);
return Optional.of(builder
.nextControlFlow("catch ($T ex)", subject.nativeNameResolver.baseErrorForService())
.addStatement("return $T.create_Failure($L, Error._typeDescriptor(), ToDafny.Error(ex))",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor)
.addStatement("return $L",
subject.dafnyNameResolver.createFailure(
successTypeDescriptor,
CodeBlock.of("ToDafny.Error(ex)")))
.endControlFlow()
.build());
}
Expand Down
4 changes: 2 additions & 2 deletions .../src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/JavaAwsSdkV2.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,8 @@ private JavaAwsSdkV2(
this.packageName = dafnyNameResolver.packageName();
}

public static JavaAwsSdkV2 createJavaAwsSdkV2(ServiceShape serviceShape, Model model) {
final AwsSdkDafnyV2 dafnyNameResolver = new AwsSdkDafnyV2(serviceShape, model);
public static JavaAwsSdkV2 createJavaAwsSdkV2(ServiceShape serviceShape, Model model, String dafnyVersion) {
final AwsSdkDafnyV2 dafnyNameResolver = new AwsSdkDafnyV2(serviceShape, model, dafnyVersion);
final AwsSdkNativeV2 nativeNameResolver = new AwsSdkNativeV2(serviceShape, model);
return new JavaAwsSdkV2(serviceShape, model, dafnyNameResolver, nativeNameResolver);
}
Expand Down
29 changes: 16 additions & 13 deletions ...odegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ShimV2.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,10 +144,10 @@ Optional<MethodSpec> operation(final ShapeId operationShapeId) {
successTypeDescriptor = CodeBlock.of(DAFNY_TUPLE0_CLASS_NAME + "._typeDescriptor()");
builder.addStatement("_impl.$L(converted)",
StringUtils.uncapitalize(operationName))
.addStatement("return $T.create_Success($L, Error._typeDescriptor(), $T.create())",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor,
DAFNY_TUPLE0_CLASS_NAME);
.addStatement("return $L",
subject.dafnyNameResolver.createSuccess(
successTypeDescriptor,
CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME)));
} else {
successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputShapeId);
builder.addStatement("$T result = _impl.$L(converted)",
Expand All @@ -156,9 +156,10 @@ Optional<MethodSpec> operation(final ShapeId operationShapeId) {
.addStatement("$T dafnyResponse = ToDafny.$L(result)",
dafnyOutput,
StringUtils.capitalize(outputShapeId.getName()))
.addStatement("return $T.create_Success($L, Error._typeDescriptor(), dafnyResponse)",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor);
.addStatement("return $L",
subject.dafnyNameResolver.createSuccess(
successTypeDescriptor,
CodeBlock.of("dafnyResponse")));
}

operationShape.getErrors().stream().sorted().forEach(shapeId -> {
Expand All @@ -171,15 +172,17 @@ Optional<MethodSpec> operation(final ShapeId operationShapeId) {

builder
.nextControlFlow("catch ($T ex)", subject.nativeNameResolver.typeForShape(shapeId))
.addStatement("return $T.create_Failure($L, Error._typeDescriptor(), ToDafny.Error(ex))",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor);
.addStatement("return $L",
subject.dafnyNameResolver.createFailure(
successTypeDescriptor,
CodeBlock.of("ToDafny.Error(ex)")));
});
return Optional.of(builder
.nextControlFlow("catch ($T ex)", subject.nativeNameResolver.baseErrorForService())
.addStatement("return $T.create_Failure($L, Error._typeDescriptor(), ToDafny.Error(ex))",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor)
.addStatement("return $L",
subject.dafnyNameResolver.createFailure(
successTypeDescriptor,
CodeBlock.of("ToDafny.Error(ex)")))
.endControlFlow()
.build());
}
Expand Down
15 changes: 7 additions & 8 deletions .../src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -522,17 +522,16 @@ MethodSpec generateConvertOpaqueError() {
// but with calls to dafnyNameResolver replaced with their expected response.
CodeBlock stringTypeDescriptor = Dafny.TYPE_DESCRIPTOR_BY_SHAPE_TYPE.get(ShapeType.STRING);
CodeBlock memberAssignment = CodeBlock.of(
"$L = $T.nonNull($L) ?\n$T.create_Some($L, $T.$L($L))\n: $T.create_None($L)",
"$L = $T.nonNull($L) ?\n$L\n: $L",
"message",
ClassName.get(Objects.class),
"nativeValue.getMessage()",
ClassName.get("Wrappers_Compile", "Option"),
stringTypeDescriptor,
COMMON_TO_DAFNY_SIMPLE,
SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE.get(ShapeType.STRING).methodName(),
"nativeValue.getMessage()",
ClassName.get("Wrappers_Compile", "Option"),
stringTypeDescriptor
subject.dafnyNameResolver.createSome(stringTypeDescriptor,
CodeBlock.of("$T.$L($L)",
COMMON_TO_DAFNY_SIMPLE,
SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE.get(ShapeType.STRING).methodName(),
"nativeValue.getMessage()")),
subject.dafnyNameResolver.createNone(stringTypeDescriptor)
);
return MethodSpec.methodBuilder("Error")
.addModifiers(Modifier.PUBLIC, Modifier.STATIC)
Expand Down
8 changes: 4 additions & 4 deletions ...gen/src/main/java/software/amazon/polymorph/smithyjava/generator/library/JavaLibrary.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,8 @@ public class JavaLibrary extends CodegenSubject {
public final ToDafnyLibrary toDafnyLibrary;
public final ToNativeLibrary toNativeLibrary;

public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion) {
super(model, serviceShape, initDafny(model, serviceShape, sdkVersion), initNative(model, serviceShape, sdkVersion), sdkVersion);
public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion, String dafnyVersion) {
super(model, serviceShape, initDafny(model, serviceShape, sdkVersion, dafnyVersion), initNative(model, serviceShape, sdkVersion), sdkVersion);
packageName = NamespaceHelper.standardize(serviceShape.getId().getNamespace());
modelPackageName = packageName + ".model";
try {
Expand All @@ -77,9 +77,9 @@ public JavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVers
toNativeLibrary = new ToNativeLibrary(this);
}

static Dafny initDafny(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion) {
static Dafny initDafny(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion, String dafnyVersion) {
String packageName = DafnyNameResolverHelpers.packageNameForNamespace(serviceShape.getId().getNamespace());
return new Dafny(packageName, model, serviceShape, awsSdkVersion);
return new Dafny(packageName, model, serviceShape, awsSdkVersion, dafnyVersion);
}

static Native initNative(Model model, ServiceShape serviceShape, AwsSdkVersion awsSdkVersion) {
Expand Down
4 changes: 2 additions & 2 deletions ...src/main/java/software/amazon/polymorph/smithyjava/generator/library/TestJavaLibrary.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ public class TestJavaLibrary extends JavaLibrary {
@SuppressWarnings("unused")
private static final Logger LOGGER = LoggerFactory.getLogger(TestJavaLibrary.class);

public TestJavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion) {
super(model, serviceShape, sdkVersion);
public TestJavaLibrary(Model model, ServiceShape serviceShape, AwsSdkVersion sdkVersion, String dafnyVersion) {
super(model, serviceShape, sdkVersion, dafnyVersion);
}

@Override
Expand Down
22 changes: 12 additions & 10 deletions ...y-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/modeled/Operation.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,28 +63,30 @@ public static MethodSpec operation(
successTypeDescriptor = CodeBlock.of("dafny.Tuple0._typeDescriptor()");
method
.addStatement(invoke(operationName))
.addStatement("return $T.create_Success($L, Error._typeDescriptor(), $T.create())",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor,
DAFNY_TUPLE0_CLASS_NAME);
.addStatement("return $L",
subject.dafnyNameResolver.createSuccess(
successTypeDescriptor,
CodeBlock.of("$T.create()", DAFNY_TUPLE0_CLASS_NAME)));
} else {
// operation is not void
successTypeDescriptor = subject.dafnyNameResolver.typeDescriptor(outputResolved.resolvedId());
TypeName nativeOutputType = preferNativeInterface(outputResolved, subject);
method
.addStatement(declareNativeOutputAndInvoke(operationName, nativeOutputType))
.addStatement(declareDafnyOutputAndConvert(outputResolved, subject))
.addStatement("return $T.create_Success($L, Error._typeDescriptor(), $L)",
DAFNY_RESULT_CLASS_NAME,
successTypeDescriptor,
DAFNY_OUTPUT);
.addStatement("return $L",
subject.dafnyNameResolver.createSuccess(
successTypeDescriptor,
CodeBlock.of(DAFNY_OUTPUT)));
}
// catch Errors in this Namespace
method
.nextControlFlow("catch ($T ex)",
ClassName.get(RuntimeException.class))
.addStatement("return $T.create_Failure($L, Error._typeDescriptor(), $T.Error(ex))",
DAFNY_RESULT_CLASS_NAME, successTypeDescriptor, shimLibrary.toDafnyClassName)
.addStatement("return $L",
subject.dafnyNameResolver.createFailure(
successTypeDescriptor,
CodeBlock.of("$T.Error(ex)", shimLibrary.toDafnyClassName)))
.endControlFlow();
return method.build();
}
Expand Down
4 changes: 2 additions & 2 deletions ...odegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV1.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@

public class AwsSdkDafnyV1 extends Dafny {

public AwsSdkDafnyV1(ServiceShape serviceShape, Model model) {
super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V1);
public AwsSdkDafnyV1(ServiceShape serviceShape, Model model, String dafnyVersion) {
super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V1, dafnyVersion);
}

@Override
Expand Down
4 changes: 2 additions & 2 deletions ...odegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/AwsSdkDafnyV2.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@

public class AwsSdkDafnyV2 extends Dafny {

public AwsSdkDafnyV2(ServiceShape serviceShape, Model model) {
super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V2);
public AwsSdkDafnyV2(ServiceShape serviceShape, Model model, String dafnyVersion) {
super(packageNameForServiceShape(serviceShape), model, serviceShape, CodegenSubject.AwsSdkVersion.V2, dafnyVersion);
}

@Override
Expand Down
1 change: 1 addition & 0 deletions ...ny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@

public class Constants {
public static final ShapeId SMITHY_API_UNIT = ShapeId.fromParts("smithy.api", "Unit");
public static final ClassName DAFNY_OPTION_CLASS_NAME = ClassName.get("Wrappers_Compile", "Option");
public static final ClassName DAFNY_RESULT_CLASS_NAME = ClassName.get("Wrappers_Compile", "Result");
public static final ClassName DAFNY_TUPLE0_CLASS_NAME = ClassName.get("dafny", "Tuple0");
public static final ClassName DAFNY_TYPE_DESCRIPTOR_CLASS_NAME = ClassName.get("dafny", "TypeDescriptor");
Expand Down
Loading

0 comments on commit a116040

Please sign in to comment.