Create alpha-equvalency format solver

.github/workflows/build.yaml

@@ -5,7 +5,7 @@ on:
   pull_request:
     branches: [main, utbot-main]
   push:
-    branches: [main, utbot-main]
+    branches: [main, utbot-main, AlphaEquiv]
 
 # Defaults for building KLEE
 env:

include/klee/Expr/ExprVisitor.h

@@ -10,8 +10,9 @@
 #ifndef KLEE_EXPRVISITOR_H
 #define KLEE_EXPRVISITOR_H
 
+#include "ArrayCache.h"
 #include "ExprHashMap.h"
-
+#include "SourceBuilder.h"
 namespace klee {
 
 class VisitorHash {
@@ -150,6 +151,60 @@ class ExprVisitor {
   ref<Expr> visit(const ref<Expr> &e);
 };
 
+class AlphaVersionBuilder : public ExprVisitor {
+private:
+  ArrayCache arrayCache;
+  ArrayCache::ArrayHashMap<const Array *> alphaArrayMap;
+
+  unsigned index = 0;
+
+  const Array *visitArray(const Array *arr) {
+    if (alphaArrayMap.find(arr) == alphaArrayMap.end()) {
+      ref<SymbolicSource> source = SourceBuilder::alphaModulo(index);
+      ref<Expr> size = visit(arr->getSize());
+
+      alphaArrayMap[arr] = arrayCache.CreateArray(size, source);
+      index++;
+    }
+    return alphaArrayMap[arr];
+  }
+
+  UpdateList visitUpdateList(UpdateList u) {
+    const Array *root = visitArray(u.root);
+    return UpdateList(u.root, u.head);
+    ;
+  }
+
+  Action visitRead(const ReadExpr &re) override {
+    ref<Expr> v = visit(re.index);
+    UpdateList u = visitUpdateList(re.updates);
+    ref<Expr> e = ReadExpr::create(u, v);
+    return Action::changeTo(e);
+  }
+
+public:
+  AlphaVersionBuilder(ArrayCache &_arrayCache) : arrayCache(_arrayCache) {}
+  constraints_ty visitConstraints(constraints_ty cs) {
+    constraints_ty result;
+    for (auto arg : cs) {
+      ref<Expr> v = visit(arg);
+      result.insert(v);
+    }
+    return result;
+  }
+  constraints_ty visitConstraints(constraints_ty cs,
+                                  ExprHashMap<ref<Expr>> &reverse) {
+    constraints_ty result;
+    for (auto arg : cs) {
+      ref<Expr> v = visit(arg);
+      result.insert(v);
+      reverse[v] = arg;
+    }
+    return result;
+  }
+  ref<Expr> visitExpr(ref<Expr> v) { return visit(v); }
+};
+
 } // namespace klee
 
 #endif /* KLEE_EXPRVISITOR_H */

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,13 @@ 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 converse all
+/// independent queries to their alpha versions
+///
+/// \param s - The underlying solver to use.
+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;

include/klee/Solver/SolverUtil.h

@@ -303,13 +303,27 @@ class InvalidResponse : public SolverResponse {
   }
 
   bool satisfies(const std::set<ref<Expr>> &key, bool allowFreeValues = true) {
-    return result.satisfies(key.begin(), key.end(), allowFreeValues);
+    std::set<ref<Expr>> booleanKey;
+    std::set<ref<Expr>> nonBooleanKey;
+
+    for (auto i : key) {
+      if (i->getWidth() == Expr::Bool) {
+        booleanKey.insert(i);
+      } else {
+        nonBooleanKey.insert(i);
+      }
+    }
+
+    return result.satisfies(booleanKey.begin(), booleanKey.end(),
+                            allowFreeValues) &&
+           result.satisfiesNonBoolean(nonBooleanKey.begin(),
+                                      nonBooleanKey.end(), allowFreeValues);
   }
 
-  bool satisfiesNonBoolean(const std::set<ref<Expr>> &key,
+  /*bool satisfiesNonBoolean(const std::set<ref<Expr>> &key,
                            bool allowFreeValues = true) {
     return result.satisfiesNonBoolean(key.begin(), key.end(), allowFreeValues);
-  }
+  }*/
 
   void dump() { result.dump(); }
 

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/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/SourceBuilder.cpp

@@ -86,4 +86,10 @@ ref<SymbolicSource> SourceBuilder::irreproducible(const std::string &name) {
   ref<SymbolicSource> r(new IrreproducibleSource(name + llvm::utostr(++id)));
   r->computeHash();
   return r;
+}
+
+ref<SymbolicSource> SourceBuilder::alphaModulo(int _index) {
+  ref<SymbolicSource> r(new AlphaModuloSource(_index));
+  r->computeHash();
+  return r;
 }