diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 00d129c0b..eb67083c2 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -164,11 +164,14 @@ add_executable(test-z3 z3_add_install_tactic_rule(${z3_test_deps}) z3_add_memory_initializer_rule(${z3_test_deps}) z3_add_gparams_register_modules_rule(${z3_test_deps}) -target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES} Z3_TEST_SRC_DIR="${CMAKE_CURRENT_SOURCE_DIR}" Z3_TEST_BIN_DIR="${PROJECT_BINARY_DIR}") +target_compile_definitions(test-z3 PRIVATE + ${Z3_COMPONENT_CXX_DEFINES} + Z3_TEST_SRC_DIR="${CMAKE_CURRENT_SOURCE_DIR}" + Z3_TEST_BIN_DIR="${PROJECT_BINARY_DIR}" +) target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS}) target_include_directories(test-z3 PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) z3_append_linker_flag_list_to_target(test-z3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps}) add_dependencies(test-z3 shell) - diff --git a/src/test/tptp.cpp b/src/test/tptp.cpp index f1558a08d..bb9c6d0a5 100644 --- a/src/test/tptp.cpp +++ b/src/test/tptp.cpp @@ -2,6 +2,8 @@ #include #include #include +#include +#include #include "util/debug.h" #ifdef _WINDOWS @@ -20,16 +22,33 @@ struct tptp_case { char const* expected_status; }; -constexpr unsigned tptp_buf_sz = 4096; +constexpr unsigned tptp_buffer_size = 4096; + +static bool is_safe_file_name(char const* s) { + while (*s) { + unsigned char c = static_cast(*s); + if (!(std::isalnum(c) || c == '.' || c == '-' || c == '_')) + return false; + ++s; + } + return true; +} static std::string run_tptp(char const* file) { + if (!is_safe_file_name(file)) { + std::cerr << "Unsafe TPTP test filename: " << file << "\n"; + ENSURE(false); + } std::ostringstream cmd; cmd << "\"" << Z3_TEST_BIN_DIR << "/" << z3_bin_name << "\" -tptp " << "\"" << Z3_TEST_SRC_DIR << "/tptp/" << file << "\" 2>&1"; FILE* pipe = Z3_POPEN(cmd.str().c_str(), "r"); - ENSURE(pipe != nullptr); + if (!pipe) { + std::cerr << "Failed to execute command: " << cmd.str() << "\n"; + ENSURE(false); + } std::string out; - char buffer[tptp_buf_sz]; + char buffer[tptp_buffer_size]; while (fgets(buffer, sizeof(buffer), pipe)) out += buffer; int code = Z3_PCLOSE(pipe); @@ -37,7 +56,11 @@ static std::string run_tptp(char const* file) { if (WIFEXITED(code)) code = WEXITSTATUS(code); #endif - ENSURE(code == 0); + if (code != 0) { + std::cerr << "TPTP command failed for file '" << file << "' with exit code " << code << "\n"; + std::cerr << out << "\n"; + ENSURE(false); + } return out; }