fix: Improve bidirectional memory allocation model (#205)

* feat: bidirectional memory proper handling

* fix: handling pointers in bitwuzla builder

* fix: memory leak in bidirectional

* fix: pointer handling in solvers

* fix: test headers

* fix: caching pointer resolutions wherever safe
(in not isolated states)

Author: metametamoon

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: {