[lsp] Abstract URI type, improve URI validation.

This should help preventing many issues that can happen due to bad
URIs; still quite a bit of work to do here, but the code overall,
while a bit uglier, seems safer.

Fixes #187

CHANGES.md

@@ -36,6 +36,9 @@
  - coq-lsp now understands a basic version of Coq Waterproof files
    (.wpn) Note that we don't associate to them by default, as to allow
    the waterproof extension to take over the files (@ejgallego, #306)
+ - URI validation is now more strict, and some further bugs should be
+   solved; note still this can be an issue on some client settings
+   (@ejgallego, #313, fixes #187)
 
 # coq-lsp 0.1.4: View
 ---------------------

controller/doc_manager.ml

@@ -39,13 +39,16 @@ module Handle = struct
     let ly, cy = y in
     lx > ly || (lx = ly && cx > cy)
 
-  let doc_table : (string, t) Hashtbl.t = Hashtbl.create 39
+  let doc_table : (Lang.LUri.File.t, t) Hashtbl.t = Hashtbl.create 39
 
   let create ~uri ~doc =
     (match Hashtbl.find_opt doc_table uri with
     | None -> ()
     | Some _ ->
-      LIO.trace "do_open" ("file " ^ uri ^ " not properly closed by client"));
+      LIO.trace "do_open"
+        ("file "
+        ^ Lang.LUri.File.to_string_uri uri
+        ^ " not properly closed by client"));
     Hashtbl.add doc_table uri
       { doc; cp_requests = Int.Set.empty; pt_requests = [] }
 
@@ -55,7 +58,8 @@ module Handle = struct
     match Hashtbl.find_opt doc_table uri with
     | Some h -> h
     | None ->
-      LIO.trace "DocHandle.find" ("file " ^ uri ^ " not available");
+      LIO.trace "DocHandle.find"
+        ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
       raise AbortRequest
 
   let find_opt ~uri = Hashtbl.find_opt doc_table uri
@@ -180,7 +184,8 @@ module Check = struct
       if completed ~doc then pending := None;
       requests
     | None ->
-      LIO.trace "Check.check" ("file " ^ uri ^ " not available");
+      LIO.trace "Check.check"
+        ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
       Int.Set.empty
 
   let maybe_check ~ofmt = Option.map (fun uri -> check ~ofmt ~uri) !pending
@@ -252,7 +257,8 @@ let create ~ofmt ~root_state ~workspace ~uri ~raw ~version =
 
 let change ~ofmt ~(doc : Fleche.Doc.t) ~version ~raw =
   let uri = doc.uri in
-  LIO.trace "bump file" (uri ^ " / version: " ^ string_of_int version);
+  LIO.trace "bump file"
+    (Lang.LUri.File.to_string_uri uri ^ " / version: " ^ string_of_int version);
   let tb = Unix.gettimeofday () in
   match Fleche.Doc.bump_version ~version ~raw doc with
   | Fleche.Contents.R.Error e ->
@@ -270,7 +276,8 @@ let change ~ofmt ~(doc : Fleche.Doc.t) ~version ~raw =
 let change ~ofmt ~uri ~version ~raw =
   match Handle.find_opt ~uri with
   | None ->
-    LIO.trace "DocHandle.find" ("file " ^ uri ^ " not available");
+    LIO.trace "DocHandle.find"
+      ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available");
     Int.Set.empty
   | Some { doc; _ } ->
     if version > doc.version then change ~ofmt ~doc ~version ~raw

controller/doc_manager.mli

@@ -27,31 +27,35 @@ val create :
      ofmt:Format.formatter
   -> root_state:Coq.State.t
   -> workspace:Coq.Workspace.t
-  -> uri:string
+  -> uri:Lang.LUri.File.t
   -> raw:string
   -> version:int
   -> unit
 
 (** Update a document, returns the list of not valid requests *)
 val change :
-  ofmt:Format.formatter -> uri:string -> version:int -> raw:string -> Int.Set.t
+     ofmt:Format.formatter
+  -> uri:Lang.LUri.File.t
+  -> version:int
+  -> raw:string
+  -> Int.Set.t
 
 (** Close a document *)
-val close : uri:string -> unit
+val close : uri:Lang.LUri.File.t -> unit
 
 exception AbortRequest
 
 (** [find_doc ~uri] , raises AbortRequest if [uri] is invalid *)
-val find_doc : uri:string -> Fleche.Doc.t
+val find_doc : uri:Lang.LUri.File.t -> Fleche.Doc.t
 
 (** Add a request to be served when the document is completed *)
-val add_on_completion : uri:string -> id:int -> unit
+val add_on_completion : uri:Lang.LUri.File.t -> id:int -> unit
 
-val remove_on_completion : uri:string -> id:int -> unit
+val remove_on_completion : uri:Lang.LUri.File.t -> id:int -> unit
 
 (** Add a request to be served when the document point data is available, for
     now, we allow a single request like that. Maybe returns the id of the
     previous request which should now be cancelled. *)
-val add_on_point : uri:string -> id:int -> point:int * int -> unit
+val add_on_point : uri:Lang.LUri.File.t -> id:int -> point:int * int -> unit
 
-val remove_on_point : uri:string -> id:int -> point:int * int -> unit
+val remove_on_point : uri:Lang.LUri.File.t -> id:int -> point:int * int -> unit

controller/lsp_core.ml

@@ -45,11 +45,11 @@ module LSP = Lsp.Base
 module PendingRequest = struct
   type t =
     | DocRequest of
-        { uri : string
+        { uri : Lang.LUri.File.t
         ; handler : Requests.document_request
         }
     | PosRequest of
-        { uri : string
+        { uri : Lang.LUri.File.t
         ; point : int * int
         ; handler : Requests.position_request
         }
@@ -159,6 +159,8 @@ let do_open ~state params =
     , int_field "version" document
     , string_field "text" document )
   in
+  (* XXX: fix this *)
+  let uri = Lang.LUri.(File.of_uri (of_string uri)) |> Result.get_ok in
   let root_state, workspace = State.(state.root_state, state.workspace) in
   Doc_manager.create ~root_state ~workspace ~uri ~raw ~version
 
@@ -167,6 +169,8 @@ let do_change ~ofmt params =
   let uri, version =
     (string_field "uri" document, int_field "version" document)
   in
+  (* XXX: fix this *)
+  let uri = Lang.LUri.(File.of_uri (of_string uri)) |> Result.get_ok in
   let changes = List.map U.to_assoc @@ list_field "contentChanges" params in
   match changes with
   | [] ->
@@ -186,11 +190,15 @@ let do_change ~ofmt params =
 let do_close ~ofmt:_ params =
   let document = dict_field "textDocument" params in
   let uri = string_field "uri" document in
+  (* XXX: fix this *)
+  let uri = Lang.LUri.(File.of_uri (of_string uri)) |> Result.get_ok in
   Doc_manager.close ~uri
 
 let get_textDocument params =
   let document = dict_field "textDocument" params in
   let uri = string_field "uri" document in
+  (* XXX fix this *)
+  let uri = Lang.LUri.(File.of_uri (of_string uri)) |> Result.get_ok in
   let doc = Doc_manager.find_doc ~uri in
   (uri, doc)
 

coq/dune

@@ -3,4 +3,4 @@
  (public_name coq-lsp.coq)
  ; Unfortunate we have to link the STM due to the LTAC plugin
  ; depending on it, we should fix this upstream
- (libraries coq-core.vernac coq-core.stm coq-serapi.serlib uri))
+ (libraries lang coq-core.vernac coq-core.stm coq-serapi.serlib))

coq/init.mli

@@ -32,5 +32,5 @@ val coq_init : coq_opts -> State.t
 val doc_init :
      root_state:State.t
   -> workspace:Workspace.t
-  -> uri:string
+  -> uri:Lang.LUri.File.t
   -> (State.t, Loc.t) Protect.E.t

coq/workspace.ml

@@ -114,7 +114,7 @@ let load_objs libs =
 
 (* We need to compute this with the right load path *)
 let dirpath_of_uri ~uri =
-  let f = Uri.pct_decode (Uri.path (Uri.of_string uri)) in
+  let f = Lang.LUri.File.to_string_file uri in
   let ldir0 =
     try
       let lp = Loadpath.find_load_path (Filename.dirname f) in

coq/workspace.mli

@@ -41,4 +41,4 @@ end
 val guess : debug:bool -> cmdline:CmdLine.t -> dir:string -> t
 
 (** [apply libname w] will prepare Coq for a new file [libname] on workspace [w] *)
-val apply : uri:string -> t -> unit
+val apply : uri:Lang.LUri.File.t -> t -> unit

examples/modα.v

@@ -0,0 +1,5 @@
+(* This is just a test for unicode filenames. *)
+
+Definition a := 3.
+
+Print a.

fleche/contents.ml

@@ -109,7 +109,7 @@ module WaterProof = struct
 end
 
 let process_contents ~uri ~raw =
-  let ext = Filename.extension uri in
+  let ext = Lang.LUri.File.extension uri in
   match ext with
   | ".v" -> R.Ok raw
   | ".mv" -> R.Ok (Markdown.process raw)

fleche/contents.mli

@@ -25,4 +25,4 @@ module R : sig
   val map : f:('a -> 'b) -> 'a t -> 'b t
 end
 
-val make : uri:string -> raw:string -> t R.t
+val make : uri:Lang.LUri.File.t -> raw:string -> t R.t

fleche/doc.ml

@@ -171,7 +171,7 @@ end
    assumed to be the tip of the document. The initial document is the empty
    list. *)
 type t =
-  { uri : string
+  { uri : Lang.LUri.File.t
   ; version : int
   ; contents : Contents.t
   ; root : Coq.State.t
@@ -184,7 +184,11 @@ let mk_doc root_state workspace uri =
   Coq.Init.doc_init ~root_state ~workspace ~uri
 
 let asts doc = List.filter_map Node.ast doc.nodes
-let init_fname ~uri = Loc.InFile { dirpath = None; file = uri }
+
+let init_fname ~uri =
+  let file = Lang.LUri.File.to_string_file uri in
+  Loc.InFile { dirpath = None; file }
+
 let init_loc ~uri = Loc.initial (init_fname ~uri)
 
 let process_init_feedback ~stats range state messages =

fleche/doc.mli

@@ -53,7 +53,7 @@ end
     meta-data map [Range.t -> data], where for now [data] is the contents of
     [Node.t]. *)
 type t = private
-  { uri : string
+  { uri : Lang.LUri.File.t
   ; version : int
   ; contents : Contents.t
   ; root : Coq.State.t
@@ -69,7 +69,7 @@ val asts : t -> Coq.Ast.t list
 val create :
      state:Coq.State.t
   -> workspace:Coq.Workspace.t
-  -> uri:string
+  -> uri:Lang.LUri.File.t
   -> version:int
   -> raw:string
   -> (t, Loc.t) Coq.Protect.R.t
@@ -95,4 +95,8 @@ val check : ofmt:Format.formatter -> target:Target.t -> doc:t -> unit -> t
 
 (** This is internal, to workaround the Coq multiple-docs problem *)
 val create_failed_permanent :
-  state:Coq.State.t -> uri:string -> version:int -> raw:string -> t Contents.R.t
+     state:Coq.State.t
+  -> uri:Lang.LUri.File.t
+  -> version:int
+  -> raw:string
+  -> t Contents.R.t

fleche/io.ml

@@ -3,13 +3,13 @@ module CallBack = struct
     { trace : string -> ?extra:string -> string -> unit
     ; send_diagnostics :
            ofmt:Format.formatter
-        -> uri:string
+        -> uri:Lang.LUri.File.t
         -> version:int
         -> Lang.Diagnostic.t list
         -> unit
     ; send_fileProgress :
            ofmt:Format.formatter
-        -> uri:string
+        -> uri:Lang.LUri.File.t
         -> version:int
         -> Progress.Info.t list
         -> unit

fleche/io.mli

@@ -5,13 +5,13 @@ module CallBack : sig
               verbose mode *)
     ; send_diagnostics :
            ofmt:Format.formatter
-        -> uri:string
+        -> uri:Lang.LUri.File.t
         -> version:int
         -> Lang.Diagnostic.t list
         -> unit
     ; send_fileProgress :
            ofmt:Format.formatter
-        -> uri:string
+        -> uri:Lang.LUri.File.t
         -> version:int
         -> Progress.Info.t list
         -> unit
@@ -30,14 +30,14 @@ end
 module Report : sig
   val diagnostics :
        ofmt:Format.formatter
-    -> uri:string
+    -> uri:Lang.LUri.File.t
     -> version:int
     -> Lang.Diagnostic.t list
     -> unit
 
   val fileProgress :
        ofmt:Format.formatter
-    -> uri:string
+    -> uri:Lang.LUri.File.t
     -> version:int
     -> Progress.Info.t list
     -> unit

lang/dune

@@ -1,4 +1,4 @@
 (library
  (name lang)
  (public_name coq-lsp.lang)
- (libraries coq-core.library))
+ (libraries uri coq-core.library))

lang/lUri.ml

@@ -0,0 +1,24 @@
+(************************************************************************)
+(* Flèche => document manager: Language Support                         *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+type t = Uri.t
+
+let of_string = Uri.of_string
+let is_file_path _ = true
+
+module File = struct
+  type uri = t
+
+  type t =
+    { uri : uri
+    ; file : string
+    }
+
+  let of_uri uri = Result.Ok { uri; file = Uri.pct_decode (Uri.path uri) }
+  let to_string_uri { uri; _ } = Uri.to_string uri
+  let to_string_file { file; _ } = file
+  let extension { file; _ } = Filename.extension file
+end

lang/lUri.mli

@@ -0,0 +1,30 @@
+(************************************************************************)
+(* Flèche => document manager: Language Support                         *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+type t
+
+(** Builds and URI from a string, like the ones present in the LSP protocol wire *)
+val of_string : string -> t
+
+(** Checks if a URI points to a (local) file *)
+val is_file_path : t -> bool
+
+(** Uris that are filesystem paths *)
+module File : sig
+  type uri = t
+  type t
+
+  val of_uri : uri -> (t, string) Result.t
+
+  (** Extension, with the dot included *)
+  val extension : t -> string
+
+  (** Percent-enconded URI as string *)
+  val to_string_uri : t -> string
+
+  (** Filename version, fit for OS functions *)
+  val to_string_file : t -> string
+end

lsp/base.ml

@@ -77,11 +77,3 @@ let mk_notification ~method_ ~params =
     ; ("method", `String method_)
     ; ("params", params)
     ]
-
-module VersionedTextDocument = struct
-  type t =
-    { uri : string
-    ; version : int
-    }
-  [@@deriving yojson]
-end

lsp/base.mli

@@ -35,14 +35,6 @@ module Message : sig
   val params : t -> (string * Yojson.Safe.t) list
 end
 
-module VersionedTextDocument : sig
-  type t =
-    { uri : string
-    ; version : int
-    }
-  [@@deriving yojson]
-end
-
 (** Build notification *)
 val mk_notification : method_:string -> params:Yojson.Safe.t -> Yojson.Safe.t