Merge remote-tracking branch 'origin/master' into lisanna/ci-release-0.8

CHANGES.md

@@ -1,4 +1,4 @@
-# Unreleased version
+# Version 0.8
 
 ## New Features
 
@@ -15,17 +15,130 @@ When the path to Java is known, SAW can automatically add system-related
 JAR files to the JAR path, which eliminates the need to manually specify
 these files with `-j`.
 
-SAWScript includes two new functions, `llvm_struct_type` and
-`llvm_packed_struct_type`, for constructing an LLVM struct type from a list
-of other LLVM types. This is not to be confused with the existing `llvm_struct`
-function, which takes a string as an argument and returns the corresponding
-alias type (which is often, but not necessarily, defined as a struct type).
-To avoid confusion, a new `llvm_alias` function has been introduced, and
-`llvm_struct` is now a synonym for `llvm_alias`. The `llvm_struct` function
-continues to be available for now.
-
-SAWScript includes a new `llvm_pointer : LLVMType -> LLVMType` function for
-constructing LLVM pointer types.
+The Crucible-based interface to Java verification is now strictly an
+improvement over the older code base, with the addition of several
+features:
+
+* Performance of JVM verification is significantly better, as a result
+  of removing some unnecessary instances of rewriting. This improves
+  performance of LLVM verification, as well.
+
+* The new `jvm_static_field_is` function allows describing the contents
+  of static variables in method specifications.
+
+* The verification code initializes all JVM classes at the start so that
+  initializers don't run at arbitrary intermediate points and clobber
+  static field values specified in preconditions. This means, however,
+  that any proofs about Java code are under the assumption that all
+  class initializers have run before the method under analysis executes.
+
+Now that the Crucible-based verification infrastructure is sufficiently
+expressive and performant, we have removed all dependencies on the old
+`jvm-verifier` library.
+
+On the LLVM side, SAWScript includes a variety of new functions for
+writing specification blocks:
+
+* The `llvm_struct_type` and `llvm_packed_struct_type` functions each
+  construct an LLVM struct type from a list of other LLVM types. This is
+  not to be confused with the existing `llvm_struct` function, which
+  takes a string as an argument and returns the corresponding alias type
+  (which is often, but not necessarily, defined as a struct type).
+
+* To avoid confusion, a new `llvm_alias` function now exists, and
+  `llvm_struct` is now a synonym for `llvm_alias`. The `llvm_struct`
+  function continues to be available for now.
+
+* The `llvm_pointer : LLVMType -> LLVMType` function allows construction
+  of arbitrary LLVM pointer types.
+
+* Two new functions, `llvm_points_to_at_type` and
+  `llvm_conditional_points_to_at_type`, mirror `llvm_points_to` and
+  `llvm_conditional_points_to`, but cast the pointer to a different
+  type. This may be useful when reading or writing a prefix of a larger
+  array, for example.
+
+* Support for using ABC as an external process is more complete:
+
+    * SAW can now generate Verilog with multiple outputs (from `Term`
+      values that have tuple or vector result types, for example).
+
+    * The new commands `write_aig_external` and `write_cnf_external`
+      generate AIG and CNF files, respectively, by first writing Verilog
+      and then using the available `abc` executable to bit-blast to the
+      lower-level representation. Corresponding proof tactics,
+      `offline_aig_external` and `offline_cnf_external` also exist.
+
+These changes are in preparation for removing the linked-in copy of ABC
+in a future release.
+
+The `saw-remote-api` RPC server and associated Python client now have
+more complete support for LLVM verification, including:
+
+* More complete points-to declarations, matching what is currently
+  available in SAWScript.
+
+* Support for more provers, including the full range of SBV-based and
+  What4-based provers available in SAWScript.
+
+* Support for ghost variables.
+
+* Support for assuming LLVM contracts directly (rather than the previous
+  behavior which would temporarily assume that failed verifications
+  succeeded to determine whether higher-level verifications would still
+  succeed).
+
+* Support for global variables and initializers.
+
+* Support for null pointers.
+
+* Support for array value literals.
+
+* Support for specifying the value of individual struct fields and array
+  elements.
+
+* Support for specifying the alignment of allocations.
+
+The most recent version of the Python client is now in the `saw-script`
+repository and available from `PyPI` with `pip install saw`.
+
+Docker images for SAW are now located on
+[GitHub](https://github.com/orgs/galoisinc/packages/container/package/saw)
+instead of [DockerHub](https://hub.docker.com/r/galoisinc/saw/).
+
+## Changes
+
+The proof management infrastructure in SAWScript is simpler and more
+consistent than before. Many of these changes are internal, to make the
+code less error-prone and easier to maintain in the future. Several are
+user-facing, though:
+
+* The `caseProofResult` command now passes a `Theorem` argument to the
+  first function argument, allowing its use as a rewrite rule, for
+  example.
+
+* A new `admit` tactic exists, which takes a `String` argument
+  describing why the user has decided omit proof of the goal. This
+  replaces the `assume_unsat` and `assume_valid` tactics, which we now
+  recommend against. They will be officially deprecated in a future
+  release, and removed after that.
+
+* Prover tactics (e.g., `yices`) now return `ProofScript ()` instead of
+  `ProofScript SatResult`.
+
+## Bug Fixes
+
+* Verilog generated from rotation operations is now in correct Verilog
+  syntax.
+
+* Closed issues #9, #25, #39, #41, #54, #55, #69, #81, #90, #92, #124,
+  #136, #144, #149, #152, #159, #271, #285, #323, #353, #377, #382,
+  #431, #446, #631, #652, #739, #740, #861, #901, #908, #924, #930,
+  #951, #962, #971, #985, #991, #993, #994, #995, #996, #1003, #1006,
+  #1009, #1021, #1022, #1023, #1031, #1032, #1050, #1051, #1052, #1055,
+  #1056, #1058, #1061, #1062, #1067, #1073, #1083, #1085, #1090, #1091,
+  #1096, #1099, #1101, #1119, #1122, #1123, #1127, #1128, #1132, #1163,
+  and #1164.
 
 # Version 0.7
 

README.md

@@ -17,7 +17,9 @@ describes the breadth of SAWScript's features.
 
 ## Precompiled Binaries
 
-Precompiled SAWScript binaries for a variety of platforms are available on the [releases page](https://github.com/GaloisInc/saw-script/releases).
+Precompiled SAWScript binaries for a variety of platforms are available
+on the [releases
+page](https://github.com/GaloisInc/saw-script/releases).
 
 ## Getting Z3
 
@@ -27,7 +29,7 @@ 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).
 
-We currently recommend Z3 4.8.7. If you plan to use path satisfiability
+We currently recommend Z3 4.8.10. 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)
@@ -68,7 +70,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 9.0, as well as the
+SAW with LLVM and `clang` versions from 3.5 to 11.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.
 

intTests/test_external_abc/test.saw

@@ -8,18 +8,24 @@ prove_print w4_abc_smtlib2 t;
 prove_print w4_abc_verilog t;
 prove_print (offline_verilog "offline_verilog") t;
 prove_print (w4_offline_smtlib2 "w4_offline_smtlib2") t;
+prove_print (offline_aig_external "offline_aig") t;
+prove_print (offline_cnf_external "offline_cnf") t;
 
 // A formula that is unsatisfiable.
 let q_unsat = {{ \(x:[8]) -> x != 0 /\ x+x == x }};
 
 write_verilog "write_verilog_unsat.v" q_unsat;
 write_smtlib2_w4 "write_smtlib2_w4_unsat.smt2" q_unsat;
+write_aig_external "write_aig_external_unsat.aig" q_unsat;
+write_cnf_external "write_aig_external_unsat.cnf" q_unsat;
 
 // A formula that is satisfiable.
 let q_sat = {{ \(x:[8]) -> x+x == x }};
 
 write_verilog "write_verilog_sat.v" q_sat;
 write_smtlib2_w4 "write_smtlib2_w4_sat.smt2" q_sat;
+write_aig_external "write_aig_external_sat.aig" q_sat;
+write_cnf_external "write_aig_external_sat.cnf" q_sat;
 
 fails (prove_print sbv_abc q_sat);
 fails (prove_print w4_abc_smtlib2 q_sat);

intTests/test_external_abc/test.sh

@@ -14,6 +14,15 @@ abc -q "%read write_verilog_unsat.v; $SCRIPT" || true;
 abc -q "%read write_verilog_sat.v; $SCRIPT" || true;
 [ -s ${CEX} ]
 
+rm -f ${CEX}
+
+abc -q "&read offline_aig.prove0.aig; &cec -m; write_aiger_cex $CEX" || true;
+[ ! -f ${CEX} ]
+abc -q "&read write_aig_external_unsat.aig; &cec -m; write_aiger_cex $CEX" || true;
+[ ! -f ${CEX} ]
+abc -q "&read write_aig_external_sat.aig; &cec -m; write_aiger_cex $CEX" || true;
+[ -s ${CEX} ]
+
 z3 w4_offline_smtlib2.prove0.smt2 | grep "^unsat$"
 z3 write_smtlib2_w4_sat.smt2 | grep "^sat$"
 z3 write_smtlib2_w4_unsat.smt2 | grep "^unsat$"
@@ -23,4 +32,4 @@ abc -q "%read write_verilog_tupt.v; %blast; &write tupt.aig"
 abc -q "cec seqt.aig tupt.aig"
 
 rm -f ${CEX}
-rm -f *.v *.aig *.smt2
+rm -f *.v *.aig *.smt2 *.cnf

intTests/test_llvm_x86_07/test.S

@@ -0,0 +1,10 @@
+section .bss
+section .text
+global precondtest
+precondtest:
+	mov rax, rdi
+        ret
+global _start
+_start:
+        mov rax, 60
+        syscall

intTests/test_llvm_x86_07/test.c

@@ -0,0 +1,8 @@
+#include <stdint.h>
+#include <stdio.h>
+
+extern uint64_t precondtest(uint64_t x);
+
+void test() {
+	precondtest(1);
+};

intTests/test_llvm_x86_07/test.saw

@@ -0,0 +1,14 @@
+enable_experimental;
+
+m <- llvm_load_module "test.bc";
+
+let precondtest_setup = do {
+  x <- crucible_fresh_var "x" (llvm_int 64);
+  crucible_precond {{ x < 10 }};
+  llvm_execute_func [crucible_term x];
+  x' <- crucible_fresh_var "x'" (llvm_int 64);
+  crucible_return (crucible_term x');
+  crucible_postcond {{ x' < 10 }};
+};
+
+llvm_verify_x86 m "./test" "precondtest" [] false precondtest_setup w4;

intTests/test_llvm_x86_07/test.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+set -e
+
+# yasm -felf64 test.S
+# ld test.o -o test
+clang -c -emit-llvm test.c
+$SAW test.saw

saw-remote-api/docs/SAW.rst

@@ -238,6 +238,22 @@ SAW/LLVM/assume (command)
 Assume the function meets its specification.
 
 
+SAW/create ghost variable (command)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+
+``display name``
+  The name to assign to the ghost variable for display.
+
+
+
+``server name``
+  The server name to use to access the ghost variable later.
+
+
+Create a ghost global variable to represent proof-specific program state.
+
+
 SAW/make simpset (command)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 

saw-remote-api/python/pyproject.toml

@@ -8,7 +8,7 @@ authors = ["Andrew Kent <andrew@galois.com>", "Aaron Tomb <atomb@galois.com>"]
 python = "^3.8"
 requests = "^2.25.1"
 BitVector = "^3.4.9"
-cryptol = { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
+cryptol = "2.11.0"
 argo-client = "0.0.4"
 
 [tool.poetry.dev-dependencies]