Skip to content

Move and cleanup declarations of C compiler intrinsics #6707

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 4 commits into from
Dec 8, 2022
Merged

Move and cleanup declarations of C compiler intrinsics #6707

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
6022a46
Move declarations of non-cprover intrinsics to subdirectory
tautschnig Mar 4, 2022
1de24b9
Python script to fetch declarations of Clang's intrinsics
tautschnig Mar 4, 2022
2436c5c
GCC/Clang compiler intrinsics: make zero arguments explicit
tautschnig Mar 4, 2022
371d886
GCC/Clang compiler intrinsics: make "int" explicit
tautschnig Mar 4, 2022
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
82 changes: 42 additions & 40 deletions src/ansi-c/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@ add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
add_executable(file_converter file_converter.cpp)

function(make_inc name)
get_filename_component(inc_path "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc" DIRECTORY)
add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc"
COMMAND ${CMAKE_COMMAND} -E make_directory ${inc_path}
COMMAND file_converter "${CMAKE_CURRENT_SOURCE_DIR}/${name}.h" > "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc"
DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${name}.h" file_converter
)
Expand Down Expand Up @@ -52,51 +54,51 @@ endif()

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

make_inc(arm_builtin_headers)
make_inc(clang_builtin_headers)
make_inc(compiler_headers/arm_builtin_headers)
make_inc(compiler_headers/clang_builtin_headers)
make_inc(compiler_headers/cw_builtin_headers)
make_inc(compiler_headers/gcc_builtin_headers_alpha)
make_inc(compiler_headers/gcc_builtin_headers_arm)
make_inc(compiler_headers/gcc_builtin_headers_generic)
make_inc(compiler_headers/gcc_builtin_headers_ia32)
make_inc(compiler_headers/gcc_builtin_headers_ia32-2)
make_inc(compiler_headers/gcc_builtin_headers_ia32-3)
make_inc(compiler_headers/gcc_builtin_headers_ia32-4)
make_inc(compiler_headers/gcc_builtin_headers_ia32-5)
make_inc(compiler_headers/gcc_builtin_headers_math)
make_inc(compiler_headers/gcc_builtin_headers_mem_string)
make_inc(compiler_headers/gcc_builtin_headers_mips)
make_inc(compiler_headers/gcc_builtin_headers_omp)
make_inc(compiler_headers/gcc_builtin_headers_power)
make_inc(compiler_headers/gcc_builtin_headers_tm)
make_inc(compiler_headers/gcc_builtin_headers_types)
make_inc(compiler_headers/gcc_builtin_headers_ubsan)
make_inc(compiler_headers/windows_builtin_headers)
make_inc(cprover_builtin_headers)
make_inc(cw_builtin_headers)
make_inc(gcc_builtin_headers_alpha)
make_inc(gcc_builtin_headers_arm)
make_inc(gcc_builtin_headers_generic)
make_inc(gcc_builtin_headers_ia32)
make_inc(gcc_builtin_headers_ia32-2)
make_inc(gcc_builtin_headers_ia32-3)
make_inc(gcc_builtin_headers_ia32-4)
make_inc(gcc_builtin_headers_ia32-5)
make_inc(gcc_builtin_headers_math)
make_inc(gcc_builtin_headers_mem_string)
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)
make_inc(windows_builtin_headers)

set(extra_dependencies
${CMAKE_CURRENT_BINARY_DIR}/arm_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/clang_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/arm_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/clang_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/cw_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_alpha.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_arm.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_generic.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-2.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-3.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-4.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32-5.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ia32.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_math.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_mem_string.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_mips.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_omp.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_power.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_tm.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_types.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ubsan.inc
${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/windows_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
${CMAKE_CURRENT_BINARY_DIR}/cprover_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/cw_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_alpha.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_arm.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_generic.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-2.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-3.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-4.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-5.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_math.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mem_string.inc
${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mips.inc
${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}/windows_builtin_headers.inc
${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
)

Expand Down
40 changes: 20 additions & 20 deletions src/ansi-c/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,27 +49,27 @@ include ../config.inc
include ../common

BUILTIN_FILES = \
arm_builtin_headers.inc \
clang_builtin_headers.inc \
cprover_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-5.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 \
windows_builtin_headers.inc
compiler_headers/arm_builtin_headers.inc \
compiler_headers/clang_builtin_headers.inc \
compiler_headers/cw_builtin_headers.inc \
compiler_headers/gcc_builtin_headers_alpha.inc \
compiler_headers/gcc_builtin_headers_arm.inc \
compiler_headers/gcc_builtin_headers_generic.inc \
compiler_headers/gcc_builtin_headers_ia32-2.inc \
compiler_headers/gcc_builtin_headers_ia32-3.inc \
compiler_headers/gcc_builtin_headers_ia32-4.inc \
compiler_headers/gcc_builtin_headers_ia32-5.inc \
compiler_headers/gcc_builtin_headers_ia32.inc \
compiler_headers/gcc_builtin_headers_math.inc \
compiler_headers/gcc_builtin_headers_mem_string.inc \
compiler_headers/gcc_builtin_headers_mips.inc \
compiler_headers/gcc_builtin_headers_omp.inc \
compiler_headers/gcc_builtin_headers_power.inc \
compiler_headers/gcc_builtin_headers_tm.inc \
compiler_headers/gcc_builtin_headers_types.inc \
compiler_headers/gcc_builtin_headers_ubsan.inc \
compiler_headers/windows_builtin_headers.inc

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 \
Expand Down
81 changes: 41 additions & 40 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 @@ -17,92 +17,93 @@ Author: Daniel Kroening, kroening@kroening.com

const char gcc_builtin_headers_types[] =
"#line 1 \"gcc_builtin_headers_types.h\"\n"
#include "gcc_builtin_headers_types.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_types.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_generic[] =
"#line 1 \"gcc_builtin_headers_generic.h\"\n"
#include "gcc_builtin_headers_generic.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_generic.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_math[] =
"#line 1 \"gcc_builtin_headers_math.h\"\n"
#include "gcc_builtin_headers_math.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_math.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_mem_string[] =
"#line 1 \"gcc_builtin_headers_mem_string.h\"\n"
#include "gcc_builtin_headers_mem_string.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
// NOLINTNEXTLINE(whitespace/line_length)
#include "compiler_headers/gcc_builtin_headers_mem_string.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_omp[] = "#line 1 \"gcc_builtin_headers_omp.h\"\n"
#include "gcc_builtin_headers_omp.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_omp.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_tm[] = "#line 1 \"gcc_builtin_headers_tm.h\"\n"
#include "gcc_builtin_headers_tm.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_tm.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_ubsan[] =
"#line 1 \"gcc_builtin_headers_ubsan.h\"\n"
#include "gcc_builtin_headers_ubsan.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_ubsan.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_ia32[] =
"#line 1 \"gcc_builtin_headers_ia32.h\"\n"
#include "gcc_builtin_headers_ia32.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_ia32.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
const char gcc_builtin_headers_ia32_2[] =
#include "gcc_builtin_headers_ia32-2.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_ia32-2.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
const char gcc_builtin_headers_ia32_3[] =
#include "gcc_builtin_headers_ia32-3.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_ia32-3.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
const char gcc_builtin_headers_ia32_4[] =
#include "gcc_builtin_headers_ia32-4.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_ia32-4.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
const char gcc_builtin_headers_ia32_5[] =
#include "gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_ia32-5.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_alpha[] =
"#line 1 \"gcc_builtin_headers_alpha.h\"\n"
#include "gcc_builtin_headers_alpha.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_alpha.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_arm[] = "#line 1 \"gcc_builtin_headers_arm.h\"\n"
#include "gcc_builtin_headers_arm.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_arm.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_mips[] =
"#line 1 \"gcc_builtin_headers_mips.h\"\n"
#include "gcc_builtin_headers_mips.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_mips.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char gcc_builtin_headers_power[] =
"#line 1 \"gcc_builtin_headers_power.h\"\n"
#include "gcc_builtin_headers_power.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/gcc_builtin_headers_power.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char arm_builtin_headers[] = "#line 1 \"arm_builtin_headers.h\"\n"
#include "arm_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/arm_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char cw_builtin_headers[] = "#line 1 \"cw_builtin_headers.h\"\n"
#include "cw_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/cw_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char clang_builtin_headers[] = "#line 1 \"clang_builtin_headers.h\"\n"
#include "clang_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/clang_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char cprover_builtin_headers[] = "#line 1 \"cprover_builtin_headers.h\"\n"
#include "cprover_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

const char windows_builtin_headers[] = "#line 1 \"windows_builtin_headers.h\"\n"
#include "windows_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)
#include "compiler_headers/windows_builtin_headers.inc" // IWYU pragma: keep
; // NOLINT(whitespace/semicolon)

static std::string architecture_string(const std::string &value, const char *s)
{
Expand Down
0 src/ansi-c/arm_builtin_headers.h → ...-c/compiler_headers/arm_builtin_headers.h
View file
Open in desktop
File renamed without changes.
4 changes: 2 additions & 2 deletions src/ansi-c/clang_builtin_headers.h → .../compiler_headers/clang_builtin_headers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ void __builtin_ia32_vp2intersect_d_128(__gcc_v4si, __gcc_v4si, unsigned char *,

__gcc_v16qi __builtin_ia32_selectb_128(unsigned short, __gcc_v16qi, __gcc_v16qi);
__gcc_v32qi __builtin_ia32_selectb_256(unsigned int, __gcc_v32qi, __gcc_v32qi);
__gcc_v64qi __builtin_ia32_selectb_512(unsigned long, __gcc_v64qi, __gcc_v64qi);
__gcc_v64qi __builtin_ia32_selectb_512(unsigned long int, __gcc_v64qi, __gcc_v64qi);
__gcc_v8hi __builtin_ia32_selectw_128(unsigned char, __gcc_v8hi, __gcc_v8hi);
__gcc_v16hi __builtin_ia32_selectw_256(unsigned short, __gcc_v16hi, __gcc_v16hi);
__gcc_v32hi __builtin_ia32_selectw_512(unsigned int, __gcc_v32hi, __gcc_v32hi);
Expand Down Expand Up @@ -70,7 +70,7 @@ void __builtin_ia32_tdpbsud(__tile, __tile, __tile);
void __builtin_ia32_tdpbusd(__tile, __tile, __tile);
void __builtin_ia32_tdpbuud(__tile, __tile, __tile);
void __builtin_ia32_tdpbf16ps(__tile, __tile, __tile);
void __builtin_ia32_ptwrite64(unsigned long long);
void __builtin_ia32_ptwrite64(unsigned long long int);

void __builtin_nontemporal_store();
void __builtin_nontemporal_load();
Expand Down
Loading