================ @@ -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, ---------------- NagyDonat wrote:
I think a name like `resolveMutexIfPossiblyDestroyed` would be more descriptive. Also, in this patch this is called from only one location; if you don't expect further use, then I think you can simply inline this at that point. 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
