about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml5
-rwxr-xr-x.travis/klee.sh19
-rwxr-xr-x.travis/metaSMT.sh6
-rw-r--r--.travis/sanitizer_flags.sh39
-rwxr-xr-x.travis/solvers.sh6
-rwxr-xr-x.travis/stp.sh7
-rw-r--r--Dockerfile4
-rw-r--r--Makefile.common10
-rw-r--r--cmake/modules/FindZ3.cmake3
-rw-r--r--include/klee/Expr.h5
-rw-r--r--include/klee/Internal/ADT/DiscretePDF.inc42
-rw-r--r--include/klee/util/Bits.h25
-rw-r--r--lib/Core/ExecutorUtil.cpp7
-rw-r--r--lib/SMT/LICENSE.CVC353
-rw-r--r--lib/SMT/Makefile27
-rw-r--r--lib/SMT/SMTParser.cpp245
-rw-r--r--lib/SMT/SMTParser.h92
-rw-r--r--lib/SMT/main.cpp40
-rw-r--r--lib/SMT/smtlib.lex263
-rw-r--r--lib/SMT/smtlib.y974
-rw-r--r--lib/Solver/STPSolver.cpp3
-rw-r--r--lib/Support/MemoryUsage.cpp65
-rw-r--r--runtime/CMakeLists.txt30
-rw-r--r--runtime/Runtest/Makefile6
-rw-r--r--test/CMakeLists.txt4
-rw-r--r--test/Feature/Vararg.c2
-rw-r--r--test/Makefile4
27 files changed, 231 insertions, 1755 deletions
diff --git a/.travis.yml b/.travis.yml
index 435d5139..a0b5e7ae 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -38,7 +38,6 @@ env:
     #- LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1
     #- LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 USE_CMAKE=1
 
-    # TODO: Add ASan build
     # TODO: Add coverage build
     # TODO: Add Doxygen build
 
@@ -47,6 +46,10 @@ env:
     - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
     - LLVM_VERSION=2.9 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 USE_CMAKE=1
 
+    # ASan build. Do unoptimized build otherwise the optimizer might remove problematic code
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_CMAKE=1 USE_TCMALLOC=0 ASAN_BUILD=1
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_CMAKE=0 USE_TCMALLOC=0 ASAN_BUILD=1
+
     # TODO: Port all configurations below to CMake build system
 
     # Test we can still build with Z3 in the old build sytem
diff --git a/.travis/klee.sh b/.travis/klee.sh
index 8db724ac..61806df3 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -112,6 +112,11 @@ else
 fi
 
 ###############################################################################
+# Handle Sanitizer flags
+###############################################################################
+source ${KLEE_SRC}/.travis/sanitizer_flags.sh
+
+###############################################################################
 # KLEE
 ###############################################################################
 mkdir klee
@@ -131,7 +136,8 @@ if [ "X${USE_CMAKE}" == "X1" ]; then
     CMAKE_BUILD_TYPE="Debug"
   fi
   # Compute CMake build type
-  CXXFLAGS="${COVERAGE_FLAGS}" \
+  CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
+  CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
   cmake \
     -DLLVM_CONFIG_BINARY="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config" \
     -DLLVMCC="${KLEE_CC}" \
@@ -163,11 +169,12 @@ else
               ${KLEE_METASMT_CONFIGURE_OPTION} \
               ${KLEE_UCLIBC_CONFIGURE_OPTION} \
               ${TCMALLOC_OPTION} \
-              CXXFLAGS="${COVERAGE_FLAGS}"
-  make \
-    DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
-    ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
-    ENABLE_SHARED=0
+              CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
+              CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
+              LDFLAGS="${SANITIZER_LD_FLAGS}"
+  make  DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
+        ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
+        ENABLE_SHARED=0
 fi
 
 ###############################################################################
diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh
index 7195ceb0..6376c4bc 100755
--- a/.travis/metaSMT.sh
+++ b/.travis/metaSMT.sh
@@ -8,6 +8,12 @@ git clone git://github.com/hoangmle/metaSMT.git
 cd metaSMT
 git clone git://github.com/agra-uni-bremen/dependencies.git
 
+source ${KLEE_SRC}/.travis/sanitizer_flags.sh
+if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
+  echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented"
+  exit 1
+fi
+
 # Bootstrap
 export BOOST_ROOT=/usr
 sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack
diff --git a/.travis/sanitizer_flags.sh b/.travis/sanitizer_flags.sh
new file mode 100644
index 00000000..4d3dce2c
--- /dev/null
+++ b/.travis/sanitizer_flags.sh
@@ -0,0 +1,39 @@
+# This file is meant to be included by shell scripts
+# that need to do a sanitized build.
+
+# Users of this script can use this variable
+# to detect if a Sanitized build was enabled.
+IS_SANITIZED_BUILD=0
+
+# AddressSanitizer
+if [ "X${ASAN_BUILD}" == "X1" ]; then
+  echo "Using ASan"
+  ASAN_CXX_FLAGS="-fsanitize=address -fno-omit-frame-pointer"
+  ASAN_C_FLAGS="${ASAN_CXX_FLAGS}"
+  ASAN_LD_FLAGS="${ASAN_CXX_FLAGS}"
+  IS_SANITIZED_BUILD=1
+else
+  echo "Not using ASan"
+  ASAN_CXX_FLAGS=""
+  ASAN_C_FLAGS=""
+  ASAN_LD_FLAGS=""
+fi
+
+# Undefined Behaviour Sanitizer
+if [ "X${UBSAN_BUILD}" == "X1" ]; then
+  echo "Using UBSan"
+  UBSAN_CXX_FLAGS="-fsanitize=undefined"
+  UBSAN_C_FLAGS="${UBSAN_CXX_FLAGS}"
+  UBSAN_LD_FLAGS="${UBSAN_CXX_FLAGS}"
+  IS_SANITIZED_BUILD=1
+else
+  echo "Not using UBSan"
+  UBSAN_CXX_FLAGS=""
+  UBSAN_C_FLAGS=""
+  UBSAN_LD_FLAGS=""
+fi
+
+# Set variables to be used by clients.
+SANITIZER_CXX_FLAGS="${ASAN_CXX_FLAGS} ${UBSAN_CXX_FLAGS}"
+SANITIZER_C_FLAGS="${ASAN_C_FLAGS} ${UBSAN_C_FLAGS}"
+SANITIZER_LD_FLAGS="${ASAN_LD_FLAGS} ${UBSAN_LD_FLAGS}"
diff --git a/.travis/solvers.sh b/.travis/solvers.sh
index d64c1077..04f3276f 100755
--- a/.travis/solvers.sh
+++ b/.travis/solvers.sh
@@ -16,6 +16,12 @@ for solver in ${SOLVER_LIST}; do
     cd ../
     ;;
   Z3)
+    # FIXME: Move this into its own script
+    source ${KLEE_SRC}/.travis/sanitizer_flags.sh
+    if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
+      echo "Error: Requested Sanitized build but Z3 being used is not sanitized"
+      exit 1
+    fi
     echo "Z3"
     # Should we install libz3-dbg too?
     sudo apt-get -y install libz3 libz3-dev
diff --git a/.travis/stp.sh b/.travis/stp.sh
index 53b7b6bc..4cc55c62 100755
--- a/.travis/stp.sh
+++ b/.travis/stp.sh
@@ -6,12 +6,17 @@ set -e
 STP_LOG="$(pwd)/stp-build.log"
 
 if [ "x${STP_VERSION}" != "x" ]; then
+    # Get Sanitizer flags
+    source ${KLEE_SRC}/.travis/sanitizer_flags.sh
+
     # Build minisat
     git clone https://github.com/stp/minisat
     cd minisat
     mkdir build
     cd build
     MINISAT_DIR=`pwd`
+    CFLAGS="${SANITIZER_C_FLAGS}" \
+    CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
     cmake -DCMAKE_INSTALL_PREFIX=/usr ..
     make
     sudo make install
@@ -23,6 +28,8 @@ if [ "x${STP_VERSION}" != "x" ]; then
     cd build
     # Disabling building of shared libs is a workaround.
     # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8
+    CFLAGS="${SANITIZER_C_FLAGS}" \
+    CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
     cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF -DNO_BOOST:BOOL=ON ../src
 
     set +e # Do not exit if build fails because we need to display the log
diff --git a/Dockerfile b/Dockerfile
index 747cbef8..d42b09c8 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -14,7 +14,9 @@ ENV LLVM_VERSION=3.4 \
     KLEE_SRC=/home/klee/klee_src \
     COVERAGE=0 \
     BUILD_DIR=/home/klee/klee_build \
-    USE_CMAKE=1
+    USE_CMAKE=1 \
+    ASAN_BUILD=0 \
+    UBSAN_BUILD=0
 
 RUN apt-get update && \
     apt-get -y --no-install-recommends install \
diff --git a/Makefile.common b/Makefile.common
index a6ce34fb..0eb741ea 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -80,8 +80,14 @@ endif
 # For metaSMT
 include $(PROJ_SRC_ROOT)/MetaSMT.mk
 
-# If building KLEE with the Sanitizers don't build the runtime with it
-# because KLEE doesn't know how to handle it.
+# When building the runtime filter out unwanted flags.
+# that add instrumentatation because KLEE can't handle this.
 ifneq ("X$(MODULE_NAME)$(BYTECODE_LIBRARY)X","XX")
+  # Sanitizer flags.
   CFLAGS := $(filter-out -fsanitize=%,$(CFLAGS))
+  # Coverag flags.
+  CFLAGS := $(filter-out -fprofile-arcs,$(CFLAGS))
+  CFLAGS := $(filter-out -ftest-coverage,$(CFLAGS))
+  CFLAGS := $(filter-out -coverage,$(CFLAGS))
+  CFLAGS := $(filter-out --coverage,$(CFLAGS))
 endif
diff --git a/cmake/modules/FindZ3.cmake b/cmake/modules/FindZ3.cmake
index b5f90974..999ed14e 100644
--- a/cmake/modules/FindZ3.cmake
+++ b/cmake/modules/FindZ3.cmake
@@ -20,6 +20,9 @@ endif()
 # Try to find headers
 find_path(Z3_INCLUDE_DIRS
   NAMES z3.h
+  # For distributions that keep the header files in a `z3` folder,
+  # for example Fedora's `z3-devel` package at `/usr/include/z3/z3.h`
+  PATH_SUFFIXES z3
   DOC "Z3 C header"
 )
 if (Z3_INCLUDE_DIRS)
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 4584ab0d..6c5351df 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -1080,7 +1080,10 @@ public:
   }
 
   static ref<ConstantExpr> create(uint64_t v, Width w) {
-    assert(v == bits64::truncateToNBits(v, w) && "invalid constant");
+#ifndef NDEBUG
+    if (w <= 64)
+      assert(v == bits64::truncateToNBits(v, w) && "invalid constant");
+#endif
     return alloc(v, w);
   }
 
diff --git a/include/klee/Internal/ADT/DiscretePDF.inc b/include/klee/Internal/ADT/DiscretePDF.inc
index 5aee2de5..eb7bd860 100644
--- a/include/klee/Internal/ADT/DiscretePDF.inc
+++ b/include/klee/Internal/ADT/DiscretePDF.inc
@@ -162,32 +162,32 @@ void DiscretePDF<T>::update(T item, weight_type weight) {
 
 template <class T>
 T DiscretePDF<T>::choose(double p) {
-  if (p<0.0 || p>=1.0) {
+  if ((p < 0.0) || (p >= 1.0))
     assert(0 && "choose: argument(p) outside valid range");
-  } else if (!m_root) {
+
+  if (!m_root)
     assert(0 && "choose: choose() called on empty tree");
-  } else {
-    weight_type w = (weight_type) (m_root->sumWeights * p);
-    Node *n = m_root;
-
-    while (1) {
-      if (n->left) {
-        if (w<n->left->sumWeights) {
-          n = n->left;
-          continue;
-        } else {
-          w -= n->left->sumWeights;
-        }
-      }
-      if (w<n->weight || !n->right) {
-        break; // !n->right condition shouldn't be necessary, just sanity check
+
+  weight_type w = (weight_type) (m_root->sumWeights * p);
+  Node *n = m_root;
+
+  while (1) {
+    if (n->left) {
+      if (w<n->left->sumWeights) {
+	n = n->left;
+	continue;
+      } else {
+	w -= n->left->sumWeights;
       }
-      w -= n->weight;
-      n = n->right;
     }
-
-    return n->key;
+    if (w<n->weight || !n->right) {
+      break; // !n->right condition shouldn't be necessary, just sanity check
+    }
+    w -= n->weight;
+    n = n->right;
   }
+
+  return n->key;
 }
 
 template <class T>
diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h
index f228b289..d56c7c21 100644
--- a/include/klee/util/Bits.h
+++ b/include/klee/util/Bits.h
@@ -12,20 +12,23 @@
 
 #include "klee/Config/Version.h"
 #include "llvm/Support/DataTypes.h"
+#include <assert.h>
 
 namespace klee {
   namespace bits32 {
     // @pre(0 <= N <= 32)
     // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
     inline unsigned maxValueOfNBits(unsigned N) {
+      assert(N <= 32);
       if (N==0)
         return 0;
-      return ((unsigned) -1) >> (32 - N);
+      return (UINT32_C(-1)) >> (32 - N);
     }
 
     // @pre(0 < N <= 32)
     inline unsigned truncateToNBits(unsigned x, unsigned N) {
-      return x&(((unsigned) -1) >> (32 - N));
+      assert(N > 0 && N <= 32);
+      return x&((UINT32_C(-1)) >> (32 - N));
     }
 
     inline unsigned withoutRightmostBit(unsigned x) {
@@ -44,12 +47,15 @@ namespace klee {
     // @pre(withoutRightmostBit(x) == 0)
     // @post((1 << retval) == x)
     inline unsigned indexOfSingleBit(unsigned x) {
+      assert(withoutRightmostBit(x) == 0);
       unsigned res = 0;
       if (x&0xFFFF0000) res += 16;
       if (x&0xFF00FF00) res += 8;
       if (x&0xF0F0F0F0) res += 4;
       if (x&0xCCCCCCCC) res += 2;
       if (x&0xAAAAAAAA) res += 1;
+      assert(res < 32);
+      assert((UINT32_C(1) << res) == x);
       return res;
     } 
 
@@ -59,17 +65,19 @@ namespace klee {
   }
 
   namespace bits64 {
-    // @pre(0 <= N <= 32)
+    // @pre(0 <= N <= 64)
     // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
     inline uint64_t maxValueOfNBits(unsigned N) {
+      assert(N <= 64);
       if (N==0)
         return 0;
-      return ((uint64_t) (int64_t) -1) >> (64 - N);
+      return ((UINT64_C(-1)) >> (64 - N));
     }
     
     // @pre(0 < N <= 64)
     inline uint64_t truncateToNBits(uint64_t x, unsigned N) {
-      return x&(((uint64_t) (int64_t) -1) >> (64 - N));
+      assert(N > 0 && N <= 64);
+      return x&((UINT64_C(-1)) >> (64 - N));
     }
 
     inline uint64_t withoutRightmostBit(uint64_t x) {
@@ -88,9 +96,12 @@ namespace klee {
     // @pre((x&(x-1)) == 0)
     // @post((1 << retval) == x)
     inline unsigned indexOfSingleBit(uint64_t x) {
+      assert((x & (x - 1)) == 0);
       unsigned res = bits32::indexOfSingleBit((unsigned) (x | (x>>32)));
-      if (x&((uint64_t) 0xFFFFFFFF << 32))
-	  res += 32;
+      if (x & (UINT64_C(0xFFFFFFFF) << 32))
+        res += 32;
+      assert(res < 64);
+      assert((UINT64_C(1) << res) == x);
       return res;
     } 
 
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 56f18e6b..b91b5dee 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -153,6 +153,11 @@ namespace klee {
     case Instruction::FCmp:
       assert(0 && "floating point ConstantExprs unsupported");
     }
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
+    llvm_unreachable("Unsupported expression in evalConstantExpr");
+#else
+    assert(0 && "Unsupported expression in evalConstantExpr");
+#endif
+    return op1;
   }
-
 }
diff --git a/lib/SMT/LICENSE.CVC3 b/lib/SMT/LICENSE.CVC3
deleted file mode 100644
index a70d12d5..00000000
--- a/lib/SMT/LICENSE.CVC3
+++ /dev/null
@@ -1,53 +0,0 @@
-/*!\page LICENSE LICENSE
-
-Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior
-University, New York University, and the University of Iowa, hereafter
-designated as the Copyright Owners.
-
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without modification,
-are permitted provided that the following conditions are met:
-
-* Redistributions of source code must retain the above copyright notice, this
-list of conditions and the following disclaimer.
-* Redistributions in binary form must reproduce the above copyright notice,
-this list of conditions and the following disclaimer in the documentation
-and/or other materials provided with the distribution.
-* Neither the names of the Copyright Owners nor the names of any contributors
-may be used to endorse or promote products derived from this software
-without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY
-EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
-WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY
-DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
-(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
-ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-Note:
-
-The following files contain code whose copyright does not belong to the
-Copyright Owners.  However, separate copyright notices in these files give
-express permission to copy, use, modify, sell, or distribute the code.  Please
-see the copyright notices in the individual files for details.
-
-<pre>
-src/include/fdstream.h
-src/include/hash_map.h
-src/include/hash_fun.h
-src/include/hash_set.h
-src/include/hash_table.h
-src/sat/minisat_varorder.h
-src/sat/minisat_solver.cpp
-src/sat/minisat_heap.h
-src/sat/minisat_types.h
-src/sat/minisat_solver.h
-src/sat/minisat_global.h
-</pre>
-
-*/
diff --git a/lib/SMT/Makefile b/lib/SMT/Makefile
deleted file mode 100644
index 92ec8018..00000000
--- a/lib/SMT/Makefile
+++ /dev/null
@@ -1,27 +0,0 @@
-#===-- lib/SMT/Makefile ------------------------------------*- Makefile -*--===#
-
-LEVEL=../..
-
-LIBRARYNAME=kleaverSMT
-DONT_BUILD_RELINKED=1
-BUILD_ARCHIVE=1
-
-include $(LEVEL)/Makefile.common
-
-# Gross, but I don't want to build proper rules for this, and I don't want users
-# to have to have bison/flex, so for now require developers to make these
-# manually (at least initially).
-
-smtlib_parser.cpp smtlib_parser.h: smtlib.y
-	bison -d -o smtlib_parser.cpp -p smtlib smtlib.y
-	mv smtlib_parser.hpp smtlib_parser.h	
-	perl -pi -e 's/union/struct/g' smtlib_parser.cpp
-	perl -pi -e 's/union/struct/g' smtlib_parser.h
-
-
-smtlib_lexer.cpp: smtlib.lex smtlib_parser.h
-	flex -I -Psmtlib -osmtlib_lexer.cpp smtlib.lex
-	perl -pi -e 's/union/struct/g' smtlib_lexer.cpp
-
-.PHONY: regen
-regen: smtlib_lexer.cpp smtlib_parser.cpp smtlib_parser.h
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
deleted file mode 100644
index 19ce5af7..00000000
--- a/lib/SMT/SMTParser.cpp
+++ /dev/null
@@ -1,245 +0,0 @@
-//===-- SMTParser.cpp -----------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "SMTParser.h"
-
-#include "klee/ExprBuilder.h"
-#include "klee/Solver.h"
-#include "klee/Constraints.h"
-#include "expr/Parser.h"
-
-#include <fstream>
-#include <string>
-#include <sstream>
-#include <cassert>
-#include <stack>
-
-//#define DEBUG
-
-using namespace klee;
-using namespace klee::expr;
-
-extern int smtlibparse(); 
-extern void *smtlib_createBuffer(int);
-extern void smtlib_deleteBuffer(void *);
-extern void smtlib_switchToBuffer(void *);
-extern int smtlib_bufSize(void);
-extern void smtlib_setInteractive(bool);
-
-SMTParser* SMTParser::parserTemp = NULL;
-
-SMTParser::SMTParser(const std::string _filename, 
-		     ExprBuilder* _builder) : fileName(_filename),
-					      lineNum(1),
-					      done(false),
-					      satQuery(NULL),
-					      bvSize(0),
-					      queryParsed(false),
-					      builder(_builder) {
-  is = new ifstream(fileName.c_str());
-  
-  // Initial empty environments
-  varEnvs.push(VarEnv());
-  fvarEnvs.push(FVarEnv());
-}
-
-void SMTParser::Parse() {
-  SMTParser::parserTemp = this;
-
-  void *buf = smtlib_createBuffer(smtlib_bufSize());
-  smtlib_switchToBuffer(buf);
-  smtlib_setInteractive(false);
-  smtlibparse();
-  //xcout << "Parsed successfully.\n";
-}
-
-Decl* SMTParser::ParseTopLevelDecl() {
-  return new QueryCommand(assumptions, builder->Not(satQuery),
-			  std::vector<ExprHandle>(), 
-			  std::vector<const Array*>());
-}
-
-bool SMTParser::Solve() {
-  // FIXME: Support choice of solver.
-  bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryKQueryLog = true;
-  Solver *S, *STP = S = 
-    UseDummySolver ? createDummySolver() : new STPSolver(true);
-  if (UseSTPQueryKQueryLog)
-    S = createKQueryLoggingSolver(S, "stp-queries.kquery");
-  if (UseFastCexSolver)
-    S = createFastCexSolver(S);
-  S = createCexCachingSolver(S);
-  S = createCachingSolver(S);
-  S = createIndependentSolver(S);
-  if (0)
-    S = createValidatingSolver(S, STP);
-
-  Decl *D = this->ParseTopLevelDecl();
-  if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
-    //llvm::cout << "Query " << ":\t";
-
-    assert("FIXME: Support counterexample query commands!");
-    if (QC->Values.empty() && QC->Objects.empty()) {
-      bool result;
-      if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
-			result)) {
-	//std::cout << (result ? "VALID" : "INVALID") << "\n";
-	return result;	
-      }
-    }
-  }
-  llvm::cout << "FAIL";
-  exit(1);
-}
-
-
-// XXX: give more info
-int SMTParser::Error(const string& msg) {
-  llvm::errs() << SMTParser::parserTemp->fileName << ":"
-               << SMTParser::parserTemp->lineNum << ": " << msg << "\n";
-  exit(1);
-  return 0;
-}
-
-
-int SMTParser::StringToInt(const std::string& s) {
-  std::stringstream str(s);
-  int x;
-  str >> x;
-  assert(str);
-  return x;
-}
-
-
-ExprHandle SMTParser::CreateAnd(std::vector<ExprHandle> kids) {
-  unsigned n_kids = kids.size();
-  assert(n_kids);
-  if (n_kids == 1)
-    return kids[0];
-
-  ExprHandle r = builder->And(kids[n_kids-2], kids[n_kids-1]);
-  for (int i=n_kids-3; i>=0; i--)
-    r = builder->And(kids[i], r);
-  return r;
-}
-
-ExprHandle SMTParser::CreateOr(std::vector<ExprHandle> kids) {
-  unsigned n_kids = kids.size();
-  assert(n_kids);
-  if (n_kids == 1)
-    return kids[0];
-
-  ExprHandle r = builder->Or(kids[n_kids-2], kids[n_kids-1]);
-  for (int i=n_kids-3; i>=0; i--)
-    r = builder->Or(kids[i], r);
-  return r;
-}
-
-ExprHandle SMTParser::CreateXor(std::vector<ExprHandle> kids) {
-  unsigned n_kids = kids.size();
-  assert(n_kids);
-  if (n_kids == 1)
-    return kids[0];
-
-  ExprHandle r = builder->Xor(kids[n_kids-2], kids[n_kids-1]);
-  for (int i=n_kids-3; i>=0; i--)
-    r = builder->Xor(kids[i], r);
-  return r;
-}
-
-
-void SMTParser::DeclareExpr(std::string name, Expr::Width w) {
-  // for now, only allow variables which are multiples of 8
-  if (w % 8 != 0) {
-    cout << "BitVec not multiple of 8 (" << w << ").  Need to update code.\n";
-    exit(1);
-  }
-  
-#ifdef DEBUG
-  std::cout << "Declaring " << name << " of width " << w << "\n";
-#endif
-  
-  const Array *arr = Array::CreateArray(name, w / 8);
-  
-  ref<Expr> *kids = new ref<Expr>[w/8];
-  for (unsigned i=0; i < w/8; i++)
-    kids[i] = builder->Read(UpdateList(arr, NULL), 
-			    builder->Constant(i, 32));
-  ref<Expr> var = ConcatExpr::createN(w/8, kids); // XXX: move to builder?
-  delete [] kids;
-  
-  AddVar(name, var);
-}
-
-
-ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w) {
-  assert(base == 2 || base == 10 || base == 16);
-  llvm::APInt ap(w, val.c_str(), val.length(), base);
-  
-  return klee::ConstantExpr::alloc(ap);
-}
-
-
-void SMTParser::PushVarEnv() {
-#ifdef DEBUG
-  cout << "Pushing new var env\n";
-#endif
-  varEnvs.push(VarEnv(varEnvs.top()));
-}
-
-void SMTParser::PopVarEnv() {
-#ifdef DEBUG
-  cout << "Popping var env\n";
-#endif
-  varEnvs.pop();
-}
-
-void SMTParser::AddVar(std::string name, ExprHandle val) {
-#ifdef DEBUG
-  cout << "Adding (" << name << ", " << val << ") to current var env.\n";
-#endif
-  varEnvs.top()[name] = val;
-}
-
-ExprHandle SMTParser::GetVar(std::string name) {
-  VarEnv top = varEnvs.top();
-  if (top.find(name) == top.end()) {
-    llvm::errs() << "Cannot find variable ?" << name << "\n";
-    exit(1);
-  }
-  return top[name];
-}
-
-
-void SMTParser::PushFVarEnv() {
-  fvarEnvs.push(FVarEnv(fvarEnvs.top()));
-}
-
-void SMTParser::PopFVarEnv(void) {
-#ifdef DEBUG
-  cout << "Popping fvar env\n";
-#endif
-  fvarEnvs.pop();
-}
-
-void SMTParser::AddFVar(std::string name, ExprHandle val) {
-#ifdef DEBUG
-  cout << "Adding (" << name << ", " << val << ") to current fvar env.\n";
-#endif
-  fvarEnvs.top()[name] = val;
-}
-
-ExprHandle SMTParser::GetFVar(std::string name) {
-  FVarEnv top = fvarEnvs.top();
-  if (top.find(name) == top.end()) {
-    llvm::errs() << "Cannot find fvar $" << name << "\n";
-    exit(1);
-  }
-  return top[name];
-}
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
deleted file mode 100644
index ac84e74c..00000000
--- a/lib/SMT/SMTParser.h
+++ /dev/null
@@ -1,92 +0,0 @@
-//===-- SMTParser.h -------------------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-
-#ifndef SMT_PARSER_H
-#define SMT_PARSER_H
-
-#include "expr/Parser.h"
-
-#include <map>
-#include <stack>
-#include <string>
-
-namespace klee {
-  class ExprBuilder;
-  
-namespace expr {
-
-class SMTParser : public klee::expr::Parser {
-  private:
-    void *buf;
-    
- public:
-  /* For interacting w/ the actual parser, should make this nicer */
-  static SMTParser* parserTemp;
-  std::string fileName;
-  std::istream* is;
-  int lineNum;
-  bool done;
-  bool arraysEnabled;
-  
-  std::vector<ExprHandle> assumptions;
-  klee::expr::ExprHandle satQuery;
-
-  int bvSize;
-  bool queryParsed;
-  
-  klee::ExprBuilder *builder;
-    
-  SMTParser(const std::string filename, ExprBuilder *builder);
-  
-  virtual klee::expr::Decl *ParseTopLevelDecl();
-  bool Solve();
-  
-  virtual void SetMaxErrors(unsigned N) { }
-  
-  virtual unsigned GetNumErrors() const {  return 1; }
-  
-  virtual ~SMTParser() {}
-  
-  void Parse(void);
-  
-  int Error(const std::string& s);
-  
-  int StringToInt(const std::string& s);
-  ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w);
-  
-  void DeclareExpr(std::string name, Expr::Width w);
-  
-  ExprHandle CreateAnd(std::vector<ExprHandle>);
-  ExprHandle CreateOr(std::vector<ExprHandle>);
-  ExprHandle CreateXor(std::vector<ExprHandle>);
-  
-
-  typedef std::map<const std::string, ExprHandle> VarEnv;
-  typedef std::map<const std::string, ExprHandle> FVarEnv;
-
-  std::stack<VarEnv> varEnvs;
-  std::stack<FVarEnv> fvarEnvs;
-
-  void PushVarEnv(void);
-  void PopVarEnv(void);
-  void AddVar(std::string name, ExprHandle val); // to current var env
-  ExprHandle GetVar(std::string name); // from current var env
-
-  void PushFVarEnv(void);
-  void PopFVarEnv(void);
-  void AddFVar(std::string name, ExprHandle val); // to current fvar env
-  ExprHandle GetFVar(std::string name); // from current fvar env
-};
-
-}
-}
-
-#endif
-
diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
deleted file mode 100644
index 31fa311d..00000000
--- a/lib/SMT/main.cpp
+++ /dev/null
@@ -1,40 +0,0 @@
-#include "SMTParser.h"
-
-#include "klee/ExprBuilder.h"
-
-using namespace klee;
-
-int main(int argc, char** argv) {
-  if (argc != 2) {
-    cout << "Usage: " << argv[0] << " <smt-filename>\n";
-    return 1;
-  }
-  
-  enum BuilderKinds {
-    DefaultBuilder,
-    ConstantFoldingBuilder,
-    SimplifyingBuilder
-  } BuilderKind = SimplifyingBuilder;
-
-  ExprBuilder *Builder = 0;
-  switch (BuilderKind) {
-  case DefaultBuilder:
-    Builder = createDefaultExprBuilder();
-    break;
-  case ConstantFoldingBuilder:
-    Builder = createDefaultExprBuilder();
-    Builder = createConstantFoldingExprBuilder(Builder);
-    break;
-  case SimplifyingBuilder:
-    Builder = createDefaultExprBuilder();
-    Builder = createConstantFoldingExprBuilder(Builder);
-    Builder = createSimplifyingExprBuilder(Builder);
-    break;
-  }
-  
-  klee::expr::SMTParser smtParser(argv[1], Builder);
-  smtParser.Parse();
-  int result = smtParser.Solve();
-  
-  cout << (result ? "UNSAT":"SAT") << "\n"; 
-}
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
deleted file mode 100644
index c614c683..00000000
--- a/lib/SMT/smtlib.lex
+++ /dev/null
@@ -1,263 +0,0 @@
-%{
-/*****************************************************************************/
-/*!
- * \file smtlib.lex
- * 
- * Author: Clark Barrett
- * 
- * Created: 2005
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-
-#include <iostream>
-#include "SMTParser.h"
-#include "smtlib_parser.h"
-
-using namespace klee;
-using namespace klee::expr;
-
-extern int smtlib_inputLine;
-extern char *smtlibtext;
-
-extern int smtliberror (const char *msg);
-
-static int smtlibinput(std::istream& is, char* buf, int size) {
-  int res;
-  if(is) {
-    // Set the terminator char to 0
-    is.getline(buf, size-1, 0);
-    // If failbit is set, but eof is not, it means the line simply
-    // didn't fit; so we clear the state and keep on reading.
-    bool partialStr = is.fail() && !is.eof();
-    if(partialStr)
-      is.clear();
-
-    for(res = 0; res<size && buf[res] != 0; res++) ;
-    if(res == size) smtliberror("Lexer bug: overfilled the buffer");
-    if(!partialStr) { // Insert \n into the buffer
-      buf[res++] = '\n';
-      buf[res] = '\0';
-    }
-  } else {
-    res = YY_NULL;
-  }
-  return res;
-}
-
-// Redefine the input buffer function to read from an istream
-#define YY_INPUT(buf,result,max_size) \
-  result = smtlibinput(*SMTParser::parserTemp->is, buf, max_size);
-
-int smtlib_bufSize() { return YY_BUF_SIZE; }
-YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }
-
-/* some wrappers for methods that need to refer to a struct.
-   These are used by SMTParser. */
-void *smtlib_createBuffer(int sz) {
-  return (void *)smtlib_create_buffer(NULL, sz);
-}
-void smtlib_deleteBuffer(void *buf_state) {
-  smtlib_delete_buffer((struct yy_buffer_state *)buf_state);
-}
-void smtlib_switchToBuffer(void *buf_state) {
-  smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state);
-}
-void *smtlib_bufState() {
-  return (void *)smtlib_buf_state();
-}
-
-void smtlib_setInteractive(bool is_interactive) {
-  yy_set_interactive(is_interactive);
-}
-
-// File-static (local to this file) variables and functions
-static std::string _string_lit;
-
- static char escapeChar(char c) {
-   switch(c) {
-   case 'n': return '\n';
-   case 't': return '\t';
-   default: return c;
-   }
- }
-
-// for now, we don't have subranges.  
-//
-// ".."		{ return DOTDOT_TOK; }
-/*OPCHAR	(['!#?\_$&\|\\@])*/
-
-%}
-
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
-%x	COMMENT
-%x	STRING_LITERAL
-%x      USER_VALUE
-%s      PAT_MODE
-
-LETTER	([a-zA-Z])
-DIGIT	([0-9])
-OPCHAR	(['\.\_])
-IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
-%%
-
-[\n]            { SMTParser::parserTemp->lineNum++; }
-[ \t\r\f]	{ /* skip whitespace */ }
-
-{DIGIT}+	{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
-
-";"		{ BEGIN COMMENT; }
-<COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  SMTParser::parserTemp->lineNum++; }
-<COMMENT>.	{ /* stay in comment mode */ }
-
-<INITIAL>"\""		{ BEGIN STRING_LITERAL; 
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-<STRING_LITERAL>"\\".	{ /* escape characters (like \n or \") */
-                          _string_lit.insert(_string_lit.end(),
-                                             escapeChar(smtlibtext[1])); }
-<STRING_LITERAL>"\""	{ BEGIN INITIAL; /* return to normal mode */ 
-			  smtliblval.str = new std::string(_string_lit);
-                          return STRING_TOK; }
-<STRING_LITERAL>.	{ _string_lit.insert(_string_lit.end(),*smtlibtext); }
-
-<INITIAL>":pat"		{ BEGIN PAT_MODE;
-                          return PAT_TOK;}
-<PAT_MODE>"}"	        { BEGIN INITIAL; 
-                          return RCURBRACK_TOK; }
-<INITIAL>"{"		{ BEGIN USER_VALUE;
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-<USER_VALUE>"\\"[{}] { /* escape characters */
-                          _string_lit.insert(_string_lit.end(),smtlibtext[1]); }
-
-<USER_VALUE>"}"	        { BEGIN INITIAL; /* return to normal mode */ 
-			  smtliblval.str = new std::string(_string_lit);
-                          return USER_VAL_TOK; }
-
-<USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');
-                          SMTParser::parserTemp->lineNum++; }
-<USER_VALUE>.	        { _string_lit.insert(_string_lit.end(),*smtlibtext); }
-
-"BitVec"        { return BITVEC_TOK; }
-
-"true"          { return TRUE_TOK; }
-"false"         { return FALSE_TOK; }
-"ite"           { return ITE_TOK; }
-"not"           { return NOT_TOK; }
-"implies"       { return IMPLIES_TOK; }
-"if_then_else"  { return IF_THEN_ELSE_TOK; }
-"and"           { return AND_TOK; }
-"or"            { return OR_TOK; }
-"xor"           { return XOR_TOK; }
-"iff"           { return IFF_TOK; }
-"exists"        { return EXISTS_TOK; }
-"forall"        { return FORALL_TOK; }
-"let"           { return LET_TOK; }
-"flet"          { return FLET_TOK; }
-"notes"         { return NOTES_TOK; }
-"cvc_command"   { return CVC_COMMAND_TOK; }
-"sorts"         { return SORTS_TOK; }
-"funs"          { return FUNS_TOK; }
-"preds"         { return PREDS_TOK; }
-"extensions"    { return EXTENSIONS_TOK; }
-"definition"    { return DEFINITION_TOK; }
-"axioms"        { return AXIOMS_TOK; }
-"logic"         { return LOGIC_TOK; }
-"sat"           { return SAT_TOK; }
-"unsat"         { return UNSAT_TOK; }
-"unknown"       { return UNKNOWN_TOK; }
-"assumption"    { return ASSUMPTION_TOK; }
-"formula"       { return FORMULA_TOK; }
-"status"        { return STATUS_TOK; }
-"benchmark"     { return BENCHMARK_TOK; }
-"extrasorts"    { return EXTRASORTS_TOK; }
-"extrafuns"     { return EXTRAFUNS_TOK; }
-"extrapreds"    { return EXTRAPREDS_TOK; }
-"language"      { return LANGUAGE_TOK; }
-"distinct"      { return DISTINCT_TOK; }
-":pattern"      { return PAT_TOK; } 
-":"             { return COLON_TOK; }
-"\["            { return LBRACKET_TOK; }
-"\]"            { return RBRACKET_TOK; }
-"{"             { return LCURBRACK_TOK;}
-"}"             { return RCURBRACK_TOK;}
-"("             { return LPAREN_TOK; }
-")"             { return RPAREN_TOK; }
-"$"             { return DOLLAR_TOK; }
-"?"             { return QUESTION_TOK; }
-
-
-"bit0"          { return BIT0_TOK; }
-"bit1"          { return BIT1_TOK; }
-
-"concat"        { return BVCONCAT_TOK; }
-"extract"       { return BVEXTRACT_TOK; }
-
-"bvnot"         { return BVNOT_TOK; }
-"bvand"         { return BVAND_TOK; }
-"bvor"          { return BVOR_TOK; }
-"bvneg"         { return BVNEG_TOK; }
-"bvnand"        { return BVNAND_TOK; }
-"bvnor"         { return BVNOR_TOK; }
-"bvxor"         { return BVXOR_TOK; }
-"bvxnor"        { return BVXNOR_TOK; }
-
-"="             { return EQ_TOK; }
-"bvcomp"        { return BVCOMP_TOK; }
-"bvult"         { return BVULT_TOK; }
-"bvule"         { return BVULE_TOK; }
-"bvugt"         { return BVUGT_TOK; }
-"bvuge"         { return BVUGE_TOK; }
-"bvslt"         { return BVSLT_TOK; }
-"bvsle"         { return BVSLE_TOK; }
-"bvsgt"         { return BVSGT_TOK; }
-"bvsge"         { return BVSGE_TOK; }
-
-"bvadd"         { return BVADD_TOK; }
-"bvsub"         { return BVSUB_TOK; }
-"bvmul"         { return BVMUL_TOK; }
-"bvudiv"        { return BVUDIV_TOK; }
-"bvurem"        { return BVUREM_TOK; }
-"bvsdiv"        { return BVSDIV_TOK; }
-"bvsrem"        { return BVSREM_TOK; }
-"bvsmod"        { return BVSMOD_TOK; }
-
-"bvshl"         { return BVSHL_TOK; }
-"bvlshr"        { return BVLSHR_TOK; }
-"bvashr"        { return BVASHR_TOK; }
-
-"repeat"        { return REPEAT_TOK; }
-"zero_extend"   { return ZEXT_TOK; }
-"sign_extend"   { return SEXT_TOK; }
-"rotate_left"   { return ROL_TOK; }
-"rotate_right"  { return ROR_TOK; }
-
-
-"bv"[0-9]+              { smtliblval.str = new std::string(smtlibtext); return BV_TOK; }
-"bvbin"[0-1]+	        { smtliblval.str = new std::string(smtlibtext); return BVBIN_TOK; }
-"bvhex"[0-9,A-F,a-f]+	{ smtliblval.str = new std::string(smtlibtext); return BVHEX_TOK; }
-
-
-({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }
-
-<<EOF>>         { return EOF_TOK; }
-
-. { smtliberror("Illegal input character."); }
-%%
-
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
deleted file mode 100644
index eb3b3890..00000000
--- a/lib/SMT/smtlib.y
+++ /dev/null
@@ -1,974 +0,0 @@
-%{
-/*****************************************************************************/
-/*!
- * \file smtlib.y
- * 
- * Author: Clark Barrett
- * 
- * Created: Apr 30 2005
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-/* 
-   This file contains the bison code for the parser that reads in CVC
-   commands in SMT-LIB language.
-*/
-
-#include "SMTParser.h"
-#include "klee/Expr.h"
-#include "klee/ExprBuilder.h"
-
-#include <sstream>
-
-using namespace klee;
-using namespace klee::expr;
-
-// Define shortcuts for various things
-#define PARSER SMTParser::parserTemp
-#define BUILDER SMTParser::parserTemp->builder
-#define DONE SMTParser::parserTemp->done
-#define ASSUMPTIONS SMTParser::parserTemp->assumptions
-#define QUERY SMTParser::parserTemp->satQuery
-
-#define ARRAYSENABLED (SMTParser::parserTemp->arraysEnabled)
-#define BVSIZE (SMTParser::parserTemp->bvSize)
-#define QUERYPARSED SMTParser::parserTemp->queryParsed
-
-// Suppress the bogus warning suppression in bison (it generates
-// compile error)
-#undef __GNUC_MINOR__
-
-/* stuff that lives in smtlib.lex */
-extern int smtliblex(void);
-
-int smtliberror(const char *s)
-{
-  return SMTParser::parserTemp->Error(s);
-}
-
-
-#define YYLTYPE_IS_TRIVIAL 1
-#define YYMAXDEPTH 10485760
-
-%}
-
-/*
-%union {
-  std::string *str;
-  std::vector<std::string> *strvec;
-  CVC3::Expr *node;
-  std::vector<CVC3::Expr> *vec;
-  std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann;
-};
-*/
-
-%union {
-  std::string *str;
-  klee::expr::ExprHandle node;
-  std::vector<klee::expr::ExprHandle> *vec;
-};
-
-
-%start cmd
-
-/* strings are for better error messages.  
-   "_TOK" is so macros don't conflict with kind names */
-/*
-%type <vec> bench_attributes sort_symbs fun_symb_decls pred_symb_decls
-%type <vec> an_formulas quant_vars an_terms fun_symb patterns
-%type <node> pattern 
-%type <node> benchmark bench_name bench_attribute
-%type <node> status fun_symb_decl fun_sig pred_symb_decl pred_sig
-%type <node> an_formula quant_var an_atom prop_atom
-%type <node> an_term basic_term sort_symb pred_symb
-%type <node> var fvar
-%type <str> logic_name quant_symb connective user_value attribute annotation
-%type <strvec> annotations
-%type <pat_ann> patterns_annotations
-*/
-
-%type <node> an_formula an_logical_formula an_atom prop_atom
-%type <vec> an_formulas
-%type <node> an_term basic_term constant
-%type <node> an_fun an_arithmetic_fun an_bitwise_fun
-%type <node> an_pred
-%type <str> logic_name status attribute user_value annotation annotations 
-%type <str> var fvar symb
-
-%token <str> NUMERAL_TOK
-%token <str> SYM_TOK
-%token <str> STRING_TOK
-%token <str> AR_SYMB
-%token <str> USER_VAL_TOK
-
-%token <str> BV_TOK
-%token <str> BVBIN_TOK
-%token <str> BVHEX_TOK
-
-%token BITVEC_TOK
-
-%token TRUE_TOK
-%token FALSE_TOK
-%token ITE_TOK
-%token NOT_TOK
-%token IMPLIES_TOK
-%token IF_THEN_ELSE_TOK
-%token AND_TOK
-%token OR_TOK
-%token XOR_TOK
-%token IFF_TOK
-%token EXISTS_TOK
-%token FORALL_TOK
-%token LET_TOK
-%token FLET_TOK
-%token NOTES_TOK
-%token CVC_COMMAND_TOK
-%token SORTS_TOK
-%token FUNS_TOK
-%token PREDS_TOK
-%token EXTENSIONS_TOK
-%token DEFINITION_TOK
-%token AXIOMS_TOK
-%token LOGIC_TOK
-%token COLON_TOK
-%token LBRACKET_TOK
-%token RBRACKET_TOK
-%token LCURBRACK_TOK
-%token RCURBRACK_TOK
-%token LPAREN_TOK
-%token RPAREN_TOK
-%token SAT_TOK
-%token UNSAT_TOK
-%token UNKNOWN_TOK
-%token ASSUMPTION_TOK
-%token FORMULA_TOK
-%token STATUS_TOK
-%token BENCHMARK_TOK
-%token EXTRASORTS_TOK
-%token EXTRAFUNS_TOK
-%token EXTRAPREDS_TOK
-%token LANGUAGE_TOK
-%token DOLLAR_TOK
-%token QUESTION_TOK
-%token DISTINCT_TOK
-%token SEMICOLON_TOK
-%token EOF_TOK
-%token PAT_TOK
-
-
-%token BIT0_TOK
-%token BIT1_TOK
-
-%token BVCONCAT_TOK
-%token BVEXTRACT_TOK
-
-%token BVNOT_TOK
-%token BVAND_TOK
-%token BVOR_TOK
-%token BVNEG_TOK
-%token BVNAND_TOK
-%token BVNOR_TOK
-%token BVXOR_TOK
-%token BVXNOR_TOK
-
-%token EQ_TOK
-%token BVCOMP_TOK
-%token BVULT_TOK
-%token BVULE_TOK
-%token BVUGT_TOK
-%token BVUGE_TOK
-%token BVSLT_TOK
-%token BVSLE_TOK
-%token BVSGT_TOK
-%token BVSGE_TOK
-
-%token BVADD_TOK
-%token BVSUB_TOK
-%token BVMUL_TOK
-%token BVUDIV_TOK
-%token BVUREM_TOK
-%token BVSDIV_TOK
-%token BVSREM_TOK
-%token BVSMOD_TOK
-%token BVSHL_TOK
-%token BVLSHR_TOK
-%token BVASHR_TOK
-
-%token REPEAT_TOK
-%token ZEXT_TOK
-%token SEXT_TOK
-%token ROL_TOK
-%token ROR_TOK
-
-%%
-
-cmd:
-    benchmark
-    {
-      YYACCEPT;
-    }
-;
-
-benchmark:
-    LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { }
-
-  | EOF_TOK
-    { 
-      DONE = true;
-    }
-;
-
-bench_name:
-    SYM_TOK { }
-;
-
-bench_attributes:
-    bench_attribute { }
-
-  | bench_attributes bench_attribute { }
-;
-
-bench_attribute:
-    COLON_TOK ASSUMPTION_TOK an_formula
-    {
-      ASSUMPTIONS.push_back($3);
-    }
-
-  | COLON_TOK FORMULA_TOK an_formula 
-    {
-      QUERYPARSED = true;
-      QUERY = $3;
-    }
-
-  | COLON_TOK STATUS_TOK status { }
-
-  | COLON_TOK LOGIC_TOK logic_name 
-    {
-      if (*$3 != "QF_BV" && *$3 != "QF_AUFBV" && *$3 != "QF_UFBV") {
-	llvm::errs() << "ERROR: Logic " << *$3 << " not supported.";
-	exit(1);
-      }
-
-      if (*$3 == "QF_AUFBV")
-        ARRAYSENABLED = true;
-    }
-/*
-  | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK
-    { 
-      // XXX?
-    }
-*/
-
-  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK LPAREN_TOK SYM_TOK BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK RPAREN_TOK RPAREN_TOK
-    {
-      PARSER->DeclareExpr(*$5, atoi($8->c_str()));
-    }
-/*
-  | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
-    {
-      //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
-      //delete $4;
-    }
-*/
-  | COLON_TOK NOTES_TOK STRING_TOK
-    {  }
-
-  | COLON_TOK CVC_COMMAND_TOK STRING_TOK
-    {  }
-
-  | annotation
-    {  }
-;
-
-
-logic_name  :
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      BVSIZE = atoi($3->c_str());
-      delete $3;
-      $$ = $1;
-    }
-  | SYM_TOK
-    {
-      $$ = $1;
-    }
-;
-
-status:
-    SAT_TOK { }
-  | UNSAT_TOK { }
-  | UNKNOWN_TOK { }
-;
-
-/*
-sort_symbs:
-    sort_symb 
-    {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  | sort_symbs sort_symb
-    { 
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-fun_symb_decls:
-    fun_symb_decl
-    {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  |
-    fun_symb_decls fun_symb_decl
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-fun_symb_decl:
-    LPAREN_TOK fun_sig annotations
-    {
-      $$ = $2;
-      delete $3;
-    }
-  | LPAREN_TOK fun_sig RPAREN_TOK
-    {
-      $$ = $2;
-    }
-;
-
-fun_sig:
-    fun_symb sort_symbs
-    {
-      if ($2->size() == 1) {
-        $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0]));
-      }
-      else {
-        CVC3::Expr tmp(VC->listExpr("_ARROW", *$2));
-        $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp));
-      }
-      delete $1;
-      delete $2;
-    }
-;
-
-pred_symb_decls:
-    pred_symb_decl
-    {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  |
-    pred_symb_decls pred_symb_decl
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-pred_symb_decl:
-    LPAREN_TOK pred_sig annotations
-    {
-      $$ = $2;
-      delete $3;
-    }
-  | LPAREN_TOK pred_sig RPAREN_TOK
-    {
-      $$ = $2;
-    }
-;
-
-pred_sig:
-    pred_symb sort_symbs
-    {
-      std::vector<CVC3::Expr> tmp(*$2);
-      tmp.push_back(VC->idExpr("_BOOLEAN"));
-      CVC3::Expr tmp2(VC->listExpr("_ARROW", tmp));
-      $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2));
-      delete $1;
-      delete $2;
-    }
-  | pred_symb
-    {
-      $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1),
-                                       VC->idExpr("_BOOLEAN")));
-      delete $1;
-    }
-;
-*/
-
-
-an_formulas:
-    an_formula
-    {
-      $$ = new std::vector<klee::expr::ExprHandle>;
-      $$->push_back($1);
-    }
-  |
-    an_formulas an_formula
-    {
-      $1->push_back($2);
-      $$ = $1;
-    }
-;
-
-
-an_logical_formula:
-
-    LPAREN_TOK NOT_TOK an_formula annotations
-    {
-      $$ = BUILDER->Not($3);
-    }
-
-  | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations
-    {
-      $$ = Expr::createImplies($3, $4);  // XXX: move to builder?
-    }
-
-  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula annotations
-    {
-      $$ = BUILDER->Select($3, $4, $5);
-    }
-
-  | LPAREN_TOK AND_TOK an_formulas annotations
-    {
-      $$ = PARSER->CreateAnd(*$3);
-    }
-
-  | LPAREN_TOK OR_TOK an_formulas annotations
-    {
-      $$ = PARSER->CreateOr(*$3);
-    }
-
-  | LPAREN_TOK XOR_TOK an_formulas annotations
-    {
-      $$ = PARSER->CreateXor(*$3);
-    }
-
-  | LPAREN_TOK IFF_TOK an_formula an_formula annotations
-    {
-      $$ = BUILDER->Eq($3, $4);
-    }
-;
-
-
-an_formula:
-    an_atom
-    {
-      $$ = $1;
-    }
-
-  | an_logical_formula
-    {
-      $$ = $1;
-    }
-
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK
-        { 
-	  PARSER->PushVarEnv();
-	  PARSER->AddVar(*$4, $5); 
-	} 
-    an_formula annotations
-    {
-      $$ = $8;
-      PARSER->PopVarEnv();
-    }
-
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK 
-        { 
-	  PARSER->PushFVarEnv();
-	  PARSER->AddFVar(*$4, $5); 
-	} 
-    an_formula annotations
-    {
-      $$ = $8;
-      PARSER->PopFVarEnv();
-    }
-;
-
-
-
-an_atom:
-    prop_atom 
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK prop_atom annotations 
-    {
-      $$ = $2;
-    }
-  
-  | an_pred
-    {
-      $$ = $1;
-    }
-
-/*
-  | LPAREN_TOK DISTINCT_TOK an_terms annotations
-    {
-      $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));
-
-//       std::vector<CVC3::Expr> tmp;
-//       tmp.push_back(*$2);
-//       tmp.insert(tmp.end(), $3->begin(), $3->end());
-//       $$ = new CVC3::Expr(VC->listExpr(tmp));
-//       for (unsigned i = 0; i < (*$3).size(); ++i) {
-//         tmp.push_back(($3)[i])
-// 	for (unsigned j = i+1; j < (*$3).size(); ++j) {
-// 	  tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j]));
-// 	}
-//       }
-//       $$ = new CVC3::Expr(VC->listExpr("_AND", tmp));
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK
-    {
-      $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));
-//       std::vector<CVC3::Expr> tmp;
-//       for (unsigned i = 0; i < (*$3).size(); ++i) {
-// 	for (unsigned j = i+1; j < (*$3).size(); ++j) {
-// 	  tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j]));
-// 	}
-//       }
-//       $$ = new CVC3::Expr(VC->listExpr("_AND", tmp));
-      delete $3;
-    }
-*/
-;
-
-prop_atom:
-    TRUE_TOK
-    {
-      $$ = BUILDER->Constant(1, 1);
-    }
-
-  | FALSE_TOK
-    { 
-      $$ = BUILDER->Constant(0, 1);;
-    }
-
-  | fvar
-    {
-      $$ = PARSER->GetFVar(*$1);
-    }
-;  
-
-
-an_pred:
-    LPAREN_TOK EQ_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Eq($3, $4);
-    }
-
-  | LPAREN_TOK BVULT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Ult($3, $4);
-    }
-
-  | LPAREN_TOK BVULE_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Ule($3, $4);
-    }
-
-  | LPAREN_TOK BVUGT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Ugt($3, $4);
-    }
-
-  | LPAREN_TOK BVUGE_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Uge($3, $4);
-    }
-
-  | LPAREN_TOK BVSLT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Slt($3, $4);
-    }
-
-  | LPAREN_TOK BVSLE_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Sle($3, $4);
-    }
-
-  | LPAREN_TOK BVSGT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Sgt($3, $4);
-    }
-
-  | LPAREN_TOK BVSGE_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Sge($3, $4);
-    }
-;
-
-
-an_arithmetic_fun:
-
-    LPAREN_TOK BVNEG_TOK an_term annotations
-    {
-      smtliberror("bvneg not supported yet");
-      $$ = NULL; // TODO
-    }
-
-  | LPAREN_TOK BVADD_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Add($3, $4);
-    }
-
-  | LPAREN_TOK BVSUB_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Sub($3, $4);
-    }
-
-  | LPAREN_TOK BVMUL_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Mul($3, $4);
-    }
-
-  | LPAREN_TOK BVUDIV_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->UDiv($3, $4);
-    }
-
-  | LPAREN_TOK BVUREM_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->URem($3, $4);
-    }
-
-  | LPAREN_TOK BVSDIV_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->SDiv($3, $4);
-    }
-
-  | LPAREN_TOK BVSREM_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->SRem($3, $4);
-    }
-
-  | LPAREN_TOK BVSMOD_TOK an_term an_term annotations
-    {
-      smtliberror("bvsmod not supported yet");
-      $$ = NULL; // TODO
-    }
-;
-
-
-an_bitwise_fun:
-    LPAREN_TOK BVNOT_TOK an_term annotations
-    {
-      $$ = BUILDER->Not($3);
-    }
-
-  | LPAREN_TOK BVAND_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->And($3, $4);
-    }
-
-  | LPAREN_TOK BVOR_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Or($3, $4);
-    }
-
-  | LPAREN_TOK BVXOR_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Xor($3, $4);
-    }
-
-  | LPAREN_TOK BVXNOR_TOK an_term an_term annotations
-    {      
-      smtliberror("bvxnor not supported yet");
-      $$ = NULL;  // TODO
-    }
-
-  | LPAREN_TOK BVSHL_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Shl($3, $4);
-    }
-
-  | LPAREN_TOK BVLSHR_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->LShr($3, $4);
-    }
-
-  | LPAREN_TOK BVASHR_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->AShr($3, $4);
-    }
-
-  | LPAREN_TOK ROL_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      smtliberror("rotate_left not supported yet");
-      $$ = NULL; // TODO
-    }
-
-  | LPAREN_TOK ROR_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      smtliberror("rotate_right not supported yet");
-      $$ = NULL; // TODO
-    }
- 
-  | LPAREN_TOK ZEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      $$ = BUILDER->ZExt($6, $6->getWidth() + PARSER->StringToInt(*$4));
-    }
-
-  | LPAREN_TOK SEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      $$ = BUILDER->SExt($6, $6->getWidth() + PARSER->StringToInt(*$4));
-    }
-
-  | LPAREN_TOK BVCONCAT_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Concat($3, $4);
-    }
-
-  | LPAREN_TOK REPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      smtliberror("repeat not supported yet");
-      $$ = NULL; // TODO
-    }
-
-  | LPAREN_TOK BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
-    {
-      int off = PARSER->StringToInt(*$6);
-      $$ = BUILDER->Extract($8, off, PARSER->StringToInt(*$4) - off + 1);
-    }
-;
-
-
-an_fun:
-    an_logical_formula
-    {
-      $$ = $1;
-    }
-
-  | an_pred
-    {
-      $$ = $1;
-    }
-
-  | LPAREN_TOK BVCOMP_TOK an_term an_term annotations
-    {
-      $$ = BUILDER->Eq($3, $4);
-    }
- 
-  | an_arithmetic_fun
-    {
-      $$ = $1;
-    }
-
-  | an_bitwise_fun
-    {
-      $$ = $1;
-    }
-
-/*
-      else if (ARRAYSENABLED && *$1 == "select") {
-        $$->push_back(VC->idExpr("_READ"));
-      }
-      else if (ARRAYSENABLED && *$1 == "store") {
-        $$->push_back(VC->idExpr("_WRITE"));
-      }
-*/
-;
-
-constant:
-    BIT0_TOK
-    {
-      $$ = PARSER->GetConstExpr("0", 2, 1);
-    }
-
-  | BIT1_TOK
-    {
-      $$ = PARSER->GetConstExpr("1", 2, 1);
-    }
-
-  | BVBIN_TOK
-    {
-      $$ = PARSER->GetConstExpr($1->substr(5), 2, $1->length()-5);
-    }
-  | BVHEX_TOK
-    {
-      $$ = PARSER->GetConstExpr($1->substr(5), 16, ($1->length()-5)*4);
-    }
-  | BV_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = PARSER->GetConstExpr($1->substr(2), 10, PARSER->StringToInt(*$3));
-    }
-;
-
-
-an_term:
-    basic_term 
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK basic_term annotations 
-    {
-      $$ = $2;
-      delete $3;
-    }
-
-  | an_fun
-    {
-      $$ = $1;
-    }
-
-  | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations
-    {
-      $$ = BUILDER->Select($3, $4, $5);
-    }
-;
-
-
-basic_term:
-    constant 
-    {
-      $$ = $1;
-    }
-
-  | var
-    {
-      $$ = PARSER->GetVar(*$1);
-    }
-  | symb
-    {
-      $$ = PARSER->GetVar(*$1);
-    }
-;
-
-
-
-annotations:
-    RPAREN_TOK { }
-  | annotation annotations { }
-;
-
-annotation:
-    attribute { }
-
-  | attribute user_value {  }
-;
-
-user_value:
-    USER_VAL_TOK  
-    {
-      delete $1;
-    }
-;
-
-/*
-sort_symb:
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      if (BVENABLED && *$1 == "BitVec") {
-        $$ = new CVC3::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)));
-      }
-      else {
-        $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3)));
-      }
-      delete $1;
-      delete $3;
-    }
-  | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      if (BVENABLED && ARRAYSENABLED && *$1 == "Array") {
-        $$ = new CVC3::Expr(VC->listExpr("_ARRAY",
-                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)),
-                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$5))));
-      }
-      else {
-        $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5)));
-      }
-      delete $1;
-      delete $3;
-      delete $5;
-    }
-  | SYM_TOK 
-    { 
-      if (*$1 == "Real") {
-	$$ = new CVC3::Expr(VC->idExpr("_REAL"));
-      } else if (*$1 == "Int") {
-	$$ = new CVC3::Expr(VC->idExpr("_INT"));
-      } else {
-	$$ = new CVC3::Expr(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-;
-
-*/
-
-/*
-fun_symb:
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      else if (BVENABLED &&
-               $1->size() > 2 &&
-               (*$1)[0] == 'b' &&
-               (*$1)[1] == 'v') {
-        int i = 2;
-        while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
-        if ((*$1)[i] == '\0') {
-          $$->push_back(VC->idExpr("_BVCONST"));
-          $$->push_back(VC->ratExpr($1->substr(2), 10));
-        }
-        else $$->push_back(VC->idExpr(*$1));
-      }
-      else $$->push_back(VC->idExpr(*$1));
-      $$->push_back(VC->ratExpr(*$3));
-      delete $1;
-      delete $3;
-    }
-;
-*/
-
-attribute:
-    COLON_TOK SYM_TOK
-    {
-      $$ = $2;
-    }
-;
-
-
-var:
-    QUESTION_TOK SYM_TOK
-    {
-      $$ = $2;
-    }
-;
-
-
-fvar:
-    DOLLAR_TOK SYM_TOK
-    {
-      $$ = $2;
-    }
-;
-
-symb:
-    SYM_TOK
-    {
-      $$ = $1;
-    }
-
-%%
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index e1d41eba..5893c28e 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -17,6 +17,7 @@
 #include "klee/util/ExprUtil.h"
 
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/Errno.h"
 #include "llvm/Support/ErrorHandling.h"
 
 #include <errno.h>
@@ -231,7 +232,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
   fflush(stderr);
   int pid = fork();
   if (pid == -1) {
-    klee_warning("fork failed (for STP)");
+    klee_warning("fork failed (for STP) - %s", llvm::sys::StrError(errno).c_str());
     if (!IgnoreSolverFailures)
       exit(1);
     return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED;
diff --git a/lib/Support/MemoryUsage.cpp b/lib/Support/MemoryUsage.cpp
index d141593a..f1757ad3 100644
--- a/lib/Support/MemoryUsage.cpp
+++ b/lib/Support/MemoryUsage.cpp
@@ -22,9 +22,74 @@
 #include <malloc/malloc.h>
 #endif
 
+// ASan Support
+//
+// When building with ASan the `mallinfo()` function is intercepted and always
+// reports zero so we can't use that to report KLEE's memory usage. Instead we
+// will use ASan's public interface to query how much memory has been
+// allocated.
+//
+// Unfortunately the interface is dependent on the compiler version. It is also
+// unfortunate that the way to detect compilation with ASan differs between
+// compilers. The preprocessor code below tries to determine if ASan is enabled
+// and if so which interface should be used.
+//
+// If ASan is enabled the `KLEE_ASAN_BUILD` macro will be defined other it will
+// be undefined. If `KLEE_ASAN_BUILD` is defined then the
+// `ASAN_GET_ALLOCATED_MEM_FUNCTION` macro will defined to the name of the ASan
+// function that can be called to get memory allocation
+
+// Make sure we start with the macro being undefined.
+#undef KLEE_ASAN_BUILD
+
+// Clang and ASan
+#if defined(__has_feature)
+#  if __has_feature(address_sanitizer)
+#     if __has_include("sanitizer/allocator_interface.h")
+#       include <sanitizer/allocator_interface.h>
+        // Modern interface
+#       define ASAN_GET_ALLOCATED_MEM_FUNCTION __sanitizer_get_current_allocated_bytes
+#     else
+#       include <sanitizer/asan_interface.h>
+        // Deprecated interface.
+#       define ASAN_GET_ALLOCATED_MEM_FUNCTION __asan_get_current_allocated_bytes
+#     endif /* has_include("sanitizer/allocator_interface.h") */
+#    define KLEE_ASAN_BUILD
+#  endif /* __has_feature(address_sanitizer) */
+#endif /* defined(__has_feature) */
+
+// For GCC and ASan
+#ifndef KLEE_ASAN_BUILD
+#  if defined(__SANITIZE_ADDRESS__)
+     // HACK: GCC doesn't ship `allocator_interface.h`  or `asan_interface.h` so
+     // just provide the proto-types here.
+     extern "C" {
+       size_t __sanitizer_get_current_allocated_bytes();
+       size_t __asan_get_current_allocated_bytes(); // Deprecated.
+     }
+     // HACK: Guess which function to use based on GCC version
+#    if __GNUC__ > 4
+       // Tested with gcc 5.2, 5.4, and 6.2.1
+       // Modern interface
+#      define ASAN_GET_ALLOCATED_MEM_FUNCTION __sanitizer_get_current_allocated_bytes
+#    else
+       // Tested with gcc 4.8 and 4.9
+       // Deprecated interface
+#      define ASAN_GET_ALLOCATED_MEM_FUNCTION __asan_get_current_allocated_bytes
+#    endif
+#    define KLEE_ASAN_BUILD
+#  endif /* defined(__SANITIZE_ADDRESS__) */
+#endif /* ndef KLEE_ASAN_BUILD */
+
 using namespace klee;
 
 size_t util::GetTotalMallocUsage() {
+#ifdef KLEE_ASAN_BUILD
+  // When building with ASan on Linux `mallinfo()` just returns 0 so use ASan runtime
+  // function instead to get used memory.
+  return ASAN_GET_ALLOCATED_MEM_FUNCTION();
+#endif
+
 #ifdef HAVE_GPERFTOOLS_MALLOC_EXTENSION_H
   size_t value = 0;
   MallocExtension::instance()->GetNumericProperty(
diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt
index 68eb9016..1e680e5d 100644
--- a/runtime/CMakeLists.txt
+++ b/runtime/CMakeLists.txt
@@ -82,19 +82,11 @@ if (NOT ENV_BINARY)
   message(FATAL_ERROR "Failed to find env binary")
 endif()
 
-# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject
-# that shipped with CMake >= 3.1. Should we just avoid using this option? We don't really
-# need it unless we are patching gsl itself and need to rebuild.
-if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1"))
-  option(KLEE_RUNTIME_ALWAYS_REBUILD "Always try to rebuild KLEE runtime" ON)
-  if (KLEE_RUNTIME_ALWAYS_REBUILD)
-    set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1)
-  else()
-    set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 0)
-  endif()
+option(KLEE_RUNTIME_ALWAYS_REBUILD "Always try to rebuild KLEE runtime" ON)
+if (KLEE_RUNTIME_ALWAYS_REBUILD)
+  set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG 1)
 else()
-  set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "")
-  message(WARNING "KLEE's runtime will not be automatically rebuilt.")
+  set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG 0)
 endif()
 
 # Build the runtime as an external project.
@@ -106,11 +98,19 @@ ExternalProject_Add(BuildKLEERuntimes
   SOURCE_DIR "${CMAKE_CURRENT_BINARY_DIR}"
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}"
   CONFIGURE_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+  BUILD_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+)
+
+# Use `ExternalProject_Add_Step` with `ALWAYS` argument instead of directly
+# building in `ExternalProject_Add` with `BUILD_ALWAYS` argument due to lack of
+# support for the `BUILD_ALWAYS` argument in CMake < 3.1.
+ExternalProject_Add_Step(BuildKLEERuntimes RuntimeBuild
   # `env` is used here to make sure `MAKEFLAGS` of KLEE's build
   # is not propagated into the bitcode build system.
-  BUILD_COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode all
-  ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
-  INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
+  COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode all
+  ALWAYS ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
+  WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
 )
 
 # FIXME: Invoke `make clean` in the bitcode build system
diff --git a/runtime/Runtest/Makefile b/runtime/Runtest/Makefile
index 82e21345..1de3281b 100644
--- a/runtime/Runtest/Makefile
+++ b/runtime/Runtest/Makefile
@@ -56,8 +56,14 @@ ifeq ($(HOST_OS), $(filter $(HOST_OS), DragonFly Linux FreeBSD GNU/kFreeBSD GNU)
 endif
 
 ifeq ($(HOST_OS), $(filter $(HOST_OS), Linux GNU GNU/kFreeBSD))
+  ifeq (-fsanitize=address,$(filter -fsanitize=address,$(CXXFLAGS)))
+    # When building with ASan the library will have undefined symbols into
+    # ASan's runtime. We want to allow this and not fail the build.
+    $(warning Allowing undefined symbols in $(LIBRARYNAME) due to ASan build)
+  else
     # Don't allow unresolved symbols.
     LLVMLibsOptions += -Wl,--no-undefined
+  endif
 endif
 
 ifeq ($(HOST_OS), Linux)
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 9f565444..a2a46e2a 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -13,8 +13,8 @@ set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}")
 # is shared by both build systems.
 set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include")
 set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include")
-set(NATIVE_CC "${CMAKE_C_COMPILER} -I ${CMAKE_SOURCE_DIR}/include")
-set(NATIVE_CXX "${CMAKE_CXX_COMPILER} -I ${CMAKE_SOURCE_DIR}/include")
+set(NATIVE_CC "${CMAKE_C_COMPILER} ${CMAKE_C_FLAGS} -I ${CMAKE_SOURCE_DIR}/include")
+set(NATIVE_CXX "${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} -I ${CMAKE_SOURCE_DIR}/include")
 set(TARGET_TRIPLE "${TARGET_TRIPLE}")
 if (ENABLE_KLEE_UCLIBC)
   set(ENABLE_UCLIBC 1)
diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c
index 398ba6f8..82fbe4f1 100644
--- a/test/Feature/Vararg.c
+++ b/test/Feature/Vararg.c
@@ -12,7 +12,7 @@ struct triple {
   int first, second, third;
 };
 
-int test1(int x, ...) {
+void test1(int x, ...) {
   va_list ap;
   va_start(ap, x);
   int i32 = va_arg(ap, int);
diff --git a/test/Makefile b/test/Makefile
index c96ae889..a2d95056 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -74,7 +74,7 @@ lit.site.cfg: lit.site.cfg.in
 	     -e "s#@HAVE_SELINUX@#$(HAVE_SELINUX)#g" \
 	     -e "s#@ENABLE_STP@#$(ENABLE_STP)#g" \
 	     -e "s#@ENABLE_Z3@#$(ENABLE_Z3)#g" \
-	     -e "s#@NATIVE_CC@#$(CC) -I$(PROJ_SRC_ROOT)/include#g" \
-	     -e "s#@NATIVE_CXX@#$(CXX) -I$(PROJ_SRC_ROOT)/include#g" \
+	     -e "s#@NATIVE_CC@#$(CC) $(CFLAGS) -I$(PROJ_SRC_ROOT)/include#g" \
+	     -e "s#@NATIVE_CXX@#$(CXX) $(CXXFLAGS) -I$(PROJ_SRC_ROOT)/include#g" \
 	     -e "s#@LIB_KLEE_RUN_TEST_PATH@#$(SharedLibDir)/$(SharedPrefix)kleeRuntest$(SHLIBEXT)#g" \
 	     $(PROJ_SRC_DIR)/lit.site.cfg.in > $@
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-04-06 22:54:47 +0000