0 | module Http2

  2 | import Debug.Trace

  3 | import Data.Either

  4 | import Data.SortedMap

  5 | import Data.Vect

  6 | import Data.List

  7 | import Data.Bits

  8 | import Data.Vect as Vect

  9 | import Data.Buffer.Indexed

 10 | import Data.Buffer -- for stringByteLength

 12 | import Control.Monad.Identity

 13 | import Control.Monad.Reader.Interface

 14 | import Control.Monad.State.State

 15 | import Control.Monad.State.Interface

 16 | import Control.Monad.Trans

 17 | import Control.Monad.Error.Either

 18 | import Control.Monad.RWS.CPS

 20 | import Cont

 21 | import BufConn

 22 | import PGTypes -- for PgRows

 23 | import UTF8

 25 | import Http2Responder

 26 | import Huffman.Decode as HD

 28 | import BitsUtil

 30 | Responder: Type

 31 | Responder = Request -> InnerCont (List Frame)

 33 | log : Monad m => String -> m ()

 34 | log = flip trace $ pure ()

 36 | modifyMap : {a: Type} -> {b: Type} -> a -> (b -> b) -> SortedMap a b -> SortedMap a b

 37 | modifyMap key fun map =

 38 |   let

 39 |     mbFound = lookup key map

 40 |   in

 41 |     case mbFound of

 42 |       Just found =>

 43 |         insert key (fun found) map

 44 |       Nothing => map

 47 | isPath : Header -> Maybe String

 48 | isPath PathSlash = Just "/"

 49 | isPath (Literal 4 path) = Just path

 50 | isPath (Literal 5 _) = Just "/index.html"

 51 | isPath _ = Nothing

 53 | data H2Err

 54 |   = InvalidHeaderBlock

 55 |   | CompressionError HpackErr

 56 |   | IndexOutOfBounds

 57 |   | UnimplementedStaticHeader Bits8

 58 |   | UnimplementedDynamicIndex

 59 |   | LiteralHeaderValueTooLong

 60 |   | UnimplementedHeaderToEncode

 62 | Show H2Err where

 63 |   show InvalidHeaderBlock = "InvalidHeaderBlock"

 64 |   show (CompressionError hpackErr) = "CompressionError(" ++ show hpackErr ++ ")"

 65 |   show IndexOutOfBounds = "IndexOutOfBounds"

 66 |   show (UnimplementedStaticHeader byte) = "UnimplementedStaticHeader(" ++ show byte ++ ")"

 67 |   show UnimplementedDynamicIndex = "UnimplementedDynamicIndex"

 68 |   show LiteralHeaderValueTooLong = "LiteralHeaderValueTooLong"

 69 |   show UnimplementedHeaderToEncode = "UnimplementedHeaderToEncode"

 71 | FrameBufConSt : Type

 72 | FrameBufConSt = BufConSt (List Frame)

 74 | bits8ToNat : Bits8 -> Fin 32 -> Nat

 75 | bits8ToNat amt shft =

 76 |   let int : Bits32

 77 |       int = cast amt

 78 |       shifted : Bits32

 79 |       shifted = int `shiftL` shft

 80 |    in fromInteger $ cast shifted

 82 | public export

 83 | END_STREAM, END_HEADERS, PRIORITY, PADDED : Bits8

 84 | END_STREAM = 0x1

 85 | END_HEADERS = 0x4

 86 | PRIORITY = 0x20

 87 | PADDED = 0x08

 89 | SETTINGS_HEADER_TABLE_SIZE : Vect 2 Bits8

 90 | SETTINGS_HEADER_TABLE_SIZE = [0, 0x1]

 92 | SETTINGS_ENABLE_PUSH : Vect 2 Bits8

 93 | SETTINGS_ENABLE_PUSH = [0, 0x2]

 95 | SETTINGS_INITIAL_WINDOW_SIZE : Vect 2 Bits8

 96 | SETTINGS_INITIAL_WINDOW_SIZE = [0, 0x4]

 98 | SETTINGS_MAX_FRAME_SIZE : Vect 2 Bits8

 99 | SETTINGS_MAX_FRAME_SIZE = [0, 0x5]

101 | is : Bits8 -> Flags -> Bool

102 | is filter (MkFlags f) = f .&. filter /= 0

104 | staticTable : Bits8 -> Either Bits8 Header

105 | staticTable =

106 |   \case

107 |   2 => Right MethodGet

108 |   3 => Right MethodPost

109 |   4 => Right PathSlash

110 |   6 => Right SchemeHttp

111 |   -- the schema is really useless:

112 |   -- https://github.com/haproxy/haproxy/issues/77

113 |   7 => Right SchemeHttps

114 |   28 => Right ContentLength

115 |   48 => Right ProxyAuthenticate

116 |   58 => Right UserAgent

117 |   -- TODO

118 |   -- These previous headers are just the ones seen in h2spec. Really they should all be added

119 |   x => Left x

121 | lengthOfStaticTable : Nat

122 | lengthOfStaticTable = 61

124 | encodeHpack : List Header -> Either H2Err (List Bits8)

125 | encodeHpack [] = Right []

126 | encodeHpack (head :: rest) = do

127 |   first <-

128 |     case head of

129 |       StatusOk => Right

130 |                   [ 0x80  -- high bit set means that it is index according to section 6.1.

131 |                     .|. 8 -- 8 is the index in Appendix A of rfc 7541 (hpack)

132 |                   ]

133 |       Literal index val =>

134 |         case (index > cast lengthOfStaticTable, length val > 0x7f) of

135 |           (True, _) => Left UnimplementedDynamicIndex

136 |           (_, True) => Left LiteralHeaderValueTooLong

137 |           _ =>

138 |             -- because the upper bit (the bit in 0x80) is not set,

139 |             -- it is not huffman encoded per section 5.2

140 |             Right $ [ 0x40 .|. index, cast (length val)] <+> toList (utf8Encode val)

141 |       _ => Left UnimplementedHeaderToEncode

142 |   (first <+>) <$> encodeHpack rest

144 | toStr : List Bits8 -> String

145 | toStr = pack . map cast

147 | fromStr : String -> List Bits8

148 | fromStr = map cast . unpack

150 | DynamicTable : Type

151 | DynamicTable = List Header

153 | record ContinuationState where

154 |   constructor MkContinuationState

155 |   currentStreamIdent : Bits32

156 |   accumulated : List Bits8

158 | Show ContinuationState where

159 |   show (MkContinuationState streamIdent accumulated) = "ContinuationState " ++ show streamIdent ++ " " ++ show accumulated

162 | data CAllow = Require | Forbidden

164 | Eq CAllow where

165 |   Require == Require = True

166 |   Forbidden == Forbidden = True

167 |   _ == _ = False

169 | data NonClosedStreamState = Idle | Open (List Bits8) (List Header)

171 | Show NonClosedStreamState where

172 |   show Idle = "Idle"

173 |   show (Open _ _) = "Open"

180 | data StreamStatus = Closed | NonClosed NonClosedStreamState

182 | Show StreamStatus where

183 |   show Closed = "Closed"

184 |   show (NonClosed inner) = "NonClosed " ++ show inner

191 | record StreamState where

192 |   constructor MkStreamState

193 |   continuationState : Maybe ContinuationState

194 |   cont : CAllow

195 |   status : StreamStatus

196 |   windowSize : Bits32

198 | record HpackState where

199 |   constructor MkHpackState

200 |   hpackDynTable : List Header

201 |   limit : Bits32

203 | record ConnState where

204 |   constructor MkConnState

205 |   connHpackState : HpackState

206 |   streams : SortedMap Bits32 StreamState

207 |   minNextStreamIdent : Bits32

208 |   initialWindowSize : Bits32

209 |   maxFrameSize : Bits32

212 | H2BufConn : Type -> Type

213 | H2BufConn a = DBufferedConn Void (List Frame) a PgRows PgInput

215 | initialConnState : ConnState

216 | initialConnState =

217 |   MkConnState

218 |     { connHpackState = MkHpackState [] 4096

219 |     , streams = empty

220 |     , minNextStreamIdent = 0

221 |     -- initial values specced in http2 sec 11.3

222 |     , initialWindowSize = 65535

223 |     , maxFrameSize = 16384

224 |     }

226 | data ErrorCode

227 |   = ProtocolErrorCode

228 |   | InternalErrorCode

229 |   | FlowControlErrorCode

230 |   | StreamClosedErrorCode

231 |   | FrameSizeErrorCode

232 |   | CompressionErrorCode

234 | Show ErrorCode where

235 |   show ProtocolErrorCode = "ProtocolError"

236 |   show InternalErrorCode = "InternalErrorCode"

237 |   show FlowControlErrorCode = "FlowControlError"

238 |   show StreamClosedErrorCode = "StreamClosedError"

239 |   show FrameSizeErrorCode = "FrameSizeError"

240 |   show CompressionErrorCode = "CompressionError"

242 | errorCodeToByte: ErrorCode -> Bits8

243 | errorCodeToByte ProtocolErrorCode     = 1

244 | errorCodeToByte InternalErrorCode     = 2

245 | errorCodeToByte FlowControlErrorCode  = 3

246 | errorCodeToByte StreamClosedErrorCode = 5

247 | errorCodeToByte FrameSizeErrorCode    = 6

248 | errorCodeToByte CompressionErrorCode  = 9

250 | getStreamState : MonadState ConnState m => Bits32 -> EitherT ErrorCode m StreamState

251 | getStreamState streamIdent = do

252 |   st <- lift get

253 |   case lookup streamIdent st.streams of

254 |     Just x => pure x

255 |     Nothing =>

256 |       if streamIdent /= 0 && streamIdent < st.minNextStreamIdent

257 |         then do

258 |           log $ "STREAM IDENT: expected at least " ++ show st.minNextStreamIdent ++ " but only got " ++ show streamIdent

259 |           throwE ProtocolErrorCode

260 |         else do

261 |           when (streamIdent /= 0) $

262 |             lift $ modify { minNextStreamIdent := streamIdent + 1 }

263 |           pure $ MkStreamState Nothing Forbidden (NonClosed Idle) st.initialWindowSize

265 | putStreamState : MonadState ConnState m => Bits32 -> StreamState -> m Unit

266 | putStreamState streamIdent newStreamState =

267 |   modify (\connState => ({ streams $= insert streamIdent newStreamState } connState))

269 | modifyStreamState : MonadState ConnState m => Bits32 -> (StreamState -> StreamState) -> m Unit

270 | modifyStreamState streamIdent f =

271 |   modify (\connState => ({ streams $= modifyMap streamIdent f } connState))

273 | data StaticOrDynamic = Static | Dynamic

275 | checkIndexOutOfBounds : Bits8 -> EitherT H2Err (State HpackState) StaticOrDynamic

276 | checkIndexOutOfBounds index = do

277 |   when (index == 0) $ do

278 |     log "Index is zero"

279 |     throwE IndexOutOfBounds

280 |   st <- lift get

281 |   let dynTable = st.hpackDynTable

282 |   let indexNat = bits8ToNat index 0

283 |       highestAllowed = lengthOfStaticTable + length dynTable

284 |   when (indexNat > highestAllowed) $ do

285 |     log $ "IndexNat " ++ show indexNat ++ " larger than lengthOfStaticTable + length dynTable " ++ show (length dynTable)

286 |     throwE IndexOutOfBounds

287 |   if indexNat > lengthOfStaticTable

288 |     -- HPACK section 2.3.3

289 |     -- "Indices strictly greater than the length of the static table"

290 |     then pure Dynamic

291 |     else pure Static

293 | shiftN16 : Fin 16 -> Bits16

294 | shiftN16 =

295 |     \case

296 |     0 => shiftL 1 0

297 |     1 => shiftL 1 1

298 |     2 => shiftL 1 2

299 |     3 => shiftL 1 3

300 |     4 => shiftL 1 4

301 |     5 => shiftL 1 5

302 |     6 => shiftL 1 6

303 |     7 => shiftL 1 7

304 |     8 => shiftL 1 8

305 |     9 => shiftL 1 9

306 |     10 => shiftL 1 10

307 |     11 => shiftL 1 11

308 |     12 => shiftL 1 12

309 |     13 => shiftL 1 13

310 |     14 => shiftL 1 14

311 |     15 => shiftL 1 15

315 | go : Nat -> Bits16 -> List Bits8 -> Either H2Err (Bits16, List Bits8)

316 | go _ _ [] = Left InvalidHeaderBlock

317 | go m i (b :: tail) =

318 |     case (,) <$> natToFin m 16 <*> natToFin (m + 7) 16 of

319 |       Just (fin16, fin16P7) => do

320 |         let newI = i + (cast b .&. 127) * shiftN16 fin16

321 |         if b .&. 128 == 128

322 |           then go (cast fin16P7) newI tail

323 |           else Right (newI, tail)

324 |       Nothing =>

325 |         Left InvalidHeaderBlock

327 | shiftN : Fin 9 -> Bits16

328 | shiftN =

329 |     \case

330 |     0 => shiftL 1 0

331 |     1 => shiftL 1 1

332 |     2 => shiftL 1 2

333 |     3 => shiftL 1 3

334 |     4 => shiftL 1 4

335 |     5 => shiftL 1 5

336 |     6 => shiftL 1 6

337 |     7 => shiftL 1 7

338 |     8 => shiftL 1 8

352 | decodeInteger : Fin 9 -> Bits8 -> List Bits8 -> Either H2Err (Bits16, List Bits8)

353 | decodeInteger n unmaskedPrefix rest = do -- see HPACK sec 5.1 for the meaning of n

354 |   let pow = shiftN n - 1

355 |       prefiks = cast unmaskedPrefix .&. pow

356 |   if prefiks < pow

357 |     then Right (prefiks, rest)

358 |     else go 0 prefiks rest

360 | setLimit : Bits32 -> HpackState -> HpackState

361 | setLimit newLimit = { limit := newLimit }

364 |   decodeIndexed : List Bits8 -> EitherT H2Err (State HpackState) (List Header)

365 |   decodeIndexed [] = pure []

366 |   decodeIndexed (bite :: rest) = do

367 |     -- indexed header field

368 |     let

369 |       -- the top bit is the one that says it is indexed.

370 |       -- so we don't need it anymore.

371 |       removedUpper = bite .&. 0x7f

372 |     staticOrDynamic <- checkIndexOutOfBounds removedUpper

373 |     newHeader <-

374 |       case staticOrDynamic of

375 |         Static =>

376 |           bimapEitherT UnimplementedStaticHeader id $

377 |             MkEitherT . pure $

378 |               staticTable removedUpper

379 |         Dynamic => do

380 |           st <- lift get

381 |           let dynTable = st.hpackDynTable

382 |           let dynIndex = removedUpper - cast lengthOfStaticTable - 1

383 |               idx = bits8ToNat dynIndex 0

384 |           case natToFin idx (length dynTable) of

385 |             Nothing => do

386 |               log "RemovedUpper \{show removedUpper} - \{show lengthOfStaticTable} is out of bounds in dynTable with length \{show $ length dynTable}"

387 |               throwE IndexOutOfBounds

388 |             Just finIdx => do

389 |               let header = index' dynTable finIdx

390 |               pure header

391 |     (newHeader ::) <$> decodeHpack rest

393 |   maybeDecodeH : Bits8 -> List Bits8 -> Either H2Err (Pair (List Bits8) (List Bits8))

394 |   maybeDecodeH lenWithH bites =

395 |     let len = lenWithH .&. 0x7f

396 |         (head, tail) = splitAt (bits8ToNat len 0) bites

397 |     in

398 |     if lenWithH .&. 0x80 /= 0

399 |       then do

400 |         dec <-

401 |           case HD.decodeHuffman head of

402 |             Left err  => Left $ CompressionError err

403 |             Right dec => Right dec

404 |         pure (dec, tail)

405 |       else

406 |         pure (head, tail)

408 |   decodeLiteral : Bits8 -> Bool -> List Bits8 -> EitherT H2Err (State HpackState) (List Header)

409 |   decodeLiteral mask saveInTable (bite :: lenWithH :: rest) = do

410 |     -- literal header field with incremental indexing

411 |     let index = mask .&. bite

412 |     (newLiteral, newRest) <-

413 |       if index == 0

414 |       then do

415 |         -- 'new name'. specced in second table of HPACK sec 6.2.1

416 |         (nameString, restWithoutName) <- MkEitherT . pure $ maybeDecodeH lenWithH rest

417 |         case restWithoutName of

418 |           [] => throwE InvalidHeaderBlock

419 |           valueLen :: valueRest => do

420 |             (valueString, restWithoutNameAndValue) <-

421 |               MkEitherT . pure $ maybeDecodeH valueLen valueRest

422 |             pure (LiteralStr (toStr nameString) (toStr valueString), restWithoutNameAndValue)

423 |       else do

424 |         _ <- checkIndexOutOfBounds index

425 |         (dec, tail) <- MkEitherT $ pure $ maybeDecodeH lenWithH rest

426 |         let decStr = toStr dec

427 |         pure (Literal index decStr, tail)

428 |     when saveInTable $

429 |       lift $ modify { hpackDynTable $= (newLiteral ::) }

430 |     (newLiteral ::) <$> decodeHpack newRest

431 |   decodeLiteral _ _ _ = throwE InvalidHeaderBlock

433 |   decodeHpack : List Bits8 -> EitherT H2Err (State HpackState) (List Header)

434 |   decodeHpack [] = pure []

435 |   decodeHpack whole@(bite :: rest) =

436 |     case ( bite .&. 0x80 /= 0 -- HPACK section 6.1

437 |          , bite .&. 0x40 /= 0 -- HPACK section 6.2.1

438 |          , bite .&. 0x20 /= 0

439 |          , bite .&. 0x10 /= 0 ) of

440 |       (True, _, _, _) => decodeIndexed whole -- mask 0x7f is inside the function

441 |       (_, True, _, _) =>              decodeLiteral 0x3f True  whole -- section 6.2.1 incremental indexing

442 |       (False, False, False, False) => decodeLiteral 0x0f False whole -- section 6.2.2 w/o indexing

443 |       (False, False, False, True) =>  decodeLiteral 0x0f False whole -- section 6.2.3 we don't implement forwarding, so this is treated the same

444 |       (False, False, True, _) => do

445 |         (newDynTableSize, newRest) <- MkEitherT . pure $ decodeInteger 5 bite rest

446 |         let

447 |           toWide : Bits16 -> Bits32

448 |           toWide = cast

449 |         hpackState <- lift get

450 |         -- hpack sec 6.3

451 |         -- "The new maximum size MUST be lower than or equal to the limit determined by the protocol using HPACK."

452 |         when (toWide newDynTableSize > hpackState.limit) $

453 |           throwE InvalidHeaderBlock

454 |         lift $ modify {limit := toWide newDynTableSize}

455 |         when (cast newDynTableSize < length hpackState.hpackDynTable) $ do

456 |           let (first, _) = splitAt (cast newDynTableSize) hpackState.hpackDynTable

457 |           lift $ modify { hpackDynTable := first }

458 |         decodeHpack newRest

459 |       _ => throwE InvalidHeaderBlock

461 | encodeFrame : Frame -> List Bits8

462 | encodeFrame f =

463 |   let

464 |     MkPayload p := f.payload

465 |     len32 : Bits32

466 |     len32 = cast (length p)

467 |     l2, l1, l0 : Bits8

468 |     l2 = cast (len32 `shiftR` 16)

469 |     l1 = cast (len32 `shiftR` 8)

470 |     l0 = cast len32

471 |     MkFlags flagByte := f.flags

472 |   in

473 |     [l2, l1, l0, encodeFrameType f.frameType, flagByte]

474 |       ++ toList (bits32ToBigEndian f.streamIdent)

475 |       ++ p

478 | headerFramesForHTML : Bits32 -> List Frame

479 | headerFramesForHTML streamIdent =

480 |   let

481 |   payloadEncoded = fromJust $ getRight (encodeHpack [StatusOk, Literal 31 "text/html; charset=utf-8"])

482 |   payload = MkPayload payloadEncoded

483 |   in

484 |   [MkFrame Headers (MkFlags END_HEADERS) streamIdent payload]

486 | HandlerResult : Type -> Type

487 | HandlerResult a = EitherT ErrorCode (RWST Responder () ConnState (Cont (DIterator (List Bits8) (List Bits8) PgRows PgInput Void))) a

489 | errReply : ErrorCode -> Bits32 -> List Frame

490 | errReply errorCode streamIdent =

491 |   let

492 |     body =

493 |       MkPayload $

494 |         -- next four bytes is 'last stream id' (part of GOAWAY frame)

495 |         toList (bits32ToBigEndian streamIdent) ++

496 |         [ 0, 0, 0, errorCodeToByte errorCode

497 |         ]

498 |   in

499 |   [MkFrame GoAway (MkFlags 0) 0 body]

501 | appendAccumulated : MonadState ConnState m => Bits32 -> List Bits8 -> EitherT ErrorCode m Unit

502 | appendAccumulated streamIdent newBytes = do

503 |   st <- getStreamState streamIdent

505 |   newContinuationState <-

506 |     case st.continuationState of

507 |       Nothing => pure $ Just $ MkContinuationState streamIdent newBytes

508 |       Just (MkContinuationState currentStreamIdent currentBytes) =>

509 |         if currentStreamIdent == streamIdent

510 |           then pure $ Just $ MkContinuationState streamIdent (currentBytes ++ newBytes)

511 |           else throwE ProtocolErrorCode

513 |   lift $ putStreamState streamIdent ({ continuationState := newContinuationState } st)

515 | dataParser: NonClosedStreamState -> Bits32 -> Payload -> Flags -> HandlerResult (Maybe (List Frame))

516 | dataParser Idle _ _ _ = do

517 |   log "Need header but got data frame. Protocol error"

518 |   throwE ProtocolErrorCode

519 | dataParser (Open x headers) streamIdent (MkPayload p) fl@(MkFlags f) = do

520 |   dataFromThisFrame <-

521 |     if f .&. 0x8 /= 0

522 |       then

523 |         case p of

524 |           [] =>

525 |             throwE ProtocolErrorCode

526 |           paddingLength :: rest => do

527 |             let

528 |               le : Nat

529 |               le = minus (length rest) (cast paddingLength) -- 0 on underflow

530 |             case le of

531 |               Z => throwE ProtocolErrorCode

532 |               _ => pure $ take le rest

533 |       else

534 |         pure p

535 |   if is END_STREAM fl

536 |     then do

537 |       log "Received all of the request body"

538 |       let all = x <+> dataFromThisFrame

539 |       resp <- ask

540 |       path::_ <- pure $ mapMaybe isPath headers

541 |         | [] => pure Nothing

542 |       reply <- lift $ lift $ resp $ MkRequest streamIdent path all headers

543 |       pure $ Just reply

544 |     else do

545 |       log "Appending to request body"

546 |       lift $ modifyStreamState streamIdent { status := NonClosed $ Open (x <+> dataFromThisFrame) headers }

547 |       pure Nothing

550 | errorsAsCompressionErrors : MonadState ConnState m => EitherT H2Err (State HpackState) a -> EitherT ErrorCode m a

551 | errorsAsCompressionErrors act = do

552 |   let stateComputation = runEitherT act

553 |   st <- lift get

554 |   let (newSt, res) = runState st.connHpackState stateComputation

555 |   lift $ modify { connHpackState := newSt }

556 |   case res of

557 |     Left err => do

558 |       log $ "errorsAsCompressionErrors: throwing CompressionErrorCode but discarding error " <+> show err

559 |       throwE CompressionErrorCode

560 |     Right suc => pure suc

562 | goSettings : MonadState ConnState m => List Bits8 -> EitherT ErrorCode m Unit

563 | goSettings (id1 :: id0 :: v3 :: v2 :: v1 :: v0 :: rest) = do

564 |   -- specced in http2 sec 6.5.2

565 |   let value = bits32FromBigEndian [v3,v2,v1,v0]

566 |   when ([id1, id0] == SETTINGS_INITIAL_WINDOW_SIZE) $ do

567 |     log $ "SETTING INITIAL WINDOW SIZE " ++ show value

568 |     when (value >= (1 `shiftL` 31)) $

569 |       throwE FlowControlErrorCode

570 |     lift $ modify {initialWindowSize := value}

571 |   when ([id1, id0] == SETTINGS_HEADER_TABLE_SIZE) $ do

572 |     log $ "SETTING HEADER_TABLE_SIZE " ++ show value

573 |     lift $ modify {connHpackState $= setLimit value}

574 |   when ([id1, id0] == SETTINGS_ENABLE_PUSH) $ do

575 |     when (value /= 0 && value /= 1) $

576 |       throwE ProtocolErrorCode

577 |     -- we don't do push anyway, so it doesn't matter if they disable it or not

578 |   when ([id1, id0] == SETTINGS_MAX_FRAME_SIZE) $ do

579 |     log $ "SETTING MAX_FRAME_SIZE " ++ show value

580 |     when (value < 16384 || value > 16777215) $

581 |       throwE ProtocolErrorCode

582 |     lift $ modify {maxFrameSize := value}

583 |   goSettings rest

584 | goSettings [] = pure ()

585 | goSettings _ = throwE ProtocolErrorCode

587 | settingsParser: MonadState ConnState m => Bits32 -> Payload -> Flags -> EitherT ErrorCode m (Maybe (List Frame))

588 | settingsParser streamIdent _ (MkFlags 1) =

589 |   pure Nothing

590 | settingsParser streamIdent (MkPayload payload) fl@(MkFlags 0) = do

591 |   -- just ack if they are not ack'ing

592 |   goSettings payload

593 |   pure $ Just [MkFrame Settings (MkFlags 1) 0 (MkPayload [])]

594 | settingsParser _ (MkPayload payload) (MkFlags flags) = do

595 |   log "Invalid settings"

596 |   log $ show (payload, flags)

597 |   throwE ProtocolErrorCode

599 | headersParser : NonClosedStreamState -> Bits32 -> Payload -> Flags -> StreamState -> HandlerResult (Maybe (List Frame))

600 | headersParser streamState streamIdent (MkPayload possiblyWithPriorityFields) fl@(MkFlags f) st = do

601 |   when (is PADDED fl) $

602 |     -- Not implemented yet

603 |     throwE InternalErrorCode

604 |   let p = if is PRIORITY fl

605 |             then drop 5 possiblyWithPriorityFields

606 |             else possiblyWithPriorityFields

607 |   case streamState of

608 |     Open _ _ => do

609 |       -- used for trailer headers

610 |       case is END_STREAM fl of

611 |         True => do

612 |           lift $ modifyStreamState streamIdent { status := Closed }

613 |           resp <- ask

614 |           reply <- lift $ lift $ resp $ MkRequest streamIdent "/" [] []

615 |           pure $ Just reply

616 |         False =>

617 |           case is END_HEADERS fl of

618 |             True =>

619 |               throwE ProtocolErrorCode

620 |             False => do

621 |               -- TODO test this. trailer header with continuation

622 |               lift $ putStreamState streamIdent ({ cont := Require } st)

623 |               () <- appendAccumulated streamIdent p

624 |               pure Nothing

625 |     Idle => do

626 |       connState <- lift get

627 |       when (streamIdent == 0) $

628 |         -- per http2/6.2/3 can't be zero

629 |         throwE ProtocolErrorCode

630 |       when (any (\streamState => case streamState.status of { NonClosed Idle => True; _ => False }) $ values connState.streams) $

631 |         -- per http2/6.2/2 there can't be two headers in progress at the same time

632 |         throwE ProtocolErrorCode

633 |       let

634 |         newContAllow =

635 |           if not (is END_HEADERS fl)

636 |             then Require

637 |             else st.cont

638 |       lift $ putStreamState streamIdent ({ cont := newContAllow } st)

639 |       case (is END_STREAM fl, is END_HEADERS fl) of

640 |         (True, True) => do

641 |           headers <- errorsAsCompressionErrors (decodeHpack p)

642 |           lift $ modifyStreamState streamIdent {continuationState := Nothing, cont := Forbidden, status := Closed }

643 |           let paths = mapMaybe isPath headers

644 |           -- what is the '2' in Literal 2 from h2spec/generic/4/2? verify that it is ':method'

645 |           case (paths, elem MethodGet headers, elem (Literal 2 "HEAD") headers) of

646 |             (path :: _, True, False) => do

647 |               log $ show paths <+> ": GET in HEADERS with END_STREAM and END_HEADERS, sending OK reply"

648 |               resp <- ask

649 |               lift . lift $ Just <$> resp (MkRequest streamIdent path [] headers)

650 |             (path :: _, False, True) => do

651 |               log $ show paths <+> ": HEAD in HEADERS with END_STREAM and END_HEADERS, sending reply"

652 |               pure . Just $ headerFramesForHTML streamIdent

653 |             _ => do

654 |               log "Unknown HEADERS ended, sending nothing"

655 |               pure Nothing

656 |         (False, False) => do

657 |           () <- appendAccumulated streamIdent p

658 |           pure Nothing

659 |         (False, True) => do

660 |           -- it can't be a continuation because the header is ending here

661 |           -- if either of these is set, the following frame can't be a continuation

662 |           -- and the previous can't have been either, since there is only one HEADER frame, and this is one

663 |           headers <- errorsAsCompressionErrors (decodeHpack p)

664 |           log "Got headers, changing to Open state"

665 |           log $ show headers

666 |           lift $ modifyStreamState streamIdent {continuationState := Nothing, cont := Forbidden, status := NonClosed $ Open [] headers }

667 |           pure Nothing

668 |         (True, False) => do

669 |            -- stream is ending but headers are not. this means a continuation frame

670 |            -- will come with the rest of the headers, -- but after that, no data will

671 |            -- come (this is the meaning of end_stream).

672 |            -- because we don't really care about the headers, we just reply now.

673 |            -- but really this should wait for all continuation frames.

674 |            lift $ modifyStreamState streamIdent {continuationState := Nothing, cont := Forbidden, status := Closed }

675 |            log "Received HEADERS has END_STREAM set, sending OK reply"

676 |            resp <- ask

677 |            reply <- lift $ lift $ resp $ MkRequest streamIdent "/" [] []

678 |            pure $ Just reply

680 | pingParser : Bits32 -> Payload -> Flags -> Maybe (List Frame)

681 | pingParser streamIdent pl@(MkPayload p) (MkFlags f) =

682 |   if streamIdent == 0 && f /= 1 && length p == 8

683 |     then

684 |       Just [MkFrame Ping (MkFlags 1) 0 pl]

685 |     else Nothing

687 | continuationParser : Bits32 -> Payload -> Flags -> NonClosedStreamState -> HandlerResult (Maybe (List Frame))

688 | continuationParser 0 _ _ _ =

689 |   throwE ProtocolErrorCode

690 | continuationParser streamIdent (MkPayload p) fl nonClosed = do

691 |   () <- appendAccumulated streamIdent p

692 |   if is END_HEADERS fl

693 |     then do

694 |       let

695 |         newState =

696 |           case nonClosed of

697 |           Idle => do

698 |             NonClosed $ Open [] []

699 |           Open _ _ => do

700 |             -- trailing headers

701 |             Closed

702 |       lift $ modifyStreamState streamIdent { continuationState := Nothing, cont := Forbidden, status := newState}

703 |       case newState of

704 |         Closed => do

705 |           -- trailing headers

706 |           resp <- ask

707 |           reply <- lift $ lift $ resp $ MkRequest streamIdent "/" [] [] -- TODO we should have saved the headers and req body to pass in here

708 |           pure $ Just reply

709 |         _ => do

710 |           -- test like h2spec/6.10 still passed when this was committed,

711 |           -- even though we deliver no reply here, because we have prematurely sent the reply in the (True, False)

712 |           -- branch of headersParser

713 |           log "CONTINUATION with END_HEADERS but NOT REPLYING"

714 |           pure Nothing

715 |     else

716 |       pure Nothing

718 | rstStreamParser : MonadState ConnState m => NonClosedStreamState -> Bits32 -> Payload -> Flags -> EitherT ErrorCode m (Maybe (List Frame))

719 | rstStreamParser nonClosed streamIdent (MkPayload p) _ = do

720 |   when (length p /= 4) (throwE FrameSizeErrorCode)

721 |   case nonClosed of

722 |     Idle => do

723 |       -- h2spec: http2/5.1/2

724 |       throwE ProtocolErrorCode

725 |     Open _ _ => do

726 |       lift $ modifyStreamState streamIdent { status := Closed }

727 |       pure Nothing

729 | windowUpdateParser : MonadState ConnState m => NonClosedStreamState -> Bits32 -> Payload -> Flags -> EitherT ErrorCode m (Maybe (List Frame))

730 | windowUpdateParser _ streamIdent (MkPayload possiblyNotFourBytes) _ = do

731 |   case Vect.toVect 4 possiblyNotFourBytes of

732 |     Nothing => throwE FrameSizeErrorCode

733 |     Just p => do

734 |       when (p == [0, 0, 0, 0]) $ do

735 |         -- RFC 9113 section 6.9 (WINDOW_UPDATE)

736 |         -- A receiver MUST treat the receipt of a WINDOW_UPDATE frame with a

737 |         -- flow-control window increment of 0 as a stream error (Section 5.4.2)

738 |         -- of type PROTOCOL_ERROR

739 |         log "Window update payload is all zeroes, throwing ProtocolErrorCode"

740 |         throwE ProtocolErrorCode

741 |       -- h2spec's test http2/5.1/3 seems to imply that a WINDOW_UPDATE in the 'idle' state is a ProtocolError.

742 |       -- But curl seems to send this, and therefore I am opting to not simply throw this error here.

743 |       -- Even though it means that h2spec fails on this test.

744 |       lift $ modifyStreamState streamIdent {windowSize $= (+ (bits32FromBigEndian p))}

745 |       pure Nothing

747 | framePayloadParserFor : FrameType -> Bits32 -> Payload -> Flags -> HandlerResult (Maybe (List Frame))

748 | framePayloadParserFor f streamIdent payload flags = do

749 |   st <- getStreamState streamIdent

750 |   when ((f, st.cont) == (Continuation, Forbidden)) $ throwE ProtocolErrorCode

751 |   when (f /= Continuation && st.cont == Require) $ throwE ProtocolErrorCode

752 |   NonClosed nonClosed <- pure st.status

753 |     | Closed => do

754 |       log $ "message on closed stream: " ++ show streamIdent

755 |       throwE StreamClosedErrorCode

756 |   case f of

757 |     Data => dataParser nonClosed streamIdent payload flags

758 |     Settings => settingsParser streamIdent payload flags

759 |     Headers => headersParser nonClosed streamIdent payload flags st

760 |     Ping => pure $ pingParser streamIdent payload flags

761 |     Continuation => continuationParser streamIdent payload flags nonClosed

762 |     RstStream => rstStreamParser nonClosed streamIdent payload flags

763 |     WindowUpdate => windowUpdateParser nonClosed streamIdent payload flags

764 |     -- TODO

765 |     t => do

766 |       log $ "UNRECOGNIZED FRAME " ++ show t

767 |       pure Nothing

769 | framePayloadLength : Frame -> Nat

770 | framePayloadLength f =

771 |   let

772 |   MkPayload p := f.payload

773 |   in

774 |   length p

776 | sendFramesIfAble : Bits32 -> ConnState -> H2BufConn ConnState

777 | sendFramesIfAble newSI newSt = do

778 |   bufConSt <- get

779 |   let

780 |     window : Bits32

781 |     window =

782 |       min newSt.maxFrameSize $

783 |         case lookup newSI newSt.streams of

784 |           Just streamState =>

785 |             streamState.windowSize

786 |           Nothing =>

787 |             newSt.initialWindowSize

788 |   case bufConSt.queuedToSend of

789 |     frame :: rest => do

790 |       let frameFits = cast (framePayloadLength frame) <= window

791 |       let windowNotEmpty = window > 0

792 |       case (frame.frameType == Data, frameFits, windowNotEmpty) of

793 |         (_, True, _) => do

794 |           send $ encodeFrame frame

795 |           modify { queuedToSend := rest }

796 |           sendFramesIfAble newSI $ { streams $= modifyMap newSI { windowSize $= (\x => x - cast (framePayloadLength frame)) }} newSt

797 |         (True, _, True) => do

798 |           let MkPayload p := frame.payload

799 |           let (first, second) = splitAt (cast window) p

800 |           let firstFrame = MkFrame Data (MkFlags 0) newSI (MkPayload first)

801 |           -- If the frame had END_STREAM, the second frame will inherit it

802 |           let secondFrame = MkFrame Data frame.flags newSI (MkPayload second)

803 |           send $ encodeFrame firstFrame

804 |           modify { queuedToSend := secondFrame :: rest }

805 |           sendFramesIfAble newSI $ { streams $= modifyMap newSI { windowSize := 0 }} newSt

806 |         _ => pure newSt

807 |     _ => pure newSt

809 | processFrame: Responder -> ConnState -> Frame -> H2BufConn ConnState

810 | processFrame responder state frame = do

811 |   let framePayload = frame.payload

812 |   let frameHeaderFlags = frame.flags

813 |   log $ "Frame type " ++ show frame.frameType

814 |   let

815 |     rwstComputation : RWST Responder Unit ConnState (Cont (DIterator (List Bits8) (List Bits8) PgRows PgInput Void)) (Either ErrorCode (Maybe (List Frame)))

816 |     rwstComputation =

817 |       runEitherT $

818 |         framePayloadParserFor frame.frameType frame.streamIdent framePayload frameHeaderFlags

819 |     ranRwst : InnerCont (Either ErrorCode (Maybe (List Frame)), ConnState, Unit)

820 |     ranRwst = runRWST responder state rwstComputation

821 |   (errOrStuffToSend, newSt, ()) <- lift ranRwst

822 |   case errOrStuffToSend of

823 |     Left err => do

824 |       log $ "processFrame: Sending GOAWAY with ErrorCode " <+> show err

825 |       modify {queuedToSend $= (++ errReply err frame.streamIdent)}

826 |     Right (Just toSend) => do

827 |       modify {queuedToSend $= (++ toSend)}

828 |     _ =>

829 |       pure ()

830 |   sendFramesIfAble frame.streamIdent newSt

832 | frameReader: Responder -> ConnState -> H2BufConn Void

833 | frameReader responder state = do

834 |   frameHeaderLength <- read 3

835 |   frameHeaderType :: [] <- read 1

836 |   frameHeaderFlags :: [] <- read 1

837 |   frameHeaderReservedAndStreamIdentifier <- read 4

838 |   let [b2, b1, b0] = frameHeaderLength

839 |   let natLen = bits8ToNat b2 16 + bits8ToNat b1 8 + bits8ToNat b0 0

840 |   framePayload <- read natLen

841 |   newState <-

842 |     case parseType frameHeaderType of

843 |       Just frameType => do

844 |         let

845 |           -- ignore reserved bit

846 |           [s3, s2, s1, s0] = frameHeaderReservedAndStreamIdentifier

847 |           newSI : Bits32

848 |           newSI =

849 |                 (cast (s3 .&. 0x7f) `shiftL` 24)

850 |             .|. (cast s2 `shiftL` 16)

851 |             .|. (cast s1 `shiftL` 8)

852 |             .|. (cast s0)

853 |           frame : Frame

854 |           frame = MkFrame

855 |             frameType (MkFlags frameHeaderFlags) newSI (MkPayload $ toList framePayload)

856 |         processFrame responder state frame

857 |       Nothing => do

858 |         log $ "Unknown frame type: " ++ show frameHeaderType

859 |         pure state

860 |   frameReader responder newState

862 | ignoreAndLog: H2BufConn Void

863 | ignoreAndLog = do

864 |   bite <- read 1

865 |   log $ "Ignoring " ++ show bite

866 |   ignoreAndLog

868 | prefaceRef : List Bits8

869 | prefaceRef = toList $ utf8Encode "PRI * HTTP/2.0\r\n\r\nSM\r\n\r\n"

871 | mkBufConn: Responder -> H2BufConn Void

872 | mkBufConn responder = do

873 |   prefaceReal <- read (length prefaceRef)

874 |   if (toList prefaceReal /= prefaceRef)

875 |     then do

876 |       log "Received bad preface, ignoring all"

877 |       let frag = errReply ProtocolErrorCode 0

878 |       traverse_ (\x => send $ encodeFrame x) frag

879 |       ignoreAndLog

880 |     else do

881 |       send [   0, 0, 6 -- len 6

882 |              , 4 -- settings

883 |              , 0, 0, 0, 0, 0, 0

884 |              , 3

885 |              , 0, 0, 0, 0x64 -- max_concurrent_streams=100

886 |            ]

887 |       frameReader responder initialConnState

890 | mkInitialHttp2Iter: (Request -> InnerCont (List Frame)) -> DIterator (List Bits8) (List Bits8) PgRows PgInput Void

891 | mkInitialHttp2Iter =

892 |   BufConn.iteratorFromBufConn (MkBufConSt [] []) . mkBufConn