Skip to content

Commit d1bf14a

Browse files
tautschnigtautschnig
committed
C++ front-end: Use C factory for compiler builtins
1 parent f9e723e commit d1bf14a

File tree

4 files changed

+113
-76
lines changed

4 files changed

+113
-76
lines changed

‎src/cpp/cpp_internal_additions.cpp

+91-76
Original file line numberDiff line numberDiff line change
@@ -42,23 +42,7 @@ std::string c2cpp(const std::string &s)
4242

4343
void cpp_internal_additions(std::ostream &out)
4444
{
45-
out << "# 1 \"<built-in>\"" << '\n';
46-
47-
// new and delete are in the root namespace!
48-
out << "void operator delete(void *);" << '\n';
49-
out << "void *operator new(__typeof__(sizeof(int)));" << '\n';
50-
51-
// auxiliaries for new/delete
52-
out << "extern \"C\" void *__new(__typeof__(sizeof(int)));" << '\n';
53-
// NOLINTNEXTLINE(whitespace/line_length)
54-
out << "extern \"C\" void *__new_array(__typeof__(sizeof(int)), __typeof__(sizeof(int)));" << '\n';
55-
// NOLINTNEXTLINE(whitespace/line_length)
56-
out << "extern \"C\" void *__placement_new(__typeof__(sizeof(int)), void *);" << '\n';
57-
// NOLINTNEXTLINE(whitespace/line_length)
58-
out << "extern \"C\" void *__placement_new_array(__typeof__(sizeof(int)), __typeof__(sizeof(int)), void *);" << '\n';
59-
out << "extern \"C\" void __delete(void *);" << '\n';
60-
out << "extern \"C\" void __delete_array(void *);" << '\n';
61-
out << "extern \"C\" bool __CPROVER_malloc_is_new_array=0;" << '\n';
45+
out << "# 1 \"<built-in-additions>\"" << '\n';
6246

6347
// __CPROVER namespace
6448
out << "namespace __CPROVER { }" << '\n';
@@ -71,84 +55,115 @@ void cpp_internal_additions(std::ostream &out)
7155
<< " __CPROVER::ssize_t;" << '\n';
7256
out << "typedef __CPROVER::ssize_t __CPROVER_ssize_t;" << '\n';
7357

74-
// assume/assert
75-
out << "extern \"C\" void assert(bool assertion);" << '\n';
76-
out << "extern \"C\" void __CPROVER_assume(bool assumption);" << '\n';
77-
out << "extern \"C\" void __CPROVER_assert("
78-
"bool assertion, const char *description);" << '\n';
79-
out << "extern \"C\" void __CPROVER::assume(bool assumption);" << '\n';
80-
out << "extern \"C\" void __CPROVER::assert("
81-
"bool assertion, const char *description);" << '\n';
58+
// new and delete are in the root namespace!
59+
out << "void operator delete(void *);" << '\n';
60+
out << "void *operator new(__CPROVER::size_t);" << '\n';
61+
62+
out << "extern \"C\" {" << '\n';
8263

8364
// CPROVER extensions
84-
out << "extern \"C\" const unsigned __CPROVER::constant_infinity_uint;\n";
85-
out << "extern \"C\" void " INITIALIZE_FUNCTION "();" << '\n';
86-
out << "extern \"C\" void __CPROVER::input(const char *id, ...);" << '\n';
87-
out << "extern \"C\" void __CPROVER::output(const char *id, ...);" << '\n';
88-
out << "extern \"C\" void __CPROVER::cover(bool condition);" << '\n';
89-
out << "extern \"C\" void __CPROVER::atomic_begin();" << '\n';
90-
out << "extern \"C\" void __CPROVER::atomic_end();" << '\n';
91-
92-
// pointers
93-
out << "extern \"C\" __CPROVER::size_t __CPROVER_POINTER_OBJECT(const void *);\n";
94-
out << "extern \"C\" __CPROVER::ssize_t __CPROVER_POINTER_OFFSET(const void *);" << '\n';
95-
out << "extern \"C\" bool __CPROVER_DYNAMIC_OBJECT(const void *p);" << '\n';
96-
// NOLINTNEXTLINE(whitespace/line_length)
97-
out << "extern \"C\" extern unsigned char __CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n';
98-
out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n';
65+
out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n';
66+
out << "typedef void __CPROVER_integer;" << '\n';
67+
out << "typedef void __CPROVER_rational;" << '\n';
68+
// TODO
69+
// out << "thread_local unsigned long __CPROVER_thread_id = 0;" << '\n';
70+
out << "__CPROVER_bool "
71+
<< "__CPROVER_threads_exited[__CPROVER::constant_infinity_uint];" << '\n';
72+
out << "unsigned long __CPROVER_next_thread_id = 0;" << '\n';
73+
out << "extern unsigned char "
74+
<< "__CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n';
9975

10076
// malloc
101-
out << "extern \"C\" void *__CPROVER_allocate(__CPROVER_size_t size,"
102-
<< " __CPROVER_bool zero);" << '\n';
103-
out << "extern \"C\" const void *__CPROVER_deallocated=0;" << '\n';
104-
out << "extern \"C\" const void *__CPROVER_malloc_object=0;" << '\n';
105-
out << "extern \"C\" __CPROVER::size_t __CPROVER_malloc_size;" << '\n';
106-
107-
// float
108-
out << "extern \"C\" int __CPROVER_rounding_mode;" << '\n';
77+
out << "const void *__CPROVER_deallocated = 0;" << '\n';
78+
out << "const void *__CPROVER_dead_object = 0;" << '\n';
79+
out << "const void *__CPROVER_malloc_object = 0;" << '\n';
80+
out << "__CPROVER::size_t __CPROVER_malloc_size;" << '\n';
81+
out << "__CPROVER_bool __CPROVER_malloc_is_new_array = 0;" << '\n';
82+
out << "const void *__CPROVER_memory_leak = 0;" << '\n';
83+
out << "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);"
84+
<< '\n';
10985

110-
// arrays
111-
// NOLINTNEXTLINE(whitespace/line_length)
112-
out << "bool __CPROVER::array_equal(const void array1[], const void array2[]);" << '\n';
113-
out << "void __CPROVER::array_copy(const void dest[], const void src[]);\n";
114-
out << "void __CPROVER::array_set(const void dest[], ...);" << '\n';
86+
// auxiliaries for new/delete
87+
out << "void *__new(__CPROVER::size_t);" << '\n';
88+
out << "void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" << '\n';
89+
out << "void *__placement_new(__CPROVER::size_t, void *);" << '\n';
90+
out << "void *__placement_new_array("
91+
<< "__CPROVER::size_t, __CPROVER::size_t, void *);" << '\n';
92+
out << "void __delete(void *);" << '\n';
93+
out << "void __delete_array(void *);" << '\n';
11594

116-
// GCC stuff, but also for ARM
95+
// float
96+
// TODO: should the thread_local
97+
out << "int __CPROVER_rounding_mode = "
98+
<< std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
99+
100+
// pipes, write, read, close
101+
out << "struct __CPROVER_pipet {\n"
102+
<< " bool widowed;\n"
103+
<< " char data[4];\n"
104+
<< " short next_avail;\n"
105+
<< " short next_unread;\n"
106+
<< "};\n";
107+
out << "extern struct __CPROVER_pipet "
108+
<< "__CPROVER_pipes[__CPROVER::constant_infinity_uint];" << '\n';
109+
// offset to make sure we don't collide with other fds
110+
out << "extern const int __CPROVER_pipe_offset;" << '\n';
111+
out << "unsigned __CPROVER_pipe_count=0;" << '\n';
112+
113+
// This function needs to be declared, or otherwise can't be called
114+
// by the entry-point construction.
115+
out << "void " INITIALIZE_FUNCTION "();" << '\n';
116+
117+
// GCC junk stuff, also for CLANG and ARM
117118
if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
118119
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
119120
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
120121
{
121-
out << "extern \"C\" {" << '\n';
122122
out << c2cpp(gcc_builtin_headers_types);
123-
out << c2cpp(gcc_builtin_headers_generic);
124-
out << c2cpp(gcc_builtin_headers_math);
125-
out << c2cpp(gcc_builtin_headers_mem_string);
126-
out << c2cpp(gcc_builtin_headers_omp);
127-
out << c2cpp(gcc_builtin_headers_tm);
128-
out << c2cpp(gcc_builtin_headers_ubsan);
129-
out << c2cpp(clang_builtin_headers);
130-
131-
if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
132-
out << "typedef double __float128;\n"; // clang doesn't do __float128
133-
134-
out << c2cpp(gcc_builtin_headers_ia32);
135-
out << c2cpp(gcc_builtin_headers_ia32_2);
136-
out << c2cpp(gcc_builtin_headers_ia32_3);
137-
out << c2cpp(gcc_builtin_headers_ia32_4);
138-
out << "}" << '\n';
123+
124+
if(config.ansi_c.arch == "i386" ||
125+
config.ansi_c.arch == "x86_64" ||
126+
config.ansi_c.arch == "x32")
127+
{
128+
// clang doesn't do __float128
129+
if(config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE)
130+
out << "typedef double __float128;" << '\n';
131+
}
132+
133+
// On 64-bit systems, gcc has typedefs
134+
// __int128_t und __uint128_t -- but not on 32 bit!
135+
if(config.ansi_c.long_int_width >= 64)
136+
{
137+
out << "typedef signed __int128 __int128_t;" << '\n';
138+
out << "typedef unsigned __int128 __uint128_t;" << '\n';
139+
}
139140
}
140141

141-
// extensions for Visual C/C++
142+
// this is Visual C/C++ only
142143
if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN)
143-
out << "extern \"C\" int __noop(...);\n";
144+
{
145+
out << "int __noop(...);" << '\n';
146+
out << "int __assume(int);" << '\n';
147+
}
148+
149+
// ARM stuff
150+
if(config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
151+
out << c2cpp(arm_builtin_headers);
152+
153+
// CW stuff
154+
if(config.ansi_c.mode==configt::ansi_ct::flavourt::CODEWARRIOR)
155+
out << c2cpp(cw_builtin_headers);
156+
157+
// ARM stuff
158+
if(config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
159+
out << c2cpp(arm_builtin_headers);
144160

145161
// string symbols to identify the architecture we have compiled for
146162
std::string architecture_strings;
147163
ansi_c_architecture_strings(architecture_strings);
164+
out << c2cpp(architecture_strings);
148165

149-
out << "extern \"C\" {" << '\n';
150-
out << architecture_strings;
151-
out << "}" << '\n';
166+
out << '}' << '\n'; // end extern "C"
152167

153168
// Microsoft stuff
154169
if(config.ansi_c.mode==configt::ansi_ct::flavourt::VISUAL_STUDIO)

‎src/cpp/cpp_typecheck.cpp

+8
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
1818
#include <util/symbol.h>
1919

2020
#include <linking/zero_initializer.h>
21+
22+
#include <ansi-c/builtin_factory.h>
2123
#include <ansi-c/c_typecast.h>
2224

2325
#include "expr2cpp.h"
@@ -338,3 +340,9 @@ bool cpp_typecheckt::contains_cpp_name(const exprt &expr)
338340
return true;
339341
return false;
340342
}
343+
344+
bool cpp_typecheckt::builtin_factory(const irep_idt &identifier)
345+
{
346+
return
347+
::builtin_factory(identifier, symbol_table, get_message_handler());
348+
}

‎src/cpp/cpp_typecheck.h

+2
Original file line numberDiff line numberDiff line change
@@ -343,6 +343,8 @@ class cpp_typecheckt:public c_typecheck_baset
343343

344344
void add_method_body(symbolt *_method_symbol);
345345

346+
bool builtin_factory(const irep_idt &);
347+
346348
// types
347349

348350
void typecheck_type(typet &type);

‎src/cpp/cpp_typecheck_resolve.cpp

+12
Original file line numberDiff line numberDiff line change
@@ -1451,8 +1451,20 @@ exprt cpp_typecheck_resolvet::resolve(
14511451
qualified?cpp_scopet::QUALIFIED:cpp_scopet::RECURSIVE;
14521452

14531453
if(template_args.is_nil())
1454+
{
14541455
cpp_typecheck.cpp_scopes.current_scope().lookup(
14551456
base_name, lookup_kind, id_set);
1457+
1458+
if(id_set.empty() && !cpp_typecheck.builtin_factory(base_name))
1459+
{
1460+
cpp_idt &builtin_id =
1461+
cpp_typecheck.cpp_scopes.get_root_scope().insert(base_name);
1462+
builtin_id.identifier = base_name;
1463+
builtin_id.id_class = cpp_idt::id_classt::SYMBOL;
1464+
1465+
id_set.insert(&builtin_id);
1466+
}
1467+
}
14561468
else
14571469
cpp_typecheck.cpp_scopes.current_scope().lookup(
14581470
base_name, lookup_kind, cpp_idt::id_classt::TEMPLATE, id_set);

0 commit comments

Comments
 (0)