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