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/c_types.h>
12 #include <util/config.h>
13 
15 
17 "# 1 \"gcc_builtin_headers_types.h\"\n"
18 #include "gcc_builtin_headers_types.inc"
19 ; // NOLINT(whitespace/semicolon)
20 
22 "# 1 \"gcc_builtin_headers_generic.h\"\n"
23 #include "gcc_builtin_headers_generic.inc"
24 ; // NOLINT(whitespace/semicolon)
25 
27 "# 1 \"gcc_builtin_headers_math.h\"\n"
28 #include "gcc_builtin_headers_math.inc"
29 ; // NOLINT(whitespace/semicolon)
30 
32 "# 1 \"gcc_builtin_headers_mem_string.h\"\n"
33 #include "gcc_builtin_headers_mem_string.inc"
34 ; // NOLINT(whitespace/semicolon)
35 
37 "# 1 \"gcc_builtin_headers_omp.h\"\n"
38 #include "gcc_builtin_headers_omp.inc"
39 ; // NOLINT(whitespace/semicolon)
40 
42 "# 1 \"gcc_builtin_headers_tm.h\"\n"
43 #include "gcc_builtin_headers_tm.inc"
44 ; // NOLINT(whitespace/semicolon)
45 
47 "# 1 \"gcc_builtin_headers_ubsan.h\"\n"
48 #include "gcc_builtin_headers_ubsan.inc"
49 ; // NOLINT(whitespace/semicolon)
50 
52 "# 1 \"gcc_builtin_headers_ia32.h\"\n"
53 #include "gcc_builtin_headers_ia32.inc"
54 ; // NOLINT(whitespace/semicolon)
56 #include "gcc_builtin_headers_ia32-2.inc"
57 ; // NOLINT(whitespace/semicolon)
59 #include "gcc_builtin_headers_ia32-3.inc"
60 ; // NOLINT(whitespace/semicolon)
62 #include "gcc_builtin_headers_ia32-4.inc"
63 ; // NOLINT(whitespace/semicolon)
64 
66 "# 1 \"gcc_builtin_headers_alpha.h\"\n"
67 #include "gcc_builtin_headers_alpha.inc"
68 ; // NOLINT(whitespace/semicolon)
69 
71 "# 1 \"gcc_builtin_headers_arm.h\"\n"
72 #include "gcc_builtin_headers_arm.inc"
73 ; // NOLINT(whitespace/semicolon)
74 
76 "# 1 \"gcc_builtin_headers_mips.h\"\n"
77 #include "gcc_builtin_headers_mips.inc"
78 ; // NOLINT(whitespace/semicolon)
79 
81 "# 1 \"gcc_builtin_headers_power.h\"\n"
82 #include "gcc_builtin_headers_power.inc"
83 ; // NOLINT(whitespace/semicolon)
84 
85 const char arm_builtin_headers[]=
86 "# 1 \"arm_builtin_headers.h\"\n"
87 #include "arm_builtin_headers.inc"
88 ; // NOLINT(whitespace/semicolon)
89 
90 const char cw_builtin_headers[]=
91 "# 1 \"cw_builtin_headers.h\"\n"
92 #include "cw_builtin_headers.inc"
93 ; // NOLINT(whitespace/semicolon)
94 
95 const char clang_builtin_headers[]=
96 "# 1 \"clang_builtin_headers.h\"\n"
97 #include "clang_builtin_headers.inc"
98 ; // NOLINT(whitespace/semicolon)
99 
101 "# 1 \"cprover_builtin_headers.h\"\n"
102 #include "cprover_builtin_headers.inc"
103 ; // NOLINT(whitespace/semicolon)
104 
106 "# 1 \"windows_builtin_headers.h\"\n"
107 #include "windows_builtin_headers.inc"
108 ; // NOLINT(whitespace/semicolon)
109 
110 static std::string architecture_string(const std::string &value, const char *s)
111 {
112  return std::string("const char *" CPROVER_PREFIX "architecture_") +
113  std::string(s) + "=\"" + value + "\";\n";
114 }
115 
116 template <typename T>
117 static std::string architecture_string(T value, const char *s)
118 {
119  return std::string("const int " CPROVER_PREFIX "architecture_") +
120  std::string(s) + "=" + std::to_string(value) + ";\n";
121 }
122 
123 void ansi_c_internal_additions(std::string &code)
124 {
125  // clang-format off
126  // do the built-in types and variables
127  code+=
128  "# 1 \"<built-in-additions>\"\n"
129  "typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
130  "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
131  " " CPROVER_PREFIX "ssize_t;\n"
132  "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
133  "typedef void " CPROVER_PREFIX "integer;\n"
134  "typedef void " CPROVER_PREFIX "rational;\n"
135  CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n"
136  CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
137  CPROVER_PREFIX "constant_infinity_uint];\n"
138  "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
139  "extern unsigned char " CPROVER_PREFIX "memory["
140  CPROVER_PREFIX "constant_infinity_uint];\n"
141 
142  // malloc
143  "const void *" CPROVER_PREFIX "deallocated=0;\n"
144  "const void *" CPROVER_PREFIX "dead_object=0;\n"
145  "const void *" CPROVER_PREFIX "malloc_object=0;\n"
146  CPROVER_PREFIX "size_t " CPROVER_PREFIX "malloc_size;\n"
147  CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
148  "const void *" CPROVER_PREFIX "memory_leak=0;\n"
149  "void *" CPROVER_PREFIX "allocate("
150  CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
151 
152  // this is ANSI-C
153  "extern " CPROVER_PREFIX "thread_local const char __func__["
154  CPROVER_PREFIX "constant_infinity_uint];\n"
155 
156  // this is GCC
157  "extern " CPROVER_PREFIX "thread_local const char __FUNCTION__["
158  CPROVER_PREFIX "constant_infinity_uint];\n"
159  "extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
160  CPROVER_PREFIX "constant_infinity_uint];\n"
161 
162  // float stuff
163  "int " CPROVER_PREFIX "thread_local " CPROVER_PREFIX "rounding_mode="+
165 
166  // pipes, write, read, close
167  "struct " CPROVER_PREFIX "pipet {\n"
168  " _Bool widowed;\n"
169  " char data[4];\n"
170  " short next_avail;\n"
171  " short next_unread;\n"
172  "};\n"
173  "extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes["
174  CPROVER_PREFIX "constant_infinity_uint];\n"
175  // offset to make sure we don't collide with other fds
176  "extern const int " CPROVER_PREFIX "pipe_offset;\n"
177  "unsigned " CPROVER_PREFIX "pipe_count=0;\n"
178  "\n"
179  // This function needs to be declared, or otherwise can't be called
180  // by the entry-point construction.
181  "void " INITIALIZE_FUNCTION "(void);\n"
182  "\n";
183  // clang-format on
184 
185  // GCC junk stuff, also for CLANG and ARM
186  if(
190  {
192 
193  // there are many more, e.g., look at
194  // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
195 
196  if(
197  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
198  config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64" ||
199  config.ansi_c.arch == "powerpc" || config.ansi_c.arch == "ppc64")
200  {
201  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
202  // For clang, __float128 is a keyword.
203  // For gcc, this is a typedef and not a keyword.
205  code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
206  }
207  else if(config.ansi_c.arch == "ppc64le")
208  {
209  // https://patchwork.ozlabs.org/patch/792295/
211  code += "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
212  }
213  else if(config.ansi_c.arch == "hppa")
214  {
215  // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
216  // For clang, __float128 is a keyword.
217  // For gcc, this is a typedef and not a keyword.
219  code+="typedef long double __float128;\n";
220  }
221 
222  if(
223  config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
224  config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
225  {
226  // clang doesn't do __float80
227  // Note that __float80 is a typedef, and not a keyword.
229  code += "typedef " CPROVER_PREFIX "Float64x __float80;\n";
230  }
231 
232  // On 64-bit systems, gcc has typedefs
233  // __int128_t und __uint128_t -- but not on 32 bit!
235  {
236  code+="typedef signed __int128 __int128_t;\n"
237  "typedef unsigned __int128 __uint128_t;\n";
238  }
239  }
240 
241  // this is Visual C/C++ only
243  code+="int __noop();\n"
244  "int __assume(int);\n";
245 
246  // ARM stuff
248  code+=arm_builtin_headers;
249 
250  // CW stuff
252  code+=cw_builtin_headers;
253 
254  // Architecture strings
256 }
257 
258 void ansi_c_architecture_strings(std::string &code)
259 {
260  // The following are CPROVER-specific.
261  // They allow identifying the architectural settings used
262  // at compile time from a goto-binary.
263 
264  code+="# 1 \"<builtin-architecture-strings>\"\n";
265 
266  code+=architecture_string(config.ansi_c.int_width, "int_width");
267  code+=architecture_string(config.ansi_c.int_width, "word_size"); // old
268  code+=architecture_string(config.ansi_c.long_int_width, "long_int_width");
269  code+=architecture_string(config.ansi_c.bool_width, "bool_width");
270  code+=architecture_string(config.ansi_c.char_width, "char_width");
271  code+=architecture_string(config.ansi_c.short_int_width, "short_int_width");
272  code+=architecture_string(config.ansi_c.long_long_int_width, "long_long_int_width"); // NOLINT(whitespace/line_length)
273  code+=architecture_string(config.ansi_c.pointer_width, "pointer_width");
274  code+=architecture_string(config.ansi_c.single_width, "single_width");
275  code+=architecture_string(config.ansi_c.double_width, "double_width");
276  code+=architecture_string(config.ansi_c.long_double_width, "long_double_width"); // NOLINT(whitespace/line_length)
277  code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
278  code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
279  code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
280  code+=architecture_string(config.ansi_c.alignment, "alignment");
281  code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
282  code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)
284  code+=architecture_string(configt::ansi_ct::os_to_string(config.ansi_c.os), "os"); // NOLINT(whitespace/line_length)
285  code+=architecture_string(config.ansi_c.NULL_is_zero, "NULL_is_zero");
286 }
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:32
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:87
gcc_builtin_headers_omp
const char gcc_builtin_headers_omp[]
Definition: ansi_c_internal_additions.cpp:36
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:40
gcc_builtin_headers_arm
const char gcc_builtin_headers_arm[]
Definition: ansi_c_internal_additions.cpp:70
architecture_string
static std::string architecture_string(const std::string &value, const char *s)
Definition: ansi_c_internal_additions.cpp:110
configt::ansi_ct::flavourt::CODEWARRIOR
windows_builtin_headers
const char windows_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:105
configt::ansi_ct::os
ost os
Definition: config.h:79
ansi_c_architecture_strings
void ansi_c_architecture_strings(std::string &code)
Definition: ansi_c_internal_additions.cpp:258
configt::ansi_ct::rounding_mode
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:55
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:69
configt::ansi_c
struct configt::ansi_ct ansi_c
gcc_builtin_headers_mem_string
const char gcc_builtin_headers_mem_string[]
Definition: ansi_c_internal_additions.cpp:31
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
configt::ansi_ct::flavourt::ARM
configt::ansi_ct::flavourt::CLANG
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:33
gcc_builtin_headers_ubsan
const char gcc_builtin_headers_ubsan[]
Definition: ansi_c_internal_additions.cpp:46
clang_builtin_headers
const char clang_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:95
gcc_builtin_headers_types
const char gcc_builtin_headers_types[]
Definition: ansi_c_internal_additions.cpp:16
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:43
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:38
ansi_c_internal_additions.h
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:73
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
signed_size_type
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
gcc_builtin_headers_ia32
const char gcc_builtin_headers_ia32[]
Definition: ansi_c_internal_additions.cpp:51
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:35
ansi_c_internal_additions
void ansi_c_internal_additions(std::string &code)
Definition: ansi_c_internal_additions.cpp:123
gcc_builtin_headers_ia32_2
const char gcc_builtin_headers_ia32_2[]
Definition: ansi_c_internal_additions.cpp:55
cw_builtin_headers
const char cw_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:90
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:84
configt::ansi_ct::ost::OS_WIN
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1096
arm_builtin_headers
const char arm_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:85
config
configt config
Definition: config.cpp:24
gcc_builtin_headers_mips
const char gcc_builtin_headers_mips[]
Definition: ansi_c_internal_additions.cpp:75
configt::ansi_ct::mode
flavourt mode
Definition: config.h:115
cprover_builtin_headers
const char cprover_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:100
c_type_as_string
std::string c_type_as_string(const irep_idt &c_type)
Definition: c_types.cpp:258
gcc_builtin_headers_power
const char gcc_builtin_headers_power[]
Definition: ansi_c_internal_additions.cpp:80
gcc_builtin_headers_ia32_3
const char gcc_builtin_headers_ia32_3[]
Definition: ansi_c_internal_additions.cpp:58
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:39
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
gcc_builtin_headers_tm
const char gcc_builtin_headers_tm[]
Definition: ansi_c_internal_additions.cpp:41
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:34
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:43
configt::ansi_ct::flavourt::GCC
gcc_builtin_headers_ia32_4
const char gcc_builtin_headers_ia32_4[]
Definition: ansi_c_internal_additions.cpp:61
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:36
static_lifetime_init.h
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:37
gcc_builtin_headers_alpha
const char gcc_builtin_headers_alpha[]
Definition: ansi_c_internal_additions.cpp:65
gcc_builtin_headers_generic
const char gcc_builtin_headers_generic[]
Definition: ansi_c_internal_additions.cpp:21
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:30
c_types.h
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:76
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:31
gcc_builtin_headers_math
const char gcc_builtin_headers_math[]
Definition: ansi_c_internal_additions.cpp:26