From 5329e7243a1de47a58ceb47a926f86e1b60551bc Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sat, 25 May 2024 01:04:40 +0200 Subject: [PATCH 1/3] fix: Ignore values not in a multiset when computing its hash in C# (#5412) Fixes #4011. --------- Co-authored-by: Aaron Tomb --- Source/DafnyRuntime/DafnyRuntime.cs | 3 +++ .../LitTests/LitTest/git-issues/git-issue-4011.dfy | 11 +++++++++++ .../LitTest/git-issues/git-issue-4011.dfy.expect | 4 ++++ .../LitTest/git-issues/git-issue-4011.dfy.rs.check | 1 + docs/dev/news/5412.fix | 1 + 5 files changed, 20 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.rs.check create mode 100644 docs/dev/news/5412.fix diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs index ecb24f16fe4..f959b66a4ac 100755 --- a/Source/DafnyRuntime/DafnyRuntime.cs +++ b/Source/DafnyRuntime/DafnyRuntime.cs @@ -524,6 +524,9 @@ public override int GetHashCode() { hashCode = hashCode * (key + 3); } foreach (var kv in dict) { + if (kv.Value <= 0) { + continue; + } var key = Dafny.Helpers.GetHashCode(kv.Key); key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); hashCode = hashCode * (key + 3); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy new file mode 100644 index 00000000000..2091c53cc7c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy @@ -0,0 +1,11 @@ +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" + +method Main() { + var a: multiset := multiset{false, true}; + var b: multiset> := multiset{a[true := 0]}; + + print b == multiset{multiset{false}}, "\n"; + print b <= multiset{multiset{false}}, "\n"; + print multiset{multiset{false}} <= b, "\n"; + print b, "\n"; +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.expect new file mode 100644 index 00000000000..19dbbdef020 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.expect @@ -0,0 +1,4 @@ +true +true +true +multiset{multiset{false}} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.rs.check new file mode 100644 index 00000000000..b2ef1d91c39 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.rs.check @@ -0,0 +1 @@ +CHECK: error: expected identifier, found `<` \ No newline at end of file diff --git a/docs/dev/news/5412.fix b/docs/dev/news/5412.fix new file mode 100644 index 00000000000..bba21ee6f63 --- /dev/null +++ b/docs/dev/news/5412.fix @@ -0,0 +1 @@ +Ignore values not in a multiset when computing its hash in C# From 7cbbe7da88799514f75c25ce8f628e6397ae335f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 27 May 2024 20:23:25 +0200 Subject: [PATCH 2/3] =?UTF-8?q?Revert=20"fix:=20Ignore=20values=20not=20in?= =?UTF-8?q?=20a=20multiset=20when=20computing=20its=20hash=20=E2=80=A6=20(?= =?UTF-8?q?#5492)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Revert latest commit to see if that fixes nightly By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyRuntime/DafnyRuntime.cs | 3 --- .../LitTests/LitTest/git-issues/git-issue-4011.dfy | 11 ----------- .../LitTest/git-issues/git-issue-4011.dfy.expect | 4 ---- .../LitTest/git-issues/git-issue-4011.dfy.rs.check | 1 - docs/dev/news/5412.fix | 1 - 5 files changed, 20 deletions(-) delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.expect delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.rs.check delete mode 100644 docs/dev/news/5412.fix diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs index f959b66a4ac..ecb24f16fe4 100755 --- a/Source/DafnyRuntime/DafnyRuntime.cs +++ b/Source/DafnyRuntime/DafnyRuntime.cs @@ -524,9 +524,6 @@ public override int GetHashCode() { hashCode = hashCode * (key + 3); } foreach (var kv in dict) { - if (kv.Value <= 0) { - continue; - } var key = Dafny.Helpers.GetHashCode(kv.Key); key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode(); hashCode = hashCode * (key + 3); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy deleted file mode 100644 index 2091c53cc7c..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" - -method Main() { - var a: multiset := multiset{false, true}; - var b: multiset> := multiset{a[true := 0]}; - - print b == multiset{multiset{false}}, "\n"; - print b <= multiset{multiset{false}}, "\n"; - print multiset{multiset{false}} <= b, "\n"; - print b, "\n"; -} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.expect deleted file mode 100644 index 19dbbdef020..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.expect +++ /dev/null @@ -1,4 +0,0 @@ -true -true -true -multiset{multiset{false}} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.rs.check deleted file mode 100644 index b2ef1d91c39..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4011.dfy.rs.check +++ /dev/null @@ -1 +0,0 @@ -CHECK: error: expected identifier, found `<` \ No newline at end of file diff --git a/docs/dev/news/5412.fix b/docs/dev/news/5412.fix deleted file mode 100644 index bba21ee6f63..00000000000 --- a/docs/dev/news/5412.fix +++ /dev/null @@ -1 +0,0 @@ -Ignore values not in a multiset when computing its hash in C# From dc2948edb90be4e0035425210c924f54bb9c1960 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 28 May 2024 01:53:53 -0700 Subject: [PATCH 3/3] ci: Use macos-11 in all CI (#5493) ### Description Addresses two issues: 1. The nightly builds are starting to occasionally fail because the `macos-latest` runners are struggling to complete integration test shards in under 2 hours. It seems likely the newer ARM-based runners are underpowered. 2. ~`macos-11` runners will be removed by 6/28, and will start temporarily failing on 6/17. Better to move off them now.~ `macos-12` hits a compiler error on DAST.cs for some reason (`error CS8078: An expression is too long or complex to compile`) so we'll stick to `macos-11` for this PR ### How has this been tested? `run-deep-tests` label By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .github/workflows/integration-tests-reusable.yml | 4 ++-- .github/workflows/publish-release-reusable.yml | 2 +- .github/workflows/release-brew.yml | 2 +- .github/workflows/release-downloads-nuget.yml | 2 +- .github/workflows/release-downloads.yml | 4 ++-- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 45805e5c334..7c8cd7d2d9e 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -27,7 +27,7 @@ jobs: - name: Populate OS list (all platforms) id: populate-os-list-all if: inputs.all_platforms - run: echo "os-list=[\"ubuntu-latest\", \"ubuntu-20.04\", \"macos-latest\", \"windows-2019\"]" >> $GITHUB_OUTPUT + run: echo "os-list=[\"ubuntu-latest\", \"ubuntu-20.04\", \"macos-11\", \"windows-2019\"]" >> $GITHUB_OUTPUT - name: Populate OS list (one platform) id: populate-os-list-one if: "!inputs.all_platforms" @@ -35,7 +35,7 @@ jobs: - name: Populate OS mapping for package.py id: populate-os-mapping run: | - echo "os-mapping={\"ubuntu-latest\": \"ubuntu\", \"ubuntu-20.04\": \"ubuntu\", \"macos-latest\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT + echo "os-mapping={\"ubuntu-latest\": \"ubuntu\", \"ubuntu-20.04\": \"ubuntu\", \"macos-11\": \"macos\", \"windows-2019\": \"windows\"}" >> $GITHUB_OUTPUT - name: Populate target runtime version list (all platforms) id: populate-target-runtime-version-all if: inputs.all_platforms diff --git a/.github/workflows/publish-release-reusable.yml b/.github/workflows/publish-release-reusable.yml index a86b9e1edeb..062905f9d3d 100644 --- a/.github/workflows/publish-release-reusable.yml +++ b/.github/workflows/publish-release-reusable.yml @@ -35,7 +35,7 @@ env: jobs: publish-release: - runs-on: macos-latest # Put back 'ubuntu-20.04' if macos-latest fails in any way + runs-on: macos-11 # Put back 'ubuntu-20.04' if macos-11 fails in any way steps: - name: Print version run: echo ${{ inputs.name }} diff --git a/.github/workflows/release-brew.yml b/.github/workflows/release-brew.yml index 00c910954f9..2ffca171c17 100644 --- a/.github/workflows/release-brew.yml +++ b/.github/workflows/release-brew.yml @@ -10,7 +10,7 @@ concurrency: jobs: build: - runs-on: macos-latest + runs-on: macos-11 steps: - name: Install dafny diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml index 31d0e91d585..6f584c636f7 100644 --- a/.github/workflows/release-downloads-nuget.yml +++ b/.github/workflows/release-downloads-nuget.yml @@ -111,7 +111,7 @@ jobs: # but note we need to skip Dafny since nuget install doesn't work for dotnet tools. library-name: [ DafnyPipeline, DafnyServer, DafnyLanguageServer, DafnyRuntime, DafnyCore, DafnyDriver ] # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906 - os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ] + os: [ ubuntu-latest, ubuntu-20.04, macos-11, windows-2019 ] steps: # Verify that the dependencies of the libraries we publish (e.g. DafnyLanguageServer) diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml index f6158a53d4c..84b7e34fd09 100644 --- a/.github/workflows/release-downloads.yml +++ b/.github/workflows/release-downloads.yml @@ -18,13 +18,13 @@ jobs: fail-fast: false matrix: # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906 - os: [ ubuntu-latest, ubuntu-20.04, macos-latest, windows-2019 ] + os: [ ubuntu-latest, ubuntu-20.04, macos-11, windows-2019 ] include: - os: 'ubuntu-latest' osn: 'ubuntu-20.04' - os: 'ubuntu-20.04' osn: 'ubuntu-20.04' - - os: 'macos-latest' + - os: 'macos-11' osn: 'x64-macos-11' - os: 'windows-2019' osn: 'windows-2019'