Create AlphaEquvalenceSolver

Author: dim8art

include/klee/Expr/AlphaBuilder.h

@@ -0,0 +1,41 @@
+//===-- AlphaBuilder.h -----------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_ALPHA_BUILDER_H
+#define KLEE_ALPHA_BUILDER_H
+
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/ExprVisitor.h"
+
+namespace klee {
+
+class AlphaBuilder : public ExprVisitor {
+public:
+  ExprHashMap<ref<Expr>> reverseExprMap;
+  ArrayCache::ArrayHashMap<const Array *> reverseAlphaArrayMap;
+  ArrayCache::ArrayHashMap<const Array *> alphaArrayMap;
+
+private:
+  ArrayCache &arrayCache;
+  unsigned index = 0;
+
+  const Array *visitArray(const Array *arr);
+  UpdateList visitUpdateList(UpdateList u);
+  Action visitRead(const ReadExpr &re);
+
+public:
+  AlphaBuilder(ArrayCache &_arrayCache);
+  constraints_ty visitConstraints(constraints_ty cs);
+  ref<Expr> visitExpr(ref<Expr> v);
+};
+
+} // namespace klee
+
+#endif /*KLEE_ALPHA_VERSION_BUILDER_H*/

include/klee/Expr/Parser/Parser.h

@@ -220,6 +220,8 @@ class Parser {
   static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB,
                         ExprBuilder *Builder, ArrayCache *TheArrayCache,
                         KModule *km, bool ClearArrayAfterQuery);
+
+  virtual ArrayCache &getArrayCache() = 0;
 };
 } // namespace expr
 } // namespace klee

include/klee/Expr/SourceBuilder.h

@@ -32,6 +32,7 @@ class SourceBuilder {
   static ref<SymbolicSource> value(const llvm::Value &_allocSite, int _index,
                                    KModule *km);
   static ref<SymbolicSource> irreproducible(const std::string &name);
+  static ref<SymbolicSource> alpha(int _index);
 };
 
 }; // namespace klee

include/klee/Expr/SymbolicSource.h

@@ -45,7 +45,8 @@ class SymbolicSource {
     LazyInitializationSize,
     Instruction,
     Argument,
-    Irreproducible
+    Irreproducible,
+    Alpha
   };
 
 public:
@@ -349,6 +350,37 @@ class IrreproducibleSource : public SymbolicSource {
   }
 };
 
+class AlphaSource : public SymbolicSource {
+public:
+  const unsigned index;
+
+  AlphaSource(unsigned _index) : index(_index) {}
+  Kind getKind() const override { return Kind::Alpha; }
+  virtual std::string getName() const override { return "alpha"; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::Alpha;
+  }
+  static bool classof(const AlphaSource *) { return true; }
+
+  virtual unsigned computeHash() override {
+    unsigned res = getKind();
+    hashValue = res ^ (index * SymbolicSource::MAGIC_HASH_CONSTANT);
+    return hashValue;
+  }
+
+  virtual int internalCompare(const SymbolicSource &b) const override {
+    if (getKind() != b.getKind()) {
+      return getKind() < b.getKind() ? -1 : 1;
+    }
+    const AlphaSource &amb = static_cast<const AlphaSource &>(b);
+    if (index != amb.index) {
+      return index < amb.index ? -1 : 1;
+    }
+    return 0;
+  }
+};
+
 } // namespace klee
 
 #endif /* KLEE_SYMBOLICSOURCE_H */

include/klee/Solver/Common.h

@@ -29,7 +29,7 @@ std::unique_ptr<Solver> constructSolverChain(
     std::unique_ptr<Solver> coreSolver, std::string querySMT2LogPath,
     std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath,
     std::string baseSolverQueryKQueryLogPath,
-    AddressGenerator *addressGenerator);
+    AddressGenerator *addressGenerator, ArrayCache &arrayCache);
 } // namespace klee
 
 #endif /* KLEE_COMMON_H */

include/klee/Solver/Solver.h

@@ -244,6 +244,14 @@ std::unique_ptr<Solver> createFastCexSolver(std::unique_ptr<Solver> s);
 /// \param s - The underlying solver to use.
 std::unique_ptr<Solver> createIndependentSolver(std::unique_ptr<Solver> s);
 
+/// createAlphaEquivalenceSolver - Create a solver which will change
+/// independent queries to their alpha-equvalent version
+///
+/// \param s - The underlying solver to use.
+/// \param arrayCache - Class to create new arrays.
+std::unique_ptr<Solver> createAlphaEquivalenceSolver(std::unique_ptr<Solver> s,
+                                                     ArrayCache &arrayCache);
+
 /// createKQueryLoggingSolver - Create a solver which will forward all queries
 /// after writing them to the given path in .kquery format.
 std::unique_ptr<Solver> createKQueryLoggingSolver(std::unique_ptr<Solver> s,

include/klee/Solver/SolverCmdLine.h

@@ -32,6 +32,8 @@ extern llvm::cl::opt<bool> UseCexCache;
 
 extern llvm::cl::opt<bool> UseBranchCache;
 
+extern llvm::cl::opt<bool> UseAlphaEquivalence;
+
 extern llvm::cl::opt<bool> UseConcretizingSolver;
 
 extern llvm::cl::opt<bool> UseIndependentSolver;

lib/Core/Executor.cpp

@@ -515,7 +515,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
       interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME),
       interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME),
-      addressManager.get());
+      addressManager.get(), arrayCache);
 
   this->solver = std::make_unique<TimingSolver>(std::move(solver), optimizer,
                                                 EqualitySubstitution);

lib/Expr/AlphaBuilder.cpp

@@ -0,0 +1,85 @@
+//===-- AlphaBuilder.cpp ---------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Expr/AlphaBuilder.h"
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/SourceBuilder.h"
+
+#include <vector>
+
+namespace klee {
+
+const Array *AlphaBuilder::visitArray(const Array *arr) {
+  if (alphaArrayMap.find(arr) == alphaArrayMap.end()) {
+    ref<SymbolicSource> source = arr->source;
+    ref<Expr> size = visit(arr->getSize());
+
+    if (!arr->isConstantArray()) {
+      source = SourceBuilder::alpha(index);
+      index++;
+      alphaArrayMap[arr] = arrayCache.CreateArray(
+          size, source, arr->getDomain(), arr->getRange());
+      reverseAlphaArrayMap[alphaArrayMap[arr]] = arr;
+    } else if (size != arr->getSize()) {
+      alphaArrayMap[arr] = arrayCache.CreateArray(
+          size, source, arr->getDomain(), arr->getRange());
+      reverseAlphaArrayMap[alphaArrayMap[arr]] = arr;
+    } else {
+      alphaArrayMap[arr] = arr;
+      reverseAlphaArrayMap[arr] = arr;
+    }
+  }
+  return alphaArrayMap[arr];
+}
+
+UpdateList AlphaBuilder::visitUpdateList(UpdateList u) {
+  const Array *root = visitArray(u.root);
+  std::vector<ref<UpdateNode>> updates;
+
+  for (auto un = u.head; un; un = un->next) {
+    updates.push_back(un);
+  }
+
+  updates.push_back(nullptr);
+
+  for (int i = updates.size() - 2; i >= 0; i--) {
+    ref<Expr> index = visit(updates[i]->index);
+    ref<Expr> value = visit(updates[i]->value);
+    updates[i] = new UpdateNode(updates[i + 1], index, value);
+  }
+  return UpdateList(root, updates[0]);
+}
+
+ExprVisitor::Action AlphaBuilder::visitRead(const ReadExpr &re) {
+  ref<Expr> v = visit(re.index);
+  UpdateList u = visitUpdateList(re.updates);
+  ref<Expr> e = ReadExpr::create(u, v);
+  return Action::changeTo(e);
+}
+
+AlphaBuilder::AlphaBuilder(ArrayCache &_arrayCache) : arrayCache(_arrayCache) {}
+
+constraints_ty AlphaBuilder::visitConstraints(constraints_ty cs) {
+  constraints_ty result;
+  for (auto arg : cs) {
+    ref<Expr> v = visit(arg);
+    reverseExprMap[v] = arg;
+    reverseExprMap[Expr::createIsZero(v)] = Expr::createIsZero(arg);
+    result.insert(v);
+  }
+  return result;
+}
+ref<Expr> AlphaBuilder::visitExpr(ref<Expr> v) {
+  ref<Expr> e = visit(v);
+  reverseExprMap[e] = v;
+  reverseExprMap[Expr::createIsZero(e)] = Expr::createIsZero(v);
+  return e;
+}
+
+} // namespace klee

lib/Expr/CMakeLists.txt

@@ -7,6 +7,7 @@
 #
 #===------------------------------------------------------------------------===#
 add_library(kleaverExpr
+  AlphaBuilder.cpp
   APFloatEval.cpp
   ArrayCache.cpp
   ArrayExprOptimizer.cpp