Skip to content

Commit 118804b

Browse files
alex-chewrobin-aws
alex-chew
and
robin-aws
authored
feat: extract CodegenEngine (#212)
Co-authored-by: Robin Salkeld <[email protected]>
1 parent 955244d commit 118804b

File tree

36 files changed

+5383
-422
lines changed

36 files changed

+5383
-422
lines changed

‎.github/workflows/smithy-polymorph.yml

+13
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,19 @@ jobs:
2828
arguments: :smithy-dafny-codegen:test
2929
build-root-directory: codegen
3030

31+
# Required for building the SQS model
32+
- name: Locally cache smithy-dafny-codegen
33+
uses: gradle/gradle-build-action@v2
34+
with:
35+
arguments: :smithy-dafny-codegen:publishToMavenLocal
36+
build-root-directory: codegen
37+
38+
- name: Sanity-check SQS test model via plugin
39+
uses: gradle/gradle-build-action@v2
40+
with:
41+
arguments: build --info
42+
build-root-directory: TestModels/aws-sdks/sqs
43+
3144
- name: Execute codegen build
3245
uses: gradle/gradle-build-action@v2
3346
with:

‎.github/workflows/test_models_dafny_verification.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ jobs:
4040
TestModels/Union,
4141
TestModels/aws-sdks/ddb,
4242
TestModels/aws-sdks/kms,
43-
TestModels/aws-sdks/sqs,
43+
TestModels/aws-sdks/sqs-via-cli,
4444
]
4545
os: [ ubuntu-latest ]
4646
runs-on: ${{ matrix.os }}

‎.github/workflows/test_models_net_tests.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ jobs:
4040
TestModels/Union,
4141
TestModels/aws-sdks/ddb,
4242
TestModels/aws-sdks/kms,
43-
TestModels/aws-sdks/sqs,
43+
TestModels/aws-sdks/sqs-via-cli,
4444
]
4545
dotnet-version: [ '6.0.x' ]
4646
os: [ ubuntu-latest ]

‎TestModels/aws-sdks/sqs/Makefile renamed to ‎TestModels/aws-sdks/sqs-via-cli/Makefile

File renamed without changes.

‎TestModels/aws-sdks/sqs/Model/sqs.json renamed to ‎TestModels/aws-sdks/sqs-via-cli/Model/sqs.json

File renamed without changes.

‎TestModels/aws-sdks/sqs-via-cli/README.md

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
# AWS-SDK-SQS
2+
3+
This project builds a Dafny SDK for [AWS SQS](https://aws.amazon.com/sqs/).
4+
It is a copy of the `TestModels/aws-sdks/sqs` project,
5+
but it generates code using the older CLI instead of the newer Smithy build plugin.
6+
This project will eventually be removed entirely as the CLI is deprecated.
7+
For more details, please see `TestModels/aws-sdks/sqs/README.md`.
8+
9+
## Build
10+
11+
### .NET
12+
13+
1. Generate the Wrappers using `polymorph`
14+
```
15+
make polymorph_dafny polymorph_net
16+
```
17+
18+
2. Transpile the tests (and implementation) to the target runtime.
19+
```
20+
make transpile_net
21+
```
22+
23+
3. Generate the executable in the .NET and execute the tests
24+
```
25+
make test_net
26+
```

‎TestModels/aws-sdks/sqs-via-cli/runtimes/net/Extern/SQSClient.cs

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
using Amazon;
2+
using Amazon.SQS;
3+
using Wrappers_Compile;
4+
using Amazon.Runtime;
5+
using Com.Amazonaws.Sqs;
6+
7+
// This extern is identified in Dafny code
8+
// that refines the AWS SDK SQS Model
9+
namespace Dafny.Com.Amazonaws.Sqs
10+
{
11+
public partial class __default
12+
{
13+
14+
public static
15+
_IResult<
16+
Types.ISQSClient,
17+
Types._IError
18+
>
19+
SQSClient()
20+
{
21+
var client = new AmazonSQSClient();
22+
23+
return Result<
24+
Types.ISQSClient,
25+
Types._IError
26+
>
27+
.create_Success(new SQSShim(client));
28+
}
29+
}
30+
}

‎TestModels/aws-sdks/sqs-via-cli/runtimes/net/SQS.csproj

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
<Project Sdk="Microsoft.NET.Sdk">
2+
3+
<PropertyGroup>
4+
<ImplicitUsings>disable</ImplicitUsings>
5+
<Nullable>disable</Nullable>
6+
<TargetFrameworks>net6.0</TargetFrameworks>
7+
<LangVersion>10</LangVersion>
8+
<EnableDefaultCompileItems>false</EnableDefaultCompileItems>
9+
</PropertyGroup>
10+
11+
<ItemGroup>
12+
<PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
13+
<PackageReference Include="AWSSDK.Core" Version="3.7.100" />
14+
<PackageReference Include="AWSSDK.SQS" Version="3.7.100" />
15+
<!--
16+
System.Collections.Immutable can be removed once dafny.msbuild is updated with
17+
https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
18+
-->
19+
<PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
20+
<!-- Work around for dafny-lang/dafny/issues/1951; remove once resolved -->
21+
<PackageReference Include="System.ValueTuple" Version="4.5.0" />
22+
23+
<Compile Include="Extern/**/*.cs" />
24+
<Compile Include="Generated/**/*.cs" />
25+
<Compile Include="ImplementationFromDafny.cs" />
26+
</ItemGroup>
27+
28+
<ItemGroup>
29+
<ProjectReference Include="../../../../dafny-dependencies/StandardLibrary/runtimes/net/STD.csproj" />
30+
</ItemGroup>
31+
32+
</Project>

‎TestModels/aws-sdks/sqs-via-cli/runtimes/net/tests/TestSQS.csproj

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
<Project Sdk="Microsoft.NET.Sdk">
2+
3+
<PropertyGroup>
4+
<RootNamespace>TestSQS</RootNamespace>
5+
<ImplicitUsings>disable</ImplicitUsings>
6+
<Nullable>disable</Nullable>
7+
<TargetFrameworks>net6.0</TargetFrameworks>
8+
<LangVersion>10</LangVersion>
9+
<OutputType>Exe</OutputType>
10+
<EnableDefaultCompileItems>false</EnableDefaultCompileItems>
11+
</PropertyGroup>
12+
13+
<ItemGroup>
14+
<!--
15+
System.Collections.Immutable can be removed once dafny.msbuild is updated with
16+
https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
17+
-->
18+
<PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
19+
<!-- Work around for dafny-lang/dafny/issues/1951; remove once resolved -->
20+
<PackageReference Include="System.ValueTuple" Version="4.5.0" />
21+
22+
<ProjectReference Include="../SQS.csproj" />
23+
<Compile Include="TestsFromDafny.cs" />
24+
</ItemGroup>
25+
26+
</Project>

‎TestModels/aws-sdks/sqs-via-cli/src/Index.dfy

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
include "../Model/ComAmazonawsSqsTypes.dfy"
5+
6+
module {:extern "Dafny.Com.Amazonaws.Sqs"} Com.Amazonaws.Sqs refines AbstractComAmazonawsSqsService {
7+
8+
function method DefaultSQSClientConfigType() : SQSClientConfigType {
9+
SQSClientConfigType
10+
}
11+
12+
}

‎TestModels/aws-sdks/sqs-via-cli/test/TestComAmazonawsSqs.dfy

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
4+
// Something like this should work once we implement the
5+
// "dafny-client-codegen" Smithy build plugin and
6+
// configure it in smithy-build.json.
7+
// Note the lack of any manually-written code in the project!
8+
9+
include "../src/Index.dfy"
10+
11+
module TestComAmazonawsSqs {
12+
import Com.Amazonaws.Sqs
13+
import opened StandardLibrary.UInt
14+
import opened Wrappers
15+
16+
method {:test} BasicSanityTest()
17+
{
18+
var client :- expect Sqs.SQSClient();
19+
20+
var input := Sqs.Types.ListQueuesRequest(
21+
QueueNamePrefix := None,
22+
NextToken := None,
23+
MaxResults := None
24+
);
25+
var ret: Sqs.Types.ListQueuesResult :- expect client.ListQueues(input);
26+
27+
var ListQueuesResult(NextToken, QueueUrls) := ret;
28+
29+
// Just asserting the request is successful.
30+
// I could expect no queues but the test account might create some some day,
31+
// and I don't want this to be brittle.
32+
expect QueueUrls.Some?;
33+
}
34+
}

‎TestModels/aws-sdks/sqs/README.md

+12-24
Original file line numberDiff line numberDiff line change
@@ -14,38 +14,26 @@ You should be able to use the standard [projections](https://smithy.io/2.0/guide
1414
to trim-down or modify a model as needed before code generation instead.
1515

1616
## Build
17-
### .NET
18-
1. Generate the Wrappers using `polymorph`
19-
```
20-
make polymorph_dafny polymorph_net
21-
```
2217

23-
2. Transpile the tests (and implementation) to the target runtime.
24-
```
25-
make transpile_net
26-
```
18+
### Dafny + .NET
2719

28-
3. Generate the executable in the .NET and execute the tests
29-
```
30-
make test_net
31-
```
32-
33-
### Typescript
34-
35-
Building a typescript client for SQS (to demonstrate how the Smithy plugins work):
20+
Building a Dafny + .NET client for SQS (to demonstrate how the Smithy plugins work):
3621

3722
```
3823
gradle build
3924
```
4025

41-
The generated client package will appear in `build/smithyprojections/typescript-codegen`.
26+
The generated client package will appear in `build/smithyprojections/sqs/source/dafny-client-codegen`.
4227

4328
## Development
4429

45-
To implement https://github.com/awslabs/polymorph/issues/151, we want to provide a similar
30+
To implement <https://github.com/awslabs/polymorph/issues/151>, we provide a similar
4631
"dafny-client-codegen" Smithy plugin that can be configured in smithy-build.json as well.
47-
It should produce a fully-formed, ready-to-build project under
48-
`build/smithyprojections/dafny-client-codegen`.
49-
This probably means emitting a Makefile with a subset of what's currently in the `SharedMakefile.mk`.
50-
51-
The JSON configuration for this plugin will need to accept a list of target languages.
32+
It will produce a fully-formed, ready-to-build project
33+
under `build/smithyprojections/sqs/source/dafny-client-codegen`.
34+
This will mean emitting a Makefile with a subset of what's currently in the `SharedMakefile.mk`,
35+
or alternatively to emit a Dafny project file (TBD).
36+
37+
For now, the plugin generates the same code files as the older CLI,
38+
but does not generate all they build configuration files necessary to build the project.
39+
This shortcoming will be addressed in a future update.

‎TestModels/aws-sdks/sqs/build.gradle.kts

+7-2
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ dependencies {
1111
implementation("software.amazon.smithy:smithy-model:1.28.0")
1212
implementation("software.amazon.smithy:smithy-aws-traits:1.28.0")
1313
implementation("software.amazon.smithy:smithy-rules-engine:1.28.0")
14+
15+
// Must be built and published to the local Maven repo
16+
implementation("software.amazon.smithy.dafny:smithy-dafny-codegen:0.1.0")
1417
}
1518

1619
configure<software.amazon.smithy.gradle.SmithyExtension> {
@@ -22,10 +25,12 @@ configure<software.amazon.smithy.gradle.SmithyExtension> {
2225
tasks["jar"].enabled = false
2326

2427
buildscript {
28+
val smithyVersion: String by project
29+
2530
repositories {
2631
mavenCentral()
2732
}
2833
dependencies {
29-
classpath("software.amazon.smithy.typescript:smithy-aws-typescript-codegen:0.12.0")
34+
"classpath"("software.amazon.smithy:smithy-cli:$smithyVersion")
3035
}
31-
}
36+
}

‎TestModels/aws-sdks/sqs/gradle.properties

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
smithyVersion=1.27.2
2+
smithyGradleVersion=0.6.0
3+

‎TestModels/aws-sdks/sqs/gradle/wrapper/gradle-wrapper.jar

333 Bytes
Binary file not shown.

‎TestModels/aws-sdks/sqs/gradle/wrapper/gradle-wrapper.properties

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
distributionBase=GRADLE_USER_HOME
22
distributionPath=wrapper/dists
3-
distributionUrl=https\://services.gradle.org/distributions/gradle-7.2-bin.zip
3+
distributionUrl=https\://services.gradle.org/distributions/gradle-7.6-bin.zip
44
zipStoreBase=GRADLE_USER_HOME
55
zipStorePath=wrapper/dists

0 commit comments

Comments
 (0)