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
14using namespace llvm;
15using 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.
19static 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
101namespace clang {
102namespace threadSafety {
103namespace lexpr {
104
105bool 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