From 3aae84a50c93a47192d0fbe212c6ddafedd5373a Mon Sep 17 00:00:00 2001 From: Bua <72684195+kbuaaaaaa@users.noreply.github.com> Date: Wed, 11 Sep 2024 15:25:47 +0100 Subject: [PATCH 1/2] Fuzzing on forks (#5762) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ### Description I have modified the fuzzing workflow to handle PR from forks. Fuzzing will only be triggered on PR created by verified contributors to prevent potential security risks. **ALL WILL BE FUZZED** mwahaha This change also fix the following annoying issues: - Reporting bugs already caught by CI: Fuzzing will now be delayed and only run if all CI checks have passed. This is implemented outside of the workflow, the PR will not be blocked. - Reporting non-bugs in Rust: Added pattern matching to ignore error that comes from not yet implemented features in Dafny-to-Rust. (sorry Mikael!) ### How has this been tested? Tested on my own dummy repo 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). --- ...ci_fuzz_no_forks.yaml => compfuzzci_fuzz.yaml} | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) rename .github/workflows/{compfuzzci_fuzz_no_forks.yaml => compfuzzci_fuzz.yaml} (58%) diff --git a/.github/workflows/compfuzzci_fuzz_no_forks.yaml b/.github/workflows/compfuzzci_fuzz.yaml similarity index 58% rename from .github/workflows/compfuzzci_fuzz_no_forks.yaml rename to .github/workflows/compfuzzci_fuzz.yaml index ee41745889c..720f6a02a76 100644 --- a/.github/workflows/compfuzzci_fuzz_no_forks.yaml +++ b/.github/workflows/compfuzzci_fuzz.yaml @@ -1,15 +1,19 @@ # This workflow is triggered on PR being opened, synced, reopened, closed. # It dispatches workflow on CompFuzzCI repository, where fuzzing of the PR is handled. +# For problems or suggestions, contact karnbongkot.boonriong23@imperial.ac.uk -name: Fuzzing on PR (excluding forks) +name: Fuzzing on PR on: - pull_request: + pull_request_target: branches: - master jobs: FuzzOnPR: - if: github.event.pull_request.base.ref == 'master' && github.event.pull_request.head.repo.owner.login == 'dafny-lang' + if: github.event.pull_request.base.ref == 'master' && + (github.event.pull_request.author_association == 'COLLABORATOR' || + github.event.pull_request.author_association == 'MEMBER' || + github.event.pull_request.author_association == 'OWNER') runs-on: ubuntu-latest steps: - name: Trigger CompFuzzCI @@ -23,9 +27,10 @@ jobs: workflow_id: 'fuzz.yaml', ref: 'main', inputs: { - commit: '${{ github.event.pull_request.head.sha }}', - main_commit: '${{github.event.pull_request.base.sha}}', + pr: '${{github.event.pull_request.number}}', + author: '${{github.event.pull_request.user.login}}', branch: '${{github.event.pull_request.head.ref}}', + head_sha: '${{github.event.pull_request.head.sha}}', duration: '3600', instance: '2' } From dc44321d6b56dc509a6bc4cd139ede8269464019 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 12 Sep 2024 16:58:04 +0200 Subject: [PATCH 2/2] Fix a bug related to hide/reveal and recursive functions (#5764) Fixes #5763 Requires the upcoming Boogie version 3.2.5, for which this PR needs to be merged first: https://github.com/boogie-org/boogie/pull/945 ### Description - No longer allow hiding functions from the Dafny prelude by using `hide *`. This affected recursive functions because they use `$LS` which is defined in the prelude. ### How has this been tested? - Added a CLI test-case to `revealFunctions.dfy` 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/DafnyCore/DafnyCore.csproj | 2 +- Source/DafnyCore/Verifier/BoogieGenerator.cs | 3 +++ .../LitTest/ast/reveal/revealFunctions.dfy | 18 ++++++++++++++++++ .../ast/reveal/revealFunctions.dfy.expect | 2 +- customBoogie.patch | 2 +- dotnet-tools.json | 2 +- 6 files changed, 25 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 5899a78c19a..73318352a5e 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index bc1c1121770..ccc218892c0 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -85,6 +85,9 @@ public BoogieGenerator(ErrorReporter reporter, ProofDependencyManager depManager Bpl.Program boogieProgram = ReadPrelude(); if (boogieProgram != null) { sink = boogieProgram; + foreach (var function in boogieProgram.TopLevelDeclarations.OfType()) { + function.AlwaysRevealed = true; + } predef = FindPredefinedDecls(boogieProgram); } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy index b22a059f208..8233d2f066e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy @@ -84,4 +84,22 @@ method ReadsClause() { reveal Obj; } } +} + +module M1 { + ghost function RecFunc(x: nat): nat { + if x == 0 then 0 + else 1 + RecFunc(x - 1) + } +} +module M2 { + import opened M1 + lemma Lemma(x: nat) + ensures RecFunc(0) == 0 + { + // Because RecFunc is recursive, it uses the fuel related $LS function, + // this was previously hidden by 'hide *', so that the ensures could not be proven + hide *; + reveal RecFunc; + } } \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect index fdb082cac82..875e3bafe09 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect @@ -2,4 +2,4 @@ revealFunctions.dfy(15,12): Error: assertion might not hold revealFunctions.dfy(22,12): Error: assertion might not hold revealFunctions.dfy(49,21): Error: assertion might not hold -Dafny program verifier finished with 15 verified, 3 errors +Dafny program verifier finished with 22 verified, 3 errors diff --git a/customBoogie.patch b/customBoogie.patch index c9ea056313d..7763dd9801c 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + + diff --git a/dotnet-tools.json b/dotnet-tools.json index 799afea8de8..3c54d779830 100644 --- a/dotnet-tools.json +++ b/dotnet-tools.json @@ -9,7 +9,7 @@ ] }, "boogie": { - "version": "3.1.3", + "version": "3.2.5", "commands": [ "boogie" ]