Details | Last modification | View Log | RSS feed
| Rev | Author | Line No. | Line |
|---|---|---|---|
| 14 | pmbaty | 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 |