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 } 113
