Skip to content

Commit

Permalink
Fix compilation issues after reachability merge (#3649)
Browse files Browse the repository at this point in the history
  • Loading branch information
@fruffy
fruffy committed Nov 1, 2022
1 parent 67da907 commit 95aa178
Show file tree
Hide file tree
Showing 4 changed files with 41 additions and 37 deletions.
15 changes: 8 additions & 7 deletions backends/p4tools/testgen/core/small_step/small_step.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ SmallStepEvaluator::Result SmallStepEvaluator::step(ExecutionState& state) {
rresult = self.reachabilityEngine->next(state.reachabilityEngineState, node);
if (!rresult.first) {
// Reachability property was failed.
const IR::Expression* cond = IRUtils::getBoolLiteral(false);
const IR::Expression* cond = IR::getBoolLiteral(false);
branches = new std::vector<Branch>({Branch(cond, state, &state)});
}
} else if (const auto* method = node->to<IR::MethodCallStatement>()) {
Expand All @@ -65,7 +65,8 @@ SmallStepEvaluator::Result SmallStepEvaluator::step(ExecutionState& state) {
return std::make_pair(rresult, branches);
}

void renginePostporcessing(ReachabilityResult& result, std::vector<Branch>* branches) {
static void renginePostprocessing(ReachabilityResult& result,
std::vector<Branch>* branches) {
// All Reachability engine state for branch should be copied.
if (branches->size() > 1 || result.second != nullptr) {
for (auto& n : *branches) {
Expand All @@ -86,16 +87,16 @@ SmallStepEvaluator::Result SmallStepEvaluator::step(ExecutionState& state) {
// Step on the given node as a command.
BUG_CHECK(node, "Attempted to evaluate null node.");
REngineType r;
if (self.reachabilityEngine) {
if (self.reachabilityEngine != nullptr) {
r = renginePreprocessing(node);
if (r.second != nullptr) {
return r.second;
}
}
auto* stepper = TestgenTarget::getCmdStepper(state, self.solver, self.programInfo);
auto* result = stepper->step(node);
if (self.reachabilityEngine) {
renginePostporcessing(r.first, result);
if (self.reachabilityEngine != nullptr) {
renginePostprocessing(r.first, result);
}
return result;
}
Expand All @@ -122,9 +123,9 @@ SmallStepEvaluator::Result SmallStepEvaluator::step(ExecutionState& state) {
auto* stepper =
TestgenTarget::getExprStepper(state, self.solver, self.programInfo);
auto* result = stepper->step(expr);
if (self.reachabilityEngine) {
if (self.reachabilityEngine != nullptr) {
ReachabilityResult rresult = std::make_pair(true, nullptr);
renginePostporcessing(rresult, result);
renginePostprocessing(rresult, result);
}
return result;
}
Expand Down
9 changes: 6 additions & 3 deletions backends/p4tools/testgen/lib/execution_state.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,9 +51,8 @@ ExecutionState::ExecutionState(const IR::P4Program* program)
setProperty("inUndefinedState", false);
// Drop is initialized to false, too.
setProperty("drop", false);
if (TestgenOptions::get().pattern.empty()) {
reachabilityEngineState = nullptr;
} else {
// If a user-pattern is provided, initialize the reachability engine state.
if (!TestgenOptions::get().pattern.empty()) {
reachabilityEngineState = ReachabilityEngineState::getInitial();
}
}
Expand All @@ -69,6 +68,10 @@ ExecutionState::ExecutionState(Continuation::Body body)
setProperty("inUndefinedState", false);
// Drop is initialized to false, too.
setProperty("drop", false);
// If a user-pattern is provided, initialize the reachability engine state.
if (!TestgenOptions::get().pattern.empty()) {
reachabilityEngineState = ReachabilityEngineState::getInitial();
}
}

/* =============================================================================================
Expand Down
4 changes: 2 additions & 2 deletions backends/p4tools/testgen/lib/execution_state.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -143,8 +143,8 @@ class ExecutionState {
/// List of branch decisions leading into this state.
std::vector<uint64_t> selectedBranches;

/// Reachability engine state.
ReachabilityEngineState* reachabilityEngineState;
/// State that is needed to track reachability of statements given a query.
ReachabilityEngineState* reachabilityEngineState = nullptr;

/* =========================================================================================
* Accessors
Expand Down
50 changes: 25 additions & 25 deletions backends/p4tools/testgen/test/small-step/reachability.cpp
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
#include "backends/p4tools/common/compiler/reachability.h"

#include <stdlib.h>

#include <cstdlib>
#include <filesystem>
#include <fstream>

Expand Down Expand Up @@ -187,10 +186,10 @@ TEST_F(P4CReachability, testTableAndActions) {
ASSERT_TRUE(egress);
const auto* hitTable = getFromHash(hash, "ingress.hit_table");
ASSERT_TRUE(hitTable);
const auto* MyAction3 = getFromHash(hash, "ingress.MyAction3");
ASSERT_TRUE(MyAction3);
const auto* MyAction7 = getFromHash(hash, "ingress.MyAction7");
ASSERT_TRUE(MyAction7);
const auto* myAction3 = getFromHash(hash, "ingress.MyAction3");
ASSERT_TRUE(myAction3);
const auto* myAction7 = getFromHash(hash, "ingress.MyAction7");
ASSERT_TRUE(myAction7);
// egress is reachable from ingress.
ASSERT_TRUE(dcg->isReachable(ingress, egress));
// igress isn't reachable from egress.
Expand All @@ -201,18 +200,18 @@ TEST_F(P4CReachability, testTableAndActions) {
ASSERT_TRUE(!dcg->isReachable(hitTable, ingress));
// egress is reachable from hit_table.
ASSERT_TRUE(dcg->isReachable(hitTable, egress));
// MyAction7 is reachable from hit_table
ASSERT_TRUE(dcg->isReachable(hitTable, MyAction7));
// MyAction3 is reachable from hit_table
ASSERT_TRUE(dcg->isReachable(hitTable, MyAction3));
// MyAction3 is reachable from MyAction7
ASSERT_TRUE(dcg->isReachable(MyAction7, MyAction3));
// MyAction7 isn't reachable from MyAction3
ASSERT_TRUE(!dcg->isReachable(MyAction3, MyAction7));
// egress is reachable from MyAction3
ASSERT_TRUE(dcg->isReachable(MyAction3, egress));
// MyAction7 isn't reachable from egress
ASSERT_TRUE(!dcg->isReachable(egress, MyAction7));
// myAction7 is reachable from hit_table
ASSERT_TRUE(dcg->isReachable(hitTable, myAction7));
// myAction3 is reachable from hit_table
ASSERT_TRUE(dcg->isReachable(hitTable, myAction3));
// myAction3 is reachable from myAction7
ASSERT_TRUE(dcg->isReachable(myAction7, myAction3));
// myAction7 isn't reachable from myAction3
ASSERT_TRUE(!dcg->isReachable(myAction3, myAction7));
// egress is reachable from myAction3
ASSERT_TRUE(dcg->isReachable(myAction3, egress));
// myAction7 isn't reachable from egress
ASSERT_TRUE(!dcg->isReachable(egress, myAction7));
}

TEST_F(P4CReachability, testSwitchStatement) {
Expand Down Expand Up @@ -360,7 +359,8 @@ TEST_F(P4CReachability, testReacabilityEngine) {

void callTestgen(const char* inputFile, const char* behavior, const char* path, int maxTests) {
std::ostringstream mkDir;
std::string prefix = "", fullPath = sourcePath;
std::string prefix;
std::string fullPath = sourcePath;
fullPath += inputFile;
mkDir << "mkdir -p " << buildPath << path << " && rm -f " << buildPath << path << "/*.stf";
if (system(mkDir.str().c_str()) != 0) {
Expand Down Expand Up @@ -390,22 +390,22 @@ bool checkResultingSTF(std::list<std::list<std::string>> identifiersList, std::s
// Each STF file should contain all identifiers from identifiersList.
auto lIds = identifiersList;
std::ifstream ifile(f.path());
while (!ifile.eof() && lIds.size()) {
while (!ifile.eof() && !lIds.empty()) {
std::string line;
std::getline(ifile, line);
for (auto lid = lIds.begin(); lid != lIds.end(); lid++) {
if (lid->size() == 0) {
for (auto& lId : lIds) {
if (lId.empty()) {
continue;
}
if (line.find(*lid->begin()) != std::string::npos) {
lid->pop_front();
if (line.find(*lId.begin()) != std::string::npos) {
lId.pop_front();
}
}
}
ifile.close();
bool hasEmptyList = false;
for (auto& l : lIds) {
if (l.size() == 0) {
if (l.empty()) {
hasEmptyList = true;
break;
}
Expand Down

0 comments on commit 95aa178

Please sign in to comment.