16bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines//===- ThreadSafetyLogical.h -----------------------------------*- C++ --*-===// 26bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines// 36bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines// The LLVM Compiler Infrastructure 46bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines// 56bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines// This file is distributed under the University of Illinois Open Source 66bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines// License. See LICENSE.TXT for details. 76bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines// 86bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines//===----------------------------------------------------------------------===// 96bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines// This file defines a representation for logical expressions with SExpr leaves 106bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines// that are used as part of fact-checking capability expressions. 116bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines//===----------------------------------------------------------------------===// 126bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 136bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines#ifndef LLVM_CLANG_THREAD_SAFETY_LOGICAL_H 146bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines#define LLVM_CLANG_THREAD_SAFETY_LOGICAL_H 156bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 166bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines#include "clang/Analysis/Analyses/ThreadSafetyTIL.h" 176bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 186bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesnamespace clang { 196bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesnamespace threadSafety { 206bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesnamespace lexpr { 216bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 226bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesclass LExpr { 236bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinespublic: 246bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines enum Opcode { 256bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines Terminal, 266bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines And, 276bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines Or, 286bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines Not 296bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines }; 306bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines Opcode kind() const { return Kind; } 316bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 326bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines /// \brief Logical implication. Returns true if the LExpr implies RHS, i.e. if 336bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines /// the LExpr holds, then RHS must hold. For example, (A & B) implies A. 346bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines inline bool implies(const LExpr *RHS) const; 356bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 366bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesprotected: 376bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines LExpr(Opcode Kind) : Kind(Kind) {} 386bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 396bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesprivate: 406bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines Opcode Kind; 416bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines}; 426bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 436bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesclass Terminal : public LExpr { 446bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines til::SExprRef Expr; 456bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 466bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinespublic: 476bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines Terminal(til::SExpr *Expr) : LExpr(LExpr::Terminal), Expr(Expr) {} 486bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 496bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines const til::SExpr *expr() const { return Expr.get(); } 506bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines til::SExpr *expr() { return Expr.get(); } 516bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 526bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines static bool classof(const LExpr *E) { return E->kind() == LExpr::Terminal; } 536bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines}; 546bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 556bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesclass BinOp : public LExpr { 566bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines LExpr *LHS, *RHS; 576bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 586bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesprotected: 596bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {} 606bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 616bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinespublic: 626bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines const LExpr *left() const { return LHS; } 636bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines LExpr *left() { return LHS; } 646bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 656bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines const LExpr *right() const { return RHS; } 666bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines LExpr *right() { return RHS; } 676bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines}; 686bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 696bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesclass And : public BinOp { 706bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinespublic: 716bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines And(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::And) {} 726bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 736bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines static bool classof(const LExpr *E) { return E->kind() == LExpr::And; } 746bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines}; 756bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 766bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesclass Or : public BinOp { 776bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinespublic: 786bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines Or(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::Or) {} 796bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 806bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines static bool classof(const LExpr *E) { return E->kind() == LExpr::Or; } 816bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines}; 826bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 836bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesclass Not : public LExpr { 846bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines LExpr *Exp; 856bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 866bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinespublic: 876bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines Not(LExpr *Exp) : LExpr(LExpr::Not), Exp(Exp) {} 886bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 896bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines const LExpr *exp() const { return Exp; } 906bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines LExpr *exp() { return Exp; } 916bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 926bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines static bool classof(const LExpr *E) { return E->kind() == LExpr::Not; } 936bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines}; 946bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 956bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines/// \brief Logical implication. Returns true if LHS implies RHS, i.e. if LHS 966bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines/// holds, then RHS must hold. For example, (A & B) implies A. 976bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesbool implies(const LExpr *LHS, const LExpr *RHS); 986bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 996bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hinesbool LExpr::implies(const LExpr *RHS) const { 1006bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines return lexpr::implies(this, RHS); 1016bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines} 1026bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 1036bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines} 1046bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines} 1056bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines} 1066bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 1076bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines#endif // LLVM_CLANG_THREAD_SAFETY_LOGICAL_H 1086bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines 109