diff options
Diffstat (limited to 'clang-r353983e/include/clang/Analysis/Analyses/ThreadSafetyLogical.h')
| -rw-r--r-- | clang-r353983e/include/clang/Analysis/Analyses/ThreadSafetyLogical.h | 107 |
1 files changed, 107 insertions, 0 deletions
diff --git a/clang-r353983e/include/clang/Analysis/Analyses/ThreadSafetyLogical.h b/clang-r353983e/include/clang/Analysis/Analyses/ThreadSafetyLogical.h new file mode 100644 index 00000000..8d938c1b --- /dev/null +++ b/clang-r353983e/include/clang/Analysis/Analyses/ThreadSafetyLogical.h @@ -0,0 +1,107 @@ +//===- ThreadSafetyLogical.h -----------------------------------*- C++ --*-===// +// +// 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 +// +//===----------------------------------------------------------------------===// +// This file defines a representation for logical expressions with SExpr leaves +// that are used as part of fact-checking capability expressions. +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H +#define LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H + +#include "clang/Analysis/Analyses/ThreadSafetyTIL.h" + +namespace clang { +namespace threadSafety { +namespace lexpr { + +class LExpr { +public: + enum Opcode { + Terminal, + And, + Or, + Not + }; + Opcode kind() const { return Kind; } + + /// Logical implication. Returns true if the LExpr implies RHS, i.e. if + /// the LExpr holds, then RHS must hold. For example, (A & B) implies A. + inline bool implies(const LExpr *RHS) const; + +protected: + LExpr(Opcode Kind) : Kind(Kind) {} + +private: + Opcode Kind; +}; + +class Terminal : public LExpr { + til::SExpr *Expr; + +public: + Terminal(til::SExpr *Expr) : LExpr(LExpr::Terminal), Expr(Expr) {} + + const til::SExpr *expr() const { return Expr; } + til::SExpr *expr() { return Expr; } + + static bool classof(const LExpr *E) { return E->kind() == LExpr::Terminal; } +}; + +class BinOp : public LExpr { + LExpr *LHS, *RHS; + +protected: + BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {} + +public: + const LExpr *left() const { return LHS; } + LExpr *left() { return LHS; } + + const LExpr *right() const { return RHS; } + LExpr *right() { return RHS; } +}; + +class And : public BinOp { +public: + And(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::And) {} + + static bool classof(const LExpr *E) { return E->kind() == LExpr::And; } +}; + +class Or : public BinOp { +public: + Or(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::Or) {} + + static bool classof(const LExpr *E) { return E->kind() == LExpr::Or; } +}; + +class Not : public LExpr { + LExpr *Exp; + +public: + Not(LExpr *Exp) : LExpr(LExpr::Not), Exp(Exp) {} + + const LExpr *exp() const { return Exp; } + LExpr *exp() { return Exp; } + + static bool classof(const LExpr *E) { return E->kind() == LExpr::Not; } +}; + +/// Logical implication. Returns true if LHS implies RHS, i.e. if LHS +/// holds, then RHS must hold. For example, (A & B) implies A. +bool implies(const LExpr *LHS, const LExpr *RHS); + +bool LExpr::implies(const LExpr *RHS) const { + return lexpr::implies(this, RHS); +} + +} +} +} + +#endif + |
