/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/include/clang/Analysis/Analyses/ThreadSafetyLogical.h
Line | Count | Source (jump to first uncovered line) |
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 | 0 | 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 | 0 | 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 | 0 | Terminal(til::SExpr *Expr) : LExpr(LExpr::Terminal), Expr(Expr) {} |
47 | | |
48 | 0 | const til::SExpr *expr() const { return Expr; } |
49 | 0 | til::SExpr *expr() { return Expr; } |
50 | | |
51 | 0 | 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 | 0 | BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {} |
59 | | |
60 | | public: |
61 | 0 | const LExpr *left() const { return LHS; } |
62 | 0 | LExpr *left() { return LHS; } |
63 | | |
64 | 0 | const LExpr *right() const { return RHS; } |
65 | 0 | LExpr *right() { return RHS; } |
66 | | }; |
67 | | |
68 | | class And : public BinOp { |
69 | | public: |
70 | 0 | And(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::And) {} |
71 | | |
72 | 0 | static bool classof(const LExpr *E) { return E->kind() == LExpr::And; } |
73 | | }; |
74 | | |
75 | | class Or : public BinOp { |
76 | | public: |
77 | 0 | Or(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::Or) {} |
78 | | |
79 | 0 | 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 | 0 | Not(LExpr *Exp) : LExpr(LExpr::Not), Exp(Exp) {} |
87 | | |
88 | 0 | const LExpr *exp() const { return Exp; } |
89 | 0 | LExpr *exp() { return Exp; } |
90 | | |
91 | 0 | 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 | 0 | bool LExpr::implies(const LExpr *RHS) const { |
99 | 0 | return lexpr::implies(this, RHS); |
100 | 0 | } |
101 | | |
102 | | } |
103 | | } |
104 | | } |
105 | | |
106 | | #endif |
107 | | |