From 9fea91d0eb44984217da3909ca972c28904bb040 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Mar 2026 14:57:16 -1000 Subject: [PATCH] Add parallel test execution to test-z3 (/j flag) Refactor src/test/main.cpp to support parallel test execution: - Add /j[:N] flag to run tests in parallel using N jobs (default: number of cores) - Use process-based parallelism: each test runs as a child process, avoiding thread-safety issues with global state like enable_debug/enable_trace - Output is captured per-test and printed atomically, so different tests never mix - Provide summary with pass/fail counts, wall time, and failed test names - Refactor test list into X-macros for single source of truth - Fix pre-existing bug where serial /a mode ran each test argc times Platform support: - Unix (Linux/macOS/FreeBSD): popen/pclose with WEXITSTATUS - Windows: _popen/_pclose - Emscripten: parallel disabled (no threading support) - Works with both SINGLE_THREAD and multi-threaded builds Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/test/main.cpp | 632 +++++++++++++++++++++++++++++++++------------- 1 file changed, 451 insertions(+), 181 deletions(-) diff --git a/src/test/main.cpp b/src/test/main.cpp index d388126b0..7f31e8a09 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -1,7 +1,10 @@ -#include -#include -#include -#include +#include +#include +#include +#include +#include +#include +#include #include "util/util.h" #include "util/trace.h" #include "util/debug.h" @@ -10,6 +13,23 @@ #include "util/memory_manager.h" #include "util/gparams.h" +#ifndef __EMSCRIPTEN__ +#include +#include +#include +#endif + +#if !defined(__EMSCRIPTEN__) && !defined(_WINDOWS) +#include +#endif + +#ifdef _WINDOWS +#define Z3_POPEN _popen +#define Z3_PCLOSE _pclose +#else +#define Z3_POPEN popen +#define Z3_PCLOSE pclose +#endif // // Unit tests fail by asserting. @@ -17,36 +37,175 @@ // and print "PASS" to indicate success. // -#define TST(MODULE) { \ - std::string s("test "); \ - s += #MODULE; \ - void tst_##MODULE(); \ - if (do_display_usage) \ - std::cout << " " << #MODULE << "\n"; \ - for (int i = 0; i < argc; ++i) \ - if (test_all || strcmp(argv[i], #MODULE) == 0) { \ - enable_debug(#MODULE); \ - timeit timeit(true, s.c_str()); \ - tst_##MODULE(); \ - std::cout << "PASS" << std::endl; \ - } \ - } +// ======================================================================== +// Test list definitions using X-macros. +// X(name) is for regular tests, X_ARGV(name) is for tests needing arguments. +// FOR_EACH_ALL_TEST: tests run with /a flag. +// FOR_EACH_EXTRA_TEST: tests only run when explicitly named. +// ======================================================================== -#define TST_ARGV(MODULE) { \ - std::string s("test "); \ - s += #MODULE; \ - void tst_##MODULE(char** argv, int argc, int& i); \ - if (do_display_usage) \ - std::cout << " " << #MODULE << "(...)\n"; \ - for (int i = 0; i < argc; ++i) \ - if (strcmp(argv[i], #MODULE) == 0) { \ - enable_trace(#MODULE); \ - enable_debug(#MODULE); \ - timeit timeit(true, s.c_str()); \ - tst_##MODULE(argv, argc, i); \ - std::cout << "PASS" << std::endl; \ - } \ -} +#define FOR_EACH_ALL_TEST(X, X_ARGV) \ + X(random) \ + X(symbol_table) \ + X(region) \ + X(symbol) \ + X(heap) \ + X(hashtable) \ + X(rational) \ + X(inf_rational) \ + X(ast) \ + X(optional) \ + X(bit_vector) \ + X(fixed_bit_vector) \ + X(tbv) \ + X(doc) \ + X(udoc_relation) \ + X(string_buffer) \ + X(map) \ + X(diff_logic) \ + X(uint_set) \ + X_ARGV(expr_rand) \ + X(list) \ + X(small_object_allocator) \ + X(timeout) \ + X(proof_checker) \ + X(simplifier) \ + X(bit_blaster) \ + X(var_subst) \ + X(simple_parser) \ + X(api) \ + X(max_reg) \ + X(max_rev) \ + X(scaled_min) \ + X(box_mod_opt) \ + X(deep_api_bugs) \ + X(api_algebraic) \ + X(api_polynomial) \ + X(api_pb) \ + X(api_datalog) \ + X(parametric_datatype) \ + X(cube_clause) \ + X(old_interval) \ + X(get_implied_equalities) \ + X(arith_simplifier_plugin) \ + X(matcher) \ + X(object_allocator) \ + X(mpz) \ + X(mpq) \ + X(mpf) \ + X(total_order) \ + X(dl_table) \ + X(dl_context) \ + X(dlist) \ + X(dl_util) \ + X(dl_product_relation) \ + X(dl_relation) \ + X(parray) \ + X(stack) \ + X(escaped) \ + X(buffer) \ + X(chashtable) \ + X(egraph) \ + X(ex) \ + X(nlarith_util) \ + X(api_ast_map) \ + X(api_bug) \ + X(api_special_relations) \ + X(arith_rewriter) \ + X(check_assumptions) \ + X(smt_context) \ + X(theory_dl) \ + X(model_retrieval) \ + X(model_based_opt) \ + X(factor_rewriter) \ + X(smt2print_parse) \ + X(substitution) \ + X(polynomial) \ + X(polynomial_factorization) \ + X(upolynomial) \ + X(algebraic) \ + X(algebraic_numbers) \ + X(ackermannize) \ + X(monomial_bounds) \ + X(nla_intervals) \ + X(horner) \ + X(prime_generator) \ + X(permutation) \ + X(nlsat) \ + X(13) \ + X(zstring) + +#define FOR_EACH_EXTRA_TEST(X, X_ARGV) \ + X(ext_numeral) \ + X(interval) \ + X(value_generator) \ + X(value_sweep) \ + X(vector) \ + X(f2n) \ + X(hwf) \ + X(trigo) \ + X(bits) \ + X(mpbq) \ + X(mpfx) \ + X(mpff) \ + X(horn_subsume_model_converter) \ + X(model2expr) \ + X(hilbert_basis) \ + X(heap_trie) \ + X(karr) \ + X(no_overflow) \ + X(datalog_parser) \ + X_ARGV(datalog_parser_file) \ + X(dl_query) \ + X(quant_solve) \ + X(rcf) \ + X(polynorm) \ + X(qe_arith) \ + X(expr_substitution) \ + X(sorting_network) \ + X(theory_pb) \ + X(simplex) \ + X(sat_user_scope) \ + X_ARGV(ddnf) \ + X(ddnf1) \ + X(model_evaluator) \ + X(get_consequences) \ + X(pb2bv) \ + X_ARGV(sat_lookahead) \ + X_ARGV(sat_local_search) \ + X_ARGV(cnf_backbones) \ + X(bdd) \ + X(pdd) \ + X(pdd_solver) \ + X(scoped_timer) \ + X(solver_pool) \ + X(finder) \ + X(totalizer) \ + X(distribution) \ + X(euf_bv_plugin) \ + X(euf_arith_plugin) \ + X(sls_test) \ + X(scoped_vector) \ + X(sls_seq_plugin) \ + X(ho_matcher) \ + X(finite_set) \ + X(finite_set_rewriter) \ + X(fpa) + +#define FOR_EACH_TEST(X, X_ARGV) \ + FOR_EACH_ALL_TEST(X, X_ARGV) \ + FOR_EACH_EXTRA_TEST(X, X_ARGV) + +// Forward declarations for all test functions +#define DECL_TST(M) void tst_##M(); +#define DECL_TST_ARGV(M) void tst_##M(char** argv, int argc, int& i); +FOR_EACH_TEST(DECL_TST, DECL_TST_ARGV) +#undef DECL_TST +#undef DECL_TST_ARGV + +// ======================================================================== +// Helper functions +// ======================================================================== void error(const char * msg) { std::cerr << "Error: " << msg << "\n"; @@ -62,6 +221,9 @@ void display_usage() { std::cout << " /v:level be verbose, where is the verbosity level.\n"; std::cout << " /w enable warning messages.\n"; std::cout << " /a run all unit tests that don't require arguments.\n"; +#ifndef __EMSCRIPTEN__ + std::cout << " /j[:N] run tests in parallel using N jobs (default: number of cores).\n"; +#endif #if defined(Z3DEBUG) || defined(_TRACE) std::cout << "\nDebugging support:\n"; #endif @@ -74,7 +236,8 @@ void display_usage() { std::cout << "\nModule names:\n"; } -void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all) { +void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all, + unsigned& num_jobs, std::vector& extra_args) { int i = 1; if (argc == 1) { display_usage(); @@ -103,18 +266,36 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t error("option argument (/v:level) is missing."); long lvl = strtol(opt_arg, nullptr, 10); set_verbosity_level(lvl); + extra_args.push_back(std::string("/v:") + opt_arg); } else if (strcmp(opt_name, "w") == 0) { enable_warning_messages(true); + extra_args.push_back("/w"); } else if (strcmp(opt_name, "a") == 0) { test_all = true; } + else if (strcmp(opt_name, "j") == 0) { +#ifndef __EMSCRIPTEN__ + if (opt_arg) { + long n = strtol(opt_arg, nullptr, 10); + if (n <= 0) error("invalid number of jobs for /j option."); + num_jobs = static_cast(n); + } + else { + unsigned hw = std::thread::hardware_concurrency(); + num_jobs = hw > 0 ? hw : 4; + } +#else + error("/j option is not supported on this platform."); +#endif + } #ifdef _TRACE else if (strcmp(opt_name, "tr") == 0) { if (!opt_arg) error("option argument (/tr:tag) is missing."); enable_trace(opt_arg); + extra_args.push_back(std::string("/tr:") + opt_arg); } #endif #ifdef Z3DEBUG @@ -122,6 +303,7 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t if (!opt_arg) error("option argument (/dbg:tag) is missing."); enable_debug(opt_arg); + extra_args.push_back(std::string("/dbg:") + opt_arg); } #endif } @@ -131,6 +313,7 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t char * value = eq_pos+1; try { gparams::set(key, value); + extra_args.push_back(std::string(key) + "=" + value); } catch (z3_exception& ex) { std::cerr << ex.what() << "\n"; @@ -141,156 +324,243 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t } +// ======================================================================== +// Parallel test execution using child processes +// ======================================================================== + +#ifndef __EMSCRIPTEN__ + +struct test_result { + std::string name; + int exit_code; + std::string output; + double elapsed_secs; +}; + +static test_result run_test_child(const char* exe_path, const char* test_name, + const std::vector& extra_args) { + test_result result; + result.name = test_name; + + std::ostringstream cmd; + cmd << "\"" << exe_path << "\"" << " " << test_name; + for (const auto& arg : extra_args) + cmd << " " << arg; + cmd << " 2>&1"; + + auto start = std::chrono::steady_clock::now(); + + FILE* pipe = Z3_POPEN(cmd.str().c_str(), "r"); + if (!pipe) { + result.exit_code = -1; + result.output = "Failed to start child process\n"; + result.elapsed_secs = 0; + return result; + } + + char buf[4096]; + while (fgets(buf, sizeof(buf), pipe)) + result.output += buf; + + int raw = Z3_PCLOSE(pipe); +#ifdef _WINDOWS + result.exit_code = raw; +#else + if (WIFEXITED(raw)) + result.exit_code = WEXITSTATUS(raw); + else if (WIFSIGNALED(raw)) + result.exit_code = 128 + WTERMSIG(raw); + else + result.exit_code = -1; +#endif + + auto end = std::chrono::steady_clock::now(); + result.elapsed_secs = std::chrono::duration(end - start).count(); + return result; +} + +static int run_parallel(const char* exe_path, bool test_all, unsigned num_jobs, + const std::vector& extra_args, + const std::vector& requested_tests) { + std::vector tests_to_run; + + if (test_all) { + #define COLLECT_ALL(M) tests_to_run.push_back(#M); + #define SKIP_ARGV_1(M) + FOR_EACH_ALL_TEST(COLLECT_ALL, SKIP_ARGV_1) + #undef COLLECT_ALL + #undef SKIP_ARGV_1 + } + else { + #define MAYBE_COLLECT(M) \ + for (const auto& req : requested_tests) \ + if (req == #M) { tests_to_run.push_back(#M); break; } + #define SKIP_ARGV_2(M) + FOR_EACH_TEST(MAYBE_COLLECT, SKIP_ARGV_2) + #undef MAYBE_COLLECT + #undef SKIP_ARGV_2 + } + + if (tests_to_run.empty()) { + std::cout << "No tests to run in parallel mode." << std::endl; + return 0; + } + + unsigned total = static_cast(tests_to_run.size()); + if (num_jobs > total) + num_jobs = total; + + std::cout << "Running " << total << " tests with " + << num_jobs << " parallel jobs..." << std::endl; + + auto wall_start = std::chrono::steady_clock::now(); + + std::mutex queue_mtx; + std::mutex output_mtx; + size_t next_idx = 0; + unsigned completed = 0; + unsigned passed = 0; + unsigned failed = 0; + std::vector failed_names; + + auto worker = [&]() { + while (true) { + size_t idx; + { + std::lock_guard lock(queue_mtx); + if (next_idx >= tests_to_run.size()) + return; + idx = next_idx++; + } + + test_result result = run_test_child(exe_path, tests_to_run[idx].c_str(), extra_args); + + { + std::lock_guard lock(output_mtx); + ++completed; + if (result.exit_code == 0) { + ++passed; + std::cout << "[" << completed << "/" << total << "] " + << result.name << " PASS (" + << std::fixed << std::setprecision(1) + << result.elapsed_secs << "s)" << std::endl; + } + else { + ++failed; + failed_names.push_back(result.name); + std::cout << "[" << completed << "/" << total << "] " + << result.name << " FAIL (exit code " + << result.exit_code << ", " + << std::fixed << std::setprecision(1) + << result.elapsed_secs << "s)" << std::endl; + if (!result.output.empty()) { + std::cout << "--- " << result.name << " output ---" << std::endl; + std::cout << result.output; + if (result.output.back() != '\n') + std::cout << std::endl; + std::cout << "--- end " << result.name << " ---" << std::endl; + } + } + } + } + }; + + std::vector threads; + for (unsigned i = 0; i < num_jobs; ++i) + threads.emplace_back(worker); + for (auto& t : threads) + t.join(); + + auto wall_end = std::chrono::steady_clock::now(); + double wall_secs = std::chrono::duration(wall_end - wall_start).count(); + + std::cout << "\n=== Test Summary ===" << std::endl; + std::cout << passed << " passed, " << failed << " failed, " + << total << " total" << std::endl; + std::cout << "Wall time: " << std::fixed << std::setprecision(1) + << wall_secs << "s" << std::endl; + + if (!failed_names.empty()) { + std::cout << "Failed tests:"; + for (const auto& name : failed_names) + std::cout << " " << name; + std::cout << std::endl; + } + + return failed > 0 ? 1 : 0; +} + +#endif // !__EMSCRIPTEN__ + + +// ======================================================================== +// main +// ======================================================================== + int main(int argc, char ** argv) { memory::initialize(0); + + // Collect potential test names before parsing modifies argv + std::vector requested_tests; + for (int i = 1; i < argc; ++i) { + const char* a = argv[i]; + if (a[0] != '-' && a[0] != '/' && !strchr(a, '=')) + requested_tests.push_back(a); + } + bool do_display_usage = false; bool test_all = false; - parse_cmd_line_args(argc, argv, do_display_usage, test_all); - TST(random); - TST(symbol_table); - TST(region); - TST(symbol); - TST(heap); - TST(hashtable); - TST(rational); - TST(inf_rational); - TST(ast); - TST(optional); - TST(bit_vector); - TST(fixed_bit_vector); - TST(tbv); - TST(doc); - TST(udoc_relation); - TST(string_buffer); - TST(map); - TST(diff_logic); - TST(uint_set); - TST_ARGV(expr_rand); - TST(list); - TST(small_object_allocator); - TST(timeout); - TST(proof_checker); - TST(simplifier); - TST(bit_blaster); - TST(var_subst); - TST(simple_parser); - TST(api); - TST(max_reg); - TST(max_rev); - TST(scaled_min); - TST(box_mod_opt); - TST(deep_api_bugs); - TST(api_algebraic); - TST(api_polynomial); - TST(api_pb); - TST(api_datalog); - TST(parametric_datatype); - TST(cube_clause); - TST(old_interval); - TST(get_implied_equalities); - TST(arith_simplifier_plugin); - TST(matcher); - TST(object_allocator); - TST(mpz); - TST(mpq); - TST(mpf); - TST(total_order); - TST(dl_table); - TST(dl_context); - TST(dlist); - TST(dl_util); - TST(dl_product_relation); - TST(dl_relation); - TST(parray); - TST(stack); - TST(escaped); - TST(buffer); - TST(chashtable); - TST(egraph); - TST(ex); - TST(nlarith_util); - TST(api_ast_map); - TST(api_bug); - TST(api_special_relations); - TST(arith_rewriter); - TST(check_assumptions); - TST(smt_context); - TST(theory_dl); - TST(model_retrieval); - TST(model_based_opt); - TST(factor_rewriter); - TST(smt2print_parse); - TST(substitution); - TST(polynomial); - TST(polynomial_factorization); - TST(upolynomial); - TST(algebraic); - TST(algebraic_numbers); - TST(ackermannize); - TST(monomial_bounds); - TST(nla_intervals); - TST(horner); - TST(prime_generator); - TST(permutation); - TST(nlsat); - TST(13); - TST(zstring); + unsigned num_jobs = 0; + std::vector extra_args; + parse_cmd_line_args(argc, argv, do_display_usage, test_all, num_jobs, extra_args); + + if (do_display_usage) { + #define DISPLAY_TST(M) std::cout << " " << #M << "\n"; + #define DISPLAY_TST_ARGV(M) std::cout << " " << #M << "(...)\n"; + FOR_EACH_TEST(DISPLAY_TST, DISPLAY_TST_ARGV) + #undef DISPLAY_TST + #undef DISPLAY_TST_ARGV + return 0; + } + +#ifndef __EMSCRIPTEN__ + if (num_jobs > 0) + return run_parallel(argv[0], test_all, num_jobs, extra_args, requested_tests); +#endif + + // Serial execution, original behavior + #define RUN_TST(M) { \ + bool run = test_all; \ + for (int i = 0; !run && i < argc; ++i) \ + run = strcmp(argv[i], #M) == 0; \ + if (run) { \ + std::string s("test "); \ + s += #M; \ + enable_debug(#M); \ + timeit timeit(true, s.c_str()); \ + tst_##M(); \ + std::cout << "PASS" << std::endl; \ + } \ + } + + #define RUN_TST_ARGV(M) { \ + for (int i = 0; i < argc; ++i) \ + if (strcmp(argv[i], #M) == 0) { \ + enable_trace(#M); \ + enable_debug(#M); \ + std::string s("test "); \ + s += #M; \ + timeit timeit(true, s.c_str()); \ + tst_##M(argv, argc, i); \ + std::cout << "PASS" << std::endl; \ + } \ + } + + FOR_EACH_ALL_TEST(RUN_TST, RUN_TST_ARGV) if (test_all) return 0; - TST(ext_numeral); - TST(interval); - TST(value_generator); - TST(value_sweep); - TST(vector); - TST(f2n); - TST(hwf); - TST(trigo); - TST(bits); - TST(mpbq); - TST(mpfx); - TST(mpff); - TST(horn_subsume_model_converter); - TST(model2expr); - TST(hilbert_basis); - TST(heap_trie); - TST(karr); - TST(no_overflow); - // TST(memory); - TST(datalog_parser); - TST_ARGV(datalog_parser_file); - TST(dl_query); - TST(quant_solve); - TST(rcf); - TST(polynorm); - TST(qe_arith); - TST(expr_substitution); - TST(sorting_network); - TST(theory_pb); - TST(simplex); - TST(sat_user_scope); - TST_ARGV(ddnf); - TST(ddnf1); - TST(model_evaluator); - TST(get_consequences); - TST(pb2bv); - TST_ARGV(sat_lookahead); - TST_ARGV(sat_local_search); - TST_ARGV(cnf_backbones); - TST(bdd); - TST(pdd); - TST(pdd_solver); - TST(scoped_timer); - TST(solver_pool); - //TST_ARGV(hs); - TST(finder); - TST(totalizer); - TST(distribution); - TST(euf_bv_plugin); - TST(euf_arith_plugin); - TST(sls_test); - TST(scoped_vector); - TST(sls_seq_plugin); - TST(ho_matcher); - TST(finite_set); - TST(finite_set_rewriter); - TST(fpa); + FOR_EACH_EXTRA_TEST(RUN_TST, RUN_TST_ARGV) + + #undef RUN_TST + #undef RUN_TST_ARGV + return 0; }