[P4 Symbolic] Make certain Z3 APIs more general.

p4_symbolic/packet_synthesizer/util.cc

@@ -185,7 +185,7 @@ absl::StatusOr<z3::expr> IrValueToZ3Bitvector(const pdpi::IrValue& value,
   ASSIGN_OR_RETURN(const std::string bytes,
                    pdpi::IrValueToNormalizedByteString(value, bitwidth));
   const std::string hex_string = pdpi::ByteStringToHexString(bytes);
-  return HexStringToZ3Bitvector(hex_string, bitwidth);
+  return HexStringToZ3Bitvector(Z3Context(), hex_string, bitwidth);
 }
 
 // The following functions return Z3 constraints corresponding to `field`

p4_symbolic/symbolic/action.cc

@@ -168,7 +168,7 @@ absl::StatusOr<z3::expr> EvaluateHexStr(const ir::HexstrValue &hexstr) {
 
   ASSIGN_OR_RETURN(pdpi::IrValue parsed_value,
                    values::ParseIrValue(hexstr.value()));
-  return HexStringToZ3Bitvector(hexstr.value());
+  return HexStringToZ3Bitvector(Z3Context(), hexstr.value());
 }
 
 absl::StatusOr<z3::expr> EvaluateBool(const ir::BoolValue &bool_value) {
@@ -336,10 +336,10 @@ absl::Status EvaluateAction(const ir::Action &action,
     const std::string &parameter_type_name =
         parameter.param().type_name().name();
     const int bitwidth = parameter.param().bitwidth();
-    ASSIGN_OR_RETURN(
-        z3::expr parameter_value,
-        values::FormatP4RTValue(/*field_name=*/"", parameter_type_name,
-                                args.at(i - 1).value(), bitwidth, translator));
+    ASSIGN_OR_RETURN(z3::expr parameter_value,
+                     values::FormatP4RTValue(
+                         Z3Context(), /*field_name=*/"", parameter_type_name,
+                         args.at(i - 1).value(), bitwidth, translator));
     context.scope.insert({parameter_name, parameter_value});
   }
 

p4_symbolic/symbolic/table.cc

@@ -154,81 +154,6 @@ std::vector<std::pair<int, pdpi::IrTableEntry>> SortEntries(
   return sorted_entries;
 }
 
-// Analyze a single match that is part of a table entry.
-// Constructs a symbolic expression that semantically corresponds to this
-// match.
-absl::StatusOr<z3::expr> EvaluateSingleMatch(
-    p4::config::v1::MatchField match_definition, const std::string &field_name,
-    const z3::expr &field_expression, const pdpi::IrMatch &match,
-    values::P4RuntimeTranslator *translator) {
-  if (match_definition.match_case() != p4::config::v1::MatchField::kMatchType) {
-    // Arch-specific match type.
-    return absl::InvalidArgumentError(
-        absl::StrCat("Found match with non-standard type"));
-  }
-
-  absl::Status mismatch =
-      gutil::InvalidArgumentErrorBuilder()
-      << "match on field '" << field_name << "' must be of type "
-      << p4::config::v1::MatchField::MatchType_Name(
-             match_definition.match_type())
-      << " according to the table definition, but got entry with match: "
-      << match_definition.ShortDebugString();
-
-  auto GetZ3Value =
-      [&](const pdpi::IrValue &value) -> absl::StatusOr<z3::expr> {
-    return values::FormatP4RTValue(field_name,
-                                   match_definition.type_name().name(), value,
-                                   match_definition.bitwidth(), translator);
-  };
-
-  switch (match_definition.match_type()) {
-    case p4::config::v1::MatchField::EXACT: {
-      if (match.match_value_case() != pdpi::IrMatch::kExact) return mismatch;
-      ASSIGN_OR_RETURN(z3::expr value_expression, GetZ3Value(match.exact()));
-      return operators::Eq(field_expression, value_expression);
-    }
-
-    case p4::config::v1::MatchField::LPM: {
-      if (match.match_value_case() != pdpi::IrMatch::kLpm) return mismatch;
-
-      ASSIGN_OR_RETURN(z3::expr value_expression,
-                       GetZ3Value(match.lpm().value()));
-      return operators::PrefixEq(
-          field_expression, value_expression,
-          static_cast<unsigned int>(match.lpm().prefix_length()));
-    }
-
-    case p4::config::v1::MatchField::TERNARY: {
-      if (match.match_value_case() != pdpi::IrMatch::kTernary) return mismatch;
-
-      ASSIGN_OR_RETURN(z3::expr mask_expression,
-                       GetZ3Value(match.ternary().mask()));
-      ASSIGN_OR_RETURN(z3::expr value_expression,
-                       GetZ3Value(match.ternary().value()));
-      ASSIGN_OR_RETURN(z3::expr masked_field,
-                       operators::BitAnd(field_expression, mask_expression));
-      return operators::Eq(masked_field, value_expression);
-    }
-
-    case p4::config::v1::MatchField::OPTIONAL: {
-      if (match.match_value_case() != pdpi::IrMatch::kOptional) return mismatch;
-      // According to the P4Runtime spec, "for don't care matches, the P4Runtime
-      // client must omit the field's entire FieldMatch entry when building the
-      // match repeated field of the TableEntry message". Therefore, if the
-      // match value is present for an optional match type, it must be a
-      // concrete value.
-      ASSIGN_OR_RETURN(z3::expr value_expression,
-                       GetZ3Value(match.optional().value()));
-      return operators::Eq(field_expression, value_expression);
-    }
-
-    default:
-      return absl::UnimplementedError(absl::StrCat(
-          "Found unsupported match type ", match_definition.DebugString()));
-  }
-}
-
 // Constructs a symbolic expression that is true if and only if this entry
 // is matched on.
 absl::StatusOr<z3::expr> EvaluateTableEntryCondition(
@@ -279,9 +204,10 @@ absl::StatusOr<z3::expr> EvaluateTableEntryCondition(
     ASSIGN_OR_RETURN(
         z3::expr match_field_expr,
         action::EvaluateFieldValue(match_field, state, fake_context));
-    ASSIGN_OR_RETURN(z3::expr match_expression,
-                     EvaluateSingleMatch(match_definition, field_name,
-                                         match_field_expr, match, translator));
+    ASSIGN_OR_RETURN(
+        z3::expr match_expression,
+        EvaluateSingleMatch(Z3Context(), match_definition, field_name,
+                            match_field_expr, match, translator));
     ASSIGN_OR_RETURN(condition_expression,
                      operators::And(condition_expression, match_expression));
   }
@@ -350,6 +276,78 @@ absl::Status EvaluateTableEntryAction(
 
 }  // namespace
 
+absl::StatusOr<z3::expr> EvaluateSingleMatch(
+    z3::context &context, p4::config::v1::MatchField match_definition,
+    const std::string &field_name, const z3::expr &field_expression,
+    const pdpi::IrMatch &match, values::P4RuntimeTranslator *translator) {
+  if (match_definition.match_case() != p4::config::v1::MatchField::kMatchType) {
+    // Arch-specific match type.
+    return absl::InvalidArgumentError(
+        absl::StrCat("Found match with non-standard type"));
+  }
+
+  absl::Status mismatch =
+      gutil::InvalidArgumentErrorBuilder()
+      << "match on field '" << field_name << "' must be of type "
+      << p4::config::v1::MatchField::MatchType_Name(
+             match_definition.match_type())
+      << " according to the table definition, but got entry with match: "
+      << match_definition.ShortDebugString();
+
+  auto GetZ3Value =
+      [&](const pdpi::IrValue &value) -> absl::StatusOr<z3::expr> {
+    return values::FormatP4RTValue(context, field_name,
+                                   match_definition.type_name().name(), value,
+                                   match_definition.bitwidth(), translator);
+  };
+
+  switch (match_definition.match_type()) {
+    case p4::config::v1::MatchField::EXACT: {
+      if (match.match_value_case() != pdpi::IrMatch::kExact) return mismatch;
+      ASSIGN_OR_RETURN(z3::expr value_expression, GetZ3Value(match.exact()));
+      return operators::Eq(field_expression, value_expression);
+    }
+
+    case p4::config::v1::MatchField::LPM: {
+      if (match.match_value_case() != pdpi::IrMatch::kLpm) return mismatch;
+
+      ASSIGN_OR_RETURN(z3::expr value_expression,
+                       GetZ3Value(match.lpm().value()));
+      return operators::PrefixEq(
+          field_expression, value_expression,
+          static_cast<unsigned int>(match.lpm().prefix_length()));
+    }
+
+    case p4::config::v1::MatchField::TERNARY: {
+      if (match.match_value_case() != pdpi::IrMatch::kTernary) return mismatch;
+
+      ASSIGN_OR_RETURN(z3::expr mask_expression,
+                       GetZ3Value(match.ternary().mask()));
+      ASSIGN_OR_RETURN(z3::expr value_expression,
+                       GetZ3Value(match.ternary().value()));
+      ASSIGN_OR_RETURN(z3::expr masked_field,
+                       operators::BitAnd(field_expression, mask_expression));
+      return operators::Eq(masked_field, value_expression);
+    }
+
+    case p4::config::v1::MatchField::OPTIONAL: {
+      if (match.match_value_case() != pdpi::IrMatch::kOptional) return mismatch;
+      // According to the P4Runtime spec, "for don't care matches, the P4Runtime
+      // client must omit the field's entire FieldMatch entry when building the
+      // match repeated field of the TableEntry message". Therefore, if the
+      // match value is present for an optional match type, it must be a
+      // concrete value.
+      ASSIGN_OR_RETURN(z3::expr value_expression,
+                       GetZ3Value(match.optional().value()));
+      return operators::Eq(field_expression, value_expression);
+    }
+
+    default:
+      return absl::UnimplementedError(absl::StrCat(
+          "Found unsupported match type ", match_definition.DebugString()));
+  }
+}
+
 absl::StatusOr<SymbolicTableMatches> EvaluateTable(
     const Dataplane &data_plane, const ir::Table &table,
     const std::vector<pdpi::IrTableEntry> &entries,

p4_symbolic/symbolic/table.h

@@ -45,6 +45,14 @@ absl::StatusOr<SymbolicTableMatches> EvaluateTable(
     SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator,
     const z3::expr &guard);
 
+// Analyze a single match that is part of a table entry.
+// Constructs a symbolic expression that semantically corresponds to this
+// match.
+absl::StatusOr<z3::expr> EvaluateSingleMatch(
+    z3::context &context, p4::config::v1::MatchField match_definition,
+    const std::string &field_name, const z3::expr &field_expression,
+    const pdpi::IrMatch &match, values::P4RuntimeTranslator *translator);
+
 }  // namespace table
 }  // namespace symbolic
 }  // namespace p4_symbolic

p4_symbolic/symbolic/values.cc

@@ -75,7 +75,8 @@ absl::StatusOr<pdpi::IrValue> ParseIrValue(const std::string &value) {
   }
 }
 
-absl::StatusOr<z3::expr> FormatP4RTValue(const std::string &field_name,
+absl::StatusOr<z3::expr> FormatP4RTValue(z3::context &context,
+                                         const std::string &field_name,
                                          const std::string &type_name,
                                          const pdpi::IrValue &value,
                                          int bitwidth,
@@ -110,7 +111,7 @@ absl::StatusOr<z3::expr> FormatP4RTValue(const std::string &field_name,
             type_name, bitwidth));
       }
 
-      return Z3Context().bv_val(int_value, bitwidth);
+      return context.bv_val(int_value, bitwidth);
     }
     default: {
       if (translator->fields_p4runtime_type.count(field_name)) {
@@ -128,7 +129,8 @@ absl::StatusOr<z3::expr> FormatP4RTValue(const std::string &field_name,
                        pdpi::ArbitraryByteStringToIrValue(
                            pdpi::HEX_STRING, bitwidth, byte_string));
       // Now convert the hex string internally.
-      return HexStringToZ3Bitvector(normalized_value.hex_str(), bitwidth);
+      return HexStringToZ3Bitvector(context, normalized_value.hex_str(),
+                                    bitwidth);
     }
   }
 }

p4_symbolic/symbolic/values.h

@@ -113,7 +113,8 @@ absl::StatusOr<pdpi::IrValue> ParseIrValue(const std::string &value);
 // translated values (i.e. string IrValues) the bitwidth MUST be 0, in which
 // case we use the minimum number of bits to encode the resulting translated
 // value.
-absl::StatusOr<z3::expr> FormatP4RTValue(const std::string &field_name,
+absl::StatusOr<z3::expr> FormatP4RTValue(z3::context &context,
+                                         const std::string &field_name,
                                          const std::string &type_name,
                                          const pdpi::IrValue &value,
                                          int bitwidth,

p4_symbolic/symbolic/values_test.cc

@@ -28,9 +28,10 @@ TEST(TranslateValueToP4RT, ReverseTranslatedValuesAreEqualToTheOriginalOnes) {
     const std::string id = absl::StrCat("id-", i);
     pdpi::IrValue ir_value;
     ir_value.set_str(id);
-    ASSERT_OK_AND_ASSIGN(z3::expr expr,
-                         FormatP4RTValue(kFieldName, kFieldType, ir_value,
-                                         /*bitwidth=*/0, &translator));
+    ASSERT_OK_AND_ASSIGN(
+        z3::expr expr,
+        FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value,
+                        /*bitwidth=*/0, &translator));
     z3_value_to_id[expr.to_string()] = id;
   }
 
@@ -49,47 +50,51 @@ TEST(FormatP4RTValue, WorksFor64BitIPv6) {
   ASSERT_OK_AND_ASSIGN(auto ir_value,
                        gutil::ParseTextProto<pdpi::IrValue>(
                            R"pb(ipv6: "0000:ffff:ffff:ffff::")pb"));
-  ASSERT_OK_AND_ASSIGN(z3::expr z3_expr,
-                       FormatP4RTValue(kFieldName, kFieldType, ir_value,
-                                       /*bitwidth=*/64, &trasnlator));
+  ASSERT_OK_AND_ASSIGN(
+      z3::expr z3_expr,
+      FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value,
+                      /*bitwidth=*/64, &trasnlator));
   ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x0000'ffff'ffff'ffffULL);
 }
 
 TEST(FormatP4RTValue, WorksForIpv4) {
   P4RuntimeTranslator trasnlator;
   ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto<pdpi::IrValue>(
                                           R"pb(ipv4: "127.0.0.1")pb"));
-  ASSERT_OK_AND_ASSIGN(z3::expr z3_expr,
-                       FormatP4RTValue(kFieldName, kFieldType, ir_value,
-                                       /*bitwidth=*/32, &trasnlator));
+  ASSERT_OK_AND_ASSIGN(
+      z3::expr z3_expr,
+      FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value,
+                      /*bitwidth=*/32, &trasnlator));
   ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x7f000001);
 }
 
 TEST(FormatP4RTValue, WorksForMac) {
   P4RuntimeTranslator trasnlator;
   ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto<pdpi::IrValue>(
                                           R"pb(mac: "01:02:03:04:05:06")pb"));
-  ASSERT_OK_AND_ASSIGN(z3::expr z3_expr,
-                       FormatP4RTValue(kFieldName, kFieldType, ir_value,
-                                       /*bitwidth=*/48, &trasnlator));
+  ASSERT_OK_AND_ASSIGN(
+      z3::expr z3_expr,
+      FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value,
+                      /*bitwidth=*/48, &trasnlator));
   ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x01'02'03'04'05'06ULL);
 }
 
 TEST(FormatP4RTValue, WorksForHexString) {
   P4RuntimeTranslator trasnlator;
   ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto<pdpi::IrValue>(
                                           R"pb(hex_str: "0xabcd")pb"));
-  ASSERT_OK_AND_ASSIGN(z3::expr z3_expr,
-                       FormatP4RTValue(kFieldName, kFieldType, ir_value,
-                                       /*bitwidth=*/16, &trasnlator));
+  ASSERT_OK_AND_ASSIGN(
+      z3::expr z3_expr,
+      FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value,
+                      /*bitwidth=*/16, &trasnlator));
   ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0xabcd);
 }
 
 TEST(FormatP4RTValue, FailsForStringWithNonZeroBitwidth) {
   P4RuntimeTranslator trasnlator;
   ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto<pdpi::IrValue>(
                                           R"pb(str: "dummy_value")pb"));
-  ASSERT_THAT(FormatP4RTValue(kFieldName, kFieldType, ir_value,
+  ASSERT_THAT(FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value,
                               /*bitwidth=*/16, &trasnlator),
               StatusIs(absl::StatusCode::kInvalidArgument));
 }

p4_symbolic/z3_util.cc

@@ -55,15 +55,16 @@ absl::StatusOr<int> EvalZ3Int(const z3::expr& int_expr,
   return model.eval(int_expr, true).get_numeral_int();
 }
 
-absl::StatusOr<z3::expr> HexStringToZ3Bitvector(const std::string& hex_string,
+absl::StatusOr<z3::expr> HexStringToZ3Bitvector(z3::context& context,
+                                                const std::string& hex_string,
                                                 absl::optional<int> bitwidth) {
   // TODO: Insert check to ensure this won't throw an exception.
   mpz_class integer = mpz_class(hex_string, /*base=*/0);
   std::string decimal = integer.get_str(/*base=*/10);
   if (!bitwidth.has_value()) {
     bitwidth = integer.get_str(/*base=*/2).size();
   }
-  return Z3Context().bv_val(decimal.c_str(), *bitwidth);
+  return context.bv_val(decimal.c_str(), *bitwidth);
 }
 
 uint64_t Z3ValueStringToInt(const std::string& value) {

p4_symbolic/z3_util.h

@@ -44,9 +44,10 @@ absl::StatusOr<std::bitset<num_bits>> EvalZ3Bitvector(const z3::expr& bv_expr,
 // -- Constructing Z3 expressions ----------------------------------------------
 
 // Returns Z3 bitvector of the given `hex_string` value.
-// If no bitwidth is
+// If no bitwidth is given, the size of the bitvector is derived from
+// `hex_string`.
 absl::StatusOr<z3::expr> HexStringToZ3Bitvector(
-    const std::string& hex_string,
+    z3::context& context, const std::string& hex_string,
     absl::optional<int> bitwidth = absl::nullopt);
 
 // -- Misc. --------------------------------------------------------------------