Skip to content

Commit 83cf582

Browse files
fruffyfruffy
authored
Implement a common incremental analysis platform with partial evaluation as first use case. (#142)
1 parent 339567c commit 83cf582

25 files changed

+722
-473
lines changed

‎core/interpreter/CMakeLists.txt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,12 @@ set(FLAY_INTERPRETER_SOURCES
55
${CMAKE_CURRENT_SOURCE_DIR}/externs.cpp
66
${CMAKE_CURRENT_SOURCE_DIR}/node_map.cpp
77
${CMAKE_CURRENT_SOURCE_DIR}/parser_stepper.cpp
8+
${CMAKE_CURRENT_SOURCE_DIR}/partial_evaluator.cpp
89
${CMAKE_CURRENT_SOURCE_DIR}/program_info.cpp
910
${CMAKE_CURRENT_SOURCE_DIR}/reachability_expression.cpp
1011
${CMAKE_CURRENT_SOURCE_DIR}/stepper.cpp
1112
${CMAKE_CURRENT_SOURCE_DIR}/substitute_placeholders.cpp
1213
${CMAKE_CURRENT_SOURCE_DIR}/substitution_expression.cpp
13-
${CMAKE_CURRENT_SOURCE_DIR}/symbolic_executor.cpp
1414
${CMAKE_CURRENT_SOURCE_DIR}/table_executor.cpp
1515
${CMAKE_CURRENT_SOURCE_DIR}/target.cpp
1616
)

‎core/interpreter/partial_evaluator.cpp‎

Lines changed: 213 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,213 @@
1+
#include "backends/p4tools/modules/flay/core/interpreter/partial_evaluator.h"
2+
3+
#include <cstdlib>
4+
5+
#include "backends/p4tools/common/lib/logging.h"
6+
#include "backends/p4tools/modules/flay/core/control_plane/bfruntime/protobuf.h"
7+
#include "backends/p4tools/modules/flay/core/control_plane/control_plane_item.h"
8+
#include "backends/p4tools/modules/flay/core/control_plane/p4runtime/protobuf.h"
9+
#include "backends/p4tools/modules/flay/core/interpreter/program_info.h"
10+
#include "backends/p4tools/modules/flay/core/interpreter/target.h"
11+
#include "backends/p4tools/modules/flay/core/lib/incremental_analysis.h"
12+
#include "backends/p4tools/modules/flay/core/lib/return_macros.h"
13+
#include "backends/p4tools/modules/flay/core/specialization/passes/specializer.h"
14+
#include "backends/p4tools/modules/flay/core/specialization/z3/reachability_map.h"
15+
#include "backends/p4tools/modules/flay/core/specialization/z3/substitution_map.h"
16+
#include "backends/p4tools/modules/flay/options.h"
17+
#include "lib/error.h"
18+
#include "lib/timer.h"
19+
20+
namespace P4Tools::Flay {
21+
22+
std::string PartialEvaluationStatistics::toFormattedString() const {
23+
std::stringstream output;
24+
for (const auto &elimRepl : eliminatedNodes) {
25+
auto [node, replaced] = elimRepl;
26+
if (node->getSourceInfo().isValid()) {
27+
auto sourceFragment = node->getSourceInfo().toSourceFragment(false).trim();
28+
if (replaced == nullptr) {
29+
output << "Eliminated node at line "
30+
<< node->getSourceInfo().toPosition().sourceLine << ": " << sourceFragment;
31+
} else {
32+
output << "Replaced node at line " << node->getSourceInfo().toPosition().sourceLine
33+
<< ": " << sourceFragment << " with ";
34+
replaced->dbprint(output);
35+
}
36+
} else {
37+
::warning("Invalid source information for node %1%. This should be fixed", node);
38+
output << "Eliminated node at line (unknown): " << node;
39+
}
40+
if (elimRepl != eliminatedNodes.back()) {
41+
output << "\n";
42+
}
43+
}
44+
return output.str();
45+
}
46+
47+
namespace {
48+
49+
AbstractReachabilityMap *initializeReachabilityMap(ReachabilityMapType mapType,
50+
const NodeAnnotationMap &nodeAnnotationMap) {
51+
printInfo("Creating the reachability map...");
52+
AbstractReachabilityMap *initializedReachabilityMap = nullptr;
53+
if (mapType == ReachabilityMapType::kZ3Precomputed) {
54+
initializedReachabilityMap = new Z3SolverReachabilityMap(nodeAnnotationMap);
55+
} else {
56+
initializedReachabilityMap = new IRReachabilityMap(nodeAnnotationMap);
57+
}
58+
return initializedReachabilityMap;
59+
}
60+
61+
AbstractSubstitutionMap *initializeSubstitutionMap(ReachabilityMapType mapType,
62+
const NodeAnnotationMap &nodeAnnotationMap) {
63+
printInfo("Creating the substitution map...");
64+
AbstractSubstitutionMap *initializedSubstitutionMap = nullptr;
65+
if (mapType == ReachabilityMapType::kZ3Precomputed) {
66+
initializedSubstitutionMap = new Z3SolverSubstitutionMap(nodeAnnotationMap);
67+
} else {
68+
initializedSubstitutionMap = new IrSubstitutionMap(nodeAnnotationMap);
69+
}
70+
return initializedSubstitutionMap;
71+
}
72+
73+
} // namespace
74+
75+
AbstractReachabilityMap *PartialEvaluation::mutableReachabilityMap() { return _reachabilityMap; }
76+
77+
AbstractSubstitutionMap *PartialEvaluation::mutableSubstitutionMap() { return _substitutionMap; }
78+
79+
const ControlPlaneConstraints &PartialEvaluation::controlPlaneConstraints() const {
80+
return _controlPlaneConstraints;
81+
}
82+
83+
ControlPlaneConstraints &PartialEvaluation::mutableControlPlaneConstraints() {
84+
return _controlPlaneConstraints;
85+
}
86+
87+
std::optional<bool> PartialEvaluation::checkForSemanticsChange() {
88+
printInfo("Checking for change in program semantics...");
89+
Util::ScopedTimer timer("Check for semantics change");
90+
91+
auto reachabilityResult =
92+
mutableReachabilityMap()->recomputeReachability(controlPlaneConstraints());
93+
if (!reachabilityResult.has_value()) {
94+
return std::nullopt;
95+
}
96+
auto substitutionResult =
97+
mutableSubstitutionMap()->recomputeSubstitution(controlPlaneConstraints());
98+
if (!substitutionResult.has_value()) {
99+
return std::nullopt;
100+
}
101+
return reachabilityResult.value() || substitutionResult.value();
102+
}
103+
104+
std::optional<bool> PartialEvaluation::checkForSemanticsChange(const SymbolSet &symbolSet) {
105+
printInfo("Checking for change in program semantics with symbol set...");
106+
Util::ScopedTimer timer("Check for semantics change with symbol set");
107+
108+
auto reachabilityResult =
109+
mutableReachabilityMap()->recomputeReachability(symbolSet, controlPlaneConstraints());
110+
if (!reachabilityResult.has_value()) {
111+
return std::nullopt;
112+
}
113+
auto substitutionResult =
114+
mutableSubstitutionMap()->recomputeSubstitution(symbolSet, controlPlaneConstraints());
115+
if (!substitutionResult.has_value()) {
116+
return std::nullopt;
117+
}
118+
return reachabilityResult.value() || substitutionResult.value();
119+
}
120+
121+
std::optional<const IR::P4Program *> PartialEvaluation::specializeProgram(
122+
const IR::P4Program &program) {
123+
auto flaySpecializer = FlaySpecializer(_refMap, *_reachabilityMap, *_substitutionMap);
124+
const auto *optimizedProgram = program.apply(flaySpecializer);
125+
if (::errorCount() > 0) {
126+
return std::nullopt;
127+
}
128+
// Update the list of eliminated nodes.
129+
_eliminatedNodes = flaySpecializer.eliminatedNodes();
130+
return optimizedProgram;
131+
}
132+
133+
std::optional<SymbolSet> PartialEvaluation::convertControlPlaneUpdate(
134+
const ControlPlaneUpdate &controlPlaneUpdate) {
135+
SymbolSet symbolSet;
136+
if (const auto *p4RuntimeUpdate = controlPlaneUpdate.to<P4RuntimeControlPlaneUpdate>()) {
137+
auto result = P4Runtime::updateControlPlaneConstraintsWithEntityMessage(
138+
p4RuntimeUpdate->update.entity(), *flayCompilerResult().getP4RuntimeApi().p4Info,
139+
_controlPlaneConstraints, p4RuntimeUpdate->update.type(), symbolSet);
140+
if (result != EXIT_SUCCESS) {
141+
return std::nullopt;
142+
}
143+
} else if (const auto *bfRuntimeUpdate = controlPlaneUpdate.to<BfRuntimeControlPlaneUpdate>()) {
144+
auto result = BfRuntime::updateControlPlaneConstraintsWithEntityMessage(
145+
bfRuntimeUpdate->update.entity(), *flayCompilerResult().getP4RuntimeApi().p4Info,
146+
_controlPlaneConstraints, bfRuntimeUpdate->update.type(), symbolSet);
147+
if (result != EXIT_SUCCESS) {
148+
return std::nullopt;
149+
}
150+
} else {
151+
::error("Unknown control plane update type: %1%", typeid(controlPlaneUpdate).name());
152+
return std::nullopt;
153+
}
154+
return symbolSet;
155+
}
156+
157+
PartialEvaluation::PartialEvaluation(const FlayOptions &flayOptions,
158+
const FlayCompilerResult &flayCompilerResult,
159+
const ProgramInfo &programInfo,
160+
const PartialEvaluationOptions &partialEvaluationOptions)
161+
: IncrementalAnalysis(flayOptions, flayCompilerResult, programInfo),
162+
_partialEvaluationOptions(partialEvaluationOptions) {
163+
flayCompilerResult.getProgram().apply(P4::ResolveReferences(&_refMap));
164+
}
165+
166+
int PartialEvaluation::initialize() {
167+
printInfo("Computing initial control plane constraints...");
168+
// Gather the initial control-plane configuration. Also from a file input,
169+
// if present.
170+
ASSIGN_OR_RETURN(
171+
_controlPlaneConstraints,
172+
FlayTarget::computeControlPlaneConstraints(flayCompilerResult(), flayOptions()),
173+
EXIT_FAILURE);
174+
175+
ExecutionState executionState(&programInfo().getP4Program());
176+
177+
printInfo("Starting data plane analysis...");
178+
Util::ScopedTimer timer("Data plane analysis");
179+
const auto *pipelineSequence = programInfo().getPipelineSequence();
180+
auto &stepper =
181+
FlayTarget::getStepper(programInfo(), mutableControlPlaneConstraints(), executionState);
182+
stepper.initializeState();
183+
for (const auto *node : *pipelineSequence) {
184+
node->apply(stepper);
185+
}
186+
/// Substitute any placeholder variables encountered in the execution state.
187+
printInfo("Substituting placeholder variables...");
188+
executionState.substitutePlaceholders();
189+
190+
printInfo("Setting up analysis maps...");
191+
_reachabilityMap = initializeReachabilityMap(_partialEvaluationOptions.get().mapType,
192+
executionState.nodeAnnotationMap());
193+
_substitutionMap = initializeSubstitutionMap(_partialEvaluationOptions.get().mapType,
194+
executionState.nodeAnnotationMap());
195+
196+
printInfo("Precomputing reachability and substitution maps with initial constraints...");
197+
auto reachabilityResult = _reachabilityMap->recomputeReachability(controlPlaneConstraints());
198+
if (!reachabilityResult.has_value()) {
199+
return EXIT_FAILURE;
200+
}
201+
auto substitutionResult =
202+
mutableSubstitutionMap()->recomputeSubstitution(controlPlaneConstraints());
203+
if (!substitutionResult.has_value()) {
204+
return EXIT_FAILURE;
205+
}
206+
return EXIT_SUCCESS;
207+
}
208+
209+
[[nodiscard]] PartialEvaluationStatistics *PartialEvaluation::computeAnalysisStatistics() const {
210+
return new PartialEvaluationStatistics{_eliminatedNodes};
211+
}
212+
213+
} // namespace P4Tools::Flay

‎core/interpreter/partial_evaluator.h‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
#ifndef BACKENDS_P4TOOLS_MODULES_FLAY_CORE_INTERPRETER_PARTIAL_EVALUATOR_H_
2+
#define BACKENDS_P4TOOLS_MODULES_FLAY_CORE_INTERPRETER_PARTIAL_EVALUATOR_H_
3+
4+
#include <cstdlib>
5+
#include <functional>
6+
#include <optional>
7+
8+
#include "backends/p4tools/modules/flay/core/control_plane/control_plane_item.h"
9+
#include "backends/p4tools/modules/flay/core/interpreter/compiler_result.h"
10+
#include "backends/p4tools/modules/flay/core/interpreter/program_info.h"
11+
#include "backends/p4tools/modules/flay/core/lib/incremental_analysis.h"
12+
#include "backends/p4tools/modules/flay/core/specialization/passes/specialization_statistics.h"
13+
#include "backends/p4tools/modules/flay/core/specialization/reachability_map.h"
14+
#include "backends/p4tools/modules/flay/core/specialization/substitution_map.h"
15+
#include "backends/p4tools/modules/flay/options.h"
16+
#include "frontends/common/resolveReferences/referenceMap.h"
17+
18+
namespace P4Tools::Flay {
19+
20+
enum ReachabilityMapType { kZ3Precomputed, kDefault };
21+
22+
struct PartialEvaluationOptions {
23+
/// The type of map to initialize.
24+
ReachabilityMapType mapType = ReachabilityMapType::kZ3Precomputed;
25+
};
26+
27+
struct PartialEvaluationStatistics : public AnalysisStatistics {
28+
explicit PartialEvaluationStatistics(std::vector<EliminatedReplacedPair> eliminatedNodes)
29+
: eliminatedNodes(std::move(eliminatedNodes)) {}
30+
31+
// The nodes eliminated in the program.
32+
std::vector<EliminatedReplacedPair> eliminatedNodes;
33+
34+
[[nodiscard]] std::string toFormattedString() const override;
35+
DECLARE_TYPEINFO(PartialEvaluationStatistics);
36+
};
37+
38+
class PartialEvaluation : public IncrementalAnalysis {
39+
private:
40+
/// The set of active control plane constraints. These constraints are added
41+
/// to every solver check to compute feasibility of a program node.
42+
ControlPlaneConstraints _controlPlaneConstraints;
43+
44+
/// The reachability map used by the server. Derived from the input argument.
45+
AbstractReachabilityMap *_reachabilityMap = nullptr;
46+
47+
/// The expression map used by the server.
48+
AbstractSubstitutionMap *_substitutionMap = nullptr;
49+
50+
/// A map to look up declaration references.
51+
P4::ReferenceMap _refMap;
52+
53+
/// Options for partial evaluation.
54+
std::reference_wrapper<const PartialEvaluationOptions> _partialEvaluationOptions;
55+
56+
/// The list of eliminated and optionally replaced nodes. Used for bookkeeping.
57+
std::vector<EliminatedReplacedPair> _eliminatedNodes;
58+
59+
/// @returns a mutable reference reachability map.
60+
AbstractReachabilityMap *mutableReachabilityMap();
61+
62+
/// @returns a mutable reference to the substitution map that this program
63+
/// info object was initialized with.
64+
AbstractSubstitutionMap *mutableSubstitutionMap();
65+
66+
/// @returns the control plane constraints that this program info object
67+
/// was initialized with.
68+
[[nodiscard]] const ControlPlaneConstraints &controlPlaneConstraints() const;
69+
70+
/// @returns a mutable reference to the control plane constraints that this
71+
/// program info object was initialized with.
72+
ControlPlaneConstraints &mutableControlPlaneConstraints();
73+
74+
protected:
75+
std::optional<bool> checkForSemanticsChange() override;
76+
std::optional<bool> checkForSemanticsChange(const SymbolSet &symbolSet) override;
77+
std::optional<const IR::P4Program *> specializeProgram(const IR::P4Program &program) override;
78+
79+
public:
80+
PartialEvaluation(const FlayOptions &flayOptions, const FlayCompilerResult &flayCompilerResult,
81+
const ProgramInfo &programInfo,
82+
const PartialEvaluationOptions &partialEvaluationOptions);
83+
84+
std::optional<SymbolSet> convertControlPlaneUpdate(
85+
const ControlPlaneUpdate &controlPlaneUpdate) override;
86+
87+
int initialize() override;
88+
89+
[[nodiscard]] PartialEvaluationStatistics *computeAnalysisStatistics() const override;
90+
91+
DECLARE_TYPEINFO(PartialEvaluation);
92+
};
93+
94+
} // namespace P4Tools::Flay
95+
96+
#endif /* BACKENDS_P4TOOLS_MODULES_FLAY_CORE_INTERPRETER_PARTIAL_EVALUATOR_H_ */

‎core/interpreter/symbolic_executor.cpp‎

Lines changed: 0 additions & 39 deletions
This file was deleted.

0 commit comments

Comments
 (0)