Skip to content

Commit 77aeeb1

Browse files
texastonyseebees
texastony
and
seebees
authored
feat(Java): local service test (#196)
Co-authored-by: seebees <[email protected]>
1 parent bab5046 commit 77aeeb1

File tree

40 files changed

+839
-239
lines changed

40 files changed

+839
-239
lines changed

‎.github/workflows/test_models_java_tests.yml

+3-3
Original file line numberDiff line numberDiff line change
@@ -15,14 +15,14 @@ jobs:
1515
TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
1616
# TestModels/Aggregate,
1717
# TestModels/AggregateReferences,
18-
# TestModels/Constraints,
18+
TestModels/Constraints,
1919
# TestModels/Constructor,
2020
# TestModels/Dependencies,
2121
# TestModels/Errors,
22-
# TestModels/Extendable,
22+
TestModels/Extendable,
2323
# TestModels/Extern,
2424
# TestModels/Refinement,
25-
# TestModels/Resource,
25+
TestModels/Resource,
2626
# TestModels/SimpleTypes/BigDecimal,
2727
# TestModels/SimpleTypes/BigInteger,
2828
# TestModels/SimpleTypes/SimpleBlob,

‎.github/workflows/test_models_net_tests.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ jobs:
1515
TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
1616
TestModels/Aggregate,
1717
# TestModels/AggregateReferences,
18-
# TestModels/Constraints,
18+
TestModels/Constraints,
1919
TestModels/Constructor,
2020
TestModels/Dependencies,
2121
TestModels/Errors,

‎TestModels/Constraints/Model/Constraints.smithy

+7-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ service SimpleConstraints {
88
version: "2021-11-01",
99
resources: [],
1010
operations: [ GetConstraints ],
11-
errors: [],
11+
errors: [ SimpleConstraintsException ],
1212
}
1313

1414
structure SimpleConstraintsConfig {}
@@ -156,3 +156,9 @@ string Utf8Bytes
156156
list ListOfUtf8Bytes {
157157
member: Utf8Bytes
158158
}
159+
160+
@error("client")
161+
structure SimpleConstraintsException {
162+
@required
163+
message: String,
164+
}

‎TestModels/Constraints/runtimes/java/build.gradle.kts

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
tasks.wrapper {
2+
gradleVersion = "7.6"
3+
}
4+
5+
plugins {
6+
`java-library`
7+
`maven-publish`
8+
}
9+
10+
group = "simple"
11+
version = "1.0-SNAPSHOT"
12+
description = "Constraints"
13+
14+
java {
15+
toolchain.languageVersion.set(JavaLanguageVersion.of(8))
16+
sourceSets["main"].java {
17+
srcDir("src/main/java")
18+
srcDir("src/main/dafny-generated")
19+
srcDir("src/main/smithy-generated")
20+
}
21+
sourceSets["test"].java {
22+
srcDir("src/test/java")
23+
srcDir("src/test/dafny-generated")
24+
}
25+
}
26+
27+
repositories {
28+
mavenCentral()
29+
mavenLocal()
30+
}
31+
32+
dependencies {
33+
implementation("dafny.lang:DafnyRuntime:3.10.0")
34+
implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
35+
implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
36+
}
37+
38+
publishing {
39+
publications.create<MavenPublication>("maven") {
40+
groupId = "simple"
41+
artifactId = "Constraints"
42+
from(components["java"])
43+
}
44+
repositories { mavenLocal() }
45+
}
46+
47+
tasks.withType<JavaCompile>() {
48+
options.encoding = "UTF-8"
49+
}
50+
51+
tasks {
52+
register("runTests", JavaExec::class.java) {
53+
mainClass.set("TestsFromDafny")
54+
classpath = sourceSets["test"].runtimeClasspath
55+
}
56+
}

‎TestModels/Constraints/runtimes/java/src/main/java/Dafny/Simple/Constraints/Types/__default.java

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
package Dafny.Simple.Constraints.Types;
2+
3+
public class __default extends _ExternBase___default {
4+
}

‎TestModels/Constraints/runtimes/java/src/main/java/Dafny/Simple/Constraints/__default.java

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
package Dafny.Simple.Constraints;
2+
3+
public class __default extends _ExternBase___default{
4+
}

‎TestModels/Constraints/runtimes/java/src/test/java/Dafny/Simple/Constraints/Wrapped/__default.java

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package Dafny.Simple.Constraints.Wrapped;
2+
3+
import simple.constraints.SimpleConstraints;
4+
import simple.constraints.ToNative;
5+
import simple.constraints.wrapped.TestSimpleConstraints;
6+
7+
import Dafny.Simple.Constraints.Types.ISimpleConstraintsClient;
8+
import Dafny.Simple.Constraints.Types.SimpleConstraintsConfig;
9+
import Dafny.Simple.Constraints.Types.Error;
10+
import Wrappers_Compile.Result;
11+
12+
public class __default extends _ExternBase___default {
13+
public static Result<ISimpleConstraintsClient, Error> WrappedSimpleConstraints(SimpleConstraintsConfig config) {
14+
simple.constraints.model.SimpleConstraintsConfig wrappedConfig = ToNative.SimpleConstraintsConfig(config);
15+
simple.constraints.SimpleConstraints impl = SimpleConstraints.builder().SimpleConstraintsConfig(wrappedConfig).build();
16+
TestSimpleConstraints wrappedClient = TestSimpleConstraints.builder().impl(impl).build();
17+
return Result.create_Success(wrappedClient);
18+
}
19+
}

‎TestModels/Extendable/runtimes/java/build.gradle.kts

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
tasks.wrapper {
2+
gradleVersion = "7.6"
3+
}
4+
5+
plugins {
6+
`java-library`
7+
`maven-publish`
8+
}
9+
10+
group = "simple.extendable.resources"
11+
version = "1.0-SNAPSHOT"
12+
description = "SimpleExtendableResources"
13+
14+
java {
15+
toolchain.languageVersion.set(JavaLanguageVersion.of(8))
16+
sourceSets["main"].java {
17+
srcDir("src/main/java")
18+
srcDir("src/main/dafny-generated")
19+
srcDir("src/main/smithy-generated")
20+
}
21+
sourceSets["test"].java {
22+
srcDir("src/test/java")
23+
srcDir("src/test/dafny-generated")
24+
}
25+
}
26+
27+
repositories {
28+
mavenCentral()
29+
mavenLocal()
30+
}
31+
32+
dependencies {
33+
implementation("dafny.lang:DafnyRuntime:3.10.0")
34+
implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
35+
implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
36+
}
37+
38+
publishing {
39+
publications.create<MavenPublication>("maven") {
40+
groupId = group as String?
41+
artifactId = description
42+
from(components["java"])
43+
}
44+
repositories { mavenLocal() }
45+
}
46+
47+
tasks.withType<JavaCompile>() {
48+
options.encoding = "UTF-8"
49+
}
50+
51+
tasks {
52+
register("runTests", JavaExec::class.java) {
53+
mainClass.set("TestsFromDafny")
54+
classpath = sourceSets["test"].runtimeClasspath
55+
}
56+
}

‎TestModels/Extendable/runtimes/java/src/main/java/Dafny/Simple/Extendable/Resources/Types/__default.java

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
package Dafny.Simple.Extendable.Resources.Types;
2+
3+
public class __default extends _ExternBase___default {
4+
}

‎TestModels/Extendable/runtimes/java/src/main/java/Dafny/Simple/Extendable/Resources/__default.java

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
package Dafny.Simple.Extendable.Resources;
2+
3+
public class __default extends _ExternBase___default {
4+
}

‎TestModels/Extendable/runtimes/java/src/main/java/Simple/Extendable/Resources/NativeResource.java

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
package Simple.Extendable.Resources;
2+
3+
import simple.extendable.resources.IExtendableResource;
4+
import simple.extendable.resources.ToNative;
5+
import simple.extendable.resources.model.GetExtendableResourceDataInput;
6+
import simple.extendable.resources.model.GetExtendableResourceDataOutput;
7+
import simple.extendable.resources.model.GetExtendableResourceErrorsInput;
8+
import simple.extendable.resources.model.GetExtendableResourceErrorsOutput;
9+
10+
import java.util.Objects;
11+
12+
import ExtendableResource_Compile.ExtendableResource;
13+
14+
public class NativeResource implements IExtendableResource {
15+
private final IExtendableResource _impl;
16+
17+
public NativeResource(final IExtendableResource impl) {
18+
this._impl = impl;
19+
}
20+
21+
@Override
22+
public GetExtendableResourceDataOutput GetExtendableResourceData(GetExtendableResourceDataInput nativeValue) {
23+
return this._impl.GetExtendableResourceData(nativeValue);
24+
}
25+
26+
@Override
27+
public GetExtendableResourceErrorsOutput AlwaysModeledError(GetExtendableResourceErrorsInput nativeValue) {
28+
return this._impl.AlwaysModeledError(nativeValue);
29+
}
30+
31+
@Override
32+
public GetExtendableResourceErrorsOutput AlwaysMultipleErrors(GetExtendableResourceErrorsInput nativeValue) {
33+
return this._impl.AlwaysMultipleErrors(nativeValue);
34+
}
35+
36+
@Override
37+
public GetExtendableResourceErrorsOutput AlwaysOpaqueError(GetExtendableResourceErrorsInput nativeValue) {
38+
if (Objects.nonNull(nativeValue.value())) {
39+
throw new RuntimeException("Java Hard Coded Exception");
40+
}
41+
return this._impl.AlwaysOpaqueError(nativeValue);
42+
}
43+
44+
public static NativeResource NativeFactory() {
45+
ExtendableResource _nw2 = new ExtendableResource();
46+
_nw2.__ctor();
47+
IExtendableResource dafnyResource = ToNative.ExtendableResource(_nw2);
48+
return new NativeResource(dafnyResource);
49+
}
50+
}

‎TestModels/Extendable/runtimes/java/src/test/java/Dafny/Simple/Extendable/Resources/NativeResourceFactory/__default.java

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
package Dafny.Simple.Extendable.Resources.NativeResourceFactory;
2+
3+
import simple.extendable.resources.ToDafny;
4+
5+
import Dafny.Simple.Extendable.Resources.Types.IExtendableResource;
6+
import Simple.Extendable.Resources.NativeResource;
7+
8+
public class __default {
9+
public static IExtendableResource DafnyFactory() {
10+
return ToDafny.ExtendableResource(NativeResource.NativeFactory());
11+
}
12+
}

‎TestModels/Extendable/runtimes/java/src/test/java/Dafny/Simple/Extendable/Resources/Wrapped/__default.java

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
package Dafny.Simple.Extendable.Resources.Wrapped;
2+
3+
import simple.extendable.resources.SimpleExtendableResources;
4+
import simple.extendable.resources.ToNative;
5+
import simple.extendable.resources.wrapped.TestSimpleExtendableResources;
6+
7+
import Dafny.Simple.Extendable.Resources.Types.ISimpleExtendableResourcesClient;
8+
import Dafny.Simple.Extendable.Resources.Types.Error;
9+
10+
import Dafny.Simple.Extendable.Resources.Types.SimpleExtendableResourcesConfig;
11+
import Wrappers_Compile.Result;
12+
13+
public class __default extends _ExternBase___default {
14+
public static Result<ISimpleExtendableResourcesClient, Error> WrappedSimpleExtendableResources(SimpleExtendableResourcesConfig config) {
15+
simple.extendable.resources.model.SimpleExtendableResourcesConfig wrappedConfig = ToNative.SimpleExtendableResourcesConfig(config);
16+
simple.extendable.resources.SimpleExtendableResources impl = SimpleExtendableResources.builder().SimpleExtendableResourcesConfig(wrappedConfig).build();
17+
TestSimpleExtendableResources wrappedClient = TestSimpleExtendableResources.builder().impl(impl).build();
18+
return Result.create_Success(wrappedClient);
19+
}
20+
}

‎TestModels/Extendable/runtimes/net/Extern/NativeResource.cs

+3-7
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@
55
using Dafny.Simple.Extendable.Resources;
66
using Dafny.Simple.Extendable.Resources.Types;
77
using Simple.Extendable.Resources;
8-
using TypeConversion = Simple.Extendable.Resources.TypeConversion;
98

109
namespace Simple.Extendable.Resources
1110
{
@@ -39,6 +38,7 @@ protected override GetExtendableResourceErrorsOutput _AlwaysOpaqueError(GetExten
3938
{
4039
throw new Exception(".NET Hard Coded Exception");
4140
}
41+
4242
return this._impl.AlwaysOpaqueError(input);
4343
}
4444

@@ -50,11 +50,7 @@ public static NativeResource NativeFactory()
5050
TypeConversion.FromDafny_N6_simple__N10_extendable__N9_resources__S27_ExtendableResourceReference(_nw2);
5151
return new NativeResource(dafnyResource);
5252
}
53-
54-
public static Dafny.Simple.Extendable.Resources.Types.IExtendableResource DafnyFactory()
55-
{
56-
return TypeConversion.ToDafny_N6_simple__N10_extendable__N9_resources__S27_ExtendableResourceReference(
57-
NativeFactory());
58-
}
5953
}
6054
}
55+
56+

‎TestModels/Extendable/runtimes/net/Extern/__default.cs

+12
Original file line numberDiff line numberDiff line change
@@ -28,3 +28,15 @@ Types._ISimpleExtendableResourcesConfig config
2828
}
2929
}
3030
}
31+
32+
namespace Dafny.Simple.Extendable.Resources.NativeResourceFactory
33+
{
34+
public partial class __default
35+
{
36+
public static Dafny.Simple.Extendable.Resources.Types.IExtendableResource DafnyFactory()
37+
{
38+
return TypeConversion.ToDafny_N6_simple__N10_extendable__N9_resources__S27_ExtendableResourceReference(
39+
NativeResource.NativeFactory());
40+
}
41+
}
42+
}

‎TestModels/Extendable/test/Helpers.dfy

+7-15
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ module TestHelpers {
8383
{
8484
expect errorOutput.Failure?;
8585
var actualError := errorOutput.PropagateFailure<Types.GetExtendableResourceErrorsOutput>().error;
86-
expect actualError.Opaque?
86+
expect actualError.Opaque?;
8787
// Opaque Errors SHOULD NOT be thrown by Dafny source.
8888
// (At least) Smithy-dotnet expects the obj
8989
// to be an Exception that it can throw.
@@ -92,14 +92,12 @@ module TestHelpers {
9292
// so we are NOT going to do that.
9393
// Therefore, we cannot constrain/test the value of obj
9494
// with pure Dafny.
95-
&& !(actualError.obj is ExtendableResource.OpaqueMessage);
96-
// For the curious,
97-
// in .NET, the obj will be a Native OpaqueError,
98-
// with the message:
99-
// "Opaque obj is not an Exception."
100-
// But we cannot test that here,
101-
// as we cannot call the TypeConversion method
102-
// from inside Dafny.
95+
// What is very odd is that
96+
// .NET cannot percieve OpaqueMessage (when using a Native Resource), but Java Can!
97+
// Put another way,
98+
// the next line is true for .NET and False for Java!
99+
// && !(actualError.obj is ExtendableResource.OpaqueMessage);
100+
// TODO: Determine why Java can pass OpaqueMessage check but .NET cannot?
103101
}
104102

105103
method CheckDafnyOpaqueError(
@@ -111,10 +109,4 @@ module TestHelpers {
111109
expect actualError.Opaque?
112110
&& (actualError.obj is ExtendableResource.OpaqueMessage);
113111
}
114-
115-
method {:extern "Simple.Extendable.Resources.NativeResource", "DafnyFactory"} DafnyFactory(
116-
) returns (
117-
output: Types.IExtendableResource
118-
)
119-
ensures output.ValidState() && fresh(output.History) && fresh(output.Modifies)
120112
}

‎TestModels/Extendable/test/NativeExtendableResourceTest.dfy

+2
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,14 @@
22
// SPDX-License-Identifier: Apache-2.0
33

44
include "./Helpers.dfy"
5+
include "./NativeResourceFactory.dfy"
56

67
module NativeExtendableResourceTest {
78
import ExtendableResource
89
import Types = SimpleExtendableResourcesTypes
910
import opened Wrappers
1011
import opened TestHelpers
12+
import opened NativeResourceFactory
1113

1214
method {:test} TestNativeResource()
1315
{

0 commit comments

Comments
 (0)