Analysis/Analyses/ThreadSafetyLogical.h

0001 //===- ThreadSafetyLogical.h -----------------------------------*- C++ --*-===//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008 // This file defines a representation for logical expressions with SExpr leaves
0009 // that are used as part of fact-checking capability expressions.
0010 //===----------------------------------------------------------------------===//
0011
0012 #ifndef LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H
0013 #define LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H
0014
0015 #include "clang/Analysis/Analyses/ThreadSafetyTIL.h"
0016
0017 namespace clang {
0018 namespace threadSafety {
0019 namespace lexpr {
0020
0021 class LExpr {
0022 public:
0023   enum Opcode {
0024     Terminal,
0025     And,
0026     Or,
0027     Not
0028   };
0029   Opcode kind() const { return Kind; }
0030
0031   /// Logical implication. Returns true if the LExpr implies RHS, i.e. if
0032   /// the LExpr holds, then RHS must hold. For example, (A & B) implies A.
0033   inline bool implies(const LExpr *RHS) const;
0034
0035 protected:
0036   LExpr(Opcode Kind) : Kind(Kind) {}
0037
0038 private:
0039   Opcode Kind;
0040 };
0041
0042 class Terminal : public LExpr {
0043   til::SExpr *Expr;
0044
0045 public:
0046   Terminal(til::SExpr *Expr) : LExpr(LExpr::Terminal), Expr(Expr) {}
0047
0048   const til::SExpr *expr() const { return Expr; }
0049   til::SExpr *expr() { return Expr; }
0050
0051   static bool classof(const LExpr *E) { return E->kind() == LExpr::Terminal; }
0052 };
0053
0054 class BinOp : public LExpr {
0055   LExpr *LHS, *RHS;
0056
0057 protected:
0058   BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {}
0059
0060 public:
0061   const LExpr *left() const { return LHS; }
0062   LExpr *left() { return LHS; }
0063
0064   const LExpr *right() const { return RHS; }
0065   LExpr *right() { return RHS; }
0066 };
0067
0068 class And : public BinOp {
0069 public:
0070   And(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::And) {}
0071
0072   static bool classof(const LExpr *E) { return E->kind() == LExpr::And; }
0073 };
0074
0075 class Or : public BinOp {
0076 public:
0077   Or(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::Or) {}
0078
0079   static bool classof(const LExpr *E) { return E->kind() == LExpr::Or; }
0080 };
0081
0082 class Not : public LExpr {
0083   LExpr *Exp;
0084
0085 public:
0086   Not(LExpr *Exp) : LExpr(LExpr::Not), Exp(Exp) {}
0087
0088   const LExpr *exp() const { return Exp; }
0089   LExpr *exp() { return Exp; }
0090
0091   static bool classof(const LExpr *E) { return E->kind() == LExpr::Not; }
0092 };
0093
0094 /// Logical implication. Returns true if LHS implies RHS, i.e. if LHS
0095 /// holds, then RHS must hold. For example, (A & B) implies A.
0096 bool implies(const LExpr *LHS, const LExpr *RHS);
0097
0098 bool LExpr::implies(const LExpr *RHS) const {
0099   return lexpr::implies(this, RHS);
0100 }
0101
0102 }
0103 }
0104 }
0105
0106 #endif
0107