Create AlphaEquvalencySolver

include/klee/Expr/AlphaVersionBuilder.h

@@ -0,0 +1,41 @@
+//===-- AlphaVersionBuilder.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_EQUIVALENCY_BUILDER_H
+#define KLEE_ALPHA_EQUIVALENCY_BUILDER_H
+
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/ExprHashMap.h"
+#include "klee/Expr/ExprVisitor.h"
+
+namespace klee {
+
+class AlphaVersionBuilder : 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:
+  AlphaVersionBuilder(ArrayCache &_arrayCache);
+  constraints_ty visitConstraints(constraints_ty cs);
+  ref<Expr> visitExpr(ref<Expr> v);
+};
+
+} // namespace klee
+
+#endif /*KLEE_ALPHA_EQUIVALENCY_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

@@ -28,6 +28,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> alphaModulo(int _index);
 };
 
 }; // namespace klee

include/klee/Expr/SymbolicSource.h

@@ -41,7 +41,8 @@ class SymbolicSource {
     LazyInitializationSize,
     Instruction,
     Argument,
-    Irreproducible
+    Irreproducible,
+    AlphaModulo
   };
 
 public:
@@ -361,6 +362,37 @@ class IrreproducibleSource : public SymbolicSource {
   }
 };
 
+class AlphaModuloSource : public SymbolicSource {
+public:
+  const unsigned index;
+
+  AlphaModuloSource(unsigned _index) : index(_index) {}
+  Kind getKind() const override { return Kind::AlphaModulo; }
+  virtual std::string getName() const override { return "alphaModulo"; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::AlphaModulo;
+  }
+  static bool classof(const AlphaModuloSource *) { 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 AlphaModuloSource &amb = static_cast<const AlphaModuloSource &>(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);
 
+/// createAlphaEquivalencySolver - 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> createAlphaEquivalencySolver(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

@@ -507,7 +507,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/AlphaVersionBuilder.cpp

@@ -0,0 +1,77 @@
+//===-- AlphaVersionBuilder.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/AlphaVersionBuilder.h"
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/SourceBuilder.h"
+
+#include <vector>
+
+namespace klee {
+
+const Array *AlphaVersionBuilder::visitArray(const Array *arr) {
+  if (alphaArrayMap.find(arr) == alphaArrayMap.end()) {
+    ref<SymbolicSource> source = arr->source;
+    if (!arr->isConstantArray()) {
+      source = SourceBuilder::alphaModulo(index);
+    }
+    ref<Expr> size = visit(arr->getSize());
+    alphaArrayMap[arr] =
+        arrayCache.CreateArray(size, source, arr->getDomain(), arr->getRange());
+    reverseAlphaArrayMap[alphaArrayMap[arr]] = arr;
+    index++;
+  }
+  return alphaArrayMap[arr];
+}
+
+UpdateList AlphaVersionBuilder::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 AlphaVersionBuilder::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);
+}
+
+AlphaVersionBuilder::AlphaVersionBuilder(ArrayCache &_arrayCache)
+    : arrayCache(_arrayCache) {}
+
+constraints_ty AlphaVersionBuilder::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> AlphaVersionBuilder::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
+  AlphaVersionBuilder.cpp
   APFloatEval.cpp
   ArrayCache.cpp
   ArrayExprOptimizer.cpp

lib/Expr/ExprPPrinter.cpp

@@ -413,6 +413,8 @@ class PPrinter : public ExprPPrinter {
          << " " << s->index;
     } else if (auto s = dyn_cast<IrreproducibleSource>(source)) {
       PC << s->name;
+    } else if (auto s = dyn_cast<AlphaModuloSource>(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 */
@@ -330,6 +332,7 @@ class ParserImpl : public Parser {
   SourceResult ParseLazyInitializationSizeSource();
   SourceResult ParseInstructionSource();
   SourceResult ParseArgumentSource();
+  SourceResult ParseAlphaModuloSource();
 
   /*** Diagnostics ***/
 
@@ -501,6 +504,8 @@ SourceResult ParserImpl::ParseSource() {
   } else if (type == "argument") {
     assert(km);
     source = ParseArgumentSource();
+  } else if (type == "alphaModulo") {
+    source = ParseAlphaModuloSource();
   } else {
     assert(0);
   }
@@ -599,6 +604,12 @@ SourceResult ParserImpl::ParseInstructionSource() {
   return SourceBuilder::instruction(*KI->inst, index, km);
 }
 
+SourceResult ParserImpl::ParseAlphaModuloSource() {
+  auto indexExpr = ParseNumber(64).get();
+  auto index = dyn_cast<ConstantExpr>(indexExpr)->getZExtValue();
+  return SourceBuilder::alphaModulo(index);
+}
+
 /// ParseCommandDecl - Parse a command declaration. The lexer should
 /// be positioned at the opening '('.
 ///

lib/Expr/SourceBuilder.cpp

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