Merge branch 'master' into at-doc-updates

.dockerignore

@@ -0,0 +1,20 @@
+*\#*
+*~
+.DS_Store
+.cabal-sandbox
+cabal.sandbox.config
+.ghc.environment.x86_64-darwin-*
+
+# vim swap files
+.*.swp
+.*.swo
+
+**/*.a
+**/*.o
+
+Dockerfile*
+
+**/.git
+**/.stack-work
+**/dist
+**/dist-newstyle

.gitmodules

@@ -25,9 +25,6 @@
 [submodule "deps/llvm-pretty-bc-parser"]
 	path = deps/llvm-pretty-bc-parser
 	url = https://github.com/GaloisInc/llvm-pretty-bc-parser.git
-[submodule "deps/llvm-verifier"]
-	path = deps/llvm-verifier
-	url = https://github.com/GaloisInc/llvm-verifier.git
 [submodule "deps/parameterized-utils"]
 	path = deps/parameterized-utils
 	url = https://github.com/GaloisInc/parameterized-utils.git

.travis.yml

@@ -17,29 +17,29 @@ git:
 
 matrix:
   include:
-    - env: CABALVER="2.4" GHCVER="8.6.3"
-      compiler: ": #GHC 8.6.3"
-      addons: {apt: {packages: [cabal-install-2.4,ghc-8.6.3], sources: [hvr-ghc]}}
-    - env: CABALVER="2.4" GHCVER="8.4.3"
-      compiler: ": #GHC 8.4.3"
-      addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.3], sources: [hvr-ghc]}}
-    - os: osx
-      env: CABALVER="2.4" GHCVER="8.6.3"
-      compiler: ": #GHC 8.6.3"
+    - env: CABALVER="2.4" GHCVER="8.6.5"
+      compiler: ": #GHC 8.6.5"
+      addons: {apt: {packages: [cabal-install-2.4,ghc-8.6.5], sources: [hvr-ghc]}}
+    - env: CABALVER="2.4" GHCVER="8.4.4"
+      compiler: ": #GHC 8.4.4"
+      addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.4], sources: [hvr-ghc]}}
+#    - os: osx
+#      env: CABALVER="2.4" GHCVER="8.6.5"
+#      compiler: ": #GHC 8.6.5"
 
 before_install:
-  - if [[ $TRAVIS_OS_NAME == 'osx' ]];
-    then
-        brew update;
-        brew install ghc;
-        brew install cabal-install;
-    fi
+#  - if [[ $TRAVIS_OS_NAME == 'osx' ]];
+#    then
+#        brew update;
+#        brew install ghc;
+#        brew install cabal-install;
+#    fi
   - unset CC
   - export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH
 
 script:
   - git submodule init
   - git submodule update
   - (cd deps/abcBridge && git submodule init && git submodule update)
-  - cabal update
-  - cabal new-build -j --disable-optimization
+  - cabal v2-update
+  - cabal v2-build -j --disable-optimization

CHANGES.md

@@ -1,3 +1,54 @@
+# Version 0.3
+
+* Java and LLVM verification has been overhauled to use the new Crucible
+  symbolic execution engine. Highlights include:
+
+    * New `crucible_llvm_verify` and `crucible_llvm_extract` commands
+      replace `llvm_verify` and `llvm_extract`, with a different
+      structure for specification blocks.
+
+    * LLVM verification tracks undefined behavior more carefully and has
+      a more sophisicated memory model. See the
+      [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#specification-based-verification)
+      for more.
+
+    * New, experimental `crucible_jvm_verify` and
+      `crucible_java_extract` commands will eventually replace
+      `java_verify` and `java_extract`. For the moment, the former two
+      are enabled with the `enable_experimental` command and the latter
+      two are enabled with `enable_deprecated`.
+
+    * More flexible specification language allows convenient description
+      of functions that allocate memory, return arbitrary values, expect
+      explicit aliasing, work with NULL pointers, cast between pointers
+      and integers, or work with opaque pointers.
+
+    * Ghost state is supported in LLVM verification, allowing reasoning
+      about certain complex or unavailable code.
+
+    * Verification of LLVM works for a larger subset of the language,
+      which particularly improves support for C++.
+
+* LLVM bitcode format support is greatly improved. Versions 3.5 to 7.0
+  are known to be mostly well-supported. We consider parsing failures
+  with any version newer than 3.5 to be a bug, so please report them on
+  [GitHub](https://github.com/GaloisInc/saw-script/issues/new).
+
+* Greatly improved error messages throughout.
+
+* Built against Cryptol 2.7.0.
+
+* New model counting commands `sharpSAT` and `approxmc` bind to the
+  external tools of the same name.
+
+* New proof script commands allow multiple goals and related proof
+  tactics. See the
+  [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#multiple-goals).
+
+* Can be built with Docker, and will be available on DockerHub.
+
+* Includes an Emacs mode.
+
 # Version 0.2-dev
 
 * Released under the 3-clause BSD license

Dockerfile

@@ -0,0 +1,30 @@
+FROM haskell:8.6 AS build
+USER root
+# TODO: install Yices, too (and CVC4?, Boolector?)
+RUN apt-get update \
+    && apt-get install -y wget libncurses-dev unzip \
+    && wget https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1-x64-debian-8.10.zip \
+    && unzip z3*.zip \
+    && mv z3-*/bin/z3 /usr/local/bin
+RUN useradd -m saw
+RUN su -c '/opt/cabal/bin/cabal v2-update' saw
+ADD . /home/saw
+RUN chown -R saw:saw /home/saw
+USER saw
+WORKDIR /home/saw
+RUN cabal v2-build
+WORKDIR /home/saw
+RUN mkdir -p rootfs/usr/local/bin \
+    && cp /usr/local/bin/z3 rootfs/usr/local/bin/z3 \
+    && cp dist-newstyle/build/*-linux/ghc-*/saw-script-*/build/saw/saw rootfs/usr/local/bin/saw
+USER root
+RUN chown -R root:root /home/saw/rootfs
+
+FROM debian:stretch-slim
+RUN apt-get update \
+    && apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 unzip
+COPY --from=build /home/saw/rootfs /
+RUN useradd -m saw && chown -R saw:saw /home/saw
+USER saw
+ENV LANG C.UTF-8
+ENTRYPOINT ["/usr/local/bin/saw"]

README.md

@@ -11,8 +11,10 @@ languages such as C, Java, and Cryptol.
 
 ## Documentation
 
-The [SAWScript tutorial](https://saw.galois.com/tutorial.html) gives
-an introduction to using the SAWScript interpreter.
+The [SAWScript tutorial](https://saw.galois.com/tutorial.html) gives an
+introduction to using the SAWScript interpreter. A longer
+[manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md)
+describes the breadth of SAWScript's features.
 
 ## Precompiled Binaries
 
@@ -26,15 +28,16 @@ solver](https://github.com/Z3Prover/z3) installed.  You can download Z3
 binaries for a variety of platforms from their [releases
 page](https://github.com/Z3Prover/z3/releases).
 
-SAW generally requires the most recent version of Z3, which at the
-time of writing this file is 4.5.0.
+Although it's not the most recent version, we currently recommend Z3
+4.7.1. If you plan to use path satisfiability checking, you'll also need
+Yices version 2.6.1 or newer.
 
 After installation, make sure that `z3` (or `z3.exe` on Windows)
 is on your PATH.
 
 ## Manual Installation
 
-To build SAWScript and related utilities (CSS, LSS, JSS) from source:
+To build SAWScript and related utilities from source:
 
   * Ensure that you have the
     [Stack](https://github.com/commercialhaskell/stack) program on your
@@ -103,7 +106,7 @@ SAW can analyze LLVM programs (usually derived from C, but potentially
 for other languages). The only tool strictly required for this is a
 compiler that can generate LLVM bitcode, such as `clang`. However,
 having the full LLVM tool suite available can be useful. We have tested
-SAW with LLVM and `clang` versions from 3.5 to 4.0, as well as the
+SAW with LLVM and `clang` versions from 3.5 to 7.0, as well as the
 version of `clang` bundled with Apple Xcode. We welcome bug reports on
 any failure to parse bitcode from LLVM versions in that range.
 
@@ -119,12 +122,12 @@ 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)
 * `deps/cryptol-verifier/`: [Cryptol Symbolic Simulator (CSS)](https://github.com/GaloisInc/cryptol-verifier)
 * `deps/jvm-verifier/`:     [Java Symbolic Simulator (JSS)](https://github.com/GaloisInc/jvm-verifier)
-* `deps/llvm-verifier/`:    [LLVM Symbolic Simulator (LSS)](https://github.com/GaloisInc/llvm-verifier)
-* `deps/saw-core/`:         [SAWCore intermediate language](https://github.com/GaloisInc/saw-core), used by CSS, JSS, LSS and SAWScript
-* `deps/cryptol/`:          [Cryptol](https://github.com/GaloisInc/cryptol)
-* `deps/abcBridge/`:        [Haskell bindings for ABC](https://github.com/GaloisInc/abcBridge)
+* `deps/saw-core/`:         [SAWCore intermediate language](https://github.com/GaloisInc/saw-core), used by CSS, JSS, and SAWScript
 
 ## For SAW developers