[fix] Fix AlphaEquivalenceSolver

UnitTestBot · Oct 27, 2023 · 0cb981d · 0cb981d
1 parent 200db1d
commit 0cb981d
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 9 deletions.
diff --git a/include/klee/Expr/AlphaBuilder.h b/include/klee/Expr/AlphaBuilder.h
@@ -35,6 +35,7 @@ class AlphaBuilder final : public ExprVisitor {
   AlphaBuilder(ArrayCache &_arrayCache);
   constraints_ty visitConstraints(constraints_ty cs);
   ref<Expr> build(ref<Expr> v);
+  const Array *buildArray(const Array *arr) { return visitArray(arr); }
 };
 
 } // namespace klee

diff --git a/lib/Solver/AlphaEquivalenceSolver.cpp b/lib/Solver/AlphaEquivalenceSolver.cpp
@@ -57,7 +57,7 @@ class AlphaEquivalenceSolver : public SolverImpl {
                              const ExprHashMap<ref<Expr>> &reverse);
   std::vector<const Array *>
   changeVersion(const std::vector<const Array *> &objects,
-                const ArrayCache::ArrayHashMap<const Array *> &reverse);
+                AlphaBuilder &builder);
   Assignment
   changeVersion(const std::vector<const Array *> &objects,
                 const std::vector<SparseStorage<unsigned char>> &values,
@@ -99,14 +99,12 @@ Assignment AlphaEquivalenceSolver::changeVersion(
   return Assignment(reverseObjects, reverseValues);
 }
 
-std::vector<const Array *> AlphaEquivalenceSolver::changeVersion(
-    const std::vector<const Array *> &objects,
-    const ArrayCache::ArrayHashMap<const Array *> &reverse) {
+std::vector<const Array *>
+AlphaEquivalenceSolver::changeVersion(const std::vector<const Array *> &objects,
+                                      AlphaBuilder &builder) {
   std::vector<const Array *> reverseObjects;
   for (size_t i = 0; i < objects.size(); i++) {
-    if (reverse.count(objects.at(i)) != 0) {
-      reverseObjects.push_back(reverse.at(objects.at(i)));
-    }
+    reverseObjects.push_back(builder.buildArray(objects.at(i)));
   }
   return reverseObjects;
 }
@@ -187,8 +185,7 @@ bool AlphaEquivalenceSolver::computeInitialValues(
   AlphaBuilder builder(arrayCache);
   constraints_ty alphaQuery = builder.visitConstraints(query.constraints.cs());
   ref<Expr> alphaQueryExpr = builder.build(query.expr);
-  const std::vector<const Array *> newObjects =
-      changeVersion(objects, builder.alphaArrayMap);
+  const std::vector<const Array *> newObjects = changeVersion(objects, builder);
 
   if (!solver->impl->computeInitialValues(
           Query(ConstraintSet(alphaQuery, {}, {}), alphaQueryExpr, query.id),

diff --git a/test/regression/2023-27-10-SimpleComparison.c b/test/regression/2023-27-10-SimpleComparison.c
@@ -0,0 +1,21 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --debug-assignment-validating-solver=false --use-fast-cex-solver=false --use-cex-cache=false --use-branch-cache=false --use-alpha-equivalence=true --use-independent-solver=false --use-concretizing-solver=false --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --use-guided-search=none %t.bc
+
+#include <assert.h>
+
+struct Node {
+  int *x;
+};
+
+int main() {
+  struct Node *nodeA;
+  struct Node *nodeB;
+  klee_make_symbolic(&nodeA, sizeof(nodeA), "nodeA");
+  klee_make_symbolic(&nodeB, sizeof(nodeB), "nodeB");
+
+  if (nodeA && nodeB && nodeA == nodeB && (*nodeA->x * 2) != (*nodeA->x + *nodeB->x)) {
+    assert(0);
+  }
+  return 0;
+}