[feat, bitwuzla] getConstraintLog implementation.

S1eGa · Nov 20, 2023 · f5859c6 · f5859c6
1 parent f2304ff
commit f5859c6
Show file tree

Hide file tree

Showing 3 changed files with 55 additions and 4 deletions.
diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
@@ -49,7 +49,11 @@ class ConstraintSet {
   bool isSymcretized(ref<Expr> expr) const;
 
   void rewriteConcretization(const Assignment &a);
-  ConstraintSet withExpr(ref<Expr> e) const;
+  ConstraintSet withExpr(ref<Expr> e) const {
+    ConstraintSet copy = ConstraintSet(*this);
+    copy.addConstraint(e, Assignment());
+    return copy;
+  }
 
   std::vector<const Array *> gatherArrays() const;
   std::vector<const Array *> gatherSymcretizedArrays() const;

diff --git a/lib/Solver/BitwuzlaBuilder.h b/lib/Solver/BitwuzlaBuilder.h
@@ -118,6 +118,10 @@ class BitwuzlaBuilder {
   // these.
   std::vector<Term> sideConstraints;
 
+  std::string symbolOf(const Array *array) {
+    return getInitialArray(array).symbol().value();
+  }
+
   BitwuzlaBuilder(bool autoClearConstructCache);
   ~BitwuzlaBuilder();
 

diff --git a/lib/Solver/BitwuzlaSolver.cpp b/lib/Solver/BitwuzlaSolver.cpp
@@ -170,7 +170,7 @@ struct BitwuzlaSolverEnv {
   inc_umap<const Array *, ExprHashSet> usedArrayBytes;
   ExprIncSet symbolicObjects;
 
-  explicit BitwuzlaSolverEnv(){};
+  explicit BitwuzlaSolverEnv() = default;
   explicit BitwuzlaSolverEnv(const arr_vec &objects);
 
   void pop(size_t popSize);
@@ -180,7 +180,7 @@ struct BitwuzlaSolverEnv {
   const arr_vec *getObjectsForGetModel(ObjectAssignment oa) const;
 };
 
-BitwuzlaSolverEnv::BitwuzlaSolverEnv(const std::vector<const Array *> &objects)
+BitwuzlaSolverEnv::BitwuzlaSolverEnv(const arr_vec &objects)
     : objectsForGetModel(objects) {}
 
 void BitwuzlaSolverEnv::pop(size_t popSize) {
@@ -314,7 +314,50 @@ BitwuzlaSolverImpl::BitwuzlaSolverImpl()
 }
 
 char *BitwuzlaSolverImpl::getConstraintLog(const Query &query) {
-  return strdup("unimplemented");
+  std::stringstream outputLog;
+
+  // We use a different builder here because we don't want to interfere
+  // with the solver's builder because it may change the solver builder's
+  // cache.
+  // NOTE: The builder does not set `z3LogInteractionFile` to avoid conflicting
+  // with whatever the solver's builder is set to do.
+  std::unique_ptr<BitwuzlaBuilder> tempBuilder(new BitwuzlaBuilder(false));
+  ConstantArrayFinder constant_arrays_in_query;
+
+  for (const auto array :
+       query.constraints.withExpr(query.expr).gatherArrays()) {
+    outputLog << "(declare-fun " << tempBuilder->symbolOf(array)
+              << " () (Array (_ BitVec " << array->getDomain() << ") (_ BitVec "
+              << array->getRange() << ")))\n";
+  }
+
+  for (auto const &constraint : query.constraints.cs()) {
+    outputLog << "(assert " << tempBuilder->construct(constraint).str(10)
+              << ")\n";
+    constant_arrays_in_query.visit(constraint);
+  }
+
+  // KLEE Queries are validity queries i.e.
+  // ∀ X Constraints(X) → query(X)
+  // but Z3 works in terms of satisfiability so instead we ask the
+  // the negation of the equivalent i.e.
+  // ∃ X Constraints(X) ∧ ¬ query(X)
+  Term formula = mk_term(Kind::NOT, {tempBuilder->construct(query.expr)});
+  constant_arrays_in_query.visit(query.expr);
+
+  for (auto const &constant_array : constant_arrays_in_query.results) {
+    for (auto const &arrayIndexValueExpr :
+         tempBuilder->constant_array_assertions[constant_array]) {
+      outputLog << "(assert " << arrayIndexValueExpr.str(10) << ")\n";
+    }
+  }
+
+  outputLog << "(assert " << formula.str(10) << ")\n";
+  outputLog << "(check-sat)"
+            << "\n";
+
+  // Client is responsible for freeing the returned C-string
+  return strdup(outputLog.str().c_str());
 }
 
 bool BitwuzlaSolverImpl::computeTruth(const ConstraintQuery &query,