Merge branch 'master' into 2114-coverage-version-bump

This brings in the recent CI changes and particularly #2118.

Author: sauclovian-g

.github/workflows/ci.yml

@@ -187,12 +187,21 @@ jobs:
             prover_tests
           dest: dist-tests
 
-      - uses: actions/upload-artifact@v2
-        if: "matrix.ghc == '9.4.8'"
+      # In the next 2 steps, we upload to different names depending on whether
+      # the binaries were compiled using HPC or not. This is done to ensure that
+      # the HPC-enabled binaries do not clobber the non-HPC-enabled binaries.
+      - uses: actions/upload-artifact@v4
+        if: matrix.ghc == '9.4.8' && matrix.hpc == false
         with:
           path: dist-tests
           name: dist-tests-${{ matrix.os }}
 
+      - uses: actions/upload-artifact@v4
+        if: matrix.ghc == '9.4.8' && matrix.hpc == true
+        with:
+          path: dist-tests
+          name: dist-tests-${{ matrix.os }}-hpc
+
       - shell: bash
         run: .github/ci.sh setup_dist_bins
 
@@ -238,23 +247,23 @@ jobs:
       # distribution version matches the HPC version, the HPC build artifacts do
       # not clobber the non-HPC distribution artifacts.
       - if: matrix.ghc == '9.4.8' && matrix.hpc == false
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }})
           path: "${{ steps.config.outputs.name }}.tar.gz*"
           if-no-files-found: error
           retention-days: ${{ needs.config.outputs.retention-days }}
 
       - if: matrix.ghc == '9.4.8' && matrix.hpc == false
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           name: ${{ steps.config.outputs.name }}-with-solvers (GHC ${{ matrix.ghc }})
           path: "${{ steps.config.outputs.name }}-with-solvers.tar.gz*"
           if-no-files-found: error
           retention-days: ${{ needs.config.outputs.retention-days }}
 
       - if: matrix.ghc == '9.4.8' && matrix.run-tests && matrix.hpc == false
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           path: dist/bin
           name: ${{ matrix.os }}-bins
@@ -264,7 +273,7 @@ jobs:
         run: .github/ci.sh collect_hpc_files
 
       - if: matrix.hpc == true
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v4
         with:
           path: hpc.tar.gz
           name: ${{ matrix.os }}-hpc.tar.gz
@@ -296,7 +305,7 @@ jobs:
           BUILD_TARGET_OS: ${{ matrix.os }}
           BUILD_TARGET_ARCH: ${{ runner.arch }}
 
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         with:
           name: "${{ matrix.os }}-bins"
           path: dist/bin
@@ -331,7 +340,7 @@ jobs:
           BUILD_TARGET_OS: ${{ matrix.os }}
           BUILD_TARGET_ARCH: ${{ runner.arch }}
 
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         with:
           name: "${{ matrix.os }}-bins"
           path: dist/bin
@@ -398,7 +407,7 @@ jobs:
           BUILD_TARGET_OS: ${{ matrix.os }}
           BUILD_TARGET_ARCH: ${{ runner.arch }}
 
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         with:
           name: "${{ matrix.os }}-bins"
           path: dist/bin
@@ -461,7 +470,7 @@ jobs:
           BUILD_TARGET_OS: ${{ matrix.os }}
           BUILD_TARGET_ARCH: ${{ runner.arch }}
 
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         with:
           name: "${{ matrix.os }}-bins"
           path: dist/bin
@@ -474,7 +483,7 @@ jobs:
         if: runner.os != 'Windows'
         run: chmod +x bin/*
 
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         with:
           name: dist-tests-${{ matrix.os }}
           path: dist-tests
@@ -554,12 +563,12 @@ jobs:
           BUILD_TARGET_OS: ${{ matrix.os }}
           BUILD_TARGET_ARCH: ${{ runner.arch }}
 
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         with:
-          name: dist-tests-${{ matrix.os }}
+          name: dist-tests-${{ matrix.os }}-hpc
           path: dist-tests
 
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         with:
           name: "${{ matrix.os }}-hpc.tar.gz"
 
@@ -609,7 +618,7 @@ jobs:
         run: |
           ./compute-coverage.sh
 
-      - uses: actions/upload-artifact@v2
+      - uses: actions/upload-artifact@v4
         with:
           path: hpc-html
           name: coverage-html-${{ github.event.number }}
@@ -755,7 +764,7 @@ jobs:
           mkdir -p s2nTests/bin
 
       - name: Download previously-built SAW
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: "${{ matrix.os }}-bins"
           path: ./s2nTests/bin
@@ -809,7 +818,7 @@ jobs:
           mkdir -p exercises/bin
 
       - name: Download previously-built SAW
-        uses: actions/download-artifact@v2
+        uses: actions/download-artifact@v4
         with:
           name: "${{ matrix.os }}-bins"
           path: ./exercises/bin

.gitmodules

@@ -49,3 +49,6 @@
 [submodule "deps/lmdb"]
 	path = deps/lmdb
 	url = https://github.com/GaloisInc/lmdb.git
+[submodule "deps/mir-json"]
+	path = deps/mir-json
+	url = https://github.com/GaloisInc/mir-json.git

CHANGES.md

@@ -1,3 +1,10 @@
+# next -- TBA
+
+## Bug fixes
+
+* Counterexamples including SMT arrays are now printed with the array
+  contents instead of placeholder text.
+
 # Version 1.2 -- 2024-08-30
 
 ## New Features

README.md

@@ -88,6 +88,26 @@ will be possible for all language constructs. There are various
 instructions that are not supported during verification. However,
 any failure during `llvm_load_module` should be considered a bug.
 
+## Notes on Rust
+
+SAW has experimental support for analyzing Rust programs. To do so, one must
+compile Rust code using [`mir-json`](https://github.com/GaloisInc/mir-json), a
+tool which compiles Rust code to a machine-readable, JSON-based format.
+Note that:
+
+* Each version of SAW understands the JSON output of a particular version of
+  `mir-json`, so make sure that you build the version `mir-json` that is
+  included in the `mir-json` submodule (located in `deps/mir-json`).
+* Moreover, SAW requires slightly modified versions of the Rust standard
+  libraries that are suited to verification purposes. SAW consults the value
+  of the `SAW_RUST_LIBRARY_PATH` environment variable to determine where to
+  look for these modified standard libraries.
+
+For complete instructions on how to install `mir-json`, the modified Rust
+standard libraries, and how to defined the `SAW_RUST_LIBRARY_PATH` environment
+variable, follow the instructions
+[here](https://github.com/GaloisInc/mir-json#installation-instructions).
+
 ## Notes on Windows
 
 If you have trouble loading the SAW REPL on Windows, try invoking it

deps/mir-json

@@ -1812,15 +1812,62 @@ In order to verify Rust code, SAW analyzes Rust's MIR (mid-level intermediate
 representation) language. In particular, SAW analyzes a particular form of MIR
 that the [`mir-json`](https://github.com/GaloisInc/mir-json) tool produces. You
 will need to intall `mir-json` and run it on Rust code in order to produce MIR
-JSON files that SAW can load (see [this section](#loading-mir)).
+JSON files that SAW can load (see [this section](#loading-mir)). You will also
+need to use `mir-json` to build custom versions of the Rust standard libraries
+that are more suited to verification purposes.
+
+If you are working from a checkout of the `saw-script` repo, you can install
+the `mir-json` tool and the custom Rust standard libraries by performing the
+following steps:
+
+1. Clone the [`crucible`](https://github.com/GaloisInc/crucible) and `mir-json`
+   submodules like so:
+
+   ```
+   $ git submodule update deps/crucible deps/mir-json
+   ```
+
+2. Navigate to the `mir-json` submodule:
+
+   ```
+   $ cd deps/mir-json
+   ```
+
+3. Follow the instructions laid out in the [`mir-json` installation
+   instructions](https://github.com/GaloisInc/mir-json#installation-instructions)
+   in order to install `mir-json`.
+
+4. Navigate to the
+   [`crux-mir`](https://github.com/GaloisInc/crucible/tree/master/crux-mir)
+   subdirectory of the `crucible` submodule:
+
+   ```
+   $ cd ../crucible/crux-mir/
+   ```
+
+5. Run the `translate_libs.sh` script:
+
+   ```
+   $ ./translate_libs.sh
+   ```
+
+   This will compile the custom versions of the Rust standard libraries using
+   `mir-json`, placing the results under the `rlibs` subdirectory.
+
+6. Finally, define a `SAW_RUST_LIBRARY_PATH` environment variable that points
+   to the newly created `rlibs` subdirectory:
+
+   ```
+   $ export SAW_RUST_LIBRARY_PATH=<...>/crucible/crux-mir/rlibs
+   ```
 
 For `cargo`-based projects, `mir-json` provides a `cargo` subcommand called
 `cargo saw-build` that builds a JSON file suitable for use with SAW. `cargo
 saw-build` integrates directly with `cargo`, so you can pass flags to it like
 any other `cargo` subcommand. For example:
 
 ```
-$ export SAW_RUST_LIBRARY_PATH=<...>
+# Make sure that SAW_RUST_LIBRARY_PATH is defined, as described above
 $ cargo saw-build <other cargo flags>
 <snip>
 linking 11 mir files into <...>/example-364cf2df365c7055.linked-mir.json
@@ -1840,7 +1887,7 @@ Note that:
 `rustc` accepts. For example:
 
 ```
-$ export SAW_RUST_LIBRARY_PATH=<...>
+# Make sure that SAW_RUST_LIBRARY_PATH is defined, as described above
 $ saw-rustc example.rs <other rustc flags>
 <snip>
 linking 11 mir files into <...>/example.linked-mir.json

doc/manual/manual.md

@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff

doc/manual/manual.pdf

@@ -0,0 +1,18 @@
+# The current checked-in test.bc was generated by:
+#    Apple clang version 15.0.0 (clang-1500.1.0.2.5)
+#    Target: arm64-apple-darwin22.6.0
+#    Thread model: posix
+#    InstalledDir: /Library/Developer/CommandLineTools/usr/bin
+# but neither the target nor the clang/llvm version is expected to be
+# significant.
+CC = clang
+CFLAGS = -g -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test2049/.gitignore

@@ -0,0 +1,2 @@
+import Array
+type Table = Array [8] [8]

intTests/test2049/Makefile

@@ -0,0 +1,12 @@
+#include <stdint.h>
+
+static uint8_t table[256];
+
+void assign(uint8_t k, uint8_t v) {
+   table[k] = v;
+}
+
+void zero(uint8_t k) {
+  assign(k, 0);
+}
+

intTests/test2049/Test.cry

@@ -0,0 +1,23 @@
+ Loading file "test.saw"
+ Assume override assign
+ Verifying zero ...
+ Simulating zero ...
+ Registering overrides for `assign`
+   variant `Symbol "assign"`
+ Matching 1 overrides of  assign ...
+ Branching on 1 override variants of assign ...
+ Applied override! assign
+ Checking proof obligations zero ...
+ Subgoal failed: zero test.saw:60:1: error: in ghost_value
+Literal equality postcondition
+
+ SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 334}
+ ----------Counterexample----------
+   zero::table: [1 := 1, <default> := 0]
+   zero::k: 1
+ ----------------------------------
+ Stack trace:
+"llvm_verify" (test.saw:60:1-60:12)
+Proof failed.
+
+FAILED

intTests/test2049/test.bc

@@ -0,0 +1,23 @@
+ Loading file "test.saw"
+ Assume override assign
+ Verifying zero ...
+ Simulating zero ...
+ Registering overrides for `assign`
+   variant `Symbol "assign"`
+ Matching 1 overrides of  assign ...
+ Branching on 1 override variants of assign ...
+ Applied override! assign
+ Checking proof obligations zero ...
+ Subgoal failed: zero test.saw:60:1: error: in ghost_value
+Literal equality postcondition
+
+ SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 334}
+ ----------Counterexample----------
+   zero::table: [0 := 0, <default> := 1]
+   zero::k: 1
+ ----------------------------------
+ Stack trace:
+"llvm_verify" (test.saw:60:1-60:12)
+Proof failed.
+
+FAILED