Home | History | Annotate | Download | only in Analyses 
      1 //===- ThreadSafetyLogical.h -----------------------------------*- C++ --*-===//
      2 //
      3 //                     The LLVM Compiler Infrastructure
      4 //
      5 // This file is distributed under the University of Illinois Open Source
      6 // License. See LICENSE.TXT for details.
      7 //
      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 //===----------------------------------------------------------------------===//
     12 
     13 #ifndef LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H
     14 #define LLVM_CLANG_ANALYSIS_ANALYSES_THREADSAFETYLOGICAL_H
     15 
     16 #include "clang/Analysis/Analyses/ThreadSafetyTIL.h"
     17 
     18 namespace clang {
     19 namespace threadSafety {
     20 namespace lexpr {
     21 
     22 class LExpr {
     23 public:
     24   enum Opcode {
     25     Terminal,
     26     And,
     27     Or,
     28     Not
     29   };
     30   Opcode kind() const { return Kind; }
     31 
     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;
     35 
     36 protected:
     37   LExpr(Opcode Kind) : Kind(Kind) {}
     38 
     39 private:
     40   Opcode Kind;
     41 };
     42 
     43 class Terminal : public LExpr {
     44   til::SExpr *Expr;
     45 
     46 public:
     47   Terminal(til::SExpr *Expr) : LExpr(LExpr::Terminal), Expr(Expr) {}
     48 
     49   const til::SExpr *expr() const { return Expr; }
     50   til::SExpr *expr() { return Expr; }
     51 
     52   static bool classof(const LExpr *E) { return E->kind() == LExpr::Terminal; }
     53 };
     54 
     55 class BinOp : public LExpr {
     56   LExpr *LHS, *RHS;
     57 
     58 protected:
     59   BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {}
     60 
     61 public:
     62   const LExpr *left() const { return LHS; }
     63   LExpr *left() { return LHS; }
     64 
     65   const LExpr *right() const { return RHS; }
     66   LExpr *right() { return RHS; }
     67 };
     68 
     69 class And : public BinOp {
     70 public:
     71   And(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::And) {}
     72 
     73   static bool classof(const LExpr *E) { return E->kind() == LExpr::And; }
     74 };
     75 
     76 class Or : public BinOp {
     77 public:
     78   Or(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::Or) {}
     79 
     80   static bool classof(const LExpr *E) { return E->kind() == LExpr::Or; }
     81 };
     82 
     83 class Not : public LExpr {
     84   LExpr *Exp;
     85 
     86 public:
     87   Not(LExpr *Exp) : LExpr(LExpr::Not), Exp(Exp) {}
     88 
     89   const LExpr *exp() const { return Exp; }
     90   LExpr *exp() { return Exp; }
     91 
     92   static bool classof(const LExpr *E) { return E->kind() == LExpr::Not; }
     93 };
     94 
     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);
     98 
     99 bool LExpr::implies(const LExpr *RHS) const {
    100   return lexpr::implies(this, RHS);
    101 }
    102 
    103 }
    104 }
    105 }
    106 
    107 #endif
    108 
    109