Skip to content

Commit

Permalink
C++ front-end: Use C factory for compiler builtins
Browse files Browse the repository at this point in the history
  • Loading branch information
@tautschnig
tautschnig committed Jun 8, 2018
1 parent 0451f1e commit 1201ffe
Show file tree
Hide file tree
Showing 4 changed files with 107 additions and 76 deletions.
163 changes: 87 additions & 76 deletions src/cpp/cpp_internal_additions.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,23 +42,7 @@ std::string c2cpp(const std::string &s)

void cpp_internal_additions(std::ostream &out)
{
out << "# 1 \"<built-in>\"" << '\n';

// new and delete are in the root namespace!
out << "void operator delete(void *);" << '\n';
out << "void *operator new(__typeof__(sizeof(int)));" << '\n';

// auxiliaries for new/delete
out << "extern \"C\" void *__new(__typeof__(sizeof(int)));" << '\n';
// NOLINTNEXTLINE(whitespace/line_length)
out << "extern \"C\" void *__new_array(__typeof__(sizeof(int)), __typeof__(sizeof(int)));" << '\n';
// NOLINTNEXTLINE(whitespace/line_length)
out << "extern \"C\" void *__placement_new(__typeof__(sizeof(int)), void *);" << '\n';
// NOLINTNEXTLINE(whitespace/line_length)
out << "extern \"C\" void *__placement_new_array(__typeof__(sizeof(int)), __typeof__(sizeof(int)), void *);" << '\n';
out << "extern \"C\" void __delete(void *);" << '\n';
out << "extern \"C\" void __delete_array(void *);" << '\n';
out << "extern \"C\" bool __CPROVER_malloc_is_new_array=0;" << '\n';
out << "# 1 \"<built-in-additions>\"" << '\n';

// __CPROVER namespace
out << "namespace __CPROVER { }" << '\n';
Expand All @@ -71,84 +55,111 @@ void cpp_internal_additions(std::ostream &out)
<< " __CPROVER::ssize_t;" << '\n';
out << "typedef __CPROVER::ssize_t __CPROVER_ssize_t;" << '\n';

// assume/assert
out << "extern \"C\" void assert(bool assertion);" << '\n';
out << "extern \"C\" void __CPROVER_assume(bool assumption);" << '\n';
out << "extern \"C\" void __CPROVER_assert("
"bool assertion, const char *description);" << '\n';
out << "extern \"C\" void __CPROVER::assume(bool assumption);" << '\n';
out << "extern \"C\" void __CPROVER::assert("
"bool assertion, const char *description);" << '\n';
// new and delete are in the root namespace!
out << "void operator delete(void *);" << '\n';
out << "void *operator new(__CPROVER::size_t);" << '\n';

out << "extern \"C\" {" << '\n';

// CPROVER extensions
out << "extern \"C\" const unsigned __CPROVER::constant_infinity_uint;\n";
out << "extern \"C\" void " INITIALIZE_FUNCTION "();" << '\n';
out << "extern \"C\" void __CPROVER::input(const char *id, ...);" << '\n';
out << "extern \"C\" void __CPROVER::output(const char *id, ...);" << '\n';
out << "extern \"C\" void __CPROVER::cover(bool condition);" << '\n';
out << "extern \"C\" void __CPROVER::atomic_begin();" << '\n';
out << "extern \"C\" void __CPROVER::atomic_end();" << '\n';

// pointers
out << "extern \"C\" __CPROVER::size_t __CPROVER_POINTER_OBJECT(const void *);\n";
out << "extern \"C\" __CPROVER::ssize_t __CPROVER_POINTER_OFFSET(const void *);" << '\n';
out << "extern \"C\" bool __CPROVER_DYNAMIC_OBJECT(const void *p);" << '\n';
// NOLINTNEXTLINE(whitespace/line_length)
out << "extern \"C\" extern unsigned char __CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n';
out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n';
out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n';
out << "typedef void __CPROVER_integer;" << '\n';
out << "typedef void __CPROVER_rational;" << '\n';
// TODO
// out << "thread_local unsigned long __CPROVER_thread_id = 0;" << '\n';
out << "__CPROVER_bool "
<< "__CPROVER_threads_exited[__CPROVER::constant_infinity_uint];" << '\n';
out << "unsigned long __CPROVER_next_thread_id = 0;" << '\n';
out << "extern unsigned char "
<< "__CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n';

// malloc
out << "extern \"C\" void *__CPROVER_allocate(__CPROVER_size_t size,"
<< " __CPROVER_bool zero);" << '\n';
out << "extern \"C\" const void *__CPROVER_deallocated=0;" << '\n';
out << "extern \"C\" const void *__CPROVER_malloc_object=0;" << '\n';
out << "extern \"C\" __CPROVER::size_t __CPROVER_malloc_size;" << '\n';
out << "const void *__CPROVER_deallocated = 0;" << '\n';
out << "const void *__CPROVER_dead_object = 0;" << '\n';
out << "const void *__CPROVER_malloc_object = 0;" << '\n';
out << "__CPROVER::size_t __CPROVER_malloc_size;" << '\n';
out << "__CPROVER_bool __CPROVER_malloc_is_new_array = 0;" << '\n';
out << "const void *__CPROVER_memory_leak = 0;" << '\n';
out << "void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);"
<< '\n';

// float
out << "extern \"C\" int __CPROVER_rounding_mode;" << '\n';

// arrays
// NOLINTNEXTLINE(whitespace/line_length)
out << "bool __CPROVER::array_equal(const void array1[], const void array2[]);" << '\n';
out << "void __CPROVER::array_copy(const void dest[], const void src[]);\n";
out << "void __CPROVER::array_set(const void dest[], ...);" << '\n';
// auxiliaries for new/delete
out << "void *__new(__CPROVER::size_t);" << '\n';
out << "void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" << '\n';
out << "void *__placement_new(__CPROVER::size_t, void *);" << '\n';
out << "void *__placement_new_array("
<< "__CPROVER::size_t, __CPROVER::size_t, void *);" << '\n';
out << "void __delete(void *);" << '\n';
out << "void __delete_array(void *);" << '\n';

// GCC stuff, but also for ARM
// float
// TODO: should the thread_local
out << "int __CPROVER_rounding_mode = "
<< std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';

// pipes, write, read, close
out << "struct __CPROVER_pipet {\n"
<< " bool widowed;\n"
<< " char data[4];\n"
<< " short next_avail;\n"
<< " short next_unread;\n"
<< "};\n";
out << "extern struct __CPROVER_pipet "
<< "__CPROVER_pipes[__CPROVER::constant_infinity_uint];" << '\n';
// offset to make sure we don't collide with other fds
out << "extern const int __CPROVER_pipe_offset;" << '\n';
out << "unsigned __CPROVER_pipe_count=0;" << '\n';

// This function needs to be declared, or otherwise can't be called
// by the entry-point construction.
out << "void " INITIALIZE_FUNCTION "();" << '\n';

// GCC junk stuff, also for CLANG and ARM
if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC ||
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
{
out << "extern \"C\" {" << '\n';
out << c2cpp(gcc_builtin_headers_types);
out << c2cpp(gcc_builtin_headers_generic);
out << c2cpp(gcc_builtin_headers_math);
out << c2cpp(gcc_builtin_headers_mem_string);
out << c2cpp(gcc_builtin_headers_omp);
out << c2cpp(gcc_builtin_headers_tm);
out << c2cpp(gcc_builtin_headers_ubsan);
out << c2cpp(clang_builtin_headers);

if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
out << "typedef double __float128;\n"; // clang doesn't do __float128

out << c2cpp(gcc_builtin_headers_ia32);
out << c2cpp(gcc_builtin_headers_ia32_2);
out << c2cpp(gcc_builtin_headers_ia32_3);
out << c2cpp(gcc_builtin_headers_ia32_4);
out << "}" << '\n';

if(
config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
config.ansi_c.arch == "x32")
{
// clang doesn't do __float128
if(config.ansi_c.mode == configt::ansi_ct::flavourt::APPLE)
out << "typedef double __float128;" << '\n';
}

// On 64-bit systems, gcc has typedefs
// __int128_t und __uint128_t -- but not on 32 bit!
if(config.ansi_c.long_int_width >= 64)
{
out << "typedef signed __int128 __int128_t;" << '\n';
out << "typedef unsigned __int128 __uint128_t;" << '\n';
}
}

// extensions for Visual C/C++
// this is Visual C/C++ only
if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN)
out << "extern \"C\" int __noop(...);\n";
{
out << "int __noop(...);" << '\n';
out << "int __assume(int);" << '\n';
}

// ARM stuff
if(config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
out << c2cpp(arm_builtin_headers);

// CW stuff
if(config.ansi_c.mode == configt::ansi_ct::flavourt::CODEWARRIOR)
out << c2cpp(cw_builtin_headers);

// string symbols to identify the architecture we have compiled for
std::string architecture_strings;
ansi_c_architecture_strings(architecture_strings);
out << c2cpp(architecture_strings);

out << "extern \"C\" {" << '\n';
out << architecture_strings;
out << "}" << '\n';
out << '}' << '\n'; // end extern "C"

// Microsoft stuff
if(config.ansi_c.mode==configt::ansi_ct::flavourt::VISUAL_STUDIO)
Expand Down
6 changes: 6 additions & 0 deletions src/cpp/cpp_typecheck.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
#include <util/source_location.h>
#include <util/symbol.h>

#include <ansi-c/builtin_factory.h>
#include <ansi-c/c_typecast.h>

#include "expr2cpp.h"
Expand Down Expand Up @@ -321,3 +322,8 @@ void cpp_typecheckt::clean_up()
}
}
}

bool cpp_typecheckt::builtin_factory(const irep_idt &identifier)
{
return ::builtin_factory(identifier, symbol_table, get_message_handler());
}
2 changes: 2 additions & 0 deletions src/cpp/cpp_typecheck.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -346,6 +346,8 @@ class cpp_typecheckt:public c_typecheck_baset
_method_symbol, template_map, instantiation_stack));
}

bool builtin_factory(const irep_idt &);

// types

void typecheck_type(typet &type);
Expand Down
12 changes: 12 additions & 0 deletions src/cpp/cpp_typecheck_resolve.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1407,8 +1407,20 @@ exprt cpp_typecheck_resolvet::resolve(
qualified?cpp_scopet::QUALIFIED:cpp_scopet::RECURSIVE;

if(template_args.is_nil())
{
cpp_typecheck.cpp_scopes.current_scope().lookup(
base_name, lookup_kind, id_set);

if(id_set.empty() && !cpp_typecheck.builtin_factory(base_name))
{
cpp_idt &builtin_id =
cpp_typecheck.cpp_scopes.get_root_scope().insert(base_name);
builtin_id.identifier = base_name;
builtin_id.id_class = cpp_idt::id_classt::SYMBOL;

id_set.insert(&builtin_id);
}
}
else
cpp_typecheck.cpp_scopes.current_scope().lookup(
base_name, lookup_kind, cpp_idt::id_classt::TEMPLATE, id_set);
Expand Down

0 comments on commit 1201ffe

Please sign in to comment.