forked from OSchip/llvm-project
112 lines
4.1 KiB
C++
112 lines
4.1 KiB
C++
//===- ThreadSafetyLogical.cpp ---------------------------------*- C++ --*-===//
|
|
//
|
|
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
|
// See https://llvm.org/LICENSE.txt for license information.
|
|
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
|
//
|
|
//===----------------------------------------------------------------------===//
|
|
// 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);
|
|
}
|
|
}
|
|
}
|
|
}
|