socket.lean segfault and lean_decode_io_error API

Stream: lean4

[James Sully]

Hi! I'm trying to play around with sockets in lean. I'm using this library

Here's my main:

import Socket

def withUnixSocket path (action : Socket → IO a) := do
  let addr := Socket.SockAddrUnix.unix path
  let sock : Socket ← Socket.mk .unix .stream
  sock.connect addr

  let result ← action sock

  sock.close

  return result

def main : IO Unit := do

  let sockPath := "/home/james/tmp/lean-timer-socket"

  withUnixSocket sockPath λ _sock ↦ do
    IO.println "socket connected"
    let stdout ← IO.getStdout
    _ ← stdout.getLine

  IO.println "end"

Running this results in a segfault.

Looking at the implementation of socket.lean, it seems like it uses alloy. Is there a way to have alloy compile with debugging symbols so that I can try to figure out what's going on?

[James Sully]

Ah, it was because I was trying to connect to a nonexistent socket. touching /home/james/tmp/lean-timer-socket changes it from a segfault to an exception.

github issue here: https://github.com/hargoniX/socket.lean/issues/14

[Henrik Böving]

The segfault seems to occur, as some error messages are seemingly unable to cope with having no file name around (others again are unable to cope with having a file name around) in the implementation of error decoding. Your error specifically goes to this branch https://github.com/leanprover/lean4/blob/554e7234330cf06efffe0cb52092e783a27561cc/src/runtime/io.cpp#L175 which then presumably segfaults on the assertion.

I'm a little curious as to why we simply crash if a file name is not provided/provided. This would assume on the one hand knowledge of both the internal behaviors as well as the errors you are potentially about to throw. In particular there might be cases where you throw both file and not file related errros so you have to branch on errno yourself. This makes the trivial fix of "just supply a file name if you are a sockaddr_un" a bit too wonky for me because who knows maybe the socket API is able to throw other errors that trigger segfaults with a file name provided :/

Maybe @Sebastian Ullrich can shine some light on these decisions?

[James Sully]

Haha thanks, I was just up to there in my digging in.
I think in this case there ought to be a path - errno is 2 - ENOENT, so it seems like socket.lean should provide the path that's missing.
I guess you're talking about a separate issue to that

[James Sully]

One thing I'm a little confused by: wouldn't an assert crash cleanly, rather than segfaulting?

[James Sully]

src/runtime/debug.h:

#define lean_assert(COND) DEBUG_CODE({if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }})

[James Sully]

src/include/lean/lean.h:

#define LEAN_UNLIKELY(x) (__builtin_expect((x), 0))

I'm not sure how to find __builtin_expect, so I can't really decipher what's going on here.

[James Sully]

I would assume lean::notify_assertion_violation would print something out, but I don't see it. Perhaps assertions are disabled in release builds, and it segfaults later due to continuing with invalid data?

[James Sully]

I know all this isn't super relevant to the matter at hand, I'm just taking this as a learning opportunity

[Henrik Böving]

James Sully said:

Haha thanks, I was just up to there in my digging in.
I think in this case there ought to be a path - errno is 2 - ENOENT, so it seems like socket.lean should provide the path that's missing.
I guess you're talking about a separate issue to that

But is that generally a good idea? What if we also throw errors where the decode code assumes we have not passed a file name? If the assertion was enabled that would also be a bug.

[James Sully]

Ahh, it took me a bit but I think I'm following you now.

[James Sully]

it does seem like there's an implicit expectation for the caller to check errno themselves and decide accordingly whether to provide fname, and you're saying lean_decode_io_error should be able to handle an fname even if it's redundant, so that callers don't have to do this check themselves?

[Henrik Böving]

Yes

[James Sully]

gotcha