diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h index 373697dc7379c..4e07053aae1af 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Arena.h +++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h @@ -11,6 +11,7 @@ #include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/StorageLocation.h" #include "clang/Analysis/FlowSensitive/Value.h" +#include "llvm/ADT/StringRef.h" #include namespace clang::dataflow { @@ -109,6 +110,10 @@ class Arena { return makeAtomRef(Value ? True : False); } + // Parses a formula from its textual representation. + // This may refer to atoms that were not produced by makeAtom() yet! + llvm::Expected parseFormula(llvm::StringRef); + /// Returns a new atomic boolean variable, distinct from any other. Atom makeAtom() { return static_cast(NextAtom++); }; diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h index 64fe8f5b630a0..51264444fda84 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Formula.h +++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h @@ -18,7 +18,6 @@ #include "llvm/Support/raw_ostream.h" #include #include -#include namespace clang::dataflow { diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp index a12da2d9b555e..b043a52b609df 100644 --- a/clang/lib/Analysis/FlowSensitive/Arena.cpp +++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp @@ -7,7 +7,10 @@ //===----------------------------------------------------------------------===// #include "clang/Analysis/FlowSensitive/Arena.h" +#include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/Value.h" +#include "llvm/Support/Error.h" +#include namespace clang::dataflow { @@ -95,4 +98,96 @@ BoolValue &Arena::makeBoolValue(const Formula &F) { return *It->second; } +namespace { +const Formula *parse(Arena &A, llvm::StringRef &In) { + auto EatSpaces = [&] { In = In.ltrim(' '); }; + EatSpaces(); + + if (In.consume_front("!")) { + if (auto *Arg = parse(A, In)) + return &A.makeNot(*Arg); + return nullptr; + } + + if (In.consume_front("(")) { + auto *Arg1 = parse(A, In); + if (!Arg1) + return nullptr; + + EatSpaces(); + decltype(&Arena::makeOr) Op; + if (In.consume_front("|")) + Op = &Arena::makeOr; + else if (In.consume_front("&")) + Op = &Arena::makeAnd; + else if (In.consume_front("=>")) + Op = &Arena::makeImplies; + else if (In.consume_front("=")) + Op = &Arena::makeEquals; + else + return nullptr; + + auto *Arg2 = parse(A, In); + if (!Arg2) + return nullptr; + + EatSpaces(); + if (!In.consume_front(")")) + return nullptr; + + return &(A.*Op)(*Arg1, *Arg2); + } + + // For now, only support unnamed variables V0, V1 etc. + // FIXME: parse e.g. "X" by allocating an atom and storing a name somewhere. + if (In.consume_front("V")) { + std::underlying_type_t At; + if (In.consumeInteger(10, At)) + return nullptr; + return &A.makeAtomRef(static_cast(At)); + } + + if (In.consume_front("true")) + return &A.makeLiteral(true); + if (In.consume_front("false")) + return &A.makeLiteral(false); + + return nullptr; +} + +class FormulaParseError : public llvm::ErrorInfo { + std::string Formula; + unsigned Offset; + +public: + static char ID; + FormulaParseError(llvm::StringRef Formula, unsigned Offset) + : Formula(Formula), Offset(Offset) {} + + void log(raw_ostream &OS) const override { + OS << "bad formula at offset " << Offset << "\n"; + OS << Formula << "\n"; + OS.indent(Offset) << "^"; + } + + std::error_code convertToErrorCode() const override { + return std::make_error_code(std::errc::invalid_argument); + } +}; + +char FormulaParseError::ID = 0; + +} // namespace + +llvm::Expected Arena::parseFormula(llvm::StringRef In) { + llvm::StringRef Rest = In; + auto *Result = parse(*this, Rest); + if (!Result) // parse() hit something unparseable + return llvm::make_error(In, In.size() - Rest.size()); + Rest = Rest.ltrim(); + if (!Rest.empty()) // parse didn't consume all the input + return llvm::make_error(In, In.size() - Rest.size()); + return *Result; +} + } // namespace clang::dataflow diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp index 504ad2fb7938a..6d22efc5db07b 100644 --- a/clang/lib/Analysis/FlowSensitive/Formula.cpp +++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp @@ -13,6 +13,7 @@ #include "llvm/Support/Allocator.h" #include "llvm/Support/ErrorHandling.h" #include +#include namespace clang::dataflow { diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp index 0f8552a58787c..1208b78a308d1 100644 --- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp @@ -8,11 +8,14 @@ #include "clang/Analysis/FlowSensitive/Arena.h" #include "llvm/Support/ScopedPrinter.h" +#include "llvm/Testing/Support/Error.h" #include "gmock/gmock.h" #include "gtest/gtest.h" namespace clang::dataflow { namespace { +using llvm::HasValue; +using testing::Ref; class ArenaTest : public ::testing::Test { protected: @@ -137,5 +140,46 @@ TEST_F(ArenaTest, Interning) { EXPECT_EQ(&B1.formula(), &F1); } +TEST_F(ArenaTest, ParseFormula) { + Atom V5{5}; + Atom V6{6}; + EXPECT_THAT_EXPECTED(A.parseFormula("V5"), HasValue(Ref(A.makeAtomRef(V5)))); + EXPECT_THAT_EXPECTED(A.parseFormula("true"), + HasValue(Ref(A.makeLiteral(true)))); + EXPECT_THAT_EXPECTED(A.parseFormula("!V5"), + HasValue(Ref(A.makeNot(A.makeAtomRef(V5))))); + + EXPECT_THAT_EXPECTED( + A.parseFormula("(V5 = V6)"), + HasValue(Ref(A.makeEquals(A.makeAtomRef(V5), A.makeAtomRef(V6))))); + EXPECT_THAT_EXPECTED( + A.parseFormula("(V5 => V6)"), + HasValue(Ref(A.makeImplies(A.makeAtomRef(V5), A.makeAtomRef(V6))))); + EXPECT_THAT_EXPECTED( + A.parseFormula("(V5 & V6)"), + HasValue(Ref(A.makeAnd(A.makeAtomRef(V5), A.makeAtomRef(V6))))); + EXPECT_THAT_EXPECTED( + A.parseFormula("(V5 | V6)"), + HasValue(Ref(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6))))); + + EXPECT_THAT_EXPECTED( + A.parseFormula("((V5 & (V6 & !false)) => ((V5 | V6) | false))"), + HasValue(Ref( + A.makeImplies(A.makeAnd(A.makeAtomRef(V5), + A.makeAnd(A.makeAtomRef(V6), + A.makeNot(A.makeLiteral(false)))), + A.makeOr(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)), + A.makeLiteral(false)))))); + + EXPECT_THAT_EXPECTED( + A.parseFormula("(V0 => error)"), llvm::FailedWithMessage(R"(bad formula at offset 7 +(V0 => error) + ^)")); + EXPECT_THAT_EXPECTED( + A.parseFormula("V1 V2"), llvm::FailedWithMessage(R"(bad formula at offset 3 +V1 V2 + ^)")); +} + } // namespace } // namespace clang::dataflow diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp index e168f0ef1378e..a61e692088a87 100644 --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -9,12 +9,15 @@ #include #include "TestingSupport.h" +#include "clang/Analysis/FlowSensitive/Arena.h" #include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/Solver.h" #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h" +#include "clang/Basic/LLVM.h" #include "llvm/ADT/ArrayRef.h" #include "gmock/gmock.h" #include "gtest/gtest.h" +#include namespace { @@ -30,6 +33,21 @@ using testing::UnorderedElementsAre; constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue; constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse; +std::vector parseAll(Arena &A, StringRef Lines) { + std::vector Result; + while (!Lines.empty()) { + auto [First, Rest] = Lines.split('\n'); + Lines = Rest; + if (First.trim().empty()) + continue; + if (auto F = A.parseFormula(First)) + Result.push_back(&*F); + else + ADD_FAILURE() << llvm::toString(F.takeError()); + } + return Result; +} + // Checks if the conjunction of `Vals` is satisfiable and returns the // corresponding result. Solver::Result solve(llvm::ArrayRef Vals) { @@ -258,114 +276,71 @@ TEST(SolverTest, IffWithUnits) { } TEST(SolverTest, IffWithUnitsConflict) { - ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - auto XEqY = Ctx.iff(X, Y); - auto NotY = Ctx.neg(Y); - - // (X <=> Y) ^ X !Y - EXPECT_THAT(solve({XEqY, X, NotY}), unsat()); + Arena A; + auto Constraints = parseAll(A, R"( + (V0 = V1) + V0 + !V1 + )"); + EXPECT_THAT(solve(Constraints), unsat()); } TEST(SolverTest, IffTransitiveConflict) { - ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - auto Z = Ctx.atom(); - auto XEqY = Ctx.iff(X, Y); - auto YEqZ = Ctx.iff(Y, Z); - auto NotX = Ctx.neg(X); - - // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X - EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat()); + Arena A; + auto Constraints = parseAll(A, R"( + (V0 = V1) + (V1 = V2) + V2 + !V0 + )"); + EXPECT_THAT(solve(Constraints), unsat()); } TEST(SolverTest, DeMorgan) { - ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - auto Z = Ctx.atom(); - auto W = Ctx.atom(); - - // !(X v Y) <=> !X ^ !Y - auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y))); - - // !(Z ^ W) <=> !Z v !W - auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W))); - - // A ^ B - EXPECT_THAT(solve({A, B}), sat(_)); + Arena A; + auto Constraints = parseAll(A, R"( + (!(V0 | V1) = (!V0 & !V1)) + (!(V2 & V3) = (!V2 | !V3)) + )"); + EXPECT_THAT(solve(Constraints), sat(_)); } TEST(SolverTest, RespectsAdditionalConstraints) { - ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - auto XEqY = Ctx.iff(X, Y); - auto NotY = Ctx.neg(Y); - - // (X <=> Y) ^ X ^ !Y - EXPECT_THAT(solve({XEqY, X, NotY}), unsat()); + Arena A; + auto Constraints = parseAll(A, R"( + (V0 = V1) + V0 + !V1 + )"); + EXPECT_THAT(solve(Constraints), unsat()); } TEST(SolverTest, ImplicationIsEquivalentToDNF) { - ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - auto XImpliesY = Ctx.impl(X, Y); - auto XImpliesYDNF = Ctx.disj(Ctx.neg(X), Y); - auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF)); - - // !((X => Y) <=> (!X v Y)) - EXPECT_THAT(solve({NotEquivalent}), unsat()); + Arena A; + auto Constraints = parseAll(A, R"( + !((V0 => V1) = (!V0 | V1)) + )"); + EXPECT_THAT(solve(Constraints), unsat()); } TEST(SolverTest, ImplicationConflict) { - ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - auto *XImplY = Ctx.impl(X, Y); - auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y)); - - // X => Y ^ X ^ !Y - EXPECT_THAT(solve({XImplY, XAndNotY}), unsat()); -} - -TEST(SolverTest, LowTimeoutResultsInTimedOut) { - WatchedLiteralsSolver solver(10); - ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - auto Z = Ctx.atom(); - auto W = Ctx.atom(); - - // !(X v Y) <=> !X ^ !Y - auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y))); - - // !(Z ^ W) <=> !Z v !W - auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W))); - - // A ^ B - EXPECT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut); + Arena A; + auto Constraints = parseAll(A, R"( + (V0 => V1) + (V0 & !V1) + )"); + EXPECT_THAT(solve(Constraints), unsat()); } TEST(SolverTest, ReachedLimitsReflectsTimeouts) { + Arena A; + auto Constraints = parseAll(A, R"( + (!(V0 | V1) = (!V0 & !V1)) + (!(V2 & V3) = (!V2 & !V3)) + )"); WatchedLiteralsSolver solver(10); - ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - auto Z = Ctx.atom(); - auto W = Ctx.atom(); - - // !(X v Y) <=> !X ^ !Y - auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y))); - - // !(Z ^ W) <=> !Z v !W - auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W))); - - // A ^ B - ASSERT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut); + ASSERT_EQ(solver.solve(Constraints).getStatus(), + Solver::Result::Status::TimedOut); EXPECT_TRUE(solver.reachedLimit()); }