|
| 1 | +/* |
| 2 | + * Copyright 2023 The P4-Constraints Authors |
| 3 | + * |
| 4 | + * Licensed under the Apache License, Version 2.0 (the "License"); |
| 5 | + * you may not use this file except in compliance with the License. |
| 6 | + * You may obtain a copy of the License at |
| 7 | + * |
| 8 | + * http://www.apache.org/licenses/LICENSE-2.0 |
| 9 | + * |
| 10 | + * Unless required by applicable law or agreed to in writing, software |
| 11 | + * distributed under the License is distributed on an "AS IS" BASIS, |
| 12 | + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| 13 | + * See the License for the specific language governing permissions and |
| 14 | + * limitations under the License. |
| 15 | + */ |
| 16 | + |
| 17 | +#include "p4_constraints/backend/symbolic_interpreter.h" |
| 18 | + |
| 19 | +#include <string> |
| 20 | +#include <variant> |
| 21 | + |
| 22 | +#include "absl/status/statusor.h" |
| 23 | +#include "absl/strings/str_cat.h" |
| 24 | +#include "absl/strings/string_view.h" |
| 25 | +#include "gutils/overload.h" |
| 26 | +#include "gutils/source_location.h" |
| 27 | +#include "gutils/status_builder.h" |
| 28 | +#include "gutils/status_macros.h" |
| 29 | +#include "p4_constraints/ast.h" |
| 30 | +#include "p4_constraints/ast.pb.h" |
| 31 | +#include "p4_constraints/backend/constraint_info.h" |
| 32 | +#include "z3++.h" |
| 33 | + |
| 34 | +namespace p4_constraints { |
| 35 | +namespace { |
| 36 | + |
| 37 | +absl::StatusOr<z3::expr> GetFieldAccess(const SymbolicKey& symbolic_key, |
| 38 | + absl::string_view field) { |
| 39 | + return std::visit( |
| 40 | + gutils::Overload{ |
| 41 | + [&](const SymbolicExact& exact) -> absl::StatusOr<z3::expr> { |
| 42 | + if (field == "value") return exact.value; |
| 43 | + return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC) |
| 44 | + << "Exact has no field '" << field << "'"; |
| 45 | + }, |
| 46 | + [&](const SymbolicTernary& ternary) -> absl::StatusOr<z3::expr> { |
| 47 | + if (field == "value") return ternary.value; |
| 48 | + if (field == "mask") return ternary.mask; |
| 49 | + return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC) |
| 50 | + << "Ternary has no field \"" << field << "\""; |
| 51 | + }, |
| 52 | + [&](const SymbolicLpm& lpm) -> absl::StatusOr<z3::expr> { |
| 53 | + if (field == "value") return lpm.value; |
| 54 | + if (field == "prefix_length") return lpm.prefix_length; |
| 55 | + return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC) |
| 56 | + << "LPM has no field \"" << field << "\""; |
| 57 | + }, |
| 58 | + }, |
| 59 | + symbolic_key); |
| 60 | +} |
| 61 | + |
| 62 | +} // namespace |
| 63 | + |
| 64 | +absl::StatusOr<SymbolicKey> AddSymbolicKey(const KeyInfo& key, |
| 65 | + z3::solver& solver) { |
| 66 | + ASSIGN_OR_RETURN(int bitwidth, ast::TypeBitwidthOrStatus(key.type)); |
| 67 | + if (bitwidth == 0) { |
| 68 | + return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC) |
| 69 | + << "expected a key type with bitwidth > 0, but got: " << key; |
| 70 | + } |
| 71 | + switch (key.type.type_case()) { |
| 72 | + case ast::Type::kExact: { |
| 73 | + return SymbolicExact{ |
| 74 | + .value = solver.ctx().bv_const(key.name.c_str(), bitwidth), |
| 75 | + }; |
| 76 | + } |
| 77 | + case ast::Type::kOptionalMatch: |
| 78 | + case ast::Type::kTernary: { |
| 79 | + // Optionals and ternaries are both encoded as ternaries. |
| 80 | + z3::expr value = solver.ctx().bv_const(key.name.c_str(), bitwidth); |
| 81 | + z3::expr mask = solver.ctx().bv_const( |
| 82 | + absl::StrCat(key.name, "_mask").c_str(), bitwidth); |
| 83 | + // This is a P4RT canonicity constraint ensuring that masked-off bits must |
| 84 | + // be zero. |
| 85 | + solver.add((mask & value) == value); |
| 86 | + if (key.type.has_optional_match()) { |
| 87 | + // For optionals in P4RT, the mask must be either 0 (denoting a |
| 88 | + // wildcard) or all ones (denoting an exact match). '-1' is equivalent |
| 89 | + // to an all_one bitvector in Z3. |
| 90 | + solver.add(mask == 0 || mask == -1); |
| 91 | + } |
| 92 | + return SymbolicTernary{ |
| 93 | + .value = value, |
| 94 | + .mask = mask, |
| 95 | + }; |
| 96 | + } |
| 97 | + case ast::Type::kLpm: { |
| 98 | + z3::expr value = solver.ctx().bv_const(key.name.c_str(), bitwidth); |
| 99 | + z3::expr prefix_length = solver.ctx().int_const( |
| 100 | + absl::StrCat(key.name, "_prefix_length").c_str()); |
| 101 | + z3::expr suffix_length = z3::int2bv( |
| 102 | + /*bitwidth=*/bitwidth, /*z3_int_expr=*/bitwidth - prefix_length); |
| 103 | + // For LPMs, the prefix length must be no larger than the bitwidth, and |
| 104 | + // only `prefix_length` bits of the value should be set. We capture the |
| 105 | + // second constraint by saying that the value is unchanged after two bit |
| 106 | + // shifts. |
| 107 | + solver.add(prefix_length >= 0 && prefix_length <= bitwidth && |
| 108 | + z3::shl(z3::lshr(value, suffix_length), suffix_length) == |
| 109 | + value); |
| 110 | + return SymbolicLpm{ |
| 111 | + .value = value, |
| 112 | + .prefix_length = prefix_length, |
| 113 | + }; |
| 114 | + } |
| 115 | + |
| 116 | + // TODO(b/291779521): Range matches are not currently supported. |
| 117 | + case ast::Type::kRange: |
| 118 | + return gutils::UnimplementedErrorBuilder(GUTILS_LOC) |
| 119 | + << "Range matches are not currently supported by the " |
| 120 | + "p4-constraints symbolic representation."; |
| 121 | + |
| 122 | + // Non-match types. |
| 123 | + case ast::Type::kUnknown: |
| 124 | + case ast::Type::kUnsupported: |
| 125 | + case ast::Type::kBoolean: |
| 126 | + case ast::Type::kArbitraryInt: |
| 127 | + case ast::Type::kFixedUnsigned: |
| 128 | + case ast::Type::TYPE_NOT_SET: |
| 129 | + return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC) |
| 130 | + << "expected a match type, but got: " << key; |
| 131 | + } |
| 132 | + return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC) |
| 133 | + << "got invalid type: " << key; |
| 134 | +} |
| 135 | + |
| 136 | +absl::StatusOr<z3::expr> GetValue(const SymbolicKey& symbolic_key) { |
| 137 | + return GetFieldAccess(symbolic_key, "value"); |
| 138 | +} |
| 139 | + |
| 140 | +absl::StatusOr<z3::expr> GetMask(const SymbolicKey& symbolic_key) { |
| 141 | + return GetFieldAccess(symbolic_key, "mask"); |
| 142 | +} |
| 143 | + |
| 144 | +absl::StatusOr<z3::expr> GetPrefixLength(const SymbolicKey& symbolic_key) { |
| 145 | + return GetFieldAccess(symbolic_key, "prefix_length"); |
| 146 | +} |
| 147 | + |
| 148 | +} // namespace p4_constraints |
0 commit comments