diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index b79a615a..3716a066 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -121,6 +121,106 @@ absl::Status InitializeTableEntries(SolverState &state, return absl::OkStatus(); } +// Adds solver constraint to restrict the statically translated given `value` of +// the given type `type_name` based on the valid values in the given +// `translator`. +void AddConstraintForStaticallyTranslatedValue( + const z3::expr &value, const std::string &type_name, + const values::P4RuntimeTranslator &translator, z3::context &z3_context, + z3::solver &solver) { + auto it = translator.p4runtime_translation_allocators.find(type_name); + if (it == translator.p4runtime_translation_allocators.end() || + it->second.IsDynamicAllocationEnabled()) + return; + + z3::expr constraint = z3_context.bool_val(false); + for (const auto &valid_value : it->second.GetAllocatedIds()) { + constraint = constraint || (value == static_cast(valid_value)); + } + solver.add(constraint); +} + +// Adds solver constraints to restrict the statically translated values (e.g., +// values of the type `port_id_t` in SAI-P4) to only the mapped values in the +// translator. +absl::Status AddConstraintsForStaticallyTranslatedValues(SolverState &state) { + // Restrict the value of all header fields with (purely static, i.e. + // dynamic_translation = false) P4Runtime translated types to what has been + // used in the translator. + for (const auto &[field, type] : + Ordered(state.translator.fields_p4runtime_type)) { + ASSIGN_OR_RETURN(z3::expr value, state.context.ingress_headers.Get(field)); + AddConstraintForStaticallyTranslatedValue(value, type, state.translator, + *state.context.z3_context, + *state.solver); + } + // Restrict the symbolic variable value of all symbolic table entries with + // (purely static) P4Runtime translated types to what has been used in the + // translator. + for (const auto &[table_name, entries_per_table] : + state.context.table_entries) { + ASSIGN_OR_RETURN(const ir::Table *table, + GetIrTable(state.program, table_name)); + for (const TableEntry &entry : entries_per_table) { + if (!entry.IsSymbolic()) continue; + const pdpi::IrTableEntry &sketch = entry.GetPdpiIrTableEntry(); + + // Constrain the symbolic variables for entry matches. + for (const pdpi::IrMatch &symbolic_match : sketch.matches()) { + const std::string &match_name = symbolic_match.name(); + ASSIGN_OR_RETURN(pdpi::IrMatchFieldDefinition match_definition, + util::GetMatchDefinition(match_name, *table)); + std::string type_name = + match_definition.match_field().type_name().name(); + if (type_name.empty()) { + // If the match definition does not specify the type name, use the + // matched header field name to get the type name based on the + // translator mapping. This seems to happen for matches on locally + // defined variables. + ASSIGN_OR_RETURN(std::string field_name, + util::GetFieldNameFromMatch(match_name, *table)); + auto it = state.translator.fields_p4runtime_type.find(field_name); + if (it != state.translator.fields_p4runtime_type.end()) + type_name = it->second; + } + ASSIGN_OR_RETURN(SymbolicMatchVariables match_variables, + entry.GetMatchValues(match_name, *table, state.program, + *state.context.z3_context)); + AddConstraintForStaticallyTranslatedValue( + match_variables.value, type_name, state.translator, + *state.context.z3_context, *state.solver); + } + + // Constrain the symbolic variables for action parameters. + for (const auto &action_ref : table->table_definition().entry_actions()) { + const std::string &action_name = action_ref.action().preamble().name(); + + // Check and get the action in P4-Symbolic IR. + auto it = state.program.actions().find(action_name); + if (it == state.program.actions().end()) { + return gutil::NotFoundErrorBuilder() + << "Action '" << action_name << "' not found."; + } + const ir::Action &action = it->second; + + for (const auto &[param_name, param_definition] : + Ordered(action.action_definition().params_by_name())) { + const std::string &type_name = + param_definition.param().type_name().name(); + ASSIGN_OR_RETURN(z3::expr param, + entry.GetActionParameter(param_name, action, *table, + *state.context.z3_context)); + AddConstraintForStaticallyTranslatedValue( + param, type_name, state.translator, *state.context.z3_context, + *state.solver); + } + } + } + } + + return absl::OkStatus(); +} + } // namespace std::string SolverState::GetSolverSMT() { @@ -165,24 +265,11 @@ absl::StatusOr> EvaluateP4Program( // Evaluate the main program, assuming it conforms to V1 model. RETURN_IF_ERROR(v1model::EvaluateV1model(*state, physical_ports)); - // Restrict the value of all fields with (purely static, i.e. - // dynamic_translation = false) P4RT translated types to what has been used in - // TranslationPerType. This should be done after the symbolic execution since - // P4Symbolic does not initially know which fields have translated types. - for (const auto &[field, type] : - Ordered(state->translator.fields_p4runtime_type)) { - if (auto it = translation_per_type.find(type); - it != translation_per_type.end() && !it->second.dynamic_translation) { - ASSIGN_OR_RETURN(z3::expr field_expr, context.ingress_headers.Get(field)); - z3::expr constraint = context.z3_context->bool_val(false); - for (const auto &[string_value, numeric_value] : - it->second.static_mapping) { - constraint = - constraint || (field_expr == static_cast(numeric_value)); - } - state->solver->add(constraint); - } - } + // Restrict the symbolic variables of statically translated types to only the + // translated values. This should be done after the symbolic execution since + // P4-Symbolic does not initially know which header fields have translated + // types. + RETURN_IF_ERROR(AddConstraintsForStaticallyTranslatedValues(*state)); // Restrict ports to the available physical ports. // TODO: Support generating packet-out packets from the CPU port. diff --git a/p4_symbolic/symbolic/values.cc b/p4_symbolic/symbolic/values.cc index de6c3388..4eb37590 100644 --- a/p4_symbolic/symbolic/values.cc +++ b/p4_symbolic/symbolic/values.cc @@ -25,6 +25,7 @@ #include #include +#include "absl/container/btree_set.h" #include "absl/numeric/bits.h" #include "absl/status/status.h" #include "absl/status/statusor.h" @@ -255,6 +256,18 @@ absl::StatusOr IdAllocator::IdToString(uint64_t value) const { } } +absl::btree_set IdAllocator::GetAllocatedIds() const { + absl::btree_set translated_ids; + for (const auto &[id, string_value] : id_to_string_map_) { + translated_ids.insert(id); + } + return translated_ids; +} + +bool IdAllocator::IsDynamicAllocationEnabled() const { + return translation_data_.dynamic_translation; +} + } // namespace values } // namespace symbolic } // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/values.h b/p4_symbolic/symbolic/values.h index 4e66d04e..6c279796 100644 --- a/p4_symbolic/symbolic/values.h +++ b/p4_symbolic/symbolic/values.h @@ -28,6 +28,7 @@ #include #include +#include "absl/container/btree_set.h" #include "absl/status/statusor.h" #include "p4_pdpi/ir.pb.h" #include "z3++.h" @@ -71,7 +72,13 @@ class IdAllocator { // which it was allocated. absl::StatusOr IdToString(uint64_t value) const; -private: + // Returns the set of translated IDs. + absl::btree_set GetAllocatedIds() const; + + // Returns whether dynamic allocation is enabled. + bool IsDynamicAllocationEnabled() const; + + private: // A mapping from string values to bitvector values. std::unordered_map string_to_id_map_;