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
17namespace clang {
18namespace threadSafety {
19namespace lexpr {
20
21class LExpr {
22public:
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
35protected:
36  LExpr(Opcode Kind) : Kind(Kind) {}
37
38private:
39  Opcode Kind;
40};
41
42class Terminal : public LExpr {
43  til::SExpr *Expr;
44
45public:
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
54class BinOp : public LExpr {
55  LExpr *LHS, *RHS;
56
57protected:
58  BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {}
59
60public:
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
68class And : public BinOp {
69public:
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
75class Or : public BinOp {
76public:
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
82class Not : public LExpr {
83  LExpr *Exp;
84
85public:
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.
96bool implies(const LExpr *LHS, const LExpr *RHS);
97
98bool LExpr::implies(const LExpr *RHS) const {
99  return lexpr::implies(this, RHS);
100}
101
102}
103}
104}
105
106#endif
107
108