about summary refs log tree commit diff homepage
path: root/unittests
diff options
context:
space:
mode:
Diffstat (limited to 'unittests')
-rw-r--r--unittests/Assignment/CMakeLists.txt4
-rw-r--r--unittests/CMakeLists.txt100
-rw-r--r--unittests/Expr/CMakeLists.txt6
-rw-r--r--unittests/Ref/CMakeLists.txt6
-rw-r--r--unittests/Solver/CMakeLists.txt12
-rw-r--r--unittests/lit-unit-tests-common.cfg11
-rw-r--r--unittests/lit-unit-tests-common.site.cfg.in9
7 files changed, 148 insertions, 0 deletions
diff --git a/unittests/Assignment/CMakeLists.txt b/unittests/Assignment/CMakeLists.txt
new file mode 100644
index 00000000..e231ee39
--- /dev/null
+++ b/unittests/Assignment/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_klee_unit_test(AssignmentTest
+  AssignmentTest.cpp)
+klee_get_llvm_libs(LLVM_LIBS Support)
+target_link_libraries(AssignmentTest PRIVATE kleaverExpr ${LLVM_LIBS})
diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt
new file mode 100644
index 00000000..a85c0a74
--- /dev/null
+++ b/unittests/CMakeLists.txt
@@ -0,0 +1,100 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+# Build GTest. We don't use a pre-built version due to
+# https://github.com/google/googletest/blob/master/googletest/docs/FAQ.md#why-is-it-not-recommended-to-install-a-pre-compiled-copy-of-google-test-for-example-into-usrlocal
+set(GTEST_SRC_DIR
+  "/usr/src/gtest"
+  CACHE
+  PATH
+  "Path to GTest source directory"
+)
+
+if (NOT EXISTS "${GTEST_SRC_DIR}")
+  message(FATAL_ERROR "GTest source directory \"${GTEST_SRC_DIR}\" cannot be found.\n"
+    "Try passing -DGTEST_SRC_DIR=<path_to_gtest_source> to cmake where "
+    "<path_to_gtest_source> is the path to the GoogleTest source tree.\n"
+    "Alternatively you can disable unit tests by passing "
+    "-DENABLE_UNIT_TESTS=OFF to cmake.")
+endif()
+
+# It's important that GTest is built with KLEE's compile flags
+# so set them here.
+set(_OLD_CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS}")
+foreach (f ${KLEE_COMPONENT_CXX_FLAGS})
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${f}")
+endforeach()
+foreach (f ${KLEE_COMPONENT_CXX_DEFINES})
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${f}")
+endforeach()
+
+# Build GTest as part of our project
+# FIXME: Prevent GTest from adding to our install target.
+# This is a problem for GTest >= 1.8. I've filled a PR to fix the issue
+# ( https://github.com/google/googletest/pull/921 ). If it gets accepted
+# we can do `set(gtest_enable_install FALSE)` to fix this.
+add_subdirectory(${GTEST_SRC_DIR} "${CMAKE_CURRENT_BINARY_DIR}/gtest_build")
+
+set(CMAKE_CXX_FLAGS "${_OLD_CMAKE_CXX_FLAGS}") # Restore the flags
+
+# This keeps track of all the unit test
+# targets so we can ensure they are built
+# before trying to run them.
+define_property(GLOBAL
+  PROPERTY KLEE_UNIT_TEST_TARGETS
+  BRIEF_DOCS "KLEE unit tests"
+  FULL_DOCS "KLEE unit tests"
+)
+
+set(GTEST_INCLUDE_DIR "${GTEST_SRC_DIR}/include")
+
+if (NOT IS_DIRECTORY "${GTEST_INCLUDE_DIR}")
+  message(FATAL_ERROR
+    "Cannot find GTest include directory \"${GTEST_INCLUDE_DIR}\"")
+endif()
+
+function(add_klee_unit_test target_name)
+  add_executable(${target_name} ${ARGN})
+  target_link_libraries(${target_name} PRIVATE gtest_main)
+  target_include_directories(${target_name} BEFORE PRIVATE "${GTEST_INCLUDE_DIR}")
+  set_target_properties(${target_name}
+    PROPERTIES
+    RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/unittests/"
+  )
+  set_property(GLOBAL
+    APPEND
+    PROPERTY KLEE_UNIT_TEST_TARGETS
+    ${target_name}
+  )
+endfunction()
+
+# Unit Tests
+add_subdirectory(Assignment)
+add_subdirectory(Expr)
+add_subdirectory(Ref)
+add_subdirectory(Solver)
+
+# Set up lit configuration
+set (UNIT_TEST_EXE_SUFFIX "Test")
+configure_file(lit-unit-tests-common.site.cfg.in
+  ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg
+  @ONLY)
+
+# Add a target to run all the unit tests using lit
+get_property(UNIT_TEST_DEPENDS
+  GLOBAL
+  PROPERTY KLEE_UNIT_TEST_TARGETS
+)
+add_custom_target(unittests
+  COMMAND
+    "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}"
+    DEPENDS ${UNIT_TEST_DEPENDS}
+    COMMENT "Running unittests"
+    ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
diff --git a/unittests/Expr/CMakeLists.txt b/unittests/Expr/CMakeLists.txt
new file mode 100644
index 00000000..4e7bc997
--- /dev/null
+++ b/unittests/Expr/CMakeLists.txt
@@ -0,0 +1,6 @@
+add_klee_unit_test(ExprTest
+  ExprTest.cpp)
+# FIXME: KLEE's libraries should just declare what libraries
+# they depend on so we don't need to manually link.
+klee_get_llvm_libs(LLVM_LIBS Support)
+target_link_libraries(ExprTest PRIVATE kleaverExpr ${LLVM_LIBS})
diff --git a/unittests/Ref/CMakeLists.txt b/unittests/Ref/CMakeLists.txt
new file mode 100644
index 00000000..d678930c
--- /dev/null
+++ b/unittests/Ref/CMakeLists.txt
@@ -0,0 +1,6 @@
+add_klee_unit_test(RefTest
+  RefTest.cpp)
+# FIXME: KLEE's libraries should just declare what libraries
+# they depend on so we don't need to manually link.
+klee_get_llvm_libs(LLVM_LIBS Support)
+target_link_libraries(RefTest PRIVATE kleaverExpr ${LLVM_LIBS})
diff --git a/unittests/Solver/CMakeLists.txt b/unittests/Solver/CMakeLists.txt
new file mode 100644
index 00000000..602a1196
--- /dev/null
+++ b/unittests/Solver/CMakeLists.txt
@@ -0,0 +1,12 @@
+add_klee_unit_test(SolverTest
+  SolverTest.cpp)
+# FIXME: KLEE's libraries should just declare what libraries
+# they depend on so we don't need to manually link.
+klee_get_llvm_libs(LLVM_LIBS Support)
+target_link_libraries(SolverTest
+  PRIVATE
+  kleaverSolver
+  kleaverExpr
+  kleeSupport
+  kleeBasic
+  ${LLVM_LIBS})
diff --git a/unittests/lit-unit-tests-common.cfg b/unittests/lit-unit-tests-common.cfg
new file mode 100644
index 00000000..57663ff7
--- /dev/null
+++ b/unittests/lit-unit-tests-common.cfg
@@ -0,0 +1,11 @@
+# Configuration file for the 'lit' test runner.
+
+import os
+
+import lit.formats
+
+# suffixes: A list of file extensions to treat as test files.
+config.suffixes = []
+
+# testFormat: The test format to use to interpret tests.
+config.test_format = lit.formats.GoogleTest('.', config.unit_test_exe_suffix)
diff --git a/unittests/lit-unit-tests-common.site.cfg.in b/unittests/lit-unit-tests-common.site.cfg.in
new file mode 100644
index 00000000..f106152f
--- /dev/null
+++ b/unittests/lit-unit-tests-common.site.cfg.in
@@ -0,0 +1,9 @@
+import sys
+import os
+
+## @AUTO_GEN_MSG@
+config.name = 'KLEE Unit tests'
+config.unit_test_exe_suffix = "@UNIT_TEST_EXE_SUFFIX@"
+
+# Let the main config do the real work.
+lit_config.load_config(config, "@CMAKE_SOURCE_DIR@/unittests/lit-unit-tests-common.cfg")