diff options
| -rw-r--r-- | include/klee/Expr/ArrayExprVisitor.h | 2 | ||||
| -rw-r--r-- | lib/Expr/ArrayExprVisitor.cpp | 20 | ||||
| -rw-r--r-- | test/ArrayOpt/test_multindex_multarray.c | 46 |
3 files changed, 55 insertions, 13 deletions
diff --git a/include/klee/Expr/ArrayExprVisitor.h b/include/klee/Expr/ArrayExprVisitor.h index 28f485d9..b2941e42 100644 --- a/include/klee/Expr/ArrayExprVisitor.h +++ b/include/klee/Expr/ArrayExprVisitor.h @@ -35,8 +35,6 @@ class ConstantArrayExprVisitor : public ExprVisitor { private: using bindings_ty = std::map<const Array *, std::vector<ref<Expr>>>; bindings_ty &arrays; - // Avoids adding the same index twice - std::unordered_set<unsigned> addedIndexes; bool incompatible; protected: diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp index 0965308a..cf0da7f6 100644 --- a/lib/Expr/ArrayExprVisitor.cpp +++ b/lib/Expr/ArrayExprVisitor.cpp @@ -73,18 +73,16 @@ ExprVisitor::Action ConstantArrayExprVisitor::visitRead(const ReadExpr &re) { } IndexCompatibilityExprVisitor compatible; compatible.visit(re.index); - if (compatible.isCompatible() && - addedIndexes.find(re.index.get()->hash()) == addedIndexes.end()) { - if (arrays.find(re.updates.root) == arrays.end()) { - arrays.insert( - std::make_pair(re.updates.root, std::vector<ref<Expr> >())); - } else { - // Another possible index to resolve, currently unsupported - incompatible = true; - return Action::skipChildren(); + if (compatible.isCompatible()) { + if (arrays.count(re.updates.root) > 0) { + const auto &indices = arrays[re.updates.root]; + if (!indices.empty() && indices.front() != re.index) { + // Another possible index to resolve, currently unsupported + incompatible = true; + return Action::skipChildren(); + } } - arrays.find(re.updates.root)->second.push_back(re.index); - addedIndexes.insert(re.index.get()->hash()); + arrays[re.updates.root].push_back(re.index); } else if (compatible.hasInnerReads()) { // This Read has an inner Read, we want to optimize the inner one // to create a cascading effect during assignment evaluation diff --git a/test/ArrayOpt/test_multindex_multarray.c b/test/ArrayOpt/test_multindex_multarray.c new file mode 100644 index 00000000..54e91f48 --- /dev/null +++ b/test/ArrayOpt/test_multindex_multarray.c @@ -0,0 +1,46 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=index %t.bc > %t.log 2>&1 +// RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful +// CHECK-CONST_ARR: const_arr + +#include "klee/klee.h" +#include <stdio.h> + +char array1[5] = {0, 1, 2, 3, 4}; +char array2[5] = {0, 1, 2, 3, 4}; + +int main() { + unsigned k; + unsigned x; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x < 5); + + // CHECK: Yes + if ((array1[k] + array2[x] + array2[k]) - 7 == 0) + printf("Yes\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} |