Incorporate heapster-saw into saw-script

.github/ci.sh → .github/ci-heapster.sh

@@ -46,7 +46,7 @@ setup_dist_bins() {
   fi
   extract_exe "saw" "dist/bin"
   export PATH=$PWD/dist/bin:$PATH
-  echo "$PWD/dist/bin" >> "$GITHUB_PATH"
+  echo "$PWD/dist/bin" >> $GITHUB_PATH
   strip dist/bin/saw* || echo "Strip failed: Ignoring harmless error"
 }
 
@@ -105,6 +105,15 @@ install_yices() {
   rm -rf "yices$ext" "yices-$YICES_VERSION"
 }
 
+install_yasm() {
+  is_exe "$BIN" "yasm" && return
+  if [[ "$RUNNER_OS" = "Linux" ]]; then
+    sudo apt-get update -q && sudo apt-get install -y yasm
+  else
+    brew install yasm
+  fi
+}
+
 build() {
   ghc_ver="$(ghc --numeric-version)"
   cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
@@ -123,9 +132,9 @@ build() {
     if [[ "$RUNNER_OS" == "macOS" ]]; then
       echo "Working around a dylib issue on macos by removing the cache and trying again"
       cabal v2-clean
-      retry cabal v2-build "$@" "${pkgs[@]}"
+      retry cabal v2-build "$@" saw jss
     else
-      return 1
+      exit 1
     fi
   fi
 }

.github/workflows/heapster.yml

@@ -0,0 +1,93 @@
+name: SAWScript Heapster
+on:
+  push:
+    branches: [wip-heapster]
+  pull_request:
+    branches: [wip-heapster]
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        ghc: ["8.6.5", "8.8.4", "8.10.2"]
+    runs-on: ${{ matrix.os }}
+    name: SAWScript - GHC v${{ matrix.ghc }} - ${{ matrix.os }}
+    # continue-on-error controls whether a failed job should cause a failed
+    # workflow notification email to be sent to the committer.
+    continue-on-error: "${{ matrix.ghc == '8.8.4' || matrix.ghc == '8.10.2' }}"
+    env:
+      OCAML_VERSION: 4.09.1
+      # also change in setup-ocaml step based on value of opamVersion:
+      # https://github.com/avsm/setup-ocaml/blob/v1.1.2/src/installer.ts#L56
+      SETUP_OCAML_ACTION_VERSION: 1.1.2
+      COQBITS_VERSION: 1.0.0
+    steps:
+      - uses: actions/checkout@v2
+      - run: |
+          git config --global url.https://github.com/.insteadOf git@github.com:
+          git submodule update --init
+          git -C deps/abcBridge submodule update --init
+
+      - name: Cache ~/.opam
+        uses: actions/cache@v2
+        with:
+          path: ~/.opam
+          key: ocaml-coqbits-${{ runner.os }}-${{ env.OCAML_VERSION }}-${{ env.SETUP_OCAML_ACTION_VERSION }}-${{ env.COQBITS_VERSION }}
+      - name: Set up ocaml and opam
+        uses: avsm/setup-ocaml@v1.1.2
+        with:
+          ocaml-version: ${{ env.OCAML_VERSION }}
+      - name: Install coq-bits
+        shell: bash
+        run: |
+          opam repo add coq-released https://coq.inria.fr/opam/released
+          opam install --unlock-base -y "coq-bits=$COQBITS_VERSION"
+
+      - uses: actions/setup-haskell@v1
+        id: setup-haskell
+        with:
+          ghc-version: ${{ matrix.ghc }}
+          enable-stack: true
+
+      - uses: actions/cache@v2
+        name: Cache cabal store
+        with:
+          path: |
+            ${{ steps.setup-haskell.outputs.cabal-store }}
+            dist-newstyle
+          key: cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles('**/cabal.GHC-*') }}-${{ github.sha }}
+          restore-keys: |
+            cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles('**/cabal.GHC-*') }}
+
+      - shell: bash
+        run: .github/ci-heapster.sh build_abc
+
+      - shell: bash
+        run: .github/ci-heapster.sh build
+
+      - shell: bash
+        run: .github/ci-heapster.sh setup_dist_bins
+
+      - run: git submodule update --init deps/saw-core-coq
+      - name: Build deps/saw-core-coq/coq
+        shell: bash
+        working-directory: deps/saw-core-coq/coq
+        run: |
+          eval $(opam env)
+          make -j2
+
+      - shell: bash
+        run: .github/ci-heapster.sh install_system_deps
+        env:
+          Z3_VERSION: "4.8.8"
+          CVC4_VERSION: "4.1.8"
+          YICES_VERSION: "2.6.2"
+
+      - name: Build deps/heapster-saw/examples
+        shell: bash
+        working-directory: deps/heapster-saw/examples
+        run: |
+          eval $(opam env)
+          make -j2

.gitmodules

@@ -40,6 +40,12 @@
 [submodule "deps/what4"]
 	path = deps/what4
 	url = https://github.com/GaloisInc/what4.git
+[submodule "deps/heapster-saw"]
+	path = deps/heapster-saw
+	url = https://github.com/GaloisInc/heapster-saw.git
 [submodule "deps/argo"]
 	path = deps/argo
 	url = https://github.com/galoisinc/argo
+[submodule "deps/language-rust"]
+	path = deps/language-rust
+	url = https://github.com/harpocrates/language-rust.git