Merge pull request #1471 from GaloisInc/at-release-0.9-prep

Prepare for the 0.9 release

.github/ci.sh

@@ -45,6 +45,7 @@ setup_dist_bins() {
     extract_exe "saw-remote-api" "dist/bin"
   fi
   extract_exe "saw" "dist/bin"
+  extract_exe "cryptol" "dist/bin"
   export PATH=$PWD/dist/bin:$PATH
   echo "$PWD/dist/bin" >> "$GITHUB_PATH"
   strip dist/bin/saw* || echo "Strip failed: Ignoring harmless error"
@@ -83,18 +84,16 @@ install_system_deps() {
 }
 
 build_cryptol() {
-  is_exe "dist/bin" "cryptol" && return
-  (cd deps/cryptol &&
-    git submodule update --init &&
-    .github/ci.sh build)
+  cabal build exe:cryptol
 }
 
 bundle_files() {
-  mkdir -p dist dist/{bin,doc,examples,include,lib}
+  mkdir -p dist dist/{bin,deps,doc,examples,include,lib}
 
   cp LICENSE README.md dist/
   $IS_WIN || chmod +x dist/bin/*
 
+  (cd deps/cryptol-specs && git archive --prefix=cryptol-specs/ --format=tar HEAD) | (cd dist/deps && tar x)
   cp doc/extcore.md dist/doc
   cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf
   cp doc/manual/manual.pdf dist/doc/manual.pdf

.github/workflows/ci.yml

@@ -111,6 +111,11 @@ jobs:
       - shell: bash
         run: .github/ci.sh build
 
+      - shell: bash
+        env:
+          RELEASE: ${{ needs.config.outputs.release }}
+        run: .github/ci.sh build_cryptol
+
       - uses: GaloisInc/.github/actions/cabal-collect-bins@v1
         id: cabal-test-suites
         with:
@@ -348,7 +353,7 @@ jobs:
   build-push-image:
     runs-on: ubuntu-latest
     needs: [config]
-    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
+    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true'
     strategy:
       fail-fast: false
       matrix:

CHANGES.md

@@ -1,4 +1,4 @@
-# Unreleased version
+# Version 0.9
 
 ## New Features
 
@@ -20,13 +20,31 @@ Several improvements have been made to JVM verification:
   "current" status, so that `enable_experimental` is no longer
   necessary for JVM verification.
 
+* The RPC API now includes methods for Java verification, as described [here](https://github.com/GaloisInc/saw-script/blob/master/saw-remote-api/docs/SAW.rst#sawjvmload-class-command).
+
 A new `enable_lax_pointer_ordering` function exists, which relaxes the
 restrictions that Crucible imposes on comparisons between pointers from
 different allocation blocks.
 
 A SAW value of type `Bool` can now be brought into scope in Cryptol expressions
 as a value of type `Bit`.
 
+A new `hoist_ifs_in_goal` proof tactic works like `hoist_ifs` but on the
+current goal in a proof script.
+
+The verification summaries produced when specifying the `-s` flag now
+contain much more detailed information. When producing JSON output (`-f
+json`), the tool in the `verif-viewer` directory can be used to
+translate it to GraphViz format.
+
+Two new experimental functions can evaluate SAWCore terms into simpler
+forms. The `normalize_term` function simplifies the given term by fully
+evaluating it with the SAWCore symbolic simulator but keeping it in
+SAWCore format. The `extract_uninterp` function allows certain
+uninterpreted functions to be replaced with extra inputs and constraints
+on those inputs, allowing propositional solvers to prove goals involving
+uninterpreted functions.
+
 ## Changes
 
 * The linked-in version of ABC (based on the Haskell `abcBridge`
@@ -52,6 +70,42 @@ as a value of type `Bit`.
   [issues](https://github.com/galoisinc/saw-script/issues) for
   performance regressions you encounter!
 
+  The removal of the linked-in ABC version means that the `abc` tactic
+  now requires an external `abc` executable. You can get this by
+  downloading a `with-solvers` package from the releases page, by
+  downloading a solver package from the [`what4-solvers`
+  repository](https://github.com/GaloisInc/what4-solvers), or by
+  building it yourself from the [ABC
+  repository](https://github.com/berkeley-abc/abc).
+
+* The LLVM bitcode reader now should support files from any LLVM version
+  between 3.6 and 12.
+
+## Bug Fixes
+
+* Overall, closed issues #109, #120, #128, #156, #233, #316, #320, #324,
+  #523, #561, #624, #689, #722, #727, #746, #869, #872, #900, #975,
+  #982, #1033, #1035, #1045, #1066, #1098, #1120, #1135, #1140, #1144,
+  #1147, #1148, #1152, #1166, #1171, #1175, #1182, #1184, #1186, #1211,
+  #1224, #1226, #1230, #1256, #1260, #1263, #1269, #1280, #1285, #1299,
+  #1307, #1308, #1311, #1318, #1341, #1355, #1367, #1375, #1381, #1388,
+  #1389, #1390, #1404, #1411, #1420, #1430, and #1438.
+
+* Overall, merged pull requests #942, #1117, #1185, #1191, #1204, #1205,
+  #1206, #1207, #1208, #1209, #1212, #1213, #1214, #1216, #1218, #1219,
+  #1267, #1270, #1272, #1274, #1275, #1276, #1278, #1279, #1281, #1282,
+  #1283, #1284, #1286, #1288, #1289, #1290, #1292, #1293, #1294, #1295,
+  #1297, #1298, #1300, #1309, #1310, #1313, #1315, #1317, #1319, #1320,
+  #1321, #1323, #1325, #1327, #1328, #1329, #1330, #1331, #1332, #1334,
+  #1335, #1336, #1337, #1342, #1343, #1345, #1346, #1349, #1351, #1356,
+  #1357, #1364, #1365, #1366, #1368, #1369, #1370, #1371, #1373, #1374,
+  #1378, #1379, #1380, #1384, #1385, #1391, #1392, #1393, #1394, #1396,
+  #1397, #1398, #1399, #1401, #1402, #1403, #1405, #1406, #1410, #1413,
+  #1414, #1415, #1416, #1422, #1423, #1424, #1426, #1427, #1428, #1429,
+  #1431, #1432, #1433, #1434, #1435, #1437, #1439, #1440, #1441, #1443,
+  #1444, #1445, #1446, #1448, #1449, #1450, #1451, #1453, #1454, #1455,
+  #1456, #1457, #1458, #1459, #1463, #1464, #1465, #1466, and #1468.
+
 # Version 0.8
 
 ## New Features

CODE_OF_CONDUCT.md

@@ -0,0 +1,86 @@
+# Code of Conduct
+
+## Our Pledge
+
+We as members, contributors, and leaders pledge to make participation in our
+community a harassment-free experience for everyone, regardless of age, body
+size, visible or invisible disability, ethnicity, sex characteristics, gender
+identity and expression, level of experience, education, socio-economic status,
+nationality, personal appearance, race, caste, color, religion, or sexual identity
+and orientation.
+
+We pledge to act and interact in ways that contribute to an open, welcoming,
+diverse, inclusive, and healthy community.
+
+## Our Standards
+
+Examples of behavior that contributes to a positive environment for our
+community include:
+
+* Demonstrating empathy and kindness toward other people
+* Being respectful of differing opinions, viewpoints, and experiences
+* Giving and gracefully accepting constructive feedback
+* Accepting responsibility and apologizing to those affected by our mistakes,
+  and learning from the experience
+* Focusing on what is best not just for us as individuals, but for the
+  overall community
+
+Examples of unacceptable behavior include:
+
+* The use of sexualized language or imagery, and sexual attention or
+  advances of any kind
+* Trolling, insulting or derogatory comments, and personal or political attacks
+* Public or private harassment
+* Publishing others' private information, such as a physical or email
+  address, without their explicit permission
+* Other conduct which could reasonably be considered inappropriate in a
+  professional setting
+
+## Enforcement Responsibilities
+
+Project maintainers are responsible for clarifying and enforcing our standards of
+acceptable behavior and will take appropriate and fair corrective action in
+response to any behavior that they deem inappropriate, threatening, offensive,
+or harmful.
+
+Project maintainers have the right and responsibility to remove, edit, or reject
+comments, commits, code, wiki edits, issues, and other contributions that are
+not aligned to this Code of Conduct, and will communicate reasons for moderation
+decisions when appropriate.
+
+## Scope
+
+This Code of Conduct applies within all community spaces, and also applies when
+an individual is officially representing the community in public spaces.
+Examples of representing our community include using an official e-mail address,
+posting via an official social media account, or acting as an appointed
+representative at an online or offline event.
+
+## Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may
+be reported to the project maintainers responsible for enforcement at
+[[email protected]](mailto:[email protected]). All complaints will be
+reviewed and investigated promptly and fairly.
+
+All project maintainers are obligated to respect the privacy and security of the
+reporter of any incident.
+
+## Attribution
+
+This Code of Conduct is adapted from the [Contributor Covenant][homepage],
+version 2.1, available at
+[https://www.contributor-covenant.org/version/2/1/code_of_conduct.html][v2.1].
+
+Community Impact Guidelines were inspired by
+[Mozilla's code of conduct enforcement ladder][Mozilla CoC].
+
+For answers to common questions about this code of conduct, see the FAQ at
+[https://www.contributor-covenant.org/faq][FAQ]. Translations are available
+at [https://www.contributor-covenant.org/translations][translations].
+
+[homepage]: https://www.contributor-covenant.org
+[v2.1]: https://www.contributor-covenant.org/version/2/1/code_of_conduct.html
+[Mozilla CoC]: https://github.com/mozilla/diversity
+[FAQ]: https://www.contributor-covenant.org/faq
+[translations]: https://www.contributor-covenant.org/translations

README.md

@@ -41,7 +41,8 @@ To build SAWScript and related utilities from source:
 
   * Ensure that you have the `cabal` and `ghc` executables in your
     `PATH`. If you don't already have them, we recommend using `ghcup`
-    to install them: <https://www.haskell.org/ghcup/>
+    to install them: <https://www.haskell.org/ghcup/>. We recommend
+    Cabal 3.4 or newer, and GHC 8.8 or 8.10.
 
   * Ensure that you have the C libraries and header files for
     `terminfo`, which generally comes as part of `ncurses` on most
@@ -70,7 +71,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 11.0, as well as the
+SAW with LLVM and `clang` versions from 3.5 to 12.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.
 
@@ -79,6 +80,11 @@ will be possible for all language constructs. There are various
 instructions that are not supported during verification. However,
 any failure during `llvm_load_module` should be considered a bug.
 
+## Notes on Windows
+
+If you have trouble loading the SAW REPL on Windows, try invoking it
+with the `--no-color` option.
+
 ## Related Packages
 
 Many dependencies are automatically downloaded into `deps/` when you

heapster-saw/examples/Makefile

@@ -16,8 +16,10 @@ ifeq ($(SAW),)
   endif
 endif
 
-%.bc: %.c
+ifeq ($(CI),)
+  %.bc: %.c
 	clang -emit-llvm -g -c $<
+endif
 
 %_gen.v: %.saw %.bc
 	$(SAW) $<

saw-remote-api/Dockerfile

@@ -1,48 +1,6 @@
-FROM debian:buster AS solvers
-
-# Install needed packages for building
-RUN apt-get update \
-    && apt-get install -y curl cmake gcc g++ git libreadline-dev unzip
-RUN useradd -m user
-RUN install -d -o user -g user /solvers
-USER user
-WORKDIR /solvers
-RUN mkdir -p rootfs/usr/local/bin
-
-# Get Z3 4.8.10 from GitHub
-RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip --output z3.zip
-RUN unzip z3.zip
-RUN mv z3-*/bin/z3 rootfs/usr/local/bin
-
-# Build abc from GitHub. (Latest version.)
-RUN git clone https://github.com/berkeley-abc/abc.git
-RUN cd abc && make -j$(nproc)
-RUN cp abc/abc rootfs/usr/local/bin
-
-# Build Boolector release 3.2.1 from source
-RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz
-RUN cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc)
-RUN cp boolector*/build/bin/boolector rootfs/usr/local/bin
-
-# Install Yices 2.6.2
-RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz
-RUN cp yices*/bin/yices-smt2 rootfs/usr/local/bin \
-    && cp yices*/bin/yices rootfs/usr/local/bin
-
-# Install CVC4 1.8
-RUN curl -L https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4
-
-# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license.
-# RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz
-# RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin
-
-# Set executable and run tests
-RUN chmod +x rootfs/usr/local/bin/*
-
 FROM haskell:8.8.4 AS build
 USER root
 RUN apt-get update && apt-get install -y wget libncurses-dev unzip
-COPY --from=solvers /solvers/rootfs /
 RUN useradd -m saw
 COPY --chown=saw:saw . /home/saw
 USER saw
@@ -53,15 +11,16 @@ COPY cabal.GHC-8.8.4.config cabal.project.freeze
 RUN cabal v2-update && cabal v2-build -j exe:saw-remote-api
 RUN mkdir -p /home/saw/rootfs/usr/local/bin
 RUN cp $(cabal v2-exec which saw-remote-api) /home/saw/rootfs/usr/local/bin/saw-remote-api
-WORKDIR /home/saw
+WORKDIR /home/saw//rootfs/usr/local/bin
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip"
+RUN unzip solvers.zip && rm solvers.zip && chmod +x *
 USER root
 RUN chown -R root:root /home/saw/rootfs
 
 FROM debian:buster-slim
 RUN apt-get update \
     && apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 unzip openjdk-11-jdk-headless
 COPY --from=build /home/saw/rootfs /
-COPY --from=solvers /solvers/rootfs /
 RUN useradd -m saw && chown -R saw:saw /home/saw
 USER saw
 ENV LANG=C.UTF-8 \