Remove dependency on abcBridge

.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

@@ -201,6 +201,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 +220,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 +268,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 +316,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]
 
@@ -421,6 +428,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 +451,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

CHANGES.md

@@ -24,6 +24,31 @@ 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/

cabal.project

@@ -14,7 +14,6 @@ packages:
     deps/llvm-pretty-bc-parser
     deps/jvm-parser
     deps/aig
-    deps/abcBridge
     deps/cryptol
     deps/what4/what4
     deps/crucible/crucible

cryptol-saw-core/cryptol-saw-core.cabal

@@ -16,10 +16,6 @@ Description:
 extra-source-files:
     saw/Cryptol.sawcore
 
-flag build-css
-  description: Build the css executable
-  default: True
-
 library
   build-depends:
     aig,
@@ -54,15 +50,12 @@ library
   GHC-options: -Wall -Werror
 
 executable css
-  if !flag(build-css)
-     buildable: False
-
   other-modules:
     Paths_cryptol_saw_core
 
   build-depends:
+    aig,
     array,
-    abcBridge,
     base,
     bytestring,
     containers,

cryptol-saw-core/css/Main.hs

@@ -19,13 +19,16 @@ import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import           Cryptol.Utils.PP
 import           Cryptol.Utils.Logger (quietLogger)
 
+import qualified Data.AIG.CompactGraph as AIG
+import qualified Data.AIG.Interface as AIG
+import qualified Data.AIG.Operations as AIG
+
 import qualified Verifier.SAW.Cryptol as C
 import           Verifier.SAW.SharedTerm
 import qualified Verifier.SAW.Cryptol.Prelude as C
 import           Verifier.SAW.CryptolEnv (schemaNoUser, meSolverConfig)
 
 
-import qualified Data.ABC as ABC
 import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 
 import qualified Paths_cryptol_saw_core as Paths
@@ -120,8 +123,8 @@ processModule menv fout funcName = do
 
 writeAIG :: SharedContext -> FilePath -> Term -> IO ()
 writeAIG sc f t = do
-  BBSim.withBitBlastedTerm ABC.giaNetwork sc mempty t $ \be ls -> do
-  ABC.writeAiger f (ABC.Network be (ABC.bvToList ls))
+  BBSim.withBitBlastedTerm AIG.compactProxy sc mempty t $ \be ls -> do
+  AIG.writeAiger f (AIG.Network be (AIG.bvToList ls))
 
 extractCryptol :: SharedContext -> CM.ModuleEnv -> String -> IO Term
 extractCryptol sc modEnv input = do

doc/tutorial/code/des-cryptol2.saw

@@ -1,3 +1,3 @@
 import "DES.cry";
 let {{ thm key msg = decrypt key (encrypt key msg) == msg }};
-prove_print abc {{ thm }};
+prove_print w4_abc_verilog {{ thm }};

doc/tutorial/code/des3.saw

@@ -2,13 +2,13 @@ import "DES.cry";
 
 print "proving dec_enc...";
 let prop1 = {{ \key msg -> decrypt key (encrypt key msg) == msg }};
-dec_enc <- prove_print abc {{prop1}};
+dec_enc <- prove_print w4_abc_verilog {{prop1}};
 
 print dec_enc;
 
 print "proving enc_dec...";
 let prop2 = {{ \key msg -> encrypt key (decrypt key msg) == msg }};
-enc_dec <- prove_print abc {{prop2}};
+enc_dec <- prove_print w4_abc_verilog {{prop2}};
 
 print enc_dec;
 
@@ -24,7 +24,7 @@ prove_print do {
     unfolding ["dec3", "enc3"];
     simplify ss;
     print_goal;
-    abc;
+    w4_abc_verilog;
 } {{prop3}};
 
 print "proving enc3_dec3...";
@@ -34,5 +34,5 @@ prove_print do {
     unfolding ["dec3", "enc3"];
     simplify ss;
     print_goal;
-    abc;
+    w4_abc_verilog;
 } {{prop4}};

doc/tutorial/code/double.saw

@@ -3,7 +3,7 @@ double_imp <- llvm_extract l "double_imp";
 double_ref <- llvm_extract l "double_ref";
 let thm = {{ \x -> double_ref x == double_imp x }};
 
-r <- prove abc thm;
+r <- prove yices thm;
 print r;
 
 r <- prove yices thm;