diff --git a/.gitignore b/.gitignore index 674e00875..9abe79ec7 100644 --- a/.gitignore +++ b/.gitignore @@ -7,6 +7,7 @@ *.clean *.ilean *.d +*.lock a.out build GPATH diff --git a/src/util/file_lock.cpp b/src/util/file_lock.cpp index e9326a2d5..64655d655 100644 --- a/src/util/file_lock.cpp +++ b/src/util/file_lock.cpp @@ -8,17 +8,68 @@ Author: Leonardo de Moura #include "util/exception.h" #include "util/sstream.h" #include "util/file_lock.h" -#ifdef _WINDOWS -namespace lean { -file_lock::file_lock(char const *, bool) { - // TODO(Leo): +#include + +#ifdef LEAN_WINDOWS +#include +#include +#define LOCK_SH 1 /* shared lock */ +#define LOCK_EX 2 /* exclusive lock */ +#define LOCK_NB 4 /* don't block when locking */ +#define LOCK_UN 8 /* unlock */ + +static BOOL lock(HANDLE h, int non_blocking, int exclusive) { + DWORD lower, upper; + OVERLAPPED ovlp; + int flags = 0; + + lower = GetFileSize(h, &upper); + memset (&ovlp, 0, sizeof(ovlp)); + + if (non_blocking) + flags |= LOCKFILE_FAIL_IMMEDIATELY; + if (exclusive) + flags |= LOCKFILE_EXCLUSIVE_LOCK; + + return LockFileEx(h, flags, 0, lower, upper, &ovlp); } -file_lock::~file_lock() { + +static BOOL unlock(HANDLE h) { + DWORD lower, upper; + lower = GetFileSize(h, &upper); + return UnlockFile(h, 0, 0, lower, upper); } + +int flock(int fd, int op) { + HANDLE h = (HANDLE)_get_osfhandle(fd); + DWORD res; + int non_blocking; + + if (h == INVALID_HANDLE_VALUE) + return -1; + + non_blocking = op & LOCK_NB; + op &= ~LOCK_NB; + + switch (op) { + case LOCK_SH: + res = lock(h, non_blocking, 0); + break; + case LOCK_EX: + res = lock(h, non_blocking, 1); + break; + case LOCK_UN: + res = unlock(h); + break; + default: + return -1; + } + return !res ? -1 : 0; } #else #include -#include +#endif + namespace lean { file_lock::file_lock(char const * fname, bool exclusive): m_fname(fname), m_fd(-1) { @@ -39,4 +90,3 @@ file_lock::~file_lock() { } } } -#endif