Source file Pretty.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
open Syntax
module Sexp = Core.Sexp
module Formatting = struct
open Format
type predicate_context = OR_L | OR_R | AND_L | AND_R | NEG | PAREN_PR
let (fmt : formatter) (hv : header_val) (asgn : string) : unit =
match hv with
| Meta (id, n) -> fprintf fmt "@[`%s %s %Lu@]" id asgn n
| Switch(n) -> fprintf fmt "@[switch %s %Lu@]" asgn n
| Location(Physical n) -> fprintf fmt "@[port %s %lu@]" asgn n
| Location(FastFail n_lst) -> fprintf fmt "@[fastFail ports %s %s@]" asgn (string_of_fastfail n_lst)
| Location(Pipe x) -> fprintf fmt "@[port %s pipe(\"%s\")@]" asgn x
| Location(Query x) -> fprintf fmt "@[port %s query(\"%s\")@]" asgn x
| From(l) -> fprintf fmt "@[from %s \"%s\"@]" asgn
(Sexp.to_string (sexp_of_abstract_location l))
| AbstractLoc(l) -> fprintf fmt "@[loc %s \"%s\"@]" asgn
(Sexp.to_string (sexp_of_abstract_location l))
| EthSrc(n) -> fprintf fmt "@[ethSrc %s %s@]" asgn (Frenetic_kernel.Packet.string_of_mac n)
| EthDst(n) -> fprintf fmt "@[ethDst %s %s@]" asgn (Frenetic_kernel.Packet.string_of_mac n)
| Vlan(n) -> fprintf fmt "@[vlanId %s %d@]" asgn n
| VlanPcp(n) -> fprintf fmt "@[vlanPcp %s %u@]" asgn n
| EthType(n) -> fprintf fmt "@[ethTyp %s 0x%x@]" asgn n
| IPProto(n) -> fprintf fmt "@[ipProto %s 0x%x@]" asgn n
| IP4Src(n,32l) -> fprintf fmt "@[ipSrc %s %s@]" asgn (Frenetic_kernel.Packet.string_of_ip n)
| IP4Dst(n,32l) -> fprintf fmt "@[ipDst %s %s@]" asgn (Frenetic_kernel.Packet.string_of_ip n)
| IP4Src(n,m) -> fprintf fmt "@[ipSrc %s %s/%lu@]" asgn (Frenetic_kernel.Packet.string_of_ip n) m
| IP4Dst(n,m) -> fprintf fmt "@[ipDst %s %s/%lu@]" asgn (Frenetic_kernel.Packet.string_of_ip n) m
| TCPSrcPort(n) -> fprintf fmt "@[tcpSrcPort %s %u@]" asgn n
| TCPDstPort(n) -> fprintf fmt "@[tcpDstPort %s %u@]" asgn n
| VSwitch(n) -> fprintf fmt "@[vswitch %s %Lu@]" asgn n
| VPort(n) -> fprintf fmt "@[vport %s %Lu@]" asgn n
| VFabric(n) -> fprintf fmt "@[vfabric %s %Lu@]" asgn n
let rec pred (cxt : predicate_context) (fmt : formatter) (pr : pred) : unit =
match pr with
| True ->
fprintf fmt "@[id@]"
| False ->
fprintf fmt "@[drop@]"
| (Test hv) ->
format_header_val fmt hv "="
| Neg p' ->
begin match cxt with
| PAREN_PR
| NEG -> fprintf fmt "@[not %a@]" (pred NEG) p'
| _ -> fprintf fmt "@[not@ @[(%a)@]@]" (pred PAREN_PR) p'
end
| And (p1, p2) ->
begin match cxt with
| PAREN_PR
| OR_L
| OR_R
| AND_L ->
fprintf fmt "@[%a and@ %a@]" (pred AND_L) p1 (pred AND_R) p2
| _ ->
fprintf fmt "@[(@[%a and@ %a@])@]" (pred AND_L) p1 (pred AND_R) p2
end
| Or (p1, p2) ->
begin match cxt with
| PAREN_PR
| OR_L -> fprintf fmt "@[%a or@ %a@]" (pred OR_L) p1 (pred OR_R) p2
| _ -> fprintf fmt "@[(@[%a or@ %a@])@]" (pred OR_L) p1 (pred OR_R) p2
end
type policy_context =
| SEQ_L | SEQ_R
| PAR_L | PAR_R
| STAR
| PAREN
let meta_init (fmt : formatter) (init : meta_init) : unit =
match init with
| Const int64 -> fprintf fmt "%Lu" int64
| Alias hv -> fprintf fmt "%s" Fdd.Field.(of_hv hv |> to_string)
let rec pol (cxt : policy_context) (fmt : formatter) (p : policy) : unit =
match p with
| Filter (True as pr) | Filter (False as pr) ->
pred PAREN_PR fmt pr
| Filter pr ->
fprintf fmt "filter "; pred PAREN_PR fmt pr
| Mod hv ->
format_header_val fmt hv ":="
| Star p' ->
begin match cxt with
| PAREN
| STAR -> fprintf fmt "@[%a*@]" (pol STAR) p'
| _ -> fprintf fmt "@[@[(%a)*@]@]" (pol PAREN) p'
end
| Union (p1, p2) ->
begin match cxt with
| PAREN
| PAR_L -> fprintf fmt "@[%a +@ %a@]" (pol PAR_L) p1 (pol PAR_R) p2
| _ -> fprintf fmt "@[(@[%a +@ %a@])@]" (pol PAR_L) p1 (pol PAR_R) p2
end
| Seq (p1, p2) ->
begin match cxt with
| PAREN
| PAR_L
| PAR_R
| SEQ_L -> fprintf fmt "@[%a;@ %a@]" (pol SEQ_L) p1 (pol SEQ_R) p2
| _ -> fprintf fmt "@[(@[%a;@ %a@])@]" (pol SEQ_L) p1 (pol SEQ_R) p2
end
| Let {id; init; mut; body=p} ->
fprintf fmt "@[%s %s := %a in %a@]"
(if mut then "var" else "let")
id
meta_init init
(pol PAREN) p
| Link (sw,pt,sw',pt') ->
fprintf fmt "@[%Lu@@%lu =>@ %Lu@@%lu@]"
sw pt sw' pt'
| VLink (vsw,vpt,vsw',vpt') ->
fprintf fmt "@[%Lu@@%Lu =>>@ %Lu@@%Lu@]"
vsw vpt vsw' vpt'
| Dup -> fprintf fmt "@[dup@]"
end
let format_policy = Formatting.pol Formatting.PAREN
let format_pred = Formatting.pred Formatting.PAREN_PR
let string_of_policy = Frenetic_kernel.Util.make_string_of format_policy
let string_of_pred = Frenetic_kernel.Util.make_string_of format_pred
let rec pretty_assoc (p : policy) : policy = match p with
| Filter _
| Mod _
| Link _
| VLink _
| Dup -> p
| Union (p1, p2) -> pretty_assoc_par p
| Seq (p1, p2) -> pretty_assoc_seq p
| Star p' -> Star (pretty_assoc p')
| Let {id; init; mut; body} -> Let {id; init; mut; body = pretty_assoc body}
and pretty_assoc_par (p : policy) : policy = match p with
| Union (p1, Union (p2, p3)) ->
Union (pretty_assoc_par (Union (p1, p2)), pretty_assoc_par p3)
| Union (p1, p2) -> Union (pretty_assoc p1, pretty_assoc p2)
| _ -> pretty_assoc p
and pretty_assoc_seq (p : policy) : policy = match p with
| Seq (p1, Seq (p2, p3)) ->
Seq (pretty_assoc_seq (Seq (p1, p2)), pretty_assoc_seq p3)
| Seq (p1, p2) -> Seq (pretty_assoc p1, pretty_assoc p2)
| _ -> pretty_assoc p