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 
264  const typet &type,
265  std::set<std::string> &out_system_headers) const
266 {
267  symbolt symbol;
268  symbol.type=type;
269  return is_symbol_internal_symbol(symbol, out_system_headers);
270 }
271 
278  const symbolt &symbol,
279  std::set<std::string> &out_system_headers) const
280 {
281  const std::string &name_str=id2string(symbol.name);
282 
283  if(has_prefix(name_str, CPROVER_PREFIX) ||
284  name_str=="__func__" ||
285  name_str=="__FUNCTION__" ||
286  name_str=="__PRETTY_FUNCTION__" ||
287  name_str=="argc'" ||
288  name_str=="argv'" ||
289  name_str=="envp'" ||
290  name_str=="envp_size'")
291  return true;
292 
293  if(has_suffix(name_str, "$object"))
294  return true;
295 
296  // exclude nondet instructions
297  if(has_prefix(name_str, "nondet_"))
298  {
299  return true;
300  }
301 
302  if(has_prefix(name_str, "__VERIFIER"))
303  {
304  return true;
305  }
306 
307  const std::string &file_str=id2string(symbol.location.get_file());
308 
309  // don't dump internal GCC builtins
310  if(has_prefix(file_str, "gcc_builtin_headers_") &&
311  has_prefix(name_str, "__builtin_"))
312  return true;
313 
314  if(name_str=="__builtin_va_start" ||
315  name_str=="__builtin_va_end" ||
316  symbol.name==ID_gcc_builtin_va_arg)
317  {
318  out_system_headers.insert("stdarg.h");
319  return true;
320  }
321 
322  // don't dump asserts
323  else if(name_str=="__assert_fail" ||
324  name_str=="_assert" ||
325  name_str=="__assert_c99" ||
326  name_str=="_wassert")
327  {
328  return true;
329  }
330 
331  const auto &it=system_library_map.find(symbol.name);
332 
333  if(it!=system_library_map.end())
334  {
335  out_system_headers.insert(id2string(it->second));
336  return true;
337  }
338 
339  if(use_all_headers &&
340  has_prefix(file_str, "/usr/include/"))
341  {
342  if(file_str.find("/bits/")==std::string::npos)
343  {
344  // Do not include transitive includes of system headers!
345  std::string::size_type prefix_len=std::string("/usr/include/").size();
346  out_system_headers.insert(file_str.substr(prefix_len));
347  }
348 
349  return true;
350  }
351 
352  return false;
353 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
prefix.h
system_library_symbolst::init_system_library_map
void init_system_library_map()
To generate a map of header file names -> list of symbols The symbol names are reserved as the header...
Definition: system_library_symbols.cpp:30
irep_idt
dstringt irep_idt
Definition: irep.h:32
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
system_library_symbolst::use_all_headers
bool use_all_headers
Definition: system_library_symbols.h:56
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
system_library_symbolst::is_type_internal
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,...
Definition: system_library_symbols.cpp:263
system_library_symbols.h
Goto Programs.
system_library_symbolst::system_library_symbolst
system_library_symbolst()
Definition: system_library_symbols.h:30
symbol.h
Symbol table entry.
cprover_prefix.h
system_library_symbolst::system_library_map
std::map< irep_idt, irep_idt > system_library_map
Definition: system_library_symbols.h:55
suffix.h
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
system_library_symbolst::is_symbol_internal_symbol
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.
Definition: system_library_symbols.cpp:277
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
system_library_symbolst::add_to_system_library
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.
Definition: system_library_symbols.cpp:246
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40