Index: include/clang/Analysis/Analyses/ThreadSafetyLogical.h =================================================================== --- include/clang/Analysis/Analyses/ThreadSafetyLogical.h (revision 0) +++ include/clang/Analysis/Analyses/ThreadSafetyLogical.h (working copy) @@ -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 + Index: include/clang/Analysis/Analyses/ThreadSafetyUtil.h =================================================================== --- include/clang/Analysis/Analyses/ThreadSafetyUtil.h (revision 208231) +++ include/clang/Analysis/Analyses/ThreadSafetyUtil.h (working copy) @@ -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 #include +#include #include namespace clang { Index: lib/Analysis/CMakeLists.txt =================================================================== --- lib/Analysis/CMakeLists.txt (revision 208231) +++ lib/Analysis/CMakeLists.txt (working copy) @@ -22,8 +22,9 @@ PseudoConstantAnalysis.cpp ReachableCode.cpp ScanfFormatString.cpp + ThreadSafety.cpp ThreadSafetyCommon.cpp - ThreadSafety.cpp + ThreadSafetyLogical.cpp UninitializedValues.cpp LINK_LIBS Index: lib/Analysis/ThreadSafety.cpp =================================================================== --- lib/Analysis/ThreadSafety.cpp (revision 208231) +++ lib/Analysis/ThreadSafety.cpp (working copy) @@ -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 @@ } }; +/// \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(CurExpr)) { + // TODO: Construct the til::SExpr leaf properly. + return new Terminal(new (Arena) Variable()); + } else if (const auto *ME = dyn_cast(CurExpr)) { + // TODO: Construct the til::SExpr leaf properly. + return new Terminal(new (Arena) Variable()); + } else if (const auto *BOE = dyn_cast(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(CurExpr)) { + if (UOE->getOpcode() == UO_LNot) { + auto *E = buildLExpr(Arena, UOE->getSubExpr()); + return new Not(E); + } + } else if (const auto *CE = dyn_cast(CurExpr)) { + return buildLExpr(Arena, CE->getSubExpr()); + } else if (const auto *PE = dyn_cast(CurExpr)) { + return buildLExpr(Arena, PE->getSubExpr()); + } + + return nullptr; +} + /// \brief A short list of SExprs class MutexIDList : public SmallVector { public: Index: lib/Analysis/ThreadSafetyLogical.cpp =================================================================== --- lib/Analysis/ThreadSafetyLogical.cpp (revision 0) +++ lib/Analysis/ThreadSafetyLogical.cpp (working copy) @@ -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(RHS)) + : RightAndOperator(cast(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(RHS)) + : RightOrOperator(cast(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(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(LHS)) + : LeftOrOperator(cast(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(LHS)) + : LeftAndOperator(cast(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(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(LHS)->expr() == cast(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); +} +} +} +}