|
| 1 | +let core_p4_str = |
| 2 | + {|/* |
| 3 | +Copyright 2013-present Barefoot Networks, Inc. |
| 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 | + http://www.apache.org/licenses/LICENSE-2.0 |
| 8 | +Unless required by applicable law or agreed to in writing, software |
| 9 | +distributed under the License is distributed on an "AS IS" BASIS, |
| 10 | +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| 11 | +See the License for the specific language governing permissions and |
| 12 | +limitations under the License. |
| 13 | +*/ |
| 14 | + |
| 15 | +/* This is the P4-16 core library, which declares some built-in P4 constructs using P4 */ |
| 16 | + |
| 17 | +#ifndef _CORE_P4_ |
| 18 | +#define _CORE_P4_ |
| 19 | + |
| 20 | +/// Standard error codes. New error codes can be declared by users. |
| 21 | +error { |
| 22 | + NoError, /// No error. |
| 23 | + PacketTooShort, /// Not enough bits in packet for 'extract'. |
| 24 | + NoMatch, /// 'select' expression has no matches. |
| 25 | + StackOutOfBounds, /// Reference to invalid element of a header stack. |
| 26 | + HeaderTooShort, /// Extracting too many bits into a varbit field. |
| 27 | + ParserTimeout, /// Parser execution time limit exceeded. |
| 28 | + ParserInvalidArgument /// Parser operation was called with a value |
| 29 | + /// not supported by the implementation. |
| 30 | +} |
| 31 | + |
| 32 | +extern packet_in { |
| 33 | + /// Read a header from the packet into a fixed-sized header @hdr and advance the cursor. |
| 34 | + /// May trigger error PacketTooShort or StackOutOfBounds. |
| 35 | + /// @T must be a fixed-size header type |
| 36 | + void extract<T>(out T hdr); |
| 37 | + /// Read bits from the packet into a variable-sized header @variableSizeHeader |
| 38 | + /// and advance the cursor. |
| 39 | + /// @T must be a header containing exactly 1 varbit field. |
| 40 | + /// May trigger errors PacketTooShort, StackOutOfBounds, or HeaderTooShort. |
| 41 | + void extract<T>(out T variableSizeHeader, |
| 42 | + in bit<32> variableFieldSizeInBits); |
| 43 | + /// Read bits from the packet without advancing the cursor. |
| 44 | + /// @returns: the bits read from the packet. |
| 45 | + /// T may be an arbitrary fixed-size type. |
| 46 | + T lookahead<T>(); |
| 47 | + /// Advance the packet cursor by the specified number of bits. |
| 48 | + void advance(in bit<32> sizeInBits); |
| 49 | + /// @return packet length in bytes. This method may be unavailable on |
| 50 | + /// some target architectures. |
| 51 | + bit<32> length(); |
| 52 | +} |
| 53 | + |
| 54 | +extern packet_out { |
| 55 | + /// Write @hdr into the output packet, advancing cursor. |
| 56 | + /// @T can be a header type, a header stack, a header_union, or a struct |
| 57 | + /// containing fields with such types. |
| 58 | + void emit<T>(in T hdr); |
| 59 | +} |
| 60 | + |
| 61 | +// TODO: remove from this file, convert to built-in |
| 62 | +/// Check a predicate @check in the parser; if the predicate is true do nothing, |
| 63 | +/// otherwise set the parser error to @toSignal, and transition to the `reject` state. |
| 64 | +extern void verify(in bool check, in error toSignal); |
| 65 | + |
| 66 | +/// Built-in action that does nothing. |
| 67 | +action NoAction() {} |
| 68 | + |
| 69 | +/// Standard match kinds for table key fields. |
| 70 | +/// Some architectures may not support all these match kinds. |
| 71 | +/// Architectures can declare additional match kinds. |
| 72 | +match_kind { |
| 73 | + /// Match bits exactly. |
| 74 | + exact, |
| 75 | + /// Ternary match, using a mask. |
| 76 | + ternary, |
| 77 | + /// Longest-prefix match. |
| 78 | + lpm |
| 79 | +} |
| 80 | + |
| 81 | +#endif /* _CORE_P4_ */ |
| 82 | +|} |
| 83 | + |
| 84 | +let core_v1_model_str = |
| 85 | + {|/* |
| 86 | +Copyright 2013-present Barefoot Networks, Inc. |
| 87 | + |
| 88 | +Licensed under the Apache License, Version 2.0 (the "License"); |
| 89 | +you may not use this file except in compliance with the License. |
| 90 | +You may obtain a copy of the License at |
| 91 | + |
| 92 | + http://www.apache.org/licenses/LICENSE-2.0 |
| 93 | + |
| 94 | +Unless required by applicable law or agreed to in writing, software |
| 95 | +distributed under the License is distributed on an "AS IS" BASIS, |
| 96 | +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| 97 | +See the License for the specific language governing permissions and |
| 98 | +limitations under the License. |
| 99 | +*/ |
| 100 | + |
| 101 | +/* P4-16 declaration of the P4 v1.0 switch model */ |
| 102 | + |
| 103 | +#ifndef _V1_MODEL_P4_ |
| 104 | +#define _V1_MODEL_P4_ |
| 105 | + |
| 106 | +#include "core.p4" |
| 107 | + |
| 108 | +match_kind { |
| 109 | + range, |
| 110 | + // Used for implementing dynamic_action_selection |
| 111 | + selector |
| 112 | +} |
| 113 | + |
| 114 | +// Are these correct? |
| 115 | +@metadata @name("standard_metadata") |
| 116 | +struct standard_metadata_t { |
| 117 | + bit<9> ingress_port; |
| 118 | + bit<9> egress_spec; |
| 119 | + bit<9> egress_port; |
| 120 | + bit<32> clone_spec; |
| 121 | + bit<32> instance_type; |
| 122 | + // The drop and recirculate_port fields are not used at all by the |
| 123 | + // behavioral-model simple_switch software switch as of September |
| 124 | + // 2018, and perhaps never was. They may be considered |
| 125 | + // deprecated, at least for that P4 target device. simple_switch |
| 126 | + // uses the value of the egress_spec field to determine whether a |
| 127 | + // packet is dropped or not, and it is recommended to use the |
| 128 | + // P4_14 drop() primitive action, or the P4_16 + v1model |
| 129 | + // mark_to_drop() primitive action, to cause that field to be |
| 130 | + // changed so the packet will be dropped. |
| 131 | + bit<1> drop; |
| 132 | + bit<16> recirculate_port; |
| 133 | + bit<32> packet_length; |
| 134 | + // |
| 135 | + // @alias is used to generate the field_alias section of the BMV2 JSON. |
| 136 | + // Field alias creates a mapping from the metadata name in P4 program to |
| 137 | + // the behavioral model's internal metadata name. Here we use it to |
| 138 | + // expose all metadata supported by simple switch to the user through |
| 139 | + // standard_metadata_t. |
| 140 | + // |
| 141 | + // flattening fields that exist in bmv2-ss |
| 142 | + // queueing metadata |
| 143 | + @alias("queueing_metadata.enq_timestamp") bit<32> enq_timestamp; |
| 144 | + @alias("queueing_metadata.enq_qdepth") bit<19> enq_qdepth; |
| 145 | + @alias("queueing_metadata.deq_timedelta") bit<32> deq_timedelta; |
| 146 | + @alias("queueing_metadata.deq_qdepth") bit<19> deq_qdepth; |
| 147 | + // intrinsic metadata |
| 148 | + @alias("intrinsic_metadata.ingress_global_timestamp") bit<48> ingress_global_timestamp; |
| 149 | + @alias("intrinsic_metadata.egress_global_timestamp") bit<48> egress_global_timestamp; |
| 150 | + @alias("intrinsic_metadata.lf_field_list") bit<32> lf_field_list; |
| 151 | + @alias("intrinsic_metadata.mcast_grp") bit<16> mcast_grp; |
| 152 | + @alias("intrinsic_metadata.resubmit_flag") bit<32> resubmit_flag; |
| 153 | + @alias("intrinsic_metadata.egress_rid") bit<16> egress_rid; |
| 154 | + /// Indicates that a verify_checksum() method has failed. |
| 155 | + // 1 if a checksum error was found, otherwise 0. |
| 156 | + bit<1> checksum_error; |
| 157 | + @alias("intrinsic_metadata.recirculate_flag") bit<32> recirculate_flag; |
| 158 | + /// Error produced by parsing |
| 159 | + error parser_error; |
| 160 | +} |
| 161 | + |
| 162 | +enum CounterType { |
| 163 | + packets, |
| 164 | + bytes, |
| 165 | + packets_and_bytes |
| 166 | +} |
| 167 | + |
| 168 | +enum MeterType { |
| 169 | + packets, |
| 170 | + bytes |
| 171 | +} |
| 172 | + |
| 173 | +extern counter { |
| 174 | + counter(bit<32> size, CounterType type); |
| 175 | + void count(in bit<32> index); |
| 176 | +} |
| 177 | + |
| 178 | +extern direct_counter { |
| 179 | + direct_counter(CounterType type); |
| 180 | + void count(); |
| 181 | +} |
| 182 | + |
| 183 | +extern meter { |
| 184 | + meter(bit<32> size, MeterType type); |
| 185 | + void execute_meter<T>(in bit<32> index, out T result); |
| 186 | +} |
| 187 | + |
| 188 | +extern direct_meter<T> { |
| 189 | + direct_meter(MeterType type); |
| 190 | + void read(out T result); |
| 191 | +} |
| 192 | + |
| 193 | +extern register<T> { |
| 194 | + register(bit<32> size); |
| 195 | + void read(out T result, in bit<32> index); |
| 196 | + void write(in bit<32> index, in T value); |
| 197 | +} |
| 198 | + |
| 199 | +// used as table implementation attribute |
| 200 | +extern action_profile { |
| 201 | + action_profile(bit<32> size); |
| 202 | +} |
| 203 | + |
| 204 | +// Get a random number in the range lo..hi |
| 205 | +extern void random<T>(out T result, in T lo, in T hi); |
| 206 | +// If the type T is a named struct, the name is used |
| 207 | +// to generate the control-plane API. |
| 208 | +extern void digest<T>(in bit<32> receiver, in T data); |
| 209 | + |
| 210 | +enum HashAlgorithm { |
| 211 | + crc32, |
| 212 | + crc32_custom, |
| 213 | + crc16, |
| 214 | + crc16_custom, |
| 215 | + random, |
| 216 | + identity, |
| 217 | + csum16, |
| 218 | + xor16 |
| 219 | +} |
| 220 | + |
| 221 | +extern void mark_to_drop(); |
| 222 | +extern void hash<O, T, D, M>(out O result, in HashAlgorithm algo, in T base, in D data, in M max); |
| 223 | + |
| 224 | +extern action_selector { |
| 225 | + action_selector(HashAlgorithm algorithm, bit<32> size, bit<32> outputWidth); |
| 226 | +} |
| 227 | + |
| 228 | +enum CloneType { |
| 229 | + I2E, |
| 230 | + E2E |
| 231 | +} |
| 232 | + |
| 233 | +@deprecated("Please use verify_checksum/update_checksum instead.") |
| 234 | +extern Checksum16 { |
| 235 | + Checksum16(); |
| 236 | + bit<16> get<D>(in D data); |
| 237 | +} |
| 238 | + |
| 239 | +/** |
| 240 | +Verifies the checksum of the supplied data. |
| 241 | +If this method detects that a checksum of the data is not correct it |
| 242 | +sets the standard_metadata checksum_error bit. |
| 243 | +@param T Must be a tuple type where all the fields are bit-fields or varbits. |
| 244 | + The total dynamic length of the fields is a multiple of the output size. |
| 245 | +@param O Checksum type; must be bit<X> type. |
| 246 | +@param condition If 'false' the verification always succeeds. |
| 247 | +@param data Data whose checksum is verified. |
| 248 | +@param checksum Expected checksum of the data; note that is must be a left-value. |
| 249 | +@param algo Algorithm to use for checksum (not all algorithms may be supported). |
| 250 | + Must be a compile-time constant. |
| 251 | +*/ |
| 252 | +extern void verify_checksum<T, O>(in bool condition, in T data, inout O checksum, HashAlgorithm algo); |
| 253 | +/** |
| 254 | +Computes the checksum of the supplied data. |
| 255 | +@param T Must be a tuple type where all the fields are bit-fields or varbits. |
| 256 | + The total dynamic length of the fields is a multiple of the output size. |
| 257 | +@param O Output type; must be bit<X> type. |
| 258 | +@param condition If 'false' the checksum is not changed |
| 259 | +@param data Data whose checksum is computed. |
| 260 | +@param checksum Checksum of the data. |
| 261 | +@param algo Algorithm to use for checksum (not all algorithms may be supported). |
| 262 | + Must be a compile-time constant. |
| 263 | +*/ |
| 264 | +extern void update_checksum<T, O>(in bool condition, in T data, inout O checksum, HashAlgorithm algo); |
| 265 | + |
| 266 | +/** |
| 267 | +Verifies the checksum of the supplied data including the payload. |
| 268 | +The payload is defined as "all bytes of the packet which were not parsed by the parser". |
| 269 | +If this method detects that a checksum of the data is not correct it |
| 270 | +sets the standard_metadata checksum_error bit. |
| 271 | +@param T Must be a tuple type where all the fields are bit-fields or varbits. |
| 272 | + The total dynamic length of the fields is a multiple of the output size. |
| 273 | +@param O Checksum type; must be bit<X> type. |
| 274 | +@param condition If 'false' the verification always succeeds. |
| 275 | +@param data Data whose checksum is verified. |
| 276 | +@param checksum Expected checksum of the data; note that is must be a left-value. |
| 277 | +@param algo Algorithm to use for checksum (not all algorithms may be supported). |
| 278 | + Must be a compile-time constant. |
| 279 | +*/ |
| 280 | +extern void verify_checksum_with_payload<T, O>(in bool condition, in T data, inout O checksum, HashAlgorithm algo); |
| 281 | +/** |
| 282 | +Computes the checksum of the supplied data including the payload. |
| 283 | +The payload is defined as "all bytes of the packet which were not parsed by the parser". |
| 284 | +@param T Must be a tuple type where all the fields are bit-fields or varbits. |
| 285 | + The total dynamic length of the fields is a multiple of the output size. |
| 286 | +@param O Output type; must be bit<X> type. |
| 287 | +@param condition If 'false' the checksum is not changed |
| 288 | +@param data Data whose checksum is computed. |
| 289 | +@param checksum Checksum of the data. |
| 290 | +@param algo Algorithm to use for checksum (not all algorithms may be supported). |
| 291 | + Must be a compile-time constant. |
| 292 | +*/ |
| 293 | +extern void update_checksum_with_payload<T, O>(in bool condition, in T data, inout O checksum, HashAlgorithm algo); |
| 294 | + |
| 295 | +extern void resubmit<T>(in T data); |
| 296 | +extern void recirculate<T>(in T data); |
| 297 | +extern void clone(in CloneType type, in bit<32> session); |
| 298 | +extern void clone3<T>(in CloneType type, in bit<32> session, in T data); |
| 299 | + |
| 300 | +extern void truncate(in bit<32> length); |
| 301 | + |
| 302 | +// The name 'standard_metadata' is reserved |
| 303 | + |
| 304 | +// Architecture. |
| 305 | +// M should be a struct of structs |
| 306 | +// H should be a struct of headers, stacks or header_unions |
| 307 | + |
| 308 | +parser Parser<H, M>(packet_in b, |
| 309 | + out H parsedHdr, |
| 310 | + inout M meta, |
| 311 | + inout standard_metadata_t standard_metadata); |
| 312 | + |
| 313 | +/* The only legal statements in the implementation of the |
| 314 | +VerifyChecksum control are: block statements, calls to the |
| 315 | +verify_checksum and verify_checksum_with_payload methods, |
| 316 | +and return statements. */ |
| 317 | +control VerifyChecksum<H, M>(inout H hdr, |
| 318 | + inout M meta); |
| 319 | +@pipeline |
| 320 | +control Ingress<H, M>(inout H hdr, |
| 321 | + inout M meta, |
| 322 | + inout standard_metadata_t standard_metadata); |
| 323 | +@pipeline |
| 324 | +control Egress<H, M>(inout H hdr, |
| 325 | + inout M meta, |
| 326 | + inout standard_metadata_t standard_metadata); |
| 327 | + |
| 328 | +/* The only legal statements in the implementation of the |
| 329 | +ComputeChecksum control are: block statements, calls to the |
| 330 | +update_checksum and update_checksum_with_payload methods, |
| 331 | +and return statements. */ |
| 332 | +control ComputeChecksum<H, M>(inout H hdr, |
| 333 | + inout M meta); |
| 334 | +@deparser |
| 335 | +control Deparser<H>(packet_out b, in H hdr); |
| 336 | + |
| 337 | +package V1Switch<H, M>(Parser<H, M> p, |
| 338 | + VerifyChecksum<H, M> vr, |
| 339 | + Ingress<H, M> ig, |
| 340 | + Egress<H, M> eg, |
| 341 | + ComputeChecksum<H, M> ck, |
| 342 | + Deparser<H> dep |
| 343 | + ); |
| 344 | + |
| 345 | +#endif /* _V1_MODEL_P4_ */ |
| 346 | +|} |
0 commit comments