Merge branch 'master' into print-sharing-control

.github/ci.sh

@@ -111,12 +111,10 @@ build() {
   cabal v2-update
   cabal v2-configure -j --enable-tests
   git status --porcelain
-  pkgs=(saw)
   if $IS_WIN; then
-    echo "flags: -builtin-abc" >> cabal.project.local
-    echo "constraints: cryptol-saw-core -build-css" >> cabal.project.local
+    pkgs=(saw)
   else
-    pkgs+=(saw-remote-api)
+    pkgs=(saw saw-remote-api)
   fi
   tee -a cabal.project.local > /dev/null < cabal.project.ci
   if ! retry cabal v2-build "$@" "${pkgs[@]}"; then
@@ -163,7 +161,6 @@ build_cryptol() {
 bundle_files() {
   mkdir -p dist dist/{bin,doc,examples,include,lib}
 
-  cp deps/abcBridge/abc-build/copyright.txt dist/ABC_LICENSE
   cp LICENSE README.md dist/
   $IS_WIN || chmod +x dist/bin/*
 

.github/workflows/ci.yml

@@ -10,6 +10,7 @@ on:
 
 env:
   CACHE_VERSION: 1
+
   # Solver versions - also update in the following locations:
   # ./saw/Dockerfile
   # ./saw-remote-api/Dockerfile
@@ -18,6 +19,8 @@ env:
   CVC4_VERSION: "4.1.8"
   YICES_VERSION: "2.6.2"
 
+  OCAML_VERSION: 4.09.x
+
 jobs:
   config:
     runs-on: ubuntu-latest
@@ -58,15 +61,10 @@ jobs:
       fail-fast: false
       matrix:
         os: [ubuntu-18.04]
-        ghc: ["8.6.5", "8.8.4", "8.10.3"]
+        ghc: ["8.8.4", "8.10.3"]
         include:
-          - os: macos-latest
-            ghc: "8.6.5"
           - os: macos-latest
             ghc: "8.8.4"
-          - os: windows-latest
-            ghc: "8.6.5"
-        exclude:
           - os: windows-latest
             ghc: "8.8.4"
     outputs:
@@ -126,15 +124,15 @@ jobs:
           dest: dist-tests
 
       - if: |
-          matrix.ghc == '8.6.5' &&
+          matrix.ghc == '8.8.4' &&
           runner.os != 'Windows'
         uses: actions/upload-artifact@v2
         with:
           path: ${{ steps.abc.outputs.path }}
           name: abc-${{ runner.os }}
 
       - uses: actions/upload-artifact@v2
-        if: "matrix.ghc == '8.6.5'"
+        if: "matrix.ghc == '8.8.4'"
         with:
           path: dist-tests
           name: dist-tests-${{ matrix.os }}
@@ -148,22 +146,22 @@ jobs:
       - shell: bash
         run: .github/ci.sh zip_dist $NAME
 
-      - if: matrix.ghc == '8.6.5' && needs.config.outputs.release == 'true'
+      - if: matrix.ghc == '8.8.4' && needs.config.outputs.release == 'true'
         shell: bash
         env:
           SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
           SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
         run: .github/ci.sh sign $NAME.tar.gz
 
-      - if: matrix.ghc == '8.6.5'
+      - if: matrix.ghc == '8.8.4'
         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 == '8.6.5'"
+      - if: "matrix.ghc == '8.8.4'"
         uses: actions/upload-artifact@v2
         with:
           path: dist/bin
@@ -175,6 +173,40 @@ jobs:
           name: "saw-${{ runner.os }}-${{ matrix.ghc }}"
           path: "dist/bin/saw"
 
+  ocaml-tests:
+    needs: [build]
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+
+      - shell: bash
+        run: .github/ci.sh install_system_deps
+
+      - uses: actions/download-artifact@v2
+        with:
+          name: "${{ runner.os }}-bins"
+          path: dist/bin
+
+      - uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: 4.09.x  # coq-bits claims to support < 4.10 only
+
+      - run: opam repo add coq-released https://coq.inria.fr/opam/released
+
+      - run: opam install --unlock-base -y coq=8.12.2 coq-bits=1.0.0
+
+      - working-directory: saw-core-coq/coq
+        run: PATH="$PWD/dist/bin:$PATH" opam exec -- make -j
+
+      - working-directory: heapster-saw/examples
+        run: PATH="$PWD/dist/bin:$PATH" opam exec -- make -j
+
   saw-remote-api-tests:
     runs-on: ${{ matrix.os }}
     needs: [build]
@@ -201,6 +233,12 @@ jobs:
           name: "${{ runner.os }}-bins"
           path: dist/bin
 
+      - if: runner.os != 'Windows'
+        uses: actions/download-artifact@v2
+        with:
+          path: dist/bin
+          name: abc-${{ runner.os }}
+
       - uses: actions/setup-python@v2
         with:
           python-version: '3.9'
@@ -214,6 +252,12 @@ jobs:
         run: |
           chmod +x dist/bin/*
           export PATH="$PWD/dist/bin:$PATH"
+          echo "$PWD/dist/bin" >> "$GITHUB_PATH"
+          abc -h || true
+          yices --version
+          yices-smt2 --version
+          saw --version
+          saw-remote-api --help
           ${{ matrix.test }}
 
   cabal-test:
@@ -256,18 +300,14 @@ jobs:
         if: "runner.os != 'Windows'"
         run: chmod +x dist/bin/*
 
-      - if: |
-          runner.os != 'Windows' &&
-          matrix.suite == 'integration_tests'
+      - if: runner.os != 'Windows'
         uses: actions/download-artifact@v2
         with:
           path: bin
           name: abc-${{ runner.os }}
 
       - shell: bash
-        if: |
-          runner.os != 'Windows' &&
-          matrix.suite == 'integration_tests'
+        if: runner.os != 'Windows'
         run: chmod +x bin/*
 
       - uses: actions/download-artifact@v2
@@ -308,9 +348,8 @@ jobs:
             cache: ghcr.io/galoisinc/cache-saw-remote-api
     steps:
       - uses: actions/checkout@v2
-      - run: |
-          git submodule update --init
-          git -C deps/abcBridge submodule update --init
+        with:
+          submodules: true
 
       - uses: rlespinasse/[email protected]
 
@@ -409,7 +448,7 @@ jobs:
           - hmac-failure
           - awslc
           - blst
-        ghc: ["8.6.5", "8.8.4", "8.10.3"]
+        ghc: ["8.8.4", "8.10.3"]
     steps:
       - uses: actions/checkout@v2
       - run: |
@@ -421,6 +460,11 @@ jobs:
           name: "saw-Linux-${{ matrix.ghc }}"
           path: ./s2nTests/bin
 
+      - uses: actions/download-artifact@v2
+        with:
+          path: ./s2nTests/bin
+          name: abc-${{ runner.os }}
+
       - shell: bash
         working-directory: s2nTests
         run: |
@@ -439,7 +483,7 @@ jobs:
         name: "s2n tests: ${{ matrix.s2n-target }}"
         working-directory: s2nTests
         run: |
-          chmod +x bin/saw
+          chmod +x bin/*
           make ${{ matrix.s2n-target }}
 
   # Indicates sufficient CI success for the purposes of mergify merging the pull
@@ -452,6 +496,7 @@ jobs:
     runs-on: ubuntu-latest
     needs:
       - build
+      - ocaml-tests
       - saw-remote-api-tests
       - cabal-test
       - build-push-image

.gitmodules

@@ -43,3 +43,6 @@
 [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

CHANGES.md

@@ -20,6 +20,35 @@ Several improvements have been made to JVM verification:
   "current" status, so that `enable_experimental` is no longer
   necessary for JVM verification.
 
+A new `enable_lax_pointer_ordering` function exists, which relaxes the
+restrictions that Crucible imposes on comparisons between pointers from
+different allocation blocks.
+
+## Changes
+
+* The linked-in version of ABC (based on the Haskell `abcBridge`
+  library) has been removed. During the original planning for this
+  removal, we marked commands based on this library as deprecated. In
+  the end, we replaced all of them except `cec` with Haskell
+  implementations, so no other commands have been removed, and the
+  following commands are now "current" again:
+
+    * `abc` (which now is the same as `w4_abc_verilog`)
+    * `load_aig`
+    * `save_aig`
+    * `save_aig_as_cnf`
+    * `bitblast`
+    * `write_aiger`
+    * `write_cnf`
+
+  We have also implemented a `w4_abc_aiger` command that writes a `Term`
+  in AIGER format and invokes ABC on it as an external process. This
+  should be very similar to the original `abc` command. Note that the
+  pure Haskell AIGER and CNF generation code has not been heavily tuned
+  for performance, and could likely be made more efficient. Please file
+  [issues](https://github.com/galoisinc/saw-script/issues) for
+  performance regressions you encounter!
+
 # Version 0.8
 
 ## New Features

README.md

@@ -86,7 +86,6 @@ build using `build.sh`; see
 [Manual Installation](#manual-installation) above. Key automatically
 downloaded dependencies include:
 
-* `deps/abcBridge/`:        [Haskell bindings for ABC](https://github.com/GaloisInc/abcBridge)
 * `deps/crucible/`:         [Crucible symbolic execution engine](https://github.com/GaloisInc/crucible)
 * `deps/cryptol/`:          [Cryptol](https://github.com/GaloisInc/cryptol)
 
@@ -129,7 +128,6 @@ systems and Windows systems end up with different package dependencies.
 Specifically, we remove lines for the following packages or flags:
 
 ```
-abcBridge
 cryptol-saw-core
 regex-posix
 saw-remote-api

build.sh

@@ -1,6 +1,5 @@
 #!/bin/bash
 git submodule update --init
-(cd deps/abcBridge && git submodule update --init)
 
 function install() {
   cp $(find dist-newstyle -type f -name $1 | sort -g | tail -1) bin/