Skip to content

Commit 56669ea

Browse files
tautschnigtautschnig
committed
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).
1 parent facb34d commit 56669ea

File tree

10 files changed

+227
-5
lines changed

10 files changed

+227
-5
lines changed

‎regression/cbmc-library/creat-01/main.c

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include <fcntl.h>
2+
3+
int main()
4+
{
5+
char *unint_path;
6+
mode_t mode;
7+
int fd = creat(unint_path, mode);
8+
return 0;
9+
}

‎regression/cbmc-library/creat-01/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check
4+
dereference failure: pointer invalid in \*pathname: FAILURE$
5+
^VERIFICATION FAILED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring

‎regression/cbmc-library/fcntl-01/main.c

+5-2
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,10 @@
33

44
int main()
55
{
6-
fcntl();
7-
assert(0);
6+
int flags;
7+
int fd = open("foo", flags);
8+
int cmd;
9+
int result = fcntl(fd, cmd);
10+
assert(fd >= 0 || result == -1);
811
return 0;
912
}

‎regression/cbmc-library/fcntl-01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

‎regression/cbmc-library/open-01/main.c

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include <fcntl.h>
2+
3+
int main()
4+
{
5+
char *unint_path;
6+
int flags;
7+
int fd = open(unint_path, flags);
8+
return 0;
9+
}

‎regression/cbmc-library/open-01/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check
4+
dereference failure: pointer invalid in \*pathname: FAILURE$
5+
^VERIFICATION FAILED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring

‎regression/cbmc-library/openat-01/main.c

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <fcntl.h>
2+
3+
int main()
4+
{
5+
int dirfd;
6+
char *unint_path;
7+
int flags;
8+
int fd = openat(dirfd, unint_path, flags);
9+
return 0;
10+
}

‎regression/cbmc-library/openat-01/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check --bounds-check
4+
dereference failure: pointer invalid in \*pathname: FAILURE$
5+
^VERIFICATION FAILED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring

‎src/ansi-c/library/fcntl.c

+164-2
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,179 @@
1-
/* FUNCTION: fcntl */
1+
/* FUNCTION: __CPROVER_fcntl */
22

33
#ifndef __CPROVER_FCNTL_H_INCLUDED
44
#include <fcntl.h>
55
#define __CPROVER_FCNTL_H_INCLUDED
66
#endif
77

8+
#ifndef __CPROVER_ERRNO_H_INCLUDED
9+
# include <errno.h>
10+
# define __CPROVER_ERRNO_H_INCLUDED
11+
#endif
12+
813
int __VERIFIER_nondet_int(void);
914

10-
int fcntl(int fd, int cmd, ...)
15+
int __CPROVER_fcntl(int fd, int cmd)
1116
{
1217
__CPROVER_HIDE:;
18+
if(fd < 0)
19+
{
20+
errno = EBADF;
21+
return -1;
22+
}
23+
1324
int return_value=__VERIFIER_nondet_int();
1425
(void)fd;
1526
(void)cmd;
1627
return return_value;
1728
}
29+
30+
/* FUNCTION: fcntl */
31+
32+
int __CPROVER_fcntl(int, int);
33+
34+
int fcntl(int fd, int cmd, ...)
35+
{
36+
return __CPROVER_fcntl(fd, cmd);
37+
}
38+
39+
/* FUNCTION: fcntl64 */
40+
41+
int __CPROVER_fcntl(int, int);
42+
43+
int fcntl64(int fd, int cmd, ...)
44+
{
45+
return __CPROVER_fcntl(fd, cmd);
46+
}
47+
48+
/* FUNCTION: __CPROVER_open */
49+
50+
#ifndef __CPROVER_FCNTL_H_INCLUDED
51+
# include <fcntl.h>
52+
# define __CPROVER_FCNTL_H_INCLUDED
53+
#endif
54+
55+
int __VERIFIER_nondet_int(void);
56+
57+
int __CPROVER_open(const char *pathname, int flags)
58+
{
59+
__CPROVER_HIDE:;
60+
int return_value = __VERIFIER_nondet_int();
61+
__CPROVER_assume(return_value >= -1);
62+
(void)*pathname;
63+
(void)flags;
64+
return return_value;
65+
}
66+
67+
/* FUNCTION: open */
68+
69+
int __CPROVER_open(const char *, int);
70+
71+
int open(const char *pathname, int flags, ...)
72+
{
73+
return __CPROVER_open(pathname, flags);
74+
}
75+
76+
/* FUNCTION: open64 */
77+
78+
int __CPROVER_open(const char *, int);
79+
80+
int open64(const char *pathname, int flags, ...)
81+
{
82+
return __CPROVER_open(pathname, flags);
83+
}
84+
85+
/* FUNCTION: __CPROVER_creat */
86+
87+
#ifndef __CPROVER_FCNTL_H_INCLUDED
88+
# include <fcntl.h>
89+
# define __CPROVER_FCNTL_H_INCLUDED
90+
#endif
91+
92+
int __VERIFIER_nondet_int(void);
93+
94+
int __CPROVER_creat(const char *pathname, mode_t mode)
95+
{
96+
__CPROVER_HIDE:;
97+
int return_value = __VERIFIER_nondet_int();
98+
__CPROVER_assume(return_value >= -1);
99+
(void)*pathname;
100+
(void)mode;
101+
return return_value;
102+
}
103+
104+
/* FUNCTION: creat */
105+
106+
#ifndef __CPROVER_FCNTL_H_INCLUDED
107+
# include <fcntl.h>
108+
# define __CPROVER_FCNTL_H_INCLUDED
109+
#endif
110+
111+
int __CPROVER_creat(const char *, mode_t);
112+
113+
int creat(const char *pathname, mode_t mode)
114+
{
115+
return __CPROVER_creat(pathname, mode);
116+
}
117+
118+
/* FUNCTION: creat64 */
119+
120+
#ifndef __CPROVER_FCNTL_H_INCLUDED
121+
# include <fcntl.h>
122+
# define __CPROVER_FCNTL_H_INCLUDED
123+
#endif
124+
125+
int __CPROVER_creat(const char *, mode_t);
126+
127+
int creat64(const char *pathname, mode_t mode)
128+
{
129+
return __CPROVER_creat(pathname, mode);
130+
}
131+
132+
/* FUNCTION: __CPROVER_openat */
133+
134+
#ifndef __CPROVER_FCNTL_H_INCLUDED
135+
# include <fcntl.h>
136+
# define __CPROVER_FCNTL_H_INCLUDED
137+
#endif
138+
139+
#ifndef __CPROVER_ERRNO_H_INCLUDED
140+
# include <errno.h>
141+
# define __CPROVER_ERRNO_H_INCLUDED
142+
#endif
143+
144+
int __VERIFIER_nondet_int(void);
145+
146+
int __CPROVER_openat(int dirfd, const char *pathname, int flags)
147+
{
148+
__CPROVER_HIDE:;
149+
if(dirfd < 0)
150+
{
151+
errno = EBADF;
152+
return -1;
153+
}
154+
155+
int return_value = __VERIFIER_nondet_int();
156+
__CPROVER_assume(return_value >= -1);
157+
(void)dirfd;
158+
(void)*pathname;
159+
(void)flags;
160+
return return_value;
161+
}
162+
163+
/* FUNCTION: openat */
164+
165+
int __CPROVER_openat(int dirfd, const char *pathname, int flags);
166+
167+
int openat(int dirfd, const char *pathname, int flags, ...)
168+
{
169+
return __CPROVER_openat(dirfd, pathname, flags);
170+
}
171+
172+
/* FUNCTION: openat64 */
173+
174+
int __CPROVER_openat(int dirfd, const char *pathname, int flags);
175+
176+
int openat64(int dirfd, const char *pathname, int flags, ...)
177+
{
178+
return __CPROVER_openat(dirfd, pathname, flags);
179+
}

‎src/ansi-c/library_check.sh

+2
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,8 @@ perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
5252
perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD
5353

5454
# Some functions are covered by existing tests:
55+
perl -p -i -e 's/^__CPROVER_(creat|fcntl|open|openat)\n//' __functions # creat, fcntl, open, openat
56+
perl -p -i -e 's/^(creat|fcntl|open|openat)64\n//' __functions # same as creat, fcntl, open, openat
5557
perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
5658
perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01
5759
perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen

0 commit comments

Comments
 (0)