117 lines
3.1 KiB
C++
117 lines
3.1 KiB
C++
|
//===- 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/Formula.h"
|
||
|
#include "llvm/Support/ScopedPrinter.h"
|
||
|
#include "llvm/Support/raw_ostream.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) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto B = Ctx.atom();
|
||
|
|
||
|
auto Expected = "V0";
|
||
|
EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, Literal) {
|
||
|
ConstraintContext Ctx;
|
||
|
EXPECT_EQ("true", llvm::to_string(*Ctx.literal(true)));
|
||
|
EXPECT_EQ("false", llvm::to_string(*Ctx.literal(false)));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, Negation) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto B = Ctx.neg(Ctx.atom());
|
||
|
|
||
|
auto Expected = "!V0";
|
||
|
EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, Conjunction) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto *V0 = Ctx.atom();
|
||
|
auto *V1 = Ctx.atom();
|
||
|
EXPECT_EQ("(V0 & V1)", llvm::to_string(*Ctx.conj(V0, V1)));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, Disjunction) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto *V0 = Ctx.atom();
|
||
|
auto *V1 = Ctx.atom();
|
||
|
EXPECT_EQ("(V0 | V1)", llvm::to_string(*Ctx.disj(V0, V1)));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, Implication) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto *V0 = Ctx.atom();
|
||
|
auto *V1 = Ctx.atom();
|
||
|
EXPECT_EQ("(V0 => V1)", llvm::to_string(*Ctx.impl(V0, V1)));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, Iff) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto *V0 = Ctx.atom();
|
||
|
auto *V1 = Ctx.atom();
|
||
|
EXPECT_EQ("(V0 = V1)", llvm::to_string(*Ctx.iff(V0, V1)));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, Xor) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto V0 = Ctx.atom();
|
||
|
auto V1 = Ctx.atom();
|
||
|
auto B = Ctx.disj(Ctx.conj(V0, Ctx.neg(V1)), Ctx.conj(Ctx.neg(V0), V1));
|
||
|
|
||
|
auto Expected = "((V0 & !V1) | (!V0 & V1))";
|
||
|
EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, NestedBoolean) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto V0 = Ctx.atom();
|
||
|
auto V1 = Ctx.atom();
|
||
|
auto V2 = Ctx.atom();
|
||
|
auto V3 = Ctx.atom();
|
||
|
auto V4 = Ctx.atom();
|
||
|
auto B = Ctx.conj(V0, Ctx.disj(V1, Ctx.conj(V2, Ctx.disj(V3, V4))));
|
||
|
|
||
|
auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
|
||
|
EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
|
||
|
}
|
||
|
|
||
|
TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
|
||
|
ConstraintContext Ctx;
|
||
|
auto X = Ctx.atom();
|
||
|
auto Y = Ctx.atom();
|
||
|
Formula::AtomNames Names;
|
||
|
Names[X->getAtom()] = "X";
|
||
|
Names[Y->getAtom()] = "Y";
|
||
|
auto V2 = Ctx.atom();
|
||
|
auto V3 = Ctx.atom();
|
||
|
auto B = Ctx.disj(Ctx.conj(Y, V2), Ctx.disj(X, V3));
|
||
|
|
||
|
auto Expected = R"(((Y & V2) | (X | V3)))";
|
||
|
std::string Actual;
|
||
|
llvm::raw_string_ostream OS(Actual);
|
||
|
B->print(OS, &Names);
|
||
|
EXPECT_THAT(Actual, StrEq(Expected));
|
||
|
}
|
||
|
|
||
|
} // namespace
|