Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
70 changes: 70 additions & 0 deletions examples/features/tuples/nested_tuples.dpt
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
// Polymorphic parsers using nested tuple arguments.
// Eth header
type eth_t = {
int<48> dst_mac;
int<48> src_mac;
int<16> etype;
}
const int<16> IP_ETHERTY = 0x0800;

// IPv4 header type
type ip_t = {
int<4> version;
int<4> ihl;
int<8> diffserv;
int<16> total_len;
int<16> id;
int<3> flags;
int<13> frag_offset;
int<8> ttl;
int<8> protocol;
int<16> hdr_csum;
int<32> src;
int<32> dst;
}

type udp_t = {
int<16> src_port;
int<16> dst_port;
int<16> length;
int<16> csum;
}

event passthrough(auto hdrs, Payload.t payload) {
generate_port(0, this);
}

parser parse_udp(auto l2_hdrs, bitstring pkt) {
udp_t udp = read(pkt);
match udp#dst_port with
| 2152 -> {
generate passthrough((l2_hdrs, udp), Payload.parse(pkt));
}
| _ -> {
generate passthrough((l2_hdrs, udp), Payload.parse(pkt));
}
}

parser parse_ip(auto l1_hdrs, bitstring pkt) {
ip_t ip = read(pkt);
match ip#protocol with
| 0x11 -> {
parse_udp((l1_hdrs, ip), pkt);
}
| 132 -> {
generate passthrough((l1_hdrs, ip), Payload.parse(pkt));
}
| _ -> {
generate passthrough((l1_hdrs, ip), Payload.parse(pkt));
}
}


parser main(bitstring pkt) {
eth_t e = read(pkt);
match e#etype with
| LUCID_ETHERTY -> { do_lucid_parsing(pkt); } // call builtin parser
| IP_ETHERTY -> { parse_ip(e, pkt); }
| _ -> { generate passthrough(e, Payload.parse(pkt)); }
}

17 changes: 17 additions & 0 deletions examples/features/tuples/tuple_event.dpt
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@

event tuple_foo(auto xy);
handle tuple_foo(auto xy) {
printf("here in tuple_foo");
}


event foo(int x, int y);
handle foo(int x, int y) {
if (x == 1) {
tuple<<int, int>> xy = (x, y);
generate(tuple_foo(xy));
} else {
generate(tuple_foo(x));
}
generate(foo(1, 2));
}
16 changes: 16 additions & 0 deletions examples/features/tuples/tuple_event2.dpt
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@

event tuple_foo(auto xy);
handle tuple_foo(auto xy) {
generate_port(1, tuple_foo(xy));
}


event foo(int x, int y);
handle foo(int x, int y) {
if (x == 1) {
tuple<<int, int>> xy = (x, y);
generate(tuple_foo(xy));
} else {
generate(tuple_foo(x));
}
}
55 changes: 55 additions & 0 deletions examples/features/tuples/tuple_event3.dpt
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
// Simple IP packet function that is generic to underlay headers.
// Uses tuples and polymorphic event parameters.
type eth_t = {
int<48> dmac;
int<48> smac;
int<16> ety;
}
type ip_hdr_t = {
int<32> src;
int<32> dst;
int<16> len;
}
type vlan_t = {
int<16> vty;
}

const int<16> ETY_IP = 0x0800;
const int<16> ETY_VLAN = 0x8080;

// packet event anon(auto hdrs, Payload.t payload) {
// generate_port(1, anon(hdrs, payload));
// }

packet event ip_packet(auto underlay_headers, ip_hdr_t ip_hdr, Payload.t unparsed_payload) {
ip_hdr_t new_ip_hdr = {ip_hdr with src = ip_hdr#dst; dst = ip_hdr#src;};
event pkt_out = ip_packet(underlay_headers, new_ip_hdr, unparsed_payload);
generate_port(1, pkt_out);
}

parser main(bitstring pkt) {
eth_t eth_hdr = read(pkt);
match eth_hdr#ety with
| LUCID_ETHERTY -> { do_lucid_parsing(pkt); }
| ETY_IP -> {
ip_hdr_t ip_hdr = read(pkt);
generate ip_packet(eth_hdr, ip_hdr, Payload.parse(pkt));
}
| ETY_VLAN -> {
vlan_t vlan_hdr = read(pkt);
match vlan_hdr#vty with
| ETY_IP -> {
ip_hdr_t ip_hdr =read(pkt);
generate ip_packet((eth_hdr, vlan_hdr), ip_hdr, Payload.parse(pkt));
}
| _ -> {
drop;
// generate anon((eth_hdr, vlan_hdr), Payload.parse(pkt));
}
}
| _ -> {
drop;
// generate anon(eth_hdr, Payload.parse(pkt));
}
}

15 changes: 15 additions & 0 deletions examples/features/tuples/tuple_event4.dpt
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
type my_t = {
int a;
int b;
}

event my_event(my_t my_arg);
handle my_event(my_t my_arg) {
my_t new_arg = {a=my_arg#b; b=my_arg#a;};
generate(my_event(new_arg));
}

event foo(int x, int y, int z, int zz);
handle foo(int x, int y, int z, int zz){
generate(my_event({a=x; b=y;}));
}
11 changes: 11 additions & 0 deletions examples/features/tuples/tuple_event_wrong.dpt
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
event tuple_foo(auto xy);
handle tuple_foo(auto xy) {
if (xy == (1, 2, 3)) {
printf("here");
}
}
event foo(int x, int y);
handle foo(int x, int y) {
tuple<<int, int>> xy = (x, y);
generate(tuple_foo(xy));
}
98 changes: 98 additions & 0 deletions examples/features/tuples/tuples.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,98 @@
## Tuples and events with polymorphic parameters


This branch (26.4.tuples) adds tuples and events with polymorphic parameters to Lucid.

### Motivation

Lucid programs typically operate at specific protocol layers, meaning they are generic to the packet headers of lower layers and the headers + payload of higher layers. Previously, it was up to the programmer to define every combination of possible underlay headers as separate record types.

For instance if the programmer wants to handle IP packets that may arrive in either ethernet or vlan packets, they must write two separate handlers for each underlay protocol stack:
```
packet event eth_ip_packet(eth_t eth_hdr, ip_hdr_t ip_hdr, bytes.t unparsed_payload) {
ip_hdr_t new_ip_hdr = {ip_hdr with src_addr = ip_hdr#dst_addr; dst_addr = ip_hdr#src_addr;};
event pkt_out = eth_ip_packet(eth_hdr, new_ip_hdr, unparsed_payload);
generate_port(ingress_port, pkt_out);
}
packet event eth_vlan_ip_packet(eth_t eth_hdr, vlan_t vlan_hdr, ip_hdr_t ip_hdr, bytes.t unparsed_payload) {
ip_hdr_t new_ip_hdr = {ip_hdr with src_addr = ip_hdr#dst_addr; dst_addr = ip_hdr#src_addr;};
event pkt_out = eth_vlan_ip_packet(eth_hdr, vlan_hdr, new_ip_hdr, unparsed_payload);
generate(ingress_port, pkt_out);
}
```
In the above example, the handler bodies are generic with respect to the underlay headers, yet there still must be separate events and handlers. This gets unweildy very quickly in programs for more realistic networks.

The solution introduced here is to support: 1. tuples as event parameters; 2. polymorphic event parameters. Then we can rewrite the above example like this:
```
packet event ip_packet(auto underlay_headers, ip_hdr_t ip_hdr, bytes.t unparsed_payload) {
ip_hdr_t new_ip_hdr = {ip_hdr with src_addr = ip_hdr#dst_addr; dst_addr = ip_hdr#src_addr;};
event pkt_out = ip_packet(underlay_headers, new_ip_hdr, unparsed_payload);
generate(pkt_out);
}
```


### New language features

#### Tuples
Tuples are basically records with anonymous fields and whose type is defined dynamically when a variable is declared. Tuples are immutable, but can be constructed, used as arguments, and projected similarly to records.

**Tuple type declarations and expressions**

`tuple<<int, int>> my_pair = (1, 2);`

**Tuple projection**

`int a = my_pair.0; int b = my_pair.1;`

#### Polymorphic event parameters
Parameters in events and handlers may now be polymorphic, using the `auto` type keyword:

```
packet event ip_packet(auto underlay_headers, ...);
handler ip_packet(auto underlay_headers, ...);
```

Polymorphism works almost the same as for functions, with one exception. In a function, the type system allows the body of a function to restrict a polymorphic parameter to a specific type by operating on it. For example:
```
fun foo(auto x) { int y = x + 1;} // the type checker infers type int for x
```

This is not (currently) allowed for events. Any operation on a polymorphic parameter in a handler body that requires the parameter to be a specific type will cause a typing error.

Events with polymorphic parameters may not be given user-defined tag numbers (because they are eliminated by monomorphization, which duplicates the declarations).

### Implementation

Tuples have dedicated AST nodes in the frontend syntax, and are eliminated before the midend.

Polymorphic event parameters are unified with the respective handler parameters by the type checker, and handlers are checked to not restrict the type of their polymorphic parameters.

Polymorphic events are eliminated by creating monomorphic duplicates based on event-typed expressions in the program (i.e., event constructors).

It is currently a runtime error to send a program an event value with an argument that uses a parameter with a type not used elsewhere in the program.

For example, if the program defines: `packet event foo(auto x, ...);`
and only ever uses `foo(int x)` events, it is a runtime error to pass in an event `foo(bool x)`.


### Test cases

`tuple_event.dpt` -- minimal example of tuples
`tuple_event_wrong.dpt` -- a handler using a polymorphic tuple parameter incorrectly
`tuple_event2.dpt` -- a handler using a polymorphic tuple parameter correctly
`tuple_event3.dpt` -- event using a polymorphic parameter with different tuple types depending on parsing (this is the ip_packet example from the motivation).
`nested_tuples.dpt` -- demonstrates support for parsers that also use tuple arguments and polymorphism.

### Future considerations

- The interpreter should be updated to support input of non-packet events with tuple types.

- It may be useful for users to define polymorphic events with monomorphic handlers, for specific instances that they want to handle, but are not generated in the program. For example:
```
event foo(auto x, auto y);
handle foo(int x, int y) { ... }
handle foo(bool x, bool y){ ... };
```

- The polymorphic event elimination pass may fail for programs that place transitive restrictions on the types of polymorphic event parameters. See the comment in MonomorphicEventArgs.ml for more information.
4 changes: 4 additions & 0 deletions src/bin/InterpMain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,10 @@ let main () =
in
match spec_file with
| None ->
(* run the midend pipeline for debugging *)
(* let _ =
MidendPipeline.process_prog ds
in *)
Console.report "No specification file provided, so skipping simulation"
| Some spec_file ->
let ds =
Expand Down
2 changes: 2 additions & 0 deletions src/lib/dune
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,9 @@
sizeInlining
builtinsTupleElimination
renaming
monomorphicEventArgs
globalArgElimination
refreshTypes
explicitReturns
moduleAliasing
recordElimination
Expand Down
13 changes: 11 additions & 2 deletions src/lib/frontend/FrontendPipeline.ml
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,8 @@ let process_prog ?(opts=def_opts) builtin_tys ds =
print_if_debug ds;
(* TODO: Might be nice to have an additional renaming pass earlier, so we
can run the slot analysis immediately after typing *)
(* TODO: fix slot analysis *)
print_if_verbose "-------Performing parser slot analysis---------";
let slot_assignments = SlotAnalysis.analyze_prog ds in
print_if_verbose "-------Eliminating modules---------";
let ds = ModuleElimination.eliminate_prog ds in
print_if_debug ds;
Expand All @@ -65,6 +65,8 @@ let process_prog ?(opts=def_opts) builtin_tys ds =
print_if_verbose "---------Eliminating events with global arguments----------";
let ds = GlobalArgElimination.eliminate_prog ds in
print_if_debug ds;
(* print_if_verbose "---------Making Polymorphic Events Monomorphic----------"; *)
let poly_event_renaming, ds = MonomorphicEventArgs.eliminate_prog builtin_tys ds in
print_if_verbose "---------------typing3-------------";
let ds = Typer.infer_prog builtin_tys ds in
print_if_debug ds;
Expand Down Expand Up @@ -98,6 +100,7 @@ let process_prog ?(opts=def_opts) builtin_tys ds =
let ds = RecordElimination.eliminate_prog ds in
print_if_debug ds;
print_if_verbose "---------------typing7-------------";

let ds = Typer.infer_prog builtin_tys ds in
ds)
else (
Expand All @@ -119,13 +122,19 @@ let process_prog ?(opts=def_opts) builtin_tys ds =
print_if_debug ds;
print_if_verbose "---------------typing9-------------";
let ds = Typer.infer_prog builtin_tys ds in
(* Slot analysis does not handle tuples, polymorphic event args, or possibly modules,
so until we get back to it, the earliest it can go is here. *)
let slot_assignments = SlotAnalysis.analyze_prog ds in

print_if_verbose "-------Inlining Constants-------";
let ds = ConstInlining.inline_prog ds in
print_if_debug ds;
(* Not sure if this is still necessary *)
print_if_verbose "-----------re-re-renaming-----------";
let renaming'', ds = Renaming.rename ds in
let renaming = Renaming.compose_envs [renaming; renaming'; renaming''] in
let renaming = Renaming.compose_envs [renaming;
poly_event_renaming;
renaming'; renaming''] in
print_if_debug ds;
print_if_verbose "---------------typing again-------------";
(* Just to be safe *)
Expand Down
1 change: 1 addition & 0 deletions src/lib/frontend/Lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ rule token = parse
| "else" { ELSE (position lexbuf) }
| "int" { TINT (position lexbuf) }
| "bool" { TBOOL (position lexbuf) }
| "tuple" { TUPLE (position lexbuf) }
| "event" { EVENT (position lexbuf) }
| "generate" { GENERATE (position lexbuf) }
| "generate_switch" { SGENERATE (position lexbuf) }
Expand Down
Loading