Fcntl.lean🔗

Linux fcntl Syscall

Models the Linux AArch64 fcntl syscall (__NR_fcntl = 25, fs/fcntl.c:590, include/uapi/asm-generic/fcntl.h:111) for F_GETFD (1) and F_SETFD (2, FD_CLOEXEC = 1).

@[expose] public section

namespace Arm64

def SYS_FCNTLL25–26 ↗#

Linux AArch64 fcntl syscall number (__NR_fcntl = 25, include/uapi/asm-generic/unistd.h:99).

def SYS_FCNTL : BitVec 64 := 25#64

def F_GETFD_W32L28–29 ↗#

Linux fcntl.h commands F_GETFD (1) and F_SETFD (2).

def F_GETFD_W32 : BitVec 32 := 1#32

def F_SETFD_W32L30 ↗#

def F_SETFD_W32 : BitVec 32 := 2#32

def execFcntlL32–53 ↗#

fcntl(fd, cmd, arg): models F_GETFD (1) and F_SETFD (2, updating FdEntry.cloexec := (arg &&& 1) != 0) on open .localFile or .localDir descriptors, and faults on all other descriptor kinds or commands.

def execFcntl (s : State) : State :=
  let rawFd := s.readReg32 Reg.x0
  let cmd   := s.readReg32 Reg.x1
  let arg   := s.readReg64 Reg.x2
  if rawFd.slt 0#32 then (s.writeReg64 Reg.x0 (-EBADF)).advancePC
  else
    let fd := rawFd.zeroExtend 64
    match s.fs.fds fd with
    | none =>
      if fd < 3#64 then s.setStatus (.Exception "unmodeled stdio fd")
      else (s.writeReg64 Reg.x0 (-EBADF)).advancePC
    | some desc =>
      if !(desc.kind == .localFile || desc.kind == .localDir) then s.setStatus (.Exception "unmodeled non-file fd")
      else if cmd == F_GETFD_W32 then
        (s.writeReg64 Reg.x0 (if desc.cloexec then 1#64 else 0#64)).advancePC
      else if cmd == F_SETFD_W32 then
        let fs' := s.fs.setFd fd (some { desc with cloexec := (arg &&& 1#64) != 0#64 })
        ((s.setFs fs').writeReg64 Reg.x0 0#64).advancePC
      else s.setStatus (.Exception "unmodeled fcntl cmd")

end Arm64