3 files changed, 161 insertions, 1 deletions
diff --git a/clang/lib/Analysis/CMakeLists.txt b/clang/lib/Analysis/CMakeLists.txt
index f3e4358974c..89f85933070 100644
--- a/clang/lib/Analysis/CMakeLists.txt
+++ b/clang/lib/Analysis/CMakeLists.txt
@@ -22,8 +22,9 @@ add_clang_library(clangAnalysis
   PseudoConstantAnalysis.cpp
   ReachableCode.cpp
   ScanfFormatString.cpp
-  ThreadSafetyCommon.cpp
   ThreadSafety.cpp
+  ThreadSafetyCommon.cpp
+  ThreadSafetyLogical.cpp
   UninitializedValues.cpp
 
   LINK_LIBS
diff --git a/clang/lib/Analysis/ThreadSafety.cpp b/clang/lib/Analysis/ThreadSafety.cpp
index b34b4814b6f..d19e04d630d 100644
--- a/clang/lib/Analysis/ThreadSafety.cpp
+++ b/clang/lib/Analysis/ThreadSafety.cpp
@@ -22,6 +22,7 @@
 #include "clang/AST/StmtVisitor.h"
 #include "clang/Analysis/Analyses/PostOrderCFGView.h"
 #include "clang/Analysis/Analyses/ThreadSafety.h"
+#include "clang/Analysis/Analyses/ThreadSafetyLogical.h"
 #include "clang/Analysis/Analyses/ThreadSafetyTIL.h"
 #include "clang/Analysis/Analyses/ThreadSafetyTraverse.h"
 #include "clang/Analysis/Analyses/ThreadSafetyCommon.h"
@@ -708,6 +709,52 @@ public:
   }
 };
 
+/// \brief Attempts to create an LExpr from a Clang Expr. If an LExpr cannot be
+/// constructed, returns a null pointer. Recursive function that terminates when
+/// the complete expression is handled, or when a failure to create an LExpr
+/// occurs.
+static clang::threadSafety::lexpr::LExpr *
+buildLExpr(threadSafety::til::MemRegionRef &Arena, const Expr *CurExpr) {
+  using namespace clang::threadSafety::lexpr;
+  using namespace clang::threadSafety::til;
+
+  if (const auto *DRE = dyn_cast<DeclRefExpr>(CurExpr)) {
+    // TODO: Construct the til::SExpr leaf properly.
+    return new Terminal(new (Arena) Variable());
+  } else if (const auto *ME = dyn_cast<MemberExpr>(CurExpr)) {
+    // TODO: Construct the til::SExpr leaf properly.
+    return new Terminal(new (Arena) Variable());
+  } else if (const auto *BOE = dyn_cast<BinaryOperator>(CurExpr)) {
+    switch (BOE->getOpcode()) {
+      case BO_LOr:
+      case BO_LAnd: {
+        auto *LHS = buildLExpr(Arena, BOE->getLHS());
+        auto *RHS = buildLExpr(Arena, BOE->getRHS());
+        if (!LHS || !RHS)
+          return nullptr;
+
+        if (BOE->getOpcode() == BO_LOr)
+          return new Or(LHS, RHS);
+        else
+          return new And(LHS, RHS);
+      }
+    default:
+      break;
+    }
+  } else if (const auto *UOE = dyn_cast<UnaryOperator>(CurExpr)) {
+    if (UOE->getOpcode() == UO_LNot) {
+      auto *E = buildLExpr(Arena, UOE->getSubExpr());
+      return new Not(E);
+    }
+  } else if (const auto *CE = dyn_cast<CastExpr>(CurExpr)) {
+    return buildLExpr(Arena, CE->getSubExpr());
+  } else if (const auto *PE = dyn_cast<ParenExpr>(CurExpr)) {
+    return buildLExpr(Arena, PE->getSubExpr());
+  }
+
+  return nullptr;
+}
+
 /// \brief A short list of SExprs
 class MutexIDList : public SmallVector<SExpr, 3> {
 public:
diff --git a/clang/lib/Analysis/ThreadSafetyLogical.cpp b/clang/lib/Analysis/ThreadSafetyLogical.cpp
new file mode 100644
index 00000000000..51a80776e77
--- /dev/null
+++ b/clang/lib/Analysis/ThreadSafetyLogical.cpp
@@ -0,0 +1,112 @@
+//===- ThreadSafetyLogical.cpp ---------------------------------*- C++ --*-===//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+// This file defines a representation for logical expressions with SExpr leaves
+// that are used as part of fact-checking capability expressions.
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/Analyses/ThreadSafetyLogical.h"
+
+using namespace llvm;
+using namespace clang::threadSafety::lexpr;
+
+// Implication.  We implement De Morgan's Laws by maintaining LNeg and RNeg
+// to keep track of whether LHS and RHS are negated.
+static bool implies(const LExpr *LHS, bool LNeg, const LExpr *RHS, bool RNeg) {
+  // In comments below, we write => for implication.
+
+  // Calculates the logical AND implication operator.
+  const auto LeftAndOperator = [=](const BinOp *A) {
+    return implies(A->left(), LNeg, RHS, RNeg) &&
+           implies(A->right(), LNeg, RHS, RNeg);
+  };
+  const auto RightAndOperator = [=](const BinOp *A) {
+    return implies(LHS, LNeg, A->left(), RNeg) &&
+           implies(LHS, LNeg, A->right(), RNeg);
+  };
+
+  // Calculates the logical OR implication operator.
+  const auto LeftOrOperator = [=](const BinOp *A) {
+    return implies(A->left(), LNeg, RHS, RNeg) ||
+           implies(A->right(), LNeg, RHS, RNeg);
+  };
+  const auto RightOrOperator = [=](const BinOp *A) {
+    return implies(LHS, LNeg, A->left(), RNeg) ||
+           implies(LHS, LNeg, A->right(), RNeg);
+  };
+
+  // Recurse on right.
+  switch (RHS->kind()) {
+  case LExpr::And:
+    // When performing right recursion:
+    //   C => A & B  [if]  C => A and C => B
+    // When performing right recursion (negated):
+    //   C => !(A & B)  [if]  C => !A | !B  [===]  C => !A or C => !B
+    return RNeg ? RightOrOperator(cast<And>(RHS))
+                : RightAndOperator(cast<And>(RHS));
+  case LExpr::Or:
+    // When performing right recursion:
+    //   C => (A | B)  [if]  C => A or C => B
+    // When performing right recursion (negated):
+    //   C => !(A | B)  [if]  C => !A & !B  [===]  C => !A and C => !B
+    return RNeg ? RightAndOperator(cast<Or>(RHS))
+                : RightOrOperator(cast<Or>(RHS));
+  case LExpr::Not:
+    // Note that C => !A is very different from !(C => A). It would be incorrect
+    // to return !implies(LHS, RHS).
+    return implies(LHS, LNeg, cast<Not>(RHS)->exp(), !RNeg);
+  case LExpr::Terminal:
+    // After reaching the terminal, it's time to recurse on the left.
+    break;
+  }
+
+  // RHS is now a terminal.  Recurse on Left.
+  switch (LHS->kind()) {
+  case LExpr::And:
+    // When performing left recursion:
+    //   A & B => C  [if]  A => C or B => C
+    // When performing left recursion (negated):
+    //   !(A & B) => C  [if]  !A | !B => C  [===]  !A => C and !B => C
+    return LNeg ? LeftAndOperator(cast<And>(LHS))
+                : LeftOrOperator(cast<And>(LHS));
+  case LExpr::Or:
+    // When performing left recursion:
+    //   A | B => C  [if]  A => C and B => C
+    // When performing left recursion (negated):
+    //   !(A | B) => C  [if]  !A & !B => C  [===]  !A => C or !B => C
+    return LNeg ? LeftOrOperator(cast<Or>(LHS))
+                : LeftAndOperator(cast<Or>(LHS));
+  case LExpr::Not:
+    // Note that A => !C is very different from !(A => C). It would be incorrect
+    // to return !implies(LHS, RHS).
+    return implies(cast<Not>(LHS)->exp(), !LNeg, RHS, RNeg);
+  case LExpr::Terminal:
+    // After reaching the terminal, it's time to perform identity comparisons.
+    break;
+  }
+
+  // A => A
+  // !A => !A
+  if (LNeg != RNeg)
+    return false;
+
+  // FIXME -- this should compare SExprs for equality, not pointer equality.
+  return cast<Terminal>(LHS)->expr() == cast<Terminal>(RHS)->expr();
+}
+
+namespace clang {
+namespace threadSafety {
+namespace lexpr {
+
+bool implies(const LExpr *LHS, const LExpr *RHS) {
+  // Start out by assuming that LHS and RHS are not negated.
+  return ::implies(LHS, false, RHS, false);
+}
+}
+}
+}