1 //===- ThreadSafetyLogical.h -----------------------------------*- C++ --*-===//
3 // The LLVM Compiler Infrastructure
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
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 //===----------------------------------------------------------------------===//
13 #ifndef LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H
14 #define LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H
16 #include "clang/Analysis/Analyses/ThreadSafetyTIL.h"
19 namespace threadSafety {
30 Opcode kind() const { return Kind; }
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;
37 LExpr(Opcode Kind) : Kind(Kind) {}
43 class Terminal : public LExpr {
47 Terminal(til::SExpr *Expr) : LExpr(LExpr::Terminal), Expr(Expr) {}
49 const til::SExpr *expr() const { return Expr; }
50 til::SExpr *expr() { return Expr; }
52 static bool classof(const LExpr *E) { return E->kind() == LExpr::Terminal; }
55 class BinOp : public LExpr {
59 BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {}
62 const LExpr *left() const { return LHS; }
63 LExpr *left() { return LHS; }
65 const LExpr *right() const { return RHS; }
66 LExpr *right() { return RHS; }
69 class And : public BinOp {
71 And(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::And) {}
73 static bool classof(const LExpr *E) { return E->kind() == LExpr::And; }
76 class Or : public BinOp {
78 Or(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::Or) {}
80 static bool classof(const LExpr *E) { return E->kind() == LExpr::Or; }
83 class Not : public LExpr {
87 Not(LExpr *Exp) : LExpr(LExpr::Not), Exp(Exp) {}
89 const LExpr *exp() const { return Exp; }
90 LExpr *exp() { return Exp; }
92 static bool classof(const LExpr *E) { return E->kind() == LExpr::Not; }
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.
97 bool implies(const LExpr *LHS, const LExpr *RHS);
99 bool LExpr::implies(const LExpr *RHS) const {
100 return lexpr::implies(this, RHS);