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