clang/lib/Analysis/ThreadSafetyLogical.cpp

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