Merge branch 'doc-updates' into release-0.1-dev

doc/tutorial/code/basic.c

@@ -0,0 +1,8 @@
+#include <stdint.h>
+uint32_t add(uint32_t x, uint32_t y) {
+    return x + y;
+}
+
+uint32_t dbl(uint32_t x) {
+    return add(x, x);
+}

doc/tutorial/code/llvm_symexec.saw

@@ -2,7 +2,7 @@ m <- llvm_load_module "basic.bc";
 add <- define "add" {{ \x y -> (x : [32]) + y }};
 x <- fresh_symbolic "x" {| [32] |};
 y <- fresh_symbolic "y" {| [32] |};
-t <- llvm_symexec m "add" [] [("x", x), ("y", y)] ["return"];
+t <- llvm_symexec m "add" [] [("x", x, 1), ("y", y, 1)] [("return", 1)];
 print_term t;
 t' <- abstract_symbolic t;
 prove_print abc {{ \a b -> t' a b == add a b }};

doc/tutorial/tutorial.md

@@ -23,12 +23,13 @@ can be described.
 Example: Find First Set
 =======================
 
-As a first example, we consider a simple function that identifies the
-first ``1`` bit in a word. The function takes an integer as input,
-treated as a vector of bits, and returns another integer which
-indicates the index of the first bit set. This function exists in a
-number of standard C libraries, and can be implemented in several
-ways.
+As a first example, we consider equivalence checking different implementations
+of the POSIX `ffsl` function, which identifies the position of the first ``1``
+bit in a word. The function takes an integer as input, treated as a vector of
+bits, and returns another integer which indicates the index of the first bit
+set. This function can be implemented in several ways with different
+performance and code clarity tradeoffs, and we would like to show those
+different implementations are equivalent.
 
 Reference Implementation
 -------------------------
@@ -133,10 +134,15 @@ function, which computes a scalar return value entirely as a function
 of its scalar parameters.
 
 The `let` statement then constructs a new term corresponding to the
-assertion of equality between two existing terms. The `prove_print`
-command can verify the validity of such an assertion, and print out
-the results of verification. The `abc` parameter indicates what
-theorem prover to use.
+assertion of equality between two existing terms.  Arbitrary
+Cryptol expressions can be embedded within SAWScript; to distinguish
+Cryptol code from SAWScript commands, the Cryptol code is placed
+within double brackets `{{` and `}}`.
+
+The `prove_print` command can verify the validity of such an assertion, and
+print out the results of verification. The `abc` parameter indicates what
+theorem prover to use; SAWScript offers support for many other SAT and
+SMT solvers as well as user definable simplification tactics.
 
 If the `saw` executable is in your PATH, you can run the script above with
 
@@ -295,13 +301,15 @@ translated into a single mathematical model. SAWScript also has
 support for more compositional proofs, as well as proofs about
 functions that use heap data structures.
 
+<!--
 Compositional Cryptol Proofs
 ----------------------------
 
 The simplest form of compositional reasoning within SAWScript involves
 treating sub-terms of models as uninterpreted functions.
 
 TODO
+-->
 
 Compositional Imperative Proofs
 -------------------------------
@@ -440,8 +448,21 @@ before execution begins, and parameters that indicate which portions
 of the program state should be returned as output when execution
 completes.
 
-More specifically, the Java version of the command has the following
-signature:
+The initial state before symbolic execution typically includes unknown
+(symbolic) elements. To construct `Term` inputs that contains symbolic
+variables, you can start by using the `fresh_symbolic` command, which
+takes a name and a type as arguments, and returns a `Term`. The name
+is used only for pretty-printing, and the type is used for later
+consistency checking. For example, consider the following command:
+
+    x <- fresh_symbolic "x" {| [32] |};
+
+This creates a new `Term` stored in the SAWScript variable `x` that is
+a 32-bit symbolic word.
+
+These symbolic variables are most commonly used by the more general
+Java and LLVM model extraction commands. The Java version of the
+command has the following signature:
 
     java_symexec : JavaClass
                 -> String
@@ -453,13 +474,34 @@ This first two parameters are the same as for `java_extract`: the
 class object and the name of the method from that class to execute.
 The third parameter describes the initial state of execution. For each
 element of this list, SAWScript writes the value of the `Term` to the
-destination variable or field named by the `String`. The syntax of
-destination follows Java syntax. For example, `o.f` describes field
-`f` of object `o`. The fourth parameter indicates which elements of
-the final state to return as output. The syntax of the strings in this
-list is the same as for the initial state description.
+destination variable or field named by the `String`. Typically, the
+`Term` will either be directly the result of `fresh_symbolic` or an
+more complex expression containing such a result, though it is allowed
+to be a constant value. The syntax of destination follows Java syntax.
+For example, `o.f` describes field `f` of object `o`. The fourth
+parameter indicates which elements of the final state to return as
+output. The syntax of the strings in this list is the same as for the
+initial state description.
+
+An example of using `java_symexec` on a simple function (using just
+scalar arguments and return values) appears in the
+`code/java_symexec.saw` file, quoted below.
+
+```
+$include all code/java_symexec.saw
+```
 
-TODO: example and limitations
+This script uses `fresh_symbolic` to construct two fresh variables,
+`x` and `y`, and then passes them in as the initial values of the
+method parameters of the same name. It then uses the special name
+`return` to refer to the return value of the method in the output
+list. Finally, it uses the `abstract_symbolic` command to convert a
+`Term` containing symbolic variables into a function that takes the
+values of those variables as parameters. This last step exists partly
+to illustrate the use of `abstract_symbolic`, and partly because the
+`prove_print` command currently cannot process terms that contain
+symbolic variables (though we plan to adapt it to be able to in the
+near future).
 
 The LLVM version of the command has some additional complexities, due
 to the less structured nature of the LLVM memory model.
@@ -491,7 +533,26 @@ pointer `p`, write 8 elements to `*p` at the beginning, and read 4
 elements from `*p` at the end. However, both the initialization and
 result sizes must be less than or equal to the allocation size.
 
-TODO: example and limitations
+An example of using `java_symexec` on a function similar to the Java
+method just discussed appears in the `code/java_symexec.saw` file,
+quoted below.
+
+```
+$include all code/llvm_symexec.saw
+```
+
+This has largely the same structure as the Java example, except that
+`llvm_symexec` command takes and extra argument, describing
+allocations, and the input and output descriptions take sizes as well
+as values, to compensate for the fact that LLVM does not track how
+much memory a given variable takes up. In simple scalar cases such as
+this one, the size argument will always be `1`. However, if an input
+or output parameter is an array, it will take on the corresponding
+size value. For instance, say an LLVM function takes as a parameter an
+array `a` containing 10 elements of type `uint32_t *`, which it reads
+and writes. We could then call `llvm_symexec` with an allocation
+argument of `[("a", 10)]`, and both input and output arguments of
+`[("*a", 10)]` (note the additional `*` in the latter).
 
 Other Examples
 ==============

src/SAWScript/Interpreter.hs

@@ -932,17 +932,38 @@ primitives = Map.fromList
   , prim "java_extract"
     "JavaClass -> String -> JavaSetup () -> TopLevel Term"
     (bicVal extractJava)
-    [ "TODO" ]
+    [ "Translate a Java method directly to a Term. The parameters of the"
+    , "Term will be the parameters of the Java method, and the return"
+    , "value will be the return value of the method. Only static methods"
+    , "with scalar argument and return types are currently supported. For"
+    , "more flexibility, see 'java_symexec' or 'java_verify'."
+    ]
 
   , prim "java_symexec"
     "JavaClass -> String -> [(String, Term)] -> [String] -> TopLevel Term"
     (bicVal symexecJava)
-    [ "TODO" ]
+    [ "Symbolically execute a Java method and construct a Term corresponding"
+    , "to its result. The first list contains pairs of variable or field"
+    , "names along with Terms specifying their initial (possibly symbolic)"
+    , "values. The second list contains the names of the variables or fields"
+    , "to treat as outputs. The resulting Term will be of tuple type, with"
+    , "as many elements as there are names in the output list."
+    ]
 
   , prim "java_verify"
     "JavaClass -> String -> [JavaMethodSpec] -> JavaSetup () -> TopLevel JavaMethodSpec"
     (bicVal verifyJava)
-    [ "TODO" ]
+    [ "Verify a Java method against a method specification. The first two"
+    , "arguments are the same as for 'java_extract' and 'java_symexec'."
+    , "The list of JavaMethodSpec values in the third argument makes it"
+    , "possible to use the results of previous verifications to take the"
+    , "place of actual execution when encountering a method call. The last"
+    , "parameter is a setup block, containing a sequence of commands of type"
+    , "'JavaSetup a' that configure the symbolic simulator and specify the"
+    , "types of variables in scope, the expected results of execution, and"
+    , "the tactics to use to verify that the method produces the expected"
+    , "results."
+    ]
 
   , prim "llvm_int"            "Int -> LLVMType"
     (pureVal llvmInt)
@@ -973,7 +994,11 @@ primitives = Map.fromList
 
   , prim "llvm_ptr"            "String -> LLVMType -> LLVMSetup Term"
     (bicVal llvmPtr)
-    [ "TODO" ]
+    [ "Declare that the named LLVM variable should point to a value of the"
+    , "given type. This command makes the given variable visible later, so"
+    , "the use of 'llvm_ptr \"p\" ...' is necessary before using, for"
+    , "instance, 'llvm_ensure \"*p\" ...'."
+    ]
 
   --, prim "llvm_may_alias"      "[String] -> LLVMSetup ()"
   --  (bicVal llvmMayAlias)
@@ -1024,17 +1049,43 @@ primitives = Map.fromList
   , prim "llvm_extract"
     "LLVMModule -> String -> LLVMSetup () -> TopLevel Term"
     (scVal extractLLVM)
-    [ "TODO" ]
+    [ "Translate an LLVM function directly to a Term. The parameters of the"
+    , "Term will be the parameters of the LLVM function, and the return"
+    , "value will be the return value of the functions. Only functions with"
+    , "scalar argument and return types are currently supported. For more"
+    , "flexibility, see 'llvm_symexec' or 'llvm_verify'."
+    ]
 
   , prim "llvm_symexec"
     "LLVMModule -> String -> [(String, Int)] -> [(String, Term, Int)] -> [(String, Int)] -> TopLevel Term"
     (bicVal symexecLLVM)
-    [ "TODO" ]
+    [ "Symbolically execute an LLVM function and construct a Term corresponding"
+    , "to its result. The first list describes what allocations should be"
+    , "performed before execution. Each name given is allocated to point to"
+    , "the given number of elements, of the appropriate type. The second list"
+    , "contains pairs of variables or expressions along with Terms specifying"
+    , "their initial (possibly symbolic) values, and the number of elements"
+    , "that the term should contain. Finally, the third list contains the"
+    , "names of the variables or expressions to treat as outputs, along with"
+    , "the number of elements to read from those locations. The resulting Term"
+    , "will be of tuple type, with as many elements as there are names in the"
+    , "output list."
+    ]
 
   , prim "llvm_verify"
     "LLVMModule -> String -> [LLVMMethodSpec] -> LLVMSetup () -> TopLevel LLVMMethodSpec"
     (bicVal verifyLLVM)
-    [ "TODO" ]
+    [ "Verify an LLVM function against a specification. The first two"
+    , "arguments are the same as for 'llvm_extract' and 'llvm_symexec'."
+    , "The list of LLVMMethodSpec values in the third argument makes it"
+    , "possible to use the results of previous verifications to take the"
+    , "place of actual execution when encountering a function call. The last"
+    , "parameter is a setup block, containing a sequence of commands of type"
+    , "'LLVMSetup a' that configure the symbolic simulator and specify the"
+    , "types of variables in scope, the expected results of execution, and"
+    , "the tactics to use to verify that the function produces the expected"
+    , "results."
+    ]
 
   , prim "caseSatResult"       "{b} SatResult -> b -> (Term -> b) -> b"
     (\_ bic -> toValueCase (biSharedContext bic) caseSatResultPrim)

stage.sh

@@ -35,6 +35,7 @@ echo Staging ...
 strip build/bin/*
 
 cp deps/abcBridge/abc-build/copyright.txt     ${TARGET}/ABC_LICENSE
+cp LICENSE                                    ${TARGET}/LICENSE
 cp build/bin/bcdump                           ${TARGET}/bin
 cp build/bin/extcore-info                     ${TARGET}/bin
 cp build/bin/jss                              ${TARGET}/bin