-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'Golang/dev' into rishav-positional
- Loading branch information
Showing
456 changed files
with
19,904 additions
and
17,478 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,81 +1,64 @@ | ||
| name: Library Go tests | ||
|
|
||
| on: ["pull_request", "push"] | ||
| on: | ||
| workflow_call: | ||
| inputs: | ||
| dafny: | ||
| description: "The Dafny version to run" | ||
| required: true | ||
| type: string | ||
| num_shards: | ||
| required: false | ||
| type: number | ||
| default: 5 | ||
|
|
||
| jobs: | ||
| test_go: | ||
| populate-matrix-dimensions: | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Populate shard list | ||
| id: populate-shard-list | ||
| run: echo "shard-list=[`seq -s , 1 ${{ inputs.num_shards }}`]" >> $GITHUB_OUTPUT | ||
| outputs: | ||
| shard-list: ${{ steps.populate-shard-list.outputs.shard-list }} | ||
| testGo: | ||
| needs: populate-matrix-dimensions | ||
| strategy: | ||
| fail-fast: false | ||
| fail-fast: false # at least for development; see all errors | ||
| matrix: | ||
| library: [ | ||
| # TODO: Uncomment below before making PR | ||
| # TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on | ||
| TestModels/Aggregate, | ||
| # TestModels/AggregateReferences, | ||
| TestModels/CodegenPatches, | ||
| TestModels/Constraints, | ||
| TestModels/Constructor, | ||
| TestModels/Dependencies, | ||
| TestModels/Errors, | ||
| TestModels/Extendable, | ||
| TestModels/Extern, | ||
| # TestModels/LanguageSpecificLogic, | ||
| # TestModels/LocalService, | ||
| # TestModels/MultipleModels, | ||
| TestModels/Positional, | ||
| TestModels/Refinement, | ||
| TestModels/Resource, | ||
| # TestModels/SimpleTypes/BigDecimal, | ||
| # TestModels/SimpleTypes/BigInteger, | ||
| TestModels/SimpleTypes/SimpleBlob, | ||
| TestModels/SimpleTypes/SimpleBoolean, | ||
| # TestModels/SimpleTypes/SimpleByte, | ||
| TestModels/SimpleTypes/SimpleDouble, | ||
| TestModels/SimpleTypes/SimpleEnum, | ||
| # TestModels/SimpleTypes/SimpleEnumV2, | ||
| # TestModels/SimpleTypes/SimpleFloat, | ||
| TestModels/SimpleTypes/SimpleInteger, | ||
| TestModels/SimpleTypes/SimpleLong, | ||
| # TestModels/SimpleTypes/SimpleShort, | ||
| TestModels/SimpleTypes/SimpleString, | ||
| # TestModels/SimpleTypes/SimpleTimestamp, | ||
| TestModels/Union, | ||
| # TestModels/aws-sdks/ddb, | ||
| TestModels/aws-sdks/kms | ||
| ] | ||
| runs-on: "macos-12" | ||
| shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }} | ||
| runs-on: "ubuntu-latest" | ||
| permissions: | ||
| id-token: write | ||
| contents: read | ||
| env: | ||
| DOTNET_CLI_TELEMETRY_OPTOUT: 1 | ||
| DOTNET_NOLOGO: 1 | ||
| steps: | ||
| - uses: actions/checkout@v2 | ||
| - name: Support longpaths on Git checkout | ||
| run: | | ||
| git config --global core.longpaths true | ||
| # - name: Setup Dafny 4.5.0 | ||
| # uses: dafny-lang/[email protected] | ||
| # with: | ||
| # dafny-version: 4.5.0 | ||
| # TODO: Setup Dafny once its released | ||
| - name: Setup dotnet | ||
| uses: actions/setup-dotnet@v4 | ||
| - name: Configure AWS Credentials | ||
| uses: aws-actions/configure-aws-credentials@v1 | ||
| with: | ||
| dotnet-version: 6.0.x | ||
| aws-region: us-west-2 | ||
| role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-PolymorphTestModels-Role-us-west-2 | ||
| role-session-name: PythonTests | ||
|
|
||
| - name: Build Dafny from source | ||
| run: | | ||
| git clone https://github.com/dafny-lang/dafny.git --recurse-submodules | ||
| cd dafny | ||
| make exe | ||
| - name: Install Z3 version 4.12.1 | ||
| run: | | ||
| cd $GITHUB_WORKSPACE/dafny | ||
| make z3-mac | ||
| - uses: actions/checkout@v3 | ||
| with: | ||
| submodules: recursive | ||
|
|
||
| - name: Add Dafny to PATH | ||
| run: | | ||
| echo "$GITHUB_WORKSPACE/dafny/Scripts" >> $GITHUB_PATH | ||
| - name: Setup Dafny | ||
| uses: dafny-lang/[email protected] | ||
| with: | ||
| dafny-version: ${{ inputs.dafny }} | ||
|
|
||
| - name: Install Go | ||
| uses: actions/setup-go@v2 | ||
| with: | ||
| go-version: '1.21' | ||
| go-version: "1.21" | ||
|
|
||
| - name: Install Go imports | ||
| run: | | ||
|
|
@@ -84,33 +67,36 @@ jobs: | |
| - name: Add go mod to Dafny Runtime Go | ||
| shell: bash | ||
| working-directory: ./DafnyRuntimeGo | ||
| run: | | ||
| run: | | ||
| go mod init github.com/dafny-lang/DafnyRuntimeGo | ||
| go mod tidy | ||
| - name: polymorph dafny dependencies | ||
| shell: bash | ||
| working-directory: ./TestModels/dafny-dependencies/StandardLibrary | ||
| run: | | ||
| export DAFNY_VERSION=4.6 | ||
| make polymorph_dafny | ||
| make transpile_go | ||
| make polymorph_go | ||
| cd ./runtimes/go/ImplementationFromDafny-go/ | ||
| go mod init github.com/dafny-lang/DafnyStandardLibGo | ||
| # TODO: This should handwritten (in the makefile or something) | ||
| echo "replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/" >> go.mod; | ||
| - name: Setup Java 17 for codegen | ||
| uses: actions/setup-java@v3 | ||
| with: | ||
| distribution: "corretto" | ||
| java-version: 17 | ||
|
|
||
| - name: Generate Polymorph Dafny and Go code | ||
| shell: bash | ||
| working-directory: ./${{ matrix.library }} | ||
| run: | | ||
| export DAFNY_VERSION=4.6 | ||
| make polymorph_dafny | ||
| sh ./removeDotFromExtern.sh | ||
| make transpile_go | ||
| make polymorph_go | ||
| - name: Setup smithy-dafny-conversion | ||
| uses: gradle/gradle-build-action@v2 | ||
| with: | ||
| arguments: publishToMavenLocal | ||
| build-root-directory: smithy-dafny-conversion | ||
|
|
||
| goimports -w runtimes/go/ | ||
| cd runtimes/go/TestsFromDafny-go/ | ||
| go run TestsFromDafny.go | ||
| - name: Install Smithy-Dafny codegen dependencies | ||
| uses: ./.github/actions/install_smithy_dafny_codegen_dependencies | ||
|
|
||
| - name: Install smithy-dafny-codegen locally | ||
| uses: gradle/gradle-build-action@v2 | ||
| with: | ||
| arguments: :smithy-dafny-codegen:pTML | ||
| build-root-directory: codegen | ||
|
|
||
| - name: Execute smithy-dafny-codegen-test tests | ||
| uses: gradle/gradle-build-action@v2 | ||
| env: | ||
| JUNIT_SHARD: ${{ matrix.shard }} | ||
| JUNIT_SHARD_COUNT: ${{ inputs.num_shards }} | ||
| with: | ||
| arguments: :smithy-dafny-codegen-test:test --tests '*smithygo*' --info | ||
| build-root-directory: codegen | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
80 changes: 80 additions & 0 deletions
80
TestModels/Aggregate/runtimes/rust/src/standard_library_externs.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,80 @@ | ||
| // Annotation to ignore the case of this module | ||
| use crate::r#_Wrappers_Compile; | ||
| use crate::UTF8; | ||
|
|
||
| impl crate::UTF8::_default { | ||
| pub fn Encode( | ||
| s: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ) -> ::std::rc::Rc< | ||
| r#_Wrappers_Compile::Result< | ||
| UTF8::ValidUTF8Bytes, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >, | ||
| > { | ||
| let v = s.to_array(); | ||
| let mut _accumulator: Vec<u8> = vec![]; | ||
| // Use of .encode_utf8 method. | ||
| let mut surrogate: Option<u16> = None; | ||
| for c in v.iter() { | ||
| let s = if let Some(s) = surrogate { | ||
| String::from_utf16(&[s, c.0]) | ||
| } else { | ||
| String::from_utf16(&[c.0]) | ||
| }; | ||
| surrogate = None; | ||
| match s { | ||
| Ok(value) => { | ||
| _accumulator.extend(value.as_bytes()); | ||
| continue; | ||
| } | ||
| Err(e) => { | ||
| if 0xD800 <= c.0 && c.0 <= 0xDFFF { | ||
| surrogate = Some(c.0); | ||
| continue; | ||
| } | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &e.to_string()) | ||
| }); | ||
| } | ||
| } | ||
| } | ||
| if let Some(s) = surrogate { | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &format!("Surrogate pair missing: 0x{:04x}", s)) | ||
| }); | ||
| } | ||
| ::std::rc::Rc::new(r#_Wrappers_Compile::Result::< | ||
| UTF8::ValidUTF8Bytes, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >::Success { | ||
| value: ::dafny_runtime::Sequence::from_array_owned(_accumulator), | ||
| }) | ||
| } | ||
| pub fn Decode( | ||
| b: &::dafny_runtime::Sequence<u8>, | ||
| ) -> ::std::rc::Rc< | ||
| r#_Wrappers_Compile::Result< | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >, | ||
| > { | ||
| let b = String::from_utf8(b.to_array().as_ref().clone()); | ||
| match b { | ||
| Ok(s) => { | ||
| ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Success { | ||
| value: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s) | ||
| }) | ||
| }, | ||
| Err(e) => { | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &e.to_string()) | ||
| }) | ||
| } | ||
| } | ||
| } | ||
| } |
Oops, something went wrong.