diff --git a/.unreleased/bug-fixes/2811-server-bind-error.md b/.unreleased/bug-fixes/2811-server-bind-error.md new file mode 100644 index 0000000000..da379caf93 --- /dev/null +++ b/.unreleased/bug-fixes/2811-server-bind-error.md @@ -0,0 +1,2 @@ +When expected server port is already bound, report clean user error instead of +crashing with a traceback (#2676). diff --git a/shai/src/main/scala/at/forsyte/apalache/shai/v1/RpcServer.scala b/shai/src/main/scala/at/forsyte/apalache/shai/v1/RpcServer.scala index 179bad094a..d213edfe73 100644 --- a/shai/src/main/scala/at/forsyte/apalache/shai/v1/RpcServer.scala +++ b/shai/src/main/scala/at/forsyte/apalache/shai/v1/RpcServer.scala @@ -1,6 +1,6 @@ package at.forsyte.apalache.shai.v1 -import zio.{console, Ref, ZEnv, ZIO} +import zio.{console, ExitCode, Ref, ZEnv, ZIO} import java.util.UUID import scalapb.zio_grpc.ServerMain @@ -8,6 +8,9 @@ import scalapb.zio_grpc.ServiceList import com.typesafe.scalalogging.LazyLogging import io.grpc.ServerBuilder +import java.io.IOException +import java.net.BindException + /** * The Shai RPC server handling gRPC requests to interact with the model checker * @@ -39,10 +42,24 @@ class RpcServer(override val port: Int) extends ServerMain with LazyLogging { // https://github.com/informalsystems/apalache/issues/2622 override def builder: (x0) forSome { type x0 <: ServerBuilder[x0] } = super.builder.maxInboundMessageSize(8 * 1024 * 1024) + + override def run(args: List[String]) = { + myAppLogic.catchAll { t => + t match { + // treat "post already in use" error specially + case e: IOException if e.getCause.isInstanceOf[BindException] => + logger.error(s"${RpcServer.STARTUP_ERROR_PROMPT} ${e.getMessage}: ${e.getCause.getMessage}") + case _ => + logger.error(RpcServer.STARTUP_ERROR_PROMPT, t) + } + ZIO.succeed(ExitCode.failure) + } + } } object RpcServer { val DEFAULT_PORT = 8822 + val STARTUP_ERROR_PROMPT = "Error while starting Apalache server:" def apply(port: Int = DEFAULT_PORT) = new RpcServer(port) } diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 56efb5371a..3237804fc2 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -3999,6 +3999,38 @@ The Apalache server is running on port 8888. Press Ctrl-C to stop. ... ``` +### server mode: error is nicely reported when port is already in use + +NOTE: These tests are skipped because the would complicate our CI process +more than is warranted by the functionality they test. To enable these tests, +remove the `$MDX skip` annotations. + +Start socat in the background to occupy the port, save its pid and wait a second to let binding happen + +```sh +$ socat TCP-L:8888,fork,reuseaddr - & echo $! > pid.pid && sleep 1 +``` + +Try to start the Apalache server on the occupied port, +redirect its output to the file, +save its exit code, +strip logger prompt +and exit with status code of the server + +```sh +$ apalache-mc server --port=8888 1>out 2>out; ext=$? && cat out | sed -E 's/E@.*$//' && exit $ext +... +Error while starting Apalache server: Failed to bind to address 0.0.0.0/0.0.0.0:8888: Address already in use +[1] +``` + +Cleanup: kill socat and delete temporary files + +```sh +$ cat pid.pid | xargs kill -9 +$ rm pid.pid out +``` + ## quint input ### quint input: quint spec can be checked