search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

(HORN, rlimit=610, rewriter.elim_and) Segmentation fault at ../src/model/model.cpp:520 #4429

Closed muchang closed 4 years ago

muchang commented 4 years ago

Hi, For this case, Z3 throws out a segmentation fault:

[622] % z3debug small.smt2
Segmentation fault
[623] % z3release small.smt2
Segmentation fault
[624] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==7796==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x55d5d8746f50 bp 0x7ffd196cb5d0 sp 0x7ffd196cb530 T0)
==7796==The signal is caused by a READ memory access.
==7796==Hint: address points to the zero page.
  #0 0x55d5d8746f4f in model::operator()(expr*) ../src/model/model.cpp:520
  #1 0x55d5d8746f4f in model::is_true(expr*) ../src/model/model.cpp:538
  #2 0x55d5d5f17d33 in spacer::context::handle_unknown(spacer::pob&, datalog::rule const*, model&) ../src/muz/spacer/spacer_context.cpp:3427
  #3 0x55d5d5f522ea in spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) ../src/muz/spacer/spacer_context.cpp:3494
  #4 0x55d5d5f56272 in spacer::context::check_reachability() ../src/muz/spacer/spacer_context.cpp:3204
  #5 0x55d5d5f5e6de in spacer::context::solve_core(unsigned int) ../src/muz/spacer/spacer_context.cpp:3023
  #6 0x55d5d5f5f58c in spacer::context::solve(unsigned int) ../src/muz/spacer/spacer_context.cpp:2720
  #7 0x55d5d5ef7538 in spacer::dl_interface::query(expr*) ../src/muz/spacer/spacer_dl_interface.cpp:167
  #8 0x55d5d6724e9d in datalog::context::query(expr*) ../src/muz/base/dl_context.cpp:880
  #9 0x55d5d5e316ed in horn_tactic::imp::verify(expr*, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&) ../src/muz/fp/horn_tactic.cpp:255
  #10 0x55d5d5e316ed in horn_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:241
  #11 0x55d5d86756f8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:937
  #12 0x55d5d863fe4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
  #13 0x55d5d864214d in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
  #14 0x55d5d84ad9c8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #15 0x55d5d84ccb67 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #16 0x55d5d84e0394 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #17 0x55d5d84bb761 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #18 0x55d5d8436170 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
  #19 0x55d5d83518b3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2595
  #20 0x55d5d83518b3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2937
  #21 0x55d5d83518b3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3129
  #22 0x55d5d8308e95 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3178
  #23 0x55d5d59b6ad6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:90
  #24 0x55d5d596f2ee in main ../src/shell/main.cpp:352
  #25 0x7f98652d2b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #26 0x55d5d59835f9 in _start (/local/suz-local/software/z3san/build-05212020212726-18bb90f/z3+0x2135f9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/model/model.cpp:520 in model::operator()(expr*)
==7796==ABORTING
[625] % 
[625] % cat small.smt2
(set-logic HORN)
(set-option :rlimit 610)
(set-option :rewriter.elim_and true)
(assert (forall ((a Int) (b Int)) (or (< a (mod b 2)) (forall ((c Int)) (> c b a)))))
(check-sat)
[626] %

OS: Ubuntu 18.04 Commit: 18bb90f

muchang commented 4 years ago

Here is another case which is simpler:

[544] % z3debug rlimit=100 small.smt2
Segmentation fault
[545] % z3release rlimit=100 small.smt2
Segmentation fault
[546] % z3san rlimit=100 small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==11151==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x563dea58bf50 bp 0x7ffe86c99950 sp 0x7ffe86c998b0 T0)
==11151==The signal is caused by a READ memory access.
==11151==Hint: address points to the zero page.
  #0 0x563dea58bf4f in model::operator()(expr*) ../src/model/model.cpp:520
  #1 0x563dea58bf4f in model::is_true(expr*) ../src/model/model.cpp:538
  #2 0x563de7d5cd33 in spacer::context::handle_unknown(spacer::pob&, datalog::rule const*, model&) ../src/muz/spacer/spacer_context.cpp:3427
  #3 0x563de7d972ea in spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) ../src/muz/spacer/spacer_context.cpp:3494
  #4 0x563de7d9b272 in spacer::context::check_reachability() ../src/muz/spacer/spacer_context.cpp:3204
  #5 0x563de7da36de in spacer::context::solve_core(unsigned int) ../src/muz/spacer/spacer_context.cpp:3023
  #6 0x563de7da458c in spacer::context::solve(unsigned int) ../src/muz/spacer/spacer_context.cpp:2720
  #7 0x563de7d3c538 in spacer::dl_interface::query(expr*) ../src/muz/spacer/spacer_dl_interface.cpp:167
  #8 0x563de8569e9d in datalog::context::query(expr*) ../src/muz/base/dl_context.cpp:880
  #9 0x563de7c766ed in horn_tactic::imp::verify(expr*, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&) ../src/muz/fp/horn_tactic.cpp:255
  #10 0x563de7c766ed in horn_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:241
  #11 0x563dea4ba6f8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:937
  #12 0x563dea484e4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
  #13 0x563dea48714d in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
  #14 0x563dea2f29c8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #15 0x563dea311b67 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #16 0x563dea325394 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #17 0x563dea300761 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #18 0x563dea27b170 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
  #19 0x563dea1968b3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2595
  #20 0x563dea1968b3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2937
  #21 0x563dea1968b3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3129
  #22 0x563dea14de95 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3178
  #23 0x563de77fbad6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:90
  #24 0x563de77b42ee in main ../src/shell/main.cpp:352
  #25 0x7f06f3848b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #26 0x563de77c85f9 in _start (/local/suz-local/software/z3san/build-05212020212726-18bb90f/z3+0x2135f9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/model/model.cpp:520 in model::operator()(expr*)
==11151==ABORTING
[547] % 
[547] % cat small.smt2
(set-logic HORN)
(assert (forall ((x Int)) (distinct x (- 1))))
(check-sat)
[548] %
muchang commented 4 years ago

Here is another case for QF_UFLIA formula:

[608] % z3debug small.smt2
Segmentation fault
[609] % z3release small.smt2
Segmentation fault
[610] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==32124==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x55cb11aa5f50 bp 0x7ffe3ed665e0 sp 0x7ffe3ed66540 T0)
==32124==The signal is caused by a READ memory access.
==32124==Hint: address points to the zero page.
  #0 0x55cb11aa5f4f in model::operator()(expr*) ../src/model/model.cpp:520
  #1 0x55cb11aa5f4f in model::is_true(expr*) ../src/model/model.cpp:538
  #2 0x55cb0f276d33 in spacer::context::handle_unknown(spacer::pob&, datalog::rule const*, model&) ../src/muz/spacer/spacer_context.cpp:3427
  #3 0x55cb0f2b12ea in spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) ../src/muz/spacer/spacer_context.cpp:3494
  #4 0x55cb0f2b2ca9 in spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) ../src/muz/spacer/spacer_context.cpp:3667
  #5 0x55cb0f2b2ca9 in spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) ../src/muz/spacer/spacer_context.cpp:3667
  #6 0x55cb0f2b5272 in spacer::context::check_reachability() ../src/muz/spacer/spacer_context.cpp:3204
  #7 0x55cb0f2bd6de in spacer::context::solve_core(unsigned int) ../src/muz/spacer/spacer_context.cpp:3023
  #8 0x55cb0f2be58c in spacer::context::solve(unsigned int) ../src/muz/spacer/spacer_context.cpp:2720
  #9 0x55cb0f256538 in spacer::dl_interface::query(expr*) ../src/muz/spacer/spacer_dl_interface.cpp:167
  #10 0x55cb0fa83e9d in datalog::context::query(expr*) ../src/muz/base/dl_context.cpp:880
  #11 0x55cb0f1906ed in horn_tactic::imp::verify(expr*, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&) ../src/muz/fp/horn_tactic.cpp:255
  #12 0x55cb0f1906ed in horn_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:241
  #13 0x55cb119d46f8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:937
  #14 0x55cb1199ee4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
  #15 0x55cb119a114d in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
  #16 0x55cb1180c9c8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #17 0x55cb1182bb67 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #18 0x55cb1183f394 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #19 0x55cb1181a761 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #20 0x55cb11795170 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
  #21 0x55cb116b08b3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2595
  #22 0x55cb116b08b3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2937
  #23 0x55cb116b08b3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3129
  #24 0x55cb11667e95 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3178
  #25 0x55cb0ed15ad6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:90
  #26 0x55cb0ecce2ee in main ../src/shell/main.cpp:352
  #27 0x7f92ca42cb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #28 0x55cb0ece25f9 in _start (/local/suz-local/software/z3san/build-05212020212726-18bb90f/z3+0x2135f9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/model/model.cpp:520 in model::operator()(expr*)
==32124==ABORTING
[611] % 
[611] % cat small.smt2
(set-logic HORN)
(set-option :rlimit 300)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= f g))
(check-sat)
[612] %
agurfinkel commented 4 years ago

@hgvk94

NikolajBjorner commented 4 years ago

I will have to close this one. The set of ways you can make Spacer crash on the cancelation path exceeds the time we can spend on it. It is very simple to generate such bugs so can be revisited if there is a real need for stability under cancelation.

for /L %I in (600,1,1000) do (z3 4429.smt2 rlimit=%I)

hgvk94 commented 4 years ago

This particular issue was fixed by PR https://github.com/Z3Prover/z3/pull/4443. Strange that ghub did not close the issue.