about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/ExecutionState.cpp33
-rw-r--r--lib/Core/Executor.cpp4
-rw-r--r--lib/Core/Memory.cpp4
-rw-r--r--lib/Core/TimingSolver.cpp23
-rw-r--r--lib/Expr/Constraints.cpp31
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp73
-rw-r--r--lib/Module/RaiseAsm.cpp10
-rw-r--r--lib/Solver/STPBuilder.cpp26
-rw-r--r--lib/Support/Time.cpp10
-rw-r--r--lib/Support/Timer.cpp10
10 files changed, 148 insertions, 76 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 5d32c936..6aeaa833 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -66,13 +66,14 @@ StackFrame::~StackFrame() {
 
 /***/
 
-ExecutionState::ExecutionState(KFunction *kf) 
-  : fakeState(false),
-    depth(0),
+ExecutionState::ExecutionState(KFunction *kf) :
     pc(kf->instructions),
     prevPC(pc),
+
     queryCost(0.), 
     weight(1),
+    depth(0),
+
     instsSinceCovNew(0),
     coveredNew(false),
     forkDisabled(false),
@@ -80,12 +81,8 @@ ExecutionState::ExecutionState(KFunction *kf)
   pushFrame(0, kf);
 }
 
-ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) 
-  : fakeState(true),
-    constraints(assumptions),
-    queryCost(0.),
-    ptreeNode(0) {
-}
+ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
+    : constraints(assumptions), queryCost(0.), ptreeNode(0) {}
 
 ExecutionState::~ExecutionState() {
   for (unsigned int i=0; i<symbolics.size(); i++)
@@ -100,28 +97,30 @@ ExecutionState::~ExecutionState() {
   while (!stack.empty()) popFrame();
 }
 
-ExecutionState::ExecutionState(const ExecutionState& state)
-  : fnAliases(state.fnAliases),
-    fakeState(state.fakeState),
-    depth(state.depth),
+ExecutionState::ExecutionState(const ExecutionState& state):
+    fnAliases(state.fnAliases),
     pc(state.pc),
     prevPC(state.prevPC),
     stack(state.stack),
+    incomingBBIndex(state.incomingBBIndex),
+
+    addressSpace(state.addressSpace),
     constraints(state.constraints),
+
     queryCost(state.queryCost),
     weight(state.weight),
-    addressSpace(state.addressSpace),
+    depth(state.depth),
+
     pathOS(state.pathOS),
     symPathOS(state.symPathOS),
+
     instsSinceCovNew(state.instsSinceCovNew),
     coveredNew(state.coveredNew),
     forkDisabled(state.forkDisabled),
     coveredLines(state.coveredLines),
     ptreeNode(state.ptreeNode),
     symbolics(state.symbolics),
-    arrayNames(state.arrayNames),
-    shadowObjects(state.shadowObjects),
-    incomingBBIndex(state.incomingBBIndex)
+    arrayNames(state.arrayNames)
 {
   for (unsigned int i=0; i<symbolics.size(); i++)
     symbolics[i].first->refCount++;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index c78c9f8a..45876659 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2592,9 +2592,7 @@ void Executor::run(ExecutionState &initialState) {
             unsigned numStates = states.size();
             unsigned toKill = std::max(1U, numStates - numStates*MaxMemory/mbs);
 
-            if (MaxMemoryInhibit)
-              klee_warning("killing %d states (over memory cap)",
-                           toKill);
+            klee_warning("killing %d states (over memory cap)", toKill);
 
             std::vector<ExecutionState*> arr(states.begin(), states.end());
             for (unsigned i=0,N=arr.size(); N && i<toKill; ++i,--N) {
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 1dd1e1fd..07c292a0 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -468,7 +468,7 @@ ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
 
   // Otherwise, follow the slow general case.
   unsigned NumBytes = width / 8;
-  assert(width == NumBytes * 8 && "Invalid write size!");
+  assert(width == NumBytes * 8 && "Invalid read size!");
   ref<Expr> Res(0);
   for (unsigned i = 0; i != NumBytes; ++i) {
     unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
@@ -488,7 +488,7 @@ ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
 
   // Otherwise, follow the slow general case.
   unsigned NumBytes = width / 8;
-  assert(width == NumBytes * 8 && "Invalid write size!");
+  assert(width == NumBytes * 8 && "Invalid width for read size!");
   ref<Expr> Res(0);
   for (unsigned i = 0; i != NumBytes; ++i) {
     unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 037b23f3..b70bcbef 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -13,10 +13,11 @@
 #include "klee/ExecutionState.h"
 #include "klee/Solver.h"
 #include "klee/Statistics.h"
+#include "klee/Internal/System/Time.h"
 
 #include "CoreStats.h"
 
-#include "llvm/Support/Process.h"
+#include "llvm/Support/TimeValue.h"
 
 using namespace klee;
 using namespace llvm;
@@ -31,15 +32,14 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
+  sys::TimeValue now = util::getWallTimeVal();
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->evaluate(Query(state.constraints, expr), result);
 
-  sys::Process::GetTimeUsage(delta,user,sys);
+  sys::TimeValue delta = util::getWallTimeVal();
   delta -= now;
   stats::solverTime += delta.usec();
   state.queryCost += delta.usec()/1000000.;
@@ -55,15 +55,14 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
+  sys::TimeValue now = util::getWallTimeVal();
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
 
-  sys::Process::GetTimeUsage(delta,user,sys);
+  sys::TimeValue delta = util::getWallTimeVal();
   delta -= now;
   stats::solverTime += delta.usec();
   state.queryCost += delta.usec()/1000000.;
@@ -102,15 +101,14 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
   
-  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
+  sys::TimeValue now = util::getWallTimeVal();
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->getValue(Query(state.constraints, expr), result);
 
-  sys::Process::GetTimeUsage(delta,user,sys);
+  sys::TimeValue delta = util::getWallTimeVal();
   delta -= now;
   stats::solverTime += delta.usec();
   state.queryCost += delta.usec()/1000000.;
@@ -127,14 +125,13 @@ TimingSolver::getInitialValues(const ExecutionState& state,
   if (objects.empty())
     return true;
 
-  sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
+  sys::TimeValue now = util::getWallTimeVal();
 
   bool success = solver->getInitialValues(Query(state.constraints,
                                                 ConstantExpr::alloc(0, Expr::Bool)), 
                                           objects, result);
   
-  sys::Process::GetTimeUsage(delta,user,sys);
+  sys::TimeValue delta = util::getWallTimeVal();
   delta -= now;
   stats::solverTime += delta.usec();
   state.queryCost += delta.usec()/1000000.;
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index ae4563f4..dbdfd999 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -23,6 +23,14 @@
 
 using namespace klee;
 
+namespace {
+  llvm::cl::opt<bool>
+  RewriteEqualities("rewrite-equalities",
+		    llvm::cl::init(true),
+		    llvm::cl::desc("Rewrite existing constraints when an equality with a constant is added (default=on)"));
+}
+
+
 class ExprReplaceVisitor : public ExprVisitor {
 private:
   ref<Expr> src, dst;
@@ -118,13 +126,7 @@ ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
 }
 
 void ConstraintManager::addConstraintInternal(ref<Expr> e) {
-  // rewrite any known equalities 
-
-  // XXX should profile the effects of this and the overhead.
-  // traversing the constraints looking for equalities is hardly the
-  // slowest thing we do, but it is probably nicer to have a
-  // ConstraintSet ADT which efficiently remembers obvious patterns
-  // (byte-constant comparison).
+  // rewrite any known equalities and split Ands into different conjuncts
 
   switch (e->getKind()) {
   case Expr::Constant:
@@ -141,10 +143,17 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
   }
 
   case Expr::Eq: {
-    BinaryExpr *be = cast<BinaryExpr>(e);
-    if (isa<ConstantExpr>(be->left)) {
-      ExprReplaceVisitor visitor(be->right, be->left);
-      rewriteConstraints(visitor);
+    if (RewriteEqualities) {
+      // XXX: should profile the effects of this and the overhead.
+      // traversing the constraints looking for equalities is hardly the
+      // slowest thing we do, but it is probably nicer to have a
+      // ConstraintSet ADT which efficiently remembers obvious patterns
+      // (byte-constant comparison).
+      BinaryExpr *be = cast<BinaryExpr>(e);
+      if (isa<ConstantExpr>(be->left)) {
+	ExprReplaceVisitor visitor(be->right, be->left);
+	rewriteConstraints(visitor);
+      }
     }
     constraints.push_back(e);
     break;
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index c780ae90..e8e9a253 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -255,7 +255,10 @@ void ExprSMTLIBPrinter::printFullExpression(
      * type T.
      */
     printLogicalOrBitVectorExpr(e, expectedSort);
+    return;
 
+  case Expr::AShr:
+    printAShrExpr(cast<AShrExpr>(e));
     return;
 
   default:
@@ -334,6 +337,73 @@ void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr> &e) {
   *p << ")";
 }
 
+void ExprSMTLIBPrinter::printAShrExpr(const ref<AShrExpr> &e) {
+  // There is a difference between AShr and SMT-LIBv2's
+  // bvashr function when the shift amount is >= the bit width
+  // so we need to treat it specially here.
+  //
+  // Technically this is undefined behaviour for LLVM's ashr operator
+  // but currently llvm::APInt:ashr(...) will emit 0 if the shift amount
+  // is >= the bit width but this does not match how SMT-LIBv2's bvashr
+  // behaves as demonstrates by the following query
+  //
+  // (declare-fun x () (_ BitVec 32))
+  // (declare-fun y () (_ BitVec 32))
+  // (declare-fun result () (_ BitVec 32))
+  // (assert (bvuge y (_ bv32 32)))
+  // (assert (= result (bvashr x y)))
+  // (assert (distinct (_ bv0 32) result))
+  // (check-sat)
+  // sat
+  //
+  // Our solution is to instead emit
+  //
+  // (ite (bvuge shift_amount bit_width)
+  //      (_ bv0 bitwidth)
+  //      (bvashr value_to_shift shift_amount)
+  // )
+  //
+
+  Expr::Width bitWidth = e->getKid(0)->getWidth();
+  assert(bitWidth > 0 && "Invalid bit width");
+  ref<Expr> bitWidthExpr = ConstantExpr::create(bitWidth, bitWidth);
+  ref<Expr> zeroExpr = ConstantExpr::create(0, bitWidth);
+
+  // FIXME: we print e->getKid(1) twice and it might not get
+  // abbreviated
+  *p << "(ite";
+  p->pushIndent();
+  printSeperator();
+
+  *p << "(bvuge";
+  p->pushIndent();
+  printSeperator();
+  printExpression(e->getKid(1), SORT_BITVECTOR);
+  printSeperator();
+  printExpression(bitWidthExpr, SORT_BITVECTOR);
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+
+  printSeperator();
+  printExpression(zeroExpr, SORT_BITVECTOR);
+  printSeperator();
+
+  *p << "(bvashr";
+  p->pushIndent();
+  printSeperator();
+  printExpression(e->getKid(0), SORT_BITVECTOR);
+  printSeperator();
+  printExpression(e->getKid(1), SORT_BITVECTOR);
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+}
+
 const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) {
 
   switch (e->getKind()) {
@@ -373,8 +443,7 @@ const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) {
     return "bvshl";
   case Expr::LShr:
     return "bvlshr";
-  case Expr::AShr:
-    return "bvashr";
+  // AShr is not supported here. See printAShrExpr()
 
   case Expr::Eq:
     return "=";
diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp
index d9145a1e..12e5479b 100644
--- a/lib/Module/RaiseAsm.cpp
+++ b/lib/Module/RaiseAsm.cpp
@@ -66,17 +66,18 @@ bool RaiseAsmPass::runOnModule(Module &M) {
   std::string HostTriple = llvm::sys::getHostTriple();
 #endif
   const Target *NativeTarget = TargetRegistry::lookupTarget(HostTriple, Err);
+  TargetMachine * TM = 0;
   if (NativeTarget == 0) {
     llvm::errs() << "Warning: unable to select native target: " << Err << "\n";
     TLI = 0;
   } else {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "", "",
+    TM = NativeTarget->createTargetMachine(HostTriple, "", "",
                                                           TargetOptions());
 #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "", "");
+    TM = NativeTarget->createTargetMachine(HostTriple, "", "");
 #else
-    TargetMachine *TM = NativeTarget->createTargetMachine(HostTriple, "");
+    TM = NativeTarget->createTargetMachine(HostTriple, "");
 #endif
     TLI = TM->getTargetLowering();
   }
@@ -91,5 +92,8 @@ bool RaiseAsmPass::runOnModule(Module &M) {
     }
   }
 
+  if (TM)
+    delete TM;
+
   return changed;
 }
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 6d7dd8b7..a5e4c5ad 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -51,11 +51,6 @@ namespace {
 
 
 STPArrayExprHash::~STPArrayExprHash() {
-  
-  // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run;
-  // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled.
-  
-   /*
   for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) {
     ::VCExpr array_expr = it->second;
     if (array_expr) {
@@ -63,16 +58,16 @@ STPArrayExprHash::~STPArrayExprHash() {
       array_expr = 0;
     }
   }
-  
-  
-  for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) {
+
+
+  for (UpdateNodeHashConstIter it = _update_node_hash.begin();
+      it != _update_node_hash.end(); ++it) {
     ::VCExpr un_expr = it->second;
     if (un_expr) {
       ::vc_DeleteExpr(un_expr);
       un_expr = 0;
     }
   }
-  */
 }
 
 /***/
@@ -218,10 +213,9 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
-  res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
-                   res,
-                   bvZero(width));
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
+
+  res = vc_iteExpr(vc, ex, res, bvZero(width));
   return res;
 }
 
@@ -239,8 +233,9 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   ex,
                    res,
                    bvZero(width));
   return res;
@@ -269,8 +264,9 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) {
   }
 
   // If overshifting, shift to zero
+  ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width));
   res = vc_iteExpr(vc,
-                   vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)),
+                   ex,
                    res,
                    bvZero(width));
   return res;
diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp
index 909e07da..be5eaf18 100644
--- a/lib/Support/Time.cpp
+++ b/lib/Support/Time.cpp
@@ -10,6 +10,7 @@
 #include "klee/Config/Version.h"
 #include "klee/Internal/System/Time.h"
 
+#include "llvm/Support/TimeValue.h"
 #include "llvm/Support/Process.h"
 
 using namespace llvm;
@@ -22,7 +23,10 @@ double util::getUserTime() {
 }
 
 double util::getWallTime() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  return (now.seconds() + (double) now.nanoseconds() * 1e-9);
+  sys::TimeValue now = getWallTimeVal();
+  return (now.seconds() + ((double) now.nanoseconds() * 1e-9));
+}
+
+sys::TimeValue util::getWallTimeVal() {
+  return sys::TimeValue::now();
 }
diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp
index c61a90a3..da969810 100644
--- a/lib/Support/Timer.cpp
+++ b/lib/Support/Timer.cpp
@@ -10,19 +10,15 @@
 #include "klee/Config/Version.h"
 #include "klee/Internal/Support/Timer.h"
 
-#include "llvm/Support/Process.h"
+#include "klee/Internal/System/Time.h"
 
 using namespace klee;
 using namespace llvm;
 
 WallTimer::WallTimer() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  startMicroseconds = now.usec();
+  startMicroseconds = util::getWallTimeVal().usec();
 }
 
 uint64_t WallTimer::check() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  return now.usec() - startMicroseconds;
+  return util::getWallTimeVal().usec() - startMicroseconds;
 }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-05-29 06:17:50 +0000