Skip to content

Commit d6f0ed8

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 41496b9 commit d6f0ed8

File tree

10 files changed

+310
-5
lines changed

10 files changed

+310
-5
lines changed

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

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <fcntl.h>
2+
3+
#ifdef _WIN32
4+
# define MODE_T int
5+
#else
6+
# define MODE_T mode_t
7+
#endif
8+
9+
int main()
10+
{
11+
char *unint_path;
12+
MODE_T mode;
13+
int fd = creat(unint_path, mode);
14+
return 0;
15+
}

‎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

+237-2
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,252 @@
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: _fcntl */
40+
41+
int __CPROVER_fcntl(int, int);
42+
43+
int _fcntl(int fd, int cmd, ...)
44+
{
45+
return __CPROVER_fcntl(fd, cmd);
46+
}
47+
48+
/* FUNCTION: fcntl64 */
49+
50+
int __CPROVER_fcntl(int, int);
51+
52+
int fcntl64(int fd, int cmd, ...)
53+
{
54+
return __CPROVER_fcntl(fd, cmd);
55+
}
56+
57+
/* FUNCTION: __CPROVER_open */
58+
59+
#ifndef __CPROVER_FCNTL_H_INCLUDED
60+
# include <fcntl.h>
61+
# define __CPROVER_FCNTL_H_INCLUDED
62+
#endif
63+
64+
int __VERIFIER_nondet_int(void);
65+
66+
int __CPROVER_open(const char *pathname, int flags)
67+
{
68+
__CPROVER_HIDE:;
69+
int return_value = __VERIFIER_nondet_int();
70+
__CPROVER_assume(return_value >= -1);
71+
(void)*pathname;
72+
(void)flags;
73+
return return_value;
74+
}
75+
76+
/* FUNCTION: open */
77+
78+
int __CPROVER_open(const char *, int);
79+
80+
int open(const char *pathname, int flags, ...)
81+
{
82+
return __CPROVER_open(pathname, flags);
83+
}
84+
85+
/* FUNCTION: _open */
86+
87+
int __CPROVER_open(const char *, int);
88+
89+
int _open(const char *pathname, int flags, ...)
90+
{
91+
return __CPROVER_open(pathname, flags);
92+
}
93+
94+
/* FUNCTION: open64 */
95+
96+
int __CPROVER_open(const char *, int);
97+
98+
int open64(const char *pathname, int flags, ...)
99+
{
100+
return __CPROVER_open(pathname, flags);
101+
}
102+
103+
/* FUNCTION: __CPROVER_creat */
104+
105+
#ifndef __CPROVER_FCNTL_H_INCLUDED
106+
# include <fcntl.h>
107+
# define __CPROVER_FCNTL_H_INCLUDED
108+
#endif
109+
110+
#ifndef MODE_T
111+
# ifdef _WIN32
112+
# define MODE_T int
113+
# else
114+
# define MODE_T mode_t
115+
# endif
116+
#endif
117+
118+
int __VERIFIER_nondet_int(void);
119+
120+
int __CPROVER_creat(const char *pathname, MODE_T mode)
121+
{
122+
__CPROVER_HIDE:;
123+
int return_value = __VERIFIER_nondet_int();
124+
__CPROVER_assume(return_value >= -1);
125+
(void)*pathname;
126+
(void)mode;
127+
return return_value;
128+
}
129+
130+
/* FUNCTION: creat */
131+
132+
#ifndef __CPROVER_FCNTL_H_INCLUDED
133+
# include <fcntl.h>
134+
# define __CPROVER_FCNTL_H_INCLUDED
135+
#endif
136+
137+
#ifndef MODE_T
138+
# ifdef _WIN32
139+
# define MODE_T int
140+
# else
141+
# define MODE_T mode_t
142+
# endif
143+
#endif
144+
145+
int __CPROVER_creat(const char *, MODE_T);
146+
147+
int creat(const char *pathname, MODE_T mode)
148+
{
149+
return __CPROVER_creat(pathname, mode);
150+
}
151+
152+
/* FUNCTION: _creat */
153+
154+
#ifndef __CPROVER_FCNTL_H_INCLUDED
155+
# include <fcntl.h>
156+
# define __CPROVER_FCNTL_H_INCLUDED
157+
#endif
158+
159+
#ifndef MODE_T
160+
# ifdef _WIN32
161+
# define MODE_T int
162+
# else
163+
# define MODE_T mode_t
164+
# endif
165+
#endif
166+
167+
int __CPROVER_creat(const char *, MODE_T);
168+
169+
int _creat(const char *pathname, MODE_T mode)
170+
{
171+
return __CPROVER_creat(pathname, mode);
172+
}
173+
174+
/* FUNCTION: creat64 */
175+
176+
#ifndef __CPROVER_FCNTL_H_INCLUDED
177+
# include <fcntl.h>
178+
# define __CPROVER_FCNTL_H_INCLUDED
179+
#endif
180+
181+
#ifndef MODE_T
182+
# ifdef _WIN32
183+
# define MODE_T int
184+
# else
185+
# define MODE_T mode_t
186+
# endif
187+
#endif
188+
189+
int __CPROVER_creat(const char *, MODE_T);
190+
191+
int creat64(const char *pathname, MODE_T mode)
192+
{
193+
return __CPROVER_creat(pathname, mode);
194+
}
195+
196+
/* FUNCTION: __CPROVER_openat */
197+
198+
#ifndef __CPROVER_FCNTL_H_INCLUDED
199+
# include <fcntl.h>
200+
# define __CPROVER_FCNTL_H_INCLUDED
201+
#endif
202+
203+
#ifndef __CPROVER_ERRNO_H_INCLUDED
204+
# include <errno.h>
205+
# define __CPROVER_ERRNO_H_INCLUDED
206+
#endif
207+
208+
int __VERIFIER_nondet_int(void);
209+
210+
int __CPROVER_openat(int dirfd, const char *pathname, int flags)
211+
{
212+
__CPROVER_HIDE:;
213+
if(dirfd < 0)
214+
{
215+
errno = EBADF;
216+
return -1;
217+
}
218+
219+
int return_value = __VERIFIER_nondet_int();
220+
__CPROVER_assume(return_value >= -1);
221+
(void)dirfd;
222+
(void)*pathname;
223+
(void)flags;
224+
return return_value;
225+
}
226+
227+
/* FUNCTION: openat */
228+
229+
int __CPROVER_openat(int dirfd, const char *pathname, int flags);
230+
231+
int openat(int dirfd, const char *pathname, int flags, ...)
232+
{
233+
return __CPROVER_openat(dirfd, pathname, flags);
234+
}
235+
236+
/* FUNCTION: _openat */
237+
238+
int __CPROVER_openat(int dirfd, const char *pathname, int flags);
239+
240+
int _openat(int dirfd, const char *pathname, int flags, ...)
241+
{
242+
return __CPROVER_openat(dirfd, pathname, flags);
243+
}
244+
245+
/* FUNCTION: openat64 */
246+
247+
int __CPROVER_openat(int dirfd, const char *pathname, int flags);
248+
249+
int openat64(int dirfd, const char *pathname, int flags, ...)
250+
{
251+
return __CPROVER_openat(dirfd, pathname, flags);
252+
}

‎src/ansi-c/library_check.sh

+6
Original file line numberDiff line numberDiff line change
@@ -31,10 +31,14 @@ perl -p -i -e 's/^__CPROVER_contracts_library\n//' __functions
3131

3232
# Some functions are implicitly covered by running on different operating
3333
# systems:
34+
perl -p -i -e 's/^_creat\n//' __functions # creat, macOS
35+
perl -p -i -e 's/^_fcntl\n//' __functions # fcntl, macOS
3436
perl -p -i -e 's/^_fopen\n//' __functions # fopen, macOS
3537
perl -p -i -e 's/^_getopt\n//' __functions # getopt, macOS
3638
perl -p -i -e 's/^_mmap\n//' __functions # mmap, macOS
3739
perl -p -i -e 's/^_munmap\n//' __functions # mumap, macOS
40+
perl -p -i -e 's/^_open\n//' __functions # open, macOS
41+
perl -p -i -e 's/^_openat\n//' __functions # openat, macOS
3842
perl -p -i -e 's/^_pipe\n//' __functions # pipe, macOS
3943
perl -p -i -e 's/^_setjmp\n//' __functions # pipe, macOS
4044
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
5256
perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD
5357

5458
# Some functions are covered by existing tests:
59+
perl -p -i -e 's/^__CPROVER_(creat|fcntl|open|openat)\n//' __functions # creat, fcntl, open, openat
60+
perl -p -i -e 's/^(creat|fcntl|open|openat)64\n//' __functions # same as creat, fcntl, open, openat
5561
perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
5662
perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01
5763
perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen

0 commit comments

Comments
 (0)