Updating the original files in libraries to Dafny 4 (#2) (#97)

Also applies dafny format and changes the lit commands to use the new CLI.

Co-authored-by: Robin Salkeld <[email protected]>

.github/workflows/check-format

@@ -0,0 +1,9 @@
+#! /usr/bin/env bash
+
+FAIL=0
+for f in `find $1 -name '*.dfy'`; do \
+  echo $f ;\
+  dafny format --check $f || ( dafny format --print $f | diff $f - ) ;\
+  if [ "$?" != 0 ] ; then FAIL=1 ;  fi; \
+done
+exit $FAIL

.github/workflows/check-format.yml

@@ -0,0 +1,38 @@
+# This workflow does static verification of the legacy modules
+name: Check formatting
+
+on:
+  workflow_dispatch:
+  pull_request:
+    branches: [ master ]
+
+jobs:
+  formatting:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: switch branch
+        run: |
+          git fetch
+          git checkout cok-code
+
+      - name: Install Dafny
+        uses: dafny-lang/setup-dafny-action@v1
+        with:
+          dafny-version: "nightly-2023-02-15-567a5ba"
+
+      - name: Install lit
+        run: pip install lit OutputCheck
+
+      - name: Set up JS dependencies
+        run: npm install bignumber.js
+
+      - name: Check exe
+        run: |
+          dafny --version
+
+      - name: Check formatting
+        run: |
+          chmod +x ./.github/workflows/check-format
+          ./.github/workflows/check-format src

.github/workflows/tests.yml

@@ -1,38 +1,66 @@
-# This workflow performs static analysis checks.
-name: tests
+# This workflow does static verification of the DafnyCore library
+name: Dafny Core verification
 
 on:
+  # Scheduled to be run sometime after the nightly build of dafny
+  schedule:
+    - cron: "7 10 * * *"
   workflow_dispatch:
-  push:
-    branches: [ master ]
   pull_request:
     branches: [ master ]
 
 jobs:
   verification:
-    runs-on: ubuntu-latest
+    continue-on-error: true
+    strategy:
+      fail-fast: false
+      matrix:
+        # nightly-latest to catch anything that breaks these tests in current development
+        # 2/18/2023 version is the first that supports logging
+        # 3.11.0 supports new CLI but does not support logging
+        version: [ nightly-latest, nightly-2023-02-18-ef4f346, 3.11.0]
+        os: [ ubuntu-latest ]
+
+    runs-on: ${{ matrix.os }}
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
 
       - name: Install Dafny
-        uses: dafny-lang/setup-dafny-action@v1
+        uses: dafny-lang/setup-dafny-action@v1.6.0
         with:
-          dafny-version: "3.9.1"
+          dafny-version: ${{ matrix.version }}
+
+      - name: Version information
+        run: |
+          dafny --version
+          echo ${{ matrix.os }} ${{ runner.os }} ${{ matrix.version }}
+
+      - name: Upgrade outdated pip
+        run: python -m pip install --upgrade pip
 
       - name: Install lit
         run: pip install lit OutputCheck
 
       - name: Set up JS dependencies
         run: npm install bignumber.js
 
-      - name: Verify Dafny Code
-        run: lit --time-tests -v --param 'dafny_params=/verificationLogger:trx /verificationLogger:csv' .
+      - name: Verify Code and Examples without logging
+        id: nolog
+        if: matrix.version == '3.11.0'
+        run: lit --time-tests -v .
+
+      - name: Verify Code and Examples
+        id: withlog
+        if: steps.nolog.conclusion == 'skipped'
+        run: |
+          lit --time-tests -v --param 'dafny_params=--log-format trx --log-format csv' .
 
       - name: Generate Report
+        if: always() && steps.withlog.conclusion != 'skipped'
         run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-duration-seconds 10
 
       - uses: actions/upload-artifact@v2  # upload test results
-        if: success() || failure()        # run this step even if previous step failed
+        if: always() && steps.withlog.conclusion != 'skipped'
         with:
           name: verification-results
           path: '**/TestResults/*.trx'

.gitignore

@@ -1,2 +1,9 @@
+**/.DS_Store
 **/Output/
 **/TestResults/
+examples/FileIO/ReadBytesFromFile.cs
+examples/FileIO/ReadBytesFromFile.jar
+examples/FileIO/ReadBytesFromFile.js
+examples/FileIO/WriteBytesToFile.cs
+examples/FileIO/WriteBytesToFile.jar
+examples/FileIO/WriteBytesToFile.js

README-TESTING.md

@@ -0,0 +1,32 @@
+# Testing the libraries
+
+The code in these libraries is tested both with deductive verification, using dafny,
+and with traditional runtime testing of compilations by dafny. 
+The latter is important as a check that dafny compiled the (verified) dafny code correctly.
+Also, some functionality (e.g. FileIO) is partially implemented using
+custom code in the target programming language, which is not verified by dafny.
+All files are also checked that they conform to standard dafny formatting,
+using `dafny format`.
+
+The tests are run using `lit`. The configuration of the tests is controlled by
+(a) the lit.site.cfg file and (b) the yml files in .github/workflows.
+
+The tests are run on each push to a pull_request and are required to pass to enable merging.
+They are also run on a nightly schedule.
+
+To run the files manually: run `lit .` in this directory (`libraries`, at the top
+of the clone of the repo). You can also manually run individual files or directories,
+but `lit` must be invoked in the `libraries` directory. You can also trigger the workflow
+using `workflow_dispatch`. To do a manual check of formatting, use `dafny format --check <file or folder>`.
+
+The tests themselves are specially formatted lines (those beginning with `// RUN:`) in
+each .dfy file. The tests use dafny's new command-line syntax, using the lit
+macros `%verify` and `%run` and the like.
+
+The versions of dafny being run are set in the `tests.yml` file. The versions tested
+must be recent enough to support the new CLI syntax, so 3.11ff. Also, if 
+verification logging is desired, the version must be at least that of 3/18/2023 when
+the logging parameters were implemented in the new CLI.
+
+Testing can be run on older versions if (a) the lit macros like `%verify` are redefined using
+old CLI syntax and (b) the runtime testing tests are rewritten to not use `dafny run`.

Scripts/pydiff.py

@@ -0,0 +1,99 @@
+#!/usr/bin/env python
+"""
+Simple driver around python's difflib that implements a basic ``diff`` like
+tool. This exists to provide a simple ``diff`` like tool that will run on
+Windows where only the ``fc`` tool is available.
+"""
+import argparse
+import difflib
+import os
+import sys
+
+def main(args):
+    parser = argparse.ArgumentParser(formatter_class=argparse.RawDescriptionHelpFormatter,
+                                     description=__doc__
+                                    )
+    # Open in binary mode so python doesn't try and do
+    # universal line endings for us.
+    parser.add_argument('from-file',
+                        type=argparse.FileType('rb'),
+                       )
+    parser.add_argument('to-file',
+                        type=argparse.FileType('rb'),
+                       )
+    parser.add_argument('-U','--unified=',
+                        type=int,
+                        default=3,
+                        help='Number of context lines to show. '
+                             'Default %(default)s'
+                       )
+    parser.add_argument('--strip-trailing-cr',
+                        action='store_true',
+                        help='strip trailing carriage return when comparing'
+                       )
+    parser.add_argument('--ignore-all-space','-w',
+                        action='store_true',
+                        help='Ignore all whitespace characters when comparing'
+                       )
+
+    parsedArgs = parser.parse_args(args)
+    fromFile, fromFileName = preProcess(getattr(parsedArgs,'from-file'),
+                                        parsedArgs.strip_trailing_cr,
+                                        parsedArgs.ignore_all_space
+                                       )
+    toFile, toFileName = preProcess(getattr(parsedArgs,'to-file'),
+                                    parsedArgs.strip_trailing_cr,
+                                    parsedArgs.ignore_all_space
+                                   )
+    result = difflib.unified_diff(fromFile,
+                                  toFile,
+                                  fromFileName,
+                                  toFileName,
+                                  n=getattr(parsedArgs,'unified='),
+                                 )
+    # Force lazy computation to happen now
+    result = list(result)
+
+    if len(result) == 0:
+        # Files are identical
+        return 0
+    else:
+        for l in result:
+            sys.stdout.write(l)
+        return 1
+
+def preProcess(openFile, stripTrailingCR=False, ignoreAllSpace=False):
+    """
+    Helper function to read lines in a file and do any necessary
+    pre-processing
+    """
+    original = openFile.readlines()
+
+    # Translation table deletes white space characters Note we don't remove
+    # newline characters because this will create a mess when outputting the
+    # diff. Is this the right behaviour?
+    deleteChars=' \t'
+    if sys.version_info.major  >= 3:
+        translationTable = str.maketrans('','', deleteChars)
+
+    copy = [ ]
+    for line in original:
+        newLine = str(line.decode())
+
+        if stripTrailingCR:
+            if newLine[-2:] == '\r\n' or newLine[-2:] == '\n\r':
+                newLine = newLine[:-2] + '\n'
+
+        if ignoreAllSpace:
+            newLine = newLine.translate(translationTable)
+
+        copy.append(newLine)
+
+    return (copy, openFile.name)
+
+def getFileName(openFile):
+    return openFile.name
+
+if __name__ == '__main__':
+    sys.exit(main(sys.argv[1:]))
+

Scripts/test-exit.py

@@ -0,0 +1,33 @@
+## This small script takes as first argument a test indicator
+## and the rest of the arguments are a command to run, with its
+## command-line arguments.
+## The script runs the command and then if the first argument is
+## (1) -any -- returns success, ignoring the exit code of the command
+## (2) -z  -- returns success iff the exit code is non-zero
+## (3) some integer literal -- return success iff the exit code 
+##     matches the given integer
+## (4) -skip -- does not run the command and just exits with success
+
+import sys
+import subprocess
+
+arg = sys.argv[1]
+if arg == "-skip":
+    print( 'Skipping' )
+    exit(0)
+
+p = subprocess.run( sys.argv[2:] )
+
+if arg == "-any":
+    exit(0)
+if arg == "-z":
+    if p.returncode == 0 :
+        print( 'Expected non-zero exit code' )
+        exit(1)
+    else:
+        exit(0)
+if p.returncode != int(arg) :
+    print( 'Expected exit code', arg, ', actual result is', p.returncode )
+    exit(1)
+
+exit(0)

examples/Collections/Arrays/BinarySearch.dfy

@@ -1,12 +1,12 @@
-// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %run "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK-L: [-6, 0, 1, 3, 7, 7, 9]
 // CHECK-NEXT-L: 3
 
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT 
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT 
+ *******************************************************************************/
 
 include "../../../src/Relations.dfy"
 include "../../../src/Collections/Arrays/BinarySearch.dfy"
@@ -20,14 +20,14 @@ module BinarySearchExamples {
   import opened Seq.MergeSort
   import opened Relations
 
-  lemma SortedByLessThanOrEqualTo(s: seq<int>) 
+  lemma SortedByLessThanOrEqualTo(s: seq<int>)
     requires SortedBy(s, (x, y) => x <= y)
     ensures SortedBy(s, (x, y) => x < y || x == y)
   {}
 
   method {:vcs_split_on_every_assert} SortAndSearch() {
     var input := [1, 7, 7, 3, 9, 0, -6];
-    
+
     var sortedInput := MergeSortBy(input, (x, y) => x <= y);
     print sortedInput, "\n";
 

examples/FileIO/ReadBytesFromFile.dfy

@@ -1,13 +1,13 @@
 /*******************************************************************************
-*  Copyright by the contributors to the Dafny Project
-*  SPDX-License-Identifier: MIT
-*******************************************************************************/
+ *  Copyright by the contributors to the Dafny Project
+ *  SPDX-License-Identifier: MIT
+ *******************************************************************************/
 
-// RUN: %dafny /compile:0 "%s"
+// RUN: %verify "%s"
 
-// RUN: %baredafny run --no-verify --target:cs "%s" --input "%S/../../src/FileIO/FileIO.cs" -- "%S/data.txt" "System.ArgumentException:"
-// RUN: %baredafny run --no-verify --target:java "%s" --input "%S/../../src/FileIO/FileIO.java" -- "%S/data.txt" "java.io.IOException:"
-// RUN: %baredafny run --no-verify --target:js "%s" --input "%S/../../src/FileIO/FileIO.js" -- "%S/data.txt" "Error: ENOENT"
+// #RUN: %run --no-verify --unicode-char:false --target:cs "%s" --input "%S/../../src/FileIO/FileIO.cs" -- "%S/data.txt" "System.ArgumentException:"
+// #RUN: %run --no-verify --unicode-char:false --target:java "%s" --input "%S/../../src/FileIO/FileIO.java" -- "%S/data.txt" "java.io.IOException:"
+// #RUN: %run --no-verify --unicode-char:false --target:js "%s" --input "%S/../../src/FileIO/FileIO.js" -- "%S/data.txt" "Error: ENOENT"
 
 include "../../src/FileIO/FileIO.dfy"
 
@@ -20,7 +20,7 @@ module ReadBytesFromFile {
     var dataPath := args[1];
     var expectedErrorPrefix := args[2];
 
-    // Happy path: read from the data file, and check that we see the expected content.
+      // Happy path: read from the data file, and check that we see the expected content.
     {
       var expectedStr := "Hello world\nGoodbye\n";
       // This conversion is safe only for ASCII values. For Unicode conversions, see the Unicode modules.
@@ -33,7 +33,7 @@ module ReadBytesFromFile {
       expect readBytes == expectedBytes, "read unexpected byte sequence";
     }
 
-    // Failure path: attempting to read from a blank file path should never work.
+      // Failure path: attempting to read from a blank file path should never work.
     {
       var res := FileIO.ReadBytesFromFile("");
       expect res.Failure?, "unexpected success";