@@ -533,8 +533,36 @@ void ExprEngine::ctuBifurcate(const CallEvent &Call, const Decl *D,
533533 inlineCall (Engine.getWorkList (), Call, D, Bldr, Pred, State);
534534}
535535
536+ static ProgramStateRef InvalidateBuffer (unsigned blockcount,
537+ ProgramStateRef state, const Expr *E,
538+ SVal V, const LocationContext *LCtx) {
539+ std::optional<Loc> L = V.getAs <Loc>();
540+ if (!L)
541+ return state;
542+
543+ if (std::optional<loc::MemRegionVal> MR = L->getAs <loc::MemRegionVal>()) {
544+
545+ const MemRegion *R = MR->getRegion ()->StripCasts ();
546+
547+ // Are we dealing with an ElementRegion? If so, we should be invalidating
548+ // the super-region.
549+ if (const ElementRegion *ER = dyn_cast<ElementRegion>(R)) {
550+ R = ER->getSuperRegion ();
551+ // FIXME: What about layers of ElementRegions?
552+ }
553+
554+ return state->invalidateRegions (
555+ R, E, blockcount, /* C.blockCount(),*/
556+ /* C.getPredecessor()->getLocationContext(),*/ LCtx, true , nullptr ,
557+ nullptr , nullptr );
558+ }
559+
560+ // If we have a non-region value by chance, just remove the binding.
561+ return state->killBinding (*L);
562+ }
563+
536564// XXX: We only handle pthreads currently
537- #pragma clang optimize off
565+ // #pragma clang optimize off
538566void ExprEngine::threadBifurcate (CallEvent const &Call, Decl const *D,
539567 NodeBuilder &Bldr, ExplodedNode *Pred,
540568 ProgramStateRef State) {
@@ -546,6 +574,9 @@ void ExprEngine::threadBifurcate(CallEvent const &Call, Decl const *D,
546574 */
547575 assert (Call.getNumArgs () == 4 && " pthread_create(3) should have 4 args" );
548576
577+ auto const *SRThreadID = Call.getArgExpr (0 );
578+ assert (SRThreadID && " pthread create should have a thread id parameter" );
579+
549580 // 1. Extract the expr for the thread's start routine
550581 auto const *SRExpr = Call.getArgExpr (2 );
551582 assert (SRExpr && " start_routine should exist" );
@@ -589,24 +620,31 @@ void ExprEngine::threadBifurcate(CallEvent const &Call, Decl const *D,
589620 StartRoutine->getType (),
590621 VK_LValue);
591622
592- auto *null_expr = new (SRR->getContext ()) CXXNullPtrLiteralExpr (QualType (), SourceLocation ());
593623
594624 CallExpr *srcall = CallExpr::Create (
595625 SRR->getContext (),
596626 srexpr,
597- {const_cast <Expr*>(SRInit) /* null_expr */ },
627+ {const_cast <Expr*>(SRInit)},
598628 StartRoutine->getType (),
599629 VK_LValue,
600- SourceLocation (),
601- FPOptionsOverride ());
630+ SourceLocation (),
631+ FPOptionsOverride ());
602632
603633 // TODO: bind the arguments?
604- auto call = CEMgr.getSimpleCall (srcall, State, LC, getCFGElementRef ());
634+ // auto call = CEMgr.getSimpleCall(srcall, State, LC, getCFGElementRef());
635+ auto call = CEMgr.getSimpleCall (srcall, Pred->getState (), Pred->getLocationContext (), getCFGElementRef ());
636+
637+ const auto LCtx = Pred->getLocationContext ();
638+ State = InvalidateBuffer (currBldrCtx->blockCount (), State, Call.getArgExpr (0 ),
639+ // State->getSVal(Call.getArg(0), LCtx),
640+ Call.getArgSVal (0 ), LCtx);
641+
642+ State = State->set <ReplayWithoutInlining>(const_cast <Stmt *>(LC->getStackFrame ()->getCallSite ()));
605643
606644 inlineCall (Engine.getWorkList (), *call, StartRoutine, Bldr, Pred, State);
607- conservativeEvalCall (*call, Bldr, Pred, State);
645+ // conservativeEvalCall(*call, Bldr, Pred, State);
608646}
609- #pragma clang optimize on
647+ // #pragma clang optimize on
610648
611649void ExprEngine::inlineCall (WorkList *WList, const CallEvent &Call,
612650 const Decl *D, NodeBuilder &Bldr,
@@ -674,7 +712,7 @@ static ProgramStateRef getInlineFailedState(ProgramStateRef State,
674712 if (!ReplayState)
675713 return nullptr ;
676714
677- assert (ReplayState == CallE && " Backtracked to the wrong call." );
715+ // assert(ReplayState == CallE && "Backtracked to the wrong call.");
678716 (void )CallE;
679717
680718 return State->remove <ReplayWithoutInlining>();
@@ -1327,12 +1365,11 @@ void ExprEngine::defaultEvalCall(NodeBuilder &Bldr, ExplodedNode *Pred,
13271365 Call->setForeign (RD.isForeign ());
13281366 const Decl *D = RD.getDecl ();
13291367
1330- // TODO: make this a proper mode
13311368 // Special case thread creation
1332- if (isThread (*Call) && Opts. ModelPthreads ) {
1369+ if (Opts. ModelPthreads && isThread (*Call)) {
13331370 llvm::errs () << " Hijacking pthread_create(3)\n " ;
13341371 threadBifurcate (*Call, D, Bldr, Pred, State);
1335- return ;
1372+ // return;
13361373 }
13371374
13381375 if (shouldInlineCall (*Call, D, Pred, CallOpts)) {
0 commit comments