Merge pull request diffblue#2294 from tautschnig/c++-built-ins

C++ front-end: Use C factory for compiler builtins
NathanJPhillips · Jun 8, 2018 · 894a20f · 894a20f
2 parents 6877b21 + 4edecbc
commit 894a20f
Show file tree

Hide file tree

Showing 28 changed files with 395 additions and 122 deletions.
diff --git a/.gitignore b/.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

diff --git a/.travis.yml b/.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

diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/link_to_library.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>

diff --git a/jbmc/src/java_bytecode/CMakeLists.txt b/jbmc/src/java_bytecode/CMakeLists.txt
@@ -12,4 +12,4 @@ generic_includes(java_bytecode)
 
 # if you link java_bytecode.a in, then you also need to link other .a libraries
 # in
-target_link_libraries(java_bytecode util goto-programs miniz json)
+target_link_libraries(java_bytecode util goto-programs miniz json ansi-c)
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -338,9 +338,6 @@ bool jdiff_parse_optionst::process_goto_program(
 {
   try
   {
-    // add the library
-    link_to_library(goto_model, get_message_handler());
-
     // remove function pointers
     status() << "Removal of function pointers and virtual functions" << eom;
     remove_function_pointers(

diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt
@@ -50,7 +50,7 @@ add_custom_command(
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
 )
 
-add_custom_target(library_check
+add_custom_target(c_library_check
     DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
 )
 

diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp
@@ -14,15 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_language.h"
 
-struct cprover_library_entryt
-{
-  const char *function;
-  const char *model;
-} cprover_library[]=
-#include "cprover_library.inc"
-; // NOLINT(whitespace/semicolon)
-
-std::string get_cprover_library_text(
+static std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
   const symbol_tablet &symbol_table)
 {
@@ -35,10 +27,29 @@ std::string get_cprover_library_text(
   if(config.ansi_c.string_abstraction)
     library_text << "#define __CPROVER_STRING_ABSTRACTION\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());
+}
+
+std::string get_cprover_library_text(
+  const std::set<irep_idt> &functions,
+  const symbol_tablet &symbol_table,
+  const struct cprover_library_entryt cprover_library[],
+  const std::string &prologue)
+{
+  std::ostringstream library_text(prologue);
+
   std::size_t count=0;
 
-  for(cprover_library_entryt *e=cprover_library;
-      e->function!=nullptr;
+  for(const cprover_library_entryt *e = cprover_library; e->function != nullptr;
       e++)
   {
     irep_idt id=e->function;
@@ -63,7 +74,7 @@ std::string get_cprover_library_text(
     return library_text.str();
 }
 
-void add_cprover_library(
+void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
   symbol_tablet &symbol_table,
   message_handlert &message_handler)

diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h
@@ -15,16 +15,24 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 #include <util/message.h>
 
+struct cprover_library_entryt
+{
+  const char *function;
+  const char *model;
+};
+
 std::string get_cprover_library_text(
   const std::set<irep_idt> &functions,
-  const symbol_tablet &);
+  const symbol_tablet &,
+  const struct cprover_library_entryt[],
+  const std::string &prologue);
 
 void add_library(
   const std::string &src,
   symbol_tablet &,
   message_handlert &);
 
-void add_cprover_library(
+void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
   symbol_tablet &,
   message_handlert &);

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -24,6 +24,9 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 
 #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>
@@ -711,7 +714,12 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_asm(goto_model);
 
     // add the library
-    link_to_library(goto_model, log.get_message_handler());
+    log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
+                 << eom;
+    link_to_library(
+      goto_model, log.get_message_handler(), cprover_cpp_library_factory);
+    link_to_library(
+      goto_model, log.get_message_handler(), cprover_c_library_factory);
 
     if(options.get_bool_option("string-abstraction"))
       string_instrumentation(goto_model, log.get_message_handler());

diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
@@ -27,7 +27,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/set_properties.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/loop_ids.h>
-#include <goto-programs/link_to_library.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
 

diff --git a/src/cpp/CMakeLists.txt b/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})
 

diff --git a/src/cpp/Makefile b/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)