ThreadSafetyLogical.cpp revision 274958
138032Speter//===- ThreadSafetyLogical.cpp ---------------------------------*- C++ --*-===// 294337Sgshapiro// 364565Sgshapiro// The LLVM Compiler Infrastructure 438032Speter// 538032Speter// This file is distributed under the University of Illinois Open Source 638032Speter// License. See LICENSE.TXT for details. 738032Speter// 838032Speter//===----------------------------------------------------------------------===// 938032Speter// This file defines a representation for logical expressions with SExpr leaves 1038032Speter// that are used as part of fact-checking capability expressions. 1138032Speter//===----------------------------------------------------------------------===// 1238032Speter 13203004Sgshapiro#include "clang/Analysis/Analyses/ThreadSafetyLogical.h" 1438032Speter 1538032Speterusing namespace llvm; 1638032Speterusing namespace clang::threadSafety::lexpr; 1738032Speter 1838032Speter// Implication. We implement De Morgan's Laws by maintaining LNeg and RNeg 1938032Speter// to keep track of whether LHS and RHS are negated. 2038032Speterstatic bool implies(const LExpr *LHS, bool LNeg, const LExpr *RHS, bool RNeg) { 2138032Speter // In comments below, we write => for implication. 2238032Speter 2364565Sgshapiro // Calculates the logical AND implication operator. 2464565Sgshapiro const auto LeftAndOperator = [=](const BinOp *A) { 2564565Sgshapiro return implies(A->left(), LNeg, RHS, RNeg) && 2638032Speter implies(A->right(), LNeg, RHS, RNeg); 2738032Speter }; 2864565Sgshapiro const auto RightAndOperator = [=](const BinOp *A) { 2938032Speter return implies(LHS, LNeg, A->left(), RNeg) && 3038032Speter implies(LHS, LNeg, A->right(), RNeg); 3138032Speter }; 3238032Speter 3364565Sgshapiro // Calculates the logical OR implication operator. 3438032Speter const auto LeftOrOperator = [=](const BinOp *A) { 3564565Sgshapiro return implies(A->left(), LNeg, RHS, RNeg) || 3664565Sgshapiro implies(A->right(), LNeg, RHS, RNeg); 3738032Speter }; 3838032Speter const auto RightOrOperator = [=](const BinOp *A) { 3938032Speter return implies(LHS, LNeg, A->left(), RNeg) || 4038032Speter implies(LHS, LNeg, A->right(), RNeg); 4138032Speter }; 4238032Speter 4364565Sgshapiro // Recurse on right. 4438032Speter switch (RHS->kind()) { 4564565Sgshapiro case LExpr::And: 4664565Sgshapiro // When performing right recursion: 4764565Sgshapiro // C => A & B [if] C => A and C => B 4864565Sgshapiro // When performing right recursion (negated): 4964565Sgshapiro // C => !(A & B) [if] C => !A | !B [===] C => !A or C => !B 5064565Sgshapiro return RNeg ? RightOrOperator(cast<And>(RHS)) 5164565Sgshapiro : RightAndOperator(cast<And>(RHS)); 5264565Sgshapiro case LExpr::Or: 5364565Sgshapiro // When performing right recursion: 5464565Sgshapiro // C => (A | B) [if] C => A or C => B 5564565Sgshapiro // When performing right recursion (negated): 5638032Speter // C => !(A | B) [if] C => !A & !B [===] C => !A and C => !B 5738032Speter return RNeg ? RightAndOperator(cast<Or>(RHS)) 5838032Speter : RightOrOperator(cast<Or>(RHS)); 5990795Sgshapiro case LExpr::Not: 6038032Speter // Note that C => !A is very different from !(C => A). It would be incorrect 6138032Speter // to return !implies(LHS, RHS). 62157006Sgshapiro return implies(LHS, LNeg, cast<Not>(RHS)->exp(), !RNeg); 63168520Sgshapiro case LExpr::Terminal: 64168520Sgshapiro // After reaching the terminal, it's time to recurse on the left. 65168520Sgshapiro break; 66168520Sgshapiro } 67168520Sgshapiro 68157006Sgshapiro // RHS is now a terminal. Recurse on Left. 69110563Sgshapiro switch (LHS->kind()) { 70157006Sgshapiro case LExpr::And: 71110563Sgshapiro // When performing left recursion: 72157006Sgshapiro // A & B => C [if] A => C or B => C 73157006Sgshapiro // When performing left recursion (negated): 74157006Sgshapiro // !(A & B) => C [if] !A | !B => C [===] !A => C and !B => C 75157006Sgshapiro return LNeg ? LeftAndOperator(cast<And>(LHS)) 76157006Sgshapiro : LeftOrOperator(cast<And>(LHS)); 77157006Sgshapiro case LExpr::Or: 78157006Sgshapiro // When performing left recursion: 79168520Sgshapiro // A | B => C [if] A => C and B => C 80157006Sgshapiro // When performing left recursion (negated): 81157006Sgshapiro // !(A | B) => C [if] !A & !B => C [===] !A => C or !B => C 82157006Sgshapiro return LNeg ? LeftOrOperator(cast<Or>(LHS)) 8390795Sgshapiro : LeftAndOperator(cast<Or>(LHS)); 84157006Sgshapiro case LExpr::Not: 85157006Sgshapiro // Note that A => !C is very different from !(A => C). It would be incorrect 8690795Sgshapiro // to return !implies(LHS, RHS). 87157006Sgshapiro return implies(cast<Not>(LHS)->exp(), !LNeg, RHS, RNeg); 88157006Sgshapiro case LExpr::Terminal: 89157006Sgshapiro // After reaching the terminal, it's time to perform identity comparisons. 90157006Sgshapiro break; 91157006Sgshapiro } 92157006Sgshapiro 9390795Sgshapiro // A => A 94157006Sgshapiro // !A => !A 95157006Sgshapiro if (LNeg != RNeg) 96157006Sgshapiro return false; 97157006Sgshapiro 9890795Sgshapiro // FIXME -- this should compare SExprs for equality, not pointer equality. 9990795Sgshapiro return cast<Terminal>(LHS)->expr() == cast<Terminal>(RHS)->expr(); 10090795Sgshapiro} 10190795Sgshapiro 10290795Sgshapironamespace clang { 10390795Sgshapironamespace threadSafety { 10490795Sgshapironamespace lexpr { 10590795Sgshapiro 10664565Sgshapirobool implies(const LExpr *LHS, const LExpr *RHS) { 10764565Sgshapiro // Start out by assuming that LHS and RHS are not negated. 10864565Sgshapiro return ::implies(LHS, false, RHS, false); 10964565Sgshapiro} 11064565Sgshapiro} 11171348Sgshapiro} 11264565Sgshapiro} 11364565Sgshapiro