CBMC
unistd.c
Go to the documentation of this file.
1 /* FUNCTION: sleep */
2 
4 
5 unsigned int sleep(unsigned int seconds)
6 {
7  __CPROVER_HIDE:;
8  // do nothing, but return nondet value
9  unsigned remaining_time=__VERIFIER_nondet_unsigned();
10  __CPROVER_assume(remaining_time <= seconds);
11 
12  return remaining_time;
13 }
14 
15 /* FUNCTION: _sleep */
16 
17 unsigned int sleep(unsigned int seconds);
18 
19 unsigned int _sleep(unsigned int seconds)
20 {
21  __CPROVER_HIDE:;
22  return sleep(seconds);
23 }
24 
25 /* FUNCTION: usleep */
26 
27 #ifndef __CPROVER_ERRNO_H_INCLUDED
28 # include <errno.h>
29 # define __CPROVER_ERRNO_H_INCLUDED
30 #endif
31 
32 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
33 
34 int usleep(unsigned int usec)
35 {
36 __CPROVER_HIDE:;
37  // do nothing, but return nondet value
38  __CPROVER_bool error = __VERIFIER_nondet___CPROVER_bool();
39  if(error)
40  {
41  if(usec >= 1000000)
42  errno = EINVAL;
43  else
44  errno = EINTR;
45  return -1;
46  }
47  return 0;
48 }
49 
50 /* FUNCTION: _usleep */
51 
52 int usleep(unsigned int);
53 
54 int _usleep(unsigned int usec)
55 {
56 __CPROVER_HIDE:;
57  return usleep(usec);
58 }
59 
60 /* FUNCTION: unlink */
61 
63 
64 int unlink(const char *s)
65 {
66  __CPROVER_HIDE:;
67  (void)*s;
68  #ifdef __CPROVER_STRING_ABSTRACTION
70  "unlink zero-termination");
71  #endif
72  int retval=__VERIFIER_nondet_int();
73  return retval;
74 }
75 
76 /* FUNCTION: pipe */
77 
78 #ifndef __CPROVER_ERRNO_H_INCLUDED
79 #include <errno.h>
80 #define __CPROVER_ERRNO_H_INCLUDED
81 #endif
82 
84 // offset to make sure we don't collide with other fds
85 extern const int __CPROVER_pipe_offset;
86 unsigned __CPROVER_pipe_count = 0;
87 
88 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
89 
90 int pipe(int fildes[2])
91 {
92  __CPROVER_HIDE:;
93  __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
94  if(error)
95  {
96  errno = __VERIFIER_nondet___CPROVER_bool() ? EMFILE : ENFILE;
97  return -1;
98  }
99 
111 
112  __CPROVER_assume(fildes[0]!=0 && fildes[0]!=1 && fildes[0]!=2);
113  __CPROVER_assume(fildes[1]!=0 && fildes[1]!=1 && fildes[1]!=2);
114 
115  return 0;
116 }
117 
118 /* FUNCTION: _pipe */
119 
120 #ifdef _WIN32
121 #undef pipe
122 int pipe(int fildes[2]);
123 
124 int _pipe(int *pfds, unsigned int psize, int textmode)
125 {
126 __CPROVER_HIDE:;
127  (void)psize;
128  (void)textmode;
129  return pipe(pfds);
130 }
131 #endif
132 
133 /* FUNCTION: close */
134 
136 // offset to make sure we don't collide with other fds
137 extern const int __CPROVER_pipe_offset;
138 
139 int close(int fildes)
140 {
141  __CPROVER_HIDE:;
142  if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
143  return 0;
144 
146 
147  int retval=-1;
148  fildes-=__CPROVER_pipe_offset;
149  if(fildes%2==1)
150  --fildes;
152  if(!__CPROVER_pipes[fildes].widowed)
153  {
154  __CPROVER_pipes[fildes].widowed=1;
156  retval=0;
157  }
159  return retval;
160 }
161 
162 /* FUNCTION: _close */
163 
164 int close(int fildes);
165 
166 int _close(int fildes)
167 {
168  __CPROVER_HIDE:;
169  return close(fildes);
170 }
171 
172 /* FUNCTION: write */
173 
174 // do not include unistd.h as this might trigger GCC asm renaming of
175 // write to _write; this is covered by the explicit definition of
176 // _write below
177 #ifdef _MSC_VER
178 #define ret_type int
179 #define size_type unsigned
180 #else
181 #ifndef __CPROVER_SYS_TYPES_H_INCLUDED
182 #include <sys/types.h>
183 #define __CPROVER_SYS_TYPES_H_INCLUDED
184 #endif
185 #define ret_type ssize_t
186 #define size_type size_t
187 #endif
188 
190 // offset to make sure we don't collide with other fds
191 extern const int __CPROVER_pipe_offset;
192 
194 
195 ret_type write(int fildes, const void *buf, size_type nbyte)
196 {
197  __CPROVER_HIDE:;
198  if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
199  {
201  __CPROVER_assume(retval>=-1 && retval<=(ret_type)nbyte);
202  return retval;
203  }
204 
206 
207  int retval=-1;
208  fildes-=__CPROVER_pipe_offset;
209  if(fildes%2==1)
210  --fildes;
212  if(
213  !__CPROVER_pipes[fildes].widowed &&
214  __CPROVER_pipes[fildes].next_avail >= 0 &&
215  sizeof(__CPROVER_pipes[fildes].data) >=
216  __CPROVER_pipes[fildes].next_avail + nbyte)
217  {
218  for(size_type i=0; i<nbyte; ++i)
219  __CPROVER_pipes[fildes].data[i+__CPROVER_pipes[fildes].next_avail]=
220  ((char*)buf)[i];
221  __CPROVER_pipes[fildes].next_avail+=nbyte;
222  retval=nbyte;
223  }
225  return retval;
226 }
227 
228 /* FUNCTION: _write */
229 
230 #ifdef _MSC_VER
231 #define ret_type int
232 #define size_type unsigned
233 #else
234 #ifndef __CPROVER_SYS_TYPES_H_INCLUDED
235 #include <sys/types.h>
236 #define __CPROVER_SYS_TYPES_H_INCLUDED
237 #endif
238 #define ret_type ssize_t
239 #define size_type size_t
240 #endif
241 
242 ret_type write(int fildes, const void *buf, size_type nbyte);
243 
244 ret_type _write(int fildes, const void *buf, size_type nbyte)
245 {
246  __CPROVER_HIDE:;
247  return write(fildes, buf, nbyte);
248 }
249 
250 /* FUNCTION: read */
251 
252 // do not include unistd.h as this might trigger GCC asm renaming of
253 // read to _read; this is covered by the explicit definition of _read
254 // below
255 #ifdef _MSC_VER
256 #define ret_type int
257 #define size_type unsigned
258 #else
259 #ifndef __CPROVER_SYS_TYPES_H_INCLUDED
260 #include <sys/types.h>
261 #define __CPROVER_SYS_TYPES_H_INCLUDED
262 #endif
263 #define ret_type ssize_t
264 #define size_type size_t
265 #endif
266 
268 // offset to make sure we don't collide with other fds
269 extern const int __CPROVER_pipe_offset;
270 
271 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
274 
275 ret_type read(int fildes, void *buf, size_type nbyte)
276 {
277  __CPROVER_HIDE:;
278  if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
279  {
281  __CPROVER_assume(0<=nread && (size_type)nread<=nbyte);
282 
283  __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
284 #if 0
285  size_type i;
286  for(i=0; i<nbyte; i++)
287  {
288  char nondet_char;
289  ((char *)buf)[i]=nondet_char;
290  }
291 #else
292  if(nbyte>0)
293  {
295  __CPROVER_assume(error ? str_length<=nbyte : str_length==nbyte);
296  // check that the memory is accessible
297  (void)*(char *)buf;
298  (void)*(((const char *)buf) + str_length - 1);
299  char contents_nondet[str_length];
300  __CPROVER_array_replace((char*)buf, contents_nondet);
301  }
302 #endif
303 
304  return error ? -1 : nread;
305  }
306 
308 
309  int retval=0;
310  fildes-=__CPROVER_pipe_offset;
311  if(fildes%2==1)
312  --fildes;
314  if(
315  !__CPROVER_pipes[fildes].widowed &&
316  __CPROVER_pipes[fildes].next_unread >= 0)
317  {
318  for(size_type i=0; i<nbyte &&
319  __CPROVER_pipes[fildes].next_unread <
320  __CPROVER_pipes[fildes].next_avail;
321  ++i)
322  {
323  ((char*)buf)[i]=__CPROVER_pipes[fildes].
325  ++__CPROVER_pipes[fildes].next_unread;
326  ++retval;
327  }
328  if(__CPROVER_pipes[fildes].next_avail==
331  }
333  return retval;
334 }
335 
336 /* FUNCTION: _read */
337 
338 #ifdef _MSC_VER
339 #define ret_type int
340 #define size_type unsigned
341 #else
342 #ifndef __CPROVER_SYS_TYPES_H_INCLUDED
343 #include <sys/types.h>
344 #define __CPROVER_SYS_TYPES_H_INCLUDED
345 #endif
346 #define ret_type ssize_t
347 #define size_type size_t
348 #endif
349 
350 ret_type read(int fildes, void *buf, size_type nbyte);
351 
352 ret_type _read(int fildes, void *buf, size_type nbyte)
353 {
354  __CPROVER_HIDE:;
355  return read(fildes, buf, nbyte);
356 }
357 
358 /* FUNCTION: sysconf */
359 
360 #ifndef __CPROVER_ERRNO_H_INCLUDED
361 # include <errno.h>
362 # define __CPROVER_ERRNO_H_INCLUDED
363 #endif
364 
366 int __VERIFIER_nondet_int(void);
367 
368 long sysconf(int name);
369 
370 // This overapproximation is based on the sysconf specification available at
371 // https://pubs.opengroup.org/onlinepubs/9699919799/functions/sysconf.html.
372 long sysconf(int name)
373 {
374 __CPROVER_HIDE:;
375  (void)name;
376  long retval = __VERIFIER_nondet_long();
377 
378  // We should keep errno as non-deterministic as possible, since this model
379  // never takes into account the name input.
380  errno = __VERIFIER_nondet_int();
381 
382  // Spec states "some returned values may be huge; they are not suitable
383  // for allocating memory". There aren't also guarantees about return
384  // values being strictly equal or greater to -1.
385  // Thus, modelling it as non-deterministic.
386  return retval;
387 }
#define __CPROVER_constant_infinity_uint
Definition: cprover.h:21
void __CPROVER_array_replace(const void *dest, const void *src)
void __CPROVER_precondition(__CPROVER_bool precondition, const char *description)
_Bool __CPROVER_is_zero_string(const void *)
void __CPROVER_atomic_begin(void)
void __CPROVER_atomic_end(void)
void __CPROVER_assume(__CPROVER_bool assumption)
short next_unread
Definition: cprover.h:43
short next_avail
Definition: cprover.h:42
_Bool widowed
Definition: cprover.h:40
char data[4]
Definition: cprover.h:41
int _usleep(unsigned int usec)
Definition: unistd.c:54
int __VERIFIER_nondet_int(void)
unsigned __VERIFIER_nondet_unsigned(void)
#define ret_type
Definition: unistd.c:346
unsigned int _sleep(unsigned int seconds)
Definition: unistd.c:19
size_t __VERIFIER_nondet_size_type(void)
int _close(int fildes)
Definition: unistd.c:166
ssize_t _write(int fildes, const void *buf, size_t nbyte)
Definition: unistd.c:244
long sysconf(int name)
Definition: unistd.c:372
unsigned int sleep(unsigned int seconds)
Definition: unistd.c:5
ssize_t _read(int fildes, void *buf, size_t nbyte)
Definition: unistd.c:352
unsigned __CPROVER_pipe_count
Definition: unistd.c:86
ssize_t __VERIFIER_nondet_ret_type(void)
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void)
const int __CPROVER_pipe_offset
Definition: unistd.c:137
int usleep(unsigned int usec)
Definition: unistd.c:34
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition: unistd.c:195
int close(int fildes)
Definition: unistd.c:139
#define size_type
Definition: unistd.c:347
ssize_t read(int fildes, void *buf, size_t nbyte)
Definition: unistd.c:275
int pipe(int fildes[2])
Definition: unistd.c:90
int unlink(const char *s)
Definition: unistd.c:64
struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]
Definition: unistd.c:135
long __VERIFIER_nondet_long(void)