Merge branch 'opaqueBlock' of github.com:keyboardDrummer/dafny into o…

…paqueBlock
dafny-lang · Sep 12, 2024 · 605cc77 · 605cc77
2 parents 467e846 + b2c9962
commit 605cc77
Show file tree

Hide file tree

Showing 7 changed files with 35 additions and 9 deletions.
diff --git a/...b/workflows/compfuzzci_fuzz_no_forks.yaml → .github/workflows/compfuzzci_fuzz.yaml b/...b/workflows/compfuzzci_fuzz_no_forks.yaml → .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 [email protected]
 
-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'
                   }

diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
@@ -34,7 +34,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.4" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.5" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

diff --git 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<Bpl.Function>()) {
+          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
@@ -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;
+    }
 }
diff --git 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
@@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644
        <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
        <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
        <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
--      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.4" />
+-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.5" />
 +      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
 +      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />

diff --git a/dotnet-tools.json b/dotnet-tools.json
@@ -9,7 +9,7 @@
       ]
     },
     "boogie": {
-      "version": "3.1.3",
+      "version": "3.2.5",
       "commands": [
         "boogie"
       ]