Merge branch 'master' into T1985

GaloisInc · Dec 5, 2023 · 6782359 · 6782359
2 parents 17f0ed7 + 6ff9711
commit 6782359
Show file tree

Hide file tree

Showing 130 changed files with 3,174 additions and 1,036 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -1,5 +1,5 @@
 # Overall configuration notes:
-# - Artifact uploads for binaries are from GHC 9.2.7
+# - Artifact uploads for binaries are from GHC 9.2.8
 # - Builds for Ubuntu happen on 22.04. We also include a single configuration
 #   for 20.04 to increase our Linux coverage.
 # - Docker builds happen nightly, on manual invocation, and on release branch commits
@@ -78,36 +78,24 @@ jobs:
       matrix:
         os: [ubuntu-22.04, macos-12, windows-2019]
         cabal: ["3.10.1.0"]
-        ghc: ["8.10.7", "9.2.7", "9.4.4"]
+        ghc: ["9.2.8", "9.4.8", "9.6.3"]
         run-tests: [true]
         hpc: [false]
         include:
           # We include one job from an older Ubuntu LTS release to increase our
           # coverage of possible Linux configurations. Since we already run the
           # tests with the newest LTS release, we won't bother testing this one.
           - os: ubuntu-20.04
-            ghc: "9.2.7"
+            ghc: "9.2.8"
             cabal: "3.10.1.0"
             run-tests: false
             hpc: false
           # Include one job with HPC enabled
           - os: ubuntu-22.04
-            ghc: "9.4.4"
+            ghc: "9.4.8"
             cabal: "3.10.1.0"
             run-tests: true
             hpc: true
-        exclude:
-          # We exclude the GHC 8.10.7 job on Windows, as it is known to suffer
-          # from a hard-to-diagnose memory-related issue that does not affect
-          # later versions of GHC on Windows. (See
-          # https://github.com/GaloisInc/saw-script/issues/1961.) When we drop
-          # support for 8.10 entirely from SAW's support Window, we can remove
-          # this part of the matrix entirely.
-          - os: windows-2019
-            ghc: "8.10.7"
-            cabal: "3.10.1.0"
-            run-tests: true
-            hpc: false
     outputs:
       cabal-test-suites-json: ${{ steps.cabal-test-suites.outputs.targets-json }}
     steps:
@@ -183,7 +171,7 @@ jobs:
           dest: dist-tests
 
       - uses: actions/upload-artifact@v2
-        if: "matrix.ghc == '9.2.7'"
+        if: "matrix.ghc == '9.2.8'"
         with:
           path: dist-tests
           name: dist-tests-${{ matrix.os }}
@@ -200,14 +188,14 @@ jobs:
       - shell: bash
         run: .github/ci.sh zip_dist_with_solvers $NAME-with-solvers
 
-      - if: matrix.ghc == '9.2.7' && github.event.pull_request.head.repo.fork == false
+      - if: matrix.ghc == '9.2.8' && github.event.pull_request.head.repo.fork == false
         shell: bash
         env:
           SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
           SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
         run: .github/ci.sh sign $NAME.tar.gz
 
-      - if: matrix.ghc == '9.2.7' && github.event.pull_request.head.repo.fork == false
+      - if: matrix.ghc == '9.2.8' && github.event.pull_request.head.repo.fork == false
         shell: bash
         env:
           SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
@@ -217,7 +205,7 @@ jobs:
       ##########################################################################
       # We upload an archive containing SAW, and also and archive containing SAW
       # and the set of possible SMT solvers, but only for our "primary"
-      # distribution (currently: GHC 9.2.7).  These archives are utilized in
+      # distribution (currently: GHC 9.2.8).  These archives are utilized in
       # subsequent CI jobs, but are also published for external users, and are
       # therefore signed.
       #
@@ -232,23 +220,23 @@ jobs:
       # In the next 3 steps we check that `matrix.hpc == false` so that if the
       # distribution version matches the HPC version, the HPC build artifacts do
       # not clobber the non-HPC distribution artifacts.
-      - if: matrix.ghc == '9.2.7' && matrix.hpc == false
+      - if: matrix.ghc == '9.2.8' && matrix.hpc == false
         uses: actions/upload-artifact@v2
         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.2.7' && matrix.hpc == false
+      - if: matrix.ghc == '9.2.8' && matrix.hpc == false
         uses: actions/upload-artifact@v2
         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.2.7' && matrix.run-tests && matrix.hpc == false
+      - if: matrix.ghc == '9.2.8' && matrix.run-tests && matrix.hpc == false
         uses: actions/upload-artifact@v2
         with:
           path: dist/bin
@@ -726,7 +714,7 @@ jobs:
           - hmac-failure
           - awslc
           - blst
-        ghc: ["9.2.7"]
+        ghc: ["9.2.8"]
     steps:
       - uses: actions/checkout@v2
       - run: |
@@ -779,7 +767,7 @@ jobs:
     runs-on: ubuntu-22.04
     strategy:
       matrix:
-        ghc: ["9.2.7"]
+        ghc: ["9.2.8"]
     steps:
       - uses: actions/checkout@v2
       - run: |

diff --git a/.gitmodules b/.gitmodules
@@ -42,7 +42,7 @@
 	url = https://github.com/galoisinc/argo
 [submodule "deps/language-rust"]
 	path = deps/language-rust
-	url = https://github.com/harpocrates/language-rust.git
+	url = https://github.com/GaloisInc/language-rust.git
 [submodule "deps/language-sally"]
 	path = deps/language-sally
 	url = https://github.com/GaloisInc/language-sally

diff --git a/CHANGES.md b/CHANGES.md
@@ -17,6 +17,13 @@
   generating LLVM setup scripts for Cryptol FFI functions with the
   `llvm_ffi_setup` command. For more information, see the [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#verifying-cryptol-ffi-functions).
 
+* Ghost state is now supported with the JVM and MIR language backends:
+  * The `llvm_declare_ghost_state` command is now deprecated in favor of the
+    new `declare_ghost_state` command, as nothing about this command is
+    LLVM-specific.
+  * Add `jvm_ghost_value` and `mir_ghost_value` commands in addition to the
+    existing `llvm_ghost_value` command.
+
 # Version 1.0 -- 2023-06-26
 
 ## New Features

diff --git a/README.md b/README.md
@@ -43,7 +43,7 @@ To build SAWScript and related utilities from source:
   * Ensure that you have the `cabal` and `ghc` executables in your
     `PATH`. If you don't already have them, we recommend using `ghcup`
     to install them: <https://www.haskell.org/ghcup/>. We recommend
-    Cabal 3.4 or newer, and GHC 8.10, 9.2, or 9.4.
+    Cabal 3.10 or newer, and GHC 9.2, 9.4, or 9.6.
 
     (If you are using the GHC 9.2 series, make sure to use 9.2.6 or later
     to avoid [this bug](https://gitlab.haskell.org/ghc/ghc/-/issues/22491).)