200 lines · cpp
1//===- unittests/Analysis/FlowSensitive/FormulaTest.cpp -------------------===//2//3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.4// See https://llvm.org/LICENSE.txt for license information.5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception6//7//===----------------------------------------------------------------------===//8 9#include "clang/Analysis/FlowSensitive/Formula.h"10#include "clang/Analysis/FlowSensitive/Arena.h"11#include "clang/Analysis/FlowSensitive/FormulaSerialization.h"12#include "llvm/Support/raw_ostream.h"13#include "llvm/Testing/Support/Error.h"14#include "gmock/gmock.h"15#include "gtest/gtest.h"16 17namespace {18 19using namespace clang;20using namespace dataflow;21 22using ::llvm::Failed;23using ::llvm::HasValue;24using ::llvm::Succeeded;25 26class SerializeFormulaTest : public ::testing::Test {27protected:28 Arena A;29 std::string Out;30 llvm::raw_string_ostream OS{Out};31 32 const Formula &A1 = A.makeAtomRef(A.makeAtom());33 const Formula &A2 = A.makeAtomRef(A.makeAtom());34};35 36TEST_F(SerializeFormulaTest, Atom) {37 serializeFormula(A1, OS);38 EXPECT_EQ(Out, "V0");39 Out = "";40 41 serializeFormula(A2, OS);42 EXPECT_EQ(Out, "V1");43}44 45TEST_F(SerializeFormulaTest, LiteralTrue) {46 serializeFormula(A.makeLiteral(true), OS);47 EXPECT_EQ(Out, "T");48}49 50TEST_F(SerializeFormulaTest, LiteralFalse) {51 serializeFormula(A.makeLiteral(false), OS);52 EXPECT_EQ(Out, "F");53}54 55TEST_F(SerializeFormulaTest, Not) {56 serializeFormula(A.makeNot(A1), OS);57 EXPECT_EQ(Out, "!V0");58}59 60TEST_F(SerializeFormulaTest, Or) {61 serializeFormula(A.makeOr(A1, A2), OS);62 EXPECT_EQ(Out, "|V0V1");63}64 65TEST_F(SerializeFormulaTest, And) {66 serializeFormula(A.makeAnd(A1, A2), OS);67 EXPECT_EQ(Out, "&V0V1");68}69 70TEST_F(SerializeFormulaTest, Implies) {71 serializeFormula(A.makeImplies(A1, A2), OS);72 EXPECT_EQ(Out, ">V0V1");73}74 75TEST_F(SerializeFormulaTest, Equal) {76 serializeFormula(A.makeEquals(A1, A2), OS);77 EXPECT_EQ(Out, "=V0V1");78}79 80TEST_F(SerializeFormulaTest, NestedBinaryUnary) {81 serializeFormula(A.makeEquals(A.makeOr(A1, A2), A2), OS);82 EXPECT_EQ(Out, "=|V0V1V1");83}84 85TEST_F(SerializeFormulaTest, NestedBinaryBinary) {86 serializeFormula(A.makeEquals(A.makeOr(A1, A2), A.makeAnd(A1, A2)), OS);87 EXPECT_EQ(Out, "=|V0V1&V0V1");88}89 90class ParseFormulaTest : public ::testing::Test {91protected:92 void SetUp() override {93 AtomMap[0] = Atom1;94 AtomMap[1] = Atom2;95 }96 97 // Convenience wrapper for `testParseFormula`.98 llvm::Expected<const Formula *> testParseFormula(llvm::StringRef Str) {99 return parseFormula(Str, A, AtomMap);100 }101 102 Arena A;103 std::string Out;104 llvm::raw_string_ostream OS{Out};105 106 Atom Atom1 = A.makeAtom();107 Atom Atom2 = A.makeAtom();108 const Formula &A1 = A.makeAtomRef(Atom1);109 const Formula &A2 = A.makeAtomRef(Atom2);110 llvm::DenseMap<unsigned, Atom> AtomMap;111};112 113TEST_F(ParseFormulaTest, Atom) {114 EXPECT_THAT_EXPECTED(testParseFormula("V0"), HasValue(&A1));115 EXPECT_THAT_EXPECTED(testParseFormula("V1"), HasValue(&A2));116}117 118TEST_F(ParseFormulaTest, LiteralTrue) {119 EXPECT_THAT_EXPECTED(testParseFormula("T"), HasValue(&A.makeLiteral(true)));120}121 122TEST_F(ParseFormulaTest, LiteralFalse) {123 EXPECT_THAT_EXPECTED(testParseFormula("F"), HasValue(&A.makeLiteral(false)));124}125 126TEST_F(ParseFormulaTest, Not) {127 EXPECT_THAT_EXPECTED(testParseFormula("!V0"), HasValue(&A.makeNot(A1)));128}129 130TEST_F(ParseFormulaTest, Or) {131 EXPECT_THAT_EXPECTED(testParseFormula("|V0V1"), HasValue(&A.makeOr(A1, A2)));132}133 134TEST_F(ParseFormulaTest, And) {135 EXPECT_THAT_EXPECTED(testParseFormula("&V0V1"), HasValue(&A.makeAnd(A1, A2)));136}137 138TEST_F(ParseFormulaTest, OutOfNumericOrder) {139 EXPECT_THAT_EXPECTED(testParseFormula("&V1V0"), HasValue(&A.makeAnd(A2, A1)));140}141 142TEST_F(ParseFormulaTest, Implies) {143 EXPECT_THAT_EXPECTED(testParseFormula(">V0V1"),144 HasValue(&A.makeImplies(A1, A2)));145}146 147TEST_F(ParseFormulaTest, Equal) {148 EXPECT_THAT_EXPECTED(testParseFormula("=V0V1"),149 HasValue(&A.makeEquals(A1, A2)));150}151 152TEST_F(ParseFormulaTest, NestedBinaryUnary) {153 EXPECT_THAT_EXPECTED(testParseFormula("=|V0V1V1"),154 HasValue(&A.makeEquals(A.makeOr(A1, A2), A2)));155}156 157TEST_F(ParseFormulaTest, NestedBinaryBinary) {158 EXPECT_THAT_EXPECTED(159 testParseFormula("=|V0V1&V0V1"),160 HasValue(&A.makeEquals(A.makeOr(A1, A2), A.makeAnd(A1, A2))));161}162 163// Verifies that parsing generates fresh atoms, if they are not already in the164// map.165TEST_F(ParseFormulaTest, GeneratesAtoms) {166 llvm::DenseMap<unsigned, Atom> FreshAtomMap;167 ASSERT_THAT_EXPECTED(parseFormula("=V0V1", A, FreshAtomMap), Succeeded());168 // The map contains two, unique elements.169 ASSERT_EQ(FreshAtomMap.size(), 2U);170 EXPECT_NE(FreshAtomMap[0], FreshAtomMap[1]);171}172 173TEST_F(ParseFormulaTest, MalformedFormulaFails) {174 // Arbitrary string.175 EXPECT_THAT_EXPECTED(testParseFormula("Hello"), Failed());176 // Empty string.177 EXPECT_THAT_EXPECTED(testParseFormula(""), Failed());178 // Malformed atom.179 EXPECT_THAT_EXPECTED(testParseFormula("Vabc"), Failed());180 // Irrelevant suffix.181 EXPECT_THAT_EXPECTED(testParseFormula("V0Hello"), Failed());182 EXPECT_THAT_EXPECTED(testParseFormula("=V0V1Hello"), Failed());183 // Sequence without operator.184 EXPECT_THAT_EXPECTED(testParseFormula("TF"), Failed());185 // Bad subformula.186 EXPECT_THAT_EXPECTED(testParseFormula("!G"), Failed());187 // Incomplete formulas.188 EXPECT_THAT_EXPECTED(testParseFormula("V"), Failed());189 EXPECT_THAT_EXPECTED(testParseFormula("&"), Failed());190 EXPECT_THAT_EXPECTED(testParseFormula("|"), Failed());191 EXPECT_THAT_EXPECTED(testParseFormula(">"), Failed());192 EXPECT_THAT_EXPECTED(testParseFormula("="), Failed());193 EXPECT_THAT_EXPECTED(testParseFormula("&V0"), Failed());194 EXPECT_THAT_EXPECTED(testParseFormula("|V0"), Failed());195 EXPECT_THAT_EXPECTED(testParseFormula(">V0"), Failed());196 EXPECT_THAT_EXPECTED(testParseFormula("=V0"), Failed());197}198 199} // namespace200