search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

Segfault when parsing a bad SMT2-Lib syntax #450

Closed JonathanSalwan closed 8 years ago

JonathanSalwan commented 8 years ago

Below the reduced PoC.

(set-logic QF_AUFBV)

(assert
  (=
    ; good syntax -> (bvslt (_ bv1 8) (_ bv2 8))
    (bvslt (_ bv1 8))
    (_ bv3 8)
  )
)

(check-sat)
(get-model)

Z3 segfaults when parsing the bvslt function which should contain at least two operands (here, only one is given).

$ z3 -smt2 poc.smt2
[2]    6118 segmentation fault  z3 -smt2 poc.smt2

According to GDB, the segfault seems to occur in the get_sort() function.

$ gdb z3
gdb-peda$ r -smt2 poc.smt2
Starting program: /usr/bin/z3 -smt2 poc.smt2
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib64/libthread_db.so.1".
Program received signal SIGSEGV, Segmentation fault.
[----------------------------------registers-----------------------------------]
RAX: 0x1375130 --> 0xd21420 (<_ZN14bv_decl_plugin11set_managerEP11ast_manageri>:        push   r15)
RBX: 0x17 
RCX: 0x0 
RDX: 0x0 
RSI: 0x17 
RDI: 0x1 
RBP: 0x13b1488 --> 0x1375130 --> 0xd21420 (<_ZN14bv_decl_plugin11set_managerEP11ast_manageri>:  push   r15)
RSP: 0x7fffffffc6f8 --> 0xd23f50 (<_ZN14bv_decl_plugin12mk_func_declEijPK9parameterjPKP4exprP4sort+160>:        mov    rax,QWORD PTR [rax+0x18])
RIP: 0xd055c0 (<_Z8get_sortPK4expr>:    cmp    WORD PTR [rdi+0x4],0x1)
R8 : 0x2 
R9 : 0x7fffffffc7a0 --> 0x1 
R10: 0x17 
R11: 0x7ffff6d46300 --> 0xfffda2b0fffd9fdf 
R12: 0x2 
R13: 0x0 
R14: 0x0 
R15: 0x7fffffffc7a0 --> 0x1
EFLAGS: 0x10202 (carry parity adjust zero sign trap INTERRUPT direction overflow)
[-------------------------------------code-------------------------------------]
   0xd055a8 <_ZN10quantifierC2EbjPKP4sortPK6symbolP4expriRS5_S9_jPKS8_jSB_+408>:        lea    rax,[r9+rsi*8+0x20]
   0xd055ad <_ZN10quantifierC2EbjPKP4sortPK6symbolP4expriRS5_S9_jPKS8_jSB_+413>:        jmp    0xd05498 <_ZN10quantifierC2EbjPKP4sortPK6symbolP4expriRS5_S9_jPKS8_jSB_+136>
   0xd055b2:    data16 data16 data16 data16 nop WORD PTR cs:[rax+rax*1+0x0]
=> 0xd055c0 <_Z8get_sortPK4expr>:       cmp    WORD PTR [rdi+0x4],0x1
   0xd055c5 <_Z8get_sortPK4expr+5>:     je     0xd055d4 <_Z8get_sortPK4expr+20>
   0xd055c7 <_Z8get_sortPK4expr+7>:     jb     0xd055e0 <_Z8get_sortPK4expr+32>
   0xd055c9 <_Z8get_sortPK4expr+9>:     mov    rdi,QWORD PTR [rdi+0x18]
   0xd055cd <_Z8get_sortPK4expr+13>:    cmp    WORD PTR [rdi+0x4],0x1
[------------------------------------stack-------------------------------------]
0000| 0x7fffffffc6f8 --> 0xd23f50 (<_ZN14bv_decl_plugin12mk_func_declEijPK9parameterjPKP4exprP4sort+160>:       mov    rax,QWORD PTR [rax+0x18])
0008| 0x7fffffffc700 --> 0x3 
0016| 0x7fffffffc708 --> 0x20 (' ')
0024| 0x7fffffffc710 --> 0x0 
0032| 0x7fffffffc718 --> 0x0 
0040| 0x7fffffffc720 --> 0x0 
0048| 0x7fffffffc728 --> 0x139dc58 --> 0x0 
0056| 0x7fffffffc730 --> 0x2 
[------------------------------------------------------------------------------]
Legend: code, data, rodata, value
Stopped reason: SIGSEGV
0x0000000000d055c0 in get_sort(expr const*) ()
gdb-peda$

This segfault also occurs with bvule, bvsle, bvuge, bvsge, bvult, bvslt, bvugt and bvsgt.

Bellow the backtrace:

gdb-peda$ bt
#0  0x0000000000d055c0 in get_sort(expr const*) ()
#1  0x0000000000d23f50 in bv_decl_plugin::mk_func_decl(int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ()
#2  0x0000000000d10ea3 in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) [clone .constprop.215] ()
#3  0x0000000000d12d9a in ast_manager::mk_app(int, int, expr*, expr*) ()
#4  0x0000000000cad6d2 in bv_rewriter::mk_slt(expr*, expr*, obj_ref<expr, ast_manager>&) ()
#5  0x0000000000cba3e2 in bv_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ()
#6  0x0000000000cd7215 in th_rewriter_cfg::reduce_app(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ()
#7  0x0000000000cdb73d in void rewriter_tpl<th_rewriter_cfg>::process_app<false>(app*, rewriter_core::frame&) ()
#8  0x0000000000cdbb3d in void rewriter_tpl<th_rewriter_cfg>::resume_core<false>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ()
#9  0x0000000000bc9064 in simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
#10 0x0000000000c5558e in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
#11 0x0000000000c59055 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&)
    ()
#12 0x0000000000c59055 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&)
    ()
#13 0x0000000000c600a0 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
#14 0x0000000000c60501 in check_sat(tactic&, ref<goal>&, ref<model>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::string&) ()
#15 0x0000000000b0c0e5 in tactic2solver::check_sat_core(unsigned int, expr* const*) ()
#16 0x0000000000b0a09c in solver_na2as::check_sat(unsigned int, expr* const*) ()
#17 0x0000000000b0b0e3 in combined_solver::check_sat(unsigned int, expr* const*) ()
#18 0x0000000000a5daa0 in cmd_context::check_sat(unsigned int, expr* const*) ()
#19 0x0000000000a384ae in smt2::parser::parse_check_sat() ()
#20 0x0000000000a405e0 in smt2::parser::operator()() ()
#21 0x0000000000a30a1b in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&) ()
#22 0x0000000000418ecd in read_smtlib2_commands(char const*) ()
#23 0x000000000040dce3 in main ()
#24 0x00007ffff6bfc7b0 in __libc_start_main () from /lib64/libc.so.6
#25 0x0000000000415c07 in _start ()

Hope these information may be useful :).

JonathanSalwan commented 8 years ago

This bug was in Z3 version 4.4.0. After a git pull on the master branch 4.4.2 this bug seems to be fixed.

$ z3 -smt2 ./poc.smt2
(error "line 6 column 21: declared arity mismatches supplied arity")
sat
(model 
)

Sorry,