ThreadSafetyLogical.cpp revision 6bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89 
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
15using namespace llvm;
16using 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.
20static 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
102namespace clang {
103namespace threadSafety {
104namespace lexpr {
105
106bool 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}
113