Create AlphaEquvalenceSolver

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,84 @@
+//===-- 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;
+    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

lib/Expr/ExprPPrinter.cpp

@@ -410,6 +410,8 @@ class PPrinter : public ExprPPrinter {
          << kf->getName().str() << " " << s->index;
     } else if (auto s = dyn_cast<IrreproducibleSource>(source)) {
       PC << s->name;
+    } else if (auto s = dyn_cast<AlphaSource>(source)) {
+      PC << s->index;
     } else {
       assert(0 && "Not implemented");
     }

lib/Expr/Parser.cpp

@@ -280,6 +280,8 @@ class ParserImpl : public Parser {
     }
   }
 
+  ArrayCache &getArrayCache() { return *TheArrayCache; }
+
   /*** Grammar productions ****/
 
   /* Top level decls */
@@ -329,6 +331,7 @@ class ParserImpl : public Parser {
   SourceResult ParseLazyInitializationSizeSource();
   SourceResult ParseInstructionSource();
   SourceResult ParseArgumentSource();
+  SourceResult ParseAlphaSource();
 
   /*** Diagnostics ***/
 
@@ -498,6 +501,8 @@ SourceResult ParserImpl::ParseSource() {
   } else if (type == "argument") {
     assert(km);
     source = ParseArgumentSource();
+  } else if (type == "alpha") {
+    source = ParseAlphaSource();
   } else {
     assert(0);
   }
@@ -626,6 +631,12 @@ SourceResult ParserImpl::ParseInstructionSource() {
   return SourceBuilder::instruction(*KI->inst, index, km);
 }
 
+SourceResult ParserImpl::ParseAlphaSource() {
+  auto indexExpr = ParseNumber(64).get();
+  auto index = dyn_cast<ConstantExpr>(indexExpr)->getZExtValue();
+  return SourceBuilder::alpha(index);
+}
+
 /// ParseCommandDecl - Parse a command declaration. The lexer should
 /// be positioned at the opening '('.
 ///

lib/Expr/SourceBuilder.cpp

@@ -88,3 +88,9 @@ ref<SymbolicSource> SourceBuilder::irreproducible(const std::string &name) {
   r->computeHash();
   return r;
 }
+
+ref<SymbolicSource> SourceBuilder::alpha(int _index) {
+  ref<SymbolicSource> r(new AlphaSource(_index));
+  r->computeHash();
+  return r;
+}