Merge pull request #3 from mit-pdos/dafny-4

Update to Dafny 4

.github/mailbot.json

@@ -1,4 +1,4 @@
 {
   "commitEmailFormat": "html",
-  "commitList": "tchajed@mit.edu,[email protected],[email protected],[email protected]"
+  "commitList": "tchajed@gmail.com,[email protected],[email protected],[email protected]"
 }

.github/workflows/main.yml

@@ -10,29 +10,29 @@ on:
 
 # settings shared across all jobs
 env:
-  dafny: "3.11.0"
-  go: "^1.20.0"
+  dafny: "4.4.0"
+  go: "^1.21.0"
 
 jobs:
   verify:
     name: Verify
     runs-on: ubuntu-latest
     steps:
+      - uses: actions/checkout@v4
       - name: Install Dafny
-        uses: dafny-lang/setup-dafny-action@v1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
           dafny-version: ${{ env.dafny }}
-      - uses: actions/checkout@v3
       - name: Verify
         run: make -j2 verify
   test-support:
     name: Test dafny_go
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/setup-go@v3
+      - uses: actions/checkout@v4
+      - uses: actions/setup-go@v5
         with:
           go-version: ${{ env.go }}
-      - uses: actions/checkout@v3
       - name: Test support library
         run: |
           go test -v -timeout=1m ./dafny_go/... ./eval
@@ -41,14 +41,14 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 10
     steps:
+      - uses: actions/checkout@v4
       - name: Install Dafny
-        uses: dafny-lang/setup-dafny-action@v1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
           dafny-version: ${{ env.dafny }}
-      - uses: actions/setup-go@v3
+      - uses: actions/setup-go@v5
         with:
           go-version: ${{ env.go }}
-      - uses: actions/checkout@v3
       - name: Install goimports
         run: |
           go install golang.org/x/tools/cmd/goimports@latest
@@ -71,17 +71,17 @@ jobs:
           ./bench/run-daisy-nfsd.sh go run ./cmd/fs-test /mnt/nfs
   test-macos:
     name: Test NFS server (macOS)
-    runs-on: macos-12
+    runs-on: macos-latest
     timeout-minutes: 10
     steps:
+      - uses: actions/checkout@v4
       - name: Install Dafny
-        uses: dafny-lang/setup-dafny-action@v1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
           dafny-version: ${{ env.dafny }}
-      - uses: actions/setup-go@v3
+      - uses: actions/setup-go@v5
         with:
           go-version: ${{ env.go }}
-      - uses: actions/checkout@v3
       - name: Install goimports
         run: |
           go install golang.org/x/tools/cmd/goimports@latest

Makefile

@@ -1,22 +1,10 @@
 DFY_FILES := $(shell find src -name "*.dfy")
 OK_FILES := $(DFY_FILES:.dfy=.dfy.ok)
 
-# use DAFNY_CORES instead of a load factor since /vcsLoad is broken in Dafny 3.5.0
-#DAFNY_LOAD := 0.5
-
-UNAME_S := $(shell uname -s)
-ifeq ($(UNAME_S),Darwin)
-	NUM_CORES := $(shell sysctl -n hw.ncpu)
-else
-	NUM_CORES := $(shell nproc)
-endif
-DAFNY_CORES ?= $(shell expr $(NUM_CORES) / 2)
-
-# these arguments don't affect verification outcomes
-DAFNY_BASIC_ARGS = /compile:0 /compileTarget:go /timeLimit:20 /vcsCores:$(DAFNY_CORES)
-
-DAFNY_ARGS := /noNLarith /arith:5
-DAFNY=./etc/dafnyq $(DAFNY_BASIC_ARGS) $(DAFNY_ARGS)
+DAFNY_CORES := "50%"
+DAFNY_BASIC_ARGS := --verification-time-limit 20 --cores $(DAFNY_CORES)
+DAFNY_ARGS := --disable-nonlinear-arithmetic
+DAFNY = ./etc/dafnyq verify $(DAFNY_BASIC_ARGS) $(DAFNY_ARGS)
 
 Q:=@
 
@@ -38,7 +26,7 @@ ifeq ($(filter clean,$(MAKECMDGOALS)),)
 endif
 
 # allow non-linear reasoning for nonlin directory specifically
-src/nonlin/%.dfy.ok: DAFNY_ARGS = /arith:1
+src/nonlin/%.dfy.ok: DAFNY_ARGS =
 
 %.dfy.ok: %.dfy
 	@echo "DAFNY $<"
@@ -53,7 +41,7 @@ src/nonlin/%.dfy.ok: DAFNY_ARGS = /arith:1
 # up unused imports emitted by Dafny.
 dafnygen/dafnygen.go: src/compile.dfy $(DFY_FILES)
 	@echo "DAFNY COMPILE $<"
-	$(Q)$(DAFNY) /countVerificationErrors:0 /spillTargetCode:2 /out dafnygen $<
+	$(Q)./etc/dafnyq translate go --no-verify --include-runtime --output dafnygen $<
 	$(Q)rm -rf dafnygen
 	$(Q)cd dafnygen-go/src && ../../etc/dafnygen-imports.py ../../dafnygen
 	$(Q)rm -r dafnygen-go

README.md

@@ -43,13 +43,13 @@ continuous integration.
 Run `make` to compile and verify everything, or `make compile` to just compile
 from Dafny to Go. Then you can build the server with `go build ./cmd/daisy-nfsd`.
 
-You'll need Dafny 3:
+You'll need Dafny 4:
 
 - On Arch Linux you can get `dafny-bin` from the AUR
 - On macOS use `brew install dafny`
 - For other systems the easiest solution is to download a binary release from
-  https://github.com/dafny-lang/dafny/releases, extract it, and add it to your
-  $PATH (this is what we have to do in CI, which runs on Ubuntu 20.04).
+  <https://github.com/dafny-lang/dafny/releases>, extract it, and add it to your
+  $PATH (this is what we have to do in CI, which runs on Ubuntu 22.04).
 
 Compilation additionally depends on `goimports` to remove unused imports:
 
@@ -97,7 +97,7 @@ the kernel to get the fix (you can check what you have with `uname -r`).
 On macOS you already have `rpcbind` and the NFS client utilities, but you'll
 need to start a couple services with:
 
-```
+```sh
 sudo launchctl start com.apple.rpcbind
 sudo launchctl start com.apple.lockd
 ```
@@ -122,3 +122,18 @@ You can run tests for this support library with `go test`:
 ```sh
 go test ./dafny_go/...
 ```
+
+## Checking verification performance
+
+To time verification and analyze the results easily, we have a script to process timing from Dafny's `/trace` option. Use it with the following fish function:
+
+```fish
+function dafny_time
+  set -l file $argv[1]
+  dafny /timeLimit:10 /compile:0 /arith:5 /noNLarith /trace $file $argv[2..-1] > .timing.prof
+  cat .timing.prof | ./etc/summarize-timing
+end
+```
+
+The timing infrastructure itself is implemented as a library in `etc/`. It even
+has tests, which you can run with `pytest`.

dafny_go/jrnl/jrnl.go

@@ -9,11 +9,7 @@ import (
 
 type Disk = disk.Disk
 
-type Companion_DefaultStruct struct{}
-
-var Companion_Default___ = Companion_DefaultStruct{}
-
-func (_ Companion_DefaultStruct) DiskSize(d *Disk) uint64 {
+func DiskSize(d *Disk) uint64 {
 	return (*d).Size()
 }
 

dfyconfig.toml

@@ -0,0 +1 @@
+includes = ["src/**/*.dfy"]

etc/test_timing.py

@@ -4,32 +4,32 @@
 
 
 def test_name_parse():
-    line = r"""Verifying CheckWellformed$$_26_Inode.__default.blks__unique ..."""
+    line = r"""Verifying TypedFs.TypedFilesys.FreeFiles (correctness) ..."""
     d = get_name(line)
     assert d is not None
-    assert d["type"] == "CheckWellformed"
-    assert d["name"] == "__default.blks__unique"
+    assert d["type"] == "correctness"
+    assert d["name"] == "TypedFilesys.FreeFiles"
 
 
 def test_timing_parse1():
-    line = r"""  [0.409 s, 1 proof obligation]  verified"""
+    line = r"""[0.006 s, solver resource count: 15761, 3 proof obligations]  verified"""
     d = get_time(line)
     assert d is not None
-    assert d["time_s"] == 0.409
-    assert d["obligations"] == 1
+    assert d["time_s"] == 0.006
+    assert d["obligations"] == 3
     assert d["result"] == "ok"
 
 
 def test_timing_parse2():
-    line = r"""  [0.360 s, 50 proof obligations]  verified"""
+    line = r"""  [0.005 s, solver resource count: 9753, 1 proof obligation]  verified"""
     d = get_time(line)
     assert d is not None
-    assert d["time_s"] == 0.360
-    assert d["obligations"] == 50
+    assert d["time_s"] == 0.005
+    assert d["obligations"] == 1
 
 
 def test_timing_parse3():
-    line = r"""  [60.987 s, 161 proof obligations]  timed out"""
+    line = r"""  [60.987 s, solver resource count: 132341, 161 proof obligations]  timed out"""
     d = get_time(line)
     assert d is not None
     assert d["time_s"] == 60.987
@@ -46,63 +46,72 @@ def test_timing_parse_new():
 
 def test_df_parse():
     lines = r"""
-Verifying CheckWellformed$$_26_Inode.__default.encode__ino ...
-  [0.128 s, 1 proof obligation]  verified
-
-Verifying Impl$$_26_Inode.__default.encode__ino ...
-  [0.360 s, 50 proof obligations]  verified
-
-Verifying CheckWellformed$$_26_Inode.__default.decode__ino ...
-  [0.133 s, 2 proof obligations]  verified
-
-Verifying Impl$$_26_Inode.__default.decode__ino ...
-  [0.286 s, 67 proof obligations]  verified
+Verifying TypedFs.TypedFilesys.zeroFreeSpace (well-formedness) ...
+[TRACE] Using prover: /opt/homebrew/bin/z3
+  [0.098 s, solver resource count: 329601, 2 proof obligations]  verified
+
+Verifying TypedFs.TypedFilesys.zeroFreeSpace (correctness) ...
+  [0.719 s, solver resource count: 4046295, 87 proof obligations]  errors
+src/fs/typed_fs.dfy(597,4): Error: a postcondition could not be proved on this return path
+src/fs/typed_fs.dfy(594,31): Related location: this is the postcondition that could not be proved
+src/fs/typed_fs.dfy(94,9): Related location
+src/fs/typed_fs.dfy(599,28): Error: a precondition for this call could not be proved
+src/fs/byte_fs.dfy(1063,15): Related location: this is the precondition that could not be proved
+src/fs/byte_fs.dfy(134,12): Related location
+
+Verifying TypedFs.TypedFilesys.TotalFiles (correctness) ...
+  [0.005 s, solver resource count: 9753, 1 proof obligation]  verified
+
+Verifying TypedFs.TypedFilesys.FreeFiles (correctness) ...
+  [0.006 s, solver resource count: 15761, 3 proof obligations]  verified
+
+Dafny program verifier finished with 51 verified, 28 errors
     """.split(
         "\n"
     )
     df = parse_df(lines)
     assert df.shape == (4, 5)
-    assert df.at[3, "name"] == "__default.decode__ino"
-    assert df.at[1, "time_s"] == 0.360
-    assert df.at[2, "obligations"] == 2
-
-
-def test_df_parse_errors():
-    lines = r"""
-Verifying CheckWellformed$$IndFs.IndFilesys.write ...
-  [0.253 s, 5 proof obligations]  verified
-
-Verifying Impl$$IndFs.IndFilesys.write ...
-  [9.172 s, 114 proof obligations]  error
-/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(379,10): Error: A postcondition might not hold on this return path.
-/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(360,14): Related location: This is the postcondition that might not hold.
-/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(339,9): Related location
-/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(330,9): Related location
-/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(289,10): Related location
-/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(290,68): Related location
-Execution trace:
-    (0,0): anon0
-    (0,0): anon10_Then
-    (0,0): anon11_Then
-    (0,0): anon12_Else
-
-Verifying CheckWellformed$$IndFs.__default.config ...
-  [0.315 s, 15 proof obligations]  verified
-
-Verifying CheckWellformed$$IndFs.__default.config__properties ...
-  [0.259 s, 1 proof obligation]  verified
-
-Verifying Impl$$IndFs.__default.config__properties ...
-  [1.582 s, 3 proof obligations]  verified
-
-Verifying Impl$$IndFs.__default.config__totals ...
-  [2.290 s, 15 proof obligations]  verified
-
-Verifying CheckWellformed$$IndFs.__default.MkRole ...
-  [0.320 s, 2 proof obligations]  verified
-    """.split(
-        "\n"
-    )
-    df = parse_df(lines)
-    assert df.shape == (7, 5)
-    assert df.at[1, "result"] == "error"
+    assert df.at[3, "name"] == "TypedFilesys.FreeFiles"
+    assert df.at[1, "time_s"] == 0.719
+    assert df.at[2, "obligations"] == 1
+
+
+#def test_df_parse_errors():
+#    lines = r"""
+#Verifying CheckWellformed$$IndFs.IndFilesys.write ...
+#  [0.253 s, 5 proof obligations]  verified
+#
+#Verifying Impl$$IndFs.IndFilesys.write ...
+#  [9.172 s, 114 proof obligations]  error
+#/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(379,10): Error: A postcondition might not hold on this return path.
+#/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(360,14): Related location: This is the postcondition that might not hold.
+#/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(339,9): Related location
+#/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(330,9): Related location
+#/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(289,10): Related location
+#/Users/tchajed/code/daisy-nfsd/src/Dafny/examples/fs/indirect_fs.dfy(290,68): Related location
+#Execution trace:
+#    (0,0): anon0
+#    (0,0): anon10_Then
+#    (0,0): anon11_Then
+#    (0,0): anon12_Else
+#
+#Verifying CheckWellformed$$IndFs.__default.config ...
+#  [0.315 s, 15 proof obligations]  verified
+#
+#Verifying CheckWellformed$$IndFs.__default.config__properties ...
+#  [0.259 s, 1 proof obligation]  verified
+#
+#Verifying Impl$$IndFs.__default.config__properties ...
+#  [1.582 s, 3 proof obligations]  verified
+#
+#Verifying Impl$$IndFs.__default.config__totals ...
+#  [2.290 s, 15 proof obligations]  verified
+#
+#Verifying CheckWellformed$$IndFs.__default.MkRole ...
+#  [0.320 s, 2 proof obligations]  verified
+#    """.split(
+#        "\n"
+#    )
+#    df = parse_df(lines)
+#    assert df.shape == (7, 5)
+#    assert df.at[1, "result"] == "error"

etc/timing.py

@@ -9,9 +9,9 @@
 
 NAME_RE = re.compile(
     r"""Verifying\s
-    (?P<type>\w*)\$\$
     (?P<module>[a-zA-Z0-9_]*)\.
     (?P<name>[a-zA-Z0-9_.]*)
+    \s\((?P<type>[a-zA-Z-]*)\)
     \s\.\.\.
     """,
     re.VERBOSE,
@@ -37,6 +37,11 @@ def get_name(line):
     re.VERBOSE,
 )
 
+SKIP_RE = re.compile(
+    r"""^\[TRACE\]""",
+    re.VERBOSE,
+)
+
 
 def get_time(line):
     m = TIME_RE.match(line)
@@ -60,11 +65,14 @@ def parse_df(lines) -> pd.DataFrame:
 
     for line in lines:
         line = line.rstrip("\n")
+        if SKIP_RE.match(line):
+            continue
         if current is None:
             current = get_name(line)
             continue
 
         # should find timing after a name
+
         timing = get_time(line)
         if timing is None:
             print(f"did not find timing info for {current}", file=sys.stderr)