9467b037fd40b20f3533264b16006603e8c4f8514d717f0f1b3b7f2db62c0569.tri (17272B)
1 !import prelude * 2 !import io * 3 !import socket * 4 !import parser * 5 !import native_math as Nat 6 !export * 7 8 -- --------------------------------------------------------------------------- 9 -- Constants 10 -- --------------------------------------------------------------------------- 11 12 maxHeaderBytes = 65536 13 maxBodyBytes = 1048576 14 15 crlfcrlf = pair 13 (pair 10 (pair 13 (pair 10 t))) 16 17 -- --------------------------------------------------------------------------- 18 -- Response construction 19 -- --------------------------------------------------------------------------- 20 21 statusPhrases = 22 [(pair 200 "OK") 23 (pair 201 "Created") 24 (pair 204 "No Content") 25 (pair 400 "Bad Request") 26 (pair 404 "Not Found") 27 (pair 405 "Method Not Allowed") 28 (pair 413 "Content Too Large") 29 (pair 431 "Request Header Fields Too Large") 30 (pair 501 "Not Implemented") 31 (pair 505 "HTTP Version Not Supported")] 32 33 lookupStatusPhrase code [(key, phrase) | rest] = (let 34 select ^code = phrase 35 select _ = lookupStatusPhrase code rest 36 in select key) 37 lookupStatusPhrase _ _ = "Internal Server Error" 38 39 statusPhrase code = lookupStatusPhrase code statusPhrases 40 41 statusLine code phrase = append "HTTP/1.1 " (append (showNumber code) (append " " (append phrase "\r\n"))) 42 headerLine key value = append key (append ": " (append value "\r\n")) 43 44 httpAppendResponseHeader accumulated (key, value) = append accumulated (headerLine key value) 45 -- Preserve the old pair-projection fallback for malformed response-header items. 46 httpAppendResponseHeader accumulated _ = append accumulated (headerLine "" "") 47 48 buildResponse status headers body = (append 49 (statusLine status (statusPhrase status)) 50 (append (foldl httpAppendResponseHeader "" headers) (append "\r\n" body))) 51 52 response status contentType body = (buildResponse status 53 [(pair "Content-Type" contentType) 54 (pair "Content-Length" (showNumber (length body))) 55 (pair "Connection" "close")] 56 body) 57 58 emptyResponse status = (buildResponse status 59 [(pair "Content-Length" "0") (pair "Connection" "close")] 60 "") 61 62 okResponse body = response 200 "text/plain; charset=utf-8" body 63 textResponse body = response 200 "text/plain; charset=utf-8" body 64 jsonResponse body = response 200 "application/json" body 65 htmlResponse body = response 200 "text/html; charset=utf-8" body 66 createdResponse body = response 201 "text/plain; charset=utf-8" body 67 notFoundResponse = response 404 "text/plain; charset=utf-8" "Not found\n" 68 badRequestResponse message = response 400 "text/plain; charset=utf-8" message 69 errorResponse status message = response status "text/plain; charset=utf-8" message 70 71 headerEndState 2 13 = 3 72 headerEndState _ 13 = 1 73 headerEndState 3 10 = 4 74 headerEndState 1 10 = 2 75 headerEndState _ _ = 0 76 77 httpHeadersOnly [byte | rest] state reversed = (let 78 accumulated = pair byte reversed 79 continue 4 = reverse accumulated 80 continue next = httpHeadersOnly rest next accumulated 81 in continue (headerEndState state byte)) 82 httpHeadersOnly _ _ reversed = reverse reversed 83 84 headersOnly bytes = httpHeadersOnly bytes 0 [] 85 86 responseForMethod "HEAD" response = headersOnly response 87 responseForMethod _ response = response 88 89 -- --------------------------------------------------------------------------- 90 -- Header receive / framing 91 -- --------------------------------------------------------------------------- 92 93 -- maxBytes bounds the entire accumulated receive buffer, including any 94 -- prefetched suffix. Retain that policy; this is not a header-only byte count. 95 httpRecvUntil sock delimiter limit accumulated count = (let 96 received (t, _) = pure (err 400 accumulated) 97 received ((t t), ([], _)) = pure (err 400 accumulated) 98 received ((t t), (chunk, _)) = (let 99 next = append accumulated chunk 100 nextCount = Nat.add count (length chunk) 101 found ^true = pure (ok next t) 102 found _ = httpRecvUntil sock delimiter limit next nextCount 103 bounded ^true = found (contains? delimiter next) 104 bounded _ = pure (err 431 next) 105 in bounded (Nat.lte nextCount limit)) 106 received _ = pure (err 400 accumulated) 107 in do bind 108 reply <- recv sock 4096 109 received reply) 110 111 recvUntilMax sock delimiter limit = httpRecvUntil sock delimiter limit [] 0 112 113 recvUntil sock delimiter = recvUntilMax sock delimiter maxHeaderBytes 114 115 recvHeaders sock = recvUntilMax sock crlfcrlf maxHeaderBytes 116 117 -- --------------------------------------------------------------------------- 118 -- Request line parsing 119 -- --------------------------------------------------------------------------- 120 121 -- HTTP/1.1 lines require CRLF. A bare CR/LF is an error, never a byte to 122 -- discard. Failure retains the offending suffix and prior consumption; EOF 123 -- cannot masquerade as a successfully parsed empty line. 124 httpLineError code found rest consumed = (parserReplyFail 125 (parserDiagnostic code "CRLF" found t ["http-line"]) 126 rest consumed false) 127 128 httpScanLine [13 10 | rest] reversed = parserReplyOk (reverse reversed) rest true false 129 httpScanLine input{[13 | _]} reversed = httpLineError 2 13 input (not? (emptyList? reversed)) 130 httpScanLine input{[10 | _]} reversed = httpLineError 2 10 input (not? (emptyList? reversed)) 131 httpScanLine [byte | rest] reversed = httpScanLine rest (pair byte reversed) 132 httpScanLine [] reversed = httpLineError 1 t [] (not? (emptyList? reversed)) 133 httpScanLine input reversed = httpLineError 2 input input (not? (emptyList? reversed)) 134 135 httpLineReply input = httpScanLine input [] 136 httpBadRequest = err 400 "Bad Request\n" 137 138 -- Unlike the old pair-only helper, this Result distinguishes a blank CRLF 139 -- line from truncated/malformed input. Both callers propagate the failure. 140 readLineBytes input = (parserMatchReply 141 (_ _ _ _ : httpBadRequest) 142 (line rest _ _ : ok line rest) 143 (httpLineReply input)) 144 145 -- The finite request line is already framed by readLineBytes. Deliberately 146 -- retain the historical three-fields grammar: empty fields are permitted, 147 -- but a third separating space is an error. The parser reply exposes byte 148 -- consumption to new clients, while parseThreeWords preserves HTTP's public 149 -- Result/400 boundary and the original "Bad Request" remainder. 150 httpNonSpace? byte = not? (equal? byte 32) 151 152 httpThreeWordsReply = (parserContext "request-line" (do parserBind 153 method <- parserTakeWhile httpNonSpace? 154 parserExpect 32 155 target <- parserTakeWhile httpNonSpace? 156 parserExpect 32 157 version <- parserTakeWhile httpNonSpace? 158 parserEof 159 parserPure (pair method (pair target version)))) 160 161 parseThreeWords = (bs : 162 parserMatchReply 163 (diagnostic rest consumed committed : err 400 "Bad Request\n") 164 (words rest consumed committed : ok words rest) 165 (httpThreeWordsReply bs)) 166 167 parseRequestLine input = (let 168 parseLine ((t t), (line, rest)) = (let 169 parsed ((t t), (request, _)) = ok request rest 170 parsed _ = httpBadRequest 171 in parsed (parseThreeWords line)) 172 parseLine _ = httpBadRequest 173 in parseLine (readLineBytes input)) 174 175 -- --------------------------------------------------------------------------- 176 -- Header parsing 177 -- --------------------------------------------------------------------------- 178 179 180 boolOr? = (a b : 181 matchBool true b a) 182 183 -- Canonical byte input (0..255), as supplied by the socket/byte codecs. 184 -- Historical malformed numeral/bit behavior is intentionally not a contract. 185 toLowerAsciiByte byte = (let 186 lower ^true = Nat.add byte 32 187 lower _ = byte 188 in lower (Nat.inRange byte 65 90)) 189 190 -- RFC 9110 token names, OWS, and field-value bytes. obs-text (128..255) 191 -- stays opaque; only the ASCII header name is lowercased. Reject obs-fold. 192 httpTokenByte? byte = (or? (Nat.letter byte) 193 (or? (Nat.digit byte) (any? (equal? byte) "!#$%&'*+-.^_`|~"))) 194 httpOws? byte = or? (equal? byte 32) (equal? byte 9) 195 httpFieldByte? byte = (or? (equal? byte 9) 196 (or? (Nat.printable byte) (Nat.inRange byte 128 255))) 197 httpTrimOws value = reverse (dropWhile httpOws? (reverse (dropWhile httpOws? value))) 198 199 -- Parse exactly one finite line, excluding CRLF. Preserve parser diagnostics 200 -- and consumption, but never accept a valid prefix followed by invalid bytes. 201 httpHeaderLineReply = (parserContext "header-line" (do parserBind 202 name <- parserLabel "header-name" (parserSome (parserSatisfy httpTokenByte?)) 203 parserLabel "colon" (parserExpect 58) 204 value <- parserLabel "header-value" (parserBefore (parserTakeWhile httpFieldByte?) parserEof) 205 parserPure (pair (map toLowerAsciiByte name) (httpTrimOws value)))) 206 207 -- Only an actual empty CRLF line ends the headers. The returned suffix is 208 -- opaque body data, even if it contains CR, LF, NUL or header-looking bytes. 209 httpParseHeaderLines input reversedHeaders = (let 210 parseLine ((t t), ([], rest)) = ok (reverse reversedHeaders) rest 211 parseLine ((t t), (line, rest)) = (let 212 continue ((t t), (header, _)) = httpParseHeaderLines rest (pair header reversedHeaders) 213 continue _ = httpBadRequest 214 in continue (httpHeaderLineReply line)) 215 parseLine _ = httpBadRequest 216 in parseLine (readLineBytes input)) 217 218 parseHeaders input = httpParseHeaderLines input [] 219 220 -- --------------------------------------------------------------------------- 221 -- Content-Length parsing 222 -- --------------------------------------------------------------------------- 223 224 -- The accumulator never exceeds maxBodyBytes. A single checked step can 225 -- reach at most 10 * maxBodyBytes + 9; after that, validate digits without 226 -- constructing a larger number. Trailing junk still means 400, not 413. 227 httpBodyTooLarge = err 413 "Request body too large\n" 228 229 httpLengthOverflow [] = httpBodyTooLarge 230 httpLengthOverflow [byte | rest] = (let 231 continue ^true = httpLengthOverflow rest 232 continue _ = httpBadRequest 233 in continue (Nat.digit byte)) 234 httpLengthOverflow _ = httpBadRequest 235 236 httpLengthDigits [] value = ok (just value) t 237 httpLengthDigits [byte | rest] value = (let 238 digit ^true = (let 239 next = Nat.decimal value (Nat.subtract byte 48) 240 bounded ^true = httpLengthDigits rest next 241 bounded _ = httpLengthOverflow rest 242 in bounded (Nat.lte next maxBodyBytes)) 243 digit _ = httpBadRequest 244 in digit (Nat.digit byte)) 245 httpLengthDigits _ _ = httpBadRequest 246 247 -- Input is a finite canonical byte list, with no OWS: parseHeaders already 248 -- trims field edges. Empty strings, signs, commas and interior whitespace fail. 249 parseContentLengthValue input{[_ | _]} = httpLengthDigits input 0 250 parseContentLengthValue _ = httpBadRequest 251 252 -- Input names are normalized by parseHeaders. Select the sole raw length 253 -- before decoding: duplicate fields and unsupported transfer coding are 400 254 -- regardless of field order or whether a length would otherwise exceed limits. 255 -- This server supports Content-Length framing only, not chunked decoding. 256 httpSelectLength [] t = ok nothing t 257 httpSelectLength [] (t value) = parseContentLengthValue value 258 httpSelectLength [("transfer-encoding", _) | _] _ = httpBadRequest 259 httpSelectLength [("content-length", value) | rest] t = httpSelectLength rest (just value) 260 httpSelectLength [("content-length", _) | _] _ = httpBadRequest 261 httpSelectLength [(_, _) | rest] selected = httpSelectLength rest selected 262 httpSelectLength _ _ = httpBadRequest 263 264 contentLength headers = httpSelectLength headers nothing 265 266 -- --------------------------------------------------------------------------- 267 -- Body reading 268 -- --------------------------------------------------------------------------- 269 270 bodyReadState remaining reversed rest = pair remaining (pair reversed rest) 271 272 -- State is (remaining, (reversed body, unused input)); zero consumes nothing. 273 -- remaining is a canonical natural supplied by the bounded length decoder. 274 takeBodyBytes bytes 0 reversed = bodyReadState 0 reversed bytes 275 takeBodyBytes [byte | rest] remaining reversed = takeBodyBytes rest (Nat.subtract remaining 1) (pair byte reversed) 276 takeBodyBytes _ remaining reversed = bodyReadState remaining reversed [] 277 278 -- Retain the existing receive-size buckets, expressed as native comparisons 279 -- rather than bit shifts. Zero is handled before asking for another chunk. 280 httpRecvBucket remaining [size | rest] = (let 281 choose ^true = size 282 choose _ = httpRecvBucket remaining rest 283 in choose (Nat.gte remaining size)) 284 httpRecvBucket _ _ = 1 285 286 recvChunkMax4096 remaining = httpRecvBucket remaining [4096 1024 256 64 16] 287 288 -- One state machine owns both buffered and subsequent socket input. EOF before 289 -- completion is a 400, not another recv with unchanged remaining length. 290 httpReadBodyState _ (0, (reversed, rest)) = pure (ok (reverse reversed) rest) 291 httpReadBodyState sock (remaining, (reversed, _)) = (let 292 received (t, (message, _)) = pure (err 400 (append "recv failed while reading body: " message)) 293 received ((t t), ([], _)) = pure (err 400 "Unexpected end of request body\n") 294 received ((t t), (chunk, _)) = httpReadBodyState sock (takeBodyBytes chunk remaining reversed) 295 received _ = pure httpBadRequest 296 in do bind 297 reply <- recv sock (recvChunkMax4096 remaining) 298 received reply) 299 httpReadBodyState _ _ = pure httpBadRequest 300 301 readBodyMore sock remaining reversed = httpReadBodyState sock (bodyReadState remaining reversed []) 302 readBodyExact sock expected initial = httpReadBodyState sock (takeBodyBytes initial expected []) 303 304 -- readBodyExact starts with remaining + length(reversed) = expected. 305 -- takeBodyBytes preserves that sum; only remaining=0 succeeds, while early EOF 306 -- or recv failure returns an error. A successful body already has exact length: 307 -- do not traverse it again solely to recount it. 308 readBody sock headers initial = (let 309 selected ((t t), (t, _)) = pure (ok [] initial) 310 selected ((t t), ((t count), _)) = readBodyExact sock count initial 311 selected failure = pure failure 312 in selected (contentLength headers)) 313 314 -- --------------------------------------------------------------------------- 315 -- Request validation 316 -- --------------------------------------------------------------------------- 317 318 validMethod? "GET" = true 319 validMethod? "POST" = true 320 validMethod? "HEAD" = true 321 validMethod? _ = false 322 323 validVersion? "HTTP/1.1" = true 324 validVersion? "HTTP/1.0" = true 325 validVersion? _ = false 326 327 validTarget? [47 | _] = true 328 validTarget? _ = false 329 330 -- Keep error precedence: method, version, then target. Headers are validated 331 -- separately; accepting them here does not select body framing. 332 validateRequest method target version _ = (let 333 targetChecked ^true = ok t t 334 targetChecked _ = httpBadRequest 335 versionChecked ^true = targetChecked (validTarget? target) 336 versionChecked _ = err 505 "HTTP Version Not Supported\n" 337 methodChecked ^true = versionChecked (validVersion? version) 338 methodChecked _ = httpBadRequest 339 in methodChecked (validMethod? method)) 340 341 -- --------------------------------------------------------------------------- 342 -- Handler pipeline 343 -- --------------------------------------------------------------------------- 344 345 routerMethod "HEAD" = "GET" 346 routerMethod method = method 347 348 -- finally preserves a send Result and attempts close even after send failure. 349 -- Like the existing IO helper, it does not catch host exceptions/abortIO. 350 respondAndClose sock response = (do onOk_ 351 finally (send sock response) (closeSocket_ sock) 352 pure (ok t t)) 353 354 httpRespond client method response = respondAndClose client (responseForMethod method response) 355 356 httpHandleBody router client method target headers reply = (let 357 handle ((t t), (body, _)) = (do bind 358 response <- router (routerMethod method) target headers body 359 httpRespond client method response) 360 handle (t, (status, message)) = httpRespond client method (errorResponse status message) 361 handle _ = httpRespond client method (badRequestResponse "Bad Request\n") 362 in handle reply) 363 364 httpHandleHeaders router client method target version input = (let 365 headersParsed ((t t), (headers, initial)) = (let 366 validated ((t t), _) = (do bind 367 reply <- readBody client headers initial 368 httpHandleBody router client method target headers reply) 369 validated (t, (status, message)) = httpRespond client method (errorResponse status message) 370 validated _ = httpRespond client method (badRequestResponse "Bad Request\n") 371 in validated (validateRequest method target version headers)) 372 -- Retain historical behavior: a header syntax failure has no trusted HEAD 373 -- response handling, even though the request line has already been parsed. 374 headersParsed _ = respondAndClose client (badRequestResponse "Bad Request\n") 375 in headersParsed (parseHeaders input)) 376 377 httpHandleRequest router client ((t t), ((method, (target, version)), headers)) = httpHandleHeaders router client method target version headers 378 httpHandleRequest _ client _ = respondAndClose client (badRequestResponse "Bad Request\n") 379 380 httpHandleReceived router client ((t t), (raw, _)) = httpHandleRequest router client (parseRequestLine raw) 381 httpHandleReceived _ client (t, (431, _)) = respondAndClose client (errorResponse 431 "Request Header Fields Too Large\n") 382 httpHandleReceived _ client _ = respondAndClose client (badRequestResponse "Bad Request\n") 383 384 httpHandlerIO router client _ = (do bind 385 reply <- recvHeaders client 386 httpHandleReceived router client reply) 387 388 -- One effectful pipeline; a pure router needs only this value-to-action adapter. 389 httpPureRouter router method target headers body = pure (router method target headers body) 390 httpHandler router client peer = httpHandlerIO (httpPureRouter router) client peer