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/CallPathManager.cpp5
-rw-r--r--lib/Core/Context.cpp5
-rw-r--r--lib/Core/ExecutionState.cpp5
-rw-r--r--lib/Core/Executor.cpp249
-rw-r--r--lib/Core/ExecutorTimerInfo.h42
-rw-r--r--lib/Core/ExecutorTimers.cpp25
-rw-r--r--lib/Core/ExecutorUtil.cpp16
-rw-r--r--lib/Core/ExternalDispatcher.cpp22
-rw-r--r--lib/Core/Memory.cpp7
-rw-r--r--lib/Core/Searcher.cpp7
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp8
-rw-r--r--lib/Core/StatsTracker.cpp26
-rw-r--r--lib/Core/TimingSolver.cpp4
13 files changed, 300 insertions, 121 deletions
diff --git a/lib/Core/CallPathManager.cpp b/lib/Core/CallPathManager.cpp
index ca127f25..03e75108 100644
--- a/lib/Core/CallPathManager.cpp
+++ b/lib/Core/CallPathManager.cpp
@@ -13,7 +13,12 @@
 
 #include <map>
 #include <vector>
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#else
 #include "llvm/Function.h"
+#endif
+
 #include "llvm/Support/raw_ostream.h"
 
 using namespace llvm;
diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp
index 979970aa..935e4316 100644
--- a/lib/Core/Context.cpp
+++ b/lib/Core/Context.cpp
@@ -11,8 +11,13 @@
 
 #include "klee/Expr.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Type.h"
+#include "llvm/IR/DerivedTypes.h"
+#else
 #include "llvm/Type.h"
 #include "llvm/DerivedTypes.h"
+#endif
 
 #include <cassert>
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index db685639..b2c2a737 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -17,8 +17,11 @@
 #include "klee/Expr.h"
 
 #include "Memory.h"
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#else
 #include "llvm/Function.h"
+#endif
 #include "llvm/Support/CommandLine.h"
 
 #include <iostream>
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 069022a2..ef55f21f 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -24,6 +24,7 @@
 #include "StatsTracker.h"
 #include "TimingSolver.h"
 #include "UserSearcher.h"
+#include "ExecutorTimerInfo.h"
 #include "../Solver/SolverStats.h"
 
 #include "klee/ExecutionState.h"
@@ -47,31 +48,40 @@
 #include "klee/Internal/Support/FloatEvaluation.h"
 #include "klee/Internal/System/Time.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Attributes.h"
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/LLVMContext.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/DataLayout.h"
+#include "llvm/IR/TypeBuilder.h"
+#else
 #include "llvm/Attributes.h"
 #include "llvm/BasicBlock.h"
 #include "llvm/Constants.h"
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
 #include "llvm/IntrinsicInst.h"
-#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
-#endif
 #include "llvm/Module.h"
+#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
+#include "llvm/Target/TargetData.h"
+#else
+#include "llvm/DataLayout.h"
+#include "llvm/TypeBuilder.h"
+#endif
+#endif
 #include "llvm/ADT/SmallPtrSet.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CallSite.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-#include "llvm/System/Process.h"
-#else
 #include "llvm/Support/Process.h"
-#endif
-#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
-#include "llvm/Target/TargetData.h"
-#else
-#include "llvm/DataLayout.h"
-#endif
 
 #include <cassert>
 #include <algorithm>
@@ -90,6 +100,33 @@
 using namespace llvm;
 using namespace klee;
 
+
+#ifdef SUPPORT_METASMT
+
+#include <metaSMT/frontend/Array.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.hpp>
+#include <metaSMT/backend/MiniSAT.hpp>
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/support/run_algorithm.hpp>
+#include <metaSMT/API/Stack.hpp>
+#include <metaSMT/API/Group.hpp>
+
+#define Expr VCExpr
+#define Type VCType
+#define STP STP_Backend
+#include <metaSMT/backend/STP.hpp>
+#undef Expr
+#undef Type
+#undef STP
+
+using namespace metaSMT;
+using namespace metaSMT::solver;
+
+#endif /* SUPPORT_METASMT */
+
+
+
 namespace {
   cl::opt<bool>
   DumpStatesOnHalt("dump-states-on-halt",
@@ -253,7 +290,41 @@ Executor::Executor(const InterpreterOptions &opts,
       : std::max(MaxCoreSolverTime,MaxInstructionTime)) {
       
   if (coreSolverTimeout) UseForkedCoreSolver = true;
-  Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);  
+  
+  Solver *coreSolver = NULL;
+  
+#ifdef SUPPORT_METASMT
+  if (UseMetaSMT != METASMT_BACKEND_NONE) {
+    
+    std::string backend;
+    
+    switch (UseMetaSMT) {
+          case METASMT_BACKEND_STP:
+              backend = "STP"; 
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          case METASMT_BACKEND_Z3:
+              backend = "Z3";
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          case METASMT_BACKEND_BOOLECTOR:
+              backend = "Boolector";
+              coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+              break;
+          default:
+              assert(false);
+              break;
+    };
+    std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n";
+  }
+  else {
+    coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+  }
+#else
+  coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+#endif /* SUPPORT_METASMT */
+  
+   
   Solver *solver = 
     constructSolverChain(coreSolver,
                          interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
@@ -309,6 +380,10 @@ Executor::~Executor() {
     delete statsTracker;
   delete solver;
   delete kmodule;
+  while(!timers.empty()) {
+    delete timers.back();
+    timers.pop_back();
+  }
 }
 
 /***/
@@ -386,10 +461,10 @@ void Executor::initializeGlobals(ExecutionState &state) {
 
   if (m->getModuleInlineAsm() != "")
     klee_warning("executable has module level assembly (ignoring)");
-
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
   assert(m->lib_begin() == m->lib_end() &&
          "XXX do not support dependent libraries");
-
+#endif
   // represent function globals using the address of the actual llvm function
   // object. given that we use malloc to allocate memory in states this also
   // ensures that we won't conflict. we don't need to allocate a memory object
@@ -501,9 +576,17 @@ void Executor::initializeGlobals(ExecutionState &state) {
       uint64_t size = kmodule->targetData->getTypeStoreSize(ty);
       MemoryObject *mo = 0;
 
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
       if (UseAsmAddresses && i->getName()[0]=='\01') {
+#else
+      if (UseAsmAddresses && !i->getName().empty()) {
+#endif
         char *end;
+#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3)
         uint64_t address = ::strtoll(i->getName().str().c_str()+1, &end, 0);
+#else
+        uint64_t address = ::strtoll(i->getName().str().c_str(), &end, 0);
+#endif
 
         if (end && *end == '\0') {
           klee_message("NOTE: allocated global at asm specified address: %#08llx"
@@ -557,20 +640,31 @@ void Executor::branch(ExecutionState &state,
   unsigned N = conditions.size();
   assert(N);
 
-  stats::forks += N-1;
+  if (MaxForks!=~0u && stats::forks >= MaxForks) {
+    unsigned next = theRNG.getInt32() % N;
+    for (unsigned i=0; i<N; ++i) {
+      if (i == next) {
+        result.push_back(&state);
+      } else {
+        result.push_back(NULL);
+      }
+    }
+  } else {
+    stats::forks += N-1;
 
-  // XXX do proper balance or keep random?
-  result.push_back(&state);
-  for (unsigned i=1; i<N; ++i) {
-    ExecutionState *es = result[theRNG.getInt32() % i];
-    ExecutionState *ns = es->branch();
-    addedStates.insert(ns);
-    result.push_back(ns);
-    es->ptreeNode->data = 0;
-    std::pair<PTree::Node*,PTree::Node*> res = 
-      processTree->split(es->ptreeNode, ns, es);
-    ns->ptreeNode = res.first;
-    es->ptreeNode = res.second;
+    // XXX do proper balance or keep random?
+    result.push_back(&state);
+    for (unsigned i=1; i<N; ++i) {
+      ExecutionState *es = result[theRNG.getInt32() % i];
+      ExecutionState *ns = es->branch();
+      addedStates.insert(ns);
+      result.push_back(ns);
+      es->ptreeNode->data = 0;
+      std::pair<PTree::Node*,PTree::Node*> res = 
+        processTree->split(es->ptreeNode, ns, es);
+      ns->ptreeNode = res.first;
+      es->ptreeNode = res.second;
+    }
   }
 
   // If necessary redistribute seeds to match conditions, killing
@@ -605,12 +699,14 @@ void Executor::branch(ExecutionState &state,
       if (i==N)
         i = theRNG.getInt32() % N;
 
-      seedMap[result[i]].push_back(*siit);
+      // Extra check in case we're replaying seeds with a max-fork
+      if (result[i])
+        seedMap[result[i]].push_back(*siit);
     }
 
     if (OnlyReplaySeeds) {
       for (unsigned i=0; i<N; ++i) {
-        if (!seedMap.count(result[i])) {
+        if (result[i] && !seedMap.count(result[i])) {
           terminateState(*result[i]);
           result[i] = NULL;
         }
@@ -1302,26 +1398,9 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) {
   }
 }
 
+/// TODO remove?
 static bool isDebugIntrinsic(const Function *f, KModule *KM) {
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-  // Fast path, getIntrinsicID is slow.
-  if (f == KM->dbgStopPointFn)
-    return true;
-
-  switch (f->getIntrinsicID()) {
-  case Intrinsic::dbg_stoppoint:
-  case Intrinsic::dbg_region_start:
-  case Intrinsic::dbg_region_end:
-  case Intrinsic::dbg_func_start:
-  case Intrinsic::dbg_declare:
-    return true;
-
-  default:
-    return false;
-  }
-#else
   return false;
-#endif
 }
 
 static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) {
@@ -1380,7 +1459,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                            CallSite(cast<CallInst>(caller)));
 
             // XXX need to check other param attrs ?
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+      bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt);
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
 	    bool isSExt = cs.paramHasAttr(0, llvm::Attributes::SExt);
 #else
 	    bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt);
@@ -1584,7 +1665,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
             if (from != to) {
               // XXX need to check other param attrs ?
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+              bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt);
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
 	      bool isSExt = cs.paramHasAttr(i+1, llvm::Attributes::SExt);
 #else
 	      bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt);
@@ -1867,14 +1950,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
  
     // Memory instructions...
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-  case Instruction::Malloc:
-  case Instruction::Alloca: {
-    AllocationInst *ai = cast<AllocationInst>(i);
-#else
   case Instruction::Alloca: {
     AllocaInst *ai = cast<AllocaInst>(i);
-#endif
     unsigned elementSize = 
       kmodule->targetData->getTypeStoreSize(ai->getAllocatedType());
     ref<Expr> size = Expr::createPointer(elementSize);
@@ -1887,12 +1964,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     executeAlloc(state, size, isLocal, ki);
     break;
   }
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-  case Instruction::Free: {
-    executeFree(state, eval(ki, 0, state).value);
-    break;
-  }
-#endif
 
   case Instruction::Load: {
     ref<Expr> base = eval(ki, 0, state).value;
@@ -1982,8 +2053,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FAdd operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.add(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue()), APFloat::rmNearestTiesToEven);
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.add(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -1996,9 +2072,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (!fpWidthToSemantics(left->getWidth()) ||
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FSub operation");
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.subtract(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.subtract(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -2012,8 +2092,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FMul operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.multiply(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.multiply(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -2027,8 +2112,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FDiv operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.divide(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven);
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.divide(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -2041,9 +2131,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (!fpWidthToSemantics(left->getWidth()) ||
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FRem operation");
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue());
+    Res.remainder(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue()));
+#else
     llvm::APFloat Res(left->getAPValue());
     Res.mod(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven);
+#endif
     bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
     break;
   }
@@ -2056,7 +2150,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (!fpWidthToSemantics(arg->getWidth()) || resultType > arg->getWidth())
       return terminateStateOnExecError(state, "Unsupported FPTrunc operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
+#else
     llvm::APFloat Res(arg->getAPValue());
+#endif
     bool losesInfo = false;
     Res.convert(*fpWidthToSemantics(resultType),
                 llvm::APFloat::rmNearestTiesToEven,
@@ -2072,8 +2170,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                                         "floating point");
     if (!fpWidthToSemantics(arg->getWidth()) || arg->getWidth() > resultType)
       return terminateStateOnExecError(state, "Unsupported FPExt operation");
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
+#else
     llvm::APFloat Res(arg->getAPValue());
+#endif
     bool losesInfo = false;
     Res.convert(*fpWidthToSemantics(resultType),
                 llvm::APFloat::rmNearestTiesToEven,
@@ -2090,7 +2191,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64)
       return terminateStateOnExecError(state, "Unsupported FPToUI operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
+#else
     llvm::APFloat Arg(arg->getAPValue());
+#endif
     uint64_t value = 0;
     bool isExact = true;
     Arg.convertToInteger(&value, resultType, false,
@@ -2106,8 +2211,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                                        "floating point");
     if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64)
       return terminateStateOnExecError(state, "Unsupported FPToSI operation");
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue());
+#else
     llvm::APFloat Arg(arg->getAPValue());
+
+#endif
     uint64_t value = 0;
     bool isExact = true;
     Arg.convertToInteger(&value, resultType, true,
@@ -2158,8 +2267,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         !fpWidthToSemantics(right->getWidth()))
       return terminateStateOnExecError(state, "Unsupported FCmp operation");
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+    APFloat LHS(*fpWidthToSemantics(left->getWidth()),left->getAPValue());
+    APFloat RHS(*fpWidthToSemantics(right->getWidth()),right->getAPValue());
+#else
     APFloat LHS(left->getAPValue());
     APFloat RHS(right->getAPValue());
+#endif
     APFloat::cmpResult CmpRes = LHS.compare(RHS);
 
     bool Result = false;
@@ -2470,8 +2584,11 @@ void Executor::run(ExecutionState &initialState) {
         // We need to avoid calling GetMallocUsage() often because it
         // is O(elts on freelist). This is really bad since we start
         // to pummel the freelist once we hit the memory cap.
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+        unsigned mbs = sys::Process::GetMallocUsage() >> 20;
+#else
         unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20;
-        
+#endif
         if (mbs > MaxMemory) {
           if (mbs > MaxMemory + 100) {
             // just guess at how many to kill
diff --git a/lib/Core/ExecutorTimerInfo.h b/lib/Core/ExecutorTimerInfo.h
new file mode 100644
index 00000000..60977b74
--- /dev/null
+++ b/lib/Core/ExecutorTimerInfo.h
@@ -0,0 +1,42 @@
+//===-- Executor.h ----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+// Class to wrap information for a timer.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef EXECUTORTIMERINFO_H_
+#define EXECUTORTIMERINFO_H_
+
+#include "klee/Internal/System/Time.h"
+
+namespace klee {
+
+class Executor::TimerInfo {
+public:
+  Timer *timer;
+
+  /// Approximate delay per timer firing.
+  double rate;
+  /// Wall time for next firing.
+  double nextFireTime;
+
+public:
+  TimerInfo(Timer *_timer, double _rate)
+    : timer(_timer),
+      rate(_rate),
+      nextFireTime(util::getWallTime() + rate) {}
+  ~TimerInfo() { delete timer; }
+};
+
+
+}
+
+
+#endif /* EXECUTORTIMERINFO_H_ */
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 2fda5cba..06fd4be7 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -13,6 +13,7 @@
 #include "Executor.h"
 #include "PTree.h"
 #include "StatsTracker.h"
+#include "ExecutorTimerInfo.h"
 
 #include "klee/ExecutionState.h"
 #include "klee/Internal/Module/InstructionInfoTable.h"
@@ -20,7 +21,12 @@
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/System/Time.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#else
 #include "llvm/Function.h"
+#endif
+
 #include "llvm/Support/CommandLine.h"
 
 #include <unistd.h>
@@ -88,7 +94,7 @@ void Executor::initTimers() {
   }
 
   if (MaxTime) {
-    addTimer(new HaltTimer(this), MaxTime);
+    addTimer(new HaltTimer(this), MaxTime.getValue());
   }
 }
 
@@ -98,23 +104,6 @@ Executor::Timer::Timer() {}
 
 Executor::Timer::~Timer() {}
 
-class Executor::TimerInfo {
-public:
-  Timer *timer;
-  
-  /// Approximate delay per timer firing.
-  double rate;
-  /// Wall time for next firing.
-  double nextFireTime;
-  
-public:
-  TimerInfo(Timer *_timer, double _rate) 
-    : timer(_timer),
-      rate(_rate),
-      nextFireTime(util::getWallTime() + rate) {}
-  ~TimerInfo() { delete timer; }
-};
-
 void Executor::addTimer(Timer *timer, double rate) {
   timers.push_back(new TimerInfo(timer, rate));
 }
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 0d85afee..0d828ec4 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -20,19 +20,27 @@
 
 #include "klee/util/GetElementPtrTypeIterator.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/DataLayout.h"
+#else
 #include "llvm/Constants.h"
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
 #include "llvm/Module.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-#include "llvm/ModuleProvider.h"
-#endif
-#include "llvm/Support/CallSite.h"
 #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1)
 #include "llvm/Target/TargetData.h"
 #else
 #include "llvm/DataLayout.h"
 #endif
+#endif
+
+#include "llvm/Support/CallSite.h"
+
+
 #include <iostream>
 #include <cassert>
 
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 7da0c350..2dc16767 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -17,24 +17,23 @@
 #undef PACKAGE_TARNAME
 #undef PACKAGE_VERSION
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Module.h"
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/DerivedTypes.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/LLVMContext.h"
+#else
 #include "llvm/Module.h"
 #include "llvm/Constants.h"
 #include "llvm/DerivedTypes.h"
 #include "llvm/Instructions.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-#include "llvm/ModuleProvider.h"
-#endif
-#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7)
 #include "llvm/LLVMContext.h"
 #endif
 #include "llvm/ExecutionEngine/JIT.h"
 #include "llvm/ExecutionEngine/GenericValue.h"
 #include "llvm/Support/CallSite.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-#include "llvm/System/DynamicLibrary.h"
-#else
 #include "llvm/Support/DynamicLibrary.h"
-#endif
 #include "llvm/Support/raw_ostream.h"
 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 0)
 #include "llvm/Target/TargetSelect.h"
@@ -89,16 +88,9 @@ void *ExternalDispatcher::resolveSymbol(const std::string &name) {
 
 ExternalDispatcher::ExternalDispatcher() {
   dispatchModule = new Module("ExternalDispatcher", getGlobalContext());
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-  ExistingModuleProvider* MP = new ExistingModuleProvider(dispatchModule);
-#endif
 
   std::string error;
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-  executionEngine = ExecutionEngine::createJIT(MP, &error);
-#else
   executionEngine = ExecutionEngine::createJIT(dispatchModule, &error);
-#endif
   if (!executionEngine) {
     std::cerr << "unable to make jit: " << error << "\n";
     abort();
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 08c95d48..4bcdd9f7 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -19,9 +19,16 @@
 #include "ObjectHolder.h"
 #include "MemoryManager.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include <llvm/IR/Function.h>
+#include <llvm/IR/Instruction.h>
+#include <llvm/IR/Value.h>
+#else
 #include <llvm/Function.h>
 #include <llvm/Instruction.h>
 #include <llvm/Value.h>
+#endif
+
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
 
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 778ef0ef..2dbabd01 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -25,10 +25,15 @@
 #include "klee/Internal/ADT/RNG.h"
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/Time.h"
-
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Module.h"
+#else
 #include "llvm/Constants.h"
 #include "llvm/Instructions.h"
 #include "llvm/Module.h"
+#endif
 #include "llvm/Support/CallSite.h"
 #include "llvm/Support/CFG.h"
 #include "llvm/Support/CommandLine.h"
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index d44e13b6..04f32780 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -21,7 +21,11 @@
 #include "Executor.h"
 #include "MemoryManager.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include "llvm/IR/Module.h"
+#else
 #include "llvm/Module.h"
+#endif
 #include "llvm/ADT/Twine.h"
 
 #include <errno.h>
@@ -131,7 +135,9 @@ void SpecialFunctionHandler::prepare() {
       // Make sure NoReturn attribute is set, for optimization and
       // coverage counting.
       if (hi.doesNotReturn)
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+        f->addFnAttr(Attribute::NoReturn);
+#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
         f->addFnAttr(Attributes::NoReturn);
 #else
         f->addFnAttr(Attribute::NoReturn);
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index c0028a05..8161a52c 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -27,6 +27,15 @@
 #include "UserSearcher.h"
 #include "../Solver/SolverStats.h"
 
+#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
+#include "llvm/IR/BasicBlock.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IR/InlineAsm.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/Type.h"
+#else
 #include "llvm/BasicBlock.h"
 #include "llvm/Function.h"
 #include "llvm/Instructions.h"
@@ -34,21 +43,15 @@
 #include "llvm/InlineAsm.h"
 #include "llvm/Module.h"
 #include "llvm/Type.h"
+#endif
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/CFG.h"
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-#include "llvm/System/Process.h"
-#else
+#include "llvm/Support/raw_os_ostream.h"
 #include "llvm/Support/Process.h"
-#endif
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-#include "llvm/System/Path.h"
-#else
 #include "llvm/Support/Path.h"
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
 #include "llvm/Support/FileSystem.h"
 #endif
-#endif
 
 #include <iostream>
 #include <fstream>
@@ -294,9 +297,6 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
         //
         // FIXME: This trick no longer works, we should fix this in the line
         // number propogation.
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
-        if (isa<DbgStopPointInst>(inst))
-#endif
           es.coveredLines[&ii.file].insert(ii.line);
 	es.coveredNew = true;
         es.instsSinceCovNew = 1;
@@ -401,7 +401,11 @@ void StatsTracker::writeStatsLine() {
              << "," << numBranches
              << "," << util::getUserTime()
              << "," << executor.states.size()
+#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
+             << "," << sys::Process::GetMallocUsage()
+#else
              << "," << sys::Process::GetTotalMemoryUsage()
+#endif
              << "," << stats::queries
              << "," << stats::queryConstructs
              << "," << 0 // was numObjects
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index d2c07f46..037b23f3 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -16,11 +16,7 @@
 
 #include "CoreStats.h"
 
-#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9)
-#include "llvm/System/Process.h"
-#else
 #include "llvm/Support/Process.h"
-#endif
 
 using namespace klee;
 using namespace llvm;
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-05-10 14:58:45 +0000