From d47605f99821a260edf248b94d2f76c4189d928d Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Thu, 21 Sep 2023 12:54:47 -0700 Subject: [PATCH 01/15] Correct debug code. --- src/mt/yices_locks_posix.c | 46 ++++++++++++++++++++++---------------- 1 file changed, 27 insertions(+), 19 deletions(-) diff --git a/src/mt/yices_locks_posix.c b/src/mt/yices_locks_posix.c index cf63e99d4..827e7f584 100644 --- a/src/mt/yices_locks_posix.c +++ b/src/mt/yices_locks_posix.c @@ -20,30 +20,38 @@ #include #include #include +#include #include "yices_locks.h" -//I see NDEBUG and DEBUG in the code; which is it? -#ifdef DEBUG -static pthread_mutexattr_t mta; -static pthread_mutexattr_t* mattr = &mta; -#else -static pthread_mutexattr_t* mattr = NULL; -#endif +static void print_error(const char *caller, const char *syscall, int errnum) { + char buffer[64]; + strerror_r(errnum, buffer, sizeof(buffer)); + fprintf(stderr, "%s failed: %s returned %d: %s\n", caller, syscall, + errnum, buffer); +} int32_t create_yices_lock(yices_lock_t* lock){ int32_t retcode; -#ifdef DEBUG - retcode = pthread_mutexattr_settype(&mta, PTHREAD_MUTEX_ERRORCHECK); - if(retcode){ - fprintf(stderr, "create_yices_lock failed: pthread_mutexattr_settype returned %d\n", retcode); - } +#ifndef NDEBUG + pthread_mutexattr_t mta; + pthread_mutexattr_t *mattr = &mta; +#else + pthread_mutexattr_t *mattr = NULL; +#endif + +#ifndef NDEBUG + retcode = pthread_mutexattr_init(mattr); + if(retcode) + print_error("create_yices_lock", "pthread_mutexattr_init", retcode); + retcode = pthread_mutexattr_settype(mattr, PTHREAD_MUTEX_ERRORCHECK); + if(retcode) + print_error("create_yices_lock", "pthread_mutextattr_settype", retcode); #endif retcode = pthread_mutex_init(lock, mattr); - if(retcode){ - fprintf(stderr, "create_yices_lock failed: pthread_mutex_init returned %d\n", retcode); - } + if(retcode) + print_error("create_yices_lock", "pthread_mutex_init", retcode); assert(retcode == 0); return retcode; } @@ -54,7 +62,7 @@ int32_t try_yices_lock(yices_lock_t* lock){ if(retcode == EBUSY){ return 1; } else { - fprintf(stderr, "try_yices_lock failed: pthread_mutex_trylock returned %d\n", retcode); + print_error("try_yices_lock", "pthread_mutex_trylock", retcode); } return -1; } @@ -65,7 +73,7 @@ int32_t try_yices_lock(yices_lock_t* lock){ int32_t get_yices_lock(yices_lock_t* lock){ int32_t retcode = pthread_mutex_lock(lock); if(retcode){ - fprintf(stderr, "get_yices_lock failed: pthread_mutex_lock returned %d\n", retcode); + print_error("get_yices_lock", "pthread_mutex_lock", retcode); } assert(retcode == 0); return retcode; @@ -74,7 +82,7 @@ int32_t get_yices_lock(yices_lock_t* lock){ int32_t release_yices_lock(yices_lock_t* lock){ int32_t retcode = pthread_mutex_unlock(lock); if(retcode){ - fprintf(stderr, "release_yices_lock failed: pthread_mutex_unlock returned %d\n", retcode); + print_error("release_yices_lock", "pthread_mutex_unlock", retcode); } assert(retcode == 0); return retcode; @@ -83,7 +91,7 @@ int32_t release_yices_lock(yices_lock_t* lock){ void destroy_yices_lock(yices_lock_t* lock){ int32_t retcode = pthread_mutex_destroy(lock); if(retcode){ - fprintf(stderr, "destroy_yices_lock failed: pthread_mutex_destroy returned %d\n", retcode); + print_error("destroy_yices_lock", "pthread_mutex_destroy", retcode); } assert(retcode == 0); } From 74f5f3b0689976535883061e9ab3ea9dca28844d Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Thu, 21 Sep 2023 18:03:30 -0700 Subject: [PATCH 02/15] Avoid deadlocks in MC-SAT. --- configure.ac | 4 ---- src/api/yices_api.c | 25 ++++++++++++------------- src/api/yices_api_lock_free.h | 9 ++++++++- src/context/context.c | 6 +++++- src/mcsat/bv/bv_explainer.c | 5 +++-- src/mcsat/bv/bv_utils.h | 7 ++++--- src/mcsat/bv/explain/eq_ext_con.c | 3 ++- src/mcsat/bv/explain/full_bv_sat.c | 8 ++++---- src/mcsat/conflict.c | 7 ++++--- src/mcsat/preprocessor.c | 9 +++++---- 10 files changed, 47 insertions(+), 36 deletions(-) diff --git a/configure.ac b/configure.ac index b66ebacd7..15b4a97b6 100644 --- a/configure.ac +++ b/configure.ac @@ -870,10 +870,6 @@ fi AC_SUBST(THREAD_SAFE) if test "x$thread_safe" = xyes ; then THREAD_SAFE=1 - # iam: the aim is to eventually eliminate this restriction, but not before the 2.6.2 release. - if test $use_mcsat = yes ; then - AC_MSG_ERROR([Building with both --enable-mcsat and --enable-thread-safety is currently not supported.]) - fi fi dnl diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 6442da188..47f1dd452 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -8669,10 +8669,10 @@ static inline bool yices_assert_formula_checks(term_t t) { MT_PROTECT(bool, __yices_globals.lock, _o_yices_assert_formula_checks(t)); } -EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) { +int32_t _o_yices_assert_formula(context_t *ctx, term_t t) { int32_t code; - if (! yices_assert_formula_checks(t)) { + if (! _o_yices_assert_formula_checks(t)) { return -1; } @@ -8711,7 +8711,7 @@ EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) { assert(context_status(ctx) == STATUS_IDLE); - code = assert_formula(ctx, t); + code = _o_assert_formula(ctx, t); if (code < 0) { // error during internalization convert_internalization_error(code); @@ -8722,6 +8722,10 @@ EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) { return 0; } +EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) { + MT_PROTECT(int32_t, __yices_globals.lock, + _o_yices_assert_formula(ctx, t)); +} @@ -9054,23 +9058,19 @@ static bool _o_unsat_core_check_assumptions(uint32_t n, const term_t a[]) { return check_good_terms(__yices_globals.manager, n, a) && check_boolean_args(__yices_globals.manager, n, a); } -static bool unsat_core_check_assumptions(uint32_t n, const term_t a[]) { - MT_PROTECT(bool, __yices_globals.lock, _o_unsat_core_check_assumptions(n, a)); -} - /* * Check context with assumptions * - n = number of assumptions * - a[0] ... a[n-1] = n assumptions. All of them must be Boolean terms. */ -EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t a[]) { +smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t a[]) { param_t default_params; ivector_t assumptions; smt_status_t stat; uint32_t i; literal_t l; - if (!unsat_core_check_assumptions(n, a)) { + if (!_o_unsat_core_check_assumptions(n, a)) { return STATUS_ERROR; // Bad assumptions } @@ -9113,8 +9113,6 @@ EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const assert(context_status(ctx) == STATUS_IDLE); - yices_obtain_mutex(); - // convert the assumptions to n literals init_ivector(&assumptions, n); for (i=0; i void bv_subexplainer_construct(bv_subexplainer_t* exp, const char* name, plugin_context_t* ctx, watch_list_manager_t* wlm, bv_evaluator_t* eval) { @@ -169,10 +170,10 @@ void bv_explainer_normalize_conflict(bv_explainer_t* exp, ivector_t* conflict_ou } void bv_explainer_check_conflict(bv_explainer_t* exp, const ivector_t* conflict) { - context_t* ctx = yices_new_context(NULL); + context_t* ctx = _o_yices_new_context(NULL); uint32_t i; for (i = 0; i < conflict->size; ++ i) { - yices_assert_formula(ctx, conflict->data[i]); + _o_yices_assert_formula(ctx, conflict->data[i]); } smt_status_t result = yices_check_context(ctx, NULL); (void) result; diff --git a/src/mcsat/bv/bv_utils.h b/src/mcsat/bv/bv_utils.h index 121fb4912..39aae56e2 100644 --- a/src/mcsat/bv/bv_utils.h +++ b/src/mcsat/bv/bv_utils.h @@ -35,6 +35,7 @@ #include "mcsat/tracing.h" #include "mcsat/value.h" #include "yices.h" +#include "api/yices_api_lock_free.h" /** Types of bitvector terms */ typedef enum { @@ -467,8 +468,8 @@ static inline bool check_rewrite(plugin_context_t* ctx, term_t old, term_t t){ if (t == old) return true; term_manager_t* tm = ctx->tm; - context_t* yctx = yices_new_context(NULL); - yices_assert_formula(yctx, mk_neq(tm, old, t)); + context_t* yctx = _o_yices_new_context(NULL); + _o_yices_assert_formula(yctx, mk_neq(tm, old, t)); smt_status_t output = yices_check_context(yctx, NULL); bool result = (output == STATUS_UNSAT); if (!result && ctx_trace_enabled(ctx, "mcsat::bv::arith::ctz")) { @@ -479,7 +480,7 @@ bool check_rewrite(plugin_context_t* ctx, term_t old, term_t t){ ctx_trace_term(ctx, t); assert(false); } - yices_free_context(yctx); + _o_yices_free_context(yctx); return result; } diff --git a/src/mcsat/bv/explain/eq_ext_con.c b/src/mcsat/bv/explain/eq_ext_con.c index f61b1a486..d49821673 100644 --- a/src/mcsat/bv/explain/eq_ext_con.c +++ b/src/mcsat/bv/explain/eq_ext_con.c @@ -33,6 +33,7 @@ #include "mcsat/eq/equality_graph.h" #include "yices.h" +#include "api/yices_api_lock_free.h" #include "eq_ext_con.h" @@ -1543,7 +1544,7 @@ term_t explain_propagation(bv_subexplainer_t* this, const ivector_t* reasons_in, if (ok) { // Concat the terms if (to_concat.size > 1) { - result_subst = yices_bvconcat(to_concat.size, to_concat.data); + result_subst = _o_yices_bvconcat(to_concat.size, to_concat.data); } else { result_subst = to_concat.data[0]; } diff --git a/src/mcsat/bv/explain/full_bv_sat.c b/src/mcsat/bv/explain/full_bv_sat.c index 3dccadfee..7d255fb29 100644 --- a/src/mcsat/bv/explain/full_bv_sat.c +++ b/src/mcsat/bv/explain/full_bv_sat.c @@ -142,8 +142,8 @@ void bb_sat_solver_add_variable(bb_sat_solver_t* solver, variable_t var, bool wi term_t var_fresh; term_kind_t kind = term_kind(solver->yices_ctx->terms, var_term); if (kind != UNINTERPRETED_TERM) { - type_t var_type = yices_type_of_term(var_term); - var_fresh = yices_new_uninterpreted_term(var_type); + type_t var_type = _o_yices_type_of_term(var_term); + var_fresh = _o_yices_new_uninterpreted_term(var_type); } else { var_fresh = var_term; } @@ -163,7 +163,7 @@ void bb_sat_solver_assert_term(bb_sat_solver_t* solver, variable_t assertion_ter fprintf(out, " previously \n"); ctx_trace_term(solver->ctx, assertion_term); } - yices_assert_formula(solver->yices_ctx, assertion_term); + _o_yices_assert_formula(solver->yices_ctx, assertion_term); } /** @@ -276,7 +276,7 @@ void bb_sat_solver_solve_and_get_core(bb_sat_solver_t* solver, term_vector_t* co } // Check the assumptions (should be unsat) - smt_status_t status = yices_check_context_with_assumptions(solver->yices_ctx, NULL, assumptions.size, assumptions.data); + smt_status_t status = _o_yices_check_context_with_assumptions(solver->yices_ctx, NULL, assumptions.size, assumptions.data); (void) status; assert(status == STATUS_UNSAT); diff --git a/src/mcsat/conflict.c b/src/mcsat/conflict.c index 648f169a6..d097a97d4 100644 --- a/src/mcsat/conflict.c +++ b/src/mcsat/conflict.c @@ -29,19 +29,20 @@ #include "mcsat/tracing.h" #include "yices.h" +#include "api/yices_api_lock_free.h" #include #define CONFLICT_DEFAULT_ELEMENT_SIZE 100 void conflict_check(conflict_t* conflict) { ctx_config_t* config = yices_new_config(); - context_t* ctx = yices_new_context(config); + context_t* ctx = _o_yices_new_context(config); uint32_t i; const ivector_t* literals = &conflict->disjuncts.element_list; for (i = 0; i < literals->size; ++i) { term_t literal = literals->data[i]; literal = opposite_term(literal); - int32_t ret = yices_assert_formula(ctx, literal); + int32_t ret = _o_yices_assert_formula(ctx, literal); if (ret != 0) { // unsupported by regular yices fprintf(stderr, "skipping conflict (ret)\n"); @@ -52,7 +53,7 @@ void conflict_check(conflict_t* conflict) { smt_status_t result = yices_check_context(ctx, NULL); (void) result; assert(result == STATUS_UNSAT); - yices_free_context(ctx); + _o_yices_free_context(ctx); yices_free_config(config); } diff --git a/src/mcsat/preprocessor.c b/src/mcsat/preprocessor.c index 3ccebcc4a..07171b1fe 100644 --- a/src/mcsat/preprocessor.c +++ b/src/mcsat/preprocessor.c @@ -34,6 +34,7 @@ #include "context/context_types.h" #include "yices.h" +#include "api/yices_api_lock_free.h" void preprocessor_construct(preprocessor_t* pre, term_table_t* terms, jmp_buf* handler, const mcsat_options_t* options) { pre->terms = terms; @@ -459,8 +460,8 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is size = 0; } } - current_pre = yices_bvconcat(n_vars, vars); - term_t eq = yices_eq(current, current_pre); + current_pre = _o_yices_bvconcat(n_vars, vars); + term_t eq = _o_yices_eq(current, current_pre); preprocessor_mark_eq(pre, eq, current); } } @@ -598,7 +599,7 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is } else { type_t arg_pre_type = term_type(pre->terms, arg_pre); term_t arg_pre_is_positive = mk_arith_term_geq0(&pre->tm, arg_pre); - term_t arg_negative = yices_neg(arg_pre); + term_t arg_negative = _o_yices_neg(arg_pre); current_pre = mk_ite(&pre->tm, arg_pre_is_positive, arg_pre, arg_negative, arg_pre_type); } break; @@ -718,7 +719,7 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is trace_term_ln(pre->tracer, terms, arg_pre); } // For simplification purposes use API - current_pre = yices_bitextract(arg_pre, index); + current_pre = _o_yices_bitextract(arg_pre, index); assert(current_pre != NULL_TERM); } } From 3f1aef403b510a8c7920e6e5aa636b7f4efe88a0 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Fri, 22 Sep 2023 07:50:01 -0700 Subject: [PATCH 03/15] Destroy in reverse order of creation. --- src/api/yices_api.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 47f1dd452..faed13510 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -1108,6 +1108,11 @@ EXPORTED void yices_exit(void) { delete_sparse_array(&the_root_types); } + free_parameter_list(); + free_config_list(); + free_model_list(); + free_context_list(); + delete_parsing_objects(); delete_fvars(); @@ -1123,11 +1128,6 @@ EXPORTED void yices_exit(void) { free_bvarith64_buffer_list(); free_arith_buffer_list(); - free_context_list(); - free_model_list(); - free_config_list(); - free_parameter_list(); - delete_list_locks(); q_clear(&r0); From 1bd4ca851f9bea7c7295913fb390cd63c3754151 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Fri, 22 Sep 2023 07:52:03 -0700 Subject: [PATCH 04/15] Allocate large arrays on the heap. --- src/mcsat/bv/explain/arith_norm.c | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/mcsat/bv/explain/arith_norm.c b/src/mcsat/bv/explain/arith_norm.c index 65b8a4a0e..d78d31f10 100644 --- a/src/mcsat/bv/explain/arith_norm.c +++ b/src/mcsat/bv/explain/arith_norm.c @@ -777,7 +777,9 @@ term_t arith_normalise_upto(arith_norm_t* norm, term_t u, uint32_t w){ case BV_ARRAY: { // Concatenated boolean terms composite_term_t* concat_desc = bvarray_term_desc(terms, t); - term_t ebits[w]; // Where we build the result + term_t *ebits; // Where we build the result + + ebits = (term_t *) safe_malloc(w * sizeof(term_t)); // First, we eliminate BIT_TERM-over-BV_ARRAYs: for (uint32_t i = 0; i < w; i++) @@ -791,7 +793,11 @@ term_t arith_normalise_upto(arith_norm_t* norm, term_t u, uint32_t w){ // preproc[1][i] is the term_t arith_normalise_upto(k,top+1) (normalised version of k over the lowest top+1 bits), let's call it norm // preproc[2][i] is the value returned by bv_evaluator_not_free_up_to(norm), let's call it maxeval // preproc[3][i] is the term_t arith_normalise_upto(norm,maxeval), if maxeval is not 0 - term_t preproc[4][w]; + + term_t *preproc[4]; + for (int i = 0; i < 4; i ++) + preproc[i] = (term_t *) safe_malloc(4 * w * sizeof(term_t)); + // We initialise the hashmap fix_htbl_init(preproc[0], w); @@ -865,6 +871,11 @@ term_t arith_normalise_upto(arith_norm_t* norm, term_t u, uint32_t w){ arith_analyse_t analysis; init_analysis(&analysis); analyse_bvarray(norm, w, ebits, &analysis); + + for (int i = 0; i < 4; i ++) + safe_free(preproc[i]); + safe_free(ebits); + return finalise(norm, t, &analysis); } From 43f1ec065df95f566e6b8a15cd8fd1c35a94db30 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Fri, 22 Sep 2023 07:53:26 -0700 Subject: [PATCH 05/15] Use lock-free API. --- src/mcsat/bv/bv_explainer.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mcsat/bv/bv_explainer.c b/src/mcsat/bv/bv_explainer.c index 6de49c802..9521bb600 100644 --- a/src/mcsat/bv/bv_explainer.c +++ b/src/mcsat/bv/bv_explainer.c @@ -178,7 +178,7 @@ void bv_explainer_check_conflict(bv_explainer_t* exp, const ivector_t* conflict) smt_status_t result = yices_check_context(ctx, NULL); (void) result; assert(result == STATUS_UNSAT); - yices_free_context(ctx); + _o_yices_free_context(ctx); } void print_counters(bv_explainer_t* exp){ From 385d61f7f736f7c854a47adddbe6c032a162d652 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Fri, 22 Sep 2023 13:23:04 -0700 Subject: [PATCH 06/15] Add option to run individual tests. Add option to pass options to SMT2 solver. Detect bad exit codes. --- tests/regress/check.sh | 45 ++++++++++++++++++++++++++++++++---------- 1 file changed, 35 insertions(+), 10 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 9cdc5013c..e2870e180 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -34,13 +34,33 @@ # what's expected. # -if test $# != 2 ; then - echo "Usage: $0 " +usage() { + echo "Usage: $0 [test1] [test2] ..." exit +} + +smt2_options= + +while getopts "s:" o; do + case "$o" in + s) + smt2_options=${OPTARG} + ;; + *) + usage + ;; + esac +done +shift $((OPTIND-1)) + +if test $# "<" 2 ; then + usage fi regress_dir=$1 bin_dir=$2 +shift 2 +all_tests="$@" # Make sure fatal errors go to stderr export LIBC_FATAL_STDERR_=1 @@ -112,11 +132,13 @@ else MCSAT_FILTER="." fi -all_tests=$( - find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' | - grep $REGRESS_FILTER | grep $MCSAT_FILTER | - sort -) +if test -z "$all_tests"; then + all_tests=$( + find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' | + grep $REGRESS_FILTER | grep $MCSAT_FILTER | + sort + ) +fi for file in $all_tests; do @@ -125,9 +147,12 @@ for file in $all_tests; do # Get the binary based on the filename filename=`basename "$file"` + options= + case $filename in *.smt2) binary=yices_smt2 + options=$smt2_options ;; *.smt) binary=yices_smtcomp @@ -144,11 +169,10 @@ for file in $all_tests; do # Get the options if [ -e "$file.options" ] then - options=`cat $file.options` + options="$options `cat $file.options`" echo " [ $options ]" test_string="$file [ $options ]" else - options= test_string="$file" echo fi @@ -172,12 +196,13 @@ for file in $all_tests; do ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null (time ./$bin_dir/$binary $options ./$file >& $outfile ) >& $timefile ) + status=$? thetime=`cat $timefile` # Do the diff DIFF=`diff -w $outfile $gold` - if [ $? -eq 0 ] + if [ $? -eq 0 ] && [ $status -eq 0 ] then echo -n $green echo PASS [${thetime} s] From c1cd4d37db3023ee146b61aeb500ef4aa0647593 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Fri, 22 Sep 2023 13:26:50 -0700 Subject: [PATCH 07/15] Add fatal error utilities. Remove yices_smt2_mt frontend, merging capability into yices_smt2. Ensure threads have large stacks. Make timeouts thread-safe. --- src/Makefile | 2 +- src/frontend/smt2/smt2_commands.c | 84 ++-- src/frontend/smt2/smt2_commands.h | 3 +- src/frontend/yices/yices_reval.c | 23 +- src/frontend/yices_smt.c | 9 +- src/frontend/yices_smt2.c | 22 +- src/frontend/yices_smt2_mt.c | 638 ------------------------------ src/frontend/yices_smtcomp.c | 10 +- src/mt/threads_posix.c | 45 ++- src/utils/error.c | 36 ++ src/utils/error.h | 29 ++ src/utils/timeout.c | 195 ++++++++- src/utils/timeout.h | 34 +- tests/unit/test_timeout.c | 15 +- 14 files changed, 377 insertions(+), 768 deletions(-) delete mode 100644 src/frontend/yices_smt2_mt.c create mode 100644 src/utils/error.c create mode 100644 src/utils/error.h diff --git a/src/Makefile b/src/Makefile index 445c6ff7b..9a14fc6ba 100644 --- a/src/Makefile +++ b/src/Makefile @@ -276,6 +276,7 @@ core_src_c := \ utils/csets.c \ utils/cputime.c \ utils/dep_tables.c \ + utils/error.c \ utils/gcd.c \ utils/generic_heap.c \ utils/hash_functions.c \ @@ -494,7 +495,6 @@ bin_src_c := \ frontend/yices_sat_new.c \ frontend/yices_smt.c \ frontend/yices_smt2.c \ - frontend/yices_smt2_mt.c \ frontend/yices_smtcomp.c \ # diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index 4d27ed7ba..af6483f4f 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -2653,8 +2653,13 @@ static void init_search_parameters(smt2_globals_t *g) { static void timeout_handler(void *data) { smt2_globals_t *g; +#ifndef THREAD_SAFE assert(data == &__smt2_globals); - +#else + /* In the multi-threaded case there are multiple copies of the + global data. */ +#endif /* THREAD_SAFE */ + g = data; if (g->efmode && g->ef_client.efsolver != NULL && g->ef_client.efsolver->status == EF_STATUS_SEARCHING) { ef_solver_stop_search(g->ef_client.efsolver); @@ -2679,14 +2684,13 @@ static smt_status_t check_sat_with_timeout(smt2_globals_t *g, const param_t *par * We call init_timeout only now because the internal timeout * consumes resources even if it's never used. */ - if (! g->timeout_initialized) { - init_timeout(); - g->timeout_initialized = true; + if (! g->to) { + g->to = init_timeout(); } g->interrupted = false; - start_timeout(g->timeout, timeout_handler, g); + start_timeout(g->to, g->timeout, timeout_handler, g); stat = check_context(g->ctx, params); - clear_timeout(); + clear_timeout(g->to); /* * Attempt to cleanly recover from interrupt @@ -2725,15 +2729,14 @@ static smt_status_t check_sat_with_assumptions(smt2_globals_t *g, const param_t * We call init_timeout only now because the internal timeout * consumes resources even if it's never used. */ - if (! g->timeout_initialized) { - init_timeout(); - g->timeout_initialized = true; + if (! g->to) { + g->to = init_timeout(); } g->interrupted = false; - start_timeout(g->timeout, timeout_handler, g); + start_timeout(g->to, g->timeout, timeout_handler, g); stat = check_with_assumptions(g->ctx, params, a->assumptions.size, a->assumptions.data, &a->core); a->status = stat; - clear_timeout(); + clear_timeout(g->to); /* * Attempt to cleanly recover from interrupt @@ -2773,14 +2776,13 @@ static smt_status_t check_sat_with_model(smt2_globals_t *g, const param_t *param * We call init_timeout only now because the internal timeout * consumes resources even if it's never used. */ - if (! g->timeout_initialized) { - init_timeout(); - g->timeout_initialized = true; + if (! g->to) { + g->to = init_timeout(); } g->interrupted = false; - start_timeout(g->timeout, timeout_handler, g); + start_timeout(g->to, g->timeout, timeout_handler, g); stat = check_with_model(g->ctx, params, n, vars, values); - clear_timeout(); + clear_timeout(g->to); /* * Attempt to cleanly recover from interrupt @@ -3026,7 +3028,7 @@ static void add_delayed_assertion(smt2_globals_t *g, term_t t) { /* * Check satisfiability of all assertions */ -static void check_delayed_assertions(smt2_globals_t *g) { +static void check_delayed_assertions(smt2_globals_t *g, bool report) { int32_t code; smt_status_t status; model_t *model; @@ -3036,12 +3038,14 @@ static void check_delayed_assertions(smt2_globals_t *g) { if (g->trivially_unsat) { trace_printf(g->tracer, 3, "(check-sat: trivially unsat)\n"); - report_status(g, STATUS_UNSAT); + if (report) + report_status(g, STATUS_UNSAT); } else if (trivially_true_assertions(g->assertions.data, g->assertions.size, &model)) { trace_printf(g->tracer, 3, "(check-sat: trivially true)\n"); g->trivially_sat = true; g->model = model; - report_status(g, STATUS_SAT); + if (report) + report_status(g, STATUS_SAT); } else { /* * check for mislabeled benchmarks: some benchmarks @@ -3105,7 +3109,8 @@ static void check_delayed_assertions(smt2_globals_t *g) { status = check_sat_with_timeout(g, &g->parameters); } - report_status(g, status); + if (report) + report_status(g, status); } } } @@ -3312,18 +3317,17 @@ static void efsolve_cmd(smt2_globals_t *g) { if (g->efmode) { efc = &g->ef_client; if (g->timeout != 0) { - if (! g->timeout_initialized) { - init_timeout(); - g->timeout_initialized = true; + if (! g->to) { + g->to = init_timeout(); } g->interrupted = false; - start_timeout(g->timeout, timeout_handler, g); + start_timeout(g->to, g->timeout, timeout_handler, g); } ef_solve(efc, g->assertions.size, g->assertions.data, &g->parameters, qf_fragment(g->logic_code), ef_arch_for_logic(g->logic_code), g->tracer, &g->term_patterns); - if (g-> timeout != 0) clear_timeout(); + if (g-> timeout != 0) clear_timeout(g->to); if (efc->efcode != EF_NO_ERROR) { // error in preprocessing @@ -4577,7 +4581,7 @@ static void init_smt2_globals(smt2_globals_t *g) { init_params_to_defaults(&g->parameters); g->nthreads = 0; g->timeout = 0; - g->timeout_initialized = false; + g->to = NULL; g->interrupted = false; g->delegate = NULL; g->avtbl = NULL; @@ -4629,8 +4633,8 @@ static void init_smt2_globals(smt2_globals_t *g) { * - delete the timeout object if it's initialized */ static void delete_smt2_globals(smt2_globals_t *g) { - if (g->timeout_initialized) { - delete_timeout(); + if (g->to) { + delete_timeout(g->to); } delete_info_table(g); if (g->logic_name != NULL) { @@ -6598,7 +6602,7 @@ static yices_thread_result_t YICES_THREAD_ATTR check_delayed_assertions_thread(v g->out = output; // /tmp/check_delayed_assertions_thread_.txt g->err = output; // /tmp/check_delayed_assertions_thread_.txt - check_delayed_assertions(g); + check_delayed_assertions(g, /*report=*/false); return yices_thread_exit(); } @@ -6621,18 +6625,22 @@ static smt_status_t get_status_from_globals(smt2_globals_t *g) { static void check_delayed_assertions_mt(smt2_globals_t *g) { bool success; uint32_t i, n; + bool verbose; n = g->nthreads; assert(n > 0); + verbose = g->verbosity > 0; + smt2_globals_t *garray = (smt2_globals_t *) safe_malloc(n * sizeof(smt2_globals_t)); for(i = 0; i < n; i++) { garray[i] = __smt2_globals; // just copy them for now. garray[i].tracer = NULL; // only main thread can use this. } - launch_threads(n, garray, sizeof(smt2_globals_t), "check_delayed_assertions_thread", check_delayed_assertions_thread, true); - fprintf(stderr, "All threads finished. Now computing check_delayed_assertions in main thread.\n"); - check_delayed_assertions(g); + launch_threads(n, garray, sizeof(smt2_globals_t), "check_delayed_assertions_thread", check_delayed_assertions_thread, verbose); + if (verbose) + fprintf(stderr, "All threads finished. Now computing check_delayed_assertions in main thread.\n"); + check_delayed_assertions(g, /*report=*/true); //could check that they are all OK @@ -6646,11 +6654,9 @@ static void check_delayed_assertions_mt(smt2_globals_t *g) { //free the model if there is one, and free the context. //IAM: valgrind says there is no leak here. This is puzzling. } - if (success) { - fprintf(stderr, "SUCCESS: All threads agree.\n"); - } else { - fprintf(stderr, "FAILURE: Threads disagree.\n"); - } + if (verbose) + fprintf(stderr, + success ? "SUCCESS: All threads agree.\n" : "FAILURE: Threads disagree.\n"); safe_free(garray); } #endif @@ -6679,10 +6685,10 @@ void smt2_check_sat(void) { } else { // show_delayed_assertions(&__smt2_globals); #ifndef THREAD_SAFE - check_delayed_assertions(&__smt2_globals); + check_delayed_assertions(&__smt2_globals, /*report=*/true); #else if (__smt2_globals.nthreads == 0) { - check_delayed_assertions(&__smt2_globals); + check_delayed_assertions(&__smt2_globals, /*report=*/true); } else { check_delayed_assertions_mt(&__smt2_globals); } diff --git a/src/frontend/smt2/smt2_commands.h b/src/frontend/smt2/smt2_commands.h index e673bee13..c7d45ef72 100644 --- a/src/frontend/smt2/smt2_commands.h +++ b/src/frontend/smt2/smt2_commands.h @@ -50,6 +50,7 @@ #include "utils/int_vectors.h" #include "utils/ptr_vectors.h" #include "utils/string_hash_map.h" +#include "utils/timeout.h" #include "parser_utils/lexer.h" #include "parser_utils/term_stack2.h" #include "io/tracer.h" @@ -401,7 +402,7 @@ typedef struct smt2_globals_s { // timeout uint32_t timeout; // default = 0 (no timeout) - bool timeout_initialized; // initially false. true once init_timeout is called + timeout_t *to; // initially NULL. Non-NULL once init_timeout is called bool interrupted; // true if the most recent call to check_sat timed out // optional: delegate sat solver for QF_BV diff --git a/src/frontend/yices/yices_reval.c b/src/frontend/yices/yices_reval.c index 14a0bb7b5..d1c8bd47a 100644 --- a/src/frontend/yices/yices_reval.c +++ b/src/frontend/yices/yices_reval.c @@ -138,7 +138,7 @@ * OTHER * - timeout: timeout value in second (applies to check) * timeout value = 0 means no timeout - * - timeout_initialized: true once init_timeout is called + * - to: the timeout structure * * COMMAND-LINE OPTIONS: * - logic_name: logic to use (option --logic=xxx) @@ -175,7 +175,7 @@ static int32_t verbosity; static tracer_t *tracer; static uint32_t timeout; -static bool timeout_initialized; +static timeout_t *to; static char *logic_name; static char *arith_name; @@ -262,8 +262,6 @@ static pp_area_t pp_area = { 140, UINT32_MAX, 0, false, false }; - - /************************** * COMMAND-LINE OPTIONS * *************************/ @@ -2542,11 +2540,10 @@ static void timeout_handler(void *data) { */ static void set_timeout(void) { if (timeout > 0) { - if (!timeout_initialized) { - init_timeout(); - timeout_initialized = true; + if (!to) { + to = init_timeout(); } - start_timeout(timeout, timeout_handler, context); + start_timeout(to, timeout, timeout_handler, context); } } @@ -2555,8 +2552,8 @@ static void set_timeout(void) { */ static void reset_timeout(void) { if (timeout > 0) { - assert(timeout_initialized); - clear_timeout(); + assert(to); + clear_timeout(to); timeout = 0; } } @@ -3999,7 +3996,7 @@ int yices_main(int argc, char *argv[]) { */ interactive = false; timeout = 0; - timeout_initialized = false; + to = NULL; include_depth = 0; ready_time = 0.0; check_process_time = 0.0; @@ -4111,8 +4108,8 @@ int yices_main(int argc, char *argv[]) { yices_exit(); - if (timeout_initialized) { - delete_timeout(); + if (to) { + delete_timeout(to); } return exit_code; diff --git a/src/frontend/yices_smt.c b/src/frontend/yices_smt.c index e70a3b7fc..8c9236871 100644 --- a/src/frontend/yices_smt.c +++ b/src/frontend/yices_smt.c @@ -182,6 +182,7 @@ static arith_solver_t arith_solver; */ static uint32_t timeout; +static timeout_t *to; /* * Filename given on the command line @@ -2040,15 +2041,15 @@ static int process_benchmark(char *filename) { start_search_time = get_cpu_time(); if (timeout > 0) { - init_timeout(); - start_timeout(timeout, timeout_handler, &context); + to = init_timeout(); + start_timeout(to, timeout, timeout_handler, &context); } code = check_context(&context, search_options); clear_handler(); if (timeout > 0) { - clear_timeout(); - delete_timeout(); + clear_timeout(to); + delete_timeout(to); } print_results(); diff --git a/src/frontend/yices_smt2.c b/src/frontend/yices_smt2.c index f7fd78344..e7d9232f8 100644 --- a/src/frontend/yices_smt2.c +++ b/src/frontend/yices_smt2.c @@ -140,6 +140,7 @@ static double ef_ematch_term_alpha; static int32_t ef_ematch_cnstr_mode; static int32_t ef_ematch_term_mode; +static uint32_t nthreads; /**************************** * COMMAND-LINE ARGUMENTS * @@ -185,9 +186,10 @@ typedef enum optid { ematch_term_alpha_opt, // set ematch term learner learning rate ematch_cnstr_mode_opt, // set cnstr mode in ematching ematch_term_mode_opt, // set term mode in ematching + nthreads_opt, // number of threads } optid_t; -#define NUM_OPTIONS (ematch_term_mode_opt+1) +#define NUM_OPTIONS (nthreads_opt+1) /* * Option descriptors @@ -232,6 +234,7 @@ static option_desc_t options[NUM_OPTIONS] = { { "ematch-term-alpha", '\0', MANDATORY_FLOAT, ematch_term_alpha_opt }, { "ematch-cnstr-mode", '\0', MANDATORY_STRING, ematch_cnstr_mode_opt }, { "ematch-term-mode", '\0', MANDATORY_STRING, ematch_term_mode_opt }, + { "nthreads", 'n', MANDATORY_INT, nthreads_opt } }; @@ -271,6 +274,8 @@ static void print_help(const char *progname) { " --mcsat Use the MCSat solver\n" " --mcsat-help Show the MCSat options\n" " --ef-help Show the EF options\n" + " --nthreads= Specify the number of threads (default = 0 = main thread only)\n" + " -n \n" "\n" "For bug reports and other information, please see http://yices.csl.sri.com/\n"); fflush(stdout); @@ -406,6 +411,8 @@ static void parse_command_line(int argc, char *argv[]) { ef_ematch_cnstr_mode = -1; ef_ematch_term_mode = -1; + nthreads = 0; + init_cmdline_parser(&parser, options, NUM_OPTIONS, argv, argc); for (;;) { @@ -463,6 +470,17 @@ static void parse_command_line(int argc, char *argv[]) { timeout = v; break; + case nthreads_opt: + v = elem.i_value; + if (v < 0) { + fprintf(stderr, "%s: the number of threads must be non-negative\n", parser.command_name); + print_usage(parser.command_name); + code = YICES_EXIT_USAGE; + goto exit; + } + nthreads = v; + break; + case incremental_opt: incremental = true; break; @@ -1059,7 +1077,7 @@ int main(int argc, char *argv[]) { init_handlers(); yices_init(); - init_smt2(!incremental, timeout, interactive); + init_mt2(!incremental, timeout, nthreads, interactive); if (smt2_model_format) smt2_force_smt2_model_format(); if (bvdecimal) smt2_force_bvdecimal_format(); if (dimacsfile != NULL && delegate == NULL) smt2_export_to_dimacs(dimacsfile); diff --git a/src/frontend/yices_smt2_mt.c b/src/frontend/yices_smt2_mt.c deleted file mode 100644 index 255429629..000000000 --- a/src/frontend/yices_smt2_mt.c +++ /dev/null @@ -1,638 +0,0 @@ -/* - * This file is part of the Yices SMT Solver. - * Copyright (C) 2017 SRI International. - * - * Yices is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * Yices is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with Yices. If not, see . - */ - -/* - * Yices solver: input in the SMT-LIB 2.0 language multithreaded test bed - */ - -#if defined(CYGWIN) || defined(MINGW) -#ifndef __YICES_DLLSPEC__ -#define __YICES_DLLSPEC__ __declspec(dllexport) -#endif -#endif - -#include -#include -#include -#include -#include -#include -#include -// EXPERIMENT -#include - - -#include "frontend/common/parameters.h" -#include "frontend/smt2/smt2_commands.h" -#include "frontend/smt2/smt2_lexer.h" -#include "frontend/smt2/smt2_parser.h" -#include "frontend/smt2/smt2_term_stack.h" -#include "utils/command_line.h" - -#include "yices.h" -#include "yices_exit_codes.h" - -/* - * yices_rev is set up at compile time in yices_version.c - */ -extern const char * const yices_rev; - -/* - * Global objects: - * - lexer/parser/stack: for processing the SMT2 input - * - incremental: if this flag is true, support for push/pop - * and multiple check_sat is enabled. Otherwise, the solver - * is configured to handle a set of declarations/assertions - * followed by a single call to (check_sat). - * - interactive: if this flag is true, print a prompt before - * parsing commands. Also set the option :print-success to true. - * - timeout: command-line option - * - * - filename = name of the input file (NULL means read stdin) - */ -static lexer_t lexer; -static parser_t parser; -static tstack_t stack; - -static bool incremental; -static bool interactive; -static bool show_stats; -static int32_t verbosity; -static uint32_t timeout; -static uint32_t nthreads; -static char *filename; - -// mcsat options -static bool mcsat; -static bool mcsat_nra_mgcd; -static bool mcsat_nra_nlsat; -static bool mcsat_nra_bound; -static int32_t mcsat_nra_bound_min; -static int32_t mcsat_nra_bound_max; - -static pvector_t trace_tags; - - -/**************************** - * COMMAND-LINE ARGUMENTS * - ***************************/ - -typedef enum optid { - show_version_opt, // print version and exit - show_help_opt, // print help and exit - show_stats_opt, // show statistics after all commands are processed - verbosity_opt, // set verbosity on the command line - incremental_opt, // enable incremental mode - interactive_opt, // enable interactive mode - timeout_opt, // give a timeout - nthreads_opt, // number of threads - mcsat_opt, // enable mcsat - mcsat_nra_mgcd_opt, // use the mgcd instead psc in projection - mcsat_nra_nlsat_opt, // use the nlsat projection instead of brown single-cell - mcsat_nra_bound_opt, // search by increasing bound - mcsat_nra_bound_min_opt, // set initial bound - mcsat_nra_bound_max_opt, // set maximal bound - trace_opt, // enable a trace tag -} optid_t; - -#define NUM_OPTIONS (trace_opt+1) - -/* - * Option descriptors - */ -static option_desc_t options[NUM_OPTIONS] = { - { "version", 'V', FLAG_OPTION, show_version_opt }, - { "help", 'h', FLAG_OPTION, show_help_opt }, - { "stats", 's', FLAG_OPTION, show_stats_opt }, - { "verbosity", 'v', MANDATORY_INT, verbosity_opt }, - { "timeout", 't', MANDATORY_INT, timeout_opt }, - { "nthreads", 'n', MANDATORY_INT, nthreads_opt }, - { "incremental", '\0', FLAG_OPTION, incremental_opt }, - { "interactive", '\0', FLAG_OPTION, interactive_opt }, - { "mcsat", '\0', FLAG_OPTION, mcsat_opt }, - { "mcsat-nra-mgcd", '\0', FLAG_OPTION, mcsat_nra_mgcd_opt }, - { "mcsat-nra-nlsat", '\0', FLAG_OPTION, mcsat_nra_nlsat_opt }, - { "mcsat-nra-bound", '\0', FLAG_OPTION, mcsat_nra_bound_opt }, - { "mcsat-nra-bound-min", '\0', MANDATORY_INT, mcsat_nra_bound_min_opt }, - { "mcsat-nra-bound-max", '\0', MANDATORY_INT, mcsat_nra_bound_max_opt }, - { "trace", 't', MANDATORY_STRING, trace_opt }, -}; - - -/* - * Processing of command-line - */ -static void print_version(void) { - printf("Yices %s\n" - "Copyright SRI International.\n" - "Linked with GMP %s\n" - "Copyright Free Software Foundation, Inc.\n" - "Build date: %s\n" - "Platform: %s (%s)\n" - "Revision: %s\n", - yices_version, gmp_version, - yices_build_date, yices_build_arch, yices_build_mode, yices_rev); - fflush(stdout); -} - -static void print_help(const char *progname) { - printf("Usage: %s [option] filename\n" - " or %s [option]\n", progname, progname); - printf("Option summary:\n" - " --version, -V Show version and exit\n" - " --help, -h Print this message and exit\n" - " --verbosity= Set verbosity level (default = 0)\n" - " -v \n" - " --timeout= Set a timeout in seconds (default = no timeout)\n" - " -t \n" - " --nthreads= Specify the number of threads (default = 0 = main thread only)\n" - " -n \n" - " --stats, -s Print statistics once all commands have been processed\n" - " --incremental Enable support for push/pop\n" - " --interactive Run in interactive mode (ignored if a filename is given)\n" -#if HAVE_MCSAT - " --mcsat Use the MCSat solver\n" - " --mcsat-nra-mgcd Use model-based GCD instead of PSC for projection\n" - " --mcsat-nra-nlsat Use NLSAT projection instead of Brown's single-cell construction\n" - " --mcsat-nra-bound Search by increasing the bound on variable magnitude\n" - " --mcsat-nra-bound-min= Set initial lower bound\n" - " --mcsat-nra-bound-max= Set maximal bound for search" - "" -#endif - "\n" - "For bug reports and other information, please see http://yices.csl.sri.com/\n"); - fflush(stdout); -} - -/* - * Message for unrecognized options or other errors on the command line. - */ -static void print_usage(const char *progname) { - fprintf(stderr, "Usage: %s [options] filename\n", progname); - fprintf(stderr, "Try '%s --help' for more information\n", progname); -} - - -/* - * Parse the command line and process options - */ -static void parse_command_line(int argc, char *argv[]) { - cmdline_parser_t parser; - cmdline_elem_t elem; - optid_t k; - int32_t v; - int code; - - filename = NULL; - incremental = false; - interactive = false; - show_stats = false; - verbosity = 0; - timeout = 0; - nthreads = 0; - - mcsat = false; - mcsat_nra_mgcd = false; - mcsat_nra_nlsat = false; - mcsat_nra_bound = false; - mcsat_nra_bound_min = -1; - mcsat_nra_bound_max = -1; - - init_pvector(&trace_tags, 5); - - init_cmdline_parser(&parser, options, NUM_OPTIONS, argv, argc); - - for (;;) { - cmdline_parse_element(&parser, &elem); - switch (elem.status) { - case cmdline_done: - goto done; - - case cmdline_argument: - if (filename == NULL) { - filename = elem.arg; - } else { - fprintf(stderr, "%s: too many arguments\n", parser.command_name); - print_usage(parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; - } - break; - - case cmdline_option: - k = elem.key; - switch (k) { - case show_version_opt: - print_version(); - code = YICES_EXIT_SUCCESS; - goto exit; - - case show_help_opt: - print_help(parser.command_name); - code = YICES_EXIT_SUCCESS; - goto exit; - - case show_stats_opt: - show_stats = true; - break; - - case verbosity_opt: - v = elem.i_value; - if (v < 0) { - fprintf(stderr, "%s: the verbosity level must be non-negative\n", parser.command_name); - print_usage(parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; - } - verbosity = v; - break; - - case timeout_opt: - v = elem.i_value; - if (v < 0) { - fprintf(stderr, "%s: the timeout must be non-negative\n", parser.command_name); - print_usage(parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; - } - timeout = v; - break; - - case nthreads_opt: - v = elem.i_value; - if (v < 0) { - fprintf(stderr, "%s: the number of threads must be non-negative\n", parser.command_name); - print_usage(parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; - } - nthreads = v; - break; - - case incremental_opt: - incremental = true; - break; - - case interactive_opt: - interactive = true; - break; - - case mcsat_opt: -#if HAVE_MCSAT - mcsat = true; -#else - fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; -#endif - break; - - case mcsat_nra_mgcd_opt: -#if HAVE_MCSAT - mcsat_nra_mgcd = true; -#else - fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; -#endif - break; - - case mcsat_nra_nlsat_opt: -#if HAVE_MCSAT - mcsat_nra_nlsat = true; -#else - fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; -#endif - break; - - case mcsat_nra_bound_opt: -#if HAVE_MCSAT - mcsat_nra_bound = true; -#else - fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; -#endif - break; - - case mcsat_nra_bound_min_opt: -#if HAVE_MCSAT - v = elem.i_value; - if (v < 0) { - fprintf(stderr, "%s: the min value must be non-negative\n", parser.command_name); - print_usage(parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; - } - mcsat_nra_bound_min = v; -#else - fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; -#endif - break; - - case mcsat_nra_bound_max_opt: -#if HAVE_MCSAT - v = elem.i_value; - if (v < 0) { - fprintf(stderr, "%s: the max value must be non-negative\n", parser.command_name); - print_usage(parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; - } - mcsat_nra_bound_max = v; -#else - fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; -#endif - break; - - case trace_opt: - pvector_push(&trace_tags, elem.s_value); - break; - } - break; - - case cmdline_error: - cmdline_print_error(&parser, &elem); - fprintf(stderr, "Try %s --help for more information\n", parser.command_name); - code = YICES_EXIT_USAGE; - goto exit; - } - } - - done: - - // force interactive to false if there's a filename - if (filename != NULL) { - interactive = false; - } - return; - - exit: - // cleanup then exit - // code is either YICES_EXIT_SUCCESS or YICES_EXIT_USAGE. - delete_pvector(&trace_tags); - exit(code); -} - -static void setup_mcsat(void) { - aval_t aval_true; - - if (mcsat) { - smt2_enable_mcsat(); - } - - aval_true = attr_vtbl_symbol(__smt2_globals.avtbl, "true"); - - if (mcsat_nra_mgcd) { - smt2_set_option(":yices-mcsat-nra-mgcd", aval_true); - } - - if (mcsat_nra_nlsat) { - smt2_set_option(":yices-mcsat-nra-nlsat", aval_true); - } - - if (mcsat_nra_bound) { - smt2_set_option(":yices-mcsat-nra-bound", aval_true); - } - - if (mcsat_nra_bound_min >= 0) { - aval_t aval_bound_min; - rational_t q; - q_init(&q); - q_set32(&q, mcsat_nra_bound_min); - aval_bound_min = attr_vtbl_rational(__smt2_globals.avtbl, &q); - smt2_set_option(":yices-mcsat-nra-bound-min", aval_bound_min); - q_clear(&q); - } - - if (mcsat_nra_bound_max >= 0) { - aval_t aval_bound_max; - rational_t q; - q_init(&q); - q_set32(&q, mcsat_nra_bound_max); - aval_bound_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); - smt2_set_option(":yices-mcsat-nra-bound-max", aval_bound_max); - q_clear(&q); - } -} - - -/******************** - * SIGNAL HANDLER * - *******************/ - -static const char signum_msg[24] = "\nInterrupted by signal "; -static char signum_buffer[100]; - -/* - * Write signal number of file 2 (assumed to be stderr): we can't use - * fprintf because it's not safe in a signal handler. - */ -static void write_signum(int signum) { - ssize_t w; - uint32_t i, n; - - memcpy(signum_buffer, signum_msg, sizeof(signum_msg)); - - // force signum to be at most two digits - signum = signum % 100; - n = sizeof(signum_msg); - if (signum > 10) { - signum_buffer[n] = (char)('0' + signum/10); - signum_buffer[n + 1] = (char)('0' + signum % 10); - signum_buffer[n + 2] = '\n'; - n += 3; - } else { - signum_buffer[n] = (char)('0' + signum); - signum_buffer[n + 1] = '\n'; - n += 2; - } - - // write to file 2 - i = 0; - do { - do { - w = write(2, signum_buffer + i, n); - } while (w < 0 && errno == EAGAIN); - if (w < 0) break; // write error, we can't do much about it. - i += (uint32_t) w; - n -= (uint32_t) w; - } while (n > 0); -} - -/* - * We call exit on SIGINT/ABORT and XCPU - * - we could try to handle SIGINT more gracefully in interactive mode - * - this will do for now. - */ -static void default_handler(int signum) { - if (verbosity > 0) { - write_signum(signum); - } - if (show_stats) { - smt2_show_stats(); - } - _exit(YICES_EXIT_INTERRUPTED); -} - - -/* - * Initialize the signal handlers - */ -static void init_handlers(void) { - signal(SIGINT, default_handler); - signal(SIGABRT, default_handler); -#ifndef MINGW - signal(SIGXCPU, default_handler); -#endif -} - - -/* - * Reset the default handlers - */ -static void reset_handlers(void) { - signal(SIGINT, SIG_DFL); - signal(SIGABRT, SIG_DFL); -#ifndef MINGW - signal(SIGXCPU, SIG_DFL); -#endif -} - - - -/********** - * MAIN * - *********/ - -#define HACK_FOR_UTF 0 - -#if HACK_FOR_UTF - -/* - * List of locales to try - */ -#define NUM_LOCALES 3 - -static const char *const locales[NUM_LOCALES] = { - "C.UTF-8", "en_US.utf8", "en_US.UTF-8", -}; - -// HACK TO FORCE UTF8 -static void force_utf8(void) { - uint32_t i; - - for (i=0; i 1) { - fprintf(stderr, "Switched to locale '%s'\n", setlocale(LC_CTYPE, NULL)); - fflush(stderr); - } - return; - } - } - - fprintf(stderr, "Failed to switch locale to UTF-8. Current locale is '%s'\n", setlocale(LC_CTYPE, NULL)); - fflush(stderr); -} - -#else - -static void force_utf8(void) { - // Do nothing -} - -#endif - -int main(int argc, char *argv[]) { - int32_t code; - uint32_t i; - - parse_command_line(argc, argv); - force_utf8(); - - if (filename != NULL) { - // read from file - if (init_smt2_file_lexer(&lexer, filename) < 0) { - perror(filename); - exit(YICES_EXIT_FILE_NOT_FOUND); - } - } else { - // read from stdin - init_smt2_stdin_lexer(&lexer); - } - - init_handlers(); - - yices_init(); - init_mt2(!incremental, timeout, nthreads, interactive); - init_smt2_tstack(&stack); - init_parser(&parser, &lexer, &stack); - - init_parameter_name_table(); - - if (verbosity > 0) { - smt2_set_verbosity(verbosity); - } - if (trace_tags.size > 0) { - for (i = 0; i < trace_tags.size; ++ i) { - smt2_enable_trace_tag(trace_tags.data[i]); - } - } - - setup_mcsat(); - - while (smt2_active()) { - if (interactive) { - // prompt - fputs("yices> ", stderr); - fflush(stderr); - } - code = parse_smt2_command(&parser); - if (code < 0) { - // syntax error - if (interactive) { - flush_lexer(&lexer); - } else { - break; // exit - } - } - } - - if (show_stats) { - smt2_show_stats(); - } - - delete_pvector(&trace_tags); - delete_parser(&parser); - close_lexer(&lexer); - delete_tstack(&stack); - delete_smt2(); - yices_exit(); - - reset_handlers(); - - return YICES_EXIT_SUCCESS; -} - diff --git a/src/frontend/yices_smtcomp.c b/src/frontend/yices_smtcomp.c index 89c53cee9..f6a4f41ad 100644 --- a/src/frontend/yices_smtcomp.c +++ b/src/frontend/yices_smtcomp.c @@ -184,6 +184,8 @@ static tracer_t tracer; */ static uint32_t timeout; +static timeout_t *to; + /* * Input file given on the command line. * If this is NULL, we read from stdin. @@ -1292,14 +1294,14 @@ static int process_benchmark(void) { start_search_time = get_cpu_time(); if (timeout > 0) { - init_timeout(); - start_timeout(timeout, timeout_handler, &context); + to = init_timeout(); + start_timeout(to, timeout, timeout_handler, &context); } code = check_context(&context, ¶ms); clear_handler(); if (timeout > 0) { - clear_timeout(); - delete_timeout(); + clear_timeout(to); + delete_timeout(to); } print_results(); diff --git a/src/mt/threads_posix.c b/src/mt/threads_posix.c index 61d051010..aa34dadeb 100644 --- a/src/mt/threads_posix.c +++ b/src/mt/threads_posix.c @@ -21,6 +21,9 @@ #include #include #include +#include + +#include "utils/error.h" void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* test, yices_thread_main_t thread_main, bool verbose){ int32_t retcode, thread; @@ -29,6 +32,10 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* thread_data_t* tdata = (thread_data_t*)calloc(nthreads, sizeof(thread_data_t)); pthread_t* tids = (pthread_t*)calloc(nthreads, sizeof(pthread_t)); + pthread_attr_t attr; + size_t stacksize; + struct rlimit rlp; + if((tdata == NULL) || (tids == NULL)){ fprintf(stderr, "Couldn't alloc memory for %d threads\n", nthreads); exit(EXIT_FAILURE); @@ -38,6 +45,19 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* printf("%d threads\n", nthreads); } + /* Give child threads the same stack size as the main thread. */ + if (getrlimit(RLIMIT_STACK, &rlp) == -1) + perror_fatal("launch_threads: getrlimit"); + retcode = pthread_attr_init(&attr); + if (retcode == -1) + perror_fatal_code("launch_threads: pthread_attr_init", retcode); + retcode = pthread_attr_getstacksize(&attr, &stacksize); + if (retcode == -1) + perror_fatal_code("launch_threads: pthread_attr_getstacksize", retcode); + retcode = pthread_attr_setstacksize(&attr, rlp.rlim_cur); + if (retcode == -1) + perror_fatal_code("launch_threads: pthread_attr_setstacksize", retcode); + for(thread = 0; thread < nthreads; thread++){ snprintf(buff, 1024, "/tmp/%s_%d.txt", test, thread); if(verbose){ @@ -48,18 +68,19 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* tdata[thread].extra = (extras + (thread * extra_sz)); } tdata[thread].output = fopen(buff, "w"); - if(tdata[thread].output == NULL){ - fprintf(stderr, "fopen failed: %s\n", strerror(errno)); - exit(EXIT_FAILURE); - } + if(tdata[thread].output == NULL) + perror_fatal("launch_threads: fopen"); - retcode = pthread_create(&tids[thread], NULL, thread_main, &tdata[thread]); - if(retcode){ - fprintf(stderr, "pthread_create failed: %s\n", strerror(retcode)); - exit(EXIT_FAILURE); - } + retcode = pthread_create(&tids[thread], &attr, thread_main, &tdata[thread]); + if(retcode) + perror_fatal_code("launch_threads: pthread_create", retcode); } + retcode = pthread_attr_destroy(&attr); + if (retcode) + perror_fatal_code("launch_threads: pthread_attr_destroy", retcode); + + if(verbose){ printf("threads away\n\n"); } @@ -67,10 +88,8 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* for(thread = 0; thread < nthreads; thread++){ retcode = pthread_join(tids[thread], NULL); - if(retcode){ - fprintf(stderr, "pthread_join failed: %s\n", strerror(retcode)); - exit(EXIT_FAILURE); - } + if(retcode) + perror_fatal_code("launch_threads: pthread_join", retcode); fclose(tdata[thread].output); } diff --git a/src/utils/error.c b/src/utils/error.c new file mode 100644 index 000000000..568fa23f0 --- /dev/null +++ b/src/utils/error.c @@ -0,0 +1,36 @@ +/* + * This file is part of the Yices SMT Solver. + * Copyright (C) 2023 SRI International. + * + * Yices is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Yices is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Yices. If not, see . + */ + +#include +#include +#include + +#include "yices_exit_codes.h" + +void perror_fatal(const char *s) { + perror_fatal(s, errno); + exit(YICES_EXIT_INTERNAL_ERROR); +} + +void perror_fatal_code(const char *s, int err) { + char buffer[64]; + + strerror_r(err, buffer, sizeof(buffer)); + fprintf(stderr, "%s: %s\n", s, buffer); + exit(YICES_EXIT_INTERNAL_ERROR); +} diff --git a/src/utils/error.h b/src/utils/error.h new file mode 100644 index 000000000..02d29d556 --- /dev/null +++ b/src/utils/error.h @@ -0,0 +1,29 @@ +/* + * This file is part of the Yices SMT Solver. + * Copyright (C) 2023 SRI International. + * + * Yices is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Yices is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Yices. If not, see . + */ + +#ifndef __ERROR_H +#define __ERROR_H + +/* Like perror, but exit after printing the message. */ +extern void perror_fatal(const char *s); + +/* Like perror, but use ERR as the error code and exit after printing + the message. */ +extern void perror_fatal_code(const char *s, int err); + +#endif diff --git a/src/utils/timeout.c b/src/utils/timeout.c index 3dadd02b4..fe3b9e6fb 100644 --- a/src/utils/timeout.c +++ b/src/utils/timeout.c @@ -44,15 +44,53 @@ #include +#include "utils/error.h" +#include "utils/memalloc.h" #include "utils/timeout.h" #include "yices_exit_codes.h" +#if !defined(MINGW) && defined(THREAD_SAFE) +#include +#endif + +/* + * Timeout state: + * - NOT_READY: initial state and after call to delete_timeout + * - READY: ready to be started (state after init_timeout + * and after clear_timeout) + * - ACTIVE: after a call to start_timeout, before the timer fires + * or the timeout is canceled + * - CANCELED: used by clear_timeout + * - FIRED: after the handler has been called + */ +typedef enum timeout_state { + TIMEOUT_NOT_READY, // 0 + TIMEOUT_READY, + TIMEOUT_ACTIVE, + TIMEOUT_CANCELED, + TIMEOUT_FIRED, +} timeout_state_t; + + +typedef struct timeout_s { + timeout_state_t state; + timeout_handler_t handler; + void *param; +#ifdef THREAD_SAFE + struct timeval tv; + pthread_t thread; + int pipe[2]; +#endif +} timeout_t; + +#ifndef THREAD_SAFE /* * Global structure common to both implementation. */ static timeout_t the_timeout; +#endif #ifndef MINGW @@ -65,7 +103,115 @@ static timeout_t the_timeout; #include #include #include +#include + +#ifdef THREAD_SAFE + +timeout_t *init_timeout(void) { + timeout_t *timeout; + timeout = (timeout_t *) safe_malloc(sizeof(timeout_t)); + + timeout->state = TIMEOUT_READY; + timeout->handler = NULL; + timeout->param = NULL; + timeout->tv.tv_sec = 0; + timeout->tv.tv_usec = 0; + timeout->pipe[0] = timeout->pipe[1] = -1; + + return timeout; +} + +void delete_timeout(timeout_t *timeout) { + /* The read end of the pipe should have been closed by the timer + thread. */ + assert(timeout->pipe[0] == -1); + /* The write end of the pipe should have been closed by + clear_timer. */ + assert(timeout->pipe[1] == -1); + + safe_free(timeout); +} + +static void *timer_thread(void *arg) { + timeout_t *timeout; + int fd; + fd_set readfds; + + timeout = (timeout_t *) arg; + + fd = timeout->pipe[0]; + FD_ZERO(&readfds); + FD_SET(fd, &readfds); + + /* Watch the read end of the pipe until the timeout occurs. */ + switch (select(fd + 1, &readfds, + /*writefds=*/NULL, /*errorfds=*/NULL, + &timeout->tv)) { + case -1: + /* Error. */ + perror_fatal("timer_thread: select"); + break; + + case 0: + /* Timeout. */ + timeout->state = TIMEOUT_FIRED; + timeout->handler(timeout->param); + break; + + case 1: + /* Canceled. */ + assert(FD_ISSET(fd, &readfds)); + timeout->state = TIMEOUT_CANCELED; + break; + + default: + assert(0); + } + + /* Close the read end of the pipe. */ + if (close(timeout->pipe[0]) == -1) + perror_fatal("timer_thread: close"); + timeout->pipe[0] = -1; + + return NULL; +} + +void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) { + int ret; + + assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL); + + timeout->state = TIMEOUT_ACTIVE; + timeout->tv.tv_sec = delay; + timeout->tv.tv_usec = 0; + timeout->handler = handler; + timeout->param = param; + + if (pipe(timeout->pipe) == -1) + perror_fatal("start_timeout: pipe"); + + ret = pthread_create(&timeout->thread, /*attr=*/NULL, timer_thread, timeout); + if (ret) + perror_fatal_code("start_timeout: pthread_create", ret); +} + +void clear_timeout(timeout_t *timeout) { + void *value; + + /* Tell the thread to exit. */ + if (close(timeout->pipe[1]) == -1) + perror_fatal("clear_timeout: close"); + timeout->pipe[1] = -1; + + /* Wait for the thread to exit. */ + if (pthread_join(timeout->thread, &value) == -1) + perror_fatal("clear_timeout: pthread_join"); + + timeout->state = TIMEOUT_READY; +} + +#else /* !defined(THREAD_SAFE) */ /* * To save the original SIG_ALRM handler @@ -92,7 +238,7 @@ static void alarm_handler(int signum) { * - install the alarm_handler (except on Solaris) * - initialize state to READY */ -void init_timeout(void) { +timeout_t *init_timeout(void) { #ifndef SOLARIS saved_handler = signal(SIGALRM, alarm_handler); if (saved_handler == SIG_ERR) { @@ -104,6 +250,8 @@ void init_timeout(void) { the_timeout.state = TIMEOUT_READY;; the_timeout.handler = NULL; the_timeout.param = NULL; + + return &the_timeout; } @@ -116,11 +264,12 @@ void init_timeout(void) { * * On Solaris: set the signal handler here. */ -void start_timeout(uint32_t delay, timeout_handler_t handler, void *param) { - assert(delay > 0 && the_timeout.state == TIMEOUT_READY && handler != NULL); - the_timeout.state = TIMEOUT_ACTIVE; - the_timeout.handler = handler; - the_timeout.param = param; +void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) { + assert(timeout == &the_timeout); + assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL); + timeout->state = TIMEOUT_ACTIVE; + timeout->handler = handler; + timeout->param = param; #ifdef SOLARIS saved_handler = signal(SIGALRM, alarm_handler); @@ -140,14 +289,16 @@ void start_timeout(uint32_t delay, timeout_handler_t handler, void *param) { * - cancel the timeout if it's not fired * - set state to READY */ -void clear_timeout(void) { +void clear_timeout(timeout_t *timeout) { + assert(timeout == &the_timeout); + // TODO: Check whether we should block the signals here? - if (the_timeout.state == TIMEOUT_ACTIVE) { + if (the_timeout->state == TIMEOUT_ACTIVE) { // not fired; - the_timeout.state = TIMEOUT_CANCELED; + the_timeout->state = TIMEOUT_CANCELED; (void) alarm(0); // cancel the alarm } - the_timeout.state = TIMEOUT_READY; + the_timeout->state = TIMEOUT_READY; } @@ -156,14 +307,17 @@ void clear_timeout(void) { * - cancel the timeout if it's active * - restore the original handler */ -void delete_timeout(void) { - if (the_timeout.state == TIMEOUT_ACTIVE) { +void delete_timeout(timeout_t *timeout) { + assert(timeout == &the_timeout); + + if (timeout->state == TIMEOUT_ACTIVE) { (void) alarm(0); } (void) signal(SIGALRM, saved_handler); - the_timeout.state = TIMEOUT_NOT_READY; + timeout->state = TIMEOUT_NOT_READY; } +#endif /* defined(THREAD_SAFE) */ #else @@ -210,7 +364,7 @@ static VOID CALLBACK timer_callback(PVOID param, BOOLEAN timer_or_wait_fired) { * Initialization: * - create the timer queue */ -void init_timeout(void) { +timeout_t *init_timeout(void) { timer_queue = CreateTimerQueue(); if (timer_queue == NULL) { fprintf(stderr, "Yices: CreateTimerQueue failed with error code %"PRIu32"\n", (uint32_t) GetLastError()); @@ -221,6 +375,8 @@ void init_timeout(void) { the_timeout.state = TIMEOUT_READY; the_timeout.handler = NULL; the_timeout.param = NULL; + + return &the_timeout; } @@ -231,9 +387,10 @@ void init_timeout(void) { * - handler = handler to call if fired * - param = parameter for the handler */ -void start_timeout(uint32_t delay, timeout_handler_t handler, void *param) { +void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) { DWORD duetime; + assert(timeout == &the_timeout); assert(delay > 0 && the_timeout.state == TIMEOUT_READY && handler != NULL); duetime = delay * 1000; // delay in milliseconds @@ -255,10 +412,12 @@ void start_timeout(uint32_t delay, timeout_handler_t handler, void *param) { /* * Delete the timer */ -void clear_timeout(void) { +void clear_timeout(timeout_t *timeout) { // GetLastError returns DWORD, which is an unsigned 32bit integer uint32_t error_code; + assert(timeout == &the_timeout); + if (the_timeout.state == TIMEOUT_ACTIVE || the_timeout.state == TIMEOUT_FIRED) { if (the_timeout.state == TIMEOUT_ACTIVE) { // active and not fired yet @@ -292,7 +451,9 @@ void clear_timeout(void) { * Final cleanup: * - delete the timer_queue */ -void delete_timeout(void) { +void delete_timeout(timeout_t *timeout) { + assert(timeout == &the_timeout); + if (! DeleteTimerQueueEx(timer_queue, INVALID_HANDLE_VALUE)) { fprintf(stderr, "Yices: DeleteTimerQueueEx failed with error code %"PRIu32"\n", (uint32_t) GetLastError()); fflush(stderr); diff --git a/src/utils/timeout.h b/src/utils/timeout.h index 6fb3e78cb..009282d0e 100644 --- a/src/utils/timeout.h +++ b/src/utils/timeout.h @@ -53,26 +53,6 @@ #include - -/* - * Timeout state: - * - NOT_READY: initial state and after call to delete_timeout - * - READY: ready to be started (state after init_timeout - * and after clear_timeout) - * - ACTIVE: after a call to start_timeout, before the timer fires - * or the timeout is canceled - * - CANCELED: used by clear_timeout - * - FIRED: after the handler has been called - */ -typedef enum timeout_state { - TIMEOUT_NOT_READY, // 0 - TIMEOUT_READY, - TIMEOUT_ACTIVE, - TIMEOUT_CANCELED, - TIMEOUT_FIRED, -} timeout_state_t; - - /* * Handler: a function with a single (void*) parameter * - should do something cheap and fast. @@ -83,11 +63,7 @@ typedef void (*timeout_handler_t)(void *data); /* * Internal structure used to manage the timeout */ -typedef struct timeout_s { - timeout_state_t state; - timeout_handler_t handler; - void *param; -} timeout_t; +typedef struct timeout_s timeout_t; @@ -98,7 +74,7 @@ typedef struct timeout_s { /* * Initialize internal structures */ -extern void init_timeout(void); +extern timeout_t *init_timeout(void); /* @@ -107,20 +83,20 @@ extern void init_timeout(void); * - handler = the handler to call * - param = data passed to the handler */ -extern void start_timeout(uint32_t delay, timeout_handler_t handler, void *param); +extern void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param); /* * Cancel the timeout if it's not fired. * Cleanup any structure allocated by start timeout. */ -extern void clear_timeout(void); +extern void clear_timeout(timeout_t *timeout); /* * Final cleanup */ -extern void delete_timeout(void); +extern void delete_timeout(timeout_t *timeout); diff --git a/tests/unit/test_timeout.c b/tests/unit/test_timeout.c index 0af1a1606..e780ae640 100644 --- a/tests/unit/test_timeout.c +++ b/tests/unit/test_timeout.c @@ -92,16 +92,16 @@ static void show_counter(uint32_t *c, uint32_t n) { /* * Test: n = size of the counter, t = timeout value */ -static void test_timeout(uint32_t *c, uint32_t n, uint32_t timeout) { +static void test_timeout(timeout_t *to, uint32_t *c, uint32_t n, uint32_t timeout) { double start, end; printf("---> test: size = %"PRIu32", timeout = %"PRIu32" s\n", n, timeout); fflush(stdout); wrapper.interrupted = false; - start_timeout(timeout, handler, &wrapper); + start_timeout(to, timeout, handler, &wrapper); start = get_cpu_time(); loop(c, n); - clear_timeout(); + clear_timeout(to); end = get_cpu_time(); printf(" cpu time = %.2f s\n", end - start); fflush(stdout); @@ -127,15 +127,16 @@ static uint32_t counter[64]; int main(void) { uint32_t n; uint32_t time; - - init_timeout(); + timeout_t *timeout; + + timeout = init_timeout(); time = 20; for (n=5; n<40; n++) { - test_timeout(counter, n, time); + test_timeout(timeout, counter, n, time); } - delete_timeout(); + delete_timeout(timeout); return 0; } From 9218605c9b71469c43a646e09076adf799dc011d Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Fri, 22 Sep 2023 13:29:18 -0700 Subject: [PATCH 08/15] Fix typo. --- src/utils/error.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/utils/error.c b/src/utils/error.c index 568fa23f0..fee3577e1 100644 --- a/src/utils/error.c +++ b/src/utils/error.c @@ -23,7 +23,7 @@ #include "yices_exit_codes.h" void perror_fatal(const char *s) { - perror_fatal(s, errno); + perror(s); exit(YICES_EXIT_INTERNAL_ERROR); } From d493dc1056ed8e9d83ffdbe428e76cda8be0731e Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Fri, 22 Sep 2023 20:40:04 -0700 Subject: [PATCH 09/15] Use ptrhead condition variables to communicate with the timer thread. --- src/utils/timeout.c | 113 ++++++++++++++++++++++---------------------- 1 file changed, 57 insertions(+), 56 deletions(-) diff --git a/src/utils/timeout.c b/src/utils/timeout.c index fe3b9e6fb..00ae7ffc3 100644 --- a/src/utils/timeout.c +++ b/src/utils/timeout.c @@ -77,9 +77,10 @@ typedef struct timeout_s { timeout_handler_t handler; void *param; #ifdef THREAD_SAFE - struct timeval tv; + struct timespec ts; pthread_t thread; - int pipe[2]; + pthread_mutex_t mutex; + pthread_cond_t cond; #endif } timeout_t; @@ -107,6 +108,13 @@ static timeout_t the_timeout; #ifdef THREAD_SAFE +#include + +static inline void check_pthread(int err, const char *msg) { + if (err) + perror_fatal_code(msg, err); +} + timeout_t *init_timeout(void) { timeout_t *timeout; @@ -115,98 +123,91 @@ timeout_t *init_timeout(void) { timeout->state = TIMEOUT_READY; timeout->handler = NULL; timeout->param = NULL; - timeout->tv.tv_sec = 0; - timeout->tv.tv_usec = 0; - timeout->pipe[0] = timeout->pipe[1] = -1; + timeout->ts.tv_sec = 0; + timeout->ts.tv_nsec = 0; + check_pthread(pthread_mutex_init(&timeout->mutex, /*attr=*/NULL), + "start_timeout: pthread_mutex_init"); + check_pthread(pthread_cond_init(&timeout->cond, /*attr=*/NULL), + "start_timeout: pthread_cond_init"); + return timeout; } void delete_timeout(timeout_t *timeout) { - /* The read end of the pipe should have been closed by the timer - thread. */ - assert(timeout->pipe[0] == -1); - /* The write end of the pipe should have been closed by - clear_timer. */ - assert(timeout->pipe[1] == -1); - + check_pthread(pthread_cond_destroy(&timeout->cond), + "delete_timeout: pthread_cond_destroy"); + check_pthread(pthread_mutex_destroy(&timeout->mutex), + "delete_timeout: pthread_mutex_destroy"); + safe_free(timeout); } static void *timer_thread(void *arg) { timeout_t *timeout; - int fd; - fd_set readfds; timeout = (timeout_t *) arg; - fd = timeout->pipe[0]; - FD_ZERO(&readfds); - FD_SET(fd, &readfds); - - /* Watch the read end of the pipe until the timeout occurs. */ - switch (select(fd + 1, &readfds, - /*writefds=*/NULL, /*errorfds=*/NULL, - &timeout->tv)) { - case -1: - /* Error. */ - perror_fatal("timer_thread: select"); - break; - - case 0: - /* Timeout. */ + /* Get exclusive access to the state. */ + check_pthread(pthread_mutex_lock(&timeout->mutex), + "timer_thread: pthread_mutex_lock"); + /* It is theoretically possible that the timeout has already been + canceled by a quick call to clear_timeout. If so, we do not need + to wait. */ + if (timeout->state != TIMEOUT_CANCELED) { + int ret = pthread_cond_timedwait(&timeout->cond, &timeout->mutex, + &timeout->ts); + if (ret && ret != ETIMEDOUT) + perror_fatal_code("timer_thread: pthread_cond_timedwait", ret); + } + + /* If the timeout wasn't canceled, then the timeout expired. */ + if (timeout->state != TIMEOUT_CANCELED) { timeout->state = TIMEOUT_FIRED; timeout->handler(timeout->param); - break; - - case 1: - /* Canceled. */ - assert(FD_ISSET(fd, &readfds)); - timeout->state = TIMEOUT_CANCELED; - break; - - default: - assert(0); } - /* Close the read end of the pipe. */ - if (close(timeout->pipe[0]) == -1) - perror_fatal("timer_thread: close"); - timeout->pipe[0] = -1; + check_pthread(pthread_mutex_unlock(&timeout->mutex), + "timer_thread: pthread_mutex_unlock"); return NULL; } void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) { - int ret; + struct timeval tv; assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL); timeout->state = TIMEOUT_ACTIVE; - timeout->tv.tv_sec = delay; - timeout->tv.tv_usec = 0; timeout->handler = handler; timeout->param = param; - if (pipe(timeout->pipe) == -1) - perror_fatal("start_timeout: pipe"); + /* Compute the desired stop time. */ + if (gettimeofday(&tv, /*tzp=*/NULL) == -1) + perror_fatal("start_timeout: gettimeofday"); + timeout->ts.tv_sec = tv.tv_sec + delay; + timeout->ts.tv_nsec = 1000 * tv.tv_usec; - ret = pthread_create(&timeout->thread, /*attr=*/NULL, timer_thread, timeout); - if (ret) - perror_fatal_code("start_timeout: pthread_create", ret); + check_pthread(pthread_create(&timeout->thread, /*attr=*/NULL, + timer_thread, timeout), + "start_timeout: pthread_create"); } void clear_timeout(timeout_t *timeout) { void *value; /* Tell the thread to exit. */ - if (close(timeout->pipe[1]) == -1) - perror_fatal("clear_timeout: close"); - timeout->pipe[1] = -1; + check_pthread(pthread_mutex_lock(&timeout->mutex), + "clear_timeout: pthread_mutex_lock"); + timeout->state = TIMEOUT_CANCELED; + check_pthread(pthread_mutex_unlock(&timeout->mutex), + "clear_timeout: pthread_mutex_unlock"); + check_pthread(pthread_cond_signal(&timeout->cond), + "clear_timeout: pthread_cond_signal"); /* Wait for the thread to exit. */ - if (pthread_join(timeout->thread, &value) == -1) - perror_fatal("clear_timeout: pthread_join"); + check_pthread(pthread_join(timeout->thread, &value), + "clear_timeout: pthread_join"); timeout->state = TIMEOUT_READY; } From 706e87fd2216b00c6c7ea9fb5a4c567bb45afb0f Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Sat, 23 Sep 2023 10:28:10 -0700 Subject: [PATCH 10/15] Simplify thread API checks. --- src/mt/threads.h | 14 +++++++++ src/mt/threads_posix.c | 33 +++++++++------------ src/mt/yices_locks_posix.c | 60 +++++++++++++++++-------------------- src/utils/timeout.c | 61 +++++++++++++++++--------------------- 4 files changed, 84 insertions(+), 84 deletions(-) diff --git a/src/mt/threads.h b/src/mt/threads.h index 9e293e5a9..9f4a40f12 100644 --- a/src/mt/threads.h +++ b/src/mt/threads.h @@ -22,6 +22,8 @@ #include #include +#include "utils/error.h" + /* the thread main */ #ifdef MINGW #define YICES_THREAD_ATTR __stdcall @@ -58,5 +60,17 @@ extern void mt_test_usage(int32_t argc, char* argv[]); extern yices_thread_result_t yices_thread_exit(void); +/* + * Wrap around a thread API call. If the API call indicates error, + * print the message, a description of the error, and exit. + */ +#ifndef MINGW +#define check_thread_api(expr, msg) (expr) +#else +static inline void check_thread_api(int expr, const char *msg) { + if (expr) + perror_fatal_code(msg, expr); +} +#endif #endif /* __THREADS_H */ diff --git a/src/mt/threads_posix.c b/src/mt/threads_posix.c index aa34dadeb..14d043aa4 100644 --- a/src/mt/threads_posix.c +++ b/src/mt/threads_posix.c @@ -26,7 +26,7 @@ #include "utils/error.h" void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* test, yices_thread_main_t thread_main, bool verbose){ - int32_t retcode, thread; + int32_t thread; char buff[1024]; thread_data_t* tdata = (thread_data_t*)calloc(nthreads, sizeof(thread_data_t)); @@ -48,15 +48,12 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* /* Give child threads the same stack size as the main thread. */ if (getrlimit(RLIMIT_STACK, &rlp) == -1) perror_fatal("launch_threads: getrlimit"); - retcode = pthread_attr_init(&attr); - if (retcode == -1) - perror_fatal_code("launch_threads: pthread_attr_init", retcode); - retcode = pthread_attr_getstacksize(&attr, &stacksize); - if (retcode == -1) - perror_fatal_code("launch_threads: pthread_attr_getstacksize", retcode); - retcode = pthread_attr_setstacksize(&attr, rlp.rlim_cur); - if (retcode == -1) - perror_fatal_code("launch_threads: pthread_attr_setstacksize", retcode); + check_thread_api(pthread_attr_init(&attr), + "launch_threads: pthread_attr_init"); + check_thread_api(pthread_attr_getstacksize(&attr, &stacksize), + "launch_threads: pthread_attr_getstacksize"); + check_thread_api(pthread_attr_setstacksize(&attr, rlp.rlim_cur), + "launch_threads: pthread_attr_setstacksize"); for(thread = 0; thread < nthreads; thread++){ snprintf(buff, 1024, "/tmp/%s_%d.txt", test, thread); @@ -71,14 +68,13 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* if(tdata[thread].output == NULL) perror_fatal("launch_threads: fopen"); - retcode = pthread_create(&tids[thread], &attr, thread_main, &tdata[thread]); - if(retcode) - perror_fatal_code("launch_threads: pthread_create", retcode); + check_thread_api(pthread_create(&tids[thread], &attr, thread_main, + &tdata[thread]), + "launch_threads: pthread_create"); } - retcode = pthread_attr_destroy(&attr); - if (retcode) - perror_fatal_code("launch_threads: pthread_attr_destroy", retcode); + check_thread_api(pthread_attr_destroy(&attr), + "launch_threads: pthread_attr_destroy"); if(verbose){ @@ -87,9 +83,8 @@ void launch_threads(int32_t nthreads, void* extras, size_t extra_sz, const char* for(thread = 0; thread < nthreads; thread++){ - retcode = pthread_join(tids[thread], NULL); - if(retcode) - perror_fatal_code("launch_threads: pthread_join", retcode); + check_thread_api(pthread_join(tids[thread], NULL), + "launch_threads: pthread_join"); fclose(tdata[thread].output); } diff --git a/src/mt/yices_locks_posix.c b/src/mt/yices_locks_posix.c index 827e7f584..a84f00f84 100644 --- a/src/mt/yices_locks_posix.c +++ b/src/mt/yices_locks_posix.c @@ -23,6 +23,7 @@ #include #include "yices_locks.h" +#include "threads.h" static void print_error(const char *caller, const char *syscall, int errnum) { char buffer[64]; @@ -33,27 +34,29 @@ static void print_error(const char *caller, const char *syscall, int errnum) { } int32_t create_yices_lock(yices_lock_t* lock){ - int32_t retcode; + pthread_mutexattr_t *mattr = NULL; + #ifndef NDEBUG + /* Make the mutex detect recursive locks. */ pthread_mutexattr_t mta; - pthread_mutexattr_t *mattr = &mta; -#else - pthread_mutexattr_t *mattr = NULL; + + mattr = &mta; + + check_thread_api(pthread_mutexattr_init(mattr), + "create_yices_lock: pthread_mutexattr_init"); + check_thread_api(pthread_mutexattr_settype(mattr, + PTHREAD_MUTEX_ERRORCHECK), + "create_yices_lock: pthread_mutextattr_settype"); #endif + check_thread_api(pthread_mutex_init(lock, mattr), + "create_yices_lock: pthread_mutex_init"); + #ifndef NDEBUG - retcode = pthread_mutexattr_init(mattr); - if(retcode) - print_error("create_yices_lock", "pthread_mutexattr_init", retcode); - retcode = pthread_mutexattr_settype(mattr, PTHREAD_MUTEX_ERRORCHECK); - if(retcode) - print_error("create_yices_lock", "pthread_mutextattr_settype", retcode); + check_thread_api(pthread_mutexattr_destroy(mattr) #endif - retcode = pthread_mutex_init(lock, mattr); - if(retcode) - print_error("create_yices_lock", "pthread_mutex_init", retcode); - assert(retcode == 0); - return retcode; + + return 0; } int32_t try_yices_lock(yices_lock_t* lock){ @@ -71,27 +74,20 @@ int32_t try_yices_lock(yices_lock_t* lock){ int32_t get_yices_lock(yices_lock_t* lock){ - int32_t retcode = pthread_mutex_lock(lock); - if(retcode){ - print_error("get_yices_lock", "pthread_mutex_lock", retcode); - } - assert(retcode == 0); - return retcode; + check_thread_api(pthread_mutex_lock(lock), + "get_yices_lock: pthread_mutex_lock"); + + return 0; } int32_t release_yices_lock(yices_lock_t* lock){ - int32_t retcode = pthread_mutex_unlock(lock); - if(retcode){ - print_error("release_yices_lock", "pthread_mutex_unlock", retcode); - } - assert(retcode == 0); - return retcode; + check_thread_api(pthread_mutex_unlock(lock), + "release_yices_lock: pthread_mutex_unlock"); + + return 0; } void destroy_yices_lock(yices_lock_t* lock){ - int32_t retcode = pthread_mutex_destroy(lock); - if(retcode){ - print_error("destroy_yices_lock", "pthread_mutex_destroy", retcode); - } - assert(retcode == 0); + check_thread_api(pthread_mutex_destroy(lock), + "destroy_yices_lock: pthread_mutex_destroy"); } diff --git a/src/utils/timeout.c b/src/utils/timeout.c index 00ae7ffc3..169e575b1 100644 --- a/src/utils/timeout.c +++ b/src/utils/timeout.c @@ -43,16 +43,16 @@ */ #include +#if !defined(MINGW) && defined(THREAD_SAFE) +#include +#include +#endif #include "utils/error.h" #include "utils/memalloc.h" #include "utils/timeout.h" #include "yices_exit_codes.h" -#if !defined(MINGW) && defined(THREAD_SAFE) -#include -#endif - /* * Timeout state: * - NOT_READY: initial state and after call to delete_timeout @@ -108,12 +108,7 @@ static timeout_t the_timeout; #ifdef THREAD_SAFE -#include - -static inline void check_pthread(int err, const char *msg) { - if (err) - perror_fatal_code(msg, err); -} +#include "mt/threads.h" timeout_t *init_timeout(void) { timeout_t *timeout; @@ -126,19 +121,19 @@ timeout_t *init_timeout(void) { timeout->ts.tv_sec = 0; timeout->ts.tv_nsec = 0; - check_pthread(pthread_mutex_init(&timeout->mutex, /*attr=*/NULL), - "start_timeout: pthread_mutex_init"); - check_pthread(pthread_cond_init(&timeout->cond, /*attr=*/NULL), - "start_timeout: pthread_cond_init"); + check_thread_api(pthread_mutex_init(&timeout->mutex, /*attr=*/NULL), + "start_timeout: pthread_mutex_init"); + check_thread_api(pthread_cond_init(&timeout->cond, /*attr=*/NULL), + "start_timeout: pthread_cond_init"); return timeout; } void delete_timeout(timeout_t *timeout) { - check_pthread(pthread_cond_destroy(&timeout->cond), - "delete_timeout: pthread_cond_destroy"); - check_pthread(pthread_mutex_destroy(&timeout->mutex), - "delete_timeout: pthread_mutex_destroy"); + check_thread_api(pthread_cond_destroy(&timeout->cond), + "delete_timeout: pthread_cond_destroy"); + check_thread_api(pthread_mutex_destroy(&timeout->mutex), + "delete_timeout: pthread_mutex_destroy"); safe_free(timeout); } @@ -149,8 +144,8 @@ static void *timer_thread(void *arg) { timeout = (timeout_t *) arg; /* Get exclusive access to the state. */ - check_pthread(pthread_mutex_lock(&timeout->mutex), - "timer_thread: pthread_mutex_lock"); + check_thread_api(pthread_mutex_lock(&timeout->mutex), + "timer_thread: pthread_mutex_lock"); /* It is theoretically possible that the timeout has already been canceled by a quick call to clear_timeout. If so, we do not need to wait. */ @@ -167,8 +162,8 @@ static void *timer_thread(void *arg) { timeout->handler(timeout->param); } - check_pthread(pthread_mutex_unlock(&timeout->mutex), - "timer_thread: pthread_mutex_unlock"); + check_thread_api(pthread_mutex_unlock(&timeout->mutex), + "timer_thread: pthread_mutex_unlock"); return NULL; } @@ -188,26 +183,26 @@ void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler timeout->ts.tv_sec = tv.tv_sec + delay; timeout->ts.tv_nsec = 1000 * tv.tv_usec; - check_pthread(pthread_create(&timeout->thread, /*attr=*/NULL, - timer_thread, timeout), - "start_timeout: pthread_create"); + check_thread_api(pthread_create(&timeout->thread, /*attr=*/NULL, + timer_thread, timeout), + "start_timeout: pthread_create"); } void clear_timeout(timeout_t *timeout) { void *value; /* Tell the thread to exit. */ - check_pthread(pthread_mutex_lock(&timeout->mutex), - "clear_timeout: pthread_mutex_lock"); + check_thread_api(pthread_mutex_lock(&timeout->mutex), + "clear_timeout: pthread_mutex_lock"); timeout->state = TIMEOUT_CANCELED; - check_pthread(pthread_mutex_unlock(&timeout->mutex), - "clear_timeout: pthread_mutex_unlock"); - check_pthread(pthread_cond_signal(&timeout->cond), - "clear_timeout: pthread_cond_signal"); + check_thread_api(pthread_mutex_unlock(&timeout->mutex), + "clear_timeout: pthread_mutex_unlock"); + check_thread_api(pthread_cond_signal(&timeout->cond), + "clear_timeout: pthread_cond_signal"); /* Wait for the thread to exit. */ - check_pthread(pthread_join(timeout->thread, &value), - "clear_timeout: pthread_join"); + check_thread_api(pthread_join(timeout->thread, &value), + "clear_timeout: pthread_join"); timeout->state = TIMEOUT_READY; } From 0069a787cf6b0f71bb14f1c005d0999dde24132e Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Sat, 23 Sep 2023 10:52:23 -0700 Subject: [PATCH 11/15] Fix typo in non-THREAD_SAFE code. --- src/utils/timeout.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/utils/timeout.c b/src/utils/timeout.c index 169e575b1..a70b9ce54 100644 --- a/src/utils/timeout.c +++ b/src/utils/timeout.c @@ -289,12 +289,12 @@ void clear_timeout(timeout_t *timeout) { assert(timeout == &the_timeout); // TODO: Check whether we should block the signals here? - if (the_timeout->state == TIMEOUT_ACTIVE) { + if (the_timeout.state == TIMEOUT_ACTIVE) { // not fired; - the_timeout->state = TIMEOUT_CANCELED; + the_timeout.state = TIMEOUT_CANCELED; (void) alarm(0); // cancel the alarm } - the_timeout->state = TIMEOUT_READY; + the_timeout.state = TIMEOUT_READY; } @@ -306,11 +306,11 @@ void clear_timeout(timeout_t *timeout) { void delete_timeout(timeout_t *timeout) { assert(timeout == &the_timeout); - if (timeout->state == TIMEOUT_ACTIVE) { + if (the_timeout.state == TIMEOUT_ACTIVE) { (void) alarm(0); } (void) signal(SIGALRM, saved_handler); - timeout->state = TIMEOUT_NOT_READY; + the_timeout.state = TIMEOUT_NOT_READY; } #endif /* defined(THREAD_SAFE) */ From a7cf045a357e325286da1563a27b338069ce1270 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Sat, 23 Sep 2023 10:56:05 -0700 Subject: [PATCH 12/15] Undo unnecessary changes. --- src/utils/timeout.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/utils/timeout.c b/src/utils/timeout.c index a70b9ce54..3a5812b3a 100644 --- a/src/utils/timeout.c +++ b/src/utils/timeout.c @@ -263,9 +263,9 @@ timeout_t *init_timeout(void) { void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) { assert(timeout == &the_timeout); assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL); - timeout->state = TIMEOUT_ACTIVE; - timeout->handler = handler; - timeout->param = param; + the_timeout.state = TIMEOUT_ACTIVE; + the_timeout.handler = handler; + the_timeout.param = param; #ifdef SOLARIS saved_handler = signal(SIGALRM, alarm_handler); From dddb30f504d8b993e541f6b581529c6ea3d54218 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Sat, 23 Sep 2023 10:57:40 -0700 Subject: [PATCH 13/15] Undo unncessary change. --- src/utils/timeout.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/utils/timeout.c b/src/utils/timeout.c index 3a5812b3a..80518f5bd 100644 --- a/src/utils/timeout.c +++ b/src/utils/timeout.c @@ -262,7 +262,7 @@ timeout_t *init_timeout(void) { */ void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) { assert(timeout == &the_timeout); - assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL); + assert(delay > 0 && the_timeout.state == TIMEOUT_READY && handler != NULL); the_timeout.state = TIMEOUT_ACTIVE; the_timeout.handler = handler; the_timeout.param = param; From d704c3acd2a063825809a02f42a03f8308eb6d24 Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Sat, 23 Sep 2023 11:13:12 -0700 Subject: [PATCH 14/15] Fix typo. --- src/mt/yices_locks_posix.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mt/yices_locks_posix.c b/src/mt/yices_locks_posix.c index a84f00f84..4ab6e1665 100644 --- a/src/mt/yices_locks_posix.c +++ b/src/mt/yices_locks_posix.c @@ -53,7 +53,7 @@ int32_t create_yices_lock(yices_lock_t* lock){ "create_yices_lock: pthread_mutex_init"); #ifndef NDEBUG - check_thread_api(pthread_mutexattr_destroy(mattr) + check_thread_api(pthread_mutexattr_destroy(mattr)); #endif return 0; From 88e46491182753b7023c87e4de55bc821f3be9ba Mon Sep 17 00:00:00 2001 From: Mark Mitchell Date: Sat, 23 Sep 2023 11:21:54 -0700 Subject: [PATCH 15/15] Fix typo. --- src/mt/yices_locks_posix.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/mt/yices_locks_posix.c b/src/mt/yices_locks_posix.c index 4ab6e1665..821b809df 100644 --- a/src/mt/yices_locks_posix.c +++ b/src/mt/yices_locks_posix.c @@ -53,7 +53,8 @@ int32_t create_yices_lock(yices_lock_t* lock){ "create_yices_lock: pthread_mutex_init"); #ifndef NDEBUG - check_thread_api(pthread_mutexattr_destroy(mattr)); + check_thread_api(pthread_mutexattr_destroy(mattr), + "create_yices_lock: pthread_mutexattr_destroy"); #endif return 0;