From f75cfb1a0f0218151b6aa5ec2e06651f08adeb42 Mon Sep 17 00:00:00 2001 From: metametamoon Date: Thu, 17 Jul 2025 13:14:39 +0300 Subject: [PATCH 1/6] feat: bidirectional memory proper handling --- lib/Core/Composer.cpp | 11 ++++++ lib/Core/Composer.h | 3 ++ lib/Core/ExecutionState.cpp | 6 +-- lib/Core/ExecutionState.h | 3 ++ lib/Core/Executor.cpp | 12 +++++- lib/Solver/Z3BitvectorBuilder.cpp | 3 +- .../Memory/cond-function-pointer-change-2.c | 36 ++++++++++++++++++ .../Memory/cond-function-pointer-change-3.c | 36 ++++++++++++++++++ .../Memory/cond-function-pointer-change.c | 38 +++++++++++++++++++ .../Memory/cond-stack-pointer-change.c | 34 +++++++++++++++++ .../Memory/double-alloc-call-possible.c | 31 +++++++++++++++ .../Memory/fake-function-pointer-change.c | 33 ++++++++++++++++ .../Memory/fake-stack-pointer-change.c | 29 ++++++++++++++ .../Memory/function-pointer-assign-change.c | 29 ++++++++++++++ .../Memory/function-pointer-change.c | 31 +++++++++++++++ .../Memory/stack-pointer-change-2.c | 38 +++++++++++++++++++ .../Memory/stack-pointer-change.c | 28 ++++++++++++++ 17 files changed, 395 insertions(+), 6 deletions(-) create mode 100644 test/Bidirectional/Memory/cond-function-pointer-change-2.c create mode 100644 test/Bidirectional/Memory/cond-function-pointer-change-3.c create mode 100644 test/Bidirectional/Memory/cond-function-pointer-change.c create mode 100644 test/Bidirectional/Memory/cond-stack-pointer-change.c create mode 100644 test/Bidirectional/Memory/double-alloc-call-possible.c create mode 100644 test/Bidirectional/Memory/fake-function-pointer-change.c create mode 100644 test/Bidirectional/Memory/fake-stack-pointer-change.c create mode 100644 test/Bidirectional/Memory/function-pointer-assign-change.c create mode 100644 test/Bidirectional/Memory/function-pointer-change.c create mode 100644 test/Bidirectional/Memory/stack-pointer-change-2.c create mode 100644 test/Bidirectional/Memory/stack-pointer-change.c diff --git a/lib/Core/Composer.cpp b/lib/Core/Composer.cpp index 975a8ad1e8..9b59d791de 100644 --- a/lib/Core/Composer.cpp +++ b/lib/Core/Composer.cpp @@ -221,6 +221,17 @@ ExprVisitor::Action ComposeVisitor::visitSelect(const SelectExpr &select) { processSelect(select.cond, select.trueExpr, select.falseExpr)); } +ExprVisitor::Action +ComposeVisitor::visitPointer(const PointerExpr &pointerExpr) { + return Action::changeTo(processPointer(pointerExpr.base, pointerExpr.value)); +} + +ref ComposeVisitor::processPointer(ref base, ref value) { + auto trueBase = visit(base)->getValue(); + auto trueValue = visit(value)->getValue(); + return PointerExpr::create(trueBase, trueValue); +} + ref ComposeVisitor::shareUpdates(ref os, const UpdateList &updates) { ref copy(new ObjectState(*os.get())); diff --git a/lib/Core/Composer.h b/lib/Core/Composer.h index c514dbe402..b7cd068c3f 100644 --- a/lib/Core/Composer.h +++ b/lib/Core/Composer.h @@ -200,6 +200,9 @@ class ComposeVisitor : public ExprVisitor { ExprVisitor::Action visitRead(const ReadExpr &) override; ExprVisitor::Action visitConcat(const ConcatExpr &concat) override; ExprVisitor::Action visitSelect(const SelectExpr &) override; + ExprVisitor::Action visitPointer(const PointerExpr &) override; + + ref processPointer(ref base, ref value); ref processRead(const Array *root, const UpdateList &updates, ref index, Expr::Width width); ref processSelect(ref cond, ref trueExpr, diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 3b7cfe4ca7..acf19ba949 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -167,9 +167,9 @@ ExecutionState::ExecutionState(const ExecutionState &state) forkDisabled(state.forkDisabled), isolated(state.isolated), finalComposing(state.finalComposing), returnValue(state.returnValue), gepExprBases(state.gepExprBases), multiplexKF(state.multiplexKF), - prevTargets_(state.prevTargets_), targets_(state.targets_), - prevHistory_(state.prevHistory_), history_(state.history_), - isTargeted_(state.isTargeted_) { + localObjects(state.localObjects), prevTargets_(state.prevTargets_), + targets_(state.targets_), prevHistory_(state.prevHistory_), + history_(state.history_), isTargeted_(state.isTargeted_) { queryMetaData.id = state.id; } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 8e030b5449..3906d642c7 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -405,6 +405,9 @@ class ExecutionState { // Temp: to know which multiplex path this state has taken KFunction *multiplexKF = nullptr; + // set with reads from alloca instructions + std::set> localObjects; + private: PersistentSet> prevTargets_; PersistentSet> targets_; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 9ba03fd78c..cd3c8c3dfa 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -7380,8 +7380,8 @@ void Executor::lazyInitializeLocalObject(ExecutionState &state, StackFrame &sf, ref id = lazyInitializeObject( state, pointer, target, elementSize, size, true, conditionExpr, state.isolated || UseSymbolicSizeLazyInit); - state.addPointerResolution(pointer, id.get()); - state.addPointerResolution(basePointer, id.get()); + // state.addPointerResolution(pointer, id.get()); + // state.addPointerResolution(basePointer, id.get()); state.addConstraint(EqExpr::create(address, id->getBaseExpr())); state.addConstraint( Expr::createIsZero(EqExpr::create(address, Expr::createPointer(0)))); @@ -7390,6 +7390,14 @@ void Executor::lazyInitializeLocalObject(ExecutionState &state, StackFrame &sf, } RefObjectPair op = state.addressSpace.findOrLazyInitializeObject(id.get()); state.addressSpace.bindObject(op.first, op.second.get()); + if (state.localObjects.count(id) == 0) { + for (auto localObject : state.localObjects) { + auto localObjectAddress = localObject->getBaseExpr(); + state.constraints.addConstraint(Expr::createIsZero( + EqExpr::create(id->getBaseExpr(), localObjectAddress))); + } + state.localObjects.insert(id); + } } void Executor::lazyInitializeLocalObject(ExecutionState &state, diff --git a/lib/Solver/Z3BitvectorBuilder.cpp b/lib/Solver/Z3BitvectorBuilder.cpp index 9127f4848d..1a59444091 100644 --- a/lib/Solver/Z3BitvectorBuilder.cpp +++ b/lib/Solver/Z3BitvectorBuilder.cpp @@ -273,7 +273,8 @@ Z3ASTHandle Z3BitvectorBuilder::constructActual(ref e, int *width_out) { switch (e->getKind()) { case Expr::Pointer: case Expr::ConstantPointer: { - assert(0 && "unreachable"); + auto ptrExpr = cast(e); + return constructActual(ptrExpr->getValue(), width_out); } case Expr::Constant: { diff --git a/test/Bidirectional/Memory/cond-function-pointer-change-2.c b/test/Bidirectional/Memory/cond-function-pointer-change-2.c new file mode 100644 index 0000000000..016be8bec6 --- /dev/null +++ b/test/Bidirectional/Memory/cond-function-pointer-change-2.c @@ -0,0 +1,36 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *km, int *kn, int inner_toggle) { + if (inner_toggle == 1) { + *km = 0; + } else { + *kn = 0; + } +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int n = 3; + int toggle; + klee_make_symbolic(&toggle, sizeof(toggle), "toggle"); + klee_assume(toggle == 0 || toggle == 1); + M(&m, &n, toggle); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/cond-function-pointer-change-3.c b/test/Bidirectional/Memory/cond-function-pointer-change-3.c new file mode 100644 index 0000000000..ca13176312 --- /dev/null +++ b/test/Bidirectional/Memory/cond-function-pointer-change-3.c @@ -0,0 +1,36 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *km, int *kn, int inner_toggle) { + if (inner_toggle == 1) { + *km = 0; + } else { + *kn = 0; + } +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int n = 3; + int toggle; + klee_make_symbolic(&toggle, sizeof(toggle), "toggle"); + M(&m, &n, toggle); + klee_assume(toggle == 1); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT diff --git a/test/Bidirectional/Memory/cond-function-pointer-change.c b/test/Bidirectional/Memory/cond-function-pointer-change.c new file mode 100644 index 0000000000..5e6f074e9a --- /dev/null +++ b/test/Bidirectional/Memory/cond-function-pointer-change.c @@ -0,0 +1,38 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *k) { + *k = 0; +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int n = 3; + int toggle; + klee_make_symbolic(&toggle, sizeof(toggle), "toggle"); + klee_assume(toggle == 0 || toggle == 1); + int *ptr; + if (toggle == 0) { + ptr = &m; + } else { + ptr = &n; + } + M(ptr); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/cond-stack-pointer-change.c b/test/Bidirectional/Memory/cond-stack-pointer-change.c new file mode 100644 index 0000000000..5fb1c8c475 --- /dev/null +++ b/test/Bidirectional/Memory/cond-stack-pointer-change.c @@ -0,0 +1,34 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int n = 3; + int toggle; + klee_make_symbolic(&toggle, sizeof(toggle), "toggle"); + klee_assume(toggle == 0 || toggle == 1); + int *ptr; + if (toggle == 0) { + ptr = &m; + } else { + ptr = &n; + } + *ptr = 0; + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/double-alloc-call-possible.c b/test/Bidirectional/Memory/double-alloc-call-possible.c new file mode 100644 index 0000000000..bb2aaa1476 --- /dev/null +++ b/test/Bidirectional/Memory/double-alloc-call-possible.c @@ -0,0 +1,31 @@ +// XFAIL: true +// do not support good symbolic memory currently +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=3 --max-stack-frames=4 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --use-visitor-hash=false --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +int *my_alloca() { + int *a = malloc(sizeof(int)); + return a; +} + +int main() { + int *x = my_alloca(); + int *y = my_alloca(); + if (y != x) { + reach_error(); + } + free(x); + free(y); +} + +// CHECK: [TRUE POSITIVE] diff --git a/test/Bidirectional/Memory/fake-function-pointer-change.c b/test/Bidirectional/Memory/fake-function-pointer-change.c new file mode 100644 index 0000000000..c5f8f2c13b --- /dev/null +++ b/test/Bidirectional/Memory/fake-function-pointer-change.c @@ -0,0 +1,33 @@ +// checks that symbolic memory works in bidirectional mode +// it does not; requires a fix + +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *k) { + *k = 0; +} + +int main() { + int m; + int n = 4; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int *ptr = &n; + M(ptr); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/fake-stack-pointer-change.c b/test/Bidirectional/Memory/fake-stack-pointer-change.c new file mode 100644 index 0000000000..3c4d6accf8 --- /dev/null +++ b/test/Bidirectional/Memory/fake-stack-pointer-change.c @@ -0,0 +1,29 @@ +// checks that symbolic memory works in bidirectional mode +// it does not; requires a fix + +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +int main() { + int m; + int n = 4; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int *ptr = &n; + *ptr = 0; + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/function-pointer-assign-change.c b/test/Bidirectional/Memory/function-pointer-assign-change.c new file mode 100644 index 0000000000..e48e65f868 --- /dev/null +++ b/test/Bidirectional/Memory/function-pointer-assign-change.c @@ -0,0 +1,29 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *k) { + *k = 0; +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int *ptr = &m; + M(ptr); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT diff --git a/test/Bidirectional/Memory/function-pointer-change.c b/test/Bidirectional/Memory/function-pointer-change.c new file mode 100644 index 0000000000..5922b015c8 --- /dev/null +++ b/test/Bidirectional/Memory/function-pointer-change.c @@ -0,0 +1,31 @@ +// checks that symbolic memory works in bidirectional mode +// it does not; requires a fix + +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *k) { + *k = 0; +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + M(&m); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT diff --git a/test/Bidirectional/Memory/stack-pointer-change-2.c b/test/Bidirectional/Memory/stack-pointer-change-2.c new file mode 100644 index 0000000000..b233110fa8 --- /dev/null +++ b/test/Bidirectional/Memory/stack-pointer-change-2.c @@ -0,0 +1,38 @@ +// checks that symbolic memory works in bidirectional mode +// it does not; requires a fix + +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void f() { + int n = 0; +} + +int main() { + int m; + int *n = &m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int k; + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k == 0); + f(); + if (k == 0) { + *n = 0; + } + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT diff --git a/test/Bidirectional/Memory/stack-pointer-change.c b/test/Bidirectional/Memory/stack-pointer-change.c new file mode 100644 index 0000000000..e2b19b8fd4 --- /dev/null +++ b/test/Bidirectional/Memory/stack-pointer-change.c @@ -0,0 +1,28 @@ +// checks that symbolic memory works in bidirectional mode +// it does not; requires a fix + +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(0 < m && m < 10000); + int *ptr = &m; + *ptr = 0; + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT From 9dad05bf66064459df869acb24bf4fc3e037ed53 Mon Sep 17 00:00:00 2001 From: metametamoon Date: Fri, 18 Jul 2025 15:25:27 +0300 Subject: [PATCH 2/6] fix: handling pointers in bitwuzla builder --- lib/Solver/BitwuzlaBuilder.cpp | 7 ++++++- test/Bidirectional/Memory/cond-function-pointer-change.c | 2 +- test/Bidirectional/Memory/cond-stack-pointer-change.c | 2 +- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp index b39f23eddd..c8ef69d98f 100644 --- a/lib/Solver/BitwuzlaBuilder.cpp +++ b/lib/Solver/BitwuzlaBuilder.cpp @@ -1113,6 +1113,11 @@ Term BitwuzlaBuilder::constructActual(ref e, int *width_out) { assert(*width_out != 1 && "uncanonicalized FNeg"); return ctx->mk_term(Kind::FP_NEG, {arg}); } + case Expr::Pointer: + case Expr::ConstantPointer: { + PointerExpr *pointerExpr = cast(e); + return constructActual(pointerExpr->getValue(), width_out); + }; // unused due to canonicalization #if 0 @@ -1124,7 +1129,7 @@ case Expr::Sge: #endif default: - assert(0 && "unhandled Expr type"); + klee_error("unhandled Expr type"); return getTrue(); } } diff --git a/test/Bidirectional/Memory/cond-function-pointer-change.c b/test/Bidirectional/Memory/cond-function-pointer-change.c index 5e6f074e9a..c84236279d 100644 --- a/test/Bidirectional/Memory/cond-function-pointer-change.c +++ b/test/Bidirectional/Memory/cond-function-pointer-change.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward --use-concretizing-solver=false %t.bc 2> %t.log // RUN: FileCheck %s -input-file=%t.log #include "klee/klee.h" diff --git a/test/Bidirectional/Memory/cond-stack-pointer-change.c b/test/Bidirectional/Memory/cond-stack-pointer-change.c index 5fb1c8c475..b3bc698949 100644 --- a/test/Bidirectional/Memory/cond-stack-pointer-change.c +++ b/test/Bidirectional/Memory/cond-stack-pointer-change.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward --use-concretizing-solver=false %t.bc 2> %t.log // RUN: FileCheck %s -input-file=%t.log #include "klee/klee.h" From c17922effab2f1417918654cb4f591f5db4e60ab Mon Sep 17 00:00:00 2001 From: metametamoon Date: Wed, 23 Jul 2025 14:23:58 +0300 Subject: [PATCH 3/6] fix: memory leak in bidirectional --- lib/Core/Executor.cpp | 1 + lib/Core/ObjectManager.h | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index cd3c8c3dfa..e236ed1118 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -5391,6 +5391,7 @@ void Executor::run(ExecutionState *initialState, } else if (ExecutionMode == ExecutionKind::Bidirectional) { InitializerPredicate *predicate = new TraceVerifyPredicate( data.specialPoints, *codeGraphInfo.get(), InitializeInJoinBlocks); + // object manager assumes ownership over predicate objectManager->setPredicate(predicate); auto initializer = createIsolatedStatesInitializer(predicate, data); isolatedStatesInitializer = initializer.get(); diff --git a/lib/Core/ObjectManager.h b/lib/Core/ObjectManager.h index 241be1138d..00c5f7538e 100644 --- a/lib/Core/ObjectManager.h +++ b/lib/Core/ObjectManager.h @@ -116,7 +116,7 @@ class ObjectManager { std::vector subscribers; PForest *processForest; - InitializerPredicate *predicate; + std::unique_ptr predicate; public: ExecutionState *emptyState; @@ -164,7 +164,7 @@ class ObjectManager { } void setPredicate(InitializerPredicate *predicate_) { - predicate = predicate_; + predicate = std::unique_ptr(predicate_); } }; From f21b11ee90d4455480b031298bc0654342b172f1 Mon Sep 17 00:00:00 2001 From: metametamoon Date: Thu, 24 Jul 2025 16:01:13 +0300 Subject: [PATCH 4/6] fix: pointer handling in solvers --- lib/Solver/MetaSMTBuilder.h | 2 +- lib/Solver/Z3CoreBuilder.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index aa32b70b05..8cda0a93ad 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -658,7 +658,7 @@ MetaSMTBuilder::constructActual(ref e, int *width_out) { switch (e->getKind()) { case Expr::Pointer: case Expr::ConstantPointer: { - assert(0 && "unreachable"); + return constructActual(e->getValue(), width_out); } case Expr::Constant: { diff --git a/lib/Solver/Z3CoreBuilder.cpp b/lib/Solver/Z3CoreBuilder.cpp index 74bf166e3a..e131070d0d 100644 --- a/lib/Solver/Z3CoreBuilder.cpp +++ b/lib/Solver/Z3CoreBuilder.cpp @@ -206,7 +206,7 @@ Z3ASTHandle Z3CoreBuilder::constructActual(ref e, int *width_out) { switch (e->getKind()) { case Expr::Pointer: case Expr::ConstantPointer: { - assert(0 && "unreachable"); + return constructActual(e->getValue(), width_out); } case Expr::Constant: { From 1cd51d7a64a583594ed9c1ddce4fe4765efeba43 Mon Sep 17 00:00:00 2001 From: metametamoon Date: Thu, 24 Jul 2025 16:06:44 +0300 Subject: [PATCH 5/6] fix: test headers --- test/Bidirectional/Memory/fake-function-pointer-change.c | 3 --- test/Bidirectional/Memory/fake-stack-pointer-change.c | 3 --- test/Bidirectional/Memory/function-pointer-change.c | 3 --- test/Bidirectional/Memory/stack-pointer-change-2.c | 4 +--- 4 files changed, 1 insertion(+), 12 deletions(-) diff --git a/test/Bidirectional/Memory/fake-function-pointer-change.c b/test/Bidirectional/Memory/fake-function-pointer-change.c index c5f8f2c13b..6e6fbcdc39 100644 --- a/test/Bidirectional/Memory/fake-function-pointer-change.c +++ b/test/Bidirectional/Memory/fake-function-pointer-change.c @@ -1,6 +1,3 @@ -// checks that symbolic memory works in bidirectional mode -// it does not; requires a fix - // RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log diff --git a/test/Bidirectional/Memory/fake-stack-pointer-change.c b/test/Bidirectional/Memory/fake-stack-pointer-change.c index 3c4d6accf8..0aaf5e9720 100644 --- a/test/Bidirectional/Memory/fake-stack-pointer-change.c +++ b/test/Bidirectional/Memory/fake-stack-pointer-change.c @@ -1,6 +1,3 @@ -// checks that symbolic memory works in bidirectional mode -// it does not; requires a fix - // RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log diff --git a/test/Bidirectional/Memory/function-pointer-change.c b/test/Bidirectional/Memory/function-pointer-change.c index 5922b015c8..00dd9b5c0d 100644 --- a/test/Bidirectional/Memory/function-pointer-change.c +++ b/test/Bidirectional/Memory/function-pointer-change.c @@ -1,6 +1,3 @@ -// checks that symbolic memory works in bidirectional mode -// it does not; requires a fix - // RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log diff --git a/test/Bidirectional/Memory/stack-pointer-change-2.c b/test/Bidirectional/Memory/stack-pointer-change-2.c index b233110fa8..3b67520ac1 100644 --- a/test/Bidirectional/Memory/stack-pointer-change-2.c +++ b/test/Bidirectional/Memory/stack-pointer-change-2.c @@ -1,6 +1,4 @@ -// checks that symbolic memory works in bidirectional mode -// it does not; requires a fix - +// REQUIRES: not-metasmt // RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log From aed34c7b80a60e3a2da9394095eabc52c07f69d1 Mon Sep 17 00:00:00 2001 From: metametamoon Date: Tue, 29 Jul 2025 10:45:00 +0300 Subject: [PATCH 6/6] fix: caching pointer resolutions wherever safe (in not isolated states) --- lib/Core/Executor.cpp | 6 ++++-- .../2023-02-01-replay-test-with-lazy-initialized-objects.c | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e236ed1118..a4e7c127b5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -7381,8 +7381,10 @@ void Executor::lazyInitializeLocalObject(ExecutionState &state, StackFrame &sf, ref id = lazyInitializeObject( state, pointer, target, elementSize, size, true, conditionExpr, state.isolated || UseSymbolicSizeLazyInit); - // state.addPointerResolution(pointer, id.get()); - // state.addPointerResolution(basePointer, id.get()); + if (!state.isolated) { + state.addPointerResolution(pointer, id.get()); + state.addPointerResolution(basePointer, id.get()); + } state.addConstraint(EqExpr::create(address, id->getBaseExpr())); state.addConstraint( Expr::createIsZero(EqExpr::create(address, Expr::createPointer(0)))); diff --git a/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c b/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c index 500b9febc3..6849ace74d 100644 --- a/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c +++ b/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c @@ -1,4 +1,4 @@ -// REQUIRES: not-darwin +// REQUIRES: not-darwin, posix // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --libc=klee --posix-runtime --skip-not-lazy-initialized --min-number-elements-li=4 %t.bc > %t.log