10b57cec5SDimitry Andric //===- ThreadSafetyLogical.cpp ---------------------------------*- C++ --*-===//
20b57cec5SDimitry Andric //
30b57cec5SDimitry Andric // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
40b57cec5SDimitry Andric // See https://llvm.org/LICENSE.txt for license information.
50b57cec5SDimitry Andric // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
60b57cec5SDimitry Andric //
70b57cec5SDimitry Andric //===----------------------------------------------------------------------===//
80b57cec5SDimitry Andric // This file defines a representation for logical expressions with SExpr leaves
90b57cec5SDimitry Andric // that are used as part of fact-checking capability expressions.
100b57cec5SDimitry Andric //===----------------------------------------------------------------------===//
110b57cec5SDimitry Andric
120b57cec5SDimitry Andric #include "clang/Analysis/Analyses/ThreadSafetyLogical.h"
130b57cec5SDimitry Andric
140b57cec5SDimitry Andric using namespace llvm;
150b57cec5SDimitry Andric using namespace clang::threadSafety::lexpr;
160b57cec5SDimitry Andric
170b57cec5SDimitry Andric // Implication. We implement De Morgan's Laws by maintaining LNeg and RNeg
180b57cec5SDimitry Andric // to keep track of whether LHS and RHS are negated.
implies(const LExpr * LHS,bool LNeg,const LExpr * RHS,bool RNeg)190b57cec5SDimitry Andric static bool implies(const LExpr *LHS, bool LNeg, const LExpr *RHS, bool RNeg) {
200b57cec5SDimitry Andric // In comments below, we write => for implication.
210b57cec5SDimitry Andric
220b57cec5SDimitry Andric // Calculates the logical AND implication operator.
230b57cec5SDimitry Andric const auto LeftAndOperator = [=](const BinOp *A) {
240b57cec5SDimitry Andric return implies(A->left(), LNeg, RHS, RNeg) &&
250b57cec5SDimitry Andric implies(A->right(), LNeg, RHS, RNeg);
260b57cec5SDimitry Andric };
270b57cec5SDimitry Andric const auto RightAndOperator = [=](const BinOp *A) {
280b57cec5SDimitry Andric return implies(LHS, LNeg, A->left(), RNeg) &&
290b57cec5SDimitry Andric implies(LHS, LNeg, A->right(), RNeg);
300b57cec5SDimitry Andric };
310b57cec5SDimitry Andric
320b57cec5SDimitry Andric // Calculates the logical OR implication operator.
330b57cec5SDimitry Andric const auto LeftOrOperator = [=](const BinOp *A) {
340b57cec5SDimitry Andric return implies(A->left(), LNeg, RHS, RNeg) ||
350b57cec5SDimitry Andric implies(A->right(), LNeg, RHS, RNeg);
360b57cec5SDimitry Andric };
370b57cec5SDimitry Andric const auto RightOrOperator = [=](const BinOp *A) {
380b57cec5SDimitry Andric return implies(LHS, LNeg, A->left(), RNeg) ||
390b57cec5SDimitry Andric implies(LHS, LNeg, A->right(), RNeg);
400b57cec5SDimitry Andric };
410b57cec5SDimitry Andric
420b57cec5SDimitry Andric // Recurse on right.
430b57cec5SDimitry Andric switch (RHS->kind()) {
440b57cec5SDimitry Andric case LExpr::And:
450b57cec5SDimitry Andric // When performing right recursion:
460b57cec5SDimitry Andric // C => A & B [if] C => A and C => B
470b57cec5SDimitry Andric // When performing right recursion (negated):
480b57cec5SDimitry Andric // C => !(A & B) [if] C => !A | !B [===] C => !A or C => !B
490b57cec5SDimitry Andric return RNeg ? RightOrOperator(cast<And>(RHS))
500b57cec5SDimitry Andric : RightAndOperator(cast<And>(RHS));
510b57cec5SDimitry Andric case LExpr::Or:
520b57cec5SDimitry Andric // When performing right recursion:
530b57cec5SDimitry Andric // C => (A | B) [if] C => A or C => B
540b57cec5SDimitry Andric // When performing right recursion (negated):
550b57cec5SDimitry Andric // C => !(A | B) [if] C => !A & !B [===] C => !A and C => !B
560b57cec5SDimitry Andric return RNeg ? RightAndOperator(cast<Or>(RHS))
570b57cec5SDimitry Andric : RightOrOperator(cast<Or>(RHS));
580b57cec5SDimitry Andric case LExpr::Not:
590b57cec5SDimitry Andric // Note that C => !A is very different from !(C => A). It would be incorrect
600b57cec5SDimitry Andric // to return !implies(LHS, RHS).
610b57cec5SDimitry Andric return implies(LHS, LNeg, cast<Not>(RHS)->exp(), !RNeg);
620b57cec5SDimitry Andric case LExpr::Terminal:
630b57cec5SDimitry Andric // After reaching the terminal, it's time to recurse on the left.
640b57cec5SDimitry Andric break;
650b57cec5SDimitry Andric }
660b57cec5SDimitry Andric
670b57cec5SDimitry Andric // RHS is now a terminal. Recurse on Left.
680b57cec5SDimitry Andric switch (LHS->kind()) {
690b57cec5SDimitry Andric case LExpr::And:
700b57cec5SDimitry Andric // When performing left recursion:
710b57cec5SDimitry Andric // A & B => C [if] A => C or B => C
720b57cec5SDimitry Andric // When performing left recursion (negated):
730b57cec5SDimitry Andric // !(A & B) => C [if] !A | !B => C [===] !A => C and !B => C
740b57cec5SDimitry Andric return LNeg ? LeftAndOperator(cast<And>(LHS))
750b57cec5SDimitry Andric : LeftOrOperator(cast<And>(LHS));
760b57cec5SDimitry Andric case LExpr::Or:
770b57cec5SDimitry Andric // When performing left recursion:
780b57cec5SDimitry Andric // A | B => C [if] A => C and B => C
790b57cec5SDimitry Andric // When performing left recursion (negated):
800b57cec5SDimitry Andric // !(A | B) => C [if] !A & !B => C [===] !A => C or !B => C
810b57cec5SDimitry Andric return LNeg ? LeftOrOperator(cast<Or>(LHS))
820b57cec5SDimitry Andric : LeftAndOperator(cast<Or>(LHS));
830b57cec5SDimitry Andric case LExpr::Not:
840b57cec5SDimitry Andric // Note that A => !C is very different from !(A => C). It would be incorrect
850b57cec5SDimitry Andric // to return !implies(LHS, RHS).
860b57cec5SDimitry Andric return implies(cast<Not>(LHS)->exp(), !LNeg, RHS, RNeg);
870b57cec5SDimitry Andric case LExpr::Terminal:
880b57cec5SDimitry Andric // After reaching the terminal, it's time to perform identity comparisons.
890b57cec5SDimitry Andric break;
900b57cec5SDimitry Andric }
910b57cec5SDimitry Andric
920b57cec5SDimitry Andric // A => A
930b57cec5SDimitry Andric // !A => !A
940b57cec5SDimitry Andric if (LNeg != RNeg)
950b57cec5SDimitry Andric return false;
960b57cec5SDimitry Andric
970b57cec5SDimitry Andric // FIXME -- this should compare SExprs for equality, not pointer equality.
980b57cec5SDimitry Andric return cast<Terminal>(LHS)->expr() == cast<Terminal>(RHS)->expr();
990b57cec5SDimitry Andric }
1000b57cec5SDimitry Andric
1010b57cec5SDimitry Andric namespace clang {
1020b57cec5SDimitry Andric namespace threadSafety {
1030b57cec5SDimitry Andric namespace lexpr {
1040b57cec5SDimitry Andric
implies(const LExpr * LHS,const LExpr * RHS)1050b57cec5SDimitry Andric bool implies(const LExpr *LHS, const LExpr *RHS) {
1060b57cec5SDimitry Andric // Start out by assuming that LHS and RHS are not negated.
1070b57cec5SDimitry Andric return ::implies(LHS, false, RHS, false);
1080b57cec5SDimitry Andric }
1090b57cec5SDimitry Andric }
1100b57cec5SDimitry Andric }
1110b57cec5SDimitry Andric }
112