Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

4 files changed, 541 insertions, 0 deletions

diff --git a/docs/SMT-COMP/BitVector_ArraysEx.smt b/docs/SMT-COMP/BitVector_ArraysEx.smt
new file mode 100644
index 00000000..a60413ca
--- /dev/null
+++ b/docs/SMT-COMP/BitVector_ArraysEx.smt
@@ -0,0 +1,74 @@
+(theory BitVector_ArraysEx
+
+ :written_by {Clark Barrett}
+ :date {May 7, 2007}
+ 
+:sorts_description {
+    All sort symbols of the form BitVec[m],
+    where m is a numeral greater than 0.
+
+    All sort symbols of the form Array[m:n],
+    where m and n are numerals with m > 0 and n > 0.
+}
+
+:funs_description {
+    All functions from the theory Fixed_Size_Bitvectors.
+}
+
+:funs_description {
+    All function symbols with arity of the form
+
+      (select Array[m:n] BitVec[m] BitVec[n])
+
+    where
+    - m,n are numerals
+    - m > 0, n > 0
+}
+
+:funs_description {
+    All function symbols with arity of the form
+
+      (store Array[m:n] BitVec[m] BitVec[n] Array[m:n])
+
+    where
+    - m,n are numerals
+    - m > 0, n > 0
+}
+
+:preds_description {
+    All predicates from the theory Fixed_Size_Bitvectors.
+}
+
+
+ :definition 
+ "This is a theory containing an infinite number of copies of the theory of
+  functional arrays with extensionality: one for each pair of bitvector sorts.
+  It can be formally defined as the union of the SMT-LIB theory
+  Fixed_Size_Bitvectors and an infinite number of variants of the SMT-LIB
+  theory ArraysEx: one for each distinct signature morphism mapping the sort Index
+  to BitVec[m] and the sort Element to Bitvec[n] where m and n range over all
+  positive numerals.  In each of the copies of ArraysEx, the sort Array is
+  renamed to Array[m:n] and each copy of ArraysEx contributes exactly one select
+  function and one store function to the infinite polymorphic family of select
+  and store functions described above.
+ "
+
+ :notes
+ "As in the theory Fixed_Size_Bitvectors, this theory does not
+  provide a value for the formal attributes :sorts, :funs, and :preds because
+  there are an infinite number of them.  See the notes in theory
+  Fixed_Size_Bitvectors for details.
+
+  If for i=1,2, T_i is an SMT-LIB theory with sorts S_i, function symbols F_i,
+  predicate symbols P_i, and axioms A_i, by \"union\" of T_1 and T_2 
+  we mean the theory T with sorts S_1 U S_2, function symbols F_1 U F_2,
+  predicate symbols P_1 U P_2, and axioms A_1 U A_2 (where U stands for set
+  theoretic union).
+
+  The theory T is a well-defined SMT-LIB theory whenever S_1, S_2, F_1, F_2, 
+  P_1, P_2 are all pairwise disjoint, as is the case for the component theories
+  considered here. 
+ "
+)
+
+
diff --git a/docs/SMT-COMP/BitVectors.smt b/docs/SMT-COMP/BitVectors.smt
new file mode 100644
index 00000000..f2cde1b3
--- /dev/null
+++ b/docs/SMT-COMP/BitVectors.smt
@@ -0,0 +1,187 @@
+(theory Fixed_Size_BitVectors
+
+:written_by {Silvio Ranise, Cesare Tinelli, and Clark Barrett}
+
+:date {May 7, 2007}
+
+:notes
+   "Against the requirements of the current SMT-LIB standard this theory does
+    not provide a value for the formal attributes :sorts, :funs, and :preds.
+    The reason is that the theory has an infinite number of sort, function, and
+    predicate symbols, and so they cannot be specified formally in the current
+    SMT-LIB language.  While extending SMT-LIB's type system with dependent
+    types would allow a finitary formal specification of all the symbols in
+    this theory's signature, such an extension does not seem to be worth the
+    trouble at the moment.  As a temporary ad-hoc solution, this theory
+    declaration specifies the signature, in English, in the user-defined
+    attributes :sorts_description, :funs_description, and :preds_description.
+    "
+
+:sorts_description {
+    All sort symbols of the form BitVec[m],
+    where m is a numeral greater than 0.
+}
+
+:funs_description {
+    Constant symbols bit0 and bit1 of sort BitVec[1]
+}
+
+:funs_description {
+    All function symbols with arity of the form
+
+      (concat BitVec[i] BitVec[j] BitVec[m])
+
+    where
+    - i,j,m are numerals
+    - i,j > 0
+    - i + j = m
+}
+
+:funs_description {
+    All function symbols with arity of the form
+
+      (extract[i:j] BitVec[m] BitVec[n])
+
+    where
+    - i,j,m,n are numerals
+    - m > i >= j >= 0,
+    - n = i-j+1.
+}
+
+:funs_description {
+    All function symbols with arity of the form
+
+       (op1 BitVec[m] BitVec[m])
+    or
+       (op2 BitVec[m] BitVec[m] BitVec[m])
+
+    where
+    - op1 is from {bvnot, bvneg}
+    - op2 is from {bvand, bvor, bvadd, bvmul, bvudiv, bvurem, bvshl, bvlshr}
+    - m is a numeral greater than 0
+}
+
+:preds_description {
+    All predicate symbols with arity of the form
+
+       (pred BitVec[m] BitVec[m])
+
+    where
+    - pred is from {bvult}
+    - m is a numeral greater than 0
+}
+
+:definition
+  "This is a core theory for fixed-size bitvectors where the operations
+   of concatenation and extraction of bitvectors as well as the usual
+   logical and arithmetic operations are overloaded.
+   The theory is defined semantically as follows.
+
+   The sort BitVec[m] (for m > 0) is the set of finite functions
+   whose domain is the initial segment of the naturals [0...m), meaning
+   that 0 is included and m is excluded, and the co-domain is {0,1}.
+
+   The semantic interpretation [[_]] of well-sorted BitVec-terms is
+   inductively defined as follows.
+
+   - Variables
+
+   If v is a variable of sort BitVec[m] with 0 < m, then
+   [[v]] is some element of [{0,...,m-1} -> {0,1}], the set of total
+   functions from {0,...,m-1} to {0,1}.
+
+   - Constant symbols bit0 and bit1 of sort BitVec[1]
+
+   [[bit0]] := \lambda x : [0,1). 0
+   [[bit1]] := \lambda x : [0,1). 1
+
+   - Function symbols for concatenation
+
+   [[(concat s t)]] := \lambda x : [0...n+m).
+                          if (x<m) then [[t]](x) else [[s]](x-m)
+   where
+   s and t are terms of sort BitVec[n] and BitVec[m], respectively,
+   0 < n, 0 < m.
+
+   - Function symbols for extraction
+
+   [[(extract[i:j] s)]] := \lambda x : [0...i-j+1). [[s]](j+x)
+   where s is of sort BitVec[l], 0 <= j <= i < l.
+
+   - Bit-wise operations
+
+   [[(bvnot s)]] := \lambda x : [0...m). if [[s]](x) = 0 then 1 else 0
+
+   [[(bvand s t)]] := \lambda x : [0...m).
+                         if [[s]](x) = 0 then 0 else [[t]](x)
+
+   [[(bvor s t)]] := \lambda x : [0...m).
+                         if [[s]](x) = 1 then 1 else [[t]](x)
+
+   where s and t are both of sort BitVec[m] and 0 < m.
+
+   - Arithmetic operations
+
+   To define the semantics of the bitvector arithmetic operators, we first
+   introduce some additional definitions:
+
+   o (x div y) where x and y are integers with x >= 0 and y > 0 returns the
+     integer part of x divided by y (i.e., truncated integer division).
+
+   o (x rem y) where x and y are integers with x >= 0 and y > 0 returns the
+     remainder when x is divided by y.  Note that we always have the following
+     equivalence (for y > 0): (x div y) * y + (x rem y) = x.
+
+   o bv2nat which takes a bitvector b: [0...m) --> {0,1}
+     with 0 < m, and returns an integer in the range [0...2^m),
+     and is defined as follows:
+
+       bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ... + b(0)*2^0
+
+   o nat2bv[m], with 0 < m, which takes a non-negative integer
+     n and returns the (unique) bitvector b: [0,...,m) -> {0,1}
+     such that
+
+       b(m-1)*2^{m-1} + ... + b(0)*2^0 = n rem 2^m
+
+   Now, we can define the following operations.  Suppose s and t are both terms
+   of sort BitVec[m], m > 0.
+
+   [[(bvneg s)]] := nat2bv[m](2^m - bv2nat([[s]]))
+
+   [[(bvadd s t)]] := nat2bv[m](bv2nat([[s]]) + bv2nat([[t]]))
+
+   [[(bvmul s t)]] := nat2bv[m](bv2nat([[s]]) * bv2nat([[t]]))
+
+   [[(bvudiv s t)]] := if bv2nat([[t]]) != 0 then
+                          nat2bv[m](bv2nat([[s]]) div bv2nat([[t]]))
+
+   [[(bvurem s t)]] := if bv2nat([[t]]) != 0 then
+                          nat2bv[m](bv2nat([[s]]) rem bv2nat([[t]]))
+
+   - Shift operations
+
+   Suppose s and t are both terms of sort BitVec[m], m > 0.  We make use of the
+   definitions given for the arithmetic operations, above.
+
+   [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]])))
+
+   [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]])))
+
+   Finally, we can define the binary predicate bvult:
+
+   (bvult s t) is interpreted to be true iff bv2nat([[s]]) < bv2nat([[t]])
+
+   Note that the semantic interpretation above is underspecified because it
+   does not specify the meaning of (bvudiv s t) or (bvurem s t) in case
+   bv2nat([[t]]) is 0.  Since the semantics of SMT-LIB's underlying logic
+   associates *total* functions to function symbols, we then consider as models
+   of this theory *any* interpretation conforming to the specifications above
+   (and defining bvudiv and bvurem arbitrarily when the second argument
+   evaluates to 0).  Benchmarks using this theory should only include a
+   :status sat or :status unsat attribute if the status is independent of
+   the particular choice of model for the theory.
+
+  "
+
+)
diff --git a/docs/SMT-COMP/QF_AUFBV.smt b/docs/SMT-COMP/QF_AUFBV.smt
new file mode 100644
index 00000000..bc055c35
--- /dev/null
+++ b/docs/SMT-COMP/QF_AUFBV.smt
@@ -0,0 +1,19 @@
+(logic QF_AUFBV
+
+ :written_by {Clark Barrett}
+ :date {May 7, 2007}
+ 
+ :theory BV_ArraysEx
+
+ :language 
+ "Closed quantifier-free formulas built over an arbitrary expansion of the
+  BV_ArraysEx signature with free function and predicate symbols over
+  the sorts of BV_ArraysEx.  Formulas in ite terms must satisfy the same
+  restriction as well, with the exception that they need not be closed (because
+  they may be in the scope of a let expression).
+ "
+ :extensions
+ "As in the logic QF_BV."
+)
+
+
diff --git a/docs/SMT-COMP/QF_BV.smt b/docs/SMT-COMP/QF_BV.smt
new file mode 100644
index 00000000..edf02241
--- /dev/null
+++ b/docs/SMT-COMP/QF_BV.smt
@@ -0,0 +1,261 @@
+(logic QF_BV
+
+:written_by {Silvio Ranise, Cesare Tinelli, and Clark Barrett}
+:date {May 7, 2007}
+
+:theory Fixed_Size_BitVectors
+
+:language
+
+ "Closed quantifier-free formulas built over an arbitrary expansion of the
+  Fixed_Size_BitVectors signature with free constant symbols over the sorts
+  BitVec[m] for 0 < m.  Formulas in ite terms must satisfy the same restriction
+  as well, with the exception that they need not be closed (because they may be
+  in the scope of a let expression).
+ "
+
+:notes
+ "For quick reference, the following is a brief and informal summary of the
+  legal symbols in this logic and their meaning (formal definitions are found
+  either in the Fixed_Size_Bitvectors theory, or in the extensions below).
+
+  Defined in theory Fixed_Size_Bitvectors:
+
+    Functions/Constants:
+
+    (bit0 BitVec[1])
+      - the constant consisting of a single bit with value 0
+    (bit1 BitVec[1])
+      - the constant consisting of a single bit with value 1
+    (concat BitVec[i] BitVec[j] BitVec[m])
+      - concatenation of bitvectors of size i and j to get a new bitvector of
+        size m, where m = i + j
+    (extract[i:j] BitVec[m] BitVec[n])
+      - extraction of bits i down to j from a bitvector of size m to yield a
+        new bitvector of size n, where n = i - j + 1
+    (bvnot BitVec[m] BitVec[m])
+      - bitwise negation
+    (bvand BitVec[m] BitVec[m] BitVec[m])
+      - bitwise and
+    (bvor BitVec[m] BitVec[m] BitVec[m])
+      - bitwise or
+    (bvneg BitVec[m] BitVec[m])
+      - 2's complement unary minus
+    (bvadd BitVec[m] BitVec[m] BitVec[m])
+      - addition modulo 2^m
+    (bvmul BitVec[m] BitVec[m] BitVec[m])
+      - multiplication modulo 2^m
+    (bvudiv BitVec[m] BitVec[m] BitVec[m])
+      - unsigned division, truncating towards 0 (undefined if divisor is 0)
+    (bvurem BitVec[m] BitVec[m] BitVec[m])
+      - unsigned remainder from truncating division (undefined if divisor is 0)
+    (bvshl BitVec[m] BitVec[m] BitVec[m])
+      - shift left (equivalent to multiplication by 2^x where x is the value of
+        the second argument)
+    (bvlshr BitVec[m] BitVec[m] BitVec[m])
+      - logical shift right (equivalent to unsigned division by 2^x where x is
+        the value of the second argument)
+
+    Predicates:
+
+    (bvult BitVec[m] BitVec[m])
+      - binary predicate for unsigned less than
+
+  Defined below:
+
+    Functions/Constants:
+
+    Bitvector constants:
+      - bvX[m] where X is a numeral in base 10 defines the bitvector constant
+        with numeric value X of size m.
+      - bvbinX where X is a binary numeral of length m defines the
+        bitvector constant with value X and size m.
+      - bvhexX where X is a hexadecimal numeral of length m defines the
+        bitvector constant with value X and size 4*m.
+    (bvnand BitVec[m] BitVec[m] BitVec[m])
+      - bitwise nand (negation of and)
+    (bvnor BitVec[m] BitVec[m] BitVec[m])
+      - bitwise nor (negation of or)
+    (bvxor BitVec[m] BitVec[m] BitVec[m])
+      - bitwise exclusive or
+    (bvxnor BitVec[m] BitVec[m] BitVec[m])
+      - bitwise equivalence (equivalently, negation of bitwise exclusive or)
+    (bvcomp BitVec[m] BitVec[m] BitVec[1])
+      - bit comparator: equals bit1 iff all bits are equal
+    (bvsub BitVec[m] BitVec[m] BitVec[m])
+      - 2's complement subtraction modulo 2^m
+    (bvsdiv BitVec[m] BitVec[m] BitVec[m])
+      - 2's complement signed division
+    (bvsrem BitVec[m] BitVec[m] BitVec[m])
+      - 2's complement signed remainder (sign follows dividend)
+    (bvsmod BitVec[m] BitVec[m] BitVec[m])
+      - 2's complement signed remainder (sign follows divisor)
+    (bvashr BitVec[m] BitVec[m] BitVec[m])
+      - Arithmetic shift right, like logical shift right except that the most
+        significant bits of the result always copy the most significant
+        bit of the first argument.
+
+    The following symbols are parameterized by the numeral i, where i >= 0.
+
+    (repeat[i] BitVec[m] BitVec[i*m])
+      - (repeat[i] x) means concatenate i copies of x
+    (zero_extend[i] BitVec[m] BitVec[m+i])
+      - (zero_extend[i] x) means extend x with zeroes to the (unsigned)
+        equivalent bitvector of size m+i
+    (sign_extend[i] BitVec[m] BitVec[m+i])
+      - (sign_extend[i] x) means extend x to the (signed) equivalent bitvector
+        of size m+i
+    (rotate_left[i] BitVec[m] BitVec[m])
+      - (rotate_left[i] x) means rotate bits of x to the left i times
+    (rotate_right[i] BitVec[m] BitVec[m])
+      - (rotate_right[i] x) means rotate bits of x to the right y times
+
+    Predicates:
+
+    (bvule BitVec[m] BitVec[m])
+      - binary predicate for unsigned less than or equal
+    (bvugt BitVec[m] BitVec[m])
+      - binary predicate for unsigned greater than
+    (bvuge BitVec[m] BitVec[m])
+      - binary predicate for unsigned greater than or equal
+    (bvslt BitVec[m] BitVec[m])
+      - binary predicate for signed less than
+    (bvsle BitVec[m] BitVec[m])
+      - binary predicate for signed less than or equal
+    (bvsgt BitVec[m] BitVec[m])
+      - binary predicate for signed greater than
+    (bvsge BitVec[m] BitVec[m])
+      - binary predicate for signed greater than or equal
+
+ "
+
+:extensions
+ "Below, let |exp| denote the integer resulting from the evaluation
+  of the arithmetic expression exp.
+
+  - Bitvector Constants:
+    The string bv followed by the numeral n and a size [m] (as in bv13[32])
+    abbreviates any term t of sort BitVec[m] built only out of the symbols in
+    {concat, bit0, bit1} such that
+
+    [[t]] = nat2bv[m](n) for n=0, ..., 2^m - 1.
+
+    See the specification of the theory's semantics for a definition
+    of the functions [[_]] and nat2bv.  Note that this convention implicitly
+    considers the numeral n as a number written in base 10.
+
+    For backward compatibility, if the size [m] is omitted, then the size is
+    assumed to be 32.
+
+    The string bvbin followed by a sequence of 0's and 1's abbreviates the
+    concatenation of a similar sequence of bit0 and bit1 terms.  Thus,
+    if n is the numeral represented in base 2 by the sequence of 0's and 1's
+    and m is the length of the sequence, then the term represents
+    nat2bv[m](n).  For example bvbin0101 is equivalent to bv5[4].
+
+    The string bvhex followed by a sequence of digits and/or letters from A to
+    F is interpreted similarly as a concatenation of bit0 and bit1 as follows.
+    If n is the numeral represented in hexadecimal (base 16) by the sequence of
+    digits and letters from A to F and m is four times the length of the
+    sequence, then the term represents nat2bv[m](n).  For example, bvbinFF is
+    equivalent to bv255[8].  Letters in the hexadecimal sequence may be in
+    either upper or lower case.
+
+  - Bitwise operators
+
+    For all terms s,t of sort BitVec[m], where 0 < m,
+
+    (bvnand s t) abbreviates (bvnot (bvand s t))
+    (bvnor s t) abbreviates (bvnot (bvor s t))
+    (bvxor s t) abbreviates (bvor (bvand s (bvnot t)) (bvand (bvnot s) t))
+    (bvxnor s t) abbreviates (bvor (bvand s t) (bvand (bvnot s) (bvnot t)))
+    (bvcomp s t) abbreviates (bvxnor s t) if m = 1, and
+       (bvand (bvxnor (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t))
+              (bvcomp (extract[|m-2|:0] s) (extract[|m-2|:0] t))) otherwise
+
+  - Arithmetic operators
+
+    For all terms s,t of sort BitVec[m], where 0 < m,
+
+    (bvsub s t) abbreviates (bvadd s (bvneg t))
+    (bvsdiv s t) abbreviates
+      (let (?msb_s (extract[|m-1|:|m-1|] s))
+      (let (?msb_t (extract[|m-1|:|m-1|] t))
+      (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
+           (bvudiv s t)
+      (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
+           (bvneg (bvudiv (bvneg s) t))
+      (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
+           (bvneg (bvudiv s (bvneg t)))
+           (bvudiv (bvneg s) (bvneg t)))))))
+    (bvsrem s t) abbreviates
+      (let (?msb_s (extract[|m-1|:|m-1|] s))
+      (let (?msb_t (extract[|m-1|:|m-1|] t))
+      (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
+           (bvurem s t)
+      (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
+           (bvneg (bvurem (bvneg s) t))
+      (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
+           (bvurem s (bvneg t)))
+           (bvneg (bvurem (bvneg s) (bvneg t)))))))
+    (bvsmod s t) abbreviates
+      (let (?msb_s (extract[|m-1|:|m-1|] s))
+      (let (?msb_t (extract[|m-1|:|m-1|] t))
+      (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
+           (bvurem s t)
+      (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
+           (bvadd (bvneg (bvurem (bvneg s) t)) t)
+      (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
+           (bvadd (bvurem s (bvneg t)) t)
+           (bvneg (bvurem (bvneg s) (bvneg t)))))))
+    (bvule s t) abbreviates (or (bvult s t) (= s t))
+    (bvugt s t) abbreviates (bvult t s)
+    (bvuge s t) abbreviates (or (bvult t s) (= s t))
+    (bvslt s t) abbreviates:
+      (or (and (= (extract[|m-1|:|m-1|] s) bit1)
+               (= (extract[|m-1|:|m-1|] t) bit0))
+          (and (= (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t))
+               (bvult s t)))
+    (bvsle s t) abbreviates:
+      (or (and (= (extract[|m-1|:|m-1|] s) bit1)
+               (= (extract[|m-1|:|m-1|] t) bit0))
+          (and (= (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t))
+               (bvule s t)))
+    (bvsgt s t) abbreviates (bvslt t s)
+    (bvsge s t) abbreviates (bvsle t s)
+
+  - Other operations
+
+    For all numerals j > 1 and 0 < m, and all terms of s and t of
+    sort BitVec[m],
+
+    (bvashr s t) abbreviates 
+      (ite (= (extract[|m-1|:|m-1|] s) bit0)
+           (bvlshr s t)
+           (bvnot (bvlshr (bvnot s) t)))
+
+    (repeat[1] t) stands for t
+    (repeat[j] t) abbreviates (concat t (repeat[|j-1|] t))
+
+    (zero_extend[0] t) stands for t
+    (zero_extend[j] t) abbreviates (concat (repeat[j] bit0) t)
+
+    (sign_extend[0] t) stands for t
+    (sign_extend[j] t) abbreviates
+      (concat (repeat[j] (extract[|m-1|:|m-1|] t)) t)
+
+    (rotate_left[0] t) stands for t
+    (rotate_left[j] t) abbreviates t if m = 1, and
+      (rotate_left[|j-1|]
+        (concat (extract[|m-2|:0] t) (extract[|m-1|:|m-1|] t))
+      otherwise
+
+    (rotate_right[0] t) stands for t
+    (rotate_right[j] t) abbreviates t if m = 1, and
+      (rotate_right[|j-1|]
+        (concat (extract[0:0] t) (extract[|m-1|:1] t)))
+      otherwise
+
+ "
+)
+