Skip to content

Invalid input causes segfault #4120

@wintered

Description

@wintered
[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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions