Skip to content

Commit

Permalink
[P4Testgen] Remove complete from the model, make it part of the evalu…
Browse files Browse the repository at this point in the history 
…ation step instead. (#4015)

* Remove complete from the model.

* Execution state refactoring.

* Remove createSymbolicVariable entirely and replace it with the static getSymbolicVariable.

---------

Co-authored-by: fruffy <[email protected]>
  • Loading branch information
@fruffy-bfn @fruffy
fruffy-bfn and fruffy authored Jun 9, 2023
1 parent b80b2cb commit ca2e383
Show file tree
Hide file tree
Showing 48 changed files with 377 additions and 457 deletions.
65 changes: 21 additions & 44 deletions backends/p4tools/common/lib/model.cpp
View file
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
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
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
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
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);
}

const IR::Expression *Taint::propagateTaint(const SymbolicMapType &varMap,
Expand Down
2 changes: 1 addition & 1 deletion backends/p4tools/common/lib/taint.h
View file
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
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
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
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

0 comments on commit ca2e383

Please sign in to comment.