Skip to content

Commit

Permalink
fix(Java): un-wrap extended resources (#215)
Browse files Browse the repository at this point in the history
Co-authored-by: seebees <ryanemer@amazon.com>
Co-authored-by: Lucas McDonald <lucasmcdonald3@gmail.com>
  • Loading branch information
3 people authored Apr 5, 2023
1 parent 790bd4c commit 4787373
Show file tree
Hide file tree
Showing 7 changed files with 76 additions and 31 deletions.
11 changes: 11 additions & 0 deletions TestModels/Extendable/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,14 @@ NAMESPACE=simple.extendable.resources

format_net:
pushd runtimes/net && dotnet format && popd

clean:
rm -f $(LIBRARY_ROOT)/Model/*Types.dfy $(LIBRARY_ROOT)/Model/*TypesWrapped.dfy
rm -f $(LIBRARY_ROOT)/runtimes/net/ImplementationFromDafny.cs
rm -f $(LIBRARY_ROOT)/runtimes/net/tests/TestFromDafny.cs
rm -rf $(LIBRARY_ROOT)/TestResults
rm -rf $(LIBRARY_ROOT)/runtimes/net/Generated $(LIBRARY_ROOT)/runtimes/net/bin $(LIBRARY_ROOT)/runtimes/net/obj
rm -rf $(LIBRARY_ROOT)/runtimes/net/tests/bin $(LIBRARY_ROOT)/runtimes/net/tests/obj
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated
Original file line number Diff line number Diff line change
Expand Up @@ -4,17 +4,37 @@
import simple.extendable.resources.ToNative;
import simple.extendable.resources.wrapped.TestSimpleExtendableResources;

import Dafny.Simple.Extendable.Resources.Types.IExtendableResource;
import Dafny.Simple.Extendable.Resources.Types.ISimpleExtendableResourcesClient;
import Dafny.Simple.Extendable.Resources.Types.Error;

import Dafny.Simple.Extendable.Resources.Types.SimpleExtendableResourcesConfig;
import Simple.Extendable.Resources.NativeResource;
import Wrappers_Compile.Result;

import static Dafny.Simple.Extendable.Resources.NativeResourceFactory.__default.DafnyFactory;

public class __default extends _ExternBase___default {
public static Result<ISimpleExtendableResourcesClient, Error> WrappedSimpleExtendableResources(SimpleExtendableResourcesConfig config) {
TestUnwrapExtendable();
simple.extendable.resources.model.SimpleExtendableResourcesConfig wrappedConfig = ToNative.SimpleExtendableResourcesConfig(config);
simple.extendable.resources.SimpleExtendableResources impl = SimpleExtendableResources.builder().SimpleExtendableResourcesConfig(wrappedConfig).build();
TestSimpleExtendableResources wrappedClient = TestSimpleExtendableResources.builder().impl(impl).build();
return Result.create_Success(wrappedClient);
}

/**
* We have not developed the ability to call ToNative from Dafny source code at this time.
* But we need to test this un-wrapping, so this is written in native code until we figure that out.
*/
public static void TestUnwrapExtendable() {
IExtendableResource dafnyWrappingNativeWrappingDafny = DafnyFactory();
simple.extendable.resources.IExtendableResource nativeWrappingDafny = ToNative.ExtendableResource(dafnyWrappingNativeWrappingDafny);
if (!(nativeWrappingDafny instanceof NativeResource)) {
throw new AssertionError(
"Polymorph MUST generate conversion methods " +
"capable of wrapping & un-wrapping" +
"these native resources.");
}
}
}
26 changes: 7 additions & 19 deletions TestModels/dafny-dependencies/Model/traits.smithy
Original file line number Diff line number Diff line change
Expand Up @@ -53,25 +53,13 @@ structure dafnyUtf8Bytes {}

// A trait indicating that the resource may be implemented by native code (instead of Dafny code).
// i.e.: Users may author their own classes that implement and extend this resource.
// Polymorph will generate and utilize NativeWrappers for these resources.
// Polymorph MUST generate and utilize NativeWrappers for these resources.
// Polymorph MUST generate conversion methods capabale of wrapping & un-wrapping
// these native resources.
// i.e.: The wrapping MUST NOT be a one way door.
@trait(selector: "resource")
structure extendable {}

// A trait indicating that a structure is a members of a union
// and MUST NOT be used independently of the union.
// This is syntactic sugar for
// union Foo {
// Bar: structure Bar { baz: String }
// }
//
// It is used like this
// union Foo {
// Bar: Bar
// }
// structure Bar { baz: String }
// This is especilay useful in Dafny.
// Because it results in a single datatype
// whos constructors are the member structures.
// datatypes Foo = Bar( baz: String )
@trait(selector: "structure")
structure datatypeUnion {}
// A trait to indicate that a resource stores local state
@trait(selector: "resource")
structure mutableLocalState {}
11 changes: 7 additions & 4 deletions TestModels/dafny-dependencies/Model/update.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
# Example: ./update.sh ~/workplace/private-aws-encryption-sdk-dafny-staging v4-seperate-modules
ESDK_PATH="$1"
ESDK_BRANCH="$2"
MDL_SRC_DIRS=('aws-sdk')
MDL_SRC_FILES=('traits.smithy')

set -e

Expand All @@ -12,13 +12,16 @@ if [ "$2" ]; then
git checkout "$ESDK_BRANCH"
git pull
fi

ESDK_COMMIT_SHA=$(git rev-parse --short HEAD)
echo -e "ESDK Commit Sha is $ESDK_COMMIT_SHA"
cd -
for DIRECTORY in "${MDL_SRC_DIRS[@]}"; do
cp -r "$ESDK_PATH/model/$DIRECTORY" "."
git add "$DIRECTORY"

for MDL_FILE in "${MDL_SRC_FILES[@]}"; do
cp "$ESDK_PATH/model/$MDL_FILE" "."
git add "$MDL_FILE"
done

printf "Pulled Files for ESDK's model and staged for commit. \n"
printf "Suggest executing: \n"
COMMIT_MSG="chore(tests): Update ESDK's Model to $ESDK_COMMIT_SHA"
Expand Down
1 change: 1 addition & 0 deletions codegen/gradle.properties
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
smithyVersion=1.28.1
smithyGradleVersion=0.6.0
org.gradle.warning.mode=none
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,11 @@
import software.amazon.polymorph.traits.PositionalTrait;
import software.amazon.polymorph.utils.ModelUtils;
import software.amazon.polymorph.smithyjava.nameresolver.Dafny;
import software.amazon.polymorph.smithyjava.nameresolver.Native;
import software.amazon.polymorph.smithyjava.unmodeled.CollectionOfErrors;
import software.amazon.polymorph.smithyjava.unmodeled.NativeError;
import software.amazon.polymorph.smithyjava.unmodeled.OpaqueError;
import software.amazon.polymorph.traits.ExtendableTrait;

import software.amazon.smithy.model.shapes.MemberShape;
import software.amazon.smithy.model.shapes.ResourceShape;
Expand Down Expand Up @@ -201,14 +203,30 @@ protected MethodSpec positionalStructure(StructureShape structureShape) {

protected MethodSpec modeledResource(ResourceShape shape) {
final String methodName = capitalize(shape.getId().getName());
return MethodSpec
MethodSpec.Builder method = MethodSpec
.methodBuilder(methodName)
.addModifiers(PUBLIC_STATIC)
.addParameter(Dafny.interfaceForResource(shape), VAR_INPUT)
.returns(subject.nativeNameResolver.classNameForResource(shape))
.addStatement("return $L", subject.wrapWithShim(shape.getId(),
CodeBlock.of(VAR_INPUT)))
.build();
.returns(Native.classNameForInterfaceOrLocalService(shape, subject.sdkVersion));

if (shape.hasTrait(ExtendableTrait.class)) {
method
.beginControlFlow(
"if ($L instanceof $T.NativeWrapper)",
VAR_INPUT, subject.nativeNameResolver.classNameForResource(shape)
)
.addStatement(
"return (($T.NativeWrapper) $L)._impl",
subject.nativeNameResolver.classNameForResource(shape), VAR_INPUT
)
.endControlFlow();
}
return method
.addStatement(
"return $L",
subject.wrapWithShim(shape.getId(), CodeBlock.of(VAR_INPUT))
)
.build();
}

protected CodeBlock returnWithConversionCall(final MemberShape shape) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
import software.amazon.smithy.model.shapes.ResourceShape;

import static javax.lang.model.element.Modifier.FINAL;
import static javax.lang.model.element.Modifier.PRIVATE;
import static javax.lang.model.element.Modifier.PROTECTED;
import static javax.lang.model.element.Modifier.STATIC;

public class NativeWrapper extends ResourceShim {
Expand All @@ -37,9 +37,13 @@ TypeSpec nativeWrapper() {
ClassName className = className();
TypeSpec.Builder spec =TypeSpec
.classBuilder(className)
.addModifiers(PRIVATE, FINAL, STATIC)
// TODO: Verify that the nested class SHOULD BE `PROTECTED` instead of `PRIVATE`
// PR #215 or #196
.addModifiers(PROTECTED, FINAL, STATIC)
.addSuperinterface(Dafny.interfaceForResource(targetShape))
.addField(interfaceName, INTERFACE_FIELD, PRIVATE, FINAL)
// TODO: It MAYBE best to keep the INTERFACE_FIELD PRIVATE, rather than PROTECTED,
// and add getter method. PR #215 or #196
.addField(interfaceName, INTERFACE_FIELD, PROTECTED, FINAL)
.addMethod(nativeWrapperConstructor());
getOperationsForTarget().forEach(oShape -> {
spec.addMethod(operation(oShape));
Expand Down

0 comments on commit 4787373

Please sign in to comment.