contrib/llvm/tools/clang/lib/Analysis/ThreadSafetyLogical.cpp

   1 //===- ThreadSafetyLogical.cpp ---------------------------------*- 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 #include "clang/Analysis/Analyses/ThreadSafetyLogical.h"
  14
  15 using namespace llvm;
  16 using namespace clang::threadSafety::lexpr;
  17
  18 // Implication.  We implement De Morgan's Laws by maintaining LNeg and RNeg
  19 // to keep track of whether LHS and RHS are negated.
  20 static bool implies(const LExpr *LHS, bool LNeg, const LExpr *RHS, bool RNeg) {
  21   // In comments below, we write => for implication.
  22
  23   // Calculates the logical AND implication operator.
  24   const auto LeftAndOperator = [=](const BinOp *A) {
  25     return implies(A->left(), LNeg, RHS, RNeg) &&
  26            implies(A->right(), LNeg, RHS, RNeg);
  27   };
  28   const auto RightAndOperator = [=](const BinOp *A) {
  29     return implies(LHS, LNeg, A->left(), RNeg) &&
  30            implies(LHS, LNeg, A->right(), RNeg);
  31   };
  32
  33   // Calculates the logical OR implication operator.
  34   const auto LeftOrOperator = [=](const BinOp *A) {
  35     return implies(A->left(), LNeg, RHS, RNeg) ||
  36            implies(A->right(), LNeg, RHS, RNeg);
  37   };
  38   const auto RightOrOperator = [=](const BinOp *A) {
  39     return implies(LHS, LNeg, A->left(), RNeg) ||
  40            implies(LHS, LNeg, A->right(), RNeg);
  41   };
  42
  43   // Recurse on right.
  44   switch (RHS->kind()) {
  45   case LExpr::And:
  46     // When performing right recursion:
  47     //   C => A & B  [if]  C => A and C => B
  48     // When performing right recursion (negated):
  49     //   C => !(A & B)  [if]  C => !A | !B  [===]  C => !A or C => !B
  50     return RNeg ? RightOrOperator(cast<And>(RHS))
  51                 : RightAndOperator(cast<And>(RHS));
  52   case LExpr::Or:
  53     // When performing right recursion:
  54     //   C => (A | B)  [if]  C => A or C => B
  55     // When performing right recursion (negated):
  56     //   C => !(A | B)  [if]  C => !A & !B  [===]  C => !A and C => !B
  57     return RNeg ? RightAndOperator(cast<Or>(RHS))
  58                 : RightOrOperator(cast<Or>(RHS));
  59   case LExpr::Not:
  60     // Note that C => !A is very different from !(C => A). It would be incorrect
  61     // to return !implies(LHS, RHS).
  62     return implies(LHS, LNeg, cast<Not>(RHS)->exp(), !RNeg);
  63   case LExpr::Terminal:
  64     // After reaching the terminal, it's time to recurse on the left.
  65     break;
  66   }
  67
  68   // RHS is now a terminal.  Recurse on Left.
  69   switch (LHS->kind()) {
  70   case LExpr::And:
  71     // When performing left recursion:
  72     //   A & B => C  [if]  A => C or B => C
  73     // When performing left recursion (negated):
  74     //   !(A & B) => C  [if]  !A | !B => C  [===]  !A => C and !B => C
  75     return LNeg ? LeftAndOperator(cast<And>(LHS))
  76                 : LeftOrOperator(cast<And>(LHS));
  77   case LExpr::Or:
  78     // When performing left recursion:
  79     //   A | B => C  [if]  A => C and B => C
  80     // When performing left recursion (negated):
  81     //   !(A | B) => C  [if]  !A & !B => C  [===]  !A => C or !B => C
  82     return LNeg ? LeftOrOperator(cast<Or>(LHS))
  83                 : LeftAndOperator(cast<Or>(LHS));
  84   case LExpr::Not:
  85     // Note that A => !C is very different from !(A => C). It would be incorrect
  86     // to return !implies(LHS, RHS).
  87     return implies(cast<Not>(LHS)->exp(), !LNeg, RHS, RNeg);
  88   case LExpr::Terminal:
  89     // After reaching the terminal, it's time to perform identity comparisons.
  90     break;
  91   }
  92
  93   // A => A
  94   // !A => !A
  95   if (LNeg != RNeg)
  96     return false;
  97
  98   // FIXME -- this should compare SExprs for equality, not pointer equality.
  99   return cast<Terminal>(LHS)->expr() == cast<Terminal>(RHS)->expr();
 100 }
 101
 102 namespace clang {
 103 namespace threadSafety {
 104 namespace lexpr {
 105
 106 bool implies(const LExpr *LHS, const LExpr *RHS) {
 107   // Start out by assuming that LHS and RHS are not negated.
 108   return ::implies(LHS, false, RHS, false);
 109 }
 110 }
 111 }
 112 }