Open file with file descriptor?

Stream: lean4

[James Sully]

Is there a way to access the file descriptor table?

I want to write a systemd service which uses socket activation. The way this works is that systemd manages the socket file. When it detects a connection, it starts up the associated service, and passes the socket to the service by assigning it to file descriptor 3.

[Henrik Böving]

No we do not have an API for that, in general most UNIX low level operations are lacking. I'm also not sure its a good idea to allow direct access to that table. This would allow users to close fds under the nose of other parts of their program. Maybe we could have a function that does something more limited but still allows you what you want to do?

[James Sully]

hm, I'm not sure what that would look like though. I guess I have to resort to learning FFI for now.

[Henrik Böving]

Do you know how this works in e.g. rust?

[James Sully]

looks like there's an unsafe function
https://doc.rust-lang.org/std/os/fd/trait.FromRawFd.html

[James Sully]

an example usage for my exact use case in this crate:
https://github.com/mitsuhiko/listenfd/blob/7d4675c314f65f237f9f5be129129128d3fefc8e/src/unix.rs#L84

[Henrik Böving]

Hmnm, well we have unsafe in Lean as well but it is more restricting than rust unsafe. I guess we could add a fromFd function to Socket.lean that has a big warning attached to it in the doc string. Would you want to PR that?

[James Sully]

sure, I'll see if I can suss it out

[James Sully]

I'm immediately stumped by trying to figure out what lean type corresponds to a c int. All the UInt* have correspondences, but int is signed. Lean's Int doesn't seem right because it can be of arbitrary size

[James Sully]

is there a reason lean doesn't have a suite of Int8, Int32, etc?

[Sebastian Ullrich]

We do want to add those. But if it's about a (mostly) opaque number like file descriptors, I think it's okay to go with the unsigned variant for now

[Henrik Böving]

James Sully said:

I'm immediately stumped by trying to figure out what lean type corresponds to a c int. All the UInt* have correspondences, but int is signed. Lean's Int doesn't seem right because it can be of arbitrary size

Besides that there is the issue that technically speaking the size of int is not determined, the C standard merely puts a lower limit on the size (that is 16 bit instead of the 32 that we have on most platforms). But I think we can just hope nobody uses obscure targets from the past and stick to UInt32

[James Sully]

@Henrik Böving I'm not very fluent in c, so I'm a little confused. I'm trying to understand this function:

alloy c extern "lean_mk_sockaddr_un"
def SockAddrUnix.unix (path : @& System.FilePath) : SockAddrUnix :=
  struct sockaddr_un* sa = malloc(sizeof(struct sockaddr_un));
  sa->sun_family = AF_UNIX;
  strncpy(sa->sun_path, lean_string_cstr(path), sizeof(sa->sun_path) - 1);
  return to_lean<SockAddrUnix>(sa);

Doing some research, it seems like struct sockaddr_un uses a very confusing feature called "flexible array members" for the sun_path field.

My understanding was that sizeof(struct sockaddr_un) does not include sun_path, since it's variable length. I would have thought you would need to malloc not just the size of the struct, but the size of the struct plus the calculated length the sun_path will need to be. Am I misunderstanding something?

[Henrik Böving]

Maybe according to the standard? But in practice sockaddr_un should is defined as a struct with an array that has some max size for the path AFAIK. The general reasoning here is that all sockaddrs should have the same size so for example sockaddr_in just has some useless padding data in the end. The whole sockaddr thing is pretty messy :D

[James Sully]

ok, thanks. Messy indeed

[Henrik Böving]

Yeah unix(7) says:

   Address format
       A UNIX domain socket address is represented in the following structure:

           struct sockaddr_un {
               sa_family_t sun_family;               /* AF_UNIX */
               char        sun_path[108];            /* Pathname */
           };

So that's just the arbitrary upper limit :D

[James Sully]

lmfao 108. obviously

[Henrik Böving]

Surely there is some reasoning :tm: to this

[James Sully]

I was reading man sockaddr_un. Silly of me