C++ front-end now has its own library

Moved new/delete implementation from ansi-c to cpp.

Author: tautschnig

.gitignore

@@ -49,6 +49,7 @@ src/ansi-c/gcc_builtin_headers_mips.inc
 src/ansi-c/gcc_builtin_headers_power.inc
 src/ansi-c/gcc_builtin_headers_ubsan.inc
 src/ansi-c/windows_builtin_headers.inc
+src/cpp/cprover_library.inc
 
 # regression/test files
 *.out

.travis.yml

@@ -286,6 +286,7 @@ install:
   - make -C jbmc/src java-models-library-download
   - make -C src minisat2-download
   - make -C src/ansi-c library_check
+  - make -C src/cpp library_check
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
   - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3

src/cbmc/cbmc_parse_options.cpp

@@ -26,6 +26,8 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_preprocess.h>
 #include <ansi-c/cprover_library.h>
 
+#include <cpp/cprover_library.h>
+
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
@@ -714,6 +716,8 @@ bool cbmc_parse_optionst::process_goto_program(
     // add the library
     log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
                  << eom;
+    link_to_library(
+      goto_model, log.get_message_handler(), add_cprover_cpp_library);
     link_to_library(
       goto_model, log.get_message_handler(), add_cprover_c_library);
 

src/cpp/CMakeLists.txt

@@ -1,3 +1,33 @@
+file(GLOB cpp_library_sources "library/*.c")
+
+add_custom_command(OUTPUT converter_input.txt
+    COMMAND cat ${cpp_library_sources} > converter_input.txt
+    DEPENDS ${cpp_library_sources}
+)
+
+add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+    COMMAND ../ansi-c/converter < "converter_input.txt" > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+    DEPENDS "converter_input.txt" ../ansi-c/converter
+)
+
+################################################################################
+
+file(GLOB library_check_sources "library/*.c")
+
+add_custom_command(
+    DEPENDS ${library_check_sources}
+    COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/../ansi-c/library_check.sh ${CMAKE_C_COMPILER} ${library_check_sources}
+    COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
+    OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+
+add_custom_target(cpp_library_check
+    DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
+)
+
+################################################################################
+
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 add_library(cpp ${sources})
 

src/cpp/Makefile

@@ -42,6 +42,7 @@ SRC = cpp_constructor.cpp \
       cpp_typecheck_using.cpp \
       cpp_typecheck_virtual_table.cpp \
       cpp_util.cpp \
+      cprover_library.cpp \
       expr2cpp.cpp \
       parse.cpp \
       template_map.cpp \
@@ -52,11 +53,27 @@ INCLUDES= -I ..
 include ../config.inc
 include ../common
 
-CLEANFILES = cpp$(LIBEXT)
+CLEANFILES = cpp$(LIBEXT) cprover_library.inc library_check
 
 all: cpp$(LIBEXT)
 
 ###############################################################################
 
+../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp
+	$(MAKE) -C ../ansi-c library/converter$(EXEEXT)
+
+library_check: library/*.c
+	../ansi-c/library_check.sh $(CC) $^
+	touch $@
+
+cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c
+	cat library/*.c | ../ansi-c/library/converter$(EXEEXT) > $@
+
+cprover_library.cpp: cprover_library.inc
+
+generated_files: cprover_library.inc
+
+###############################################################################
+
 cpp$(LIBEXT): $(OBJ)
 	$(LINKLIB)

src/cpp/cprover_library.cpp

@@ -0,0 +1,50 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "cprover_library.h"
+
+#include <sstream>
+
+#include <util/config.h>
+
+#include <ansi-c/cprover_library.h>
+
+static std::string get_cprover_library_text(
+  const std::set<irep_idt> &functions,
+  const symbol_tablet &symbol_table)
+{
+  std::ostringstream library_text;
+
+  library_text << "#line 1 \"<builtin-library>\"\n"
+               << "#undef inline\n";
+
+  // cprover_library.inc may not have been generated when running Doxygen, thus
+  // make Doxygen skip this part
+  /// \cond
+  const struct cprover_library_entryt cprover_library[] =
+#include "cprover_library.inc"
+    ; // NOLINT(whitespace/semicolon)
+  /// \endcond
+
+  return get_cprover_library_text(
+    functions, symbol_table, cprover_library, library_text.str());
+}
+
+void add_cprover_cpp_library(
+  const std::set<irep_idt> &functions,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
+{
+  if(config.ansi_c.lib == configt::ansi_ct::libt::LIB_NONE)
+    return;
+
+  const std::string library_text =
+    get_cprover_library_text(functions, symbol_table);
+
+  add_library(library_text, symbol_table, message_handler);
+}

src/cpp/cprover_library.h

@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_CPP_CPROVER_LIBRARY_H
+#define CPROVER_CPP_CPROVER_LIBRARY_H
+
+#include <set>
+
+#include <util/irep.h>
+
+class message_handlert;
+class symbol_tablet;
+
+void add_cprover_cpp_library(
+  const std::set<irep_idt> &functions,
+  symbol_tablet &,
+  message_handlert &);
+
+#endif // CPROVER_CPP_CPROVER_LIBRARY_H

src/cpp/library/cprover.h

@@ -0,0 +1,52 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_CPP_LIBRARY_CPROVER_H
+#define CPROVER_CPP_LIBRARY_CPROVER_H
+
+// NOLINTNEXTLINE(readability/identifiers)
+typedef __typeof__(sizeof(int)) __CPROVER_size_t;
+void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
+extern const void *__CPROVER_deallocated;
+extern const void *__CPROVER_malloc_object;
+extern __CPROVER_size_t __CPROVER_malloc_size;
+extern _Bool __CPROVER_malloc_is_new_array;
+extern const void *__CPROVER_memory_leak;
+
+void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
+void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
+void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
+
+void __CPROVER_input(const char *id, ...);
+void __CPROVER_output(const char *id, ...);
+
+// concurrency-related
+void __CPROVER_atomic_begin();
+void __CPROVER_atomic_end();
+void __CPROVER_fence(const char *kind, ...);
+
+// pointers
+unsigned __CPROVER_POINTER_OBJECT(const void *p);
+signed __CPROVER_POINTER_OFFSET(const void *p);
+__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
+
+// arrays
+// __CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
+void __CPROVER_array_copy(const void *dest, const void *src);
+void __CPROVER_array_set(const void *dest, ...);
+void __CPROVER_array_replace(const void *dest, const void *src);
+
+void __CPROVER_set_must(const void *, const char *);
+void __CPROVER_set_may(const void *, const char *);
+void __CPROVER_clear_must(const void *, const char *);
+void __CPROVER_clear_may(const void *, const char *);
+void __CPROVER_cleanup(const void *, void (*)(void *));
+__CPROVER_bool __CPROVER_get_must(const void *, const char *);
+__CPROVER_bool __CPROVER_get_may(const void *, const char *);
+
+#endif // CPROVER_CPP_LIBRARY_CPROVER_H

src/cpp/library/module_dependencies.txt

@@ -0,0 +1,2 @@
+cpp
+cpp/library

src/ansi-c/library/new.c renamed to src/cpp/library/new.c

@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/cprover_library.h>
 
 #include <cpp/cpp_language.h>
+#include <cpp/cprover_library.h>
+
 #include <jsil/jsil_language.h>
 
 #include <goto-programs/initialize_goto_model.h>
@@ -727,6 +729,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
 
     // add the library
     status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
+    link_to_library(goto_model, ui_message_handler, add_cprover_cpp_library);
     link_to_library(goto_model, ui_message_handler, add_cprover_c_library);
     #endif
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -53,6 +53,7 @@ Author: Peter Schrammel
 #include <langapi/mode.h>
 
 #include <ansi-c/cprover_library.h>
+#include <cpp/cprover_library.h>
 
 #include <cbmc/version.h>
 
@@ -397,6 +398,7 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // add the library
     status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
+    link_to_library(goto_model, get_message_handler(), add_cprover_cpp_library);
     link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
 
     // remove function pointers

src/goto-diff/goto_diff_parse_options.cpp

@@ -63,6 +63,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/is_threaded.h>
 
 #include <ansi-c/cprover_library.h>
+#include <cpp/cprover_library.h>
 
 #include <cbmc/version.h>
 
@@ -960,6 +961,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     // add the library
     status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
+    link_to_library(goto_model, get_message_handler(), add_cprover_cpp_library);
     link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
   }