cprover
system_library_symbols.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs
4 
5 Author: Thomas Kiley
6 
7 \*******************************************************************/
8 
11 
12 #include "system_library_symbols.h"
13 #include <util/cprover_prefix.h>
14 #include <util/prefix.h>
15 #include <util/suffix.h>
16 #include <util/symbol.h>
17 #include <util/type.h>
18 #include <sstream>
19 
21  use_all_headers(false)
22 {
23  if(init)
25 }
26 
31 {
32  // ctype.h
33  std::list<irep_idt> ctype_syms=
34  {
35  "isalnum", "isalpha", "isblank", "iscntrl", "isdigit", "isgraph",
36  "islower", "isprint", "ispunct", "isspace", "isupper", "isxdigit",
37  "tolower", "toupper"
38  };
39  add_to_system_library("ctype.h", ctype_syms);
40 
41  // fcntl.h
42  std::list<irep_idt> fcntl_syms=
43  {
44  "creat", "fcntl", "open"
45  };
46  add_to_system_library("fcntl.h", fcntl_syms);
47 
48  // locale.h
49  std::list<irep_idt> locale_syms=
50  {
51  "setlocale"
52  };
53  add_to_system_library("locale.h", locale_syms);
54 
55  // math.h
56  std::list<irep_idt> math_syms=
57  {
58  "acos", "acosh", "asin", "asinh", "atan", "atan2", "atanh",
59  "cbrt", "ceil", "copysign", "cos", "cosh", "erf", "erfc", "exp",
60  "exp2", "expm1", "fabs", "fdim", "floor", "fma", "fmax", "fmin",
61  "fmod", "fpclassify", "fpclassifyl", "fpclassifyf", "frexp",
62  "hypot", "ilogb", "isfinite", "isinf", "isnan", "isnormal",
63  "j0", "j1", "jn", "ldexp", "lgamma", "llrint", "llround", "log",
64  "log10", "log1p", "log2", "logb", "lrint", "lround", "modf", "nan",
65  "nearbyint", "nextafter", "pow", "remainder", "remquo", "rint",
66  "round", "scalbln", "scalbn", "signbit", "sin", "sinh", "sqrt",
67  "tan", "tanh", "tgamma", "trunc", "y0", "y1", "yn", "isinff",
68  "isinfl", "isnanf", "isnanl"
69  };
70  add_to_system_library("math.h", math_syms);
71 
72  // for some reason the math functions can sometimes be prefixed with
73  // a double underscore
74  std::list<irep_idt> underscore_math_syms;
75  for(const irep_idt &math_sym : math_syms)
76  {
77  std::ostringstream underscore_id;
78  underscore_id << "__" << math_sym;
79  underscore_math_syms.push_back(irep_idt(underscore_id.str()));
80  }
81  add_to_system_library("math.h", underscore_math_syms);
82 
83  // pthread.h
84  std::list<irep_idt> pthread_syms=
85  {
86  "pthread_cleanup_pop", "pthread_cleanup_push",
87  "pthread_cond_broadcast", "pthread_cond_destroy",
88  "pthread_cond_init", "pthread_cond_signal",
89  "pthread_cond_timedwait", "pthread_cond_wait", "pthread_create",
90  "pthread_detach", "pthread_equal", "pthread_exit",
91  "pthread_getspecific", "pthread_join", "pthread_key_delete",
92  "pthread_mutex_destroy", "pthread_mutex_init",
93  "pthread_mutex_lock", "pthread_mutex_trylock",
94  "pthread_mutex_unlock", "pthread_once", "pthread_rwlock_destroy",
95  "pthread_rwlock_init", "pthread_rwlock_rdlock",
96  "pthread_rwlock_unlock", "pthread_rwlock_wrlock",
97  "pthread_rwlockattr_destroy", "pthread_rwlockattr_getpshared",
98  "pthread_rwlockattr_init", "pthread_rwlockattr_setpshared",
99  "pthread_self", "pthread_setspecific",
100  /* non-public struct types */
101  "tag-__pthread_internal_list", "tag-__pthread_mutex_s",
102  "pthread_mutex_t"
103  };
104  add_to_system_library("pthread.h", pthread_syms);
105 
106  // setjmp.h
107  std::list<irep_idt> setjmp_syms=
108  {
109  "_longjmp", "_setjmp", "jmp_buf", "longjmp", "longjmperror", "setjmp",
110  "siglongjmp", "sigsetjmp"
111  };
112  add_to_system_library("setjmp.h", setjmp_syms);
113 
114  // stdio.h
115  std::list<irep_idt> stdio_syms=
116  {
117  "asprintf", "clearerr", "fclose", "fdopen", "feof", "ferror",
118  "fflush", "fgetc", "fgetln", "fgetpos", "fgets", "fgetwc",
119  "fgetws", "fileno", "fopen", "fprintf", "fpurge", "fputc",
120  "fputs", "fputwc", "fputws", "fread", "freopen", "fropen",
121  "fscanf", "fseek", "fsetpos", "ftell", "funopen", "fwide",
122  "fwopen", "fwprintf", "fwrite", "getc", "getchar", "getdelim",
123  "getline", "gets", "getw", "getwc", "getwchar", "mkdtemp",
124  "mkstemp", "mktemp", "perror", "printf", "putc", "putchar",
125  "puts", "putw", "putwc", "putwchar", "remove", "rewind", "scanf",
126  "setbuf", "setbuffer", "setlinebuf", "setvbuf", "snprintf",
127  "sprintf", "sscanf", "swprintf", "sys_errlist",
128  "sys_nerr", "tempnam", "tmpfile", "tmpnam", "ungetc", "ungetwc",
129  "vasprintf", "vfprintf", "vfscanf", "vfwprintf", "vprintf",
130  "vscanf", "vsnprintf", "vsprintf", "vsscanf", "vswprintf",
131  "vwprintf", "wprintf",
132  /* non-public struct types */
133  "tag-__sFILE", "tag-__sbuf", // OS X
134  "tag-_IO_FILE", "tag-_IO_marker", // Linux
135  };
136  add_to_system_library("stdio.h", stdio_syms);
137 
138  // stdlib.h
139  std::list<irep_idt> stdlib_syms=
140  {
141  "abort", "abs", "atexit", "atof", "atoi", "atol", "atoll",
142  "bsearch", "calloc", "div", "exit", "free", "getenv", "labs",
143  "ldiv", "llabs", "lldiv", "malloc", "mblen", "mbstowcs", "mbtowc",
144  "qsort", "rand", "realloc", "srand", "strtod", "strtof", "strtol",
145  "strtold", "strtoll", "strtoul", "strtoull", "system", "wcstombs",
146  "wctomb"
147  };
148  add_to_system_library("stdlib.h", stdlib_syms);
149 
150  // string.h
151  std::list<irep_idt> string_syms=
152  {
153  "strcat", "strncat", "strchr", "strrchr", "strcmp", "strncmp",
154  "strcpy", "strncpy", "strerror", "strlen", "strpbrk", "strspn",
155  "strcspn", "strstr", "strtok", "strcasecmp", "strncasecmp", "strdup",
156  "memset"
157  };
158  add_to_system_library("string.h", string_syms);
159 
160  // time.h
161  std::list<irep_idt> time_syms=
162  {
163  "asctime", "asctime_r", "ctime", "ctime_r", "difftime", "gmtime",
164  "gmtime_r", "localtime", "localtime_r", "mktime", "strftime",
165  /* non-public struct types */
166  "tag-timespec", "tag-timeval", "tag-tm"
167  };
168  add_to_system_library("time.h", time_syms);
169 
170  // unistd.h
171  std::list<irep_idt> unistd_syms=
172  {
173  "_exit", "access", "alarm", "chdir", "chown", "close", "dup",
174  "dup2", "execl", "execle", "execlp", "execv", "execve", "execvp",
175  "fork", "fpathconf", "getcwd", "getegid", "geteuid", "getgid",
176  "getgroups", "getlogin", "getpgrp", "getpid", "getppid", "getuid",
177  "isatty", "link", "lseek", "pathconf", "pause", "pipe", "read",
178  "rmdir", "setgid", "setpgid", "setsid", "setuid", "sleep",
179  "sysconf", "tcgetpgrp", "tcsetpgrp", "ttyname", "ttyname_r",
180  "unlink", "write"
181  };
182  add_to_system_library("unistd.h", unistd_syms);
183 
184  // sys/select.h
185  std::list<irep_idt> sys_select_syms=
186  {
187  "select",
188  /* non-public struct types */
189  "fd_set"
190  };
191  add_to_system_library("sys/select.h", sys_select_syms);
192 
193  // sys/socket.h
194  std::list<irep_idt> sys_socket_syms=
195  {
196  "accept", "bind", "connect",
197  /* non-public struct types */
198  "tag-sockaddr"
199  };
200  add_to_system_library("sys/socket.h", sys_socket_syms);
201 
202  // sys/stat.h
203  std::list<irep_idt> sys_stat_syms=
204  {
205  "fstat", "lstat", "stat",
206  /* non-public struct types */
207  "tag-stat"
208  };
209  add_to_system_library("sys/stat.h", sys_stat_syms);
210 
211  std::list<irep_idt> fenv_syms=
212  {
213  "fenv_t", "fexcept_t", "feclearexcept", "fegetexceptflag",
214  "feraiseexcept", "fesetexceptflag", "fetestexcept",
215  "fegetround", "fesetround", "fegetenv", "feholdexcept",
216  "fesetenv", "feupdateenv"
217  };
218  add_to_system_library("fenv.h", fenv_syms);
219 
220  std::list<irep_idt> errno_syms=
221  {
222  "__error", "__errno_location", "__errno"
223  };
224  add_to_system_library("errno.h", errno_syms);
225 
226 #if 0
227  // sys/types.h
228  std::list<irep_idt> sys_types_syms=
229  {
230  };
231  add_to_system_library("sys/types.h", sys_types_syms);
232 #endif
233 
234  // sys/wait.h
235  std::list<irep_idt> sys_wait_syms=
236  {
237  "wait", "waitpid"
238  };
239  add_to_system_library("sys/wait.h", sys_wait_syms);
240 }
241 
247  irep_idt header_file,
248  std::list<irep_idt> symbols)
249 {
250  for(const irep_idt &symbol : symbols)
251  {
252  system_library_map[symbol]=header_file;
253  }
254 }
255 
263  const typet &type,
264  std::set<std::string> &out_system_headers) const
265 {
266  symbolt symbol;
267  symbol.type=type;
268  return is_symbol_internal_symbol(symbol, out_system_headers);
269 }
270 
276  const symbolt &symbol,
277  std::set<std::string> &out_system_headers) const
278 {
279  const std::string &name_str=id2string(symbol.name);
280 
281  if(has_prefix(name_str, CPROVER_PREFIX) ||
282  name_str=="__func__" ||
283  name_str=="__FUNCTION__" ||
284  name_str=="__PRETTY_FUNCTION__" ||
285  name_str=="argc'" ||
286  name_str=="argv'" ||
287  name_str=="envp'" ||
288  name_str=="envp_size'")
289  return true;
290 
291  if(has_suffix(name_str, "$object"))
292  return true;
293 
294  // exclude nondet instructions
295  if(has_prefix(name_str, "nondet_"))
296  {
297  return true;
298  }
299 
300  if(has_prefix(name_str, "__VERIFIER"))
301  {
302  return true;
303  }
304 
305  const std::string &file_str=id2string(symbol.location.get_file());
306 
307  // don't dump internal GCC builtins
308  if(has_prefix(file_str, "gcc_builtin_headers_") &&
309  has_prefix(name_str, "__builtin_"))
310  return true;
311 
312  if(name_str=="__builtin_va_start" ||
313  name_str=="__builtin_va_end" ||
314  symbol.name==ID_gcc_builtin_va_arg)
315  {
316  out_system_headers.insert("stdarg.h");
317  return true;
318  }
319 
320  // don't dump asserts
321  else if(name_str=="__assert_fail" ||
322  name_str=="_assert" ||
323  name_str=="__assert_c99" ||
324  name_str=="_wassert")
325  {
326  return true;
327  }
328 
329  const auto &it=system_library_map.find(symbol.name);
330 
331  if(it!=system_library_map.end())
332  {
333  out_system_headers.insert(id2string(it->second));
334  return true;
335  }
336 
337  if(use_all_headers &&
338  has_prefix(file_str, "/usr/include/"))
339  {
340  if(file_str.find("/bits/")==std::string::npos)
341  {
342  // Do not include transitive includes of system headers!
343  std::string::size_type prefix_len=std::string("/usr/include/").size();
344  out_system_headers.insert(file_str.substr(prefix_len));
345  }
346 
347  return true;
348  }
349 
350  return false;
351 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
#define CPROVER_PREFIX
bool is_symbol_internal_symbol(const symbolt &symbol, std::set< std::string > &out_system_headers) const
To find out if a symbol is an internal symbol.
unsignedbv_typet size_type()
Definition: c_types.cpp:58
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
bool is_type_internal(const typet &type, std::set< std::string > &out_system_headers) const
Helper function to call is_symbol_internal_symbol on a nameless fake symbol with the given type...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
const irep_idt & get_file() const
void init_system_library_map()
To generate a map of header file names -> list of symbols The symbol names are reserved as the header...
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
dstringt irep_idt
Definition: irep.h:32
void add_to_system_library(irep_idt header_file, std::list< irep_idt > symbols)
To add the symbols from a specific header file to the system library map.
std::map< irep_idt, irep_idt > system_library_map