Skip to content

on-demand definitions for compiler-built-in functions #1910

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Mar 7, 2018
Merged

on-demand definitions for compiler-built-in functions #1910

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
4a5b952
export all gcc bultin headers
kroening Mar 5, 2018
1711345
added a factory for builtin function declarations
kroening Mar 5, 2018
15ec42f
use the builtins factory in the C frontend
kroening Mar 5, 2018
80ee0b1
pass type definitions to the C++ front-end
kroening Mar 5, 2018
17d9897
switch to C++ version of find_pattern
kroening Mar 6, 2018
2c8ae92
Makefile: use a variable for all those generated .inc files
kroening Mar 6, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/ansi-c/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ make_inc(gcc_builtin_headers_mips)
make_inc(gcc_builtin_headers_omp)
make_inc(gcc_builtin_headers_power)
make_inc(gcc_builtin_headers_tm)
make_inc(gcc_builtin_headers_types)
make_inc(gcc_builtin_headers_ubsan)

set(extra_dependencies
Expand All @@ -92,6 +93,7 @@ set(extra_dependencies
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_omp.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_power.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_tm.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_types.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc
${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
)
Expand Down
65 changes: 28 additions & 37 deletions src/ansi-c/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ SRC = anonymous_member.cpp \
ansi_c_scope.cpp \
ansi_c_typecheck.cpp \
ansi_c_y.tab.cpp \
builtin_factory.cpp \
c_misc.cpp \
c_nondet_symbol_factory.cpp \
c_preprocess.cpp \
Expand Down Expand Up @@ -43,20 +44,32 @@ INCLUDES= -I ..
include ../config.inc
include ../common

BUILTIN_FILES = \
arm_builtin_headers.inc \
clang_builtin_headers.inc \
cw_builtin_headers.inc \
gcc_builtin_headers_alpha.inc \
gcc_builtin_headers_arm.inc \
gcc_builtin_headers_generic.inc \
gcc_builtin_headers_ia32-2.inc \
gcc_builtin_headers_ia32-3.inc \
gcc_builtin_headers_ia32-4.inc \
gcc_builtin_headers_ia32.inc \
gcc_builtin_headers_math.inc \
gcc_builtin_headers_mem_string.inc \
gcc_builtin_headers_mips.inc \
gcc_builtin_headers_omp.inc \
gcc_builtin_headers_power.inc \
gcc_builtin_headers_tm.inc \
gcc_builtin_headers_types.inc \
gcc_builtin_headers_ubsan.inc
Copy link
Collaborator

@tautschnig tautschnig Mar 6, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While at this, would it be possible to introduce a Makefile variable holding all the header files? As is, the same list of files appears three times.

Copy link
Collaborator Author

@kroening kroening Mar 6, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done


CLEANFILES = ansi-c$(LIBEXT) \
ansi_c_y.tab.h ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.cpp.output \
ansi_c_y.output \
library/converter$(EXEEXT) cprover_library.inc \
file_converter$(EXEEXT) library_check \
gcc_builtin_headers_generic.inc gcc_builtin_headers_ia32.inc \
arm_builtin_headers.inc cw_builtin_headers.inc \
gcc_builtin_headers_arm.inc gcc_builtin_headers_alpha.inc \
gcc_builtin_headers_mips.inc gcc_builtin_headers_power.inc \
clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
gcc_builtin_headers_mem_string.inc \
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
$(BUILTIN_FILES)

all: ansi-c$(LIBEXT)

Expand Down Expand Up @@ -102,34 +115,12 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c

cprover_library.cpp: cprover_library.inc

ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc
ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc
ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc
ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc
ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc

generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \
gcc_builtin_headers_ia32.inc gcc_builtin_headers_alpha.inc \
gcc_builtin_headers_arm.inc gcc_builtin_headers_mips.inc \
gcc_builtin_headers_power.inc arm_builtin_headers.inc \
cw_builtin_headers.inc ansi_c_y.tab.cpp ansi_c_lex.yy.cpp \
ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \
gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \
gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \
gcc_builtin_headers_mem_string.inc \
gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc
ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES)

generated_files: \
ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.h \
cprover_library.inc \
$(BUILTIN_FILES)

###############################################################################

Expand Down
48 changes: 10 additions & 38 deletions src/ansi-c/ansi_c_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com

#include <util/config.h>

const char gcc_builtin_headers_types[]=
"# 1 \"gcc_builtin_headers_types.h\"\n"
#include "gcc_builtin_headers_types.inc"
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_generic[]=
"# 1 \"gcc_builtin_headers_generic.h\"\n"
#include "gcc_builtin_headers_generic.inc"
Expand Down Expand Up @@ -89,6 +94,10 @@ const char clang_builtin_headers[]=
#include "clang_builtin_headers.inc"
; // NOLINT(whitespace/semicolon)

const char windows_builtin_headers[]=
"int __noop();\n"
Copy link
Collaborator

@tautschnig tautschnig Mar 6, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this have a file name as the others do?

Copy link
Collaborator Author

@kroening kroening Mar 6, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seemed unnecessary luxury for two lines.

Copy link
Collaborator

@tautschnig tautschnig Mar 6, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One day those 2 lines will be 10 and no-one will notice that they should have inserted the file name. It's near zero cost right now, but it might prove costly later.

"int __assume(int);\n";

static std::string architecture_string(const std::string &value, const char *s)
{
return std::string("const char *__CPROVER_architecture_")+
Expand Down Expand Up @@ -257,13 +266,7 @@ void ansi_c_internal_additions(std::string &code)
config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE ||
config.ansi_c.mode==configt::ansi_ct::flavourt::ARM)
{
code+=gcc_builtin_headers_generic;
code+=gcc_builtin_headers_math;
code+=gcc_builtin_headers_mem_string;
code+=gcc_builtin_headers_omp;
code+=gcc_builtin_headers_tm;
code+=gcc_builtin_headers_ubsan;
code+=clang_builtin_headers;
code+=gcc_builtin_headers_types;

// there are many more, e.g., look at
// https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
Expand All @@ -274,37 +277,6 @@ void ansi_c_internal_additions(std::string &code)
{
if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE)
code+="typedef double __float128;\n"; // clang doesn't do __float128

code+=gcc_builtin_headers_ia32;
code+=gcc_builtin_headers_ia32_2;
code+=gcc_builtin_headers_ia32_3;
code+=gcc_builtin_headers_ia32_4;
}
else if(config.ansi_c.arch=="arm64" ||
config.ansi_c.arch=="armel" ||
config.ansi_c.arch=="armhf" ||
config.ansi_c.arch=="arm")
{
code+=gcc_builtin_headers_arm;
}
else if(config.ansi_c.arch=="alpha")
{
code+=gcc_builtin_headers_alpha;
}
else if(config.ansi_c.arch=="mips64el" ||
config.ansi_c.arch=="mipsn32el" ||
config.ansi_c.arch=="mipsel" ||
config.ansi_c.arch=="mips64" ||
config.ansi_c.arch=="mipsn32" ||
config.ansi_c.arch=="mips")
{
code+=gcc_builtin_headers_mips;
}
else if(config.ansi_c.arch=="powerpc" ||
config.ansi_c.arch=="ppc64" ||
config.ansi_c.arch=="ppc64le")
{
code+=gcc_builtin_headers_power;
}

// On 64-bit systems, gcc has typedefs
Expand Down
9 changes: 8 additions & 1 deletion src/ansi-c/ansi_c_internal_additions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,17 +15,24 @@ Author: Daniel Kroening, kroening@kroening.com
void ansi_c_internal_additions(std::string &code);
void ansi_c_architecture_strings(std::string &code);

extern const char clang_builtin_headers[];
extern const char gcc_builtin_headers_types[];
extern const char gcc_builtin_headers_generic[];
extern const char gcc_builtin_headers_math[];
extern const char gcc_builtin_headers_mem_string[];
extern const char gcc_builtin_headers_omp[];
extern const char gcc_builtin_headers_tm[];
extern const char gcc_builtin_headers_ubsan[];
extern const char clang_builtin_headers[];
extern const char gcc_builtin_headers_ia32[];
extern const char gcc_builtin_headers_ia32_2[];
extern const char gcc_builtin_headers_ia32_3[];
extern const char gcc_builtin_headers_ia32_4[];
extern const char gcc_builtin_headers_alpha[];
extern const char gcc_builtin_headers_arm[];
extern const char gcc_builtin_headers_mips[];
extern const char gcc_builtin_headers_power[];
extern const char arm_builtin_headers[];
extern const char cw_builtin_headers[];
extern const char windows_builtin_headers[];

#endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H
Loading