cprover
system_library_symbols.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Programs
4
5Author: Thomas Kiley
6
7\*******************************************************************/
8
11
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}
unsignedbv_typet size_type()
Definition: c_types.cpp:68
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const irep_idt & get_file() const
Symbol table entry.
Definition: symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
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.
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 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.
std::map< irep_idt, irep_idt > system_library_map
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,...
The type of an expression, extends irept.
Definition: type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
Symbol table entry.
Defines typet, type_with_subtypet and type_with_subtypest.