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