Skip to content

Lock-step Solving and Timeout for IDE Solver #638

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 15 commits into from
Jun 29, 2023
Merged

Lock-step Solving and Timeout for IDE Solver #638

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
ab2cc7d
Add worklist for Phase I in IDESolver
fabianbs96 Jun 3, 2023
f8e910f
Add worklist for Phase II in IDESolver
fabianbs96 Jun 3, 2023
2a02370
Merge branch 'development' into f-WorklistForIDESolver
fabianbs96 Jun 11, 2023
49b4b08
Remove out-commented recursive calls in IDESolver
fabianbs96 Jun 11, 2023
2965ef2
Add IDE solving kind that allows interrupting the analysis or injecti…
fabianbs96 Jun 14, 2023
c7fd496
Merge branch 'development' into f-InteractiveIDESolver
fabianbs96 Jun 22, 2023
5cdc608
Comments + some minor refactoring
fabianbs96 Jun 23, 2023
d390eaa
Add unittest
fabianbs96 Jun 23, 2023
0267699
Generalize the IDESolver mixin + more comments
fabianbs96 Jun 23, 2023
28600cc
Add async cancellation
fabianbs96 Jun 24, 2023
9a0050d
Adding continuations
fabianbs96 Jun 26, 2023
4034a68
Make the PAMM tests sleep less
fabianbs96 Jun 26, 2023
f22a944
Add tests for async cancellation and continuing
fabianbs96 Jun 28, 2023
d35330b
Update comments
fabianbs96 Jun 28, 2023
886ffbd
Apply review comments
fabianbs96 Jun 29, 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
139 changes: 81 additions & 58 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 @@ -27,6 +27,7 @@
#include "phasar/DataFlow/IfdsIde/IFDSTabulationProblem.h"
#include "phasar/DataFlow/IfdsIde/InitialSeeds.h"
#include "phasar/DataFlow/IfdsIde/Solver/FlowEdgeFunctionCache.h"
#include "phasar/DataFlow/IfdsIde/Solver/IDESolverAPIMixin.h"
#include "phasar/DataFlow/IfdsIde/Solver/JumpFunctions.h"
#include "phasar/DataFlow/IfdsIde/Solver/PathEdge.h"
#include "phasar/DataFlow/IfdsIde/SolverResults.h"
Expand Down Expand Up @@ -59,7 +60,10 @@ namespace psr {
/// can then be queried by using resultAt() and resultsAt().
template <typename AnalysisDomainTy,
typename Container = std::set<typename AnalysisDomainTy::d_t>>
class IDESolver {
class IDESolver
: public IDESolverAPIMixin<IDESolver<AnalysisDomainTy, Container>> {
friend IDESolverAPIMixin<IDESolver<AnalysisDomainTy, Container>>;

public:
using ProblemTy = IDETabulationProblem<AnalysisDomainTy, Container>;
using container_type = typename ProblemTy::container_type;
Expand Down Expand Up @@ -127,63 +131,6 @@ class IDESolver {
return J;
}

/// \brief Runs the solver on the configured problem. This can take some time.
virtual void solve() {
PAMM_GET_INSTANCE;
REG_COUNTER("Gen facts", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("Kill facts", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("Summary-reuse", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("Intra Path Edges", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("Inter Path Edges", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("FF Queries", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("EF Queries", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Value Propagation", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Value Computation", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("SpecialSummary-FF Application", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("SpecialSummary-EF Queries", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("JumpFn Construction", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Process Call", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Process Normal", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Process Exit", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("[Calls] getAliasSet", 0, PAMM_SEVERITY_LEVEL::Full);
REG_HISTOGRAM("Data-flow facts", PAMM_SEVERITY_LEVEL::Full);
REG_HISTOGRAM("Points-to", PAMM_SEVERITY_LEVEL::Full);

PHASAR_LOG_LEVEL(INFO, "IDE solver is solving the specified problem");
PHASAR_LOG_LEVEL(INFO,
"Submit initial seeds, construct exploded super graph");
// computations starting here
START_TIMER("DFA Phase I", PAMM_SEVERITY_LEVEL::Full);
// We start our analysis and construct exploded supergraph
submitInitialSeeds();

while (!WorkList.empty()) {
auto [Edge, EF] = std::move(WorkList.back());
WorkList.pop_back();

auto [SourceVal, Target, TargetVal] = Edge.consume();
propagate(std::move(SourceVal), std::move(Target), std::move(TargetVal),
std::move(EF));
}

STOP_TIMER("DFA Phase I", PAMM_SEVERITY_LEVEL::Full);
if (SolverConfig.computeValues()) {
START_TIMER("DFA Phase II", PAMM_SEVERITY_LEVEL::Full);
// Computing the final values for the edge functions
PHASAR_LOG_LEVEL(
INFO, "Compute the final values according to the edge functions");
computeValues();
STOP_TIMER("DFA Phase II", PAMM_SEVERITY_LEVEL::Full);
}
PHASAR_LOG_LEVEL(INFO, "Problem solved");
if constexpr (PAMM_CURR_SEV_LEVEL >= PAMM_SEVERITY_LEVEL::Core) {
computeAndPrintStatistics();
}
if (SolverConfig.emitESG()) {
emitESGAsDot();
}
}

/// Returns the L-type result for the given value at the given statement.
[[nodiscard]] l_t resultAt(n_t Stmt, d_t Value) {
return getSolverResults().resultAt(Stmt, Value);
Expand Down Expand Up @@ -1696,6 +1643,7 @@ class IDESolver {
OS << G;
}

private:
/// @brief: Allows less-than comparison based on the statement ID.
struct StmtLess {
const i_t *ICF;
Expand All @@ -1706,6 +1654,81 @@ class IDESolver {
}
};

/// -- InteractiveIDESolverMixin implementation

bool doInitialize() {
PAMM_GET_INSTANCE;
REG_COUNTER("Gen facts", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("Kill facts", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("Summary-reuse", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("Intra Path Edges", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("Inter Path Edges", 0, PAMM_SEVERITY_LEVEL::Core);
REG_COUNTER("FF Queries", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("EF Queries", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Value Propagation", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Value Computation", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("SpecialSummary-FF Application", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("SpecialSummary-EF Queries", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("JumpFn Construction", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Process Call", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Process Normal", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("Process Exit", 0, PAMM_SEVERITY_LEVEL::Full);
REG_COUNTER("[Calls] getAliasSet", 0, PAMM_SEVERITY_LEVEL::Full);
REG_HISTOGRAM("Data-flow facts", PAMM_SEVERITY_LEVEL::Full);
REG_HISTOGRAM("Points-to", PAMM_SEVERITY_LEVEL::Full);

PHASAR_LOG_LEVEL(INFO, "IDE solver is solving the specified problem");
PHASAR_LOG_LEVEL(INFO,
"Submit initial seeds, construct exploded super graph");
// computations starting here
START_TIMER("DFA Phase I", PAMM_SEVERITY_LEVEL::Full);

// We start our analysis and construct exploded supergraph
submitInitialSeeds();
return !WorkList.empty();
}

bool doNext() {
assert(!WorkList.empty());
auto [Edge, EF] = std::move(WorkList.back());
WorkList.pop_back();

auto [SourceVal, Target, TargetVal] = Edge.consume();
propagate(std::move(SourceVal), std::move(Target), std::move(TargetVal),
std::move(EF));

return !WorkList.empty();
}

void finalizeInternal() {
STOP_TIMER("DFA Phase I", PAMM_SEVERITY_LEVEL::Full);
if (SolverConfig.computeValues()) {
START_TIMER("DFA Phase II", PAMM_SEVERITY_LEVEL::Full);
// Computing the final values for the edge functions
PHASAR_LOG_LEVEL(
INFO, "Compute the final values according to the edge functions");
computeValues();
STOP_TIMER("DFA Phase II", PAMM_SEVERITY_LEVEL::Full);
}
PHASAR_LOG_LEVEL(INFO, "Problem solved");
if constexpr (PAMM_CURR_SEV_LEVEL >= PAMM_SEVERITY_LEVEL::Core) {
computeAndPrintStatistics();
}
if (SolverConfig.emitESG()) {
emitESGAsDot();
}
}

SolverResults<n_t, d_t, l_t> doFinalize() & {
finalizeInternal();
return getSolverResults();
}

OwningSolverResults<n_t, d_t, l_t> doFinalize() && {
finalizeInternal();
return consumeSolverResults();
}

/// -- Data members

IDETabulationProblem<AnalysisDomainTy, Container> &IDEProblem;
Expand Down
Loading