1ef8225444452a1486bd721f3285301fe84643b00Stephen Hines//===- ThreadSafetyLogical.cpp ---------------------------------*- C++ --*-===// 2ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// 3ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// The LLVM Compiler Infrastructure 4ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// 5ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// This file is distributed under the University of Illinois Open Source 6ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// License. See LICENSE.TXT for details. 7ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// 8ef8225444452a1486bd721f3285301fe84643b00Stephen Hines//===----------------------------------------------------------------------===// 9ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// This file defines a representation for logical expressions with SExpr leaves 10ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// that are used as part of fact-checking capability expressions. 11ef8225444452a1486bd721f3285301fe84643b00Stephen Hines//===----------------------------------------------------------------------===// 12ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 13ef8225444452a1486bd721f3285301fe84643b00Stephen Hines#include "clang/Analysis/Analyses/ThreadSafetyLogical.h" 14ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 15ef8225444452a1486bd721f3285301fe84643b00Stephen Hinesusing namespace llvm; 16ef8225444452a1486bd721f3285301fe84643b00Stephen Hinesusing namespace clang::threadSafety::lexpr; 17ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 18ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// Implication. We implement De Morgan's Laws by maintaining LNeg and RNeg 19ef8225444452a1486bd721f3285301fe84643b00Stephen Hines// to keep track of whether LHS and RHS are negated. 20ef8225444452a1486bd721f3285301fe84643b00Stephen Hinesstatic bool implies(const LExpr *LHS, bool LNeg, const LExpr *RHS, bool RNeg) { 21ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // In comments below, we write => for implication. 22ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 23ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // Calculates the logical AND implication operator. 24ef8225444452a1486bd721f3285301fe84643b00Stephen Hines const auto LeftAndOperator = [=](const BinOp *A) { 25ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return implies(A->left(), LNeg, RHS, RNeg) && 26ef8225444452a1486bd721f3285301fe84643b00Stephen Hines implies(A->right(), LNeg, RHS, RNeg); 27ef8225444452a1486bd721f3285301fe84643b00Stephen Hines }; 28ef8225444452a1486bd721f3285301fe84643b00Stephen Hines const auto RightAndOperator = [=](const BinOp *A) { 29ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return implies(LHS, LNeg, A->left(), RNeg) && 30ef8225444452a1486bd721f3285301fe84643b00Stephen Hines implies(LHS, LNeg, A->right(), RNeg); 31ef8225444452a1486bd721f3285301fe84643b00Stephen Hines }; 32ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 33ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // Calculates the logical OR implication operator. 34ef8225444452a1486bd721f3285301fe84643b00Stephen Hines const auto LeftOrOperator = [=](const BinOp *A) { 35ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return implies(A->left(), LNeg, RHS, RNeg) || 36ef8225444452a1486bd721f3285301fe84643b00Stephen Hines implies(A->right(), LNeg, RHS, RNeg); 37ef8225444452a1486bd721f3285301fe84643b00Stephen Hines }; 38ef8225444452a1486bd721f3285301fe84643b00Stephen Hines const auto RightOrOperator = [=](const BinOp *A) { 39ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return implies(LHS, LNeg, A->left(), RNeg) || 40ef8225444452a1486bd721f3285301fe84643b00Stephen Hines implies(LHS, LNeg, A->right(), RNeg); 41ef8225444452a1486bd721f3285301fe84643b00Stephen Hines }; 42ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 43ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // Recurse on right. 44ef8225444452a1486bd721f3285301fe84643b00Stephen Hines switch (RHS->kind()) { 45ef8225444452a1486bd721f3285301fe84643b00Stephen Hines case LExpr::And: 46ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // When performing right recursion: 47ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // C => A & B [if] C => A and C => B 48ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // When performing right recursion (negated): 49ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // C => !(A & B) [if] C => !A | !B [===] C => !A or C => !B 50ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return RNeg ? RightOrOperator(cast<And>(RHS)) 51ef8225444452a1486bd721f3285301fe84643b00Stephen Hines : RightAndOperator(cast<And>(RHS)); 52ef8225444452a1486bd721f3285301fe84643b00Stephen Hines case LExpr::Or: 53ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // When performing right recursion: 54ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // C => (A | B) [if] C => A or C => B 55ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // When performing right recursion (negated): 56ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // C => !(A | B) [if] C => !A & !B [===] C => !A and C => !B 57ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return RNeg ? RightAndOperator(cast<Or>(RHS)) 58ef8225444452a1486bd721f3285301fe84643b00Stephen Hines : RightOrOperator(cast<Or>(RHS)); 59ef8225444452a1486bd721f3285301fe84643b00Stephen Hines case LExpr::Not: 60ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // Note that C => !A is very different from !(C => A). It would be incorrect 61ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // to return !implies(LHS, RHS). 62ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return implies(LHS, LNeg, cast<Not>(RHS)->exp(), !RNeg); 63ef8225444452a1486bd721f3285301fe84643b00Stephen Hines case LExpr::Terminal: 64ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // After reaching the terminal, it's time to recurse on the left. 65ef8225444452a1486bd721f3285301fe84643b00Stephen Hines break; 66ef8225444452a1486bd721f3285301fe84643b00Stephen Hines } 67ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 68ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // RHS is now a terminal. Recurse on Left. 69ef8225444452a1486bd721f3285301fe84643b00Stephen Hines switch (LHS->kind()) { 70ef8225444452a1486bd721f3285301fe84643b00Stephen Hines case LExpr::And: 71ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // When performing left recursion: 72ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // A & B => C [if] A => C or B => C 73ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // When performing left recursion (negated): 74ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // !(A & B) => C [if] !A | !B => C [===] !A => C and !B => C 75ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return LNeg ? LeftAndOperator(cast<And>(LHS)) 76ef8225444452a1486bd721f3285301fe84643b00Stephen Hines : LeftOrOperator(cast<And>(LHS)); 77ef8225444452a1486bd721f3285301fe84643b00Stephen Hines case LExpr::Or: 78ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // When performing left recursion: 79ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // A | B => C [if] A => C and B => C 80ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // When performing left recursion (negated): 81ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // !(A | B) => C [if] !A & !B => C [===] !A => C or !B => C 82ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return LNeg ? LeftOrOperator(cast<Or>(LHS)) 83ef8225444452a1486bd721f3285301fe84643b00Stephen Hines : LeftAndOperator(cast<Or>(LHS)); 84ef8225444452a1486bd721f3285301fe84643b00Stephen Hines case LExpr::Not: 85ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // Note that A => !C is very different from !(A => C). It would be incorrect 86ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // to return !implies(LHS, RHS). 87ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return implies(cast<Not>(LHS)->exp(), !LNeg, RHS, RNeg); 88ef8225444452a1486bd721f3285301fe84643b00Stephen Hines case LExpr::Terminal: 89ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // After reaching the terminal, it's time to perform identity comparisons. 90ef8225444452a1486bd721f3285301fe84643b00Stephen Hines break; 91ef8225444452a1486bd721f3285301fe84643b00Stephen Hines } 92ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 93ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // A => A 94ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // !A => !A 95ef8225444452a1486bd721f3285301fe84643b00Stephen Hines if (LNeg != RNeg) 96ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return false; 97ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 98ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // FIXME -- this should compare SExprs for equality, not pointer equality. 99ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return cast<Terminal>(LHS)->expr() == cast<Terminal>(RHS)->expr(); 100ef8225444452a1486bd721f3285301fe84643b00Stephen Hines} 101ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 102ef8225444452a1486bd721f3285301fe84643b00Stephen Hinesnamespace clang { 103ef8225444452a1486bd721f3285301fe84643b00Stephen Hinesnamespace threadSafety { 104ef8225444452a1486bd721f3285301fe84643b00Stephen Hinesnamespace lexpr { 105ef8225444452a1486bd721f3285301fe84643b00Stephen Hines 106ef8225444452a1486bd721f3285301fe84643b00Stephen Hinesbool implies(const LExpr *LHS, const LExpr *RHS) { 107ef8225444452a1486bd721f3285301fe84643b00Stephen Hines // Start out by assuming that LHS and RHS are not negated. 108ef8225444452a1486bd721f3285301fe84643b00Stephen Hines return ::implies(LHS, false, RHS, false); 109ef8225444452a1486bd721f3285301fe84643b00Stephen Hines} 110ef8225444452a1486bd721f3285301fe84643b00Stephen Hines} 111ef8225444452a1486bd721f3285301fe84643b00Stephen Hines} 112ef8225444452a1486bd721f3285301fe84643b00Stephen Hines} 113