193 lines · cpp
1//===- ArenaTest.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/Arena.h"10#include "llvm/Support/ScopedPrinter.h"11#include "llvm/Testing/Support/Error.h"12#include "gmock/gmock.h"13#include "gtest/gtest.h"14 15namespace clang::dataflow {16namespace {17using llvm::HasValue;18using testing::Ref;19 20class ArenaTest : public ::testing::Test {21protected:22 Arena A;23};24 25TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {26 auto &X = A.makeAtomValue();27 auto &Y = A.makeAtomValue();28 EXPECT_NE(&X, &Y);29}30 31TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {32 auto &X = A.makeTopValue();33 auto &Y = A.makeTopValue();34 EXPECT_NE(&X, &Y);35}36 37TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {38 auto &X = A.makeAtomRef(A.makeAtom());39 auto &Y = A.makeAtomRef(A.makeAtom());40 auto &XAndY1 = A.makeAnd(X, Y);41 auto &XAndY2 = A.makeAnd(X, Y);42 EXPECT_EQ(&XAndY1, &XAndY2);43 44 auto &YAndX = A.makeAnd(Y, X);45 EXPECT_EQ(&XAndY1, &YAndX);46 47 auto &Z = A.makeAtomRef(A.makeAtom());48 auto &XAndZ = A.makeAnd(X, Z);49 EXPECT_NE(&XAndY1, &XAndZ);50}51 52TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {53 auto &X = A.makeAtomRef(A.makeAtom());54 auto &Y = A.makeAtomRef(A.makeAtom());55 auto &XOrY1 = A.makeOr(X, Y);56 auto &XOrY2 = A.makeOr(X, Y);57 EXPECT_EQ(&XOrY1, &XOrY2);58 59 auto &YOrX = A.makeOr(Y, X);60 EXPECT_EQ(&XOrY1, &YOrX);61 62 auto &Z = A.makeAtomRef(A.makeAtom());63 auto &XOrZ = A.makeOr(X, Z);64 EXPECT_NE(&XOrY1, &XOrZ);65}66 67TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {68 auto &X = A.makeAtomRef(A.makeAtom());69 auto &NotX1 = A.makeNot(X);70 auto &NotX2 = A.makeNot(X);71 EXPECT_EQ(&NotX1, &NotX2);72 auto &Y = A.makeAtomRef(A.makeAtom());73 auto &NotY = A.makeNot(Y);74 EXPECT_NE(&NotX1, &NotY);75}76 77TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {78 auto &X = A.makeAtomRef(A.makeAtom());79 auto &Y = A.makeAtomRef(A.makeAtom());80 auto &XImpliesY1 = A.makeImplies(X, Y);81 auto &XImpliesY2 = A.makeImplies(X, Y);82 EXPECT_EQ(&XImpliesY1, &XImpliesY2);83 84 auto &YImpliesX = A.makeImplies(Y, X);85 EXPECT_NE(&XImpliesY1, &YImpliesX);86 87 auto &Z = A.makeAtomRef(A.makeAtom());88 auto &XImpliesZ = A.makeImplies(X, Z);89 EXPECT_NE(&XImpliesY1, &XImpliesZ);90}91 92TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {93 auto &X = A.makeAtomRef(A.makeAtom());94 auto &Y = A.makeAtomRef(A.makeAtom());95 auto &XIffY1 = A.makeEquals(X, Y);96 auto &XIffY2 = A.makeEquals(X, Y);97 EXPECT_EQ(&XIffY1, &XIffY2);98 99 auto &YIffX = A.makeEquals(Y, X);100 EXPECT_EQ(&XIffY1, &YIffX);101 102 auto &Z = A.makeAtomRef(A.makeAtom());103 auto &XIffZ = A.makeEquals(X, Z);104 EXPECT_NE(&XIffY1, &XIffZ);105}106 107TEST_F(ArenaTest, Interning) {108 Atom X = A.makeAtom();109 Atom Y = A.makeAtom();110 const Formula &F1 = A.makeAnd(A.makeAtomRef(X), A.makeAtomRef(Y));111 const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X));112 EXPECT_EQ(&F1, &F2);113 BoolValue &B1 = A.makeBoolValue(F1);114 BoolValue &B2 = A.makeBoolValue(F2);115 EXPECT_EQ(&B1, &B2);116 EXPECT_EQ(&B1.formula(), &F1);117}118 119TEST_F(ArenaTest, ParseFormula) {120 Atom V5{5};121 Atom V6{6};122 EXPECT_THAT_EXPECTED(A.parseFormula("V5"), HasValue(Ref(A.makeAtomRef(V5))));123 EXPECT_THAT_EXPECTED(A.parseFormula("true"),124 HasValue(Ref(A.makeLiteral(true))));125 EXPECT_THAT_EXPECTED(A.parseFormula("!V5"),126 HasValue(Ref(A.makeNot(A.makeAtomRef(V5)))));127 128 EXPECT_THAT_EXPECTED(129 A.parseFormula("(V5 = V6)"),130 HasValue(Ref(A.makeEquals(A.makeAtomRef(V5), A.makeAtomRef(V6)))));131 EXPECT_THAT_EXPECTED(132 A.parseFormula("(V5 => V6)"),133 HasValue(Ref(A.makeImplies(A.makeAtomRef(V5), A.makeAtomRef(V6)))));134 EXPECT_THAT_EXPECTED(135 A.parseFormula("(V5 & V6)"),136 HasValue(Ref(A.makeAnd(A.makeAtomRef(V5), A.makeAtomRef(V6)))));137 EXPECT_THAT_EXPECTED(138 A.parseFormula("(V5 | V6)"),139 HasValue(Ref(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)))));140 141 EXPECT_THAT_EXPECTED(142 A.parseFormula("((V5 & (V6 & !false)) => ((V5 | V6) | false))"),143 HasValue(Ref(144 A.makeImplies(A.makeAnd(A.makeAtomRef(V5),145 A.makeAnd(A.makeAtomRef(V6),146 A.makeNot(A.makeLiteral(false)))),147 A.makeOr(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)),148 A.makeLiteral(false))))));149 150 EXPECT_THAT_EXPECTED(151 A.parseFormula("(V0 => error)"), llvm::FailedWithMessage(R"(bad formula at offset 7152(V0 => error)153 ^)"));154 EXPECT_THAT_EXPECTED(155 A.parseFormula("V1 V2"), llvm::FailedWithMessage(R"(bad formula at offset 3156V1 V2157 ^)"));158}159 160TEST_F(ArenaTest, IdentitySimplification) {161 auto &X = A.makeAtomRef(A.makeAtom());162 163 EXPECT_EQ(&X, &A.makeAnd(X, X));164 EXPECT_EQ(&X, &A.makeOr(X, X));165 EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X));166 EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X));167 EXPECT_EQ(&X, &A.makeNot(A.makeNot(X)));168}169 170TEST_F(ArenaTest, LiteralSimplification) {171 auto &X = A.makeAtomRef(A.makeAtom());172 173 EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true)));174 EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false)));175 176 EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true)));177 EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false)));178 179 EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true)));180 EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false)));181 EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X));182 EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X));183 184 EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true)));185 EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false)));186 187 EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true)));188 EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false)));189}190 191} // namespace192} // namespace clang::dataflow193