Skip to content

Commit

Permalink
[P4_Symbolic] Use absl numeric bit_width instead of custom implementa…
Browse files Browse the repository at this point in the history 
…tion.Evaluate symbolic table entries with symbolic headers.
  • Loading branch information
@kishanps @VSuryaprasad-HCL
kishanps authored and VSuryaprasad-HCL committed Jan 20, 2025
1 parent b578509 commit 3be308b
Show file tree
Hide file tree
Showing 16 changed files with 346 additions and 244 deletions.
1 change: 1 addition & 0 deletions p4_symbolic/symbolic/BUILD.bazel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ cc_library(
"@com_google_absl//absl/cleanup",
"@com_google_absl//absl/container:btree",
"@com_google_absl//absl/container:flat_hash_map",
"@com_google_absl//absl/numeric:bits",
"@com_google_absl//absl/status",
"@com_google_absl//absl/status:statusor",
"@com_google_absl//absl/strings",
Expand Down
109 changes: 70 additions & 39 deletions p4_symbolic/symbolic/action.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,13 @@
#include "google/protobuf/repeated_ptr_field.h"
#include "gutil/collections.h"
#include "gutil/status.h"
#include "p4_pdpi/internal/ordered_map.h"
#include "p4_pdpi/ir.pb.h"
#include "p4_symbolic/ir/ir.pb.h"
#include "p4_symbolic/symbolic/context.h"
#include "p4_symbolic/symbolic/operators.h"
#include "p4_symbolic/symbolic/symbolic.h"
#include "p4_symbolic/symbolic/table_entry.h"
#include "p4_symbolic/symbolic/v1model.h"
#include "p4_symbolic/symbolic/values.h"
#include "p4_symbolic/z3_util.h"
Expand All @@ -41,41 +43,41 @@ namespace symbolic {
namespace action {

absl::Status EvaluateStatement(const ir::Statement &statement,
SymbolicPerPacketState *state,
SymbolicPerPacketState &headers,
ActionContext *context, z3::context &z3_context,
const z3::expr &guard) {
switch (statement.statement_case()) {
case ir::Statement::kAssignment: {
return EvaluateAssignmentStatement(statement.assignment(), state, context,
z3_context, guard);
return EvaluateAssignmentStatement(statement.assignment(), headers,
context, z3_context, guard);
}
case ir::Statement::kClone: {
// TODO: Add support for cloning.
return state->Set(std::string(kGotClonedPseudoField),
z3_context.bool_val(true), guard);
return headers.Set(std::string(kGotClonedPseudoField),
z3_context.bool_val(true), guard);
}
case ir::Statement::kDrop: {
// https://github.com/p4lang/p4c/blob/7ee76d16da63883c5092ab0c28321f04c2646759/p4include/v1model.p4#L435
const std::string &header_name = statement.drop().header().header_name();
RETURN_IF_ERROR(state->Set(absl::StrFormat("%s.egress_spec", header_name),
v1model::EgressSpecDroppedValue(z3_context),
guard));
RETURN_IF_ERROR(
headers.Set(absl::StrFormat("%s.egress_spec", header_name),
v1model::EgressSpecDroppedValue(z3_context), guard));
return absl::OkStatus();
}
case ir::Statement::kHash: {
const ir::FieldValue &field = statement.hash().field();
std::string field_name =
absl::StrFormat("%s.%s", field.header_name(), field.field_name());
if (!state->ContainsKey(field_name)) {
if (!headers.ContainsKey(field_name)) {
return absl::NotFoundError(absl::StrCat(
"Action ", context->action_name, " hashes to unknown header field ",
field.DebugString()));
}
ASSIGN_OR_RETURN(z3::expr old_value, state->Get(field_name));
ASSIGN_OR_RETURN(z3::expr old_value, headers.Get(field_name));
ASSIGN_OR_RETURN(
z3::expr free_variable,
operators::FreeVariable(field_name, old_value.get_sort()));
RETURN_IF_ERROR(state->Set(field_name, free_variable, guard));
RETURN_IF_ERROR(headers.Set(field_name, free_variable, guard));
return absl::OkStatus();
}
case ir::Statement::kExit: {
Expand All @@ -95,18 +97,18 @@ absl::Status EvaluateStatement(const ir::Statement &statement,
// constrains it in an enclosing assignment expression, or stores it in
// the action scope.
absl::Status EvaluateAssignmentStatement(
const ir::AssignmentStatement &assignment, SymbolicPerPacketState *state,
const ir::AssignmentStatement &assignment, SymbolicPerPacketState &headers,
ActionContext *context, z3::context &z3_context, const z3::expr &guard) {
// Evaluate RValue recursively, evaluate LValue in this function, then
// assign RValue to the scope at LValue.
ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(assignment.right(), *state,
ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(assignment.right(), headers,
*context, z3_context));

switch (assignment.left().lvalue_case()) {
case ir::LValue::kFieldValue: {
const ir::FieldValue &field_value = assignment.left().field_value();
RETURN_IF_ERROR(state->Set(field_value.header_name(),
field_value.field_name(), right, guard));
RETURN_IF_ERROR(headers.Set(field_value.header_name(),
field_value.field_name(), right, guard));
return absl::OkStatus();
}

Expand All @@ -126,12 +128,12 @@ absl::Status EvaluateAssignmentStatement(
// Constructs a symbolic expression corresponding to this value, according
// to its type.
absl::StatusOr<z3::expr> EvaluateRValue(const ir::RValue &rvalue,
const SymbolicPerPacketState &state,
const SymbolicPerPacketState &headers,
const ActionContext &context,
z3::context &z3_context) {
switch (rvalue.rvalue_case()) {
case ir::RValue::kFieldValue:
return EvaluateFieldValue(rvalue.field_value(), state);
return EvaluateFieldValue(rvalue.field_value(), headers);

case ir::RValue::kHexstrValue:
return EvaluateHexStr(rvalue.hexstr_value(), z3_context);
Expand All @@ -146,7 +148,7 @@ absl::StatusOr<z3::expr> EvaluateRValue(const ir::RValue &rvalue,
return EvaluateVariable(rvalue.variable_value(), context);

case ir::RValue::kExpressionValue:
return EvaluateRExpression(rvalue.expression_value(), state, context,
return EvaluateRExpression(rvalue.expression_value(), headers, context,
z3_context);

default:
Expand All @@ -158,8 +160,8 @@ absl::StatusOr<z3::expr> EvaluateRValue(const ir::RValue &rvalue,

// Extract the field symbolic value from the symbolic state.
absl::StatusOr<z3::expr> EvaluateFieldValue(
const ir::FieldValue &field_value, const SymbolicPerPacketState &state) {
return state.Get(field_value.header_name(), field_value.field_name());
const ir::FieldValue &field_value, const SymbolicPerPacketState &headers) {
return headers.Get(field_value.header_name(), field_value.field_name());
}

// Turns bmv2 values to Symbolic Expressions.
Expand Down Expand Up @@ -200,14 +202,14 @@ absl::StatusOr<z3::expr> EvaluateVariable(const ir::Variable &variable,

// Recursively evaluate expressions.
absl::StatusOr<z3::expr> EvaluateRExpression(
const ir::RExpression &expr, const SymbolicPerPacketState &state,
const ir::RExpression &expr, const SymbolicPerPacketState &headers,
const ActionContext &context, z3::context &z3_context) {
switch (expr.expression_case()) {
case ir::RExpression::kBinaryExpression: {
ir::BinaryExpression bin_expr = expr.binary_expression();
ASSIGN_OR_RETURN(z3::expr left, EvaluateRValue(bin_expr.left(), state,
ASSIGN_OR_RETURN(z3::expr left, EvaluateRValue(bin_expr.left(), headers,
context, z3_context));
ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(bin_expr.right(), state,
ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(bin_expr.right(), headers,
context, z3_context));
switch (bin_expr.operation()) {
case ir::BinaryExpression::PLUS:
Expand Down Expand Up @@ -255,7 +257,7 @@ absl::StatusOr<z3::expr> EvaluateRExpression(
ir::UnaryExpression un_expr = expr.unary_expression();
ASSIGN_OR_RETURN(
z3::expr operand,
EvaluateRValue(un_expr.operand(), state, context, z3_context));
EvaluateRValue(un_expr.operand(), headers, context, z3_context));
switch (un_expr.operation()) {
case ir::UnaryExpression::NOT:
return operators::Not(operand);
Expand All @@ -273,11 +275,12 @@ absl::StatusOr<z3::expr> EvaluateRExpression(
ir::TernaryExpression tern_expr = expr.ternary_expression();
ASSIGN_OR_RETURN(
z3::expr condition,
EvaluateRValue(tern_expr.condition(), state, context, z3_context));
ASSIGN_OR_RETURN(z3::expr left, EvaluateRValue(tern_expr.left(), state,
EvaluateRValue(tern_expr.condition(), headers, context, z3_context));
ASSIGN_OR_RETURN(z3::expr left, EvaluateRValue(tern_expr.left(), headers,
context, z3_context));
ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(tern_expr.right(), state,
context, z3_context));
ASSIGN_OR_RETURN(
z3::expr right,
EvaluateRValue(tern_expr.right(), headers, context, z3_context));
return operators::Ite(condition, left, right);
}

Expand All @@ -286,8 +289,8 @@ absl::StatusOr<z3::expr> EvaluateRExpression(
// Evaluate arguments.
std::vector<z3::expr> args;
for (const auto &arg_value : builtin_expr.arguments()) {
ASSIGN_OR_RETURN(z3::expr arg,
EvaluateRValue(arg_value, state, context, z3_context));
ASSIGN_OR_RETURN(z3::expr arg, EvaluateRValue(arg_value, headers,
context, z3_context));
args.push_back(arg);
}

Expand All @@ -311,15 +314,12 @@ absl::StatusOr<z3::expr> EvaluateRExpression(
}
}

// Symbolically evaluates the given action on the given symbolic parameters.
// This produces a symbolic expression on the symbolic parameters that is
// semantically equivalent to the behavior of the action on its concrete
// parameters.
absl::Status EvaluateAction(const ir::Action &action,
const google::protobuf::RepeatedPtrField<
pdpi::IrActionInvocation::IrActionParam> &args,
SolverState &state, SymbolicPerPacketState *headers,
const z3::expr &guard) {
absl::Status EvaluateConcreteAction(
const ir::Action &action,
const google::protobuf::RepeatedPtrField<
pdpi::IrActionInvocation::IrActionParam> &args,
SolverState &state, SymbolicPerPacketState &headers,
const z3::expr &guard) {
// Construct this action's context.
ActionContext context;
context.action_name = action.action_definition().preamble().name();
Expand Down Expand Up @@ -362,6 +362,37 @@ absl::Status EvaluateAction(const ir::Action &action,
return absl::OkStatus();
}

absl::Status EvaluateSymbolicAction(const ir::Action &action,
const TableEntry &entry, SolverState &state,
SymbolicPerPacketState &headers,
const z3::expr &guard) {
// At this point the table must exists because otherwise an absl error would
// have been returned upon initializing the table entries, so no exception
// will be thrown.
const ir::Table &table = state.program.tables().at(entry.GetTableName());

// Construct the action's context.
ActionContext context;
context.action_name = action.action_definition().preamble().name();

// Add the symbolic action parameters to scope.
for (const auto &[param_name, _] :
Ordered(action.action_definition().params_by_name())) {
ASSIGN_OR_RETURN(z3::expr param_value,
entry.GetActionParameter(param_name, action, table,
*state.context.z3_context));
context.scope.insert({param_name, param_value});
}

// Iterate over the body in order, and evaluate each statement.
for (const auto &statement : action.action_implementation().action_body()) {
RETURN_IF_ERROR(EvaluateStatement(statement, headers, &context,
*state.context.z3_context, guard));
}

return absl::OkStatus();
}

} // namespace action
} // namespace symbolic
} // namespace p4_symbolic
39 changes: 24 additions & 15 deletions p4_symbolic/symbolic/action.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,22 +29,13 @@
#include "p4_symbolic/ir/ir.pb.h"
#include "p4_symbolic/symbolic/context.h"
#include "p4_symbolic/symbolic/symbolic.h"
#include "p4_symbolic/symbolic/table_entry.h"
#include "z3++.h"

namespace p4_symbolic {
namespace symbolic {
namespace action {

// Symbolically evaluates the given action on the given symbolic parameters.
// This produces a symbolic expression on the symbolic parameters that is
// semantically equivalent to the behavior of the action on its concrete
// parameters.
absl::Status EvaluateAction(const ir::Action &action,
const google::protobuf::RepeatedPtrField<
pdpi::IrActionInvocation::IrActionParam> &args,
SolverState &state, SymbolicPerPacketState *headers,
const z3::expr &guard);

// Internal functions used to Evaluate statements and expressions within an
// action body. These are internal functions not used beyond this header and its
// associated source file.
Expand All @@ -58,27 +49,27 @@ struct ActionContext {
// Performs a switch case over support statement types and call the
// appropriate function.
absl::Status EvaluateStatement(const ir::Statement &statement,
SymbolicPerPacketState *state,
SymbolicPerPacketState &headers,
ActionContext *context, z3::context &z3_context,
const z3::expr &guard);

// Constructs a symbolic expression for the assignment value, and either
// constrains it in an enclosing assignment expression, or stores it in
// the action scope.
absl::Status EvaluateAssignmentStatement(
const ir::AssignmentStatement &assignment, SymbolicPerPacketState *state,
const ir::AssignmentStatement &assignment, SymbolicPerPacketState &headers,
ActionContext *context, z3::context &z3_context, const z3::expr &guard);

// Constructs a symbolic expression corresponding to this value, according
// to its type.
absl::StatusOr<z3::expr> EvaluateRValue(const ir::RValue &rvalue,
const SymbolicPerPacketState &state,
const SymbolicPerPacketState &headers,
const ActionContext &context,
z3::context &z3_context);

// Extract the field symbolic value from the symbolic state.
absl::StatusOr<z3::expr> EvaluateFieldValue(
const ir::FieldValue &field_value, const SymbolicPerPacketState &state);
const ir::FieldValue &field_value, const SymbolicPerPacketState &headers);

// Parse and format literal values as symbolic expression.
absl::StatusOr<z3::expr> EvaluateHexStr(const ir::HexstrValue &hexstr,
Expand All @@ -97,9 +88,27 @@ absl::StatusOr<z3::expr> EvaluateVariable(const ir::Variable &variable,
// Evaluate expression by recursively evaluating operands and applying the
// symbolic version of the operator to them.
absl::StatusOr<z3::expr> EvaluateRExpression(
const ir::RExpression &expr, const SymbolicPerPacketState &state,
const ir::RExpression &expr, const SymbolicPerPacketState &headers,
const ActionContext &context, z3::context &z3_context);

// Symbolically evaluates the given `action` based on the given concrete
// parameters in `args`.
// This applies the action with concrete parameters on the symbolic `headers`.
absl::Status EvaluateConcreteAction(
const ir::Action &action,
const google::protobuf::RepeatedPtrField<
pdpi::IrActionInvocation::IrActionParam> &args,
SolverState &state, SymbolicPerPacketState &headers, const z3::expr &guard);

// Symbolically evaluates the given `action` based on the given symbolic
// parameters of the given `entry`.
// This applies the action with symbolic parameters on the symbolic `headers`.
absl::Status EvaluateSymbolicAction(const ir::Action &action,
const TableEntry &entry, SolverState &state,
SymbolicPerPacketState &headers,
const z3::expr &guard);


} // namespace action
} // namespace symbolic
} // namespace p4_symbolic
Expand Down
4 changes: 2 additions & 2 deletions p4_symbolic/symbolic/conditional.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,12 @@ namespace conditional {

absl::StatusOr<SymbolicTableMatches> EvaluateConditional(
const ir::Conditional &conditional, SolverState &state,
SymbolicPerPacketState *headers, const z3::expr &guard) {
SymbolicPerPacketState &headers, const z3::expr &guard) {
// Evaluate the condition.
action::ActionContext fake_context = {conditional.name(), {}};
ASSIGN_OR_RETURN(
z3::expr condition,
action::EvaluateRValue(conditional.condition(), *headers, fake_context,
action::EvaluateRValue(conditional.condition(), headers, fake_context,
*state.context.z3_context));
ASSIGN_OR_RETURN(z3::expr negated_condition, operators::Not(condition));

Expand Down
2 changes: 1 addition & 1 deletion p4_symbolic/symbolic/conditional.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ namespace conditional {

absl::StatusOr<SymbolicTableMatches> EvaluateConditional(
const ir::Conditional &conditional, SolverState &state,
SymbolicPerPacketState *headers, const z3::expr &guard);
SymbolicPerPacketState &headers, const z3::expr &guard);

} // namespace conditional
} // namespace symbolic
Expand Down
4 changes: 2 additions & 2 deletions p4_symbolic/symbolic/control.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ namespace p4_symbolic::symbolic::control {

absl::StatusOr<SymbolicTableMatches> EvaluatePipeline(
const std::string &pipeline_name, SolverState &state,
SymbolicPerPacketState *headers, const z3::expr &guard) {
SymbolicPerPacketState &headers, const z3::expr &guard) {
if (auto it = state.program.pipeline().find(pipeline_name);
it != state.program.pipeline().end()) {
return EvaluateControl(it->second.initial_control(), state, headers, guard);
Expand All @@ -49,7 +49,7 @@ absl::StatusOr<SymbolicTableMatches> EvaluatePipeline(

absl::StatusOr<SymbolicTableMatches> EvaluateControl(
const std::string &control_name, SolverState &state,
SymbolicPerPacketState *headers, const z3::expr &guard) {
SymbolicPerPacketState &headers, const z3::expr &guard) {
// Base case: we got to the end of the evaluation, no more controls!
if (control_name == ir::EndOfPipeline()) return SymbolicTableMatches();

Expand Down
4 changes: 2 additions & 2 deletions p4_symbolic/symbolic/control.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,12 +71,12 @@ namespace control {
// Evaluate the passed pipeline.
absl::StatusOr<SymbolicTableMatches> EvaluatePipeline(
const std::string &pipeline_name, SolverState &state,
SymbolicPerPacketState *headers, const z3::expr &guard);
SymbolicPerPacketState &headers, const z3::expr &guard);

// Evaluate the passed control construct.
absl::StatusOr<SymbolicTableMatches> EvaluateControl(
const std::string &control_name, SolverState &state,
SymbolicPerPacketState *headers, const z3::expr &guard);
SymbolicPerPacketState &headers, const z3::expr &guard);

} // namespace control
} // namespace symbolic
Expand Down
Loading

0 comments on commit 3be308b

Please sign in to comment.