mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
fix: http1.0 behavior
This commit is contained in:
@@ -309,9 +309,13 @@ private def checkReceivingMessageHead (message : Message.Head .receiving) : Exce
|
||||
if !isValidRequestTargetForMethod message then
|
||||
throw .badMessage
|
||||
|
||||
-- Host validation
|
||||
if !hasSingleAcceptedHostHeader message then
|
||||
throw .badMessage
|
||||
-- Host validation:
|
||||
-- • HTTP/1.1: a Host header is REQUIRED (RFC 9112 §3.2).
|
||||
-- • HTTP/1.0: Host is optional (RFC 2616 §14.23), but if present it must
|
||||
-- be a single, well-formed value (no duplicates, correct authority form).
|
||||
if message.version == .v11 || message.headers.contains .host then
|
||||
if !hasSingleAcceptedHostHeader message then
|
||||
throw .badMessage
|
||||
|
||||
-- Gets the size of the message.
|
||||
match message.getSize (allowEOFBody := true) with
|
||||
|
||||
@@ -91,7 +91,11 @@ def Message.Head.getSize (message : Message.Head dir) (allowEOFBody : Bool) : Op
|
||||
let te := Header.TransferEncoding.parse header
|
||||
|
||||
match Header.TransferEncoding.isChunked <$> te, contentLength with
|
||||
| some true, none => some .chunked
|
||||
| some true, none =>
|
||||
-- HTTP/1.0 does not define chunked transfer encoding (RFC 2068 §19.4.6).
|
||||
-- A server MUST NOT use chunked with an HTTP/1.0 peer; likewise, an
|
||||
-- HTTP/1.0 request carrying Transfer-Encoding: chunked is malformed.
|
||||
if message.version == .v10 then none else some .chunked
|
||||
| _, _ => none -- To avoid request smuggling when TE and CL are mixed.
|
||||
|
||||
-- We disallow multiple transfer-encoding headers.
|
||||
@@ -99,23 +103,24 @@ def Message.Head.getSize (message : Message.Head dir) (allowEOFBody : Bool) : Op
|
||||
/--
|
||||
Checks whether the message indicates that the connection should be kept alive.
|
||||
-/
|
||||
@[inline]
|
||||
def Message.Head.shouldKeepAlive (message : Message.Head dir) : Bool :=
|
||||
if message.version ≠ .v11 then
|
||||
false
|
||||
else
|
||||
let tokens? : Option (Array String) :=
|
||||
match message.headers.getAll? .connection with
|
||||
| none => true
|
||||
| none => some #[]
|
||||
| some values =>
|
||||
let tokens? : Option (Array String) :=
|
||||
values.foldl (fun acc raw => do
|
||||
let acc ← acc
|
||||
let parsed ← Header.Connection.parse raw
|
||||
pure (acc ++ parsed.tokens)
|
||||
) (some #[])
|
||||
match tokens? with
|
||||
| none => false
|
||||
| some tokens => !tokens.any (· == "close")
|
||||
values.foldl (fun acc raw => do
|
||||
let acc ← acc
|
||||
let parsed ← Header.Connection.parse raw
|
||||
pure (acc ++ parsed.tokens)
|
||||
) (some #[])
|
||||
|
||||
match tokens? with
|
||||
| none =>false
|
||||
| some tokens =>
|
||||
if message.version == .v11 then
|
||||
!tokens.any (· == "close")
|
||||
else
|
||||
tokens.any (· == "keep-alive")
|
||||
|
||||
instance : Repr (Message.Head dir) :=
|
||||
match dir with
|
||||
|
||||
Reference in New Issue
Block a user