blob: 2e97f38a0effcc0de95a40fe3cfe48dc82bd5791 (
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
|
#===------------------------------------------------------------------------===#
#
# The KLEE Symbolic Virtual Machine
#
# This file is distributed under the University of Illinois Open Source
# License. See LICENSE.TXT for details.
#
#===------------------------------------------------------------------------===#
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}")
if (ENABLE_KLEE_UCLIBC)
set(ENABLE_UCLIBC 1)
else()
set(ENABLE_UCLIBC 0)
endif()
# FIXME: Do this to avoid changing the template file that
# is shared by both build systems.
if (ENABLE_POSIX_RUNTIME)
if (ENABLE_KLEE_UCLIBC)
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()
if (DOWNLOAD_FILECHECK_SOURCE)
set(FILECHECK_SRC_URL "https://raw.githubusercontent.com/llvm-mirror/llvm/release_${LLVM_VERSION_MAJOR}${LLVM_VERSION_MINOR}/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)
endif()
add_executable(FileCheck
${FILECHECK_SRC_FILE}
)
klee_get_llvm_libs(FILECHECK_NEEDED_LIBS Support)
target_include_directories(FileCheck PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS})
target_compile_options(FileCheck PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
target_compile_definitions(FileCheck PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
target_link_libraries(FileCheck PRIVATE ${FILECHECK_NEEDED_LIBS})
endif()
if (DOWNLOAD_NOT_SOURCE)
set(NOT_SRC_URL "https://raw.githubusercontent.com/llvm-mirror/llvm/release_${LLVM_VERSION_MAJOR}${LLVM_VERSION_MINOR}/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)
endif()
add_executable("not"
${NOT_SRC_FILE}
)
klee_get_llvm_libs(NOT_NEEDED_LIBS Support)
target_include_directories("not" PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS})
target_compile_options("not" PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
target_compile_definitions("not" PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
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`.
# FIXME: This is not the right way to get the location of the target we have to
# set CMP0026 to old.
# This will likely break if using a multi-configuration generator.
if (POLICY CMP0026)
# HACK: Allow reading `LOCATION` property.
cmake_policy(SET CMP0026 OLD)
endif()
get_property(LIB_KLEE_RUN_TEST_PATH
TARGET kleeRuntest
PROPERTY LOCATION
)
configure_file(lit.site.cfg.in
${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg
@ONLY
)
add_custom_target(systemtests
COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}"
DEPENDS klee kleaver kleeRuntest
COMMENT "Running system tests"
${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
)
# 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}
)
|
