1:- module(frames, [data_frame//3,
2 header_frame//4,
3 priority_frame//4,
4 rst_frame//2,
5 settings_frame//1,
6 settings_ack_frame//0,
7 push_promise_frame//4,
8 ping_frame//2,
9 goaway_frame//3,
10 window_update_frame//2,
11 continuation_frame//3,
12 header_frames//5
13 ]).
19:- use_module(library(apply_macros)). 20:- use_module(library(clpfd)). 21:- use_module(library(record)). 22:- use_module(library(predicate_options)). 23:- use_module(library(delay), [delay/1]). 24:- use_module(library(list_util), [replicate/3]). 25:- use_module(hpack, [hpack/7, hpack_max//5]). 26:- use_module(reif). 27
28/*
29 +-----------------------------------------------+
30 | Length (24) |
31 +---------------+---------------+---------------+
32 | Type (8) | Flags (8) |
33 +-+-------------+---------------+-------------------------------+
34 |R| Stream Identifier (31) |
35 +=+=============================================================+
36 | Frame Payload (0...) ...
37 +---------------------------------------------------------------+
38*/
39frame(Type, Flags, Ident, Payload) -->
40 { delay(length(Payload, Length)),
41 [Type, Flags] ins 0..255,
42 IdentMax #= 2^32 - 1, % high bit is reserved
43 Ident in 0..IdentMax },
44 int24(Length),
45 [Type, Flags],
46 int31(Ident),
47 Payload.
48
49% https://httpwg.org/specs/rfc7540.html#FrameTypes
50% [TODO] need to ensure that each frame is less than
51% SETTINGS_MAX_FRAME_SIZE
52% (default 2^14 octets)
53
54/*
55 +---------------+
56 |Pad Length? (8)|
57 +---------------+-----------------------------------------------+
58 | Data (*) ...
59 +---------------------------------------------------------------+
60 | Padding (*) ...
61 +---------------------------------------------------------------+
62*/
63:- record data_opts(padded=0, end_stream=false).
64:- predicate_options(data_frame//3, 3, [padded(integer),
65 end_stream(boolean)]). 66%! data_frame(?StreamIdent:integer, ?Data:list, ?Options)//
67% DCG for an HTTP/2 data frame
68%
69% @arg Options Options list:
70% * padded(PadLength)
71% If non-zero, the stream will be padded with that many zero bytes.
72% * end_stream(End)
73% If =true=, this frame indicates the end of the stream
74%
75% @bug Technically, I think having a padding of zero is allowed, but
76% currently that isn't representable
77data_frame(StreamIdent, Data, Options) -->
78 int24(Length), [0x0],
79 { make_data_opts(Options, Opts),
80
81 StreamIdent #> 0,
82
83 delay(length(Data, DataLength)),
84 data_opts_padded(Opts, PadLen),
85 zcompare(Comp, PadLen, 0),
86 if_(Comp = (=),
87 (PadFlag = 0x0,
88 Length #= DataLength,
89 PadLenBytes = [], PadBytes = []),
90 (PadFlag = 0x8,
91 PadLenBytes = [PadLen],
92 replicate(PadLen, 0, PadBytes),
93 Length #= PadLen + DataLength + 1)),
94
95 % need to check this after, so on backtracking we can flip this
96 % boolean instead of trying all possible lengths
97 data_opts_end_stream(Opts, StreamEnd),
98 if_(StreamEnd = true, EndFlag #= 0x1,
99 (StreamEnd = false, EndFlag #= 0x0)),
100
101 Flags #= EndFlag \/ PadFlag },
102 [Flags], int31(StreamIdent),
103 PadLenBytes, Data, PadBytes, !.
104
105/*
106 +---------------+
107 |Pad Length? (8)|
108 +-+-------------+-----------------------------------------------+
109 |E| Stream Dependency? (31) |
110 +-+-------------+-----------------------------------------------+
111 | Weight? (8) |
112 +-+-------------+-----------------------------------------------+
113 | Header Block Fragment (*) ...
114 +---------------------------------------------------------------+
115 | Padding (*) ...
116 +---------------------------------------------------------------+
117*/
118:- record header_opts(end_stream=false,
119 end_headers=true,
120 padded=0,
121 priority=false,
122 is_exclusive=false,
123 stream_dependency=0,
124 weight=0).
125:- predicate_options(header_frame//3, 3,
126 [end_stream(boolean),
127 end_headers(boolean),
128 padded(integer),
129 priority(boolean),
130 is_exclusive(boolean),
131 stream_dependency(integer),
132 weight(integer)]).
152header_frame(StreamIdent, Headers, Size-Table0-SizeOut-Table1, Options) -->
153 { 154 155 156 when(nonvar(Headers);ground(Data),
157 phrase(hpack(Headers, Size, SizeOut, Table0, Table1), Data)) },
158 header_frame_raw(StreamIdent, Data, Options).
159
160%! header_frame_raw(?StreamIdent, ?HeaderData, ?Options)//
161% Helper DCG to generate header frames, passing the HPACK'd data through
162header_frame_raw(StreamIdent, Data, Options) -->
163 int24(Length), [0x1],
164 { make_header_opts(Options, Opts),
165 header_opts_padded(Opts, PadLen),
166 header_opts_end_stream(Opts, EndStream),
167 header_opts_priority(Opts, IsPriority),
168 header_opts_end_headers(Opts, EndHeaders),
169 header_opts_is_exclusive(Opts, IsExclusive),
170 header_opts_stream_dependency(Opts, StreamDep),
171 header_opts_weight(Opts, Weight),
172
173 DataLength #>= 0,
174 delay(length(Data, DataLength)),
175 zcompare(Comp, PadLen, 0),
176 if_(Comp = (=),
177 (PadFlag = 0x0,
178 Length_ #= DataLength,
179 PadLenBytes = [], PadBytes = []),
180 (PadFlag = 0x8,
181 PadLenBytes = [PadLen],
182 replicate(PadLen, 0, PadBytes),
183 Length_ #= PadLen + DataLength + 1)),
184
185 if_(EndStream = true, EndStreamFlag #= 0x1,
186 (EndStream = false, EndStreamFlag #= 0)),
187 if_(EndHeaders = true, EndHeadersFlag #= 0x4,
188 (EndHeaders = false, EndHeadersFlag #= 0)),
189 if_(IsPriority = true,
190 (IsPriorityFlag #= 0x20,
191 StreamDep #> 0,
192 if_(IsExclusive = true,
193 (EStreamDep #= StreamDep + 2^31,
194 StreamDep #= EStreamDep mod 2^31),
195 (IsExclusive = false,
196 StreamDep #= EStreamDep)),
197 EStreamDepBytes = int32(EStreamDep),
198 Length #= Length_ + 5,
199 WeightBytes = [Weight]),
200 (IsPriority = false,
201 IsPriorityFlag #= 0x0,
202 Length #= Length_,
203 EStreamDepBytes = [], WeightBytes = [])),
204
205 Flags #= EndStreamFlag \/ EndHeadersFlag \/ IsPriorityFlag \/ PadFlag },
206 [Flags],
207 int31(StreamIdent),
208 PadLenBytes,
209 EStreamDepBytes, WeightBytes,
210 Data, PadBytes, !.
211
212/*
213 +-+-------------------------------------------------------------+
214 |E| Stream Dependency (31) |
215 +-+-------------+-----------------------------------------------+
216 | Weight (8) |
217 +-+-------------+
218*/
219%! priority_frame(?StreamIdent:integer, ?Exclusive:boolean, ?StreamDep:integer, ?Weight:integer)//
220priority_frame(StreamIdent, Exclusive, StreamDep, Weight) -->
221 int24(5), [0x02, 0],
222 { Weight in 0..255,
223 if_(Exclusive = true, ExclusiveFlag #= 0x8000_0000,
224 (Exclusive = false, ExclusiveFlag #= 0)),
225 StreamDep #< 2^31,
226 E_StreamDep #= ExclusiveFlag \/ StreamDep },
227 int31(StreamIdent),
228 int32(E_StreamDep), [Weight].
229
236rst_frame(StreamIdent, ErrCode) -->
237 int24(4), [0x3, 0], int31(StreamIdent), int32(ErrCode).
238
239/*
240 +-------------------------------+
241 | Identifier (16) |
242 +-------------------------------+-------------------------------+
243 | Value (32) |
244 +---------------------------------------------------------------+
245 ...
246*/
247%! settings_frame(?Settings:list)//
248settings_frame(Settings) -->
249 int24(Length),
250 [0x4, 0x0], int32(0),
251 { delay(length(Settings, SettingsLength)),
252 Length #= SettingsLength * 6 },
253 settings_params(Settings).
254
255settings_params([K-V|Settings]) -->
256 { setting_name_num(K, KNum) },
257 int16(KNum), int32(V),
258 settings_params(Settings), !.
259settings_params([]) --> [].
260
261setting_name_num(header_table_size, 0x1).
262setting_name_num(enable_push, 0x2).
263setting_name_num(max_concurrent_streams, 0x3).
264setting_name_num(initial_window_size, 0x4).
265setting_name_num(max_frame_size, 0x5).
266setting_name_num(max_header_list_size, 0x6).
267setting_name_num(N, N).
272settings_ack_frame -->
273 int24(0), [0x4, 0x1], int32(0).
274
275/*
276 +---------------+
277 |Pad Length? (8)|
278 +-+-------------+-----------------------------------------------+
279 |R| Promised Stream ID (31) |
280 +-+-----------------------------+-------------------------------+
281 | Header Block Fragment (*) ...
282 +---------------------------------------------------------------+
283 | Padding (*) ...
284 +---------------------------------------------------------------+
285*/
286:- record push_promise_opts(end_headers=true,
287 padded=0).
288:- predicate_options(push_promise_frame//4, 4,
289 [end_headers(boolean),
290 padded(integer)]). 291%! push_promise_frame(?StreamIdent:integer, ?NewStreamID:integer, ?HeaderInfo, ?Options:list)//
292% DCG for a push-promise frame, which is a frame notifying the
293% receiver about a new stream the sender intends to initiate.
294%
295% @arg HeaderInfo Information to be passed to hpack:hpack/7, in the
296% form =|TableSizeInOut-HeadersList|=
297% @arg Options Options list:
298% * padded(PadLength)
299% If non-zero, the data will be padded by the indicated number of zero bytes
300% * end_headers(End)
301% If true, this frame is the end of the stream
302% @see hpack:hpack/7
303% @bug Technically, I think having a padding of zero is allowed, but
304% currently that isn't representable
305push_promise_frame(StreamIdent, NewStreamIdent, (SizeIn-Tbl0-SizeOut-Tbl1)-Headers, Options) -->
306 int24(Length), [0x5],
307 { make_push_promise_opts(Options, Opts),
308 push_promise_opts_padded(Opts, PadLen),
309 push_promise_opts_end_headers(Opts, EndHeaders),
310
311 R_NewStreamIdent #= NewStreamIdent mod 2^32,
312 NewStreamIdent #= R_NewStreamIdent mod 2^32,
313
314 % As noted in header_frame//4, it would be nice if we could do
315 % this in a better way...
316 when(nonvar(Headers);ground(Data),
317 phrase(hpack(Headers, SizeIn, SizeOut, Tbl0, Tbl1), Data)),
318
319 delay(length(Data, DataLength)),
320 zcompare(Comp, PadLen, 0),
321 if_(Comp = (=),
322 (PadFlag #= 0,
323 Length #= 4 + DataLength,
324 PadLenBytes = [], PadBytes = []),
325 (PadFlag #= 0x8,
326 Length #= 4 + DataLength + PadLen + 1,
327 PadLenBytes = [PadLen],
328 replicate(PadLen, 0, PadBytes))),
329
330 if_(EndHeaders = true, EndFlag #= 0x4,
331 (EndHeaders = false, EndFlag #= 0x0)),
332
333 Flags #= EndFlag \/ PadFlag },
334 [Flags],
335 int31(StreamIdent),
336 PadLenBytes, int32(R_NewStreamIdent), Data, PadBytes, !.
337
338/*
339 +---------------------------------------------------------------+
340 | |
341 | Opaque Data (64) |
342 | |
343 +---------------------------------------------------------------+
344*/
345%! ping_frame(?Data:list, ?Ack:boolean)//
346ping_frame(Data, Ack) -->
347 { if_(Ack = true, Flags #= 0x1,
348 (Ack = false, Flags #= 0x0)),
349 length(Data, 8) },
350 frame(0x6, Flags, 0x0, Data), !.
351
352/*
353 +-+-------------------------------------------------------------+
354 |R| Last-Stream-ID (31) |
355 +-+-------------------------------------------------------------+
356 | Error Code (32) |
357 +---------------------------------------------------------------+
358 | Additional Debug Data (*) |
359 +---------------------------------------------------------------+
360*/
361%! goaway_frame(?LastStreamId, ?ErrorCode, ?Data)//
362goaway_frame(LastStreamId, Error, Data) -->
363 int24(Length), [0x7, 0], int32(0),
364 { delay(length(Data, DataLength)),
365 Length #= DataLength + 4 + 4 },
366 int31(LastStreamId), int32(Error),
367 Data.
368
375window_update_frame(StreamIdent, Increment) -->
376 int24(4), [0x8, 0],
377 int31(StreamIdent),
378 int31(Increment).
379
388continuation_frame(StreamIdent, (Size-Tbl0-SizeOut-Tbl1)-Headers, End) -->
389 { when(nonvar(Headers);ground(Data),
390 phrase(hpack(Headers, Size, SizeOut, Tbl0, Tbl1), Data)) },
391 continuation_frame_raw(StreamIdent, Data, End), !.
392
393continuation_frame_raw(StreamIdent, Data, End) -->
394 int24(Length), [0x9],
395 { delay(length(Data, Length)),
396 if_(End = true, Flags #= 0x4,
397 (End = false, Flags #= 0x0)) },
398 [Flags], int31(StreamIdent),
399 Data.
400
(MaxSize, StreamIdent, Headers, TableSize0-Table0-TableSize2-Table2, Options) -->
403 { phrase(hpack_max(MaxSize, Headers, TableSize0-Table0-TableSize1-Table1, Leftover, 0), Data),
404 (Leftover = []
405 -> End = true
406 ; End = false) },
407 header_frame_raw(StreamIdent, Data, [end_headers(End)|Options]),
408 continue_frames(MaxSize, StreamIdent, Leftover, TableSize1-Table1-TableSize2-Table2).
409
410continue_frames(_, _, [], TableSize-Table-TableSize-Table) --> !.
411continue_frames(MaxSize, StreamIdent, Headers, TableSize0-Table0-TableSize2-Table2) -->
412 { phrase(hpack_max(MaxSize, Headers, TableSize0-Table0-TableSize1-Table1, Leftover, 0), Data),
413 (Leftover = []
414 -> End = true
415 ; End = false) },
416 continuation_frame_raw(StreamIdent, Data, End),
417 continue_frames(MaxSize, StreamIdent, Leftover, TableSize1-Table1-TableSize2-Table2).
418
419
420% Helper predicates
421
422int16(I) -->
423 { [A, B] ins 0..255,
424 I #= A * (2^8) + B },
425 [A, B].
426
427int24(I) -->
428 { [A, B, C] ins 0..255,
429 I #= A * (2^16) + B * (2^8) + C },
430 [A, B, C].
431
432int31(I) -->
433 { [A, B, C, D] ins 0..255,
434 A_ in 0..127,
435 A_ #= A mod 128,
436 I in 0..0x7fff_ffff,
437 I #= A_ * (2^24) + B * (2^16) + C * (2^8) + D,
438 % Annoying thing with StreamIdent: we want to ignore the high
439 % bit when receiving, but set it to zero when sending
440 (ground(I) -> A #= A_ ; true) },
441 [A, B, C, D].
442
443int32(I) -->
444 { [A, B, C, D]
DCGs for parsing HTTP/2 frames