From 1201ffe947f4b0ca63c208608d3036ecd2288003 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 21 Aug 2017 09:11:11 +0100 Subject: [PATCH] C++ front-end: Use C factory for compiler builtins --- src/cpp/cpp_internal_additions.cpp | 163 +++++++++++++++-------------- src/cpp/cpp_typecheck.cpp | 6 ++ src/cpp/cpp_typecheck.h | 2 + src/cpp/cpp_typecheck_resolve.cpp | 12 +++ 4 files changed, 107 insertions(+), 76 deletions(-) diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 2c3d33a00d6..9f733c6abab 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -42,23 +42,7 @@ std::string c2cpp(const std::string &s) void cpp_internal_additions(std::ostream &out) { - out << "# 1 \"\"" << '\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 \"\"" << '\n'; // __CPROVER namespace out << "namespace __CPROVER { }" << '\n'; @@ -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) diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 16d307e2324..8b3c64cebc3 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include #include "expr2cpp.h" @@ -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()); +} diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index 29a2a7e0efc..307a6188fa2 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -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); diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index c160b58790e..86fcddea3bc 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -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);