Skip to content
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

[P4Testgen] Remove complete from the model, make it part of the evaluation step instead. #4015

Merged
merged 3 commits into from
Jun 9, 2023
Merged

[P4Testgen] Remove complete from the model, make it part of the evaluation step instead. #4015

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
a9b29d0
Remove complete from the model.
fruffy-bfn May 25, 2023
647473e
Execution state refactoring.
fruffy Jun 2, 2023
c7b4538
Remove createSymbolicVariable entirely and replace it with the static…
fruffy-bfn Jun 2, 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
65 changes: 21 additions & 44 deletions backends/p4tools/common/lib/model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,65 +16,40 @@

namespace P4Tools {

Model::SubstVisitor::SubstVisitor(const Model &model) : self(model) {}
Model::SubstVisitor::SubstVisitor(const Model &model, bool doComplete)
: self(model), doComplete(doComplete) {}

const IR::Literal *Model::SubstVisitor::preorder(IR::StateVariable *var) {
BUG("At this point all state variables should have been resolved. Encountered %1%.", var);
}

const IR::Literal *Model::SubstVisitor::preorder(IR::SymbolicVariable *var) {
BUG_CHECK(self.symbolicMap.find(var) != self.symbolicMap.end(),
"Variable not bound in model: %1%", var);
auto varIt = self.symbolicMap.find(var);
if (varIt == self.symbolicMap.end()) {
if (doComplete) {
return IR::getDefaultValue(var->type, var->srcInfo, true)->checkedTo<IR::Literal>();
}
BUG("Variable not bound in model: %1%", var);
}
prune();
return self.symbolicMap.at(var)->checkedTo<IR::Literal>();
return varIt->second->checkedTo<IR::Literal>();
}

const IR::Literal *Model::SubstVisitor::preorder(IR::TaintExpression *var) {
return IR::getDefaultValue(var->type, var->getSourceInfo())->checkedTo<IR::Literal>();
}

Model::CompleteVisitor::CompleteVisitor(Model &model) : self(model) {}

bool Model::CompleteVisitor::preorder(const IR::SymbolicVariable *var) {
if (self.symbolicMap.find(var) == self.symbolicMap.end()) {
LOG_FEATURE("common", 5,
"***** Did not find a binding for " << var << ". Autocompleting." << std::endl);
const auto *type = var->type;
self.symbolicMap.emplace(var, IR::getDefaultValue(type, var->getSourceInfo()));
}
return false;
}

bool Model::CompleteVisitor::preorder(const IR::StateVariable *var) {
BUG("At this point all state variables should have been resolved. Encountered %1%.", var);
}

void Model::complete(const IR::Expression *expr) { expr->apply(CompleteVisitor(*this)); }

void Model::complete(const SymbolicSet &inputSet) {
auto completionVisitor = CompleteVisitor(*this);
for (const auto &var : inputSet) {
var->apply(completionVisitor);
}
}

void Model::complete(const SymbolicMapType &inputMap) {
for (const auto &inputTuple : inputMap) {
const auto *expr = inputTuple.second;
expr->apply(CompleteVisitor(*this));
}
}

const IR::StructExpression *Model::evaluateStructExpr(const IR::StructExpression *structExpr,
bool doComplete,
ExpressionMap *resolvedExpressions) const {
auto *resolvedStructExpr =
new IR::StructExpression(structExpr->srcInfo, structExpr->type, structExpr->structType, {});
for (const auto *namedExpr : structExpr->components) {
const IR::Expression *resolvedExpr = nullptr;
if (const auto *subStructExpr = namedExpr->expression->to<IR::StructExpression>()) {
resolvedExpr = evaluateStructExpr(subStructExpr, resolvedExpressions);
resolvedExpr = evaluateStructExpr(subStructExpr, doComplete, resolvedExpressions);
} else {
resolvedExpr = evaluate(namedExpr->expression, resolvedExpressions);
resolvedExpr = evaluate(namedExpr->expression, doComplete, resolvedExpressions);
}
resolvedStructExpr->components.push_back(
new IR::NamedExpression(namedExpr->srcInfo, namedExpr->name, resolvedExpr));
Expand All @@ -83,23 +58,24 @@ const IR::StructExpression *Model::evaluateStructExpr(const IR::StructExpression
}

const IR::ListExpression *Model::evaluateListExpr(const IR::ListExpression *listExpr,
bool doComplete,
ExpressionMap *resolvedExpressions) const {
auto *resolvedListExpr = new IR::ListExpression(listExpr->srcInfo, listExpr->type, {});
for (const auto *expr : listExpr->components) {
const IR::Expression *resolvedExpr = nullptr;
if (const auto *subStructExpr = expr->to<IR::ListExpression>()) {
resolvedExpr = evaluateListExpr(subStructExpr, resolvedExpressions);
resolvedExpr = evaluateListExpr(subStructExpr, doComplete, resolvedExpressions);
} else {
resolvedExpr = evaluate(expr, resolvedExpressions);
resolvedExpr = evaluate(expr, doComplete, resolvedExpressions);
}
resolvedListExpr->components.push_back(resolvedExpr);
}
return resolvedListExpr;
}

const IR::Literal *Model::evaluate(const IR::Expression *expr,
const IR::Literal *Model::evaluate(const IR::Expression *expr, bool doComplete,
ExpressionMap *resolvedExpressions) const {
const auto *substituted = expr->apply(SubstVisitor(*this));
const auto *substituted = expr->apply(SubstVisitor(*this, doComplete));
const auto *evaluated = P4::optimizeExpression(substituted);
const auto *literal = evaluated->checkedTo<IR::Literal>();
// Add the variable to the resolvedExpressions list, if the list is not null.
Expand All @@ -109,12 +85,13 @@ const IR::Literal *Model::evaluate(const IR::Expression *expr,
return literal;
}

Model *Model::evaluate(const SymbolicMapType &inputMap, ExpressionMap *resolvedExpressions) const {
Model *Model::evaluate(const SymbolicMapType &inputMap, bool doComplete,
ExpressionMap *resolvedExpressions) const {
auto *result = new Model(*this);
for (const auto &inputTuple : inputMap) {
const auto &name = inputTuple.first;
const auto *expr = inputTuple.second;
(*result)[name] = evaluate(expr, resolvedExpressions);
(*result)[name] = evaluate(expr, doComplete, resolvedExpressions);
}
return result;
}
Expand Down
45 changes: 12 additions & 33 deletions backends/p4tools/common/lib/model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,24 +31,17 @@ class Model : public SymbolicMapType {
class SubstVisitor : public Transform {
const Model &self;

/// If doComplete is true, the visitor will not throw an error if a variable does not have a
/// substitution and instead assign a random or zero value (depending on whether there is a
/// seed) to the variable..
bool doComplete;

public:
const IR::Literal *preorder(IR::StateVariable *var) override;
const IR::Literal *preorder(IR::SymbolicVariable *var) override;
const IR::Literal *preorder(IR::TaintExpression *var) override;

explicit SubstVisitor(const Model &model);
};

// @see SubstVisitor. Does not fail if a variable is not part of the model.
/// Instead, it completes the variable and adds it to the symbolic map.
class CompleteVisitor : public Inspector {
Model &self;

public:
bool preorder(const IR::SymbolicVariable *var) override;
bool preorder(const IR::StateVariable *var) override;

explicit CompleteVisitor(Model &model);
explicit SubstVisitor(const Model &model, bool doComplete);
};

public:
Expand All @@ -64,37 +57,23 @@ class Model : public SymbolicMapType {
Model &operator=(Model &&) = default;
~Model() = default;

/// Completes the model with the variables in the given expression. A variable needs to be
/// completed if it is not present in the model computed by the solver that produced the
/// model. This typically happens when a variable is not needed to solve a set of
/// constraints.
void complete(const IR::Expression *expr);

/// Completes the model with the variables in the given list of expressions. A variable needs to
/// be completed if it is not present in the model computed by the solver that produced the
/// model. This typically happens when a variable is not needed to solve a set of constraints.
void complete(const SymbolicMapType &inputMap);

/// Adds the given set of variables to the model (if they do not exist already).
/// If the variable does not exist, it is initialized to a default value.
void complete(const SymbolicSet &inputSet);

/// Evaluates a P4 expression in the context of this model.
///
/// A BUG occurs if the given expression refers to a variable that is not bound by this model.
/// If the input list @param resolvedExpressions is not null, we also collect the resolved value
/// of this expression.
const IR::Literal *evaluate(const IR::Expression *expr,
const IR::Literal *evaluate(const IR::Expression *expr, bool doComplete,
ExpressionMap *resolvedExpressions = nullptr) const;

// Evaluates a P4 StructExpression in the context of this model. Recursively calls into
// @evaluate and substitutes all members of this list with a Value type.
const IR::StructExpression *evaluateStructExpr(const IR::StructExpression *structExpr,
bool doComplete,
ExpressionMap *resolvedExpressions) const;

// Evaluates a P4 ListExpression in the context of this model. Recursively calls into @evaluate
// and substitutes all members of this list with a Value type.
const IR::ListExpression *evaluateListExpr(const IR::ListExpression *listExpr,
const IR::ListExpression *evaluateListExpr(const IR::ListExpression *listExpr, bool doComplete,
ExpressionMap *resolvedExpressions) const;

/// Evaluates a collection of P4 expressions in the context of this model by calling @evaluate
Expand All @@ -106,11 +85,11 @@ class Model : public SymbolicMapType {
/// of all the variables we have resolved within this expression.
template <template <class...> class Collection>
std::vector<const IR::Literal *> evaluateAll(
const Collection<const IR::Expression *> *exprs,
const Collection<const IR::Expression *> *exprs, bool doComplete,
ExpressionMap *resolvedExpressions = nullptr) const {
std::vector<const IR::Literal *> result(exprs->size());
for (const auto *expr : *exprs) {
result.push_back(evaluate(expr, resolvedExpressions));
result.push_back(evaluate(expr, doComplete, resolvedExpressions));
}
return result;
}
Expand All @@ -121,7 +100,7 @@ class Model : public SymbolicMapType {
/// variable that is not bound by this model. If the input list @param resolvedExpressions is
/// not null, we also collect the bound values of all the variables we have resolved within this
/// expression.
Model *evaluate(const SymbolicMapType &inputMap,
Model *evaluate(const SymbolicMapType &inputMap, bool doComplete,
ExpressionMap *resolvedExpressions = nullptr) const;

/// Tries to retrieve @param var from the model.
Expand Down
10 changes: 1 addition & 9 deletions backends/p4tools/common/lib/symbolic_env.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,17 +31,9 @@ void SymbolicEnv::set(const IR::StateVariable &var, const IR::Expression *value)
map[var] = P4::optimizeExpression(value);
}

Model *SymbolicEnv::complete(const Model &model) const {
// Produce a new model based on the input model
// Add the variables contained in this environment and try to complete them.
auto *newModel = new Model(model);
newModel->complete(map);
return newModel;
}

Model *SymbolicEnv::evaluate(const Model &model) const {
// Produce a new model based on the input model
return model.evaluate(map);
return model.evaluate(map, true);
}

const IR::Expression *SymbolicEnv::subst(const IR::Expression *expr) const {
Expand Down
3 changes: 0 additions & 3 deletions backends/p4tools/common/lib/symbolic_env.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,6 @@ class SymbolicEnv {
/// done on the given value before updating the symbolic state.
void set(const IR::StateVariable &var, const IR::Expression *value);

/// Completes the model with all variables referenced in the symbolic environment.
[[nodiscard]] Model *complete(const Model &model) const;

/// Evaluates this symbolic environment in the context of the given model.
///
/// A BUG occurs if any symbolic value in this environment refers to a variable that is not
Expand Down
4 changes: 2 additions & 2 deletions backends/p4tools/common/lib/taint.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,14 +274,14 @@ class MaskBuilder : public Transform {
MaskBuilder() { visitDagOnce = false; }
};

const IR::Literal *Taint::buildTaintMask(const SymbolicMapType &varMap, const Model *completedModel,
const IR::Literal *Taint::buildTaintMask(const SymbolicMapType &varMap, const Model *evaluatedModel,
const IR::Expression *programPacket) {
// First propagate taint and simplify the packet.
const auto *taintedPacket = programPacket->apply(TaintPropagator(varMap));
// Then create the mask based on the remaining expressions.
const auto *mask = taintedPacket->apply(MaskBuilder());
// Produce the evaluated literal. The hex expression should only have 0 or f.
return completedModel->evaluate(mask);
return evaluatedModel->evaluate(mask, false);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are only few places where this is false, so can't we make it a default argument as true?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have been thinking about this and I would rather make this explicit to force users to think about whether they want to autocomplete values or not.

}

const IR::Expression *Taint::propagateTaint(const SymbolicMapType &varMap,
Expand Down
2 changes: 1 addition & 1 deletion backends/p4tools/common/lib/taint.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ class Taint {
/// @returns the mask for the corresponding program packet, indicating bits of the expression
/// which are not tainted.
static const IR::Literal *buildTaintMask(const SymbolicMapType &varMap,
const Model *completedModel,
const Model *evaluatedModel,
const IR::Expression *programPacket);
};

Expand Down
6 changes: 3 additions & 3 deletions backends/p4tools/common/lib/trace_event.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,10 @@ TraceEvent::TraceEvent() = default;

const TraceEvent *TraceEvent::subst(const SymbolicEnv & /*env*/) const { return this; }

void TraceEvent::complete(Model * /*model*/) const {}

const TraceEvent *TraceEvent::apply(Transform & /*visitor*/) const { return this; }

const TraceEvent *TraceEvent::evaluate(const Model & /*model*/) const { return this; }
const TraceEvent *TraceEvent::evaluate(const Model & /*model*/, bool /*doComplete*/) const {
return this;
}

} // namespace P4Tools
5 changes: 1 addition & 4 deletions backends/p4tools/common/lib/trace_event.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,12 +27,9 @@ class TraceEvent : public ICastable {
/// Applies the given IR transform to the expressions in this trace event.
virtual const TraceEvent *apply(Transform &visitor) const;

/// Completes a model with the variables used in this trace event.
virtual void complete(Model *model) const;

/// Evaluates expressions in the body of this trace event for their concrete value in the given
/// model. A BUG occurs if there are any variables that are unbound by the given model.
[[nodiscard]] virtual const TraceEvent *evaluate(const Model &model) const;
[[nodiscard]] virtual const TraceEvent *evaluate(const Model &model, bool doComplete) const;

protected:
/// Prints this trace event to the given ostream.
Expand Down
39 changes: 11 additions & 28 deletions backends/p4tools/common/lib/trace_event_types.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,13 +38,11 @@ const Expression *Expression::apply(Transform &visitor) const {
return new Expression(value->apply(visitor), label);
}

void Expression::complete(Model *model) const { model->complete(value); }

const Expression *Expression::evaluate(const Model &model) const {
const Expression *Expression::evaluate(const Model &model, bool doComplete) const {
if (Taint::hasTaint(model, value)) {
return new Expression(&Taint::TAINTED_STRING_LITERAL, label);
}
return new Expression(model.evaluate(value), label);
return new Expression(model.evaluate(value, doComplete), label);
}

void Expression::print(std::ostream &os) const {
Expand Down Expand Up @@ -72,14 +70,13 @@ const IfStatementCondition *IfStatementCondition::apply(Transform &visitor) cons
return traceEvent;
}

void IfStatementCondition::complete(Model *model) const { model->complete(postEvalCond); }

const IfStatementCondition *IfStatementCondition::evaluate(const Model &model) const {
const IfStatementCondition *IfStatementCondition::evaluate(const Model &model,
bool doComplete) const {
const IR::Literal *evaluatedPostVal = nullptr;
if (Taint::hasTaint(model, postEvalCond)) {
evaluatedPostVal = &Taint::TAINTED_STRING_LITERAL;
} else {
evaluatedPostVal = model.evaluate(postEvalCond);
evaluatedPostVal = model.evaluate(postEvalCond, doComplete);
}
auto *traceEvent = new IfStatementCondition(evaluatedPostVal);
traceEvent->setPreEvalCond(postEvalCond);
Expand Down Expand Up @@ -133,20 +130,14 @@ const ExtractSuccess *ExtractSuccess::apply(Transform &visitor) const {
return new ExtractSuccess(extractedHeader, offset, condition, applyFields);
}

void ExtractSuccess::complete(Model *model) const {
for (const auto &field : fields) {
model->complete(field.second);
}
}

const ExtractSuccess *ExtractSuccess::evaluate(const Model &model) const {
const ExtractSuccess *ExtractSuccess::evaluate(const Model &model, bool doComplete) const {
std::vector<std::pair<IR::StateVariable, const IR::Expression *>> applyFields;
applyFields.reserve(fields.size());
for (const auto &field : fields) {
if (Taint::hasTaint(model, field.second)) {
applyFields.emplace_back(field.first, &Taint::TAINTED_STRING_LITERAL);
} else {
applyFields.emplace_back(field.first, model.evaluate(field.second));
applyFields.emplace_back(field.first, model.evaluate(field.second, doComplete));
}
}
return new ExtractSuccess(extractedHeader, offset, condition, applyFields);
Expand Down Expand Up @@ -210,20 +201,14 @@ const Emit *Emit::apply(Transform &visitor) const {
return new Emit(emitHeader, applyFields);
}

void Emit::complete(Model *model) const {
for (const auto &field : fields) {
model->complete(field.second);
}
}

const Emit *Emit::evaluate(const Model &model) const {
const Emit *Emit::evaluate(const Model &model, bool doComplete) const {
std::vector<std::pair<IR::StateVariable, const IR::Expression *>> applyFields;
applyFields.reserve(fields.size());
for (const auto &field : fields) {
if (Taint::hasTaint(model, field.second)) {
applyFields.emplace_back(field.first, &Taint::TAINTED_STRING_LITERAL);
} else {
applyFields.emplace_back(field.first, model.evaluate(field.second));
applyFields.emplace_back(field.first, model.evaluate(field.second, doComplete));
}
}
return new Emit(emitHeader, applyFields);
Expand Down Expand Up @@ -254,13 +239,11 @@ const Packet *Packet::apply(Transform &visitor) const {
return new Packet(direction, packetValue->apply(visitor));
}

void Packet::complete(Model *model) const { model->complete(packetValue); }

const Packet *Packet::evaluate(const Model &model) const {
const Packet *Packet::evaluate(const Model &model, bool doComplete) const {
if (Taint::hasTaint(model, packetValue)) {
return new Packet(direction, &Taint::TAINTED_STRING_LITERAL);
}
return new Packet(direction, model.evaluate(packetValue));
return new Packet(direction, model.evaluate(packetValue, doComplete));
}

void Packet::print(std::ostream &os) const {
Expand Down
Loading