fix: Improve bidirectional memory allocation model

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<Expr> ComposeVisitor::processPointer(ref<Expr> base, ref<Expr> value) {
+  auto trueBase = visit(base)->getValue();
+  auto trueValue = visit(value)->getValue();
+  return PointerExpr::create(trueBase, trueValue);
+}
+
 ref<ObjectState> ComposeVisitor::shareUpdates(ref<ObjectState> os,
                                               const UpdateList &updates) {
   ref<ObjectState> copy(new ObjectState(*os.get()));

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<Expr> processPointer(ref<Expr> base, ref<Expr> value);
   ref<Expr> processRead(const Array *root, const UpdateList &updates,
                         ref<Expr> index, Expr::Width width);
   ref<Expr> processSelect(ref<Expr> cond, ref<Expr> trueExpr,

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;
 }
 

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<ref<const MemoryObject>> localObjects;
+
 private:
   PersistentSet<ref<Target>> prevTargets_;
   PersistentSet<ref<Target>> targets_;

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();
@@ -7380,8 +7381,10 @@ void Executor::lazyInitializeLocalObject(ExecutionState &state, StackFrame &sf,
   ref<const MemoryObject> 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))));
@@ -7390,6 +7393,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,

lib/Core/ObjectManager.h

@@ -116,7 +116,7 @@ class ObjectManager {
   std::vector<Subscriber *> subscribers;
   PForest *processForest;
 
-  InitializerPredicate *predicate;
+  std::unique_ptr<InitializerPredicate> predicate;
 
 public:
   ExecutionState *emptyState;
@@ -164,7 +164,7 @@ class ObjectManager {
   }
 
   void setPredicate(InitializerPredicate *predicate_) {
-    predicate = predicate_;
+    predicate = std::unique_ptr<InitializerPredicate>(predicate_);
   }
 };
 

lib/Solver/BitwuzlaBuilder.cpp

@@ -1113,6 +1113,11 @@ Term BitwuzlaBuilder::constructActual(ref<Expr> 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<PointerExpr>(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();
   }
 }

lib/Solver/MetaSMTBuilder.h

@@ -658,7 +658,7 @@ MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> 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: {

lib/Solver/Z3BitvectorBuilder.cpp

@@ -273,7 +273,8 @@ Z3ASTHandle Z3BitvectorBuilder::constructActual(ref<Expr> e, int *width_out) {
   switch (e->getKind()) {
   case Expr::Pointer:
   case Expr::ConstantPointer: {
-    assert(0 && "unreachable");
+    auto ptrExpr = cast<PointerExpr>(e);
+    return constructActual(ptrExpr->getValue(), width_out);
   }
 
   case Expr::Constant: {

lib/Solver/Z3CoreBuilder.cpp

@@ -206,7 +206,7 @@ Z3ASTHandle Z3CoreBuilder::constructActual(ref<Expr> 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: {

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 <assert.h>
+#include <stdlib.h>
+
+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

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 <assert.h>
+#include <stdlib.h>
+
+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

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 --use-concretizing-solver=false %t.bc 2> %t.log
+// RUN: FileCheck %s -input-file=%t.log
+
+#include "klee/klee.h"
+#include <assert.h>
+#include <stdlib.h>
+
+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

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 --use-concretizing-solver=false %t.bc 2> %t.log
+// RUN: FileCheck %s -input-file=%t.log
+
+#include "klee/klee.h"
+#include <assert.h>
+#include <stdlib.h>
+
+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

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 <assert.h>
+#include <stdlib.h>
+
+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]

test/Bidirectional/Memory/fake-function-pointer-change.c

@@ -0,0 +1,30 @@
+// 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 <assert.h>
+#include <stdlib.h>
+
+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

test/Bidirectional/Memory/fake-stack-pointer-change.c

@@ -0,0 +1,26 @@
+// 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 <assert.h>
+#include <stdlib.h>
+
+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