From ef97390a8bab40e0d5b8e07d0001baad81fc9938 Mon Sep 17 00:00:00 2001 From: xenia Date: Thu, 7 Sep 2023 23:39:39 +0200 Subject: [PATCH] Parse the request line properly --- src/Base.agda | 13 ++++- src/Main.agda | 4 +- src/NonEmpty.agda | 7 +++ src/Parse-HTTP.agda | 111 ++++++++++++++++++++++++------------ src/Parse-HTTP/Helpers.agda | 17 +++++- src/Parse-HTTP/Test.agda | 27 +++++---- src/Parse-HTTP/URL.agda | 29 +++++++--- src/Parsing.agda | 20 +++++++ 8 files changed, 167 insertions(+), 61 deletions(-) diff --git a/src/Base.agda b/src/Base.agda index e56bb90..b4c0b13 100644 --- a/src/Base.agda +++ b/src/Base.agda @@ -26,6 +26,11 @@ record Monad (M : Type → Type) : Type₁ where _<$>_ : {A B : Type} → (A → B) → M A → M B f <$> x = x >>= (λ a → pure (f a)) + infixl 5 _>>=_ + infixl 5 _>>_ + infixr 4 _<$>_ + + open Monad ⦃...⦄ public data Maybe (A : Type) : Type where @@ -38,7 +43,7 @@ _or-else_ : {A : Type} → Maybe A → A → A (real x) or-else _ = x cake or-else x = x -infix 10 _or-else_ +infix 1 _or-else_ is-real : {A : Type} → Maybe A → Type is-real cake = ⊥ @@ -78,6 +83,12 @@ instance EqMaybe ._==_ (real _) cake = false EqMaybe ._==_ cake (real _) = false + EqList : {T : Type} → ⦃ Eq T ⦄ → Eq (List T) + EqList ._==_ [] [] = true + EqList ._==_ (x ∷ xs) (y ∷ ys) = x == y ∧ xs == ys + EqList ._==_ (_ ∷ _) [] = false + EqList ._==_ [] (_ ∷ _) = false + record Show (T : Type) : Type₁ where field show : T → String.String diff --git a/src/Main.agda b/src/Main.agda index d1087b5..8e41683 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -73,7 +73,7 @@ module Pages where < p > "welcome to the " , < span & style ＝ "color: white;" > "index" , - ((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" ) <$> query or-else L.[]) + (((λ q → < span & style ＝ "color: fuchsia;" > " (query = " , q , ")" ) <$> query) or-else L.[]) @@ -104,7 +104,7 @@ handle sock = do (do putStrLn "handle: got request" putStrLn (" method = " S.++ show (req .method)) - putStrLn (" target .path = " S.++ show (req .target .path) S.++ (λ q → ", target .query = " S.++ show q) <$> (req .target .query) or-else "") + putStrLn (" target = " S.++ show (req .target)) putStrLn (" version = " S.++ show (req .version)) putStrLn (" headers = " S.++ show (req .headers)) case req .content of λ where diff --git a/src/NonEmpty.agda b/src/NonEmpty.agda index c2a583a..bad9e67 100644 --- a/src/NonEmpty.agda +++ b/src/NonEmpty.agda @@ -3,6 +3,7 @@ open import Agda.Primitive renaming (Set to Type) open import Data.Product open import Data.Nat open import Data.List using (List; []; _∷_) +open import Data.Bool import Data.Vec as V open import Base @@ -40,3 +41,9 @@ instance ShowList⁺ .show x = show (list⁺-to-list x) String.++ "⁺" where import Data.String as String + + EqList⁺ : {T : Type} → ⦃ Eq T ⦄ → Eq (List⁺ T) + EqList⁺ ._==_ [ x ]⁺ [ y ]⁺ = x == y + EqList⁺ ._==_ (x ∷⁺ xs) (y ∷⁺ ys) = x == y ∧ xs == ys + EqList⁺ ._==_ (_ ∷⁺ _) [ _ ]⁺ = false + EqList⁺ ._==_ [ _ ]⁺ (_ ∷⁺ _) = false diff --git a/src/Parse-HTTP.agda b/src/Parse-HTTP.agda index 1869ae5..b7f46d1 100644 --- a/src/Parse-HTTP.agda +++ b/src/Parse-HTTP.agda @@ -1,6 +1,8 @@ +{-# OPTIONS --allow-unsolved-metas #-} + open import Agda.Primitive renaming (Set to Type) -open import Data.Vec renaming (map to mapᵥ) hiding ([_]; foldr; foldl) +open import Data.Vec renaming (map to mapᵥ) hiding ([_]; foldr; foldl; _>>=_) import Data.List as List open import Data.Nat open import Data.Nat.Properties using (<ᵇ⇒<) @@ -32,7 +34,6 @@ private module Parse-URL where open import Parse-HTTP.URL - -- commonly used sub-parsers private gen-delims sub-delims reserved unreserved : [ Parser Byte ] @@ -54,11 +55,16 @@ module Parse-URL where reg-name = decode-utf8⁺ <$?>′ (many (unreserved <|>′ percent-encoded <|>′ sub-delims)) unchecked : [ Parser Authority ] - unchecked = (λ (host , rest) → host ꞉ (proj₂ <$> rest or-else 80)) - <$>′ (reg-name <&?>′ enbox (any-of ":" <&>′ enbox number)) + unchecked = (λ (host , rest) → host ꞉ ((proj₂ <$> rest) or-else 80)) + <$>′ (reg-name <&?>□ any-of ":" <&>□ number) parse-path : [ Parser Path ] - parse-path = foldr (λ (slash , seg) path → seg / path) $ <$>′ (many (any-of "/" <&>′ enbox segment)) + parse-path = + List.foldr (λ (slash , seg) path → seg / path) $ <$>′ + ( + (list⁺-to-list <$>′ many (any-of "/" <&>′ enbox segment)) + <|>′ ((λ _ → List.[]) <$>′ any-of "/") + ) where segment : [ Parser String.String ] segment = decode-utf8⁺ <$?>′ many pchar @@ -67,34 +73,24 @@ module Parse-URL where parse-query = decode-utf8⁺ <$?>′ many (pchar <|>′ any-of "/?") parse-fragment = parse-query - record RequestTarget : Type where - field - path : Path - query : Maybe String.String - open RequestTarget public - - parse-request-target : [ Parser RequestTarget ] - parse-request-target = (λ (path , mquery) → record { path = path ; query = mquery }) <$>′ (parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)) + parse-absolute-url : [ Parser (Authority × Path) ] + parse-absolute-url = + (parse-scheme >?=′ (_== "http")) + <&⃗>□ exact (string-to-ascii-vec "://") + <&⃗>□ parse-authority + <&>□ parse-path parse-url : [ Parser URL ] - parse-url = enurl <$?>′ parse-parts - where - enurl : String.String × Authority × (Path × Maybe String.String) × Maybe String.String → Maybe URL - enurl (scheme , auth , (path , mquery) , mfrag) = - if true -- scheme == "http" - then real (http:// auth / path ¿ mquery # mfrag) - else cake + parse-url = + parse-absolute-url + <&?>□ (any-of "?" <&⃗>□ parse-query) + >$=′ λ ((auth , path) , mquery) → http:// auth / path ¿ mquery - parse-parts : [ Parser (String.String × Authority × (Path × Maybe String.String) × Maybe String.String) ] - parse-parts = - parse-scheme - <&>□ (any-of ":" <&>□ repeat 2 (any-of "/")) - <&⃗>□ parse-authority - <&>□ (parse-path <&?>□ (any-of "?" <&⃗>□ parse-query)) - <&?>□ (any-of "#" <&⃗>□ parse-fragment) open Parse-URL public module Parse-Header where + open import Parse-HTTP.URL using (Authority) + record Header : Type where field name : List⁺ Byte @@ -105,12 +101,22 @@ module Parse-Header where ShowHeader : Show Header ShowHeader .show hdr = show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .name)) String.++ ": " String.++ show ⦃ ShowByteList ⦄ (list⁺-to-list (hdr .value)) + get-field : List⁺ Byte → List.List Header → Maybe (List⁺ Byte) + get-field field-name List.[] = cake + get-field field-name (hdr List.∷ rest) = + if hdr .name == field-name + then real (hdr .value) + else get-field field-name rest + content-length : List.List Header → Maybe ℕ - content-length List.[] = cake - content-length (hdr List.∷ rest) = - if decode-utf8⁺ (hdr .name) == real "Content-Length" - then (λ x → x .result) <$> (number .parse (proj₂ (list⁺-to-vec (hdr .value)))) - else content-length rest + content-length headers = + get-field (string-to-ascii-list⁺ "Content-Length") headers + >>= parse-list⁺ number + + host : List.List Header → Maybe Authority + host headers = + get-field (string-to-ascii-list⁺ "Host") headers + >>= parse-list⁺ parse-authority private parse-vchar-sp : [ Parser Byte ] @@ -141,6 +147,32 @@ module Parse-Header where open Parse-Header public module Parse-Request where + open import Parse-HTTP.URL + + data RequestTargetPath : Type where + OriginForm : Path → RequestTargetPath + AbsoluteForm : Authority → Path → RequestTargetPath + -- We do not care about authority-form nor asterisk form as we don't do any CONNECT nor OPTIONS requests + + record RequestTarget : Type where + field + path : RequestTargetPath + query : Maybe String.String + open RequestTarget public + + parse-request-target : [ Parser RequestTarget ] + parse-request-target = + (parse-origin-form <|>′ parse-absolute-form) <&?>□ (any-of "?" <&⃗>□ parse-query) + >$=′ λ (path , query) → record { path = path; query = query } + where + parse-origin-form parse-absolute-form : [ Parser RequestTargetPath ] + parse-origin-form = + parse-path >$=′ OriginForm + + parse-absolute-form = + parse-absolute-url >$=′ λ (auth , path) → AbsoluteForm auth path + + data HTTP-Version : Type where HTTP11 : HTTP-Version -- we only support 1.1 @@ -149,8 +181,7 @@ module Parse-Request where ShowHTTP-Version .show HTTP11 = "HTTP/1.1" parse-http-version : [ Parser HTTP-Version ] - parse-http-version = (λ _ → HTTP11) <$>′ exact (string-to-ascii "HTTP/1.1") - + parse-http-version = (λ _ → HTTP11) <$>′ exact (string-to-ascii-vec "HTTP/1.1") parse-specific-http-method : HTTP-Method → [ Parser HTTP-Method ] parse-specific-http-method m = (λ _ → m) <$>′ exact (proj₂ (list⁺-to-vec (name-of-method m))) @@ -176,7 +207,7 @@ module Parse-Request where record Request : Type where field method : HTTP-Method - target : RequestTarget + target : URL version : HTTP-Version headers : List.List Header content : Maybe (List.List Byte) @@ -184,7 +215,8 @@ module Parse-Request where parse-request : [ Parser Request ] parse-request = ((parse-request-line <&⃖>□ crlf) <&>□ many (parse-header <&⃖>□ crlf)) - >>=′ λ ((method , target , version) , headers) → enbox ( + >$?=′ find-target + >>=′ λ (method , target , version , headers) → enbox ( case content-length (list⁺-to-list headers) of λ where cake → ( @@ -202,5 +234,12 @@ module Parse-Request where <$>′ (crlf <&⃗>□ (repeat n any₁)) ) ) + where + find-target : ((HTTP-Method × RequestTarget × HTTP-Version) × List⁺ Header) → Maybe (HTTP-Method × URL × HTTP-Version × List⁺ Header) + find-target ((method , record { path = OriginForm path ; query = query } , ver) , headers) = + Parse-Header.host (list⁺-to-list headers) >>= λ auth → + real (method , (http:// auth / path ¿ query) , ver , headers) + find-target ((method , record { path = AbsoluteForm auth path ; query = query } , ver) , headers) = + real (method , (http:// auth / path ¿ query) , ver , headers) open Parse-Request public diff --git a/src/Parse-HTTP/Helpers.agda b/src/Parse-HTTP/Helpers.agda index 6069f7d..88f59e0 100644 --- a/src/Parse-HTTP/Helpers.agda +++ b/src/Parse-HTTP/Helpers.agda @@ -7,6 +7,8 @@ open import Data.Vec hiding ([_]; foldl) import Data.List as List open import Data.Product +open import Relation.Binary.PropositionalEquality hiding ([_]) + import Data.String as String import Data.Char as Char @@ -35,13 +37,24 @@ list-is-ascii (c List.∷ chs) = (Char.toℕ c <ᵇ 128) ∧ list-is-ascii chs string-is-ascii : String.String → Type string-is-ascii x = T (list-is-ascii (String.toList x)) -string-to-ascii : (s : String.String) → {string-is-ascii s} → Vec Byte (String.length s) -string-to-ascii x {prf} = go (String.toList x) +string-to-ascii-vec : (s : String.String) → {string-is-ascii s} → Vec Byte (String.length s) +string-to-ascii-vec x {prf} = go (String.toList x) where go : (l : List.List Char.Char) → Vec Byte (List.length l) go List.[] = [] go (ch List.∷ chs) = mkClip (Char.toℕ ch) ∷ go chs +string-to-ascii-list⁺ : (s : String.String) → {string-is-ascii s} → {T (0 <ᵇ String.length s)} → List⁺ Byte +string-to-ascii-list⁺ s {ascii} {nonempty} = vec-to-list⁺ v + where + open import Data.Nat.Properties + + len≢0 : String.length s ≢ 0 + len≢0 = m′ any₁) <|>′ p) fail (String.toList x) diff --git a/src/Parse-HTTP/Test.agda b/src/Parse-HTTP/Test.agda index ec03dff..0aec247 100644 --- a/src/Parse-HTTP/Test.agda +++ b/src/Parse-HTTP/Test.agda @@ -75,32 +75,37 @@ module Test-HTTP where ≡ cake test-auth-port-out-of-range = refl - test-path₁ : parse-path .parse (enc "/mjau/cat.html?meowing=true") + test-path : parse-path .parse (enc "/mjau/cat.html?meowing=true") ≡ real ⟨ "mjau" / "cat.html" / $ , _ , enc "?meowing=true" ⟩ - test-path₁ = refl + test-path = refl - test-path₂ : parse-path .parse (enc "/%68%65%77%77%6f/%3f%5e%2f%2f%5e%3f?mjau") + test-path-encoded : parse-path .parse (enc "/%68%65%77%77%6f/%3f%5e%2f%2f%5e%3f?mjau") ≡ real ⟨ "hewwo" / "?^//^?" / $ , _ , enc "?mjau" ⟩ - test-path₂ = refl + test-path-encoded = refl - test-url : parse-url .parse (enc "http://www.rfc-editor.org/rfc/rfc3986.html#section-2.1") - ≡ real ⟨ http:// "www.rfc-editor.org" ꞉ 80 / ("rfc" / "rfc3986.html" / $) ¿ cake # real "section-2.1" , _ , enc "" ⟩ + test-path-bare : parse-path .parse (enc "/") + ≡ real ⟨ $ , _ , enc "" ⟩ + test-path-bare = refl + + test-url : parse-url .parse (enc "http://www.rfc-editor.org/rfc/rfc3986.html") + ≡ real ⟨ http:// "www.rfc-editor.org" ꞉ 80 / ("rfc" / "rfc3986.html" / $) ¿ cake , _ , enc "" ⟩ test-url = refl test-header : parse-header .parse (enc "Content-Length: 6\r\n") - ≡ real ⟨ record { name = vec-to-list⁺ (string-to-ascii "Content-Length") ; value = vec-to-list⁺ (string-to-ascii "6") } , _ , enc "\r\n" ⟩ + ≡ real ⟨ record { name = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-list⁺ "6" } , _ , enc "\r\n" ⟩ test-header = refl - test-request : parse-request .parse (enc "POST /site/index.html?mjau HTTP/1.1\r\nContent-Length: 6\r\n\r\nmjau:)\r\n") + test-request : parse-request .parse (enc "POST /site/index.html?mjau HTTP/1.1\r\nContent-Length: 6\r\nHost: agda.nu\r\n\r\nmjau:)\r\n") ≡ real ⟨ record { method = POST - ; target = record { path = "site" / "index.html" / $ ; query = real "mjau" } + ; target = http:// "agda.nu" ꞉ 80 / ("site" / "index.html" / $) ¿ real "mjau" ; version = HTTP11 ; headers = - record { name = vec-to-list⁺ (string-to-ascii "Content-Length") ; value = vec-to-list⁺ (string-to-ascii "6") } + record { name = string-to-ascii-list⁺ "Content-Length" ; value = string-to-ascii-list⁺ "6" } + List.∷ record { name = string-to-ascii-list⁺ "Host" ; value = string-to-ascii-list⁺ "agda.nu" } List.∷ List.[] - ; body = real (Vec.toList (string-to-ascii "mjau:)")) + ; content = real (list⁺-to-list (string-to-ascii-list⁺ "mjau:)")) } , _ , enc "\r\n" diff --git a/src/Parse-HTTP/URL.agda b/src/Parse-HTTP/URL.agda index cc6a55f..cf4fa64 100644 --- a/src/Parse-HTTP/URL.agda +++ b/src/Parse-HTTP/URL.agda @@ -1,6 +1,6 @@ open import Agda.Primitive renaming (Set to Type) -import Data.String as String +import Data.String as S open import Data.Nat open import Data.Bool @@ -10,23 +10,30 @@ module Parse-HTTP.URL where record Authority : Type where constructor _꞉_ field - host : String.String -- TODO: Split out IP:s as a separate type? + host : S.String -- TODO: Split out IP:s as a separate type? port : ℕ -- TODO: maybe include {port-in-range} : port < 2 ^ 16 open Authority public +instance + ShowAuthority : Show Authority + ShowAuthority .show x = + if x .port == 80 + then x .host + else x .host S.++ ":" S.++ show (x .port) + infix 10 _꞉_ data Path : Type where $ : Path -- end - _/_ : String.String → Path → Path + _/_ : S.String → Path → Path open Path public instance ShowPath : Show Path ShowPath .show $ = "(empty path)" ShowPath .show (p / $) = p - ShowPath .show (p / rest@(_ / _)) = p String.++ "/" String.++ show rest + ShowPath .show (p / rest@(_ / _)) = p S.++ "/" S.++ show rest EqPath : Eq Path EqPath ._==_ $ $ = true @@ -37,17 +44,21 @@ instance infixr 5 _/_ record URL : Type where - constructor http://_/_¿_#_ + constructor http://_/_¿_ field authority : Authority path : Path - query : Maybe String.String - fragment : Maybe String.String + query : Maybe S.String open URL public -infix 0 http://_/_¿_#_ +infix 0 http://_/_¿_ + +instance + ShowURL : Show URL + ShowURL .show url = + "http://" S.++ show (url .authority) S.++ "/" S.++ show (url .path) S.++ ((λ q → "?" S.++ q) <$> url .query or-else "") private sample-url : URL - sample-url = http:// "coral.shoes" ꞉ 80 / ("pages" / "index.html" / $) ¿ real "key=value" # cake + sample-url = http:// "coral.shoes" ꞉ 80 / ("pages" / "index.html" / $) ¿ real "key=value" diff --git a/src/Parsing.agda b/src/Parsing.agda index 8988df3..ac7f683 100644 --- a/src/Parsing.agda +++ b/src/Parsing.agda @@ -28,8 +28,17 @@ open Parse public record Parser (A : Type) (n : ℕ) : Type where field parse : Vec T n → Maybe (Parse A n) + open Parser public +parse-list⁺ : {A : Type} → [ Parser A ] → List⁺ T → Maybe A +parse-list⁺ p l = + p .parse (proj₂ (list⁺-to-vec l)) + >>= λ parse → + if parse .m == 0 + then pure (parse .result) + else cake + -- Parser combinators _<$>′_ : {A B : Type} → (A → B) → [ Parser A →′ Parser B ] (f <$>′ p) .parse a = do @@ -136,6 +145,17 @@ _>>=′_ : {A B : Type} → [ Parser A →′ ((k′ A) →′ □ Parser B) → _>>′_ : {A B : Type} → [ Parser A →′ □ Parser B →′ Parser B ] pa >>′ pb = pa >>=′ λ _ → pb +_>$=′_ : {A B : Type} → [ Parser A →′ k′ (A → B) →′ Parser B ] +pa >$=′ f = f <$>′ pa + +_>?=′_ : {A : Type} → [ Parser A →′ k′ (A → Bool) →′ Parser A ] +pa >?=′ f = f ′ pa + +_>$?=′_ : {A B : Type} → [ Parser A →′ k′ (A → Maybe B) →′ Parser B ] +pa >$?=′ f = f <$?>′ pa + +infixl 10 _>>=′_ _>>′_ _>$=′_ _>$?=′_ _>?=′_ + fail : {A : Type} → [ Parser A ] fail .parse _ = cake