Skip to content

Commit 894a20f

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#2294 from tautschnig/c++-built-ins
C++ front-end: Use C factory for compiler builtins
2 parents 6877b21 + 4edecbc commit 894a20f

28 files changed

+395
-122
lines changed

‎.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,7 @@ src/ansi-c/gcc_builtin_headers_mips.inc
4949
src/ansi-c/gcc_builtin_headers_power.inc
5050
src/ansi-c/gcc_builtin_headers_ubsan.inc
5151
src/ansi-c/windows_builtin_headers.inc
52+
src/cpp/cprover_library.inc
5253

5354
# regression/test files
5455
*.out

‎.travis.yml

+1
Original file line numberDiff line numberDiff line change
@@ -286,6 +286,7 @@ install:
286286
- make -C jbmc/src java-models-library-download
287287
- make -C src minisat2-download
288288
- make -C src/ansi-c library_check
289+
- make -C src/cpp library_check
289290
- make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
290291
- make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
291292
- make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
2222
#include <goto-programs/goto_convert_functions.h>
2323
#include <goto-programs/goto_inline.h>
2424
#include <goto-programs/initialize_goto_model.h>
25-
#include <goto-programs/link_to_library.h>
2625
#include <goto-programs/read_goto_binary.h>
2726
#include <goto-programs/remove_complex.h>
2827
#include <goto-programs/remove_function_pointers.h>

‎jbmc/src/java_bytecode/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,4 +12,4 @@ generic_includes(java_bytecode)
1212

1313
# if you link java_bytecode.a in, then you also need to link other .a libraries
1414
# in
15-
target_link_libraries(java_bytecode util goto-programs miniz json)
15+
target_link_libraries(java_bytecode util goto-programs miniz json ansi-c)

‎jbmc/src/jdiff/jdiff_parse_options.cpp

-3
Original file line numberDiff line numberDiff line change
@@ -338,9 +338,6 @@ bool jdiff_parse_optionst::process_goto_program(
338338
{
339339
try
340340
{
341-
// add the library
342-
link_to_library(goto_model, get_message_handler());
343-
344341
// remove function pointers
345342
status() << "Removal of function pointers and virtual functions" << eom;
346343
remove_function_pointers(

‎src/ansi-c/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ add_custom_command(
5050
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
5151
)
5252

53-
add_custom_target(library_check
53+
add_custom_target(c_library_check
5454
DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
5555
)
5656

‎src/ansi-c/cprover_library.cpp

+23-12
Original file line numberDiff line numberDiff line change
@@ -14,15 +14,7 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include "ansi_c_language.h"
1616

17-
struct cprover_library_entryt
18-
{
19-
const char *function;
20-
const char *model;
21-
} cprover_library[]=
22-
#include "cprover_library.inc"
23-
; // NOLINT(whitespace/semicolon)
24-
25-
std::string get_cprover_library_text(
17+
static std::string get_cprover_library_text(
2618
const std::set<irep_idt> &functions,
2719
const symbol_tablet &symbol_table)
2820
{
@@ -35,10 +27,29 @@ std::string get_cprover_library_text(
3527
if(config.ansi_c.string_abstraction)
3628
library_text << "#define __CPROVER_STRING_ABSTRACTION\n";
3729

30+
// cprover_library.inc may not have been generated when running Doxygen, thus
31+
// make Doxygen skip this part
32+
/// \cond
33+
const struct cprover_library_entryt cprover_library[] =
34+
#include "cprover_library.inc"
35+
; // NOLINT(whitespace/semicolon)
36+
/// \endcond
37+
38+
return get_cprover_library_text(
39+
functions, symbol_table, cprover_library, library_text.str());
40+
}
41+
42+
std::string get_cprover_library_text(
43+
const std::set<irep_idt> &functions,
44+
const symbol_tablet &symbol_table,
45+
const struct cprover_library_entryt cprover_library[],
46+
const std::string &prologue)
47+
{
48+
std::ostringstream library_text(prologue);
49+
3850
std::size_t count=0;
3951

40-
for(cprover_library_entryt *e=cprover_library;
41-
e->function!=nullptr;
52+
for(const cprover_library_entryt *e = cprover_library; e->function != nullptr;
4253
e++)
4354
{
4455
irep_idt id=e->function;
@@ -63,7 +74,7 @@ std::string get_cprover_library_text(
6374
return library_text.str();
6475
}
6576

66-
void add_cprover_library(
77+
void cprover_c_library_factory(
6778
const std::set<irep_idt> &functions,
6879
symbol_tablet &symbol_table,
6980
message_handlert &message_handler)

‎src/ansi-c/cprover_library.h

+10-2
Original file line numberDiff line numberDiff line change
@@ -15,16 +15,24 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/symbol_table.h>
1616
#include <util/message.h>
1717

18+
struct cprover_library_entryt
19+
{
20+
const char *function;
21+
const char *model;
22+
};
23+
1824
std::string get_cprover_library_text(
1925
const std::set<irep_idt> &functions,
20-
const symbol_tablet &);
26+
const symbol_tablet &,
27+
const struct cprover_library_entryt[],
28+
const std::string &prologue);
2129

2230
void add_library(
2331
const std::string &src,
2432
symbol_tablet &,
2533
message_handlert &);
2634

27-
void add_cprover_library(
35+
void cprover_c_library_factory(
2836
const std::set<irep_idt> &functions,
2937
symbol_tablet &,
3038
message_handlert &);

‎src/cbmc/cbmc_parse_options.cpp

+9-1
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,9 @@ Author: Daniel Kroening, [email protected]
2424
#include <langapi/language.h>
2525

2626
#include <ansi-c/c_preprocess.h>
27+
#include <ansi-c/cprover_library.h>
28+
29+
#include <cpp/cprover_library.h>
2730

2831
#include <goto-programs/adjust_float_expressions.h>
2932
#include <goto-programs/initialize_goto_model.h>
@@ -711,7 +714,12 @@ bool cbmc_parse_optionst::process_goto_program(
711714
remove_asm(goto_model);
712715

713716
// add the library
714-
link_to_library(goto_model, log.get_message_handler());
717+
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
718+
<< eom;
719+
link_to_library(
720+
goto_model, log.get_message_handler(), cprover_cpp_library_factory);
721+
link_to_library(
722+
goto_model, log.get_message_handler(), cprover_c_library_factory);
715723

716724
if(options.get_bool_option("string-abstraction"))
717725
string_instrumentation(goto_model, log.get_message_handler());

‎src/clobber/clobber_parse_options.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,6 @@ Author: Daniel Kroening, [email protected]
2727
#include <goto-programs/set_properties.h>
2828
#include <goto-programs/read_goto_binary.h>
2929
#include <goto-programs/loop_ids.h>
30-
#include <goto-programs/link_to_library.h>
3130
#include <goto-programs/goto_inline.h>
3231
#include <goto-programs/xml_goto_trace.h>
3332

‎src/cpp/CMakeLists.txt

+30
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,33 @@
1+
file(GLOB cpp_library_sources "library/*.c")
2+
3+
add_custom_command(OUTPUT converter_input.txt
4+
COMMAND cat ${cpp_library_sources} > converter_input.txt
5+
DEPENDS ${cpp_library_sources}
6+
)
7+
8+
add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
9+
COMMAND ../ansi-c/converter < "converter_input.txt" > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
10+
DEPENDS "converter_input.txt" ../ansi-c/converter
11+
)
12+
13+
################################################################################
14+
15+
file(GLOB library_check_sources "library/*.c")
16+
17+
add_custom_command(
18+
DEPENDS ${library_check_sources}
19+
COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/../ansi-c/library_check.sh ${CMAKE_C_COMPILER} ${library_check_sources}
20+
COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
21+
OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
22+
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
23+
)
24+
25+
add_custom_target(cpp_library_check
26+
DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
27+
)
28+
29+
################################################################################
30+
131
file(GLOB_RECURSE sources "*.cpp" "*.h")
232
add_library(cpp ${sources})
333

‎src/cpp/Makefile

+18-1
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ SRC = cpp_constructor.cpp \
4242
cpp_typecheck_using.cpp \
4343
cpp_typecheck_virtual_table.cpp \
4444
cpp_util.cpp \
45+
cprover_library.cpp \
4546
expr2cpp.cpp \
4647
parse.cpp \
4748
template_map.cpp \
@@ -52,11 +53,27 @@ INCLUDES= -I ..
5253
include ../config.inc
5354
include ../common
5455

55-
CLEANFILES = cpp$(LIBEXT)
56+
CLEANFILES = cpp$(LIBEXT) cprover_library.inc library_check
5657

5758
all: cpp$(LIBEXT)
5859

5960
###############################################################################
6061

62+
../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp
63+
$(MAKE) -C ../ansi-c library/converter$(EXEEXT)
64+
65+
library_check: library/*.c
66+
../ansi-c/library_check.sh $(CC) $^
67+
touch $@
68+
69+
cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c
70+
cat library/*.c | ../ansi-c/library/converter$(EXEEXT) > $@
71+
72+
cprover_library.cpp: cprover_library.inc
73+
74+
generated_files: cprover_library.inc
75+
76+
###############################################################################
77+
6178
cpp$(LIBEXT): $(OBJ)
6279
$(LINKLIB)

0 commit comments

Comments
 (0)