diff --git a/.github/workflows/smithy-polymorph.yml b/.github/workflows/smithy-polymorph.yml index 164ea5880..8b1782d43 100644 --- a/.github/workflows/smithy-polymorph.yml +++ b/.github/workflows/smithy-polymorph.yml @@ -26,7 +26,7 @@ jobs: - name: Setup Maven Action uses: s4u/setup-maven-action@v1.7.0 with: - java-version: 8 + java-version: '17' maven-version: 3.8.7 # Java DafnyRuntime is not published to maven, @@ -49,8 +49,14 @@ jobs: arguments: publishToMavenLocal build-root-directory: dafny-java-conversion - - name: Execute tests + - name: Execute smithy-polymorph tests uses: gradle/gradle-build-action@v2 with: arguments: test build-root-directory: smithy-polymorph + + - name: Execute smithy-dafny-codegen tests + uses: gradle/gradle-build-action@v2 + with: + arguments: :smithy-dafny-codegen:test + build-root-directory: codegen diff --git a/codegen/.gitattributes b/codegen/.gitattributes new file mode 100644 index 000000000..097f9f98d --- /dev/null +++ b/codegen/.gitattributes @@ -0,0 +1,9 @@ +# +# https://help.github.com/articles/dealing-with-line-endings/ +# +# Linux start script should use lf +/gradlew text eol=lf + +# These are Windows script files and should use crlf +*.bat text eol=crlf + diff --git a/codegen/.gitignore b/codegen/.gitignore new file mode 100644 index 000000000..249d1652e --- /dev/null +++ b/codegen/.gitignore @@ -0,0 +1,22 @@ +# IntelliJ +.idea/ +*.iml +*.iws + +# Mac +.DS_Store + +# Maven +target/ +**/dependency-reduced-pom.xml + +# Gradle +/.gradle +build/ +*/out/ +*/*/out/ +wrapper/ +.attach_pid* + +# VS Code +.vscode/* diff --git a/codegen/LICENSE b/codegen/LICENSE new file mode 100644 index 000000000..261eeb9e9 --- /dev/null +++ b/codegen/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/codegen/NOTICE b/codegen/NOTICE new file mode 100644 index 000000000..9b9b17844 --- /dev/null +++ b/codegen/NOTICE @@ -0,0 +1,5 @@ +Smithy Dafny +Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + +This product includes software developed by +Amazon Technologies, Inc (http://www.amazon.com/). diff --git a/codegen/README.md b/codegen/README.md new file mode 100644 index 000000000..20c0a39c8 --- /dev/null +++ b/codegen/README.md @@ -0,0 +1,22 @@ +# smithy-dafny-codegen + +This library supports the standard Smithy workflow +for generating a Dafny client for a given Smithy model, +as described in the +[Smithy codegen docs](https://smithy.io/2.0/guides/using-code-generation/generating-a-client.html). +For now the library will only support AWS service models, +since the implementation will generate both Dafny code and target language code +to wrap existing AWS SDKs. + +*WARNING: All internal and external interfaces are considered unstable and subject to change without notice.* + +The file layout of the library follows the +[Codegen repo layout](https://smithy.io/2.0/guides/building-codegen/creating-codegen-repo.html#codegen-repo-layout) +described in the Smithy documentation. + +Most configuration (e.g. `config`) and build files (e.g. `build.gradle.kts`) +were adapted from the corresponding files in the +[smithy-typescript](https://github.com/awslabs/smithy-typescript) +and/or +[smithy-go](https://github.com/aws/smithy-go/tree/main/codegen) +repositories. diff --git a/codegen/build.gradle.kts b/codegen/build.gradle.kts new file mode 100644 index 000000000..40f99aef0 --- /dev/null +++ b/codegen/build.gradle.kts @@ -0,0 +1,244 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +plugins { + `java-library` + `maven-publish` + signing + checkstyle + jacoco + id("com.github.spotbugs") version "4.7.1" + id("io.codearte.nexus-staging") version "0.30.0" +} + +allprojects { + group = "software.amazon.smithy.dafny" + version = "0.1.0" +} + +// The root project doesn't produce a JAR. +tasks["jar"].enabled = false + +// Load the Sonatype user/password for use in publishing tasks. +val sonatypeUser: String? by project +val sonatypePassword: String? by project + +/* + * Sonatype Staging Finalization + * ==================================================== + * + * When publishing to Maven Central, we need to close the staging + * repository and release the artifacts after they have been + * validated. This configuration is for the root project because + * it operates at the "group" level. + */ +if (sonatypeUser != null && sonatypePassword != null) { + apply(plugin = "io.codearte.nexus-staging") + + nexusStaging { + packageGroup = "software.amazon" + stagingProfileId = null // TODO + + username = sonatypeUser + password = sonatypePassword + } +} + +repositories { + mavenLocal() + mavenCentral() +} + +subprojects { + val subproject = this + + /* + * Java + * ==================================================== + */ + if (subproject.name != "smithy-dafny-codegen-test") { + apply(plugin = "java-library") + + java { + sourceCompatibility = JavaVersion.VERSION_17 + targetCompatibility = JavaVersion.VERSION_17 + } + + tasks.withType { + options.encoding = "UTF-8" + } + + // Use Junit5's test runner. + tasks.withType { + useJUnitPlatform() + } + + // Apply junit 5 and hamcrest test dependencies to all java projects. + dependencies { + testImplementation("org.junit.jupiter:junit-jupiter-api:5.9.2") + testImplementation("org.junit.jupiter:junit-jupiter-engine:5.9.2") + testImplementation("org.junit.jupiter:junit-jupiter-params:5.9.2") + testImplementation("org.hamcrest:hamcrest:2.2") + } + + // Reusable license copySpec + val licenseSpec = copySpec { + from("${project.rootDir}/LICENSE") + from("${project.rootDir}/NOTICE") + } + + // Set up tasks that build source and javadoc jars. + tasks.register("sourcesJar") { + metaInf.with(licenseSpec) + from(sourceSets.main.get().allJava) + archiveClassifier.set("sources") + } + + tasks.register("javadocJar") { + metaInf.with(licenseSpec) + from(tasks.javadoc) + archiveClassifier.set("javadoc") + } + + // Configure jars to include license related info + tasks.jar { + metaInf.with(licenseSpec) + inputs.property("moduleName", subproject.extra["moduleName"]) + manifest { + attributes["Automatic-Module-Name"] = subproject.extra["moduleName"] + } + } + + // Always run javadoc after build. + tasks["build"].finalizedBy(tasks["javadoc"]) + + /* + * Maven + * ==================================================== + */ + apply(plugin = "maven-publish") + apply(plugin = "signing") + + repositories { + mavenLocal() + mavenCentral() + } + + publishing { + repositories { + mavenCentral { + url = uri("https://aws.oss.sonatype.org/service/local/staging/deploy/maven2/") + credentials { + username = sonatypeUser + password = sonatypePassword + } + } + } + + publications { + create("mavenJava") { + from(components["java"]) + + // Ship the source and javadoc jars. + artifact(tasks["sourcesJar"]) + artifact(tasks["javadocJar"]) + + // Include extra information in the POMs. + afterEvaluate { + pom { + name.set(subproject.extra["displayName"].toString()) + description.set(subproject.description) + url.set("https://github.com/awslabs/smithy") + licenses { + license { + name.set("Apache License 2.0") + url.set("http://www.apache.org/licenses/LICENSE-2.0.txt") + distribution.set("repo") + } + } + developers { + developer { + id.set("smithy") + name.set("Smithy") + organization.set("Amazon Web Services") + organizationUrl.set("https://aws.amazon.com") + roles.add("developer") + } + } + scm { + url.set("https://github.com/awslabs/smithy.git") + } + } + } + } + } + } + + // Don't sign the artifacts if we didn't get a key and password to use. + val signingKey: String? by project + val signingPassword: String? by project + if (signingKey != null && signingPassword != null) { + signing { + useInMemoryPgpKeys(signingKey, signingPassword) + sign(publishing.publications["mavenJava"]) + } + } + + /* + * CheckStyle + * ==================================================== + */ + apply(plugin = "checkstyle") + + tasks["checkstyleTest"].enabled = false + + /* + * Tests + * ==================================================== + * + * Configure the running of tests. + */ + // Log on passed, skipped, and failed test events if the `-Plog-tests` property is set. + if (project.hasProperty("log-tests")) { + tasks.test { + testLogging.events("passed", "skipped", "failed") + } + } + + /* + * Code coverage + * ==================================================== + */ + apply(plugin = "jacoco") + + // Always run the jacoco test report after testing. + tasks["test"].finalizedBy(tasks["jacocoTestReport"]) + + // Configure jacoco to generate an HTML report. + tasks.jacocoTestReport { + reports { + xml.isEnabled = false + csv.isEnabled = false + html.destination = file("$buildDir/reports/jacoco") + } + } + + /* + * Spotbugs + * ==================================================== + */ + apply(plugin = "com.github.spotbugs") + + // We don't need to lint tests. + tasks["spotbugsTest"].enabled = false + + // Configure the bug filter for spotbugs. + spotbugs { + setEffort("max") + val excludeFile = File("${project.rootDir}/config/spotbugs/filter.xml") + if (excludeFile.exists()) { + excludeFilter.set(excludeFile) + } + } + } +} diff --git a/codegen/config/checkstyle/checkstyle.xml b/codegen/config/checkstyle/checkstyle.xml new file mode 100644 index 000000000..9e6f3b27c --- /dev/null +++ b/codegen/config/checkstyle/checkstyle.xml @@ -0,0 +1,197 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/codegen/config/checkstyle/suppressions.xml b/codegen/config/checkstyle/suppressions.xml new file mode 100644 index 000000000..71a9b4e9d --- /dev/null +++ b/codegen/config/checkstyle/suppressions.xml @@ -0,0 +1,21 @@ + + + + + + diff --git a/codegen/config/spotbugs/filter.xml b/codegen/config/spotbugs/filter.xml new file mode 100644 index 000000000..e88959a97 --- /dev/null +++ b/codegen/config/spotbugs/filter.xml @@ -0,0 +1,27 @@ + + + + + + + + + + + + + + diff --git a/codegen/gradle.properties b/codegen/gradle.properties new file mode 100644 index 000000000..04885b86c --- /dev/null +++ b/codegen/gradle.properties @@ -0,0 +1,2 @@ +smithyVersion=1.27.2 +smithyGradleVersion=0.6.0 diff --git a/codegen/gradle/wrapper/gradle-wrapper.jar b/codegen/gradle/wrapper/gradle-wrapper.jar new file mode 100644 index 000000000..943f0cbfa Binary files /dev/null and b/codegen/gradle/wrapper/gradle-wrapper.jar differ diff --git a/codegen/gradle/wrapper/gradle-wrapper.properties b/codegen/gradle/wrapper/gradle-wrapper.properties new file mode 100644 index 000000000..f398c33c4 --- /dev/null +++ b/codegen/gradle/wrapper/gradle-wrapper.properties @@ -0,0 +1,6 @@ +distributionBase=GRADLE_USER_HOME +distributionPath=wrapper/dists +distributionUrl=https\://services.gradle.org/distributions/gradle-7.6-bin.zip +networkTimeout=10000 +zipStoreBase=GRADLE_USER_HOME +zipStorePath=wrapper/dists diff --git a/codegen/gradlew b/codegen/gradlew new file mode 100755 index 000000000..65dcd68d6 --- /dev/null +++ b/codegen/gradlew @@ -0,0 +1,244 @@ +#!/bin/sh + +# +# Copyright © 2015-2021 the original authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +# + +############################################################################## +# +# Gradle start up script for POSIX generated by Gradle. +# +# Important for running: +# +# (1) You need a POSIX-compliant shell to run this script. If your /bin/sh is +# noncompliant, but you have some other compliant shell such as ksh or +# bash, then to run this script, type that shell name before the whole +# command line, like: +# +# ksh Gradle +# +# Busybox and similar reduced shells will NOT work, because this script +# requires all of these POSIX shell features: +# * functions; +# * expansions «$var», «${var}», «${var:-default}», «${var+SET}», +# «${var#prefix}», «${var%suffix}», and «$( cmd )»; +# * compound commands having a testable exit status, especially «case»; +# * various built-in commands including «command», «set», and «ulimit». +# +# Important for patching: +# +# (2) This script targets any POSIX shell, so it avoids extensions provided +# by Bash, Ksh, etc; in particular arrays are avoided. +# +# The "traditional" practice of packing multiple parameters into a +# space-separated string is a well documented source of bugs and security +# problems, so this is (mostly) avoided, by progressively accumulating +# options in "$@", and eventually passing that to Java. +# +# Where the inherited environment variables (DEFAULT_JVM_OPTS, JAVA_OPTS, +# and GRADLE_OPTS) rely on word-splitting, this is performed explicitly; +# see the in-line comments for details. +# +# There are tweaks for specific operating systems such as AIX, CygWin, +# Darwin, MinGW, and NonStop. +# +# (3) This script is generated from the Groovy template +# https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt +# within the Gradle project. +# +# You can find Gradle at https://github.com/gradle/gradle/. +# +############################################################################## + +# Attempt to set APP_HOME + +# Resolve links: $0 may be a link +app_path=$0 + +# Need this for daisy-chained symlinks. +while + APP_HOME=${app_path%"${app_path##*/}"} # leaves a trailing /; empty if no leading path + [ -h "$app_path" ] +do + ls=$( ls -ld "$app_path" ) + link=${ls#*' -> '} + case $link in #( + /*) app_path=$link ;; #( + *) app_path=$APP_HOME$link ;; + esac +done + +# This is normally unused +# shellcheck disable=SC2034 +APP_BASE_NAME=${0##*/} +APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit + +# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. +DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"' + +# Use the maximum available, or set MAX_FD != -1 to use that value. +MAX_FD=maximum + +warn () { + echo "$*" +} >&2 + +die () { + echo + echo "$*" + echo + exit 1 +} >&2 + +# OS specific support (must be 'true' or 'false'). +cygwin=false +msys=false +darwin=false +nonstop=false +case "$( uname )" in #( + CYGWIN* ) cygwin=true ;; #( + Darwin* ) darwin=true ;; #( + MSYS* | MINGW* ) msys=true ;; #( + NONSTOP* ) nonstop=true ;; +esac + +CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar + + +# Determine the Java command to use to start the JVM. +if [ -n "$JAVA_HOME" ] ; then + if [ -x "$JAVA_HOME/jre/sh/java" ] ; then + # IBM's JDK on AIX uses strange locations for the executables + JAVACMD=$JAVA_HOME/jre/sh/java + else + JAVACMD=$JAVA_HOME/bin/java + fi + if [ ! -x "$JAVACMD" ] ; then + die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME + +Please set the JAVA_HOME variable in your environment to match the +location of your Java installation." + fi +else + JAVACMD=java + which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. + +Please set the JAVA_HOME variable in your environment to match the +location of your Java installation." +fi + +# Increase the maximum file descriptors if we can. +if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then + case $MAX_FD in #( + max*) + # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked. + # shellcheck disable=SC3045 + MAX_FD=$( ulimit -H -n ) || + warn "Could not query maximum file descriptor limit" + esac + case $MAX_FD in #( + '' | soft) :;; #( + *) + # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked. + # shellcheck disable=SC3045 + ulimit -n "$MAX_FD" || + warn "Could not set maximum file descriptor limit to $MAX_FD" + esac +fi + +# Collect all arguments for the java command, stacking in reverse order: +# * args from the command line +# * the main class name +# * -classpath +# * -D...appname settings +# * --module-path (only if needed) +# * DEFAULT_JVM_OPTS, JAVA_OPTS, and GRADLE_OPTS environment variables. + +# For Cygwin or MSYS, switch paths to Windows format before running java +if "$cygwin" || "$msys" ; then + APP_HOME=$( cygpath --path --mixed "$APP_HOME" ) + CLASSPATH=$( cygpath --path --mixed "$CLASSPATH" ) + + JAVACMD=$( cygpath --unix "$JAVACMD" ) + + # Now convert the arguments - kludge to limit ourselves to /bin/sh + for arg do + if + case $arg in #( + -*) false ;; # don't mess with options #( + /?*) t=${arg#/} t=/${t%%/*} # looks like a POSIX filepath + [ -e "$t" ] ;; #( + *) false ;; + esac + then + arg=$( cygpath --path --ignore --mixed "$arg" ) + fi + # Roll the args list around exactly as many times as the number of + # args, so each arg winds up back in the position where it started, but + # possibly modified. + # + # NB: a `for` loop captures its iteration list before it begins, so + # changing the positional parameters here affects neither the number of + # iterations, nor the values presented in `arg`. + shift # remove old arg + set -- "$@" "$arg" # push replacement arg + done +fi + +# Collect all arguments for the java command; +# * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of +# shell script including quotes and variable substitutions, so put them in +# double quotes to make sure that they get re-expanded; and +# * put everything else in single quotes, so that it's not re-expanded. + +set -- \ + "-Dorg.gradle.appname=$APP_BASE_NAME" \ + -classpath "$CLASSPATH" \ + org.gradle.wrapper.GradleWrapperMain \ + "$@" + +# Stop when "xargs" is not available. +if ! command -v xargs >/dev/null 2>&1 +then + die "xargs is not available" +fi + +# Use "xargs" to parse quoted args. +# +# With -n1 it outputs one arg per line, with the quotes and backslashes removed. +# +# In Bash we could simply go: +# +# readarray ARGS < <( xargs -n1 <<<"$var" ) && +# set -- "${ARGS[@]}" "$@" +# +# but POSIX shell has neither arrays nor command substitution, so instead we +# post-process each arg (as a line of input to sed) to backslash-escape any +# character that might be a shell metacharacter, then use eval to reverse +# that process (while maintaining the separation between arguments), and wrap +# the whole thing up as a single "set" statement. +# +# This will of course break if any of these variables contains a newline or +# an unmatched quote. +# + +eval "set -- $( + printf '%s\n' "$DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS" | + xargs -n1 | + sed ' s~[^-[:alnum:]+,./:=@_]~\\&~g; ' | + tr '\n' ' ' + )" '"$@"' + +exec "$JAVACMD" "$@" diff --git a/codegen/gradlew.bat b/codegen/gradlew.bat new file mode 100644 index 000000000..93e3f59f1 --- /dev/null +++ b/codegen/gradlew.bat @@ -0,0 +1,92 @@ +@rem +@rem Copyright 2015 the original author or authors. +@rem +@rem Licensed under the Apache License, Version 2.0 (the "License"); +@rem you may not use this file except in compliance with the License. +@rem You may obtain a copy of the License at +@rem +@rem https://www.apache.org/licenses/LICENSE-2.0 +@rem +@rem Unless required by applicable law or agreed to in writing, software +@rem distributed under the License is distributed on an "AS IS" BASIS, +@rem WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +@rem See the License for the specific language governing permissions and +@rem limitations under the License. +@rem + +@if "%DEBUG%"=="" @echo off +@rem ########################################################################## +@rem +@rem Gradle startup script for Windows +@rem +@rem ########################################################################## + +@rem Set local scope for the variables with windows NT shell +if "%OS%"=="Windows_NT" setlocal + +set DIRNAME=%~dp0 +if "%DIRNAME%"=="" set DIRNAME=. +@rem This is normally unused +set APP_BASE_NAME=%~n0 +set APP_HOME=%DIRNAME% + +@rem Resolve any "." and ".." in APP_HOME to make it shorter. +for %%i in ("%APP_HOME%") do set APP_HOME=%%~fi + +@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. +set DEFAULT_JVM_OPTS="-Xmx64m" "-Xms64m" + +@rem Find java.exe +if defined JAVA_HOME goto findJavaFromJavaHome + +set JAVA_EXE=java.exe +%JAVA_EXE% -version >NUL 2>&1 +if %ERRORLEVEL% equ 0 goto execute + +echo. +echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. +echo. +echo Please set the JAVA_HOME variable in your environment to match the +echo location of your Java installation. + +goto fail + +:findJavaFromJavaHome +set JAVA_HOME=%JAVA_HOME:"=% +set JAVA_EXE=%JAVA_HOME%/bin/java.exe + +if exist "%JAVA_EXE%" goto execute + +echo. +echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% +echo. +echo Please set the JAVA_HOME variable in your environment to match the +echo location of your Java installation. + +goto fail + +:execute +@rem Setup the command line + +set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar + + +@rem Execute Gradle +"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %* + +:end +@rem End local scope for the variables with windows NT shell +if %ERRORLEVEL% equ 0 goto mainEnd + +:fail +rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of +rem the _cmd.exe /c_ return code! +set EXIT_CODE=%ERRORLEVEL% +if %EXIT_CODE% equ 0 set EXIT_CODE=1 +if not ""=="%GRADLE_EXIT_CONSOLE%" exit %EXIT_CODE% +exit /b %EXIT_CODE% + +:mainEnd +if "%OS%"=="Windows_NT" endlocal + +:omega diff --git a/codegen/settings.gradle.kts b/codegen/settings.gradle.kts new file mode 100644 index 000000000..758b41074 --- /dev/null +++ b/codegen/settings.gradle.kts @@ -0,0 +1,14 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +rootProject.name = "smithy-dafny" +include(":smithy-dafny-codegen") +include(":smithy-dafny-codegen-test") + +pluginManagement { + repositories { + mavenLocal() + mavenCentral() + gradlePluginPortal() + } +} diff --git a/codegen/smithy-dafny-codegen-test/README.md b/codegen/smithy-dafny-codegen-test/README.md new file mode 100644 index 000000000..eb996fb83 --- /dev/null +++ b/codegen/smithy-dafny-codegen-test/README.md @@ -0,0 +1,3 @@ +# smithy-dafny-codegen-test + +This directory contains a test project used to exercise the code generator. diff --git a/codegen/smithy-dafny-codegen-test/build.gradle.kts b/codegen/smithy-dafny-codegen-test/build.gradle.kts new file mode 100644 index 000000000..908ae279e --- /dev/null +++ b/codegen/smithy-dafny-codegen-test/build.gradle.kts @@ -0,0 +1,37 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +extra["displayName"] = "Smithy :: Dafny :: Codegen :: Test" +extra["moduleName"] = "software.amazon.smithy.dafny.codegen.test" + +tasks["jar"].enabled = false + +val smithyVersion: String by project + +buildscript { + val smithyVersion: String by project + + repositories { + mavenCentral() + } + dependencies { + "classpath"("software.amazon.smithy:smithy-cli:$smithyVersion") + } +} + +plugins { + val smithyGradleVersion: String by project + + id("software.amazon.smithy").version(smithyGradleVersion) +} + +repositories { + mavenLocal() + mavenCentral() +} + +dependencies { + implementation(project(":smithy-dafny-codegen")) + implementation("software.amazon.smithy:smithy-waiters:$smithyVersion") + implementation("software.amazon.smithy:smithy-protocol-test-traits:$smithyVersion") +} diff --git a/codegen/smithy-dafny-codegen-test/model/main.smithy b/codegen/smithy-dafny-codegen-test/model/main.smithy new file mode 100644 index 000000000..1cebb3511 --- /dev/null +++ b/codegen/smithy-dafny-codegen-test/model/main.smithy @@ -0,0 +1,4 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +$version: "2" diff --git a/codegen/smithy-dafny-codegen-test/smithy-build.json b/codegen/smithy-dafny-codegen-test/smithy-build.json new file mode 100644 index 000000000..ff4c27ed0 --- /dev/null +++ b/codegen/smithy-dafny-codegen-test/smithy-build.json @@ -0,0 +1,6 @@ +{ + "version": "1.0", + "plugins": { + "_comment": "TODO" + } +} diff --git a/codegen/smithy-dafny-codegen/README.md b/codegen/smithy-dafny-codegen/README.md new file mode 100644 index 000000000..8f2e1e1a0 --- /dev/null +++ b/codegen/smithy-dafny-codegen/README.md @@ -0,0 +1,3 @@ +# smithy-dafny-codegen + +This directory contains the code generator implementation. diff --git a/codegen/smithy-dafny-codegen/build.gradle.kts b/codegen/smithy-dafny-codegen/build.gradle.kts new file mode 100644 index 000000000..c39815249 --- /dev/null +++ b/codegen/smithy-dafny-codegen/build.gradle.kts @@ -0,0 +1,27 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +description = "Generates Dafny code from Smithy models" +extra["displayName"] = "Smithy :: Dafny :: Codegen" +extra["moduleName"] = "software.amazon.smithy.dafny.codegen" + +val smithyVersion: String by project + +buildscript { + val smithyVersion: String by project + + repositories { + mavenCentral() + } + dependencies { + "classpath"("software.amazon.smithy:smithy-cli:$smithyVersion") + } +} + +dependencies { + api("software.amazon.smithy:smithy-codegen-core:$smithyVersion") + api("software.amazon.smithy:smithy-model:$smithyVersion") + api("software.amazon.smithy:smithy-rules-engine:$smithyVersion") + api("software.amazon.smithy:smithy-waiters:$smithyVersion") + implementation("software.amazon.smithy:smithy-protocol-test-traits:$smithyVersion") +} diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPlugin.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPlugin.java new file mode 100644 index 000000000..04450a7fb --- /dev/null +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPlugin.java @@ -0,0 +1,19 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +package software.amazon.smithy.dafny.codegen; + +import software.amazon.smithy.build.PluginContext; +import software.amazon.smithy.build.SmithyBuildPlugin; + +public final class DafnyClientCodegenPlugin implements SmithyBuildPlugin { + @Override + public String getName() { + return "dafny-client-codegen"; + } + + @Override + public void execute(PluginContext context) { + // TODO generate code + } +} diff --git a/codegen/smithy-dafny-codegen/src/main/resources/META-INF/services/software.amazon.smithy.build.SmithyBuildPlugin b/codegen/smithy-dafny-codegen/src/main/resources/META-INF/services/software.amazon.smithy.build.SmithyBuildPlugin new file mode 100644 index 000000000..2e4e59c7d --- /dev/null +++ b/codegen/smithy-dafny-codegen/src/main/resources/META-INF/services/software.amazon.smithy.build.SmithyBuildPlugin @@ -0,0 +1 @@ +software.amazon.smithy.dafny.codegen.DafnyClientCodegenPlugin diff --git a/codegen/smithy-dafny-codegen/src/test/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginTest.java b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginTest.java new file mode 100644 index 000000000..e1a9ac5f5 --- /dev/null +++ b/codegen/smithy-dafny-codegen/src/test/java/software/amazon/smithy/dafny/codegen/DafnyClientCodegenPluginTest.java @@ -0,0 +1,16 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +package software.amazon.smithy.dafny.codegen; + +import static org.junit.jupiter.api.Assertions.assertTrue; + +import org.junit.jupiter.api.Test; + +public class DafnyClientCodegenPluginTest { + @Test + public void emptyTest() { + // FIXME placeholder test + assertTrue(true); + } +} diff --git a/codegen/smithy-dafny-codegen/src/test/resources/software/amazon/smithy/dafny/codegen/.gitkeep b/codegen/smithy-dafny-codegen/src/test/resources/software/amazon/smithy/dafny/codegen/.gitkeep new file mode 100644 index 000000000..e69de29bb