From d6f0ed834547fdd0b9049866544f294319f48f8b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Apr 2024 09:33:13 +0000 Subject: [PATCH] C library: add creat, open, openat These take pointer-typed arguments, which we should check for validity. Also add their large-filesystem version (with suffix 64). --- regression/cbmc-library/creat-01/main.c | 15 ++ regression/cbmc-library/creat-01/test.desc | 9 + regression/cbmc-library/fcntl-01/main.c | 7 +- regression/cbmc-library/fcntl-01/test.desc | 2 +- regression/cbmc-library/open-01/main.c | 9 + regression/cbmc-library/open-01/test.desc | 9 + regression/cbmc-library/openat-01/main.c | 10 + regression/cbmc-library/openat-01/test.desc | 9 + src/ansi-c/library/fcntl.c | 239 +++++++++++++++++++- src/ansi-c/library_check.sh | 6 + 10 files changed, 310 insertions(+), 5 deletions(-) create mode 100644 regression/cbmc-library/creat-01/main.c create mode 100644 regression/cbmc-library/creat-01/test.desc create mode 100644 regression/cbmc-library/open-01/main.c create mode 100644 regression/cbmc-library/open-01/test.desc create mode 100644 regression/cbmc-library/openat-01/main.c create mode 100644 regression/cbmc-library/openat-01/test.desc diff --git a/regression/cbmc-library/creat-01/main.c b/regression/cbmc-library/creat-01/main.c new file mode 100644 index 00000000000..e74267f724d --- /dev/null +++ b/regression/cbmc-library/creat-01/main.c @@ -0,0 +1,15 @@ +#include + +#ifdef _WIN32 +# define MODE_T int +#else +# define MODE_T mode_t +#endif + +int main() +{ + char *unint_path; + MODE_T mode; + int fd = creat(unint_path, mode); + return 0; +} diff --git a/regression/cbmc-library/creat-01/test.desc b/regression/cbmc-library/creat-01/test.desc new file mode 100644 index 00000000000..7eeca57ed56 --- /dev/null +++ b/regression/cbmc-library/creat-01/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check --bounds-check +dereference failure: pointer invalid in \*pathname: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/fcntl-01/main.c b/regression/cbmc-library/fcntl-01/main.c index d8174355b5a..001bbdeb794 100644 --- a/regression/cbmc-library/fcntl-01/main.c +++ b/regression/cbmc-library/fcntl-01/main.c @@ -3,7 +3,10 @@ int main() { - fcntl(); - assert(0); + int flags; + int fd = open("foo", flags); + int cmd; + int result = fcntl(fd, cmd); + assert(fd >= 0 || result == -1); return 0; } diff --git a/regression/cbmc-library/fcntl-01/test.desc b/regression/cbmc-library/fcntl-01/test.desc index 9542d988e8d..96c9b4bcd7b 100644 --- a/regression/cbmc-library/fcntl-01/test.desc +++ b/regression/cbmc-library/fcntl-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/open-01/main.c b/regression/cbmc-library/open-01/main.c new file mode 100644 index 00000000000..b61d2c9bff6 --- /dev/null +++ b/regression/cbmc-library/open-01/main.c @@ -0,0 +1,9 @@ +#include + +int main() +{ + char *unint_path; + int flags; + int fd = open(unint_path, flags); + return 0; +} diff --git a/regression/cbmc-library/open-01/test.desc b/regression/cbmc-library/open-01/test.desc new file mode 100644 index 00000000000..7eeca57ed56 --- /dev/null +++ b/regression/cbmc-library/open-01/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check --bounds-check +dereference failure: pointer invalid in \*pathname: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc-library/openat-01/main.c b/regression/cbmc-library/openat-01/main.c new file mode 100644 index 00000000000..20386011093 --- /dev/null +++ b/regression/cbmc-library/openat-01/main.c @@ -0,0 +1,10 @@ +#include + +int main() +{ + int dirfd; + char *unint_path; + int flags; + int fd = openat(dirfd, unint_path, flags); + return 0; +} diff --git a/regression/cbmc-library/openat-01/test.desc b/regression/cbmc-library/openat-01/test.desc new file mode 100644 index 00000000000..7eeca57ed56 --- /dev/null +++ b/regression/cbmc-library/openat-01/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check --bounds-check +dereference failure: pointer invalid in \*pathname: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/ansi-c/library/fcntl.c b/src/ansi-c/library/fcntl.c index 5de5546bf2e..e3c86d3f40d 100644 --- a/src/ansi-c/library/fcntl.c +++ b/src/ansi-c/library/fcntl.c @@ -1,17 +1,252 @@ -/* FUNCTION: fcntl */ +/* FUNCTION: __CPROVER_fcntl */ #ifndef __CPROVER_FCNTL_H_INCLUDED #include #define __CPROVER_FCNTL_H_INCLUDED #endif +#ifndef __CPROVER_ERRNO_H_INCLUDED +# include +# define __CPROVER_ERRNO_H_INCLUDED +#endif + int __VERIFIER_nondet_int(void); -int fcntl(int fd, int cmd, ...) +int __CPROVER_fcntl(int fd, int cmd) { __CPROVER_HIDE:; + if(fd < 0) + { + errno = EBADF; + return -1; + } + int return_value=__VERIFIER_nondet_int(); (void)fd; (void)cmd; return return_value; } + +/* FUNCTION: fcntl */ + +int __CPROVER_fcntl(int, int); + +int fcntl(int fd, int cmd, ...) +{ + return __CPROVER_fcntl(fd, cmd); +} + +/* FUNCTION: _fcntl */ + +int __CPROVER_fcntl(int, int); + +int _fcntl(int fd, int cmd, ...) +{ + return __CPROVER_fcntl(fd, cmd); +} + +/* FUNCTION: fcntl64 */ + +int __CPROVER_fcntl(int, int); + +int fcntl64(int fd, int cmd, ...) +{ + return __CPROVER_fcntl(fd, cmd); +} + +/* FUNCTION: __CPROVER_open */ + +#ifndef __CPROVER_FCNTL_H_INCLUDED +# include +# define __CPROVER_FCNTL_H_INCLUDED +#endif + +int __VERIFIER_nondet_int(void); + +int __CPROVER_open(const char *pathname, int flags) +{ +__CPROVER_HIDE:; + int return_value = __VERIFIER_nondet_int(); + __CPROVER_assume(return_value >= -1); + (void)*pathname; + (void)flags; + return return_value; +} + +/* FUNCTION: open */ + +int __CPROVER_open(const char *, int); + +int open(const char *pathname, int flags, ...) +{ + return __CPROVER_open(pathname, flags); +} + +/* FUNCTION: _open */ + +int __CPROVER_open(const char *, int); + +int _open(const char *pathname, int flags, ...) +{ + return __CPROVER_open(pathname, flags); +} + +/* FUNCTION: open64 */ + +int __CPROVER_open(const char *, int); + +int open64(const char *pathname, int flags, ...) +{ + return __CPROVER_open(pathname, flags); +} + +/* FUNCTION: __CPROVER_creat */ + +#ifndef __CPROVER_FCNTL_H_INCLUDED +# include +# define __CPROVER_FCNTL_H_INCLUDED +#endif + +#ifndef MODE_T +# ifdef _WIN32 +# define MODE_T int +# else +# define MODE_T mode_t +# endif +#endif + +int __VERIFIER_nondet_int(void); + +int __CPROVER_creat(const char *pathname, MODE_T mode) +{ +__CPROVER_HIDE:; + int return_value = __VERIFIER_nondet_int(); + __CPROVER_assume(return_value >= -1); + (void)*pathname; + (void)mode; + return return_value; +} + +/* FUNCTION: creat */ + +#ifndef __CPROVER_FCNTL_H_INCLUDED +# include +# define __CPROVER_FCNTL_H_INCLUDED +#endif + +#ifndef MODE_T +# ifdef _WIN32 +# define MODE_T int +# else +# define MODE_T mode_t +# endif +#endif + +int __CPROVER_creat(const char *, MODE_T); + +int creat(const char *pathname, MODE_T mode) +{ + return __CPROVER_creat(pathname, mode); +} + +/* FUNCTION: _creat */ + +#ifndef __CPROVER_FCNTL_H_INCLUDED +# include +# define __CPROVER_FCNTL_H_INCLUDED +#endif + +#ifndef MODE_T +# ifdef _WIN32 +# define MODE_T int +# else +# define MODE_T mode_t +# endif +#endif + +int __CPROVER_creat(const char *, MODE_T); + +int _creat(const char *pathname, MODE_T mode) +{ + return __CPROVER_creat(pathname, mode); +} + +/* FUNCTION: creat64 */ + +#ifndef __CPROVER_FCNTL_H_INCLUDED +# include +# define __CPROVER_FCNTL_H_INCLUDED +#endif + +#ifndef MODE_T +# ifdef _WIN32 +# define MODE_T int +# else +# define MODE_T mode_t +# endif +#endif + +int __CPROVER_creat(const char *, MODE_T); + +int creat64(const char *pathname, MODE_T mode) +{ + return __CPROVER_creat(pathname, mode); +} + +/* FUNCTION: __CPROVER_openat */ + +#ifndef __CPROVER_FCNTL_H_INCLUDED +# include +# define __CPROVER_FCNTL_H_INCLUDED +#endif + +#ifndef __CPROVER_ERRNO_H_INCLUDED +# include +# define __CPROVER_ERRNO_H_INCLUDED +#endif + +int __VERIFIER_nondet_int(void); + +int __CPROVER_openat(int dirfd, const char *pathname, int flags) +{ +__CPROVER_HIDE:; + if(dirfd < 0) + { + errno = EBADF; + return -1; + } + + int return_value = __VERIFIER_nondet_int(); + __CPROVER_assume(return_value >= -1); + (void)dirfd; + (void)*pathname; + (void)flags; + return return_value; +} + +/* FUNCTION: openat */ + +int __CPROVER_openat(int dirfd, const char *pathname, int flags); + +int openat(int dirfd, const char *pathname, int flags, ...) +{ + return __CPROVER_openat(dirfd, pathname, flags); +} + +/* FUNCTION: _openat */ + +int __CPROVER_openat(int dirfd, const char *pathname, int flags); + +int _openat(int dirfd, const char *pathname, int flags, ...) +{ + return __CPROVER_openat(dirfd, pathname, flags); +} + +/* FUNCTION: openat64 */ + +int __CPROVER_openat(int dirfd, const char *pathname, int flags); + +int openat64(int dirfd, const char *pathname, int flags, ...) +{ + return __CPROVER_openat(dirfd, pathname, flags); +} diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh index cb3eedf4260..b6ee26d03f7 100755 --- a/src/ansi-c/library_check.sh +++ b/src/ansi-c/library_check.sh @@ -31,10 +31,14 @@ perl -p -i -e 's/^__CPROVER_contracts_library\n//' __functions # Some functions are implicitly covered by running on different operating # systems: +perl -p -i -e 's/^_creat\n//' __functions # creat, macOS +perl -p -i -e 's/^_fcntl\n//' __functions # fcntl, macOS perl -p -i -e 's/^_fopen\n//' __functions # fopen, macOS perl -p -i -e 's/^_getopt\n//' __functions # getopt, macOS perl -p -i -e 's/^_mmap\n//' __functions # mmap, macOS perl -p -i -e 's/^_munmap\n//' __functions # mumap, macOS +perl -p -i -e 's/^_open\n//' __functions # open, macOS +perl -p -i -e 's/^_openat\n//' __functions # openat, macOS perl -p -i -e 's/^_pipe\n//' __functions # pipe, macOS perl -p -i -e 's/^_setjmp\n//' __functions # pipe, macOS perl -p -i -e 's/^_time(32|64)\n//' __functions # time, Windows @@ -52,6 +56,8 @@ perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD # Some functions are covered by existing tests: +perl -p -i -e 's/^__CPROVER_(creat|fcntl|open|openat)\n//' __functions # creat, fcntl, open, openat +perl -p -i -e 's/^(creat|fcntl|open|openat)64\n//' __functions # same as creat, fcntl, open, openat perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01 perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01 perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen