Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Null pointer dereference in internal_symbol_table::get_str(char const*) #1267

Closed
fumfel opened this Issue Sep 23, 2017 · 5 comments

Comments

Projects
None yet
2 participants
@fumfel
Copy link

fumfel commented Sep 23, 2017

Git HEAD: 1d6f53c

Faulting input

Command: z3 -smt2 z3_nullptr

ASAN:

==2940==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x7f924641cd0e bp 0x629000000290 sp 0x7ffca9173fd0 T0)
==2940==The signal is caused by a READ memory access.
==2940==Hint: address points to the zero page.
    #0 0x7f924641cd0d in int __kmp_acquire_queuing_lock_timed_template<false>(kmp_queuing_lock*, int) (/usr/local/lib/libomp.so+0x63d0d)
    #1 0x7f924641cce5 in __kmp_acquire_queuing_lock (/usr/local/lib/libomp.so+0x63ce5)
    #2 0x7f92463dc9a8 in __kmpc_critical_with_hint (/usr/local/lib/libomp.so+0x239a8)
    #3 0x67cac50 in internal_symbol_table::get_str(char const*) XYZ/z3/build/../src/util/symbol.cpp:38:17
    #4 0x67c8e91 in symbol::symbol(char const*) XYZ/z3/build/../src/util/symbol.cpp:80:34
    #5 0x580f1be in bv_util::bv_util(ast_manager&) XYZ/z3/build/../src/ast/bv_decl_plugin.cpp:844:35
    #6 0x58afb48 in datalog::dl_decl_util::dl_decl_util(ast_manager&) XYZ/z3/build/../src/ast/dl_decl_plugin.cpp:649:9
    #7 0x5375d24 in dl_rewriter::dl_rewriter(ast_manager&) XYZ/z3/build/../src/ast/rewriter/dl_rewriter.h:28:34
    #8 0x5375d24 in th_rewriter_cfg::th_rewriter_cfg(ast_manager&, params_ref const&) XYZ/z3/build/../src/ast/rewriter/th_rewriter.cpp:675
    #9 0x5367b95 in th_rewriter::imp::imp(ast_manager&, params_ref const&) XYZ/z3/build/../src/ast/rewriter/th_rewriter.cpp:714:9
    #10 0x5367b95 in th_rewriter::th_rewriter(ast_manager&, params_ref const&) XYZ/z3/build/../src/ast/rewriter/th_rewriter.cpp:727
    #11 0x4a2b0fb in simplify_tactic::imp::imp(ast_manager&, params_ref const&) XYZ/z3/build/../src/tactic/core/simplify_tactic.cpp:30:9
    #12 0x4a2b0fb in simplify_tactic::simplify_tactic(ast_manager&, params_ref const&) XYZ/z3/build/../src/tactic/core/simplify_tactic.cpp:79
    #13 0x4a2b0fb in mk_simplify_tactic(ast_manager&, params_ref const&) XYZ/z3/build/../src/tactic/core/simplify_tactic.cpp:124
    #14 0x45f2920 in mk_purify_arith_tactic(ast_manager&, params_ref const&) XYZ/z3/build/../src/tactic/arith/purify_arith_tactic.cpp:870:21
    #15 0x451c84b in mk_qfnra_nlsat_tactic(ast_manager&, params_ref const&) XYZ/z3/build/../src/nlsat/tactic/qfnra_nlsat_tactic.cpp:47:43
    #16 0xa4be94 in mk_qfnra_tactic(ast_manager&, params_ref const&) XYZ/z3/build/../src/tactic/smtlogics/qfnra_tactic.cpp:45:37
    #17 0xa2fae2 in mk_qffp_tactic(ast_manager&, params_ref const&) XYZ/z3/build/../src/tactic/fpa/qffp_tactic.cpp:100:38
    #18 0x9f5f62 in mk_default_tactic(ast_manager&, params_ref const&) XYZ/z3/build/../src/tactic/portfolio/default_tactic.cpp:46:66
    #19 0x9f209c in mk_tactic_for_logic(ast_manager&, params_ref const&, symbol const&) XYZ/z3/build/../src/tactic/portfolio/smt_strategic_solver.cpp:101:16
    #20 0x9f403a in smt_strategic_solver_factory::operator()(ast_manager&, params_ref const&, bool, bool, bool, symbol const&) XYZ/z3/build/../src/tactic/portfolio/smt_strategic_solver.cpp:134:22
    #21 0x3f6fee5 in cmd_context::mk_solver() XYZ/z3/build/../src/cmd_context/cmd_context.cpp:1787:20
    #22 0x3f6f0dd in cmd_context::init_manager_core(bool) XYZ/z3/build/../src/cmd_context/cmd_context.cpp:734:9
    #23 0x3f705f0 in cmd_context::init_manager() XYZ/z3/build/../src/cmd_context/cmd_context.cpp
    #24 0x3f6f9d1 in cmd_context::m() const XYZ/z3/build/../src/cmd_context/cmd_context.h:355:63
    #25 0x3f6f9d1 in cmd_context::mk_solver() XYZ/z3/build/../src/cmd_context/cmd_context.cpp:1782
    #26 0x3fa0833 in cmd_context::set_solver_factory(solver_factory*) XYZ/z3/build/../src/cmd_context/cmd_context.cpp:1799:9
    #27 0x9d7e52 in smtlib::solver::solve_benchmark(smtlib::benchmark&) XYZ/z3/build/../src/parsers/smt/smtlib_solver.cpp:89:16
    #28 0x9d7648 in smtlib::solver::solve_smt(char const*) XYZ/z3/build/../src/parsers/smt/smtlib_solver.cpp:64:9
    #29 0x5313fa in read_smtlib_file(char const*) XYZ/z3/build/../src/shell/smtlib_frontend.cpp:84:17
    #30 0x517eb8 in main XYZ/z3/build/../src/shell/main.cpp:354:28
    #31 0x7f9245df982f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #32 0x43f228 in _start (/usr/bin/z3+0x43f228)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/usr/local/lib/libomp.so+0x63d0d) in int __kmp_acquire_queuing_lock_timed_template<false>(kmp_queuing_lock*, int)
==2940==ABORTING
@NikolajBjorner

This comment has been minimized.

Copy link
Contributor

NikolajBjorner commented Sep 23, 2017

your input looks garbled to me

NikolajBjorner added a commit that referenced this issue Sep 24, 2017

check for eof, based on testing garbled repro from #1267
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner

This comment has been minimized.

Copy link
Contributor

NikolajBjorner commented Sep 24, 2017

Could you check your uploaded file?
The file is probably not what you used, but it exposed one issue in the scanner that was fixed.

@fumfel

This comment has been minimized.

Copy link
Author

fumfel commented Sep 25, 2017

@NikolajBjorner

This comment has been minimized.

Copy link
Contributor

NikolajBjorner commented Sep 25, 2017

Didn't work. Can you just put it in this conversation? The file seems fairly small.

@NikolajBjorner

This comment has been minimized.

Copy link
Contributor

NikolajBjorner commented Oct 2, 2017

After the fix for the garbled file the crash doesn't reproduce.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.