Skip to content

Commit 3f78d6a

Browse files
sam-mccallsam-mccall
authored
[dataflow] Parse formulas from text (#66424)
My immediate use for this is not in checked-in code, but rather the ability to plug printed flow conditions (from analysis logs) back into sat solver unittests to reproduce slowness. It does allow simplifying some of the existing solver tests, though.
1 parent b2bbf69 commit 3f78d6a

File tree

6 files changed

+209
-90
lines changed

6 files changed

+209
-90
lines changed

‎clang/include/clang/Analysis/FlowSensitive/Arena.h‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
#include "clang/Analysis/FlowSensitive/Formula.h"
1212
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
1313
#include "clang/Analysis/FlowSensitive/Value.h"
14+
#include "llvm/ADT/StringRef.h"
1415
#include <vector>
1516

1617
namespace clang::dataflow {
@@ -109,6 +110,10 @@ class Arena {
109110
return makeAtomRef(Value ? True : False);
110111
}
111112

113+
// Parses a formula from its textual representation.
114+
// This may refer to atoms that were not produced by makeAtom() yet!
115+
llvm::Expected<const Formula &> parseFormula(llvm::StringRef);
116+
112117
/// Returns a new atomic boolean variable, distinct from any other.
113118
Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
114119

‎clang/include/clang/Analysis/FlowSensitive/Formula.h‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@
1818
#include "llvm/Support/raw_ostream.h"
1919
#include <cassert>
2020
#include <string>
21-
#include <type_traits>
2221

2322
namespace clang::dataflow {
2423

‎clang/lib/Analysis/FlowSensitive/Arena.cpp‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,10 @@
77
//===----------------------------------------------------------------------===//
88

99
#include "clang/Analysis/FlowSensitive/Arena.h"
10+
#include "clang/Analysis/FlowSensitive/Formula.h"
1011
#include "clang/Analysis/FlowSensitive/Value.h"
12+
#include "llvm/Support/Error.h"
13+
#include <string>
1114

1215
namespace clang::dataflow {
1316

@@ -95,4 +98,96 @@ BoolValue &Arena::makeBoolValue(const Formula &F) {
9598
return *It->second;
9699
}
97100

101+
namespace {
102+
const Formula *parse(Arena &A, llvm::StringRef &In) {
103+
auto EatSpaces = [&] { In = In.ltrim(' '); };
104+
EatSpaces();
105+
106+
if (In.consume_front("!")) {
107+
if (auto *Arg = parse(A, In))
108+
return &A.makeNot(*Arg);
109+
return nullptr;
110+
}
111+
112+
if (In.consume_front("(")) {
113+
auto *Arg1 = parse(A, In);
114+
if (!Arg1)
115+
return nullptr;
116+
117+
EatSpaces();
118+
decltype(&Arena::makeOr) Op;
119+
if (In.consume_front("|"))
120+
Op = &Arena::makeOr;
121+
else if (In.consume_front("&"))
122+
Op = &Arena::makeAnd;
123+
else if (In.consume_front("=>"))
124+
Op = &Arena::makeImplies;
125+
else if (In.consume_front("="))
126+
Op = &Arena::makeEquals;
127+
else
128+
return nullptr;
129+
130+
auto *Arg2 = parse(A, In);
131+
if (!Arg2)
132+
return nullptr;
133+
134+
EatSpaces();
135+
if (!In.consume_front(")"))
136+
return nullptr;
137+
138+
return &(A.*Op)(*Arg1, *Arg2);
139+
}
140+
141+
// For now, only support unnamed variables V0, V1 etc.
142+
// FIXME: parse e.g. "X" by allocating an atom and storing a name somewhere.
143+
if (In.consume_front("V")) {
144+
std::underlying_type_t<Atom> At;
145+
if (In.consumeInteger(10, At))
146+
return nullptr;
147+
return &A.makeAtomRef(static_cast<Atom>(At));
148+
}
149+
150+
if (In.consume_front("true"))
151+
return &A.makeLiteral(true);
152+
if (In.consume_front("false"))
153+
return &A.makeLiteral(false);
154+
155+
return nullptr;
156+
}
157+
158+
class FormulaParseError : public llvm::ErrorInfo<FormulaParseError> {
159+
std::string Formula;
160+
unsigned Offset;
161+
162+
public:
163+
static char ID;
164+
FormulaParseError(llvm::StringRef Formula, unsigned Offset)
165+
: Formula(Formula), Offset(Offset) {}
166+
167+
void log(raw_ostream &OS) const override {
168+
OS << "bad formula at offset " << Offset << "\n";
169+
OS << Formula << "\n";
170+
OS.indent(Offset) << "^";
171+
}
172+
173+
std::error_code convertToErrorCode() const override {
174+
return std::make_error_code(std::errc::invalid_argument);
175+
}
176+
};
177+
178+
char FormulaParseError::ID = 0;
179+
180+
} // namespace
181+
182+
llvm::Expected<const Formula &> Arena::parseFormula(llvm::StringRef In) {
183+
llvm::StringRef Rest = In;
184+
auto *Result = parse(*this, Rest);
185+
if (!Result) // parse() hit something unparseable
186+
return llvm::make_error<FormulaParseError>(In, In.size() - Rest.size());
187+
Rest = Rest.ltrim();
188+
if (!Rest.empty()) // parse didn't consume all the input
189+
return llvm::make_error<FormulaParseError>(In, In.size() - Rest.size());
190+
return *Result;
191+
}
192+
98193
} // namespace clang::dataflow

‎clang/lib/Analysis/FlowSensitive/Formula.cpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
#include "llvm/Support/Allocator.h"
1414
#include "llvm/Support/ErrorHandling.h"
1515
#include <cassert>
16+
#include <type_traits>
1617

1718
namespace clang::dataflow {
1819

‎clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,14 @@
88

99
#include "clang/Analysis/FlowSensitive/Arena.h"
1010
#include "llvm/Support/ScopedPrinter.h"
11+
#include "llvm/Testing/Support/Error.h"
1112
#include "gmock/gmock.h"
1213
#include "gtest/gtest.h"
1314

1415
namespace clang::dataflow {
1516
namespace {
17+
using llvm::HasValue;
18+
using testing::Ref;
1619

1720
class ArenaTest : public ::testing::Test {
1821
protected:
@@ -137,5 +140,46 @@ TEST_F(ArenaTest, Interning) {
137140
EXPECT_EQ(&B1.formula(), &F1);
138141
}
139142

143+
TEST_F(ArenaTest, ParseFormula) {
144+
Atom V5{5};
145+
Atom V6{6};
146+
EXPECT_THAT_EXPECTED(A.parseFormula("V5"), HasValue(Ref(A.makeAtomRef(V5))));
147+
EXPECT_THAT_EXPECTED(A.parseFormula("true"),
148+
HasValue(Ref(A.makeLiteral(true))));
149+
EXPECT_THAT_EXPECTED(A.parseFormula("!V5"),
150+
HasValue(Ref(A.makeNot(A.makeAtomRef(V5)))));
151+
152+
EXPECT_THAT_EXPECTED(
153+
A.parseFormula("(V5 = V6)"),
154+
HasValue(Ref(A.makeEquals(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
155+
EXPECT_THAT_EXPECTED(
156+
A.parseFormula("(V5 => V6)"),
157+
HasValue(Ref(A.makeImplies(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
158+
EXPECT_THAT_EXPECTED(
159+
A.parseFormula("(V5 & V6)"),
160+
HasValue(Ref(A.makeAnd(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
161+
EXPECT_THAT_EXPECTED(
162+
A.parseFormula("(V5 | V6)"),
163+
HasValue(Ref(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)))));
164+
165+
EXPECT_THAT_EXPECTED(
166+
A.parseFormula("((V5 & (V6 & !false)) => ((V5 | V6) | false))"),
167+
HasValue(Ref(
168+
A.makeImplies(A.makeAnd(A.makeAtomRef(V5),
169+
A.makeAnd(A.makeAtomRef(V6),
170+
A.makeNot(A.makeLiteral(false)))),
171+
A.makeOr(A.makeOr(A.makeAtomRef(V5), A.makeAtomRef(V6)),
172+
A.makeLiteral(false))))));
173+
174+
EXPECT_THAT_EXPECTED(
175+
A.parseFormula("(V0 => error)"), llvm::FailedWithMessage(R"(bad formula at offset 7
176+
(V0 => error)
177+
^)"));
178+
EXPECT_THAT_EXPECTED(
179+
A.parseFormula("V1 V2"), llvm::FailedWithMessage(R"(bad formula at offset 3
180+
V1 V2
181+
^)"));
182+
}
183+
140184
} // namespace
141185
} // namespace clang::dataflow

0 commit comments

Comments
 (0)