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.
implies(const LExpr * LHS,bool LNeg,const LExpr * RHS,bool RNeg)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
implies(const LExpr * LHS,const LExpr * RHS)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