mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 11:55:49 +00:00
Code Activity

Add parallel test execution to test-z3 (/j flag)

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-03-18 14:57:16 -10:00 • committed by Lev Nachmanson
parent b5bf4be87e
commit 9fea91d0eb
1 changed files with 451 additions and 181 deletions
Download patch file Download diff file Expand all files Collapse all files

632
src/test/main.cpp
View file

@ -1,7 +1,10 @@
#include<iostream>
#include<time.h>
#include<string>
#include<cstring>
#include <iostream>
#include <iomanip>
#include <string>
#include <cstring>
#include <cstdio>
#include <vector>
#include <sstream>
#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 <thread>
#include <mutex>
#include <chrono>
#endif
#if !defined(__EMSCRIPTEN__) && !defined(_WINDOWS)
#include <sys/wait.h>
#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 <level> 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<std::string>& 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<unsigned>(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<std::string>& 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<double>(end - start).count();
return result;
}
static int run_parallel(const char* exe_path, bool test_all, unsigned num_jobs,
const std::vector<std::string>& extra_args,
const std::vector<std::string>& requested_tests) {
std::vector<std::string> 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<unsigned>(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<std::string> failed_names;
auto worker = [&]() {
while (true) {
size_t idx;
{
std::lock_guard<std::mutex> 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<std::mutex> 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<std::thread> 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<double>(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<std::string> 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<std::string> 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;
}