6024e5c395
clang 20.0.0 (based on r547379) from build 12806354. Bug: http://b/379133546 Test: N/A Change-Id: I2eb8938af55d809de674be63cb30cf27e801862b Upstream-Commit: ad834e67b1105d15ef907f6255d4c96e8e733f57
108 lines
2.7 KiB
C++
108 lines
2.7 KiB
C++
//===- 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
|
|
|