Source file patch.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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
open Domain
open Lang
module Value = Runtime.Value
module Run = Runtime.Dynamic_Runner.Signature
open Error
open Util.Source
let rec value_as_exp (value : Value.t) : Il.exp =
let at_value = value.at in
let typ_value = value.note.typ in
let exp =
match value.it with
| BoolV b -> Il.BoolE b
| NumV n -> Il.NumE n
| TextV t -> Il.TextE t
| StructV valuefields ->
let expfields =
List.map
(fun (atom_field, value_field) ->
let exp_field = value_as_exp value_field in
(atom_field, exp_field))
valuefields
in
Il.StrE expfields
| CaseV valuecase ->
let notexp = Mixfix.map value_as_exp valuecase in
Il.CaseE notexp
| TupleV values ->
let exps = List.map value_as_exp values in
Il.TupleE exps
| OptV value_opt ->
let exp_opt = Option.map value_as_exp value_opt in
Il.OptE exp_opt
| ListV values ->
let exps = List.map value_as_exp values in
Il.ListE exps
| _ ->
error at_value
"cannot convert a function or extern value to an expression"
in
exp $$ (at_value, typ_value)
let parse_spec (layer_spec : Config.layer) (interface_spec : Config.interface) :
Value.t =
let parse_spec =
match interface_spec with
| P4_interface -> assert false
| AL_interface -> Interface.SpecTec_AL.parse_program []
| SL_interface -> Interface.SpecTec_SL.parse_program []
in
match parse_spec [ layer_spec.specdir ] with
| Run.Pass value_spec -> value_spec
| Run.Fail (`Syntax (at, msg)) -> error at msg
let parse_target (target : Config.target) (level_target : Config.level) :
Value.t =
let parse_target =
match level_target.interface with
| P4_interface -> Interface.P4.parse_program
| AL_interface | SL_interface -> assert false
in
match parse_target target.includes [ target.path ] with
| Run.Pass value_target -> value_target
| Run.Fail (`Syntax (at, msg)) -> error at msg
let apply_il (level_meta : Config.level) (value_meta : Value.t)
(value_spec : Value.t) : Value.t =
let rel_meta = level_meta.layer.rel in
let defs = Interface.SpecTec_AL.unboot_script value_spec in
let mixop_rel, inputs_rel =
List.find_map
(fun (def : Al.def) ->
match def.it with
| RelD (id, nottyp, inputs, _, _, _) when id.it = rel_meta ->
let mixop, _ = Mixfix.split nottyp.it in
Some (mixop, inputs)
| _ -> None)
defs
|> function
| Some (mixop_rel, inputs_rel) -> (mixop_rel, inputs_rel)
| None ->
error no_region
(Format.asprintf "relation %s not found in the spec" rel_meta)
in
check
(List.length inputs_rel = 1)
no_region
(Format.asprintf "relation %s must have exactly one input" rel_meta);
let def =
let id = "main" $ no_region in
let tparams = [] in
let params = [] in
let typ_ret = Il.TextT $ no_region in
let clauses =
let clause =
let args = [] in
let exp_output = Il.TextE "pass" $$ (no_region, Il.TextT) in
let prems =
let exp_bind =
Il.VarE ("x" $ no_region)
$$ (no_region, Il.VarT ("x" $ no_region, []))
in
let exp_value = value_as_exp value_meta in
let prem_bind = Il.LetPr (exp_bind, exp_value) $ no_region in
let exps_output =
List.init
(Mixop.arity mixop_rel - List.length inputs_rel)
(fun idx ->
Il.VarE ("y_" ^ string_of_int idx $ no_region)
$$ ( no_region,
Il.VarT ("y_" ^ string_of_int idx $ no_region, []) ))
in
let prem_call =
let exps =
Hints.Input.combine inputs_rel [ exp_bind ] exps_output
in
let notexp = Mixfix.fill mixop_rel exps in
Il.RulePr (rel_meta $ no_region, notexp, inputs_rel) $ no_region
in
[ prem_bind; prem_call ]
in
(args, exp_output, prems) $ no_region
in
[ clause ]
in
let elseclause_opt = None in
let hints = [] in
Al.FuncDecD (id, tparams, params, typ_ret, clauses, elseclause_opt, hints)
$ no_region
in
let value_spec = defs @ [ def ] |> Interface.SpecTec_AL.boot_spec in
value_spec
let apply_sl (level_meta : Config.level) (value_meta : Value.t)
(value_spec : Value.t) : Value.t =
let rel_meta = level_meta.layer.rel in
let defs = Interface.SpecTec_SL.unboot_script value_spec in
let mixop_rel, inputs_rel =
List.find_map
(fun (def : Sl.def) ->
match def.it with
| RelD (id, (nottyp, inputs), _, _, _, _) when id.it = rel_meta ->
let mixop, _ = Mixfix.split nottyp.it in
Some (mixop, inputs)
| _ -> None)
defs
|> function
| Some (mixop_rel, inputs_rel) -> (mixop_rel, inputs_rel)
| None ->
error no_region
(Format.asprintf "relation %s not found in the spec" rel_meta)
in
check
(List.length inputs_rel = 1)
no_region
(Format.asprintf "relation %s must have exactly one input" rel_meta);
let def =
let id = "main" $ no_region in
let tparams = [] in
let params = [] in
let typ_ret = Il.TextT $ no_region in
let block =
let exp_bind =
Il.VarE ("x" $ no_region) $$ (no_region, Il.VarT ("x" $ no_region, []))
in
let exp_value = value_as_exp value_meta in
let instr_return =
let exp_output = Il.TextE "pass" $$ (no_region, Il.TextT) in
Sl.(ReturnI exp_output $$ (no_region, { iid = 0 }))
in
let instr_call_sl =
let exps_output_sl =
List.init
(Mixop.arity mixop_rel - List.length inputs_rel)
(fun idx ->
Il.VarE ("y_" ^ string_of_int idx $ no_region)
$$ (no_region, Il.VarT ("y_" ^ string_of_int idx $ no_region, [])))
in
let exps = Hints.Input.combine inputs_rel [ exp_bind ] exps_output_sl in
let notexp = Mixfix.fill mixop_rel exps in
Sl.(
RuleI (rel_meta $ no_region, notexp, inputs_rel, [], [ instr_return ])
$$ (no_region, { iid = 0 }))
in
let instr_bind =
Sl.(
LetI (exp_bind, exp_value, [], [ instr_call_sl ])
$$ (no_region, { iid = 0 }))
in
[ instr_bind ]
in
let elseblock_opt = None in
let hints = [] in
Sl.FuncDecD (id, tparams, params, typ_ret, block, elseblock_opt, hints)
$ no_region
in
let value_spec = defs @ [ def ] |> Interface.SpecTec_SL.boot_spec in
value_spec
let apply (level_meta : Config.level) (value_meta : Value.t)
(level_spec : Config.level) (value_spec : Value.t) : Value.t =
match level_spec.interface with
| P4_interface -> assert false
| AL_interface -> apply_il level_meta value_meta value_spec
| SL_interface -> apply_sl level_meta value_meta value_spec
let apply_target (target : Config.target) (level_target : Config.level)
(level_spec : Config.level) : Value.t =
let value_spec = parse_spec level_target.layer level_spec.interface in
let value_target = parse_target target level_target in
apply level_target value_target level_spec value_spec
let apply_interm (level_meta : Config.level) (value_meta : Value.t)
(level_spec : Config.level) : Value.t =
let value_spec = parse_spec level_meta.layer level_spec.interface in
apply level_meta value_meta level_spec value_spec
let apply_tower (tower : Config.tower) : Value.t =
let levels =
(tower.level_boot :: tower.levels_interm) @ [ tower.level_target ]
|> List.rev
in
let level_pairs =
levels
|> List.fold_left
(fun (level_above, level_pairs) level ->
match level_above with
| None -> (Some level, level_pairs)
| Some level_above ->
(Some level, level_pairs @ [ (level_above, level) ]))
(None, [])
|> snd
in
let level_pair_target, level_pairs =
(List.hd level_pairs, List.tl level_pairs)
in
let value_script =
let level_target, level_spec = level_pair_target in
apply_target tower.target level_target level_spec
in
List.fold_left
(fun value_meta level_pair ->
let level_meta, level_spec = level_pair in
apply_interm level_meta value_meta level_spec)
value_script level_pairs