1 //===- ThreadSafetyLogical.h -----------------------------------*- C++ --*-===// 2 // 3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4 // See https://llvm.org/LICENSE.txt for license information. 5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6 // 7 //===----------------------------------------------------------------------===// 8 // This file defines a representation for logical expressions with SExpr leaves 9 // that are used as part of fact-checking capability expressions. 10 //===----------------------------------------------------------------------===// 11 12 #ifndef LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H 13 #define LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H 14 15 #include "clang/Analysis/Analyses/ThreadSafetyTIL.h" 16 17 namespace clang { 18 namespace threadSafety { 19 namespace lexpr { 20 21 class LExpr { 22 public: 23 enum Opcode { 24 Terminal, 25 And, 26 Or, 27 Not 28 }; 29 Opcode kind() const { return Kind; } 30 31 /// Logical implication. Returns true if the LExpr implies RHS, i.e. if 32 /// the LExpr holds, then RHS must hold. For example, (A & B) implies A. 33 inline bool implies(const LExpr *RHS) const; 34 35 protected: 36 LExpr(Opcode Kind) : Kind(Kind) {} 37 38 private: 39 Opcode Kind; 40 }; 41 42 class Terminal : public LExpr { 43 til::SExpr *Expr; 44 45 public: 46 Terminal(til::SExpr *Expr) : LExpr(LExpr::Terminal), Expr(Expr) {} 47 48 const til::SExpr *expr() const { return Expr; } 49 til::SExpr *expr() { return Expr; } 50 51 static bool classof(const LExpr *E) { return E->kind() == LExpr::Terminal; } 52 }; 53 54 class BinOp : public LExpr { 55 LExpr *LHS, *RHS; 56 57 protected: 58 BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {} 59 60 public: 61 const LExpr *left() const { return LHS; } 62 LExpr *left() { return LHS; } 63 64 const LExpr *right() const { return RHS; } 65 LExpr *right() { return RHS; } 66 }; 67 68 class And : public BinOp { 69 public: 70 And(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::And) {} 71 72 static bool classof(const LExpr *E) { return E->kind() == LExpr::And; } 73 }; 74 75 class Or : public BinOp { 76 public: 77 Or(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::Or) {} 78 79 static bool classof(const LExpr *E) { return E->kind() == LExpr::Or; } 80 }; 81 82 class Not : public LExpr { 83 LExpr *Exp; 84 85 public: 86 Not(LExpr *Exp) : LExpr(LExpr::Not), Exp(Exp) {} 87 88 const LExpr *exp() const { return Exp; } 89 LExpr *exp() { return Exp; } 90 91 static bool classof(const LExpr *E) { return E->kind() == LExpr::Not; } 92 }; 93 94 /// Logical implication. Returns true if LHS implies RHS, i.e. if LHS 95 /// holds, then RHS must hold. For example, (A & B) implies A. 96 bool implies(const LExpr *LHS, const LExpr *RHS); 97 98 bool LExpr::implies(const LExpr *RHS) const { 99 return lexpr::implies(this, RHS); 100 } 101 102 } 103 } 104 } 105 106 #endif 107 108