================ @@ -0,0 +1,773 @@ +//===--- MutexModeling.cpp - Modeling of mutexes --------------------------===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// Defines modeling checker for tracking mutex states. +// +//===----------------------------------------------------------------------===// + +#include "MutexModeling/MutexModelingAPI.h" +#include "MutexModeling/MutexModelingDomain.h" +#include "MutexModeling/MutexRegionExtractor.h" + +#include "clang/StaticAnalyzer/Core/Checker.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h" +#include "clang/StaticAnalyzer/Frontend/CheckerRegistry.h" +#include <memory> + +using namespace clang; +using namespace ento; +using namespace mutex_modeling; + +namespace { + +// When a lock is destroyed, in some semantics(like PthreadSemantics) we are not +// sure if the destroy call has succeeded or failed, and the lock enters one of +// the 'possibly destroyed' state. There is a short time frame for the +// programmer to check the return value to see if the lock was successfully +// destroyed. Before we model the next operation over that lock, we call this +// function to see if the return value was checked by now and set the lock state +// - either to destroyed state or back to its previous state. + +// In PthreadSemantics, pthread_mutex_destroy() returns zero if the lock is +// successfully destroyed and it returns a non-zero value otherwise. +ProgramStateRef resolvePossiblyDestroyedMutex(ProgramStateRef State, + const MemRegion *LockReg, + const SymbolRef *LockReturnSym) { + const LockStateKind *LockState = State->get<LockStates>(LockReg); + // Existence in DestroyRetVal ensures existence in LockMap. + // Existence in Destroyed also ensures that the lock state for lockR is either + // UntouchedAndPossiblyDestroyed or UnlockedAndPossiblyDestroyed. + assert(LockState); + assert(*LockState == LockStateKind::UntouchedAndPossiblyDestroyed || + *LockState == LockStateKind::UnlockedAndPossiblyDestroyed); + + ConstraintManager &CMgr = State->getConstraintManager(); + ConditionTruthVal RetZero = CMgr.isNull(State, *LockReturnSym); + if (RetZero.isConstrainedFalse()) { + switch (*LockState) { + case LockStateKind::UntouchedAndPossiblyDestroyed: { + State = State->remove<LockStates>(LockReg); + break; + } + case LockStateKind::UnlockedAndPossiblyDestroyed: { + State = State->set<LockStates>(LockReg, LockStateKind::Unlocked); + break; + } + default: + llvm_unreachable("Unknown lock state for a lock inside DestroyRetVal"); + } + } else { + State = State->set<LockStates>(LockReg, LockStateKind::Destroyed); + } + + // Removing the map entry (LockReg, sym) from DestroyRetVal as the lock + // state is now resolved. + return State->remove<DestroyedRetVals>(LockReg); +} + +ProgramStateRef doResolvePossiblyDestroyedMutex(ProgramStateRef State, + const MemRegion *MTX) { + assert(MTX && "should only be called with a mutex region"); + + if (const SymbolRef *Sym = State->get<DestroyedRetVals>(MTX)) + return resolvePossiblyDestroyedMutex(State, MTX, Sym); + return State; +} + +class MutexModeling : public Checker<check::PostCall, check::DeadSymbols, + check::RegionChanges> { +public: + void checkPostCall(const CallEvent &Call, CheckerContext &C) const; + + void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const; + + ProgramStateRef + checkRegionChanges(ProgramStateRef State, const InvalidatedSymbols *Symbols, + ArrayRef<const MemRegion *> ExplicitRegions, + ArrayRef<const MemRegion *> Regions, + const LocationContext *LCtx, const CallEvent *Call) const; + +private: + mutable std::unique_ptr<BugType> BT_initlock; + + // When handling events, NoteTags can be placed on ProgramPoints. This struct + // supports returning both the resulting ProgramState and a NoteTag. + struct ModelingResult { + ProgramStateRef State; + const NoteTag *Note = nullptr; + }; ---------------- NagyDonat wrote:
This is a nice little struct, I like it :) https://github.com/llvm/llvm-project/pull/111381 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
