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