/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/lib/Analysis/ThreadSafetyLogical.cpp
Line | Count | Source (jump to first uncovered line) |
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. |
19 | 0 | 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 | 0 | const auto LeftAndOperator = [=](const BinOp *A) { |
24 | 0 | return implies(A->left(), LNeg, RHS, RNeg) && |
25 | 0 | implies(A->right(), LNeg, RHS, RNeg); |
26 | 0 | }; |
27 | 0 | const auto RightAndOperator = [=](const BinOp *A) { |
28 | 0 | return implies(LHS, LNeg, A->left(), RNeg) && |
29 | 0 | implies(LHS, LNeg, A->right(), RNeg); |
30 | 0 | }; |
31 | | |
32 | | // Calculates the logical OR implication operator. |
33 | 0 | const auto LeftOrOperator = [=](const BinOp *A) { |
34 | 0 | return implies(A->left(), LNeg, RHS, RNeg) || |
35 | 0 | implies(A->right(), LNeg, RHS, RNeg); |
36 | 0 | }; |
37 | 0 | const auto RightOrOperator = [=](const BinOp *A) { |
38 | 0 | return implies(LHS, LNeg, A->left(), RNeg) || |
39 | 0 | implies(LHS, LNeg, A->right(), RNeg); |
40 | 0 | }; |
41 | | |
42 | | // Recurse on right. |
43 | 0 | switch (RHS->kind()) { |
44 | 0 | 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 | 0 | return RNeg ? RightOrOperator(cast<And>(RHS)) |
50 | 0 | : RightAndOperator(cast<And>(RHS)); |
51 | 0 | 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 | 0 | return RNeg ? RightAndOperator(cast<Or>(RHS)) |
57 | 0 | : RightOrOperator(cast<Or>(RHS)); |
58 | 0 | 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 | 0 | return implies(LHS, LNeg, cast<Not>(RHS)->exp(), !RNeg); |
62 | 0 | case LExpr::Terminal: |
63 | | // After reaching the terminal, it's time to recurse on the left. |
64 | 0 | break; |
65 | 0 | } |
66 | | |
67 | | // RHS is now a terminal. Recurse on Left. |
68 | 0 | switch (LHS->kind()) { |
69 | 0 | 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 | 0 | return LNeg ? LeftAndOperator(cast<And>(LHS)) |
75 | 0 | : LeftOrOperator(cast<And>(LHS)); |
76 | 0 | 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 | 0 | return LNeg ? LeftOrOperator(cast<Or>(LHS)) |
82 | 0 | : LeftAndOperator(cast<Or>(LHS)); |
83 | 0 | 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 | 0 | return implies(cast<Not>(LHS)->exp(), !LNeg, RHS, RNeg); |
87 | 0 | case LExpr::Terminal: |
88 | | // After reaching the terminal, it's time to perform identity comparisons. |
89 | 0 | break; |
90 | 0 | } |
91 | | |
92 | | // A => A |
93 | | // !A => !A |
94 | 0 | if (LNeg != RNeg) |
95 | 0 | return false; |
96 | | |
97 | | // FIXME -- this should compare SExprs for equality, not pointer equality. |
98 | 0 | return cast<Terminal>(LHS)->expr() == cast<Terminal>(RHS)->expr(); |
99 | 0 | } |
100 | | |
101 | | namespace clang { |
102 | | namespace threadSafety { |
103 | | namespace lexpr { |
104 | | |
105 | 0 | bool implies(const LExpr *LHS, const LExpr *RHS) { |
106 | | // Start out by assuming that LHS and RHS are not negated. |
107 | 0 | return ::implies(LHS, false, RHS, false); |
108 | 0 | } |
109 | | } |
110 | | } |
111 | | } |