The parser yields an instance of class HeaderDeclaration
for every encountered P4 declaration.
This data structure contains the names of the fields, the width and the offset from the beginning of the header.
Note that header field lengths that are runtime determined are not supported by vanilla SEFL.
Also field modifiers are ignored (saturating, signed etc).
- Header Instances
A defined header instance is identified either by:
- a name
- a name + an index - in case of array instances
Implemented and tested (visually): modify_field
, subtract_from_field
, register_read
Actions currently implemented, but not tested thouroughly: add_header
, copy_header
,
remove_header
, add_to_field
, add
, push
, pop
, resubmit
, register_write
,
resubmit
, recirculate
, clone_i2i
, clone_i2e
, clone_e2i
, clone_e2e
See test case "NAT spec can be parsed - actions, reg defs and field lists are there" in
HeaderDefinitionParsingTest
class
Currently implemented: add_to_field
, add
, subtract_from_field
, subtract
.
Should be implementable: modify_field
, modify_field_rng_uniform
, TBD: bitwise operations.
Cannot be implemented: modify_field_with_hash_based_offset
Currently implemented: TBD
Should be implementable: add_header
, copy_header
, remove_header
, push
, pop
Cannot be implemented: TBD
The switch needs to be initialized whenever it is started - i.e. zero out registers and counters - and whenever a new packet enters the pipeline - i.e. zero out or initialize metadata instances and headers.
Class org.change.parser.p4.InitializeCode
has methods switchInitializeGlobally
for global init
and switchInitializePacketEnter
which initializes metadata and header instances
prior to parsing assuming standard_metadata.instance_type == normal
(i.e. not clone, nor recirculate or resubmit)
See test cases "SWITCH - new packet initializer" and "SWITCH - global initializer" in HeaderDefinitionParsingTest
class
Addressing a global register (string with the following format): s"${switchInstance.getName}.reg.${argSource1.toString}[$intVal]"
Addressing a static register - per table - (string with the following format): s"${switchInstance.getName}.reg[$table].${argSource1.toString}[$intVal]"
Addressing a direct register - per flow@table - not implemented
Addressing metadata instance: as a string of the following format:
x.getName + "." + f.getName
, where x is a HeaderInstance and f is a field defined for the given layoutx.getName + index + "." + f.getName
, where x is an ArrayInstance, index is an integer referencing an array index and f is a field for the given layout
Each header_instance
declared by the P4 program may be valid or invalid. Thus, a validity flag
is declared for all header instances declared by the P4 program. In the packet_in initializer code,
all validity flags for all declared header instances are set to 0.
In order to handle validity of array instances, there is one validity flag for each entry in the array instance (assuming static length). To address the validity flag for each header instance, the following naming convention was employed:
- For arrays:
hname + x + ".IsValid"
, wherehname
is the name of the header array,x
is the index in the array - For scalars:
hname + ".IsValid"
, wherehname
is the name of the scalar header instance
Some per-table metadata are required for matching in the control flow functions.
<action_name>.Fired
- a flag which indicates if the actions was fired (0 or 1)<table_name>.Hit
- a flag which indicates if any entry in the table was matched (0 or 1)IsClone
- a flag which indicates that the current state is a clone. This flag is used to bypass the current table, as there might be rules which also apply to it. At the end of the current table, the clone (aka cloneForward
operation is executed and the packet is sent to the desired locationegress
oringress
)
A P4 switch is composed of the following components:
- control functions (denoted
control.<control_function_name>
) - table calls (denoted
table.<table_name>.in.<table_call_id>
, wheretable_call_id
is a pseudo-random string which ensures proper connection in the control flow - parser mechanism (denoted
<switch_instance_name>.parser.in
) - shall convert the current tagged representation to a parsed packet representation and shall set all<header_instance>.IsValid
flags to 1 for all headers which were extracted. NB: All header instance fields shall be allocated with their fixed size as declared. At the end of the parser function, the resulting parsed representation will be saved for clone cases. As such, let<header_instance>.<field>
be a field in the resulting parsed packet, thenOriginal.<header_instance>.<field>
shall be allocated with the corresponding width and assigned as a reference to the current<header_instance>.<field>
's value - deparser mechanism (denoted
<switch_instance_name>.deparser.in
) - shall convert the current parsed packet representation to a tag-based representation - buffer mechanism (denoted
<switch_instance_name>.buffer.in
) - performsegress_port
population based on the currentegress_spec
if normal copy orclone_spec
if clone copy - output mechanism (denoted
<switch_instance_name>.output.in
) perfoms the actual forwarding of a packet to one of the switch's declared interfaces based on the setegress_port
. If a port with the given id is not found, the execution fails. - input mechanism (denoted
<switch_instance_name>.input.in
) - performsingress_port
population and initializes header instances and metadata. After this point, all header instances shall have<header_instance>.IsValid
flag set to 0
Links:
-
A control function may perform one or more table calls.
-
The input mechanism links to the parser mechanism
-
The parser mechanism links to the ingress control function
-
The ingress control function links to the buffer mechanism
-
The buffer mechanism links to the egress control function
-
The egress control function links to the output mechanism
Currently, a limited implementation for some bitwise operands is provided.
As such, the Z3BVSolver
succesfully handles the and
, or
, xor
operations.
- Shift left, multiplication and division operations are not implemented
recirculate
andresubmit
instructions are not implemented entirely as per spec - in the spec the packet is marked for resubmission and only at the end of the current pipeline is it resubmited for processing to the parser. Also, the effect of multiple recirculate/resubmit actions is not taken into account- Meters and counters are not implemented. Consequently, no actions which take inputs meter or counter references are implemented
- No calculations are currently implemented. Consequently, no actions which take as inputs calculated fields are implemented
count
instruction is not implemented- The current parser and interpreter works on p4 codes where declarations are prior to usage in functions. As such, all header types need to be declared first, then all header instances, then actions. Manually modify P4 files accordingly
- The current parser cannot ignore comments. - Worked around using approach in issue 8.
- The current parser has no built-in precompile step and will throw whenever
macro definitions are used - in order to use still use them, run the following command
assuming
f.p4
is your input file:gcc -E -x c -P f.p4 > f-ppc.p4
and then run Symnet-P4 integration against the pre-processed filef-ppc.p4
- No support for parser
value sets
- No support for variable-width header fields
Vera was tested against several p4 examples located in the inputs/ folder.
The bulk of the test-cases are in src/test/scala/parser/p4/test. A good starting place for exploring the codebase is in class P4Nat in test("INTEGRATION - simple-nat test no entries")
Running Vera implies:
- Parsing a p4 file => P4 AST i.e. class Switch in package org.change.v2.p4.model
- Parsing a commands file + P4 AST => abstract class ISwitchInstance in package org.change.v2.p4.model with multiple implementations
- Switch + ISwitchInstance => Equivalent SEFL program (i.e. a tuple instructions: Map[String, Instruction], links: Map[String, String]) generated in class ControlFlowInterpreter
- ControlFlowInterpreter => initial packets. It is possible to generate all packets acceptable by a P4 switch's parser. Given an object of class ControlFlowInterpreter (let's say res), the call to res.allParserStatesInstruction() will generate a set of symbolic packets which will be accepted by the parser starting from an initially clean state (i.e. State.clean).
- Customizing the control flow (Optional) class ControlFlowInterpreter can be customized to hook custom initialization code (both global and local init), custom parser/deparser codes and to accept different kinds of ISwitchInstances.
- Creating a SEFL executor from a SEFL program - class CodeAwareInstructionExecutor
- Executing the code taking some input packet(s) and port(s) and gathering the resulting states
Symbolic execution for middleboxes made easy and fast.
- JDK 8 (in case a different one is used the ScalaZ3 jar needs to be rebuilt against this, different, JDK)
- sbt - The simple build tool for Scala projects
See setup.sh for a concrete setup script (it was tested on 64bit Ubuntu 12.04, 14.04 and 15.10).
Then from project root issue sbt sample.
There is also a Vagrantfile if you prefer this option. This also uses setup.sh for provisioning.
See src/main/scala/change/v2/runners/experiments/SEFLRunner.scala to start experimenting with SEFL. sbt sample will run that code.
Look at the description of the instructions method in src/main/scala/org/change/v2/Template.scala; try to understand what the instructions attatched to input port 0 do. Check src/main/resources/click_test_files/Template.click in order to get the complete picture.
From the project root issue sbt click which performs the symbolic execution of Template.click file.
You should find the output in template.output.
Play with the code, check the output. Loop.