Change saw-core tuple representation.

.github/ci.sh

@@ -103,7 +103,6 @@ haddock() {
     saw:saw-core-sbv
     saw:saw-core-aig
     saw:saw-core-coq
-    saw:heapster
     saw:saw-central
     saw:saw-script
     saw:saw-server

.github/workflows/ci.yml

@@ -194,7 +194,6 @@ jobs:
             cryptol-saw-core-tests
             crux-mir-comp-tests
             saw-core-coq-tests
-            heapster-prover-tests
           dest: dist-tests
 
       # In the next 2 steps, we upload to different names depending on whether
@@ -470,94 +469,6 @@ jobs:
           publish_dir: gh-pages
           keep_files: true
 
-  mr-solver-tests:
-    needs: [build]
-    strategy:
-      fail-fast: false
-      matrix:
-        os: [ubuntu-24.04, macos-14]
-    runs-on: ${{ matrix.os }}
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          submodules: true
-
-      - shell: bash
-        run: .github/ci.sh install_system_deps
-        env:
-          BUILD_TARGET_OS: ${{ matrix.os }}
-          BUILD_TARGET_ARCH: ${{ runner.arch }}
-
-      - uses: actions/download-artifact@v4
-        with:
-          name: "${{ matrix.os }}-bins"
-          path: dist/bin
-
-      - name: Update PATH to include SAW
-        shell: bash
-        run: |
-          chmod +x dist/bin/*
-          echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH
-
-      - working-directory: examples/mr_solver
-        shell: bash
-        run: |
-          saw monadify.saw
-          saw mr_solver_unit_tests.saw
-
-  heapster-tests:
-    needs: [build]
-    strategy:
-      fail-fast: false
-      matrix:
-        os: [ubuntu-24.04, macos-14]
-    runs-on: ${{ matrix.os }}
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          submodules: true
-
-      - shell: bash
-        run: .github/ci.sh install_system_deps
-        env:
-          BUILD_TARGET_OS: ${{ matrix.os }}
-          BUILD_TARGET_ARCH: ${{ runner.arch }}
-
-      - uses: actions/download-artifact@v4
-        with:
-          name: "${{ matrix.os }}-bins"
-          path: dist/bin
-
-      - name: Update PATH to include SAW
-        shell: bash
-        run: |
-          chmod +x dist/bin/*
-          echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH
-
-      - uses: ocaml/setup-ocaml@v3
-        with:
-          ocaml-compiler: "4.14"
-
-      - run: opam repo add coq-released https://coq.inria.fr/opam/released
-
-      - run: opam install -y coq=8.15.2 coq-bits=1.1.0
-
-        # If you change the entree-specs commit below, make sure you update the
-        # documentation in saw-core-coq/README.md accordingly.
-      - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#f104f6b3e6fe5987d543d90265cdc52f532de5fe
-
-      # FIXME: the following steps generate Coq libraries for the SAW core to
-      # Coq translator and builds them; if we do other Coq tests, these steps
-      # should become their own build artifact, to avoid re-compiling the Coq
-      # libraries
-      - working-directory: saw-core-coq/coq
-        shell: bash
-        run: opam exec -- make -j
-
-      - working-directory: heapster/examples
-        shell: bash
-        run: opam exec -- make -j
-
   crux-mir-comp-tests:
     needs: [build]
     strategy:
@@ -1092,7 +1003,6 @@ jobs:
     runs-on: ubuntu-24.04
     needs:
       - build
-      - heapster-tests
       - crux-mir-comp-tests
       - saw-remote-api-tests
       - cabal-test

CONTRIBUTING.md

@@ -255,8 +255,6 @@ The top-level repository directories are:
   solver queries using the [What4](https://github.com/GaloisInc/what4)
   library.
 
-* `heapster` - The Heapster tool.
-
 * `saw-central` - A library containing the bulk of SAW.
 
 * `saw-script` - A library containing the SAWScript interpreter.

build.sh

@@ -84,8 +84,7 @@ tgt_build() {
                 test-suite:integration-tests test-suite:saw-core-tests \
                 test-suite:crux-mir-comp-tests \
                 test-suite:cryptol-saw-core-tests \
-                test-suite:saw-core-coq-tests \
-                test-suite:heapster-prover-tests
+                test-suite:saw-core-coq-tests
 
     echo "rm -rf bin && mkdir bin"
     rm -rf bin && mkdir bin

cabal.project

@@ -42,11 +42,6 @@ packages:
     deps/rme/rme
     deps/rme/rme-what4
 
-source-repository-package
-    type: git
-    location: https://github.com/eddywestbrook/hobbits.git
-    tag: 70963e0e3eba2b16f6fc030acb582e8100955e47
-
 -- enable ghc >= 9.8's additional build parallelism
 semaphore: true
 

crucible-mir-comp/src/Mir/Compositional/Convert.hs

@@ -156,7 +156,6 @@ termToReg sym varMap term shp0 = do
   where
     go :: forall tp'. TypeShape tp' -> SValue sym -> IO (RegValue sym tp')
     go shp sv = case (shp, sv) of
-        (UnitShape _, SAW.VUnit) -> return ()
         (PrimShape _ BaseBoolRepr, SAW.VBool b) -> return b
         (PrimShape _ (BaseBVRepr w), SAW.VWord (W4.DBV e))
           | Just Refl <- testEquality (W4.exprType e) (BaseBVRepr w) -> return e
@@ -167,8 +166,8 @@ termToReg sym varMap term shp0 = do
                 _ -> fail $ "termToReg: type error: need to produce " ++ show (shapeType shp) ++
                     ", but simulator returned a vector containing " ++ show x
             buildBitVector w bits
-        (TupleShape _ elems, _) -> do
-            svs <- reverse <$> tupleToListRev (length elems) [] sv
+        (TupleShape _ elems, SAW.VTuple thunks) -> do
+            svs <- mapM SAW.force $ toList thunks
             buildMirAggregate sym elems svs $ \_ _ shp' sv' -> go shp' sv'
         (ArrayShape (M.TyArray _ n) _ shp', SAW.VVector thunks) -> do
             svs <- mapM SAW.force $ toList thunks
@@ -191,21 +190,6 @@ termToReg sym varMap term shp0 = do
         _ -> error $ "termToReg: type error: need to produce " ++ show (shapeType shp) ++
             ", but simulator returned " ++ show sv
 
-    -- | Convert an `SValue` tuple (built from nested `VPair`s) into a list of
-    -- the inner `SValue`s, in reverse order.
-    tupleToListRev :: Int -> [SValue sym] -> SValue sym -> IO [SValue sym]
-    tupleToListRev 2 acc (SAW.VPair x y) = do
-        x' <- SAW.force x
-        y' <- SAW.force y
-        return $ y' : x' : acc
-    tupleToListRev n acc (SAW.VPair x xs) | n > 2 = do
-        x' <- SAW.force x
-        xs' <- SAW.force xs
-        tupleToListRev (n - 1) (x' : acc) xs'
-    tupleToListRev n _ _ | n < 2 = error $ "bad tuple size " ++ show n
-    tupleToListRev n _ v = error $ "termToReg: expected tuple of " ++ show n ++
-        " elements, but got " ++ show v
-
     -- | Build a bitvector from a vector of bits.  The length of the vector is
     -- required to match `tw`.
     buildBitVector :: forall tw. (1 <= tw) =>