[posix-runtime] Simple GET/SET_LK model

2 files changed, 26 insertions, 0 deletions

diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index ae08183f..240e589e 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -995,6 +995,7 @@ int fcntl(int fd, int cmd, ...) {
   exe_file_t *f = __get_file(fd);
   va_list ap;
   unsigned arg; /* 32 bit assumption (int/ptr) */
+  struct flock *lock;
 
   if (!f) {
     errno = EBADF;
@@ -1007,6 +1008,10 @@ int fcntl(int fd, int cmd, ...) {
    if (cmd==F_GETFD || cmd==F_GETFL || cmd==F_GETOWN) {
 #endif
     arg = 0;
+  } else if (cmd == F_GETLK || cmd == F_SETLK || cmd == F_SETLKW) {
+    va_start(ap, cmd);
+    lock = va_arg(ap, struct flock *);
+    va_end(ap);
   } else {
     va_start(ap, cmd);
     arg = va_arg(ap, int);
@@ -1036,6 +1041,20 @@ int fcntl(int fd, int cmd, ...) {
       */
       return 0;
     }
+    // Initially no other process keeps a lock, so we say the file is unlocked.
+    // Of course this doesn't account for a program locking and then checking if
+    // a lock is there. However this is quite paranoid programming and we assume
+    // doesn't happen.
+    case F_GETLK: {
+      lock->l_type = F_UNLCK;
+      return 0;
+    }
+    // We assume the application does locking correctly and will lock/unlock
+    // files correctly.
+    // Therefore this call always succeeds.
+    case F_SETLK: {
+      return 0;
+    }
     default:
       klee_warning("symbolic file, ignoring (EINVAL)");
       errno = EINVAL;
diff --git a/test/Runtime/POSIX/Fcntl.c b/test/Runtime/POSIX/Fcntl.c
index 41aeb326..53246a15 100644
--- a/test/Runtime/POSIX/Fcntl.c
+++ b/test/Runtime/POSIX/Fcntl.c
@@ -14,5 +14,12 @@ int main(int argc, char **argv) {
   assert(fcntl(fd, F_SETFD, FD_CLOEXEC, 1) == 0);
   assert((fcntl(fd, F_GETFD) & FD_CLOEXEC) != 0);
 
+  struct flock lck;
+  assert(fcntl(fd, F_GETLK, &lck) == 0);
+  assert(lck.l_type == F_UNLCK);
+  lck.l_type = F_RDLCK;
+  assert(fcntl(fd, F_SETLK, &lck) == 0);
+  lck.l_type = F_UNLCK;
+  assert(fcntl(fd, F_SETLK, &lck) == 0);
   return 0;
 }