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