diff --git a/include/klee/Expr/AlphaBuilder.h b/include/klee/Expr/AlphaBuilder.h index 79c09bf457..9095c489e2 100644 --- 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 build(ref v); + const Array *buildArray(const Array *arr) { return visitArray(arr); } }; } // namespace klee diff --git a/lib/Solver/AlphaEquivalenceSolver.cpp b/lib/Solver/AlphaEquivalenceSolver.cpp index b8e5e1f8b7..2c5df35fdb 100644 --- a/lib/Solver/AlphaEquivalenceSolver.cpp +++ b/lib/Solver/AlphaEquivalenceSolver.cpp @@ -57,7 +57,7 @@ class AlphaEquivalenceSolver : public SolverImpl { const ExprHashMap> &reverse); std::vector changeVersion(const std::vector &objects, - const ArrayCache::ArrayHashMap &reverse); + AlphaBuilder &builder); Assignment changeVersion(const std::vector &objects, const std::vector> &values, @@ -99,14 +99,12 @@ Assignment AlphaEquivalenceSolver::changeVersion( return Assignment(reverseObjects, reverseValues); } -std::vector AlphaEquivalenceSolver::changeVersion( - const std::vector &objects, - const ArrayCache::ArrayHashMap &reverse) { +std::vector +AlphaEquivalenceSolver::changeVersion(const std::vector &objects, + AlphaBuilder &builder) { std::vector 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 alphaQueryExpr = builder.build(query.expr); - const std::vector newObjects = - changeVersion(objects, builder.alphaArrayMap); + const std::vector 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 new file mode 100644 index 0000000000..def7647d8c --- /dev/null +++ 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 + +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; +}