Merge pull request #2526 from kant2002/kant/lsp-fix

Do not crash LSP server on malformed Content-Length

src/fstar/FStar.Interactive.Lsp.fst

@@ -192,7 +192,9 @@ let rec parse_header_len (stream: stream_reader) (len: int): int =
   match U.read_line stream with
   | Some s ->
     if U.starts_with s "Content-Length: " then
-      parse_header_len stream (U.int_of_string (U.substring_from s 16))
+      match U.safe_int_of_string (U.substring_from s 16) with
+      | Some new_len -> parse_header_len stream new_len
+      | None -> raise MalformedHeader
     else if U.starts_with s "Content-Type: " then
       parse_header_len stream len
     else if s = "" then

tests/Makefile

@@ -6,7 +6,7 @@ bug-reports \
 error-messages \
 friends \
 incl \
-interactive \
+ide \
 machine_integers \
 micro-benchmarks \
 prettyprinting \

tests/ide/Makefile

@@ -0,0 +1,15 @@
+FSTAR_HOME=../..
+include ../../examples/Makefile.include
+
+ALL_TEST_DIRS=\
+lsp \
+emacs
+
+all: $(addsuffix .all, $(ALL_TEST_DIRS))
+clean: $(addsuffix .clean, $(ALL_TEST_DIRS))
+
+%.all: %
+	+$(MAKE) -C $^ all
+
+%.clean: %
+	+$(MAKE) -C $^ clean

tests/interactive/Makefile → tests/ide/Makefile.common

@@ -37,29 +37,20 @@ touch:
 
 %.in: .FORCE
 
-FSTAR_HOME = ../..
+FSTAR_HOME = ../../..
 include $(FSTAR_HOME)/ulib/gmake/z3.mk
 
 ifdef Z3
 SMT=--smt $(Z3)
 endif
 
-FSTAR:=${FSTAR_HOME}/bin/fstar.exe $(SMT) --ide --warn_error -282
-
-
-# Feed .in to F* and record output as .out.  Output is passed through cleanup.py
-# to ensure that the output is deterministic by pretty-printing JSON messages
-# (otherwise the order of fields in JSON dictionaries might vary across runs)
-# We turn off the .checked file cache so we don't get any races in CI
-%.out: %.in $(FSTAR_HOME)/bin/fstar.exe
-	$(eval FST := $(firstword $(subst ., ,$<)))
-	$(FSTAR) --cache_off "$(realpath ${FST}.fst)" < "$<" | python cleanup.py "$@"
+JSON_CLEANUP:=python ../cleanup.py
 
 # Clean up and accept an existing ‘.out’ file (possibly generated by
 # ‘fstar-write-transcript’, or possibly by ‘make build’) and save it as
 # ‘.out.expected’.
 %.out.accept: %.out
-	python cleanup.py "$<.expected" < "$<"
+	$(JSON_CLEANUP) "$<.expected" < "$<"
 
 # Verify that a given output matches the corresponding input
 %.out.check: %.out %.out.expected

tests/ide/emacs/Makefile

@@ -0,0 +1,11 @@
+include ../Makefile.common
+
+FSTAR:=${FSTAR_HOME}/bin/fstar.exe $(SMT) --ide --warn_error -282
+
+# Feed .in to F* and record output as .out.  Output is passed through cleanup.py
+# to ensure that the output is deterministic by pretty-printing JSON messages
+# (otherwise the order of fields in JSON dictionaries might vary across runs)
+# We turn off the .checked file cache so we don't get any races in CI
+%.out: %.in $(FSTAR_HOME)/bin/fstar.exe
+	$(eval FST := $(firstword $(subst ., ,$<)))
+	$(FSTAR) --cache_off "$(realpath ${FST}.fst)" < "$<" | $(JSON_CLEANUP) "$@"

tests/ide/lsp/.gitignore

@@ -0,0 +1,2 @@
+*.out
+*.out.check

tests/ide/lsp/Makefile

@@ -0,0 +1,11 @@
+include ../Makefile.common
+
+FSTAR:=${FSTAR_HOME}/bin/fstar.exe $(SMT) --lsp --warn_error -282
+
+# Feed .in to F* and record output as .out.  Output is passed through cleanup.py
+# to ensure that the output is deterministic by pretty-printing JSON messages
+# (otherwise the order of fields in JSON dictionaries might vary across runs)
+# We turn off the .checked file cache so we don't get any races in CI
+%.out: %.in $(FSTAR_HOME)/bin/fstar.exe
+	$(FSTAR) < "$<" 2>&1 | $(JSON_CLEANUP) "$@"
+

tests/ide/lsp/broken_content_length.in

@@ -0,0 +1,4 @@
+Content-Length: a
+Content-Length: 46
+
+{"jsonrpc":"2.0","method":"exit","params":{}}

tests/ide/lsp/broken_content_length.out.expected

@@ -0,0 +1 @@
+[E] Malformed Content Header

tests/ide/lsp/exit.in

@@ -0,0 +1,3 @@
+Content-Length: 46
+
+{"jsonrpc":"2.0","method":"exit","params":{}}