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

Invalid input causes segfault #4120

Closed
wintered opened this issue Apr 27, 2020 · 0 comments
Closed

Invalid input causes segfault #4120

wintered opened this issue Apr 27, 2020 · 0 comments

Comments

@wintered
Copy link

[510] % z3 small.smt2
(error "line 1 column 38: invalid recursive function definition, '(' expected")
Segmentation fault
[511] % z3release small.smt2
(error "line 1 column 38: invalid recursive function definition, '(' expected")
Segmentation fault
[512] % z3san small.smt2
(error "line 1 column 38: invalid recursive function definition, '(' expected")
ASAN:DEADLYSIGNAL
=================================================================
==8280==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x562d164cd8dd bp 0x7ffebfe9e100 sp 0x7ffebfe9e0d0 T0)
==8280==The signal is caused by a READ memory access.
==8280==Hint: address points to the zero page.
  #0 0x562d164cd8dc in ast::get_kind() const ../src/ast/ast.h:504
  #1 0x562d164cd8dc in is_app(ast const*) ../src/ast/ast.h:914
  #2 0x562d164cd8dc in is_ground(expr const*) ../src/ast/ast.h:1378
  #3 0x562d164cd8dc in var_subst::operator()(expr*, unsigned int, expr* const*) ../src/ast/rewriter/var_subst.cpp:28
  #4 0x562d1644373d in recfun_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/recfun_rewriter.cpp:31
  #5 0x562d16416c73 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:225
  #6 0x562d16416c73 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:620
  #7 0x562d1642052a in process_app<false> ../src/ast/rewriter/rewriter_def.h:298
  #8 0x562d1642052a in resume_core<false> ../src/ast/rewriter/rewriter_def.h:769
  #9 0x562d1643057a in main_loop<false> ../src/ast/rewriter/rewriter_def.h:728
  #10 0x562d1643057a in operator() ../src/ast/rewriter/rewriter_def.h:800
  #11 0x562d1643057a in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:860
  #12 0x562d14dca2cb in asserted_formulas::assert_expr(expr*, app*) ../src/smt/asserted_formulas.cpp:158
  #13 0x562d148b5c4c in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:2901
  #14 0x562d148b5c4c in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:2913
  #15 0x562d148b5c4c in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:2908
  #16 0x562d15fe8e5c in solver::assert_expr(expr*) ../src/solver/solver.cpp:210
  #17 0x562d15fe8e5c in solver::assert_expr(expr*) ../src/solver/solver.cpp:210
  #18 0x562d15f1f788 in cmd_context::assert_expr(expr*) ../src/cmd_context/cmd_context.cpp:1319
  #19 0x562d15e81618 in smt2::parser::parse_assert() ../src/parsers/smt2/smt2parser.cpp:2571
  #20 0x562d15e87db7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2926
  #21 0x562d15e87db7 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #22 0x562d15e3f245 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #23 0x562d134d10b6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #24 0x562d134a994e in main ../src/shell/main.cpp:352
  #25 0x7f341d1cfb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #26 0x562d134bd729 in _start (/home/suz/software/z3san/build-04262020232942-a0de244/z3+0x1f7729)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:504 in ast::get_kind() const
==8280==ABORTING
[513] %
[513] % cat small.smt2
(define-funs-rec ((a ((b Int)) Bool)))
(assert (a 0))
(check-sat)
[514] %

OS: Ubuntu 18.04
Commit: a0de244

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant