================
@@ -0,0 +1,169 @@
+//===--- MutexModelingGDM.h - Modeling of mutexes in GDM ------------------===//
+//
+// 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 the GDM definitions for tracking mutex states.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELINGGDM_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CHECKERS_MUTEXMODELINGGDM_H
+
+#include "MutexModelingDomain.h"
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include "llvm/ADT/FoldingSet.h"
+
+// GDM-related handle-types for tracking mutex states.
+namespace clang {
+namespace ento {
+namespace mutex_modeling {
+
+// Raw data of the mutex events.
+class MutexEvents {};
+using MutexEventsTy = llvm::ImmutableList<EventMarker>;
+
+// Aggregated data structures for tracking critical sections.
+class CritSections {};
+using CritSectionsTy = llvm::ImmutableList<CritSectionMarker>;
+
+// Aggregated data structures for tracking mutex states.
+class LockStates {};
+using LockStatesTy = llvm::ImmutableMap<const MemRegion *, LockStateKind>;
+
+// Tracks return values of destroy operations for potentially destroyed mutexes
+class DestroyedRetVals {};
+using DestroyedRetValsTy = llvm::ImmutableMap<const MemRegion *, SymbolRef>;
+
+} // namespace mutex_modeling
+} // namespace ento
+} // namespace clang
+
+// Enable usage of mutex modeling data structures in llvm::FoldingSet.
+namespace llvm {
+// Specialization for EventMarker to allow its use in FoldingSet
+template <> struct FoldingSetTrait<clang::ento::mutex_modeling::EventMarker> {
+ static void Profile(const clang::ento::mutex_modeling::EventMarker &EM,
+ llvm::FoldingSetNodeID &ID) {
+ ID.Add(EM.Kind);
+ ID.Add(EM.Library);
+ ID.Add(EM.Semantics);
+ ID.Add(EM.EventII);
+ ID.Add(EM.EventExpr);
+ ID.Add(EM.MutexRegion);
+ }
+};
+
+// Specialization for CritSectionMarker to allow its use in FoldingSet
+template <>
+struct FoldingSetTrait<clang::ento::mutex_modeling::CritSectionMarker> {
+ static void Profile(const clang::ento::mutex_modeling::CritSectionMarker &CSM,
+ llvm::FoldingSetNodeID &ID) {
+ ID.Add(CSM.BeginExpr);
+ ID.Add(CSM.MutexRegion);
+ }
+};
+} // namespace llvm
+
+// Iterator traits for ImmutableList and ImmutableMap data structures
+// that enable the use of STL algorithms.
+namespace std {
+// These specializations allow the use of STL algorithms with our custom data
+// structures
+// TODO: Move these to llvm::ImmutableList when overhauling immutable data
+// structures for proper iterator concept support.
+template <>
+struct iterator_traits<typename llvm::ImmutableList<
+ clang::ento::mutex_modeling::EventMarker>::iterator> {
+ using iterator_category = std::forward_iterator_tag;
+ using value_type = clang::ento::mutex_modeling::EventMarker;
+ using difference_type = std::ptrdiff_t;
+ using reference = clang::ento::mutex_modeling::EventMarker &;
+ using pointer = clang::ento::mutex_modeling::EventMarker *;
+};
+template <>
+struct iterator_traits<typename llvm::ImmutableList<
+ clang::ento::mutex_modeling::CritSectionMarker>::iterator> {
+ using iterator_category = std::forward_iterator_tag;
+ using value_type = clang::ento::mutex_modeling::CritSectionMarker;
+ using difference_type = std::ptrdiff_t;
+ using reference = clang::ento::mutex_modeling::CritSectionMarker &;
+ using pointer = clang::ento::mutex_modeling::CritSectionMarker *;
+};
+template <>
+struct iterator_traits<typename llvm::ImmutableMap<
+ const clang::ento::MemRegion *,
+ clang::ento::mutex_modeling::LockStateKind>::iterator> {
+ using iterator_category = std::forward_iterator_tag;
+ using value_type = std::pair<const clang::ento::MemRegion *,
+ clang::ento::mutex_modeling::LockStateKind>;
+ using difference_type = std::ptrdiff_t;
+ using reference = std::pair<const clang::ento::MemRegion *,
+ clang::ento::mutex_modeling::LockStateKind> &;
+ using pointer = std::pair<const clang::ento::MemRegion *,
+ clang::ento::mutex_modeling::LockStateKind> *;
+};
+template <>
+struct iterator_traits<typename llvm::ImmutableMap<
+ const clang::ento::MemRegion *, clang::ento::SymbolRef>::iterator> {
+ using iterator_category = std::forward_iterator_tag;
+ using value_type =
+ std::pair<const clang::ento::MemRegion *, clang::ento::SymbolRef>;
+ using difference_type = std::ptrdiff_t;
+ using reference =
+ std::pair<const clang::ento::MemRegion *, clang::ento::SymbolRef> &;
+ using pointer =
+ std::pair<const clang::ento::MemRegion *, clang::ento::SymbolRef> *;
+};
+} // namespace std
+
+// NOTE: ProgramState macros are not used here, because the visibility of these
+// GDM entries must span multiple translation units (multiple checkers).
+// TODO: check if this is still true after finishing the implementation.
----------------
NagyDonat wrote:
Another alternative would be placing these in a single translation unit (`MutexModeling.cpp`) and introducing some externally visible boilerplate functions that wrap their operations that need to be seen from outside. I don't know if this would be better or worse than your current solution where you expose and duplicate the internals of the state trait macros.
https://github.com/llvm/llvm-project/pull/111381