| //===- ThreadSafetyLogical.cpp ---------------------------------*- C++ --*-===// |
| // |
| // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. |
| // See https://llvm.org/LICENSE.txt for license information. |
| // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception |
| // |
| //===----------------------------------------------------------------------===// |
| // This file defines a representation for logical expressions with SExpr leaves |
| // that are used as part of fact-checking capability expressions. |
| //===----------------------------------------------------------------------===// |
| |
| #include "clang/Analysis/Analyses/ThreadSafetyLogical.h" |
| |
| using namespace llvm; |
| using namespace clang::threadSafety::lexpr; |
| |
| // Implication. We implement De Morgan's Laws by maintaining LNeg and RNeg |
| // to keep track of whether LHS and RHS are negated. |
| static bool implies(const LExpr *LHS, bool LNeg, const LExpr *RHS, bool RNeg) { |
| // In comments below, we write => for implication. |
| |
| // Calculates the logical AND implication operator. |
| const auto LeftAndOperator = [=](const BinOp *A) { |
| return implies(A->left(), LNeg, RHS, RNeg) && |
| implies(A->right(), LNeg, RHS, RNeg); |
| }; |
| const auto RightAndOperator = [=](const BinOp *A) { |
| return implies(LHS, LNeg, A->left(), RNeg) && |
| implies(LHS, LNeg, A->right(), RNeg); |
| }; |
| |
| // Calculates the logical OR implication operator. |
| const auto LeftOrOperator = [=](const BinOp *A) { |
| return implies(A->left(), LNeg, RHS, RNeg) || |
| implies(A->right(), LNeg, RHS, RNeg); |
| }; |
| const auto RightOrOperator = [=](const BinOp *A) { |
| return implies(LHS, LNeg, A->left(), RNeg) || |
| implies(LHS, LNeg, A->right(), RNeg); |
| }; |
| |
| // Recurse on right. |
| switch (RHS->kind()) { |
| case LExpr::And: |
| // When performing right recursion: |
| // C => A & B [if] C => A and C => B |
| // When performing right recursion (negated): |
| // C => !(A & B) [if] C => !A | !B [===] C => !A or C => !B |
| return RNeg ? RightOrOperator(cast<And>(RHS)) |
| : RightAndOperator(cast<And>(RHS)); |
| case LExpr::Or: |
| // When performing right recursion: |
| // C => (A | B) [if] C => A or C => B |
| // When performing right recursion (negated): |
| // C => !(A | B) [if] C => !A & !B [===] C => !A and C => !B |
| return RNeg ? RightAndOperator(cast<Or>(RHS)) |
| : RightOrOperator(cast<Or>(RHS)); |
| case LExpr::Not: |
| // Note that C => !A is very different from !(C => A). It would be incorrect |
| // to return !implies(LHS, RHS). |
| return implies(LHS, LNeg, cast<Not>(RHS)->exp(), !RNeg); |
| case LExpr::Terminal: |
| // After reaching the terminal, it's time to recurse on the left. |
| break; |
| } |
| |
| // RHS is now a terminal. Recurse on Left. |
| switch (LHS->kind()) { |
| case LExpr::And: |
| // When performing left recursion: |
| // A & B => C [if] A => C or B => C |
| // When performing left recursion (negated): |
| // !(A & B) => C [if] !A | !B => C [===] !A => C and !B => C |
| return LNeg ? LeftAndOperator(cast<And>(LHS)) |
| : LeftOrOperator(cast<And>(LHS)); |
| case LExpr::Or: |
| // When performing left recursion: |
| // A | B => C [if] A => C and B => C |
| // When performing left recursion (negated): |
| // !(A | B) => C [if] !A & !B => C [===] !A => C or !B => C |
| return LNeg ? LeftOrOperator(cast<Or>(LHS)) |
| : LeftAndOperator(cast<Or>(LHS)); |
| case LExpr::Not: |
| // Note that A => !C is very different from !(A => C). It would be incorrect |
| // to return !implies(LHS, RHS). |
| return implies(cast<Not>(LHS)->exp(), !LNeg, RHS, RNeg); |
| case LExpr::Terminal: |
| // After reaching the terminal, it's time to perform identity comparisons. |
| break; |
| } |
| |
| // A => A |
| // !A => !A |
| if (LNeg != RNeg) |
| return false; |
| |
| // FIXME -- this should compare SExprs for equality, not pointer equality. |
| return cast<Terminal>(LHS)->expr() == cast<Terminal>(RHS)->expr(); |
| } |
| |
| namespace clang { |
| namespace threadSafety { |
| namespace lexpr { |
| |
| bool implies(const LExpr *LHS, const LExpr *RHS) { |
| // Start out by assuming that LHS and RHS are not negated. |
| return ::implies(LHS, false, RHS, false); |
| } |
| } |
| } |
| } |