f3a638408191ef8c13cb42d1e6561aa9e716db2facc4b42421bf5ff96750afe5.tri (13052B)
1 !import prelude * 2 !import parser * 3 !import native_math as Nat 4 !export * 5 6 -- --------------------------------------------------------------------------- 7 -- Constants 8 -- --------------------------------------------------------------------------- 9 10 maxHeaderBytes = 65536 11 maxBodyBytes = 1048576 12 13 crlfcrlf = pair 13 (pair 10 (pair 13 (pair 10 t))) 14 15 -- --------------------------------------------------------------------------- 16 -- Response construction 17 -- --------------------------------------------------------------------------- 18 19 statusPhrases = 20 [(pair 200 "OK") 21 (pair 201 "Created") 22 (pair 204 "No Content") 23 (pair 400 "Bad Request") 24 (pair 404 "Not Found") 25 (pair 405 "Method Not Allowed") 26 (pair 413 "Content Too Large") 27 (pair 431 "Request Header Fields Too Large") 28 (pair 501 "Not Implemented") 29 (pair 505 "HTTP Version Not Supported")] 30 31 lookupStatusPhrase code [(key, phrase) | rest] = case key of 32 ^code = phrase 33 _ = lookupStatusPhrase code rest 34 35 lookupStatusPhrase _ _ = "Internal Server Error" 36 37 statusPhrase code = lookupStatusPhrase code statusPhrases 38 39 statusLine code phrase = append "HTTP/1.1 " (append (showNumber code) (append " " (append phrase "\r\n"))) 40 headerLine key value = append key (append ": " (append value "\r\n")) 41 42 httpAppendResponseHeader accumulated (key, value) = append accumulated (headerLine key value) 43 -- Preserve the old pair-projection fallback for malformed response-header items. 44 httpAppendResponseHeader accumulated _ = append accumulated (headerLine "" "") 45 46 buildResponse status headers body = (append 47 (statusLine status (statusPhrase status)) 48 (append (foldl httpAppendResponseHeader "" headers) (append "\r\n" body))) 49 50 -- Count a proper response-body list in one pass. Unlike general listOf, 51 -- this boundary never transforms elements, so no validated copy is needed. 52 -- Force each successor's outer constructor before advancing: do not retain a 53 -- successor continuation for every byte. Input elements remain unforced. 54 -- Malformed list spines retain length's ordinary contract-failure Result. 55 httpBodyLength values = let rec 56 walk remaining count = triage count 57 (_ : contractErr "not a list" t) 58 (_ tail : case Nat.successor count of 59 next{(_, _)} = walk tail next 60 _ = contractErr "Invalid internal length counter" t) 61 remaining 62 in walk values 0 63 64 response status contentType body = (buildResponse status 65 [(pair "Content-Type" contentType) 66 (pair "Content-Length" (showNumber (httpBodyLength body))) 67 (pair "Connection" "close")] 68 body) 69 70 emptyResponse status = (buildResponse status 71 [(pair "Content-Length" "0") (pair "Connection" "close")] 72 "") 73 74 okResponse body = response 200 "text/plain; charset=utf-8" body 75 textResponse body = response 200 "text/plain; charset=utf-8" body 76 jsonResponse body = response 200 "application/json" body 77 htmlResponse body = response 200 "text/html; charset=utf-8" body 78 createdResponse body = response 201 "text/plain; charset=utf-8" body 79 notFoundResponse = response 404 "text/plain; charset=utf-8" "Not found\n" 80 badRequestResponse message = response 400 "text/plain; charset=utf-8" message 81 errorResponse status message = response status "text/plain; charset=utf-8" message 82 83 headerEndState 2 13 = 3 84 headerEndState _ 13 = 1 85 headerEndState 3 10 = 4 86 headerEndState 1 10 = 2 87 headerEndState _ _ = 0 88 89 httpHeadersOnly [byte | rest] state reversed = (let 90 accumulated = pair byte reversed 91 continue 4 = reverse accumulated 92 continue next = httpHeadersOnly rest next accumulated 93 in continue (headerEndState state byte)) 94 httpHeadersOnly _ _ reversed = reverse reversed 95 96 headersOnly bytes = httpHeadersOnly bytes 0 [] 97 98 responseForMethod "HEAD" response = headersOnly response 99 responseForMethod _ response = response 100 101 -- --------------------------------------------------------------------------- 102 -- Request line parsing 103 -- --------------------------------------------------------------------------- 104 105 -- HTTP/1.1 lines require CRLF. A bare CR/LF is an error, never a byte to 106 -- discard. Failure retains the offending suffix and prior consumption; EOF 107 -- cannot masquerade as a successfully parsed empty line. 108 httpLineError code found rest consumed = (parserReplyFail 109 (parserDiagnostic code "CRLF" found t ["http-line"]) 110 rest consumed false) 111 112 httpScanLine [13 10 | rest] reversed = parserReplyOk (reverse reversed) rest true false 113 httpScanLine input{[13 | _]} reversed = httpLineError 2 13 input (not? (emptyList? reversed)) 114 httpScanLine input{[10 | _]} reversed = httpLineError 2 10 input (not? (emptyList? reversed)) 115 httpScanLine [byte | rest] reversed = httpScanLine rest (pair byte reversed) 116 httpScanLine [] reversed = httpLineError 1 t [] (not? (emptyList? reversed)) 117 httpScanLine input reversed = httpLineError 2 input input (not? (emptyList? reversed)) 118 119 httpLineReply input = httpScanLine input [] 120 httpBadRequest = err 400 "Bad Request\n" 121 122 -- Unlike the old pair-only helper, this Result distinguishes a blank CRLF 123 -- line from truncated/malformed input. Both callers propagate the failure. 124 readLineBytes input = (parserMatchReply 125 (_ _ _ _ : httpBadRequest) 126 (line rest _ _ : ok line rest) 127 (httpLineReply input)) 128 129 -- The finite request line is already framed by readLineBytes. Deliberately 130 -- retain the historical three-fields grammar: empty fields are permitted, 131 -- but a third separating space is an error. The parser reply exposes byte 132 -- consumption to new clients, while parseThreeWords preserves HTTP's public 133 -- Result/400 boundary and the original "Bad Request" remainder. 134 httpNonSpace? byte = not? (equal? byte 32) 135 136 httpThreeWordsReply = (parserContext "request-line" (do parserBind 137 method <- parserTakeWhile httpNonSpace? 138 parserExpect 32 139 target <- parserTakeWhile httpNonSpace? 140 parserExpect 32 141 version <- parserTakeWhile httpNonSpace? 142 parserEof 143 parserPure (pair method (pair target version)))) 144 145 parseThreeWords = (bs : 146 parserMatchReply 147 (diagnostic rest consumed committed : err 400 "Bad Request\n") 148 (words rest consumed committed : ok words rest) 149 (httpThreeWordsReply bs)) 150 151 parseRequestLine input = case (readLineBytes input) of 152 ((t t), (line, rest)) = case (parseThreeWords line) of 153 ((t t), (request, _)) = ok request rest 154 _ = httpBadRequest 155 _ = httpBadRequest 156 157 -- --------------------------------------------------------------------------- 158 -- Header parsing 159 -- --------------------------------------------------------------------------- 160 161 -- Canonical byte input (0..255), as supplied by the socket/byte codecs. 162 -- Historical malformed numeral/bit behavior is intentionally not a contract. 163 toLowerAsciiByte byte = case (Nat.inRange byte 65 90) of 164 ^true = Nat.add byte 32 165 _ = byte 166 167 -- RFC 9110 token names, OWS, and field-value bytes. obs-text (128..255) 168 -- stays opaque; only the ASCII header name is lowercased. Reject obs-fold. 169 httpTokenByte? byte = (or? (Nat.letter byte) 170 (or? (Nat.digit byte) (any? (equal? byte) "!#$%&'*+-.^_`|~"))) 171 httpOws? byte = or? (equal? byte 32) (equal? byte 9) 172 httpFieldByte? byte = (or? (equal? byte 9) 173 (or? (Nat.printable byte) (Nat.inRange byte 128 255))) 174 httpTrimOws value = reverse (dropWhile httpOws? (reverse (dropWhile httpOws? value))) 175 176 -- Parse exactly one finite line, excluding CRLF. Preserve parser diagnostics 177 -- and consumption, but never accept a valid prefix followed by invalid bytes. 178 httpHeaderLineReply = (parserContext "header-line" (do parserBind 179 name <- parserLabel "header-name" (parserSome (parserSatisfy httpTokenByte?)) 180 parserLabel "colon" (parserExpect 58) 181 value <- parserLabel "header-value" (parserBefore (parserTakeWhile httpFieldByte?) parserEof) 182 parserPure (pair (map toLowerAsciiByte name) (httpTrimOws value)))) 183 184 -- Only an actual empty CRLF line ends the headers. The returned suffix is 185 -- opaque body data, even if it contains CR, LF, NUL or header-looking bytes. 186 httpParseHeaderLines input reversedHeaders = case (readLineBytes input) of 187 ((t t), ([], rest)) = ok (reverse reversedHeaders) rest 188 ((t t), (line, rest)) = case (httpHeaderLineReply line) of 189 ((t t), (header, _)) = httpParseHeaderLines rest (pair header reversedHeaders) 190 _ = httpBadRequest 191 _ = httpBadRequest 192 193 parseHeaders input = httpParseHeaderLines input [] 194 195 -- --------------------------------------------------------------------------- 196 -- Content-Length parsing 197 -- --------------------------------------------------------------------------- 198 199 -- The accumulator never exceeds maxBodyBytes. A single checked step can 200 -- reach at most 10 * maxBodyBytes + 9; after that, validate digits without 201 -- constructing a larger number. Trailing junk still means 400, not 413. 202 httpBodyTooLarge = err 413 "Request body too large\n" 203 204 httpLengthOverflow [] = httpBodyTooLarge 205 httpLengthOverflow [byte | rest] = (let 206 continue ^true = httpLengthOverflow rest 207 continue _ = httpBadRequest 208 in continue (Nat.digit byte)) 209 httpLengthOverflow _ = httpBadRequest 210 211 httpLengthDigits [] value = ok (just value) t 212 httpLengthDigits [byte | rest] value = (let 213 digit ^true = (let 214 next = Nat.decimal value (Nat.subtract byte 48) 215 bounded ^true = httpLengthDigits rest next 216 bounded _ = httpLengthOverflow rest 217 in bounded (Nat.lte next maxBodyBytes)) 218 digit _ = httpBadRequest 219 in digit (Nat.digit byte)) 220 httpLengthDigits _ _ = httpBadRequest 221 222 -- Input is a finite canonical byte list, with no OWS: parseHeaders already 223 -- trims field edges. Empty strings, signs, commas and interior whitespace fail. 224 parseContentLengthValue input{[_ | _]} = httpLengthDigits input 0 225 parseContentLengthValue _ = httpBadRequest 226 227 -- Input names are normalized by parseHeaders. Select the sole raw length 228 -- before decoding: duplicate fields and unsupported transfer coding are 400 229 -- regardless of field order or whether a length would otherwise exceed limits. 230 -- This server supports Content-Length framing only, not chunked decoding. 231 httpSelectLength [] t = ok nothing t 232 httpSelectLength [] (t value) = parseContentLengthValue value 233 httpSelectLength [("transfer-encoding", _) | _] _ = httpBadRequest 234 httpSelectLength [("content-length", value) | rest] t = httpSelectLength rest (just value) 235 httpSelectLength [("content-length", _) | _] _ = httpBadRequest 236 httpSelectLength [(_, _) | rest] selected = httpSelectLength rest selected 237 httpSelectLength _ _ = httpBadRequest 238 239 contentLength headers = httpSelectLength headers nothing 240 241 -- --------------------------------------------------------------------------- 242 -- Body reading 243 -- --------------------------------------------------------------------------- 244 245 bodyReadState remaining reversed rest = pair remaining (pair reversed rest) 246 247 -- State is (remaining, (reversed body, unused input)); zero consumes nothing. 248 -- remaining is a canonical natural supplied by the bounded length decoder. 249 takeBodyBytes bytes 0 reversed = bodyReadState 0 reversed bytes 250 -- The zero equation above excludes underflow. Specialized predecessor avoids 251 -- a full-width comparison/subtraction per byte of a canonical body counter. 252 takeBodyBytes [byte | rest] remaining reversed = takeBodyBytes rest (Nat.predecessor remaining) (pair byte reversed) 253 takeBodyBytes _ remaining reversed = bodyReadState remaining reversed [] 254 255 -- Retain the existing receive-size buckets, expressed as native comparisons 256 -- rather than bit shifts. Zero is handled before asking for another chunk. 257 httpRecvBucket remaining [size | rest] = (let 258 choose ^true = size 259 choose _ = httpRecvBucket remaining rest 260 in choose (Nat.gte remaining size)) 261 httpRecvBucket _ _ = 1 262 263 recvChunkMax4096 remaining = httpRecvBucket remaining [4096 1024 256 64 16] 264 265 -- --------------------------------------------------------------------------- 266 -- Request validation 267 -- --------------------------------------------------------------------------- 268 269 validMethod? "GET" = true 270 validMethod? "POST" = true 271 validMethod? "HEAD" = true 272 validMethod? _ = false 273 274 validVersion? "HTTP/1.1" = true 275 validVersion? "HTTP/1.0" = true 276 validVersion? _ = false 277 278 validTarget? [47 | _] = true 279 validTarget? _ = false 280 281 -- Keep error precedence: method, version, then target. Headers are validated 282 -- separately; accepting them here does not select body framing. 283 validateRequest method target version _ = (let 284 targetChecked ^true = ok t t 285 targetChecked _ = httpBadRequest 286 versionChecked ^true = targetChecked (validTarget? target) 287 versionChecked _ = err 505 "HTTP Version Not Supported\n" 288 methodChecked ^true = versionChecked (validVersion? version) 289 methodChecked _ = httpBadRequest 290 in methodChecked (validMethod? method)) 291 292 -- --------------------------------------------------------------------------- 293 -- Handler pipeline 294 -- --------------------------------------------------------------------------- 295 296 routerMethod "HEAD" = "GET" 297 routerMethod method = method