about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/ExecutionState.cpp33
-rw-r--r--lib/Core/Executor.cpp49
-rw-r--r--lib/Core/ExternalDispatcher.cpp7
-rw-r--r--lib/Core/Memory.cpp4
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp27
-rw-r--r--lib/Core/SpecialFunctionHandler.h1
-rw-r--r--lib/Core/StatsTracker.cpp7
-rw-r--r--lib/Core/TimingSolver.cpp23
8 files changed, 80 insertions, 71 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..49e526f5 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -140,10 +140,6 @@ namespace {
 		   cl::desc("Dump test cases for all active states on exit (default=on)"));
  
   cl::opt<bool>
-  NoPreferCex("no-prefer-cex",
-              cl::init(false));
- 
-  cl::opt<bool>
   RandomizeFork("randomize-fork",
                 cl::init(false),
 		cl::desc("Randomly swap the true and false states on a fork (default=off)"));
@@ -2592,9 +2588,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) {
@@ -3484,20 +3478,33 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   solver->setTimeout(coreSolverTimeout);
 
   ExecutionState tmp(state);
-  if (!NoPreferCex) {
-    for (unsigned i = 0; i != state.symbolics.size(); ++i) {
-      const MemoryObject *mo = state.symbolics[i].first;
-      std::vector< ref<Expr> >::const_iterator pi = 
-        mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
-      for (; pi != pie; ++pi) {
-        bool mustBeTrue;
-        bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), 
-                                          mustBeTrue);
-        if (!success) break;
-        if (!mustBeTrue) tmp.addConstraint(*pi);
-      }
-      if (pi!=pie) break;
-    }
+
+  // Go through each byte in every test case and attempt to restrict
+  // it to the constraints contained in cexPreferences.  (Note:
+  // usually this means trying to make it an ASCII character (0-127)
+  // and therefore human readable. It is also possible to customize
+  // the preferred constraints.  See test/Features/PreferCex.c for
+  // an example) While this process can be very expensive, it can
+  // also make understanding individual test cases much easier.
+  for (unsigned i = 0; i != state.symbolics.size(); ++i) {
+    const MemoryObject *mo = state.symbolics[i].first;
+    std::vector< ref<Expr> >::const_iterator pi = 
+      mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
+    for (; pi != pie; ++pi) {
+      bool mustBeTrue;
+      // Attempt to bound byte to constraints held in cexPreferences
+      bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), 
+					mustBeTrue);
+      // If it isn't possible to constrain this particular byte in the desired
+      // way (normally this would mean that the byte can't be constrained to
+      // be between 0 and 127 without making the entire constraint list UNSAT)
+      // then just continue on to the next byte.
+      if (!success) break;
+      // If the particular constraint operated on in this iteration through
+      // the loop isn't implied then add it to the list of constraints.
+      if (!mustBeTrue) tmp.addConstraint(*pi);
+    }
+    if (pi!=pie) break;
   }
 
   std::vector< std::vector<unsigned char> > values;
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 5f9f8dc6..ecc9912e 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -10,13 +10,6 @@
 #include "ExternalDispatcher.h"
 #include "klee/Config/Version.h"
 
-// Ugh.
-#undef PACKAGE_BUGREPORT
-#undef PACKAGE_NAME
-#undef PACKAGE_STRING
-#undef PACKAGE_TARNAME
-#undef PACKAGE_VERSION
-
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/IR/Module.h"
 #include "llvm/IR/Constants.h"
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/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index f06ae4f5..52abff5f 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -22,6 +22,8 @@
 #include "Executor.h"
 #include "MemoryManager.h"
 
+#include "klee/CommandLine.h"
+
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/IR/Module.h"
 #else
@@ -34,6 +36,15 @@
 using namespace llvm;
 using namespace klee;
 
+namespace {
+  cl::opt<bool>
+  ReadablePosix("readable-posix-inputs",
+            cl::init(false),
+            cl::desc("Prefer creation of POSIX inputs (command-line arguments, files, etc.) with human readable bytes. "
+                     "Note: option is expensive when creating lots of tests (default=false)"));
+}
+
+
 /// \todo Almost all of the demands in this file should be replaced
 /// with terminateState calls.
 
@@ -81,6 +92,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("klee_mark_global", handleMarkGlobal, false),
   add("klee_merge", handleMerge, false),
   add("klee_prefer_cex", handlePreferCex, false),
+  add("klee_posix_prefer_cex", handlePosixPreferCex, false),
   add("klee_print_expr", handlePrintExpr, false),
   add("klee_print_range", handlePrintRange, false),
   add("klee_set_forking", handleSetForking, false),
@@ -222,7 +234,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
   ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr);
   if (!state.addressSpace.resolveOne(address, op))
     assert(0 && "XXX out of bounds / multiple resolution unhandled");
-  bool res;
+  bool res __attribute__ ((unused));
   assert(executor.solver->mustBeTrue(state, 
                                      EqExpr::create(address, 
                                                     op.first->getBaseExpr()),
@@ -376,7 +388,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state,
     e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth()));
   
   bool res;
-  bool success = executor.solver->mustBeFalse(state, e, res);
+  bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res);
   assert(success && "FIXME: Unhandled solver failure");
   if (res) {
     executor.terminateStateOnError(state, 
@@ -416,6 +428,13 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
   rl[0].first.first->cexPreferences.push_back(cond);
 }
 
+void SpecialFunctionHandler::handlePosixPreferCex(ExecutionState &state,
+                                             KInstruction *target,
+                                             std::vector<ref<Expr> > &arguments) {
+  if (ReadablePosix)
+    return handlePreferCex(state, target, arguments);
+}
+
 void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
                                   KInstruction *target,
                                   std::vector<ref<Expr> > &arguments) {
@@ -480,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
   if (!isa<ConstantExpr>(arguments[1])) {
     // FIXME: Pull into a unique value method?
     ref<ConstantExpr> value;
-    bool success = executor.solver->getValue(state, arguments[1], value);
+    bool success __attribute__ ((unused)) = executor.solver->getValue(state, arguments[1], value);
     assert(success && "FIXME: Unhandled solver failure");
     bool res;
     success = executor.solver->mustBeTrue(state, 
@@ -679,7 +698,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
 
     // FIXME: Type coercion should be done consistently somewhere.
     bool res;
-    bool success =
+    bool success __attribute__ ((unused)) =
       executor.solver->mustBeTrue(*s, 
                                   EqExpr::create(ZExtExpr::create(arguments[1],
                                                                   Context::get().getPointerWidth()),
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index d52b8fc5..2dfdde43 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -120,6 +120,7 @@ namespace klee {
     HANDLER(handleNew);
     HANDLER(handleNewArray);
     HANDLER(handlePreferCex);
+    HANDLER(handlePosixPreferCex);
     HANDLER(handlePrintExpr);
     HANDLER(handlePrintRange);
     HANDLER(handleRange);
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 0e564fe5..cf8a1654 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -27,13 +27,6 @@
 #include "UserSearcher.h"
 #include "../Solver/SolverStats.h"
 
-// FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs.
-#undef PACKAGE_BUGREPORT
-#undef PACKAGE_NAME
-#undef PACKAGE_STRING
-#undef PACKAGE_TARNAME
-#undef PACKAGE_VERSION
-
 #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
 #include "llvm/IR/BasicBlock.h"
 #include "llvm/IR/Function.h"
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.;
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-10-06 12:33:32 +0000