LSP error of type "Parse error"/"Invalid Request" is missing the "id" property

[robflop]

The provided code for reproduction is written in Scala, as that is what I am utilizing the Dafny Language Server in.
It uses the "os-lib" library for scala that can be found here: https://github.com/com-lihaoyi/os-lib.

Dafny version

4.10.0+f24efae13647804624723de981bb5c95ea83e177

Code to produce this issue

import os.{SubProcess, spawn}
import java.nio.charset.StandardCharsets
import scala.collection.mutable.ArrayBuffer

@main
def main(): Unit = {
  val sub: SubProcess = spawn(cmd = ("dafny", "server"))

  // First send initialize or the language server won't respond at all
  val initMsg: String =
    """{
      |  "jsonrpc": "2.0",
      |  "id": 1,
      |  "method": "initialize",
      |  "params": {
      |    "processId": null,
      |    "rootUri": null,
      |    "capabilities": {}
      |  }
      |}""".stripMargin
  val initMsgBytes: Array[Byte] = initMsg.getBytes(StandardCharsets.UTF_8)
  val initMsgHeader: String     = s"Content-Length: ${initMsgBytes.length}\r\n\r\n"

  sub.stdin.write(initMsgHeader)
  sub.stdin.write(initMsg)
  sub.stdin.flush()

  // Form and send invalid message
  val invalidMsg: String    = "invalid message"
  val msgBytes: Array[Byte] = invalidMsg.getBytes(StandardCharsets.UTF_8)
  val msgHeader: String     = s"Content-Length: ${msgBytes.length}\r\n\r\n"

  sub.stdin.write(msgHeader)
  sub.stdin.write(invalidMsg)
  sub.stdin.flush()

  // Read out responses
  while true do {
    val headerBytes: ArrayBuffer[Byte] = new collection.mutable.ArrayBuffer[Byte]()
    val terminator: Array[Byte]        = "\r\n\r\n".getBytes(StandardCharsets.UTF_8)
    var foundTerminator: Boolean       = false

    // Find the header terminator
    while !foundTerminator do {
      val b: Byte = sub.stdout.readByte()
      headerBytes.append(b)

      if headerBytes.size >= terminator.length then {
        // Compare the last X bytes, where X is the terminator's byte length, to the terminator string
        // If the last X bytes equal the terminator, the end of the message header has been found
        val tail: Array[Byte] = headerBytes.takeRight(terminator.length).toArray

        if tail.sameElements(terminator) then {
          foundTerminator = true
        }
      }
    }

    // Find message length and read that number of bytes from stdout
    val replyHeader: String = new String(headerBytes.toArray(), StandardCharsets.UTF_8)
    val contentLength: Int = "Content-Length:\\s*(\\d+)".r.findFirstMatchIn(replyHeader) match {
      case Some(m) => m.group(1).toInt
      case None    => throw new Exception("Content-Length header not found.")
    }

    val replyBytes: Array[Byte] = new Array[Byte](contentLength)
    sub.stdout.readFully(replyBytes)

    val replyMessage: String = new String(replyBytes, StandardCharsets.UTF_8)

    // One of these printed messages will be the faulty error response
    println(s"Read message content:\n$replyMessage")
  }
}

Command to run and resulting output

Read message content:
{"jsonrpc":"2.0","method":"telemetry/event","params":{"kind":3,"payload":"Z3 version 4.8.5"}}
Read message content:
{"jsonrpc":"2.0","method":"telemetry/event","params":{"kind":2,"payload":"z3"}}
Read message content:
{"jsonrpc":"2.0","method":"serverStarted","params":"4.10.0.0"}
Read message content:
{"jsonrpc":"2.0","method":"dafnyLanguageServerVersionReceived","params":"4.10.0.0"}
Read message content:
{"jsonrpc":"2.0","error":{"code":-32700,"message":"Parse Error"}}
Read message content:
{"jsonrpc":"2.0","id":1,"result":{"capabilities":{"textDocumentSync":2,"experimental":{},"workspace":{"workspaceFolders":{"changeNotifications":false},"fileOperations":{}}},"serverInfo":{"name":"Dafny","version":"4.10.0.0"}}}

What happened?

When sending the Dafny Language Server a message leading to a "Parse error" or "Invalid request" error, the Dafny LS responds with the following:

{"jsonrpc":"2.0","error":{"code":-32700,"message":"Parse Error"}}

While the error itself is expected, this response is missing the id property. Per JSON-RPC 2.0 specification, the id property is required for all kinds of error responses, but must be null for parse errors and invalid requests.

A proper response per spec would therefore look like the following:

{"jsonrpc":"2.0","error":{"code":-32700,"message":"Parse Error"}, "id": null}

See the JSON-RPC 2.0 Specification under the "5 Response object" section.

p.S.: It seems strange to me that the language server does not respond at all if you do not send an initialize message first. Based on the LSP spec, I'd imagine it should be sending an error with code -32002 when receiving messages from a client before initializing (regardless of whether it is a valid message or an invalid one like in above example), see here for reference.

What type of operating system are you experiencing the problem on?

Windows