diff options
author | thegeorg <thegeorg@yandex-team.com> | 2024-03-13 13:58:24 +0300 |
---|---|---|
committer | thegeorg <thegeorg@yandex-team.com> | 2024-03-13 14:11:53 +0300 |
commit | 11a895b7e15d1c5a1f52706396b82e3f9db953cb (patch) | |
tree | fabc6d883b0f946151f61ae7865cee9f529a1fdd /contrib/libs/clang16/lib/Analysis/ThreadSafetyLogical.cpp | |
parent | 9685917341315774aad5733b1793b1e533a88bbb (diff) | |
download | ydb-11a895b7e15d1c5a1f52706396b82e3f9db953cb.tar.gz |
Export clang-format16 via ydblib project
6e6be3a95868fde888d801b7590af4044049563f
Diffstat (limited to 'contrib/libs/clang16/lib/Analysis/ThreadSafetyLogical.cpp')
-rw-r--r-- | contrib/libs/clang16/lib/Analysis/ThreadSafetyLogical.cpp | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/contrib/libs/clang16/lib/Analysis/ThreadSafetyLogical.cpp b/contrib/libs/clang16/lib/Analysis/ThreadSafetyLogical.cpp new file mode 100644 index 0000000000..ac73077009 --- /dev/null +++ b/contrib/libs/clang16/lib/Analysis/ThreadSafetyLogical.cpp @@ -0,0 +1,111 @@ +//===- 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); +} +} +} +} |