summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clang/include/clang/Analysis/Analyses/ThreadSafetyLogical.h108
-rw-r--r--clang/include/clang/Analysis/Analyses/ThreadSafetyUtil.h2
-rw-r--r--clang/lib/Analysis/CMakeLists.txt3
-rw-r--r--clang/lib/Analysis/ThreadSafety.cpp47
-rw-r--r--clang/lib/Analysis/ThreadSafetyLogical.cpp112
5 files changed, 271 insertions, 1 deletions
diff --git a/clang/include/clang/Analysis/Analyses/ThreadSafetyLogical.h b/clang/include/clang/Analysis/Analyses/ThreadSafetyLogical.h
new file mode 100644
index 00000000000..c4f4b21aab1
--- /dev/null
+++ b/clang/include/clang/Analysis/Analyses/ThreadSafetyLogical.h
@@ -0,0 +1,108 @@
+//===- ThreadSafetyLogical.h -----------------------------------*- 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.
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_THREAD_SAFETY_LOGICAL_H
+#define LLVM_CLANG_THREAD_SAFETY_LOGICAL_H
+
+#include "clang/Analysis/Analyses/ThreadSafetyTIL.h"
+
+namespace clang {
+namespace threadSafety {
+namespace lexpr {
+
+class LExpr {
+public:
+ enum Opcode {
+ Terminal,
+ And,
+ Or,
+ Not
+ };
+ Opcode kind() const { return Kind; }
+
+ /// \brief Logical implication. Returns true if the LExpr implies RHS, i.e. if
+ /// the LExpr holds, then RHS must hold. For example, (A & B) implies A.
+ inline bool implies(const LExpr *RHS) const;
+
+protected:
+ LExpr(Opcode Kind) : Kind(Kind) {}
+
+private:
+ Opcode Kind;
+};
+
+class Terminal : public LExpr {
+ til::SExprRef Expr;
+
+public:
+ Terminal(til::SExpr *Expr) : LExpr(LExpr::Terminal), Expr(Expr) {}
+
+ const til::SExpr *expr() const { return Expr.get(); }
+ til::SExpr *expr() { return Expr.get(); }
+
+ static bool classof(const LExpr *E) { return E->kind() == LExpr::Terminal; }
+};
+
+class BinOp : public LExpr {
+ LExpr *LHS, *RHS;
+
+protected:
+ BinOp(LExpr *LHS, LExpr *RHS, Opcode Code) : LExpr(Code), LHS(LHS), RHS(RHS) {}
+
+public:
+ const LExpr *left() const { return LHS; }
+ LExpr *left() { return LHS; }
+
+ const LExpr *right() const { return RHS; }
+ LExpr *right() { return RHS; }
+};
+
+class And : public BinOp {
+public:
+ And(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::And) {}
+
+ static bool classof(const LExpr *E) { return E->kind() == LExpr::And; }
+};
+
+class Or : public BinOp {
+public:
+ Or(LExpr *LHS, LExpr *RHS) : BinOp(LHS, RHS, LExpr::Or) {}
+
+ static bool classof(const LExpr *E) { return E->kind() == LExpr::Or; }
+};
+
+class Not : public LExpr {
+ LExpr *Exp;
+
+public:
+ Not(LExpr *Exp) : LExpr(LExpr::Not), Exp(Exp) {}
+
+ const LExpr *exp() const { return Exp; }
+ LExpr *exp() { return Exp; }
+
+ static bool classof(const LExpr *E) { return E->kind() == LExpr::Not; }
+};
+
+/// \brief Logical implication. Returns true if LHS implies RHS, i.e. if LHS
+/// holds, then RHS must hold. For example, (A & B) implies A.
+bool implies(const LExpr *LHS, const LExpr *RHS);
+
+bool LExpr::implies(const LExpr *RHS) const {
+ return lexpr::implies(this, RHS);
+}
+
+}
+}
+}
+
+#endif // LLVM_CLANG_THREAD_SAFETY_LOGICAL_H
+
diff --git a/clang/include/clang/Analysis/Analyses/ThreadSafetyUtil.h b/clang/include/clang/Analysis/Analyses/ThreadSafetyUtil.h
index 3b768c5a692..ece7425c225 100644
--- a/clang/include/clang/Analysis/Analyses/ThreadSafetyUtil.h
+++ b/clang/include/clang/Analysis/Analyses/ThreadSafetyUtil.h
@@ -14,11 +14,13 @@
#ifndef LLVM_CLANG_THREAD_SAFETY_UTIL_H
#define LLVM_CLANG_THREAD_SAFETY_UTIL_H
+#include "llvm/ADT/StringRef.h"
#include "llvm/Support/AlignOf.h"
#include "llvm/Support/Allocator.h"
#include <cassert>
#include <cstddef>
+#include <vector>
#include <utility>
namespace clang {
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);
+}
+}
+}
+}
OpenPOWER on IntegriCloud