about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h8
-rw-r--r--include/klee/util/ArrayExprHash.h2
-rw-r--r--include/klee/util/Assignment.h7
-rw-r--r--include/klee/util/ExprRangeEvaluator.h2
-rw-r--r--lib/Core/Searcher.cpp6
-rw-r--r--lib/Core/Searcher.h3
-rw-r--r--lib/Core/UserSearcher.cpp12
-rw-r--r--lib/Expr/Updates.cpp10
-rw-r--r--lib/Solver/FastCexSolver.cpp15
-rw-r--r--lib/Solver/Solver.cpp16
10 files changed, 44 insertions, 37 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index ee3c3253..a302591a 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -675,15 +675,15 @@ public:
   
   static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
   
-  Width getWidth() const { return updates.root->getRange(); }
+  Width getWidth() const { assert(updates.root); return updates.root->getRange(); }
   Kind getKind() const { return Read; }
   
   unsigned getNumKids() const { return numKids; }
-  ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }  
+  ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }
   
   int compareContents(const Expr &b) const;
 
-  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { 
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
     return create(updates, kids[0]);
   }
 
@@ -691,7 +691,7 @@ public:
 
 private:
   ReadExpr(const UpdateList &_updates, const ref<Expr> &_index) : 
-    updates(_updates), index(_index) {}
+    updates(_updates), index(_index) { assert(updates.root); }
 
 public:
   static bool classof(const Expr *E) {
diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h
index 9a527bcd..1e5ffc2e 100644
--- a/include/klee/util/ArrayExprHash.h
+++ b/include/klee/util/ArrayExprHash.h
@@ -132,4 +132,4 @@ void ArrayExprHash<T>::hashUpdateNodeExpr(const UpdateNode* un, T& exp)
 
 }
 
-#endif
\ No newline at end of file
+#endif
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 838d03bd..63df4b65 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -67,15 +67,16 @@ namespace klee {
 
   inline ref<Expr> Assignment::evaluate(const Array *array, 
                                         unsigned index) const {
+    assert(array);
     bindings_ty::const_iterator it = bindings.find(array);
     if (it!=bindings.end() && index<it->second.size()) {
-      return ConstantExpr::alloc(it->second[index], Expr::Int8);
+      return ConstantExpr::alloc(it->second[index], array->getRange());
     } else {
       if (allowFreeValues) {
         return ReadExpr::create(UpdateList(array, 0), 
-                                ConstantExpr::alloc(index, Expr::Int32));
+                                ConstantExpr::alloc(index, array->getDomain()));
       } else {
-        return ConstantExpr::alloc(0, Expr::Int8);
+        return ConstantExpr::alloc(0, array->getRange());
       }
     }
   }
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
index 34b85520..fea30b5b 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -102,7 +102,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     const ReadExpr *re = cast<ReadExpr>(e);
     T index = evaluate(re->index);
 
-    assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read");
+    assert(re->updates.root && re->getWidth() == re->updates.root->range && "unexpected multibyte read");
 
     return evalRead(re->updates, index);
   }
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 2dbabd01..8c3e26bc 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -157,10 +157,8 @@ void RandomSearcher::update(ExecutionState *current,
 
 ///
 
-WeightedRandomSearcher::WeightedRandomSearcher(Executor &_executor,
-                                               WeightType _type) 
-  : executor(_executor),
-    states(new DiscretePDF<ExecutionState*>()),
+WeightedRandomSearcher::WeightedRandomSearcher(WeightType _type)
+  : states(new DiscretePDF<ExecutionState*>()),
     type(_type) {
   switch(type) {
   case Depth: 
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 79c233c4..3944d4b4 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -135,7 +135,6 @@ namespace klee {
     };
 
   private:
-    Executor &executor;
     DiscretePDF<ExecutionState*> *states;
     WeightType type;
     bool updateWeights;
@@ -143,7 +142,7 @@ namespace klee {
     double getWeight(ExecutionState*);
 
   public:
-    WeightedRandomSearcher(Executor &executor, WeightType type);
+    WeightedRandomSearcher(WeightType type);
     ~WeightedRandomSearcher();
 
     ExecutionState &selectState();
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index a20ae968..2c75f796 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -81,12 +81,12 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
   case Searcher::BFS: searcher = new BFSSearcher(); break;
   case Searcher::RandomState: searcher = new RandomSearcher(); break;
   case Searcher::RandomPath: searcher = new RandomPathSearcher(executor); break;
-  case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CoveringNew); break;
-  case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::MinDistToUncovered); break;
-  case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::Depth); break;
-  case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::InstCount); break;
-  case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CPInstCount); break;
-  case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::QueryCost); break;
+  case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew); break;
+  case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered); break;
+  case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth); break;
+  case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::InstCount); break;
+  case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CPInstCount); break;
+  case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::QueryCost); break;
   }
 
   return searcher;
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 14fd8308..bf7049ba 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -22,8 +22,12 @@ UpdateNode::UpdateNode(const UpdateNode *_next,
     next(_next),
     index(_index),
     value(_value) {
+  // FIXME: What we need to check here instead is that _value is of the same width 
+  // as the range of the array that the update node is part of.
+  /*
   assert(_value->getWidth() == Expr::Int8 && 
          "Update value should be 8-bit wide.");
+  */
   computeHash();
   if (next) {
     ++next->refCount;
@@ -84,6 +88,12 @@ UpdateList &UpdateList::operator=(const UpdateList &b) {
 }
 
 void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
+  
+  if (root) {
+    assert(root->getDomain() == index->getWidth());
+    assert(root->getRange() == value->getWidth());
+  }
+
   if (head) --head->refCount;
   head = new UpdateNode(head, index, value);
   ++head->refCount;
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 08a9ef7c..6e52dc32 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -363,12 +363,12 @@ protected:
     // value cannot be part of the assignment.
     if (index >= array.size)
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
       
     std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array);
     return ConstantExpr::alloc((it == objects.end() ? 127 : 
                                 it->second->getPossibleValue(index)),
-                               Expr::Int8);
+                               array.getRange());
   }
 
 public:
@@ -384,19 +384,19 @@ protected:
     // value cannot be part of the assignment.
     if (index >= array.size)
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
       
     std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array);
     if (it == objects.end())
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
 
     CexValueData cvd = it->second->getExactValues(index);
     if (!cvd.isFixed())
       return ReadExpr::create(UpdateList(&array, 0), 
-                              ConstantExpr::alloc(index, Expr::Int32));
+                              ConstantExpr::alloc(index, array.getDomain()));
 
-    return ConstantExpr::alloc(cvd.min(), Expr::Int8);
+    return ConstantExpr::alloc(cvd.min(), array.getRange());
   }
 
 public:
@@ -1109,13 +1109,14 @@ FastCexSolver::computeInitialValues(const Query& query,
   // Propogation found a satisfying assignment, compute the initial values.
   for (unsigned i = 0; i != objects.size(); ++i) {
     const Array *array = objects[i];
+    assert(array);
     std::vector<unsigned char> data;
     data.reserve(array->size);
 
     for (unsigned i=0; i < array->size; i++) {
       ref<Expr> read = 
         ReadExpr::create(UpdateList(array, 0),
-                         ConstantExpr::create(i, Expr::Int32));
+                         ConstantExpr::create(i, array->getDomain()));
       ref<Expr> value = cd.evaluatePossible(read);
       
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 22b1545f..025c70f2 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -407,11 +407,12 @@ ValidatingSolver::computeInitialValues(const Query& query,
     std::vector< ref<Expr> > bindings;
     for (unsigned i = 0; i != values.size(); ++i) {
       const Array *array = objects[i];
+      assert(array);
       for (unsigned j=0; j<array->size; j++) {
         unsigned char value = values[i][j];
         bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0),
-                                                           ConstantExpr::alloc(j, Expr::Int32)),
-                                          ConstantExpr::alloc(value, Expr::Int8)));
+                                                           ConstantExpr::alloc(j, array->getDomain())),
+                                          ConstantExpr::alloc(value, array->getRange())));
       }
     }
     ConstraintManager tmp(bindings);
@@ -493,8 +494,6 @@ Solver *klee::createDummySolver() {
 
 class STPSolverImpl : public SolverImpl {
 private:
-  /// The solver we are part of, for access to public information.
-  STPSolver *solver;
   VC vc;
   STPBuilder *builder;
   double timeout;
@@ -502,7 +501,7 @@ private:
   SolverRunStatus runStatusCode;
 
 public:
-  STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
+  STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
   
   char *getConstraintLog(const Query&);
@@ -526,9 +525,8 @@ static void stp_error_handler(const char* err_msg) {
   abort();
 }
 
-STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides)
-  : solver(_solver),
-    vc(vc_createValidityChecker()),
+STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
+  : vc(vc_createValidityChecker()),
     builder(new STPBuilder(vc, _optimizeDivides)),
     timeout(0.0),
     useForkedSTP(_useForkedSTP),
@@ -565,7 +563,7 @@ STPSolverImpl::~STPSolverImpl() {
 /***/
 
 STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
-  : Solver(new STPSolverImpl(this, useForkedSTP, optimizeDivides))
+  : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides))
 {
 }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-10-06 20:20:56 +0000