Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 73 additions & 0 deletions TestModels/Aggregate/runtimes/java/build.gradle.kts
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
import java.io.File
import java.io.FileInputStream
import java.util.Properties

tasks.wrapper {
gradleVersion = "7.6"
}

plugins {
`java-library`
`maven-publish`
}

var props = Properties().apply {
load(FileInputStream(File(rootProject.rootDir, "../../project.properties")))
}
var dafnyVersion = props.getProperty("dafnyVersion")

group = "simple"
version = "1.0-SNAPSHOT"
description = "Constraints"

java {
toolchain.languageVersion.set(JavaLanguageVersion.of(8))
sourceSets["main"].java {
srcDir("src/main/java")
srcDir("src/main/dafny-generated")
srcDir("src/main/smithy-generated")
}
sourceSets["test"].java {
srcDir("src/test/java")
srcDir("src/test/dafny-generated")
srcDir("src/test/smithy-generated")
}
}

repositories {
mavenCentral()
mavenLocal()
}

dependencies {
implementation("org.dafny:DafnyRuntime:${dafnyVersion}")
implementation("software.amazon.smithy.dafny:conversion:0.1.1")
implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
testImplementation("org.testng:testng:7.5")
}

publishing {
publications.create<MavenPublication>("maven") {
groupId = "simple"
artifactId = "Constraints"
from(components["java"])
}
repositories { mavenLocal() }
}

tasks.withType<JavaCompile>() {
options.encoding = "UTF-8"
}

tasks {
register("runTests", JavaExec::class.java) {
mainClass.set("TestsFromDafny")
classpath = sourceSets["test"].runtimeClasspath
}
}

tasks.named<Test>("test") {
useTestNG()
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
package simple.aggregate.internaldafny;

public class __default extends _ExternBase___default {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
package simple.aggregate.internaldafny.types;

public class __default extends _ExternBase___default {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
package simple.aggregate.internaldafny.wrapped;

import Wrappers_Compile.Result;
import simple.aggregate.SimpleAggregate;
import simple.aggregate.ToNative;
import simple.aggregate.internaldafny.types.Error;
import simple.aggregate.internaldafny.types.ISimpleAggregateClient;
import simple.aggregate.internaldafny.types.SimpleAggregateConfig;
import simple.aggregate.wrapped.TestSimpleAggregate;

public class __default extends _ExternBase___default {

public static Result<
ISimpleAggregateClient,
Error
> WrappedSimpleAggregate(SimpleAggregateConfig config) {
simple.aggregate.model.SimpleAggregateConfig wrappedConfig =
ToNative.SimpleAggregateConfig(config);
simple.aggregate.SimpleAggregate impl = SimpleAggregate
.builder()
.SimpleAggregateConfig(wrappedConfig)
.build();
TestSimpleAggregate wrappedClient = TestSimpleAggregate
.builder()
.impl(impl)
.build();
return simple.aggregate.internaldafny.__default.CreateSuccessOfClient(
wrappedClient
);
}
}
64 changes: 60 additions & 4 deletions TestModels/Aggregate/test/SimpleAggregateImplTest.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,19 @@ module SimpleAggregateImplTest {
import opened SimpleAggregateTypes
import opened Wrappers
method{:test} GetAggregate(){
var client :- expect SimpleAggregate.SimpleAggregate();
TestGetAggregate(client);
TestGetAggregateKnownValue(client);
var client :- expect SimpleAggregate.SimpleAggregate();
TestAggregate(client);
}

method TestAggregate(client: ISimpleAggregateClient)
requires client.ValidState()
modifies client.Modifies
ensures client.ValidState()
{
TestGetAggregate(client);
TestGetAggregateKnownValue(client);
TestEmptyAggregate(client);
TestNoneAggregate(client);
}

method TestGetAggregate(client: ISimpleAggregateClient)
Expand Down Expand Up @@ -37,7 +47,7 @@ module SimpleAggregateImplTest {
}

method TestGetAggregateKnownValue(client: ISimpleAggregateClient)
requires client.ValidState()
requires client.ValidState()
modifies client.Modifies
ensures client.ValidState()
{
Expand All @@ -59,4 +69,50 @@ module SimpleAggregateImplTest {
expect ret.nestedStructure.UnwrapOr(NestedStructure(stringStructure := Some(StringStructure(value := Some(""))))) == nestedStructure;
print ret;
}

method TestEmptyAggregate(client: ISimpleAggregateClient)
requires client.ValidState()
modifies client.Modifies
ensures client.ValidState()
{
var stringList := [];
var simpleStringMap := map[];
var structureList :=[];
var simpleIntegerMap := map[];
var nestedStructure := NestedStructure(stringStructure := Some(StringStructure(value := Some("Nested"))));
var ret :- expect client.GetAggregate(GetAggregateInput(simpleIntegerMap := Some(simpleIntegerMap),
simpleStringMap := Some(simpleStringMap),
simpleStringList := Some(stringList),
structureList := Some(structureList),
nestedStructure := Some(nestedStructure))
);
expect ret.simpleStringList == Some(stringList);
expect ret.structureList == Some(structureList);
expect ret.simpleStringMap == Some(simpleStringMap);
expect ret.simpleIntegerMap == Some(simpleIntegerMap);
expect ret.nestedStructure.UnwrapOr(NestedStructure(stringStructure := Some(StringStructure(value := Some(""))))) == nestedStructure;
print ret;
}

method TestNoneAggregate(client: ISimpleAggregateClient)
requires client.ValidState()
modifies client.Modifies
ensures client.ValidState()
{

var ret :- expect client.GetAggregate(
GetAggregateInput(
simpleIntegerMap := None,
simpleStringMap := None,
simpleStringList := None,
structureList := None,
nestedStructure := None)
);
expect ret.simpleStringList == None;
expect ret.structureList == None;
expect ret.simpleStringMap == None;
expect ret.simpleIntegerMap == None;
expect ret.nestedStructure == None;
print ret;
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ module WrappedSimpleTypesStringTest {
import opened Wrappers
method{:test} GetAggregate() {
var client :- expect WrappedSimpleAggregateService.WrappedSimpleAggregate();
SimpleAggregateImplTest.TestGetAggregate(client);
SimpleAggregateImplTest.TestGetAggregateKnownValue(client);
SimpleAggregateImplTest.TestAggregate(client);
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,6 @@ class JavaTestModels extends TestModelTest {
private static final Set<String> DISABLED_TESTS = new HashSet<>();

static {
DISABLED_TESTS.add("Aggregate");
DISABLED_TESTS.add("AggregateReferences");
DISABLED_TESTS.add("CallingAWSSDKFromLocalService");
DISABLED_TESTS.add("Constructor");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,10 @@ protected CodeBlock memberAssign(
);
CodeBlock isSetCheck = isNullCheck;
Shape targetShape = subject.model.expectShape(memberShape.getTarget());
if (Constants.LIST_MAP_SET_SHAPE_TYPES.contains(targetShape.getType())) {
if (
Constants.LIST_MAP_SET_SHAPE_TYPES.contains(targetShape.getType())
&& AwsSdkNameResolverHelpers.isInAwsSdkNamespace(memberShape.getTarget())
) {
isSetCheck = CodeBlock.of("($L && $L.size() > 0)", isNullCheck, inputVar);
}
CodeBlock typeDescriptor = subject.dafnyNameResolver.typeDescriptor(
Expand Down
Loading