blob: ae038b80e52775543441a949bf205b065ad94255 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
|
#===------------------------------------------------------------------------===#
#
# The KLEE Symbolic Virtual Machine
#
# This file is distributed under the University of Illinois Open Source
# License. See LICENSE.TXT for details.
#
#===------------------------------------------------------------------------===#
set(LIT_AUTOGENERATED_WARNING "This file is autogenerated, do not edit!")
set(KLEE_TOOLS_DIR "${CMAKE_BINARY_DIR}/bin")
set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}")
# FIXME: Do this to avoid changing the template file that
# is shared by both build systems.
set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include")
set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include")
set(NATIVE_CC "${CMAKE_C_COMPILER} ${CMAKE_C_FLAGS} -I ${CMAKE_SOURCE_DIR}/include")
set(NATIVE_CXX "${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} -I ${CMAKE_SOURCE_DIR}/include")
set(TARGET_TRIPLE "${TARGET_TRIPLE}")
# Extend native compiler invocation on macOS to point to the currently selected systems directory
if (${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
execute_process(
COMMAND xcrun --sdk macosx --show-sdk-path
OUTPUT_VARIABLE MAC_OS_SDK_PATH
OUTPUT_STRIP_TRAILING_WHITESPACE)
set(NATIVE_CC "${NATIVE_CC} -isysroot ${MAC_OS_SDK_PATH}")
set(NATIVE_CXX "${NATIVE_CXX} -isysroot ${MAC_OS_SDK_PATH}")
endif()
if (NOT KLEE_UCLIBC_PATH STREQUAL "")
set(SUPPORT_KLEE_UCLIBC 1)
else()
set(SUPPORT_KLEE_UCLIBC 0)
endif()
# FIXME: Do this to avoid changing the template file that
# is shared by both build systems.
if (ENABLE_POSIX_RUNTIME)
if (NOT KLEE_UCLIBC_PATH STREQUAL "")
set(ENABLE_POSIX_RUNTIME 1)
else()
message(AUTHOR_WARNING
"Disabling POSIX runtime tests because they depend on klee-uclibc"
"\nFIXME!")
set(ENABLE_POSIX_RUNTIME 0)
endif()
else()
set(ENABLE_POSIX_RUNTIME 0)
endif()
###############################################################################
# Find LLVM testing tools
###############################################################################
option(DOWNLOAD_LLVM_TESTING_TOOLS "Always download LLVM testing tools sources" OFF)
mark_as_advanced(DOWNLOAD_LLVM_TESTING_TOOLS)
# Check `FileCheck` and the `not` tools are available. By default we'll try
# looking in the LLVM binary directory. If that fails download the sources.
# This might be necessary if using a shipped version of LLVM because LLVM
# unfortunately does not ship its testing tools.
set(DOWNLOAD_FILECHECK_SOURCE FALSE)
set(DOWNLOAD_NOT_SOURCE FALSE)
if (DOWNLOAD_LLVM_TESTING_TOOLS)
set(DOWNLOAD_FILECHECK_SOURCE TRUE)
set(DOWNLOAD_NOT_SOURCE TRUE)
endif()
if (NOT EXISTS "${LLVM_TOOLS_BINARY_DIR}/FileCheck")
message(WARNING "\"${LLVM_TOOLS_BINARY_DIR}/FileCheck\" does not exist. Downloading sources.")
set(DOWNLOAD_FILECHECK_SOURCE TRUE)
endif()
if (NOT EXISTS "${LLVM_TOOLS_BINARY_DIR}/not")
message(WARNING "\"${LLVM_TOOLS_BINARY_DIR}/not\" does not exist. Downloading sources.")
set(DOWNLOAD_NOT_SOURCE TRUE)
endif()
# Do not build FileCheck and not to ${KLEE_TOOLS_DIR} as it will not be in lit's PATH.
set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${KLEE_TOOLS_DIR}/testtools)
if (DOWNLOAD_FILECHECK_SOURCE)
set(FILECHECK_SRC_URL "https://raw.githubusercontent.com/llvm/llvm-project/release/${LLVM_VERSION_MAJOR}.x/llvm/utils/FileCheck/FileCheck.cpp")
set(FILECHECK_SRC_FILE "${CMAKE_CURRENT_BINARY_DIR}/FileCheck.cpp")
if (NOT EXISTS "${FILECHECK_SRC_FILE}")
message(STATUS "Downloading LLVM FileCheck source")
file(DOWNLOAD "${FILECHECK_SRC_URL}" "${FILECHECK_SRC_FILE}" SHOW_PROGRESS STATUS DOWNLOAD_STATUS)
list(GET DOWNLOAD_STATUS 0 DOWNLOAD_STATUS_CODE)
if (NOT DOWNLOAD_STATUS_CODE EQUAL 0)
file(REMOVE "${FILECHECK_SRC_FILE}")
list(GET DOWNLOAD_STATUS 1 DOWNLOAD_STATUS_MESSAGE)
message(FATAL_ERROR "Download failed with error: ${DOWNLOAD_STATUS_CODE} - ${DOWNLOAD_STATUS_MESSAGE}")
endif()
endif()
add_executable(FileCheck
${FILECHECK_SRC_FILE}
)
llvm_config(FileCheck "${USE_LLVM_SHARED}" support)
target_include_directories(FileCheck PRIVATE ${LLVM_INCLUDE_DIRS})
target_link_libraries(FileCheck PRIVATE ${FILECHECK_NEEDED_LIBS})
endif()
if (DOWNLOAD_NOT_SOURCE)
set(NOT_SRC_URL "https://raw.githubusercontent.com/llvm/llvm-project/release/${LLVM_VERSION_MAJOR}.x/llvm/utils/not/not.cpp")
set(NOT_SRC_FILE "${CMAKE_CURRENT_BINARY_DIR}/not.cpp")
if (NOT EXISTS "${NOT_SRC_FILE}")
message(STATUS "Downloading LLVM not source")
file(DOWNLOAD "${NOT_SRC_URL}" "${NOT_SRC_FILE}" SHOW_PROGRESS STATUS DOWNLOAD_STATUS)
list(GET DOWNLOAD_STATUS 0 DOWNLOAD_STATUS_CODE)
if (NOT DOWNLOAD_STATUS_CODE EQUAL 0)
file(REMOVE "${NOT_SRC_FILE}")
list(GET DOWNLOAD_STATUS 1 DOWNLOAD_STATUS_MESSAGE)
message(FATAL_ERROR "Download failed with error: ${DOWNLOAD_STATUS_CODE} - ${DOWNLOAD_STATUS_MESSAGE}")
endif()
endif()
add_executable("not"
${NOT_SRC_FILE}
)
llvm_config("not" "${USE_LLVM_SHARED}" support)
target_include_directories("not" PRIVATE ${LLVM_INCLUDE_DIRS})
target_link_libraries("not" PRIVATE ${NOT_NEEDED_LIBS})
endif()
###############################################################################
# Concrete tests build system
###############################################################################
add_subdirectory(Concrete)
###############################################################################
# Configure lit test suite
###############################################################################
# Find path to libkleeRuntest target for `lit.site.cfg`.
set(LIB_KLEE_RUN_TEST_PATH $<TARGET_FILE:kleeRuntest>)
configure_file(lit.site.cfg.in
${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg.imd
@ONLY
)
# Evaluate all generator expressions inserted during the configure step.
file(GENERATE
OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg
INPUT ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg.imd
)
add_custom_target(systemtests
COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS klee kleaver klee-ptree klee-replay kleeRuntest ktest-gen ktest-randgen
COMMENT "Running system tests"
USES_TERMINAL
)
# Tell CMake to remove lit's output directories when
# running `make clean`.
file(GLOB_RECURSE
test_contents
LIST_DIRECTORIES true
RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}"
"*"
)
set(dirs_to_clean "")
foreach (f ${test_contents})
if (IS_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/${f}")
list(APPEND dirs_to_clean "${CMAKE_CURRENT_BINARY_DIR}/${f}/Output")
endif()
endforeach()
set_property(
DIRECTORY
APPEND
PROPERTY ADDITIONAL_MAKE_CLEAN_FILES
${dirs_to_clean}
)
|
