1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
//===- 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, 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 True = Ctx.atom();
auto False = Ctx.atom();
auto V2 = Ctx.atom();
auto V3 = Ctx.atom();
Formula::AtomNames Names;
Names[True->getAtom()] = "true";
Names[False->getAtom()] = "false";
auto B = Ctx.disj(Ctx.conj(False, V2), Ctx.disj(True, V3));
auto Expected = R"(((false & V2) | (true | V3)))";
std::string Actual;
llvm::raw_string_ostream OS(Actual);
B->print(OS, &Names);
EXPECT_THAT(Actual, StrEq(Expected));
}
} // namespace
|
