Skip to content

Commit 290f455

Browse files
authored
Consume solver results (#608)
* Change solver-config default to not implicitly record the ESG edges anymore * Allow moving the SolverResults out of the IDESolver * Move some more results code from IDESolver to SolverResults
1 parent 2a941ee commit 290f455

6 files changed

Lines changed: 279 additions & 130 deletions

File tree

include/phasar/DataFlow/IfdsIde/IFDSIDESolverConfig.h

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -63,9 +63,8 @@ struct IFDSIDESolverConfig {
6363
const IFDSIDESolverConfig &SC);
6464

6565
private:
66-
SolverConfigOptions Options = SolverConfigOptions::AutoAddZero |
67-
SolverConfigOptions::ComputeValues |
68-
SolverConfigOptions::RecordEdges;
66+
SolverConfigOptions Options =
67+
SolverConfigOptions::AutoAddZero | SolverConfigOptions::ComputeValues;
6968
};
7069

7170
} // namespace psr

include/phasar/DataFlow/IfdsIde/Solver/IDESolver.h

Lines changed: 35 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -50,14 +50,7 @@
5050
#include <unordered_set>
5151
#include <utility>
5252

53-
namespace llvm {
54-
class Instruction;
55-
class Value;
56-
} // namespace llvm
57-
5853
namespace psr {
59-
// For sorting the results in dumpResults()
60-
std::string getMetaDataID(const llvm::Value *V);
6154

6255
/// Solves the given IDETabulationProblem as described in the 1996 paper by
6356
/// Sagiv, Horwitz and Reps. To solve the problem, call solve(). Results
@@ -180,8 +173,8 @@ class IDESolver {
180173
}
181174

182175
/// Returns the L-type result for the given value at the given statement.
183-
[[nodiscard]] virtual l_t resultAt(n_t Stmt, d_t Value) {
184-
return ValTab.get(Stmt, Value);
176+
[[nodiscard]] l_t resultAt(n_t Stmt, d_t Value) {
177+
return getSolverResults().resultAt(Stmt, Value);
185178
}
186179

187180
/// Returns the L-type result at the given statement for the given data-flow
@@ -203,29 +196,15 @@ class IDESolver {
203196
[[nodiscard]] typename std::enable_if_t<
204197
std::is_same_v<std::remove_reference_t<NTy>, llvm::Instruction *>, l_t>
205198
resultAtInLLVMSSA(NTy Stmt, d_t Value) {
206-
if (Stmt->getType()->isVoidTy()) {
207-
return ValTab.get(Stmt, Value);
208-
}
209-
assert(Stmt->getNextNode() && "Expected to find a valid successor node!");
210-
return ValTab.get(Stmt->getNextNode(), Value);
199+
return getSolverResults().resultAtInLLVMSSA(Stmt, Value);
211200
}
212201

213202
/// Returns the resulting environment for the given statement.
214203
/// The artificial zero value can be automatically stripped.
215204
/// TOP values are never returned.
216205
[[nodiscard]] virtual std::unordered_map<d_t, l_t>
217206
resultsAt(n_t Stmt, bool StripZero = false) /*TODO const*/ {
218-
std::unordered_map<d_t, l_t> Result = ValTab.row(Stmt);
219-
if (StripZero) {
220-
for (auto It = Result.begin(); It != Result.end();) {
221-
if (IDEProblem.isZeroValue(It->first)) {
222-
It = Result.erase(It);
223-
} else {
224-
++It;
225-
}
226-
}
227-
}
228-
return Result;
207+
return getSolverResults().resultsAt(Stmt, StripZero);
229208
}
230209

231210
/// Returns the data-flow results at the given statement while respecting
@@ -248,23 +227,7 @@ class IDESolver {
248227
std::is_same_v<std::remove_reference_t<NTy>, llvm::Instruction *>,
249228
std::unordered_map<d_t, l_t>>
250229
resultsAtInLLVMSSA(NTy Stmt, bool StripZero = false) {
251-
std::unordered_map<d_t, l_t> Result = [this, Stmt]() {
252-
if (Stmt->getType()->isVoidTy()) {
253-
return ValTab.row(Stmt);
254-
}
255-
return ValTab.row(Stmt->getNextNode());
256-
}();
257-
if (StripZero) {
258-
// TODO: replace with std::erase_if (C++20)
259-
for (auto It = Result.begin(); It != Result.end();) {
260-
if (IDEProblem.isZeroValue(It->first)) {
261-
It = Result.erase(It);
262-
} else {
263-
++It;
264-
}
265-
}
266-
}
267-
return Result;
230+
return getSolverResults().resultsAtInLLVMSSA(Stmt, StripZero);
268231
}
269232

270233
virtual void emitTextReport(llvm::raw_ostream &OS = llvm::outs()) {
@@ -276,49 +239,7 @@ class IDESolver {
276239
}
277240

278241
void dumpResults(llvm::raw_ostream &OS = llvm::outs()) {
279-
PAMM_GET_INSTANCE;
280-
START_TIMER("DFA IDE Result Dumping", PAMM_SEVERITY_LEVEL::Full);
281-
OS << "\n***************************************************************\n"
282-
<< "* Raw IDESolver results *\n"
283-
<< "***************************************************************\n";
284-
auto Cells = this->ValTab.cellVec();
285-
if (Cells.empty()) {
286-
OS << "No results computed!" << '\n';
287-
} else {
288-
std::sort(
289-
Cells.begin(), Cells.end(), [](const auto &Lhs, const auto &Rhs) {
290-
if constexpr (std::is_same_v<n_t, const llvm::Instruction *>) {
291-
return StringIDLess{}(getMetaDataID(Lhs.getRowKey()),
292-
getMetaDataID(Rhs.getRowKey()));
293-
} else {
294-
// If non-LLVM IR is used
295-
return Lhs.getRowKey() < Rhs.getRowKey();
296-
}
297-
});
298-
n_t Prev = n_t{};
299-
n_t Curr = n_t{};
300-
f_t PrevFn = f_t{};
301-
f_t CurrFn = f_t{};
302-
for (unsigned I = 0; I < Cells.size(); ++I) {
303-
Curr = Cells[I].getRowKey();
304-
CurrFn = ICF->getFunctionOf(Curr);
305-
if (PrevFn != CurrFn) {
306-
PrevFn = CurrFn;
307-
OS << "\n\n============ Results for function '" +
308-
ICF->getFunctionName(CurrFn) + "' ============\n";
309-
}
310-
if (Prev != Curr) {
311-
Prev = Curr;
312-
std::string NString = IDEProblem.NtoString(Curr);
313-
std::string Line(NString.size(), '-');
314-
OS << "\n\nN: " << NString << "\n---" << Line << '\n';
315-
}
316-
OS << "\tD: " << IDEProblem.DtoString(Cells[I].getColumnKey())
317-
<< " | V: " << IDEProblem.LtoString(Cells[I].getValue()) << '\n';
318-
}
319-
}
320-
OS << '\n';
321-
STOP_TIMER("DFA IDE Result Dumping", PAMM_SEVERITY_LEVEL::Full);
242+
getSolverResults().dumpResults(*ICF, IDEProblem, OS);
322243
}
323244

324245
void dumpAllInterPathEdges() {
@@ -361,9 +282,24 @@ class IDESolver {
361282
}
362283
}
363284

364-
SolverResults<n_t, d_t, l_t> getSolverResults() {
365-
return SolverResults<n_t, d_t, l_t>(this->ValTab,
366-
IDEProblem.getZeroValue());
285+
/// Returns a view into the computed solver-results.
286+
///
287+
/// NOTE: The SolverResults store a reference into this IDESolver, so its
288+
/// lifetime is also bound to the lifetime of this solver. If you want to use
289+
/// the solverResults beyond the lifetime of this solver, use
290+
/// comsumeSolverResults() instead.
291+
[[nodiscard]] SolverResults<n_t, d_t, l_t> getSolverResults() noexcept {
292+
return SolverResults<n_t, d_t, l_t>(this->ValTab, ZeroValue);
293+
}
294+
295+
/// Moves the computed solver-results out of this solver such that the solver
296+
/// can be destroyed without that the analysis results are lost.
297+
/// Do not call any function (including getSolverResults()) on this IDESolver
298+
/// instance after that.
299+
[[nodiscard]] OwningSolverResults<n_t, d_t, l_t>
300+
consumeSolverResults() noexcept(std::is_nothrow_move_constructible_v<d_t>) {
301+
return OwningSolverResults<n_t, d_t, l_t>(std::move(this->ValTab),
302+
std::move(ZeroValue));
367303
}
368304

369305
protected:
@@ -1818,6 +1754,17 @@ template <typename Problem>
18181754
using IDESolver_P = IDESolver<typename Problem::ProblemAnalysisDomain,
18191755
typename Problem::container_type>;
18201756

1757+
template <typename AnalysisDomainTy, typename Container>
1758+
OwningSolverResults<typename AnalysisDomainTy::n_t,
1759+
typename AnalysisDomainTy::d_t,
1760+
typename AnalysisDomainTy::l_t>
1761+
solveIDEProblem(IDETabulationProblem<AnalysisDomainTy, Container> &Problem,
1762+
const typename AnalysisDomainTy::i_t &ICF) {
1763+
IDESolver<AnalysisDomainTy, Container> Solver(Problem, &ICF);
1764+
Solver.solve();
1765+
return Solver.consumeSolverResults();
1766+
}
1767+
18211768
} // namespace psr
18221769

18231770
#endif

include/phasar/DataFlow/IfdsIde/Solver/IFDSSolver.h

Lines changed: 21 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,10 @@
2828

2929
namespace psr {
3030

31-
template <typename AnalysisDomainTy>
32-
class IFDSSolver : public IDESolver<WithBinaryValueDomain<AnalysisDomainTy>> {
31+
template <typename AnalysisDomainTy,
32+
typename Container = std::set<typename AnalysisDomainTy::d_t>>
33+
class IFDSSolver
34+
: public IDESolver<WithBinaryValueDomain<AnalysisDomainTy>, Container> {
3335
public:
3436
using ProblemTy = IFDSTabulationProblem<AnalysisDomainTy>;
3537
using d_t = typename AnalysisDomainTy::d_t;
@@ -39,7 +41,8 @@ class IFDSSolver : public IDESolver<WithBinaryValueDomain<AnalysisDomainTy>> {
3941
template <typename IfdsDomainTy,
4042
typename = std::enable_if_t<
4143
std::is_base_of_v<IfdsDomainTy, AnalysisDomainTy>>>
42-
IFDSSolver(IFDSTabulationProblem<IfdsDomainTy> &IFDSProblem, const i_t *ICF)
44+
IFDSSolver(IFDSTabulationProblem<IfdsDomainTy, Container> &IFDSProblem,
45+
const i_t *ICF)
4346
: IDESolver<WithBinaryValueDomain<AnalysisDomainTy>>(IFDSProblem, ICF) {}
4447

4548
virtual ~IFDSSolver() = default;
@@ -96,10 +99,23 @@ class IFDSSolver : public IDESolver<WithBinaryValueDomain<AnalysisDomainTy>> {
9699

97100
template <typename Problem, typename ICF>
98101
IFDSSolver(Problem &, ICF *)
99-
-> IFDSSolver<typename Problem::ProblemAnalysisDomain>;
102+
-> IFDSSolver<typename Problem::ProblemAnalysisDomain,
103+
typename Problem::container_type>;
100104

101105
template <typename Problem>
102-
using IFDSSolver_P = IFDSSolver<typename Problem::ProblemAnalysisDomain>;
106+
using IFDSSolver_P = IFDSSolver<typename Problem::ProblemAnalysisDomain,
107+
typename Problem::container_type>;
108+
109+
template <typename AnalysisDomainTy, typename Container>
110+
OwningSolverResults<typename AnalysisDomainTy::n_t,
111+
typename AnalysisDomainTy::d_t,
112+
typename AnalysisDomainTy::l_t>
113+
solveIFDSProblem(IFDSTabulationProblem<AnalysisDomainTy, Container> &Problem,
114+
const typename AnalysisDomainTy::i_t &ICF) {
115+
IFDSSolver<AnalysisDomainTy, Container> Solver(Problem, &ICF);
116+
Solver.solve();
117+
return Solver.consumeSolverResults();
118+
}
103119

104120
} // namespace psr
105121

0 commit comments

Comments
 (0)