Stephen Hines | c568f1e | 2014-07-21 00:47:37 -0700 | [diff] [blame] | 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 | } |