Skip to content

Consume solver results #608

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MMory merged 3 commits into from
Apr 20, 2023
Merged

Consume solver results #608

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8f4cdaf
Change solver-config default to not implicitly record the ESG edges a…
fabianbs96 Apr 3, 2023
13e2787
Allow moving the SolverResults out of the IDESolver
fabianbs96 Apr 3, 2023
37844a9
Move some more results code from IDESolver to SolverResults
fabianbs96 Apr 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions include/phasar/DataFlow/IfdsIde/IFDSIDESolverConfig.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,9 +63,8 @@ struct IFDSIDESolverConfig {
const IFDSIDESolverConfig &SC);

private:
SolverConfigOptions Options = SolverConfigOptions::AutoAddZero |
SolverConfigOptions::ComputeValues |
SolverConfigOptions::RecordEdges;
SolverConfigOptions Options =
SolverConfigOptions::AutoAddZero | SolverConfigOptions::ComputeValues;
};

} // namespace psr
Expand Down
123 changes: 35 additions & 88 deletions include/phasar/DataFlow/IfdsIde/Solver/IDESolver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,14 +50,7 @@
#include <unordered_set>
#include <utility>

namespace llvm {
class Instruction;
class Value;
} // namespace llvm

namespace psr {
// For sorting the results in dumpResults()
std::string getMetaDataID(const llvm::Value *V);

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

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

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

/// Returns the resulting environment for the given statement.
/// The artificial zero value can be automatically stripped.
/// TOP values are never returned.
[[nodiscard]] virtual std::unordered_map<d_t, l_t>
resultsAt(n_t Stmt, bool StripZero = false) /*TODO const*/ {
std::unordered_map<d_t, l_t> Result = ValTab.row(Stmt);
if (StripZero) {
for (auto It = Result.begin(); It != Result.end();) {
if (IDEProblem.isZeroValue(It->first)) {
It = Result.erase(It);
} else {
++It;
}
}
}
return Result;
return getSolverResults().resultsAt(Stmt, StripZero);
}

/// Returns the data-flow results at the given statement while respecting
Expand All @@ -248,23 +227,7 @@ class IDESolver {
std::is_same_v<std::remove_reference_t<NTy>, llvm::Instruction *>,
std::unordered_map<d_t, l_t>>
resultsAtInLLVMSSA(NTy Stmt, bool StripZero = false) {
std::unordered_map<d_t, l_t> Result = [this, Stmt]() {
if (Stmt->getType()->isVoidTy()) {
return ValTab.row(Stmt);
}
return ValTab.row(Stmt->getNextNode());
}();
if (StripZero) {
// TODO: replace with std::erase_if (C++20)
for (auto It = Result.begin(); It != Result.end();) {
if (IDEProblem.isZeroValue(It->first)) {
It = Result.erase(It);
} else {
++It;
}
}
}
return Result;
return getSolverResults().resultsAtInLLVMSSA(Stmt, StripZero);
}

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

void dumpResults(llvm::raw_ostream &OS = llvm::outs()) {
PAMM_GET_INSTANCE;
START_TIMER("DFA IDE Result Dumping", PAMM_SEVERITY_LEVEL::Full);
OS << "\n***************************************************************\n"
<< "* Raw IDESolver results *\n"
<< "***************************************************************\n";
auto Cells = this->ValTab.cellVec();
if (Cells.empty()) {
OS << "No results computed!" << '\n';
} else {
std::sort(
Cells.begin(), Cells.end(), [](const auto &Lhs, const auto &Rhs) {
if constexpr (std::is_same_v<n_t, const llvm::Instruction *>) {
return StringIDLess{}(getMetaDataID(Lhs.getRowKey()),
getMetaDataID(Rhs.getRowKey()));
} else {
// If non-LLVM IR is used
return Lhs.getRowKey() < Rhs.getRowKey();
}
});
n_t Prev = n_t{};
n_t Curr = n_t{};
f_t PrevFn = f_t{};
f_t CurrFn = f_t{};
for (unsigned I = 0; I < Cells.size(); ++I) {
Curr = Cells[I].getRowKey();
CurrFn = ICF->getFunctionOf(Curr);
if (PrevFn != CurrFn) {
PrevFn = CurrFn;
OS << "\n\n============ Results for function '" +
ICF->getFunctionName(CurrFn) + "' ============\n";
}
if (Prev != Curr) {
Prev = Curr;
std::string NString = IDEProblem.NtoString(Curr);
std::string Line(NString.size(), '-');
OS << "\n\nN: " << NString << "\n---" << Line << '\n';
}
OS << "\tD: " << IDEProblem.DtoString(Cells[I].getColumnKey())
<< " | V: " << IDEProblem.LtoString(Cells[I].getValue()) << '\n';
}
}
OS << '\n';
STOP_TIMER("DFA IDE Result Dumping", PAMM_SEVERITY_LEVEL::Full);
getSolverResults().dumpResults(*ICF, IDEProblem, OS);
}

void dumpAllInterPathEdges() {
Expand Down Expand Up @@ -361,9 +282,24 @@ class IDESolver {
}
}

SolverResults<n_t, d_t, l_t> getSolverResults() {
return SolverResults<n_t, d_t, l_t>(this->ValTab,
IDEProblem.getZeroValue());
/// Returns a view into the computed solver-results.
///
/// NOTE: The SolverResults store a reference into this IDESolver, so its
/// lifetime is also bound to the lifetime of this solver. If you want to use
/// the solverResults beyond the lifetime of this solver, use
/// comsumeSolverResults() instead.
[[nodiscard]] SolverResults<n_t, d_t, l_t> getSolverResults() noexcept {
return SolverResults<n_t, d_t, l_t>(this->ValTab, ZeroValue);
}

/// Moves the computed solver-results out of this solver such that the solver
/// can be destroyed without that the analysis results are lost.
/// Do not call any function (including getSolverResults()) on this IDESolver
/// instance after that.
[[nodiscard]] OwningSolverResults<n_t, d_t, l_t>
consumeSolverResults() noexcept(std::is_nothrow_move_constructible_v<d_t>) {
return OwningSolverResults<n_t, d_t, l_t>(std::move(this->ValTab),
std::move(ZeroValue));
}

protected:
Expand Down Expand Up @@ -1818,6 +1754,17 @@ template <typename Problem>
using IDESolver_P = IDESolver<typename Problem::ProblemAnalysisDomain,
typename Problem::container_type>;

template <typename AnalysisDomainTy, typename Container>
OwningSolverResults<typename AnalysisDomainTy::n_t,
typename AnalysisDomainTy::d_t,
typename AnalysisDomainTy::l_t>
solveIDEProblem(IDETabulationProblem<AnalysisDomainTy, Container> &Problem,
const typename AnalysisDomainTy::i_t &ICF) {
IDESolver<AnalysisDomainTy, Container> Solver(Problem, &ICF);
Solver.solve();
return Solver.consumeSolverResults();
}

} // namespace psr

#endif
26 changes: 21 additions & 5 deletions include/phasar/DataFlow/IfdsIde/Solver/IFDSSolver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,10 @@

namespace psr {

template <typename AnalysisDomainTy>
class IFDSSolver : public IDESolver<WithBinaryValueDomain<AnalysisDomainTy>> {
template <typename AnalysisDomainTy,
typename Container = std::set<typename AnalysisDomainTy::d_t>>
class IFDSSolver
: public IDESolver<WithBinaryValueDomain<AnalysisDomainTy>, Container> {
public:
using ProblemTy = IFDSTabulationProblem<AnalysisDomainTy>;
using d_t = typename AnalysisDomainTy::d_t;
Expand All @@ -39,7 +41,8 @@ class IFDSSolver : public IDESolver<WithBinaryValueDomain<AnalysisDomainTy>> {
template <typename IfdsDomainTy,
typename = std::enable_if_t<
std::is_base_of_v<IfdsDomainTy, AnalysisDomainTy>>>
IFDSSolver(IFDSTabulationProblem<IfdsDomainTy> &IFDSProblem, const i_t *ICF)
IFDSSolver(IFDSTabulationProblem<IfdsDomainTy, Container> &IFDSProblem,
const i_t *ICF)
: IDESolver<WithBinaryValueDomain<AnalysisDomainTy>>(IFDSProblem, ICF) {}

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

template <typename Problem, typename ICF>
IFDSSolver(Problem &, ICF *)
-> IFDSSolver<typename Problem::ProblemAnalysisDomain>;
-> IFDSSolver<typename Problem::ProblemAnalysisDomain,
typename Problem::container_type>;

template <typename Problem>
using IFDSSolver_P = IFDSSolver<typename Problem::ProblemAnalysisDomain>;
using IFDSSolver_P = IFDSSolver<typename Problem::ProblemAnalysisDomain,
typename Problem::container_type>;

template <typename AnalysisDomainTy, typename Container>
OwningSolverResults<typename AnalysisDomainTy::n_t,
typename AnalysisDomainTy::d_t,
typename AnalysisDomainTy::l_t>
solveIFDSProblem(IFDSTabulationProblem<AnalysisDomainTy, Container> &Problem,
const typename AnalysisDomainTy::i_t &ICF) {
IFDSSolver<AnalysisDomainTy, Container> Solver(Problem, &ICF);
Solver.solve();
return Solver.consumeSolverResults();
}

} // namespace psr

Expand Down
Loading