feat: fix problems with the parser

Http/Data/Headers.lean

@@ -26,3 +26,6 @@ def Headers.add (headers : Headers) (name : String) (value : String) : Headers :
 
 def Headers.with (name: String) (value: String) (headers: Headers) : Headers :=
   headers.add name value
+
+def Headers.contains (name: String) (headers: Headers) : Bool :=
+  headers.headers.contains name

Http/IO/Connection.lean

@@ -5,6 +5,8 @@ import LibUV
 
 namespace Http.IO.Connection
 
+-- Recipients of an invalid request-line SHOULD respond with either a 400 (Bad Request)
+
 open Http.Data
 
 -- ASYNC IO Component
@@ -18,103 +20,125 @@ def IO.toUVIO (act: IO α) : UV.IO α := IO.toEIO (λx => UV.Error.user x.toStri
 
 -- Parsed
 
-structure AccURI where
-  uri : Http.Data.Uri
-  deriving Inhabited, Repr
-
 structure Accumulate where
   contentLength : Option UInt64
   prop : String
   value : String
   req: Request
-  uri: URI.Parser.Data AccURI
+  hasHost : Bool
+  uri: URI.Parser.Data Http.Data.Uri
 
-def Accumulate.empty (uri: URI.Parser.Data AccURI) : Accumulate :=
+structure Connection where
+  version : Version
+
+def Accumulate.empty (uri: URI.Parser.Data Http.Data.Uri) : Accumulate :=
   { req := Request.empty
   , contentLength := none
   , prop := ""
   , value := ""
+  , hasHost := false
   , uri }
 
-def toStr (func: String → α → IO (α × Int)) (st: Nat) (en: Nat) (bt: ByteArray) (data: α) : IO (α × Int) :=
+def toStr (func: String → α → IO (α × Nat)) (st: Nat) (en: Nat) (bt: ByteArray) (data: α) : IO (α × Nat) :=
   func (String.fromUTF8! (bt.extract st en)) data
 
-def toBS (func: ByteArray → α → IO (α × Int)) (st: Nat) (en: Nat) (bt: ByteArray) (data: α) : IO (α × Int) :=
+def toBS (func: ByteArray → α → IO (α × Nat)) (st: Nat) (en: Nat) (bt: ByteArray) (data: α) : IO (α × Nat) :=
   func (bt.extract st en) data
 
-def noop : Nat -> Nat -> ByteArray -> α -> IO (α × Int) := λ_ _ _ a => pure (a, 0)
+def noop : Nat -> Nat -> ByteArray -> α -> IO (α × Nat) := λ_ _ _ a => pure (a, 0)
 
 def appendOr (data: Option String) (str: String) : Option String :=
   match data with
   | some res => some $ res.append str
   | none => some str
 
-def uriParser : UV.IO (URI.Parser.Data AccURI) := do
-  IO.toUVIO $
-    URI.Parser.create
-      (on_path := toStr (λval acc => pure ({acc with uri := {acc.uri with path := appendOr acc.uri.path val }}, 0)))
-      (on_port := toStr (λval acc => pure ({acc with uri := {acc.uri with port := appendOr acc.uri.port val }}, 0)))
-      (on_schema := toStr (λval acc => pure ({acc with uri := {acc.uri with scheme := appendOr acc.uri.scheme val }}, 0)))
-      (on_host := toStr (λval acc => pure ({acc with uri := {acc.uri with authority := appendOr acc.uri.authority val }}, 0)))
-      (on_query := toStr (λval acc => pure ({acc with uri := {acc.uri with query := appendOr acc.uri.query val }}, 0)))
-      (on_fragment := toStr (λval acc => pure ({acc with uri := {acc.uri with fragment := appendOr acc.uri.fragment val }}, 0)))
-      Inhabited.default
-
-def on_url (str: ByteArray) (data: Accumulate) : IO (Accumulate × Int) := do
+def uriParser : (URI.Parser.Data Http.Data.Uri) :=
+  URI.Parser.create
+    (on_path := toStr (λval acc => pure ({acc with path := appendOr acc.path val }, 0)))
+    (on_port := toStr (λval acc => pure ({acc with port := appendOr acc.port val }, 0)))
+    (on_schema := toStr (λval acc => pure ({acc with scheme := appendOr acc.scheme val }, 0)))
+    (on_host := toStr (λval acc => pure ({acc with authority := appendOr acc.authority val }, 0)))
+    (on_query := toStr (λval acc => pure ({acc with query := appendOr acc.query val }, 0)))
+    (on_fragment := toStr (λval acc => pure ({acc with fragment := appendOr acc.fragment val }, 0)))
+    Inhabited.default
+
+def onUrl (str: ByteArray) (data: Accumulate) : IO (Accumulate × Nat) := do
   let uri ← URI.Parser.parse data.uri str
   pure ({ data with uri }, 0)
 
-def end_url (data: Accumulate) : IO (Accumulate × Int) := do
-  let uriParser ← UV.IO.run uriParser
-  let uri := data.uri.data.uri
+def endUrl (data: Accumulate) : IO (Accumulate × Nat) := do
+  let uriParser := uriParser
+  let uri := data.uri.info
   pure ({ data with uri := uriParser, req := {data.req with uri } }, 0)
 
-def end_field (data: Accumulate) : IO (Accumulate × Int) := do
-  pure ({ data with req := {data.req with headers := data.req.headers.add data.prop data.value }, prop := "", value := ""}, 0)
+def endField (data: Accumulate) : IO (Accumulate × Nat) := do
+  let prop := data.prop.toLower
+  let value := data.value
 
-def end_prop (data: Accumulate) : IO (Accumulate × Int) := do
-  pure (data, if data.prop.toLower == "content-length" then 1 else 0)
+  let (data, code) :=
+    match prop with
+    | "host" =>
+      if !data.hasHost then
+        let data := {data with hasHost := true }
+        (data, (data.uri.info.authority.map (· != value)).getD true)
+      else
+        (data, false)
+    | _ => (data, true)
 
-def on_body (fn: Request → IO Unit) (body: String) (acc: Accumulate) : IO (Accumulate × Int) := do
+  let req :=  {data.req with headers := data.req.headers.add prop value}
+  pure ({ data with req, prop := "", value := ""}, if code then 0 else 1)
 
+def endProp (data: Accumulate) : IO (Accumulate × Nat) := do
+  pure (data, if data.prop.toLower == "content-length" then 1 else 0)
+
+def onBody (fn: Request → IO Unit) (body: String) (acc: Accumulate) : IO (Accumulate × Nat) := do
   fn {acc.req with body};
   pure (acc, 0)
 
-def requestParser (fn: Request → IO Unit) : UV.IO (Parser.Data Accumulate) := do
-  IO.toUVIO $
+def onRequestLine (method: Nat) (major: Nat) (minor: Nat) (acc: Accumulate) : IO (Accumulate × Nat) := do
+  let acc := {acc with req := {acc.req with version := Version.mk major minor, method := (Method.fromNumber method).get!}}
+  return (acc, 0)
+
+def requestParser (fn: Request → IO Unit) : Parser.Data Accumulate :=
     Parser.create
       (on_reasonPhrase := noop)
-      (on_url := toBS on_url)
-      (on_body := toStr (on_body fn))
+      (on_url := toBS onUrl)
+      (on_body := toStr (onBody fn))
       (on_prop := toStr (λval acc => pure ({acc with prop := acc.prop.append val}, 0)))
       (on_value := toStr (λval acc => pure ({acc with value := acc.value.append val}, 0)))
-      (on_endProp := end_prop)
-      (on_endUrl := end_url)
-      (on_endField := end_field)
-      (on_endRequestLine := λacc method major minor => pure ({acc with req := {acc.req with version := Version.mk major minor, method := (Method.fromNumber method).get!}}, 0))
-      (Accumulate.empty (← uriParser))
+      (on_endProp := endProp)
+      (on_endUrl := endUrl)
+      (on_endField := endField)
+      (on_endRequestLine := onRequestLine)
+      (on_endHeaders := λacc => pure (acc, if acc.hasHost then 0 else 1))
+      (Accumulate.empty (uriParser))
 
 def parse (data: Parser.Data Accumulate) (arr: ByteArray) : UV.IO (Parser.Data Accumulate) :=
    IO.toUVIO $ Parser.parse data arr
 
 -- Socket
 
-def readSocket (socket: UV.TCP) (on_eof: UV.IO Unit) (fn: Request → UV.IO Response) : UV.IO Unit := do
-  let data ← requestParser $ λreq => UV.IO.run $ do
+def readSocket (socket: UV.TCP) (on_error: UV.IO Unit) (fn: Request → UV.IO Response) : UV.IO Unit := do
+  let data := requestParser $ λreq => UV.IO.run $ do
     let resp ← fn req
     let _ ← socket.write #[(ToString.toString resp).toUTF8] (λ_ => pure ())
 
   let ref ← IO.toUVIO (IO.mkRef data)
+
   socket.read_start fun
     | .error _ => do
       socket.read_stop
       socket.stop
-    | .eof => do
-      on_eof
+    | .eof => pure ()
     | .ok bytes => do
+      UV.log s!"ok '{String.fromUTF8! bytes}'"
       let data ← ref.get
       let res ← parse data bytes
       ref.set res
+      if res.error == 1 then
+        let response := Response.mk (Version.v11) (Status.badRequest) "BAD REQUEST" Headers.empty ""
+        let _ ← socket.write #[(ToString.toString response).toUTF8] (λ_ => pure ())
+        on_error
 
 def server (host: String) (port: UInt16) (fn: Request → UV.IO Response) (timeout : UInt64 := 10000) : IO Unit := do
   let go : UV.IO Unit := do
@@ -125,9 +149,10 @@ def server (host: String) (port: UInt16) (fn: Request → UV.IO Response) (timeo
     server.listen 128 do
       let client ← loop.mkTCP
       server.accept client
-      let timer ← loop.mkTimer
-      let onEOF := do timer.stop
-      timer.start timeout (timeout * 2) do onEOF
+      let onEOF := do
+        client.read_stop
+        client.stop
       readSocket client onEOF fn
-    let _ ← loop.run
+    let still ← loop.run
+    UV.log s!"res {still}"
   UV.IO.run go

Http/Parser.lean

@@ -6,10 +6,11 @@ namespace Http
 open Parse.DSL
 
 /-!
-  HTTP Parser based on https://httpwg.org/specs/rfc9112.html
+  HTTP Message Parser based on https://httpwg.org/specs/rfc9112.html.
+  - We do not replace CR with SP before processing
 -/
 
-parser Parser where
+parser Parser in C where
   def type : u8
   def method : u8
   def statusCode : u16
@@ -30,12 +31,15 @@ parser Parser where
   callback endProp
   callback endUrl
   callback endField
+  callback endHeaders
   callback endRequestLine : method major minor
 
+  -- Defines if its a `request-line` or `status-line`, this parser is used for both request and response.
   node statusLine where
     peek 'H' (call (store type 0) httpVersionStart)
     otherwise (call (store type 1) method)
 
+  -- The start of the `request-line` defined in https://httpwg.org/specs/rfc9112.html#request.line
   node method where
     switch (store method beforeUrl)
       | "HEAD" => 0
@@ -50,9 +54,9 @@ parser Parser where
     otherwise (error 2)
 
     node beforeUrl where
-      is " " beforeUrl
-      otherwise (start url url)
+      is " " (start url url)
 
+    -- The start of the `request-target` defined in https://httpwg.org/specs/rfc9112.html#request.target
     node url where
       peek ' ' (end url (call endUrl endUrl))
       any url
@@ -100,12 +104,22 @@ parser Parser where
       any reasonPhrase
 
     node lineAlmostDone where
-      is "\r\n" (call endRequestLine fieldLineStart)
+      is "\r\n" requestLine
+
+    node requestLine where
+      select endRequestLine
+        | 0 => fieldLineStart
+        default => error 1
 
     node fieldLineStart where
-      peek '\r' endMessage
+      peek '\r' endHeaders
       otherwise (start prop fieldLineProp)
 
+    node endHeaders where
+      select endHeaders
+        | 0 => endMessage
+        default => error 1
+
     node fieldLineProp where
       peek ':' (end prop (call (callStore endProp isCL) fieldLineColon))
       any fieldLineProp
@@ -124,13 +138,18 @@ parser Parser where
         default => error 0
 
     node contentLength where
-      peek '\r' (end value fieldLineEnd)
+      peek '\r' (end value selectLineEnd)
       is digit (call (mulAdd contentLength) contentLength)
 
     node fieldLineValue where
-      peek '\r' (end value (call endField fieldLineEnd))
+      peek '\r' (end value selectLineEnd)
       any fieldLineValue
 
+    node selectLineEnd where
+      select endField
+        | 0 => fieldLineEnd
+        default => error 1
+
     node fieldLineEnd where
       is "\r\n" fieldLineStart
 

Http/URI/Parser.lean

@@ -9,7 +9,7 @@ namespace Http.URI
 
 open Parse.DSL
 
-parser Parser where
+parser Parser in C where
   def path : span
   def port : span
   def schema : span
@@ -58,7 +58,7 @@ parser Parser where
   node server where
     is "?" (end host queryStart)
     peek '/' (end host (start path path))
-    peek ':' (end host beforePort)
+    peek ':' beforePort
     is userinfo_chars server
     is ["[" "]"] server
     is "@" serverWithAt
@@ -68,7 +68,7 @@ parser Parser where
 
   node port where
     is digit port
-    otherwise (end port afterPort)
+    otherwise (end port (end host afterPort))
 
   node afterPort where
     is "?" queryStart
@@ -77,7 +77,7 @@ parser Parser where
   node serverWithAt where
     is "?" (end host queryStart)
     peek '/' (end host (start path path))
-    peek ':' (end host (start port port))
+    peek ':' (start port port)
     is userinfo_chars serverWithAt
     is ["[" "]"] serverWithAt
     is "@" (error 3)

lake-manifest.json

@@ -19,10 +19,10 @@
   {"url": "https://github.com/algebraic-sofia/lean-libuv.git",
    "type": "git",
    "subDir": null,
-   "rev": "cfd5b66fc6c1ab0eaa4836a83ff71313cb2e9301",
+   "rev": "b7fa34c8fed5bd9511748b6d6de2e3097b55949f",
    "name": "LibUV",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "socket-fix",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Http",

lakefile.lean

@@ -7,7 +7,6 @@ module_data alloy.c.o.export : BuildJob FilePath
 module_data alloy.c.o.noexport : BuildJob FilePath
 
 open Lean
-
 lean_lib Http where
   precompileModules := true
   nativeFacets := fun shouldExport =>
@@ -17,5 +16,5 @@ lean_lib Http where
       #[Module.oNoExportFacet, `alloy.c.o.noexport]
 
 require alloy from git "https://github.com/tydeu/lean4-alloy.git"
-require Parse from git "https://github.com/axiomed/Parse.lean.git"
-require LibUV from git "https://github.com/algebraic-sofia/lean-libuv.git"
+require Parse from "../lean-parse"
+require LibUV from git "https://github.com/algebraic-sofia/lean-libuv.git" @ "socket-fix"