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