baierd
commented
4 years ago The first problem is not reproduceable for me on the current CPAchecker version. It was in the version from 2 weeks ago, so either JavaSMT version 2.6.0 changed something (We didn't change the Mathsat version in that release) or CPAchecker changed something in the last ~12 days. I extracted the query from that problem and can't reproduce a crash in Mathsat itself (current release version) no matter how often i let it run.
The third problem is not reproduceable for me either in the CPAchecker, but this may be fixed as it was reported earlier this year.
The issue stated above for this has some SMT querys that are interesting though!
The formula is UNSAT per definition, so checking the model afterwards results in no model.
Creating a model-iter with msat_create_model_iterator() results in an error as it should.
(I checked this with native code. Calling msat_create_model_iterator() after the UNSAT fails a subsequent assert of the return value of the msat_create_model_iterator() call. It is possible that that was/is a problem with our code that we don't check properly that no model is checked after UNSAT or that we don't check the return value of msat_create_model_iterator() resulting in calling a subsequent method with a null pointer.)
The second problem persists and i could recreate the crash in Mathsat. Program below:
//Example for failing model iterator in mathsat5
//Most of this code is copied from the example on the webpage and edited
/*
* to compile: gcc example_model_iterator.c -I${MSAT_DIR}/include -L${MSAT_DIR}/lib -lmathsat -lgmpxx -lgmp -lstdc++ -o example_model_iterator
*/
#include <stdio.h>
#include <assert.h>
#include <stdlib.h>
#include "mathsat.h"
// Taken directly from example on the mathsat webpage
static void print_model(msat_env env)
{
msat_model_iterator iter = msat_create_model_iterator(env);
assert(!MSAT_ERROR_MODEL_ITERATOR(iter));
printf("Model:\n");
while (msat_model_iterator_has_next(iter)) {
msat_term t, v;
char *s;
msat_model_iterator_next(iter, &t, &v); // As far as i understand this causes the crash!
s = msat_term_repr(t);
assert(s);
printf(" %s = ", s);
msat_free(s);
s = msat_term_repr(v);
assert(s);
printf("%s\n", s);
msat_free(s);
}
msat_destroy_model_iterator(iter);
}
static void modelCrashExample()
{
msat_config cfg;
msat_env env;
msat_result status;
int res;
printf("\nExample start\n");
cfg = msat_create_config();
/* enable model generation */
msat_set_option(cfg, "model_generation", "true");
env = msat_create_env(cfg);
assert(!MSAT_ERROR_ENV(env));
// Parse SMT-LIB2 file that will cause a crash in the model later
FILE *fp = fopen("mathsat_model_iter_segfault", "r");
if (fp == NULL) {
fprintf(stderr, "Can't open input file in example!\n");
exit(1);
}
res = msat_push_backtrack_point(env);
assert(res == 0);
msat_term parsed_formula = msat_from_smtlib2_file(env, fp);
assert(!MSAT_ERROR_TERM(parsed_formula));
res = msat_assert_formula(env, parsed_formula);
assert(res == 0);
printf("Parsed, now check SAT\n");
status = msat_solve(env);
assert(status == MSAT_SAT);
printf("SAT, now get model\n");
/* display the model. Will cause a Segmentation fault */
print_model(env);
msat_destroy_env(env);
msat_destroy_config(cfg);
printf("\nEnd of example\n");
}
int main()
{
printf("This example illustrates a SegFault when using the model iterator\n");
modelCrashExample();
return 0;
}The file that is getting parsed: (More then likely you can delete the options! I just let them be as that's the exact dump of the problem in the CPAchecker. I just commented out the push as it would crash and the sat check as i wanted to do that manually in the program.)
;; MathSAT API call trace
;; generated on Thu 16 Jul 2020 10:28:14 AM CEST
(set-option :global-declarations true)
(set-option :config "verbosity=0")
(set-option :config "proof_generation=false")
(set-option :config "interpolation=false")
(set-option :config "model_generation=true")
(set-option :config "bool_model_generation=false")
(set-option :config "unsat_core_generation=0")
(set-option :config "random_seed=42")
(set-option :config "debug.dump_theory_lemmas=false")
(set-option :config "debug.solver_enabled=true")
(set-option :config "printer.bv_number_format=0")
(set-option :config "printer.fp_number_format=1")
(set-option :config "printer.defines_prefix=")
(set-option :config "printer.model_as_formula=false")
(set-option :config "preprocessor.toplevel_propagation=true")
(set-option :config "preprocessor.toplevel_propagation_limit=0")
(set-option :config "preprocessor.simplification=23")
(set-option :config "preprocessor.ite_minimization=false")
(set-option :config "preprocessor.ite_minimization_call_limit=150000")
(set-option :config "preprocessor.interpolation_ite_elimination=false")
(set-option :config "preprocessor.partial_nnf_conversion=false")
(set-option :config "preprocessor.full_cnf_conversion=false")
(set-option :config "dpll.restart_strategy=0")
(set-option :config "dpll.restart_initial=200")
(set-option :config "dpll.restart_geometric_factor=1.5")
(set-option :config "dpll.store_tlemmas=false")
(set-option :config "dpll.branching_random_frequency=0.001")
(set-option :config "dpll.branching_initial_phase=0")
(set-option :config "dpll.branching_cache_phase=2")
(set-option :config "dpll.branching_random_invalidate_phase_cache=false")
(set-option :config "dpll.branching_random_ignore_polarity=true")
(set-option :config "dpll.ghost_filtering=true")
(set-option :config "dpll.minimize_model=false")
(set-option :config "dpll.allsat_minimize_model=false")
(set-option :config "dpll.allsat_allow_duplicates=false")
(set-option :config "dpll.pop_btpoint_reset_var_order=true")
(set-option :config "dpll.glucose_var_activity=false")
(set-option :config "dpll.glucose_learnt_minimization=false")
(set-option :config "dpll.interpolation_mode=0")
(set-option :config "dpll.proof_simplification=false")
(set-option :config "dpll.preprocessor.mode=0")
(set-option :config "dpll.preprocessor.clause_size_limit=20")
(set-option :config "dpll.preprocessor.subsumption_size_limit=1000")
(set-option :config "dpll.preprocessor.elimination_grow_limit=0")
(set-option :config "dpll.preprocessor.elimination_phase=1")
(set-option :config "dpll.preprocessor.elimination_recent_vars_only=false")
(set-option :config "dpll.preprocessor.try_reelimination=true")
(set-option :config "theory.eq_propagation=true")
(set-option :config "theory.interface_eq_policy=2")
(set-option :config "theory.pairwise_interface_eq=true")
(set-option :config "theory.interface_eq_batch_size=100")
(set-option :config "theory.pure_literal_filtering=false")
(set-option :config "theory.euf.enabled=true")
(set-option :config "theory.euf.dyn_ack=0")
(set-option :config "theory.euf.dyn_ack_threshold=1")
(set-option :config "theory.euf.dyn_ack_limit=1000")
(set-option :config "theory.la.enabled=true")
(set-option :config "theory.la.split_rat_eq=false")
(set-option :config "theory.la.delay_alien=false")
(set-option :config "theory.la.pivoting_greedy_threshold=0")
(set-option :config "theory.la.lazy_expl_threshold=10")
(set-option :config "theory.la.interpolation_laz_use_floor=true")
(set-option :config "theory.la.pure_equality_filtering=true")
(set-option :config "theory.la.detect_euf_fragment=false")
(set-option :config "theory.la.deduction_enabled=true")
(set-option :config "theory.la.laz_equality_elimination=true")
(set-option :config "theory.la.laz_internal_branch_and_bound=true")
(set-option :config "theory.la.laz_internal_branch_and_bound_limit=1")
(set-option :config "theory.la.laz_cuts_from_proofs_mode=3")
(set-option :config "theory.la.laz_enabled=true")
(set-option :config "theory.la.laz_unit_cube_test=true")
(set-option :config "theory.la.interpolation_mode=0")
(set-option :config "theory.bv.enabled=true")
(set-option :config "theory.bv.div_by_zero_mode=0")
(set-option :config "theory.bv.delay_propagated_eqs=true")
(set-option :config "theory.bv.eager=true")
(set-option :config "theory.bv.bit_blast_mode=1")
(set-option :config "theory.bv.interpolation_mode=0")
(set-option :config "theory.bv.proof_simplification=false")
(set-option :config "theory.bv.lazydpll.restart_strategy=0")
(set-option :config "theory.bv.lazydpll.restart_initial=200")
(set-option :config "theory.bv.lazydpll.restart_geometric_factor=1.5")
(set-option :config "theory.bv.lazydpll.branching_random_frequency=0")
(set-option :config "theory.bv.lazydpll.branching_initial_phase=0")
(set-option :config "theory.bv.lazydpll.branching_cache_phase=2")
(set-option :config "theory.bv.lazydpll.branching_random_invalidate_phase_cache=false")
(set-option :config "theory.bv.lazydpll.branching_random_ignore_polarity=true")
(set-option :config "theory.bv.lazydpll.ghost_filtering=false")
(set-option :config "theory.bv.lazydpll.glucose_var_activity=false")
(set-option :config "theory.bv.lazydpll.glucose_learnt_minimization=false")
(set-option :config "theory.arr.enabled=true")
(set-option :config "theory.arr.mode=0")
(set-option :config "theory.arr.lazy_lemmas=false")
(set-option :config "theory.arr.max_ext_lemmas=0")
(set-option :config "theory.arr.enable_ext_polarity=true")
(set-option :config "theory.arr.enable_ext_arg=true")
(set-option :config "theory.arr.enable_witness=true")
(set-option :config "theory.fp.enabled=true")
(set-option :config "theory.fp.minmax_zero_mode=1")
(set-option :config "theory.fp.mode=1")
(set-option :config "theory.fp.bv_combination_enabled=true")
(set-option :config "theory.fp.bit_blast_mode=2")
(set-option :config "theory.fp.dpll.restart_strategy=3")
(set-option :config "theory.fp.dpll.restart_initial=200")
(set-option :config "theory.fp.dpll.restart_geometric_factor=1.5")
(set-option :config "theory.fp.dpll.branching_random_frequency=0.01")
(set-option :config "theory.fp.dpll.branching_initial_phase=0")
(set-option :config "theory.fp.dpll.branching_cache_phase=1")
(set-option :config "theory.fp.dpll.branching_random_invalidate_phase_cache=false")
(set-option :config "theory.fp.dpll.branching_random_ignore_polarity=true")
(set-option :config "theory.fp.dpll.ghost_filtering=false")
(set-option :config "theory.fp.dpll.glucose_var_activity=true")
(set-option :config "theory.fp.dpll.glucose_learnt_minimization=true")
(set-option :config "theory.fp.acdcl_conflict_generalization=2")
(set-option :config "theory.fp.interpolation_mode=0")
(set-option :config "theory.fp.acdcl_single_propagation_limit=0")
(set-option :config "theory.fp.acdcl_single_generalization_limit=0")
(set-option :config "theory.fp.acdcl_generalization_fair=true")
(set-option :config "theory.na.enabled=true")
(set-option :config "theory.na.permanent_lemmas=true")
(set-option :config "theory.na.eager_lemmas=false")
(set-option :config "theory.na.enable_tangent_lemmas_frontier=true")
(set-option :config "theory.na.tangent_lemmas_rat_approx=0")
(set-option :config "theory.na.tangent_lemmas_limit=0")
(set-option :config "theory.na.tangent_lemmas_enabled=true")
(set-option :config "theory.na.sat_check_enabled=true")
(set-option :config "theory.na.bound_lemmas_enabled=true")
(set-option :config "theory.na.nta_enabled=true")
(set-option :config "theory.na.nta_rat_approx=3")
(set-option :config "theory.na.nta_rat_approx_limit=10")
(set-option :config "theory.na.nta_sat_mode=1")
(set-option :config "theory.na.nta_eager=true")
; (push 1)
(declare-fun __VERIFIER_nondet_int!2@ () Int)
(declare-fun |main::length@3| () Int)
(declare-fun |__ADDRESS_OF___VERIFIER_successful_alloc_*void#1@| () Int)
(declare-fun |main::arr@3| () Int)
(declare-fun |main::a@2| () Int)
(declare-fun *int@1 () (Array Int Int))
(declare-fun *int@2 () (Array Int Int))
(declare-fun |main::__CPAchecker_TMP_0@2| () Int)
(declare-fun |main::a@3| () Int)
(define-fun v8 () Int 0)
(define-fun v13 () Int 4)
(define-fun v14 () Int __VERIFIER_nondet_int!2@)
(define-fun v15 () Int |main::length@3|)
(define-fun v16 () Bool (= v14 v15))
(define-fun v17 () Int 1)
(define-fun v18 () Bool (<= v17 v15))
(define-fun v22 () Bool (and v16 v18))
(define-fun v30 () Int |__ADDRESS_OF___VERIFIER_successful_alloc_*void#1@|)
(define-fun v31 () Bool (<= v30 v8))
(define-fun v32 () Bool (not v31))
(define-fun v33 () Bool ((_ divisible 4) (- v30 v8)))
(define-fun v35 () Int (- 4))
(define-fun v36 () Bool (<= v30 v35))
(define-fun v37 () Bool (not v36))
(define-fun v41 () Int |main::arr@3|)
(define-fun v42 () Bool (= v30 v41))
(define-fun v43 () Bool (and v32 v33))
(define-fun v44 () Bool (and v37 v43))
(define-fun v48 () Bool (= v41 v8))
(define-fun v51 () Bool (not v48))
(define-fun v54 () Int (- 1))
(define-fun v56 () Int |main::a@2|)
(define-fun v57 () Int (* v54 v56))
(define-fun v58 () Int (+ v41 v57))
(define-fun v2300 () (Array Int Int) *int@1)
(define-fun v2304 () (Array Int Int) *int@2)
(define-fun v6120 () Int (select v2300 v56))
(define-fun v6121 () Int (select v2300 v41))
(define-fun v6122 () Bool (= v6120 v6121))
(define-fun v6123 () Bool (not v6122))
(define-fun v6135 () Int |main::__CPAchecker_TMP_0@2|)
(define-fun v6136 () Bool (= v56 v6135))
(define-fun v6139 () Int |main::a@3|)
(define-fun v6140 () Int (* v54 v6139))
(define-fun v6141 () Int (+ v56 v6140))
(define-fun v6142 () Bool (= v6141 v13))
(define-fun v6144 () Int (+ v6120 v6121))
(define-fun v6145 () (Array Int Int) (store v2300 v56 v6144))
(define-fun v6146 () Bool (= v2304 v6145))
(define-fun v18733 () Int (* v13 v15))
(define-fun v18735 () Int (+ v18733 v30))
(define-fun v18736 () Bool (<= v18735 v8))
(define-fun v18737 () Bool (not v18736))
(define-fun v18738 () Bool (and v44 v18737))
(define-fun v18739 () Bool (and v42 v18738))
(define-fun v18740 () Bool (and v22 v18739))
(define-fun v18741 () Bool (and v51 v18740))
(define-fun v18744 () Int (+ v18733 v58))
(define-fun v18745 () Bool (= v18744 v13))
(define-fun v18746 () Bool (and v18741 v18745))
(define-fun v18747 () Bool (and v6123 v18746))
(define-fun v18748 () Bool (and v6146 v18747))
(define-fun v18749 () Bool (and v6136 v18748))
(define-fun v18750 () Bool (and v6142 v18749))
(assert v18750)
; (check-sat)
kfriedberger
There are several smaller bugs in MathSAT5 (version 5.6.3) that need to be reported to the MathSAT5 developers. Most of the bugs regularly appear in CPAchecker benchmarks.
We can set a low priority for interpolation-related problems like
mixed AB termsorie-local interpolantwhich we already handle via an internal whitelist. The main goal of this issue is to detect crashes during normal activities likecheck-satorget-model.The following issues are known in CPAchecker:
check-sat:This Buildbot table contains several cases where MathSAT5 fails with a nondeterministic SegFault.
Issue CPAchecker#651 already mentiones this problem.
The following cmdline for CPAchecker triggers the bug:
scripts/cpa.sh -noout -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -terminationAnalysis -64 -spec test/programs/benchmarks/properties/termination.prp test/programs/benchmarks/termination-15/add_first_alloca.iIssue Cpachecker#680 also mentiones a model problem. Parts of it seem to have been resolved and fixed already. Current status is unknown.
We need to check whether there are more exception in any Buildbot jobs. The reasiest way is to take a look at the result tables and filter for
exceptionorerror. This should be done regularly anyway.The optimal case would be to extract an SMT query from CPAchecker that directly crashes the MathSAT binary release. For this, just enable output (do not use
-benchmarkor -noout) and use-setprop solver.logAllQueries=true` to dump the queries. It might even be possible to shorten the query before reporting them. Further investigation of API calls is difficult, as we need to tell Alberto where to look for a bug. We could try to provide a more elaborate stacktrace, or extract the last solved (or failing) query and implement a small C-programm directly linked against MathSAT5. Any better idea is welcome.