112 lines · cpp
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-exception6//7//===----------------------------------------------------------------------===//8// This file defines a representation for logical expressions with SExpr leaves9// that are used as part of fact-checking capability expressions.10//===----------------------------------------------------------------------===//11 12#include "clang/Analysis/Analyses/ThreadSafetyLogical.h"13 14using namespace llvm;15using namespace clang::threadSafety::lexpr;16 17// Implication. We implement De Morgan's Laws by maintaining LNeg and RNeg18// to keep track of whether LHS and RHS are negated.19static 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 => B47 // When performing right recursion (negated):48 // C => !(A & B) [if] C => !A | !B [===] C => !A or C => !B49 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 => B54 // When performing right recursion (negated):55 // C => !(A | B) [if] C => !A & !B [===] C => !A and C => !B56 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 incorrect60 // 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 => C72 // When performing left recursion (negated):73 // !(A & B) => C [if] !A | !B => C [===] !A => C and !B => C74 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 => C79 // When performing left recursion (negated):80 // !(A | B) => C [if] !A & !B => C [===] !A => C or !B => C81 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 incorrect85 // 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 => A93 // !A => !A94 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 101namespace clang {102namespace threadSafety {103namespace lexpr {104 105bool 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