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