cprover
ansi_c_internal_additions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <util/config.h>
12 
14 "# 1 \"gcc_builtin_headers_generic.h\"\n"
15 #include "gcc_builtin_headers_generic.inc"
16 ; // NOLINT(whitespace/semicolon)
17 
19 "# 1 \"gcc_builtin_headers_math.h\"\n"
20 #include "gcc_builtin_headers_math.inc"
21 ; // NOLINT(whitespace/semicolon)
22 
24 "# 1 \"gcc_builtin_headers_mem_string.h\"\n"
25 #include "gcc_builtin_headers_mem_string.inc"
26 ; // NOLINT(whitespace/semicolon)
27 
29 "# 1 \"gcc_builtin_headers_omp.h\"\n"
30 #include "gcc_builtin_headers_omp.inc"
31 ; // NOLINT(whitespace/semicolon)
32 
34 "# 1 \"gcc_builtin_headers_tm.h\"\n"
35 #include "gcc_builtin_headers_tm.inc"
36 ; // NOLINT(whitespace/semicolon)
37 
39 "# 1 \"gcc_builtin_headers_ubsan.h\"\n"
40 #include "gcc_builtin_headers_ubsan.inc"
41 ; // NOLINT(whitespace/semicolon)
42 
44 "# 1 \"gcc_builtin_headers_ia32.h\"\n"
45 #include "gcc_builtin_headers_ia32.inc"
46 ; // NOLINT(whitespace/semicolon)
48 #include "gcc_builtin_headers_ia32-2.inc"
49 ; // NOLINT(whitespace/semicolon)
51 #include "gcc_builtin_headers_ia32-3.inc"
52 ; // NOLINT(whitespace/semicolon)
54 #include "gcc_builtin_headers_ia32-4.inc"
55 ; // NOLINT(whitespace/semicolon)
56 
58 "# 1 \"gcc_builtin_headers_alpha.h\"\n"
59 #include "gcc_builtin_headers_alpha.inc"
60 ; // NOLINT(whitespace/semicolon)
61 
63 "# 1 \"gcc_builtin_headers_arm.h\"\n"
64 #include "gcc_builtin_headers_arm.inc"
65 ; // NOLINT(whitespace/semicolon)
66 
68 "# 1 \"gcc_builtin_headers_mips.h\"\n"
69 #include "gcc_builtin_headers_mips.inc"
70 ; // NOLINT(whitespace/semicolon)
71 
73 "# 1 \"gcc_builtin_headers_power.h\"\n"
74 #include "gcc_builtin_headers_power.inc"
75 ; // NOLINT(whitespace/semicolon)
76 
77 const char arm_builtin_headers[]=
78 "# 1 \"arm_builtin_headers.h\"\n"
79 #include "arm_builtin_headers.inc"
80 ; // NOLINT(whitespace/semicolon)
81 
82 const char cw_builtin_headers[]=
83 "# 1 \"cw_builtin_headers.h\"\n"
84 #include "cw_builtin_headers.inc"
85 ; // NOLINT(whitespace/semicolon)
86 
87 const char clang_builtin_headers[]=
88 "# 1 \"clang_builtin_headers.h\"\n"
89 #include "clang_builtin_headers.inc"
90 ; // NOLINT(whitespace/semicolon)
91 
92 static std::string architecture_string(const std::string &value, const char *s)
93 {
94  return std::string("const char *__CPROVER_architecture_")+
95  std::string(s)+
96  "=\""+value+"\";\n";
97 }
98 
99 static std::string architecture_string(int value, const char *s)
100 {
101  return std::string("const int __CPROVER_architecture_")+
102  std::string(s)+
103  "="+std::to_string(value)+";\n";
104 }
105 
106 void ansi_c_internal_additions(std::string &code)
107 {
108  code+=
109  "# 1 \"<built-in-additions>\"\n"
110  "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
111  "void __CPROVER_assume(__CPROVER_bool assumption);\n"
112  "void __VERIFIER_assume(__CPROVER_bool assumption);\n"
113  // NOLINTNEXTLINE(whitespace/line_length)
114  "void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
115  "__CPROVER_bool __CPROVER_equal();\n"
116  "__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
117  "__CPROVER_bool __CPROVER_invalid_pointer(const void *);\n"
118  "__CPROVER_bool __CPROVER_is_zero_string(const void *);\n"
119  "__CPROVER_size_t __CPROVER_zero_string_length(const void *);\n"
120  "__CPROVER_size_t __CPROVER_buffer_size(const void *);\n"
121 
122  "__CPROVER_bool __CPROVER_get_flag(const void *, const char *);\n"
123  "void __CPROVER_set_must(const void *, const char *);\n"
124  "void __CPROVER_clear_must(const void *, const char *);\n"
125  "void __CPROVER_set_may(const void *, const char *);\n"
126  "void __CPROVER_clear_may(const void *, const char *);\n"
127  "void __CPROVER_cleanup(const void *, const void *);\n"
128  "__CPROVER_bool __CPROVER_get_must(const void *, const char *);\n"
129  "__CPROVER_bool __CPROVER_get_may(const void *, const char *);\n"
130 
131  "const unsigned __CPROVER_constant_infinity_uint;\n"
132  "typedef void __CPROVER_integer;\n"
133  "typedef void __CPROVER_rational;\n"
134  "void __CPROVER_initialize(void);\n"
135  "void __CPROVER_input(const char *id, ...);\n"
136  "void __CPROVER_output(const char *id, ...);\n"
137  "void __CPROVER_cover(__CPROVER_bool condition);\n"
138 
139  // concurrency-related
140  "void __CPROVER_atomic_begin();\n"
141  "void __CPROVER_atomic_end();\n"
142  "void __CPROVER_fence(const char *kind, ...);\n"
143  "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
144  // NOLINTNEXTLINE(whitespace/line_length)
145  "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n"
146  "unsigned long __CPROVER_next_thread_id=0;\n"
147 
148  // traces
149  "void CBMC_trace(int lvl, const char *event, ...);\n"
150 
151  // pointers
152  "unsigned __CPROVER_POINTER_OBJECT(const void *p);\n"
153  "signed __CPROVER_POINTER_OFFSET(const void *p);\n"
154  "__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\n"
155  "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n"
156  // NOLINTNEXTLINE(whitespace/line_length)
157  "void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
158 
159  // malloc
160  "void *__CPROVER_malloc(__CPROVER_size_t size);\n"
161  "const void *__CPROVER_deallocated=0;\n"
162  "const void *__CPROVER_dead_object=0;\n"
163  "const void *__CPROVER_malloc_object=0;\n"
164  "__CPROVER_size_t __CPROVER_malloc_size;\n"
165  "__CPROVER_bool __CPROVER_malloc_is_new_array=0;\n" // for C++
166  "const void *__CPROVER_memory_leak=0;\n"
167 
168  // this is ANSI-C
169  // NOLINTNEXTLINE(whitespace/line_length)
170  "extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n"
171 
172  // this is GCC
173  // NOLINTNEXTLINE(whitespace/line_length)
174  "extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n"
175  // NOLINTNEXTLINE(whitespace/line_length)
176  "extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n"
177 
178  // float stuff
179  "__CPROVER_bool __CPROVER_isnanf(float f);\n"
180  "__CPROVER_bool __CPROVER_isnand(double f);\n"
181  "__CPROVER_bool __CPROVER_isnanld(long double f);\n"
182  "__CPROVER_bool __CPROVER_isfinitef(float f);\n"
183  "__CPROVER_bool __CPROVER_isfinited(double f);\n"
184  "__CPROVER_bool __CPROVER_isfiniteld(long double f);\n"
185  "__CPROVER_bool __CPROVER_isinff(float f);\n"
186  "__CPROVER_bool __CPROVER_isinfd(double f);\n"
187  "__CPROVER_bool __CPROVER_isinfld(long double f);\n"
188  "__CPROVER_bool __CPROVER_isnormalf(float f);\n"
189  "__CPROVER_bool __CPROVER_isnormald(double f);\n"
190  "__CPROVER_bool __CPROVER_isnormalld(long double f);\n"
191  "__CPROVER_bool __CPROVER_signf(float f);\n"
192  "__CPROVER_bool __CPROVER_signd(double f);\n"
193  "__CPROVER_bool __CPROVER_signld(long double f);\n"
194  "double __CPROVER_inf(void);\n"
195  "float __CPROVER_inff(void);\n"
196  "long double __CPROVER_infl(void);\n"
197  "int __CPROVER_thread_local __CPROVER_rounding_mode="+
198  std::to_string(config.ansi_c.rounding_mode)+";\n"
199  "int __CPROVER_isgreaterf(float f, float g);\n"
200  "int __CPROVER_isgreaterd(double f, double g);\n"
201  "int __CPROVER_isgreaterequalf(float f, float g);\n"
202  "int __CPROVER_isgreaterequald(double f, double g);\n"
203  "int __CPROVER_islessf(float f, float g);\n"
204  "int __CPROVER_islessd(double f, double g);\n"
205  "int __CPROVER_islessequalf(float f, float g);\n"
206  "int __CPROVER_islessequald(double f, double g);\n"
207  "int __CPROVER_islessgreaterf(float f, float g);\n"
208  "int __CPROVER_islessgreaterd(double f, double g);\n"
209  "int __CPROVER_isunorderedf(float f, float g);\n"
210  "int __CPROVER_isunorderedd(double f, double g);\n"
211 
212  // absolute value
213  "int __CPROVER_abs(int x);\n"
214  "long int __CPROVER_labs(long int x);\n"
215  "long int __CPROVER_llabs(long long int x);\n"
216  "double __CPROVER_fabs(double x);\n"
217  "long double __CPROVER_fabsl(long double x);\n"
218  "float __CPROVER_fabsf(float x);\n"
219 
220  // arrays
221  // NOLINTNEXTLINE(whitespace/line_length)
222  "__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
223  // overwrite all of *dest (possibly using nondet values), even
224  // if *src is smaller
225  "void __CPROVER_array_copy(const void *dest, const void *src);\n"
226  // replace at most size-of-*src bytes in *dest
227  "void __CPROVER_array_replace(const void *dest, const void *src);\n"
228  "void __CPROVER_array_set(const void *dest, ...);\n"
229 
230  // k-induction
231  "void __CPROVER_k_induction_hint(unsigned min, unsigned max, "
232  "unsigned step, unsigned loop_free);\n"
233 
234  // format string-related
235  "int __CPROVER_scanf(const char *, ...);\n"
236 
237  // pipes, write, read, close
238  "struct __CPROVER_pipet {\n"
239  " _Bool widowed;\n"
240  " char data[4];\n"
241  " short next_avail;\n"
242  " short next_unread;\n"
243  "};\n"
244  // NOLINTNEXTLINE(whitespace/line_length)
245  "extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n"
246  // offset to make sure we don't collide with other fds
247  "extern const int __CPROVER_pipe_offset;\n"
248  "unsigned __CPROVER_pipe_count=0;\n"
249 
250  "\n";
251 
252  // GCC junk stuff, also for CLANG and ARM
256  {
263  code+=clang_builtin_headers;
264 
265  // there are many more, e.g., look at
266  // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
267 
268  if(config.ansi_c.arch=="i386" ||
269  config.ansi_c.arch=="x86_64" ||
270  config.ansi_c.arch=="x32")
271  {
273  code+="typedef double __float128;\n"; // clang doesn't do __float128
274 
279  }
280  else if(config.ansi_c.arch=="arm64" ||
281  config.ansi_c.arch=="armel" ||
282  config.ansi_c.arch=="armhf" ||
283  config.ansi_c.arch=="arm")
284  {
286  }
287  else if(config.ansi_c.arch=="alpha")
288  {
290  }
291  else if(config.ansi_c.arch=="mips64el" ||
292  config.ansi_c.arch=="mipsn32el" ||
293  config.ansi_c.arch=="mipsel" ||
294  config.ansi_c.arch=="mips64" ||
295  config.ansi_c.arch=="mipsn32" ||
296  config.ansi_c.arch=="mips")
297  {
299  }
300  else if(config.ansi_c.arch=="powerpc" ||
301  config.ansi_c.arch=="ppc64" ||
302  config.ansi_c.arch=="ppc64le")
303  {
305  }
306 
307  // On 64-bit systems, gcc has typedefs
308  // __int128_t und __uint128_t -- but not on 32 bit!
310  {
311  code+="typedef signed __int128 __int128_t;\n"
312  "typedef unsigned __int128 __uint128_t;\n";
313  }
314  }
315 
316  // this is Visual C/C++ only
318  code+="int __noop();\n"
319  "int __assume(int);\n";
320 
321  // ARM stuff
323  code+=arm_builtin_headers;
324 
325  // CW stuff
327  code+=cw_builtin_headers;
328 
329  // Architecture strings
331 }
332 
333 void ansi_c_architecture_strings(std::string &code)
334 {
335  // The following are CPROVER-specific.
336  // They allow identifying the architectural settings used
337  // at compile time from a goto-binary.
338 
339  code+="# 1 \"<builtin-architecture-strings>\"\n";
340 
341  code+=architecture_string(config.ansi_c.int_width, "int_width");
342  code+=architecture_string(config.ansi_c.int_width, "word_size"); // old
343  code+=architecture_string(config.ansi_c.long_int_width, "long_int_width");
344  code+=architecture_string(config.ansi_c.bool_width, "bool_width");
345  code+=architecture_string(config.ansi_c.char_width, "char_width");
346  code+=architecture_string(config.ansi_c.short_int_width, "short_int_width");
347  code+=architecture_string(config.ansi_c.long_long_int_width, "long_long_int_width"); // NOLINT(whitespace/line_length)
348  code+=architecture_string(config.ansi_c.pointer_width, "pointer_width");
349  code+=architecture_string(config.ansi_c.single_width, "single_width");
350  code+=architecture_string(config.ansi_c.double_width, "double_width");
351  code+=architecture_string(config.ansi_c.long_double_width, "long_double_width"); // NOLINT(whitespace/line_length)
352  code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
353  code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
354  code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
355  code+=architecture_string(config.ansi_c.use_fixed_for_float, "fixed_for_float"); // NOLINT(whitespace/line_length)
356  code+=architecture_string(config.ansi_c.alignment, "alignment");
357  code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
358  code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)
360  code+=architecture_string(configt::ansi_ct::os_to_string(config.ansi_c.os), "os"); // NOLINT(whitespace/line_length)
361  code+=architecture_string(config.ansi_c.NULL_is_zero, "NULL_is_zero");
362 }
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
unsigned int_width
Definition: config.h:30
unsigned single_width
Definition: config.h:37
const char gcc_builtin_headers_ia32_3[]
const char gcc_builtin_headers_ubsan[]
static std::string os_to_string(ost)
Definition: config.cpp:1016
unsigned alignment
Definition: config.h:68
endiannesst endianness
Definition: config.h:75
unsigned short_int_width
Definition: config.h:34
bool NULL_is_zero
Definition: config.h:86
const char gcc_builtin_headers_alpha[]
unsigned char_width
Definition: config.h:33
configt config
Definition: config.cpp:21
const char arm_builtin_headers[]
void ansi_c_internal_additions(std::string &code)
const char cw_builtin_headers[]
const char gcc_builtin_headers_omp[]
const char gcc_builtin_headers_mips[]
unsigned wchar_t_width
Definition: config.h:40
static std::string architecture_string(const std::string &value, const char *s)
flavourt mode
Definition: config.h:105
unsigned long_long_int_width
Definition: config.h:35
irep_idt arch
Definition: config.h:83
void ansi_c_architecture_strings(std::string &code)
const char gcc_builtin_headers_generic[]
const char gcc_builtin_headers_tm[]
unsigned memory_operand_size
Definition: config.h:72
const char gcc_builtin_headers_mem_string[]
const char gcc_builtin_headers_ia32_4[]
bool char_is_unsigned
Definition: config.h:43
bool use_fixed_for_float
Definition: config.h:44
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:54
const char clang_builtin_headers[]
const char gcc_builtin_headers_math[]
unsigned bool_width
Definition: config.h:32
unsigned long_double_width
Definition: config.h:39
const char gcc_builtin_headers_ia32[]
unsigned double_width
Definition: config.h:38
const char gcc_builtin_headers_arm[]
unsigned long_int_width
Definition: config.h:31
bool wchar_t_is_unsigned
Definition: config.h:43
unsigned pointer_width
Definition: config.h:36
const char gcc_builtin_headers_ia32_2[]
const char gcc_builtin_headers_power[]