forked from OSchip/llvm-project
[clang][dataflow] Generate readable form of boolean values.
Differential Revision: https://reviews.llvm.org/D129547
This commit is contained in:
parent
1e9cd04d7b
commit
c9666d2339
|
@ -129,6 +129,7 @@ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
|
|||
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
|
||||
clang/include/clang/Analysis/FlowSensitive/DataflowLattice.h
|
||||
clang/include/clang/Analysis/FlowSensitive/DataflowWorklist.h
|
||||
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
|
||||
clang/include/clang/Analysis/FlowSensitive/MapLattice.h
|
||||
clang/include/clang/Analysis/FlowSensitive/MatchSwitch.h
|
||||
clang/include/clang/Analysis/FlowSensitive/NoopLattice.h
|
||||
|
@ -309,6 +310,7 @@ clang/lib/Analysis/CodeInjector.cpp
|
|||
clang/lib/Analysis/FlowSensitive/ControlFlowContext.cpp
|
||||
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
|
||||
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
|
||||
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
|
||||
clang/lib/Analysis/FlowSensitive/Transfer.cpp
|
||||
clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
|
||||
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
|
||||
|
|
|
@ -0,0 +1,39 @@
|
|||
//===-- DebugSupport.h ------------------------------------------*- 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 functions which generate more readable forms of data
|
||||
// structures used in the dataflow analyses, for debugging purposes.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
|
||||
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
|
||||
|
||||
#include <string>
|
||||
|
||||
#include "clang/Analysis/FlowSensitive/Value.h"
|
||||
#include "llvm/ADT/DenseMap.h"
|
||||
|
||||
namespace clang {
|
||||
namespace dataflow {
|
||||
/// Returns a string representation for the boolean value `B`.
|
||||
///
|
||||
/// Atomic booleans appearing in the boolean value `B` are assigned to labels
|
||||
/// either specified in `AtomNames` or created by default rules as B0, B1, ...
|
||||
///
|
||||
/// Requirements:
|
||||
///
|
||||
/// Names assigned to atoms should not be repeated in `AtomNames`.
|
||||
std::string debugString(
|
||||
const BoolValue &B,
|
||||
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
|
||||
|
||||
} // namespace dataflow
|
||||
} // namespace clang
|
||||
|
||||
#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
|
|
@ -5,6 +5,7 @@ add_clang_library(clangAnalysisFlowSensitive
|
|||
Transfer.cpp
|
||||
TypeErasedDataflowAnalysis.cpp
|
||||
WatchedLiteralsSolver.cpp
|
||||
DebugSupport.cpp
|
||||
|
||||
LINK_LIBS
|
||||
clangAnalysis
|
||||
|
|
|
@ -0,0 +1,106 @@
|
|||
//===- DebugSupport.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 functions which generate more readable forms of data
|
||||
// structures used in the dataflow analyses, for debugging purposes.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
|
||||
#include "clang/Analysis/FlowSensitive/Value.h"
|
||||
#include "llvm/ADT/DenseMap.h"
|
||||
#include "llvm/ADT/StringSet.h"
|
||||
#include "llvm/Support/ErrorHandling.h"
|
||||
#include "llvm/Support/FormatAdapters.h"
|
||||
#include "llvm/Support/FormatVariadic.h"
|
||||
|
||||
namespace clang {
|
||||
namespace dataflow {
|
||||
|
||||
using llvm::fmt_pad;
|
||||
using llvm::formatv;
|
||||
|
||||
namespace {
|
||||
|
||||
class DebugStringGenerator {
|
||||
public:
|
||||
explicit DebugStringGenerator(
|
||||
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
|
||||
: Counter(0), AtomNames(std::move(AtomNamesArg)) {
|
||||
#ifndef NDEBUG
|
||||
llvm::StringSet<> Names;
|
||||
for (auto &N : AtomNames) {
|
||||
assert(Names.insert(N.second).second &&
|
||||
"The same name must not assigned to different atoms");
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
/// Returns a string representation of a boolean value `B`.
|
||||
std::string debugString(const BoolValue &B, size_t Depth = 0) {
|
||||
std::string S;
|
||||
switch (B.getKind()) {
|
||||
case Value::Kind::AtomicBool: {
|
||||
S = getAtomName(&cast<AtomicBoolValue>(B));
|
||||
break;
|
||||
}
|
||||
case Value::Kind::Conjunction: {
|
||||
auto &C = cast<ConjunctionValue>(B);
|
||||
auto L = debugString(C.getLeftSubValue(), Depth + 1);
|
||||
auto R = debugString(C.getRightSubValue(), Depth + 1);
|
||||
S = formatv("(and\n{0}\n{1})", L, R);
|
||||
break;
|
||||
}
|
||||
case Value::Kind::Disjunction: {
|
||||
auto &D = cast<DisjunctionValue>(B);
|
||||
auto L = debugString(D.getLeftSubValue(), Depth + 1);
|
||||
auto R = debugString(D.getRightSubValue(), Depth + 1);
|
||||
S = formatv("(or\n{0}\n{1})", L, R);
|
||||
break;
|
||||
}
|
||||
case Value::Kind::Negation: {
|
||||
auto &N = cast<NegationValue>(B);
|
||||
S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
|
||||
break;
|
||||
}
|
||||
default:
|
||||
llvm_unreachable("Unhandled value kind");
|
||||
}
|
||||
auto Indent = Depth * 4;
|
||||
return formatv("{0}", fmt_pad(S, Indent, 0));
|
||||
}
|
||||
|
||||
private:
|
||||
/// Returns the name assigned to `Atom`, either user-specified or created by
|
||||
/// default rules (B0, B1, ...).
|
||||
std::string getAtomName(const AtomicBoolValue *Atom) {
|
||||
auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
|
||||
if (Entry.second) {
|
||||
Counter++;
|
||||
}
|
||||
return Entry.first->second;
|
||||
}
|
||||
|
||||
// Keep track of number of atoms without a user-specified name, used to assign
|
||||
// non-repeating default names to such atoms.
|
||||
size_t Counter;
|
||||
|
||||
// Keep track of names assigned to atoms.
|
||||
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
|
||||
};
|
||||
|
||||
} // namespace
|
||||
|
||||
std::string
|
||||
debugString(const BoolValue &B,
|
||||
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
|
||||
return DebugStringGenerator(std::move(AtomNames)).debugString(B);
|
||||
}
|
||||
|
||||
} // namespace dataflow
|
||||
} // namespace clang
|
|
@ -7,6 +7,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
|
|||
ChromiumCheckModelTest.cpp
|
||||
DataflowAnalysisContextTest.cpp
|
||||
DataflowEnvironmentTest.cpp
|
||||
DebugSupportTest.cpp
|
||||
MapLatticeTest.cpp
|
||||
MatchSwitchTest.cpp
|
||||
MultiVarConstantPropagationTest.cpp
|
||||
|
|
|
@ -0,0 +1,190 @@
|
|||
//===- unittests/Analysis/FlowSensitive/DebugSupportTest.cpp --------------===//
|
||||
//
|
||||
// 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
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
|
||||
#include "TestingSupport.h"
|
||||
#include "clang/Analysis/FlowSensitive/Value.h"
|
||||
#include "gmock/gmock.h"
|
||||
#include "gtest/gtest.h"
|
||||
|
||||
namespace {
|
||||
|
||||
using namespace clang;
|
||||
using namespace dataflow;
|
||||
|
||||
using test::ConstraintContext;
|
||||
using testing::StrEq;
|
||||
|
||||
TEST(BoolValueDebugStringTest, AtomicBoolean) {
|
||||
// B0
|
||||
ConstraintContext Ctx;
|
||||
auto B = Ctx.atom();
|
||||
|
||||
auto Expected = R"(B0)";
|
||||
debugString(*B);
|
||||
EXPECT_THAT(debugString(*B), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, Negation) {
|
||||
// !B0
|
||||
ConstraintContext Ctx;
|
||||
auto B = Ctx.neg(Ctx.atom());
|
||||
|
||||
auto Expected = R"((not
|
||||
B0))";
|
||||
EXPECT_THAT(debugString(*B), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, Conjunction) {
|
||||
// B0 ^ B1
|
||||
ConstraintContext Ctx;
|
||||
auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
|
||||
|
||||
auto Expected = R"((and
|
||||
B0
|
||||
B1))";
|
||||
EXPECT_THAT(debugString(*B), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, Disjunction) {
|
||||
// B0 v B1
|
||||
ConstraintContext Ctx;
|
||||
auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
|
||||
|
||||
auto Expected = R"((or
|
||||
B0
|
||||
B1))";
|
||||
EXPECT_THAT(debugString(*B), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, Implication) {
|
||||
// B0 => B1, implemented as !B0 v B1
|
||||
ConstraintContext Ctx;
|
||||
auto B = Ctx.disj(Ctx.neg(Ctx.atom()), Ctx.atom());
|
||||
|
||||
auto Expected = R"((or
|
||||
(not
|
||||
B0)
|
||||
B1))";
|
||||
EXPECT_THAT(debugString(*B), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, Iff) {
|
||||
// B0 <=> B1, implemented as (!B0 v B1) ^ (B0 v !B1)
|
||||
ConstraintContext Ctx;
|
||||
auto B0 = Ctx.atom();
|
||||
auto B1 = Ctx.atom();
|
||||
auto B = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
|
||||
|
||||
auto Expected = R"((and
|
||||
(or
|
||||
(not
|
||||
B0)
|
||||
B1)
|
||||
(or
|
||||
B0
|
||||
(not
|
||||
B1))))";
|
||||
EXPECT_THAT(debugString(*B), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, Xor) {
|
||||
// (B0 ^ !B1) V (!B0 ^ B1)
|
||||
ConstraintContext Ctx;
|
||||
auto B0 = Ctx.atom();
|
||||
auto B1 = Ctx.atom();
|
||||
auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
|
||||
|
||||
auto Expected = R"((or
|
||||
(and
|
||||
B0
|
||||
(not
|
||||
B1))
|
||||
(and
|
||||
(not
|
||||
B0)
|
||||
B1)))";
|
||||
EXPECT_THAT(debugString(*B), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, NestedBoolean) {
|
||||
// B0 ^ (B1 v (B2 ^ (B3 v B4)))
|
||||
ConstraintContext Ctx;
|
||||
auto B = Ctx.conj(
|
||||
Ctx.atom(),
|
||||
Ctx.disj(Ctx.atom(),
|
||||
Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
|
||||
|
||||
auto Expected = R"((and
|
||||
B0
|
||||
(or
|
||||
B1
|
||||
(and
|
||||
B2
|
||||
(or
|
||||
B3
|
||||
B4)))))";
|
||||
EXPECT_THAT(debugString(*B), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
|
||||
// True
|
||||
ConstraintContext Ctx;
|
||||
auto True = cast<AtomicBoolValue>(Ctx.atom());
|
||||
auto B = True;
|
||||
|
||||
auto Expected = R"(True)";
|
||||
EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
|
||||
// (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
|
||||
ConstraintContext Ctx;
|
||||
auto Cond = cast<AtomicBoolValue>(Ctx.atom());
|
||||
auto Then = cast<AtomicBoolValue>(Ctx.atom());
|
||||
auto Else = cast<AtomicBoolValue>(Ctx.atom());
|
||||
auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
|
||||
Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
|
||||
|
||||
auto Expected = R"((or
|
||||
(and
|
||||
Cond
|
||||
(and
|
||||
Then
|
||||
(not
|
||||
Else)))
|
||||
(and
|
||||
(not
|
||||
Cond)
|
||||
(and
|
||||
(not
|
||||
Then)
|
||||
Else))))";
|
||||
EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
|
||||
StrEq(Expected));
|
||||
}
|
||||
|
||||
TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
|
||||
// (False && B0) v (True v B1)
|
||||
ConstraintContext Ctx;
|
||||
auto True = cast<AtomicBoolValue>(Ctx.atom());
|
||||
auto False = cast<AtomicBoolValue>(Ctx.atom());
|
||||
auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
|
||||
|
||||
auto Expected = R"((or
|
||||
(and
|
||||
False
|
||||
B0)
|
||||
(or
|
||||
True
|
||||
B1)))";
|
||||
EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
|
||||
StrEq(Expected));
|
||||
}
|
||||
|
||||
} // namespace
|
|
@ -12,5 +12,6 @@ static_library("FlowSensitive") {
|
|||
"Transfer.cpp",
|
||||
"TypeErasedDataflowAnalysis.cpp",
|
||||
"WatchedLiteralsSolver.cpp",
|
||||
"DebugSupport.cpp",
|
||||
]
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue