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