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                  ]).

DCGs for parsing HTTP/2 frames

author
- James Cash */
   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)]).
 data_frame(?StreamIdent:integer, ?Data:list, ?Options)//
DCG for an HTTP/2 data frame
Arguments:
Options- Options list:
padded(PadLength)
If non-zero, the stream will be padded with that many zero bytes.
end_stream(End)
If true, this frame indicates the end of the stream
bug
- Technically, I think having a padding of zero is allowed, but 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)]).
 header_frame(?StreamIdent:integer, ?Headers:list, ?TableSizeInOut, ?Options)//
DCG for an HTTP/2 header frame.
Arguments:
TableSizeInOut- Header table configuration information that is passed to the hpack/7 DCG.
Options- Allowed options:
padded(PadLength)
If non-zero, the stream will be padded with that many zero bytes.
end_stream(EndStream)
If true, this frame indicates the end of the stream
end_headers(End)
If true, this frame indicates the end of the headers
priority(Priority)
If true, this frame has priority set.
See also
- hpack/7
bug
- Technically, I think having a padding of zero is allowed, but currently that isn't representable
To be done
- Support for stream-priority flag
  152header_frame(StreamIdent, Headers, Size-Table0-SizeOut-Table1, Options) -->
  153    { % dumb that we have to call phrase/2 inside a DCG, but we need
  154      % to know the length of the output & I'm not sure how else to do
  155      % this
  156      when(nonvar(Headers);ground(Data),
  157           phrase(hpack(Headers, Size, SizeOut, Table0, Table1), Data)) },
  158    header_frame_raw(StreamIdent, Data, Options).
 header_frame_raw(?StreamIdent, ?HeaderData, ?Options)//
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*/
 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
  230/*
  231 +---------------------------------------------------------------+
  232 |                        Error Code (32)                        |
  233 +---------------------------------------------------------------+
  234*/
 rst_frame(?StreamIdent:integer, ?ErrorCode:integer)//
  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*/
 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).
 settings_ack_frame//
Special case of settings_frame//1 to acknowledge the reciept of headers.
  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)]).
 push_promise_frame(?StreamIdent:integer, ?NewStreamID:integer, ?HeaderInfo, ?Options:list)//
DCG for a push-promise frame, which is a frame notifying the receiver about a new stream the sender intends to initiate.
Arguments:
HeaderInfo- Information to be passed to hpack/7, in the form TableSizeInOut-HeadersList
Options- Options list:
padded(PadLength)
If non-zero, the data will be padded by the indicated number of zero bytes
end_headers(End)
If true, this frame is the end of the stream
See also
- hpack/7
bug
- Technically, I think having a padding of zero is allowed, but 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*/
 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*/
 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
  369/*
  370 +-+-------------------------------------------------------------+
  371 |R|              Window Size Increment (31)                     |
  372 +-+-------------------------------------------------------------+
  373*/
 window_update_frame(?StreamIdent, ?Increment)//
  375window_update_frame(StreamIdent, Increment) -->
  376    int24(4),  [0x8, 0],
  377    int31(StreamIdent),
  378    int31(Increment).
  379
  380/*
  381 +---------------------------------------------------------------+
  382 |                   Header Block Fragment (*)                 ...
  383 +---------------------------------------------------------------+
  384*/
 continuation_frame(?StreamIdent:integer, ?HeaderInfo, ?End:boolean)//
Arguments:
HeaderInfo- Information to be passed to hpack/7 HeaderInfo = HeaderTableSize-TableIn-TableOut-HeaderList
  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
  401% only going to work in the serializing mode
  402header_frames(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] ins 0..255,
  445      I #= A * (2^24) + B * (2^16) + C * (2^8) + D },
  446    [A, B, C, D]