Buffer overflow in sat/sat_clause.cpp

[izbyshev]

Debug build of Z3 (e8141aaa84bb47a927282ce0318686fd12c7b2f9) reports the following assertion failure when given query.txt as input.

ASSERTION VIOLATION
File: ../src/sat/sat_clause.cpp
Line: 149
m_num_segments <= c_max_segments

The stack trace follows.

#0  0x00007f0299cccada in waitpid () from /lib64/libc.so.6
#1  0x00007f0299c548db in do_system () from /lib64/libc.so.6
#2  0x0000000001c9b60a in invoke_gdb () at ../src/util/debug.cpp:100
#3  0x0000000001b41698 in sat::clause_allocator::get_segment (this=0x7fff9528e1c0, ptr=106583908417536)
    at ../src/sat/sat_clause.cpp:149
#4  0x0000000001b417ca in sat::clause_allocator::get_offset (this=0x7fff9528e1c0, ptr=0x60f00000b268)
    at ../src/sat/sat_clause.cpp:159
#5  0x0000000001b02525 in sat::solver::attach_nary_clause (this=0x7fff9528e0a8, c=..., reinit=@0x7fff9528d520: false)
    at ../src/sat/sat_solver.cpp:300
#6  0x0000000001b0223b in sat::solver::mk_nary_clause (this=0x7fff9528e0a8, num_lits=34, lits=0x61e000002490, learned=false)
    at ../src/sat/sat_solver.cpp:286
#7  0x0000000001b01423 in sat::solver::mk_clause_core (this=0x7fff9528e0a8, num_lits=34, lits=0x61e000002490, learned=false)
    at ../src/sat/sat_solver.cpp:206
#8  0x0000000001b00b9e in sat::solver::mk_clause (this=0x7fff9528e0a8, num_lits=34, lits=0x61e000002490)
    at ../src/sat/sat_solver.cpp:156
#9  0x00000000015ee9d3 in goal2sat::imp::mk_clause (this=0x7fff9528db80, num=34, lits=0x61e000002490)
    at ../src/sat/tactic/goal2sat.cpp:102
#10 0x00000000015eff93 in goal2sat::imp::convert_or (this=0x7fff9528db80, t=0x61300002da08, root=false, sign=true)
    at ../src/sat/tactic/goal2sat.cpp:229
#11 0x00000000015f0e78 in goal2sat::imp::convert (this=0x7fff9528db80, t=0x61300002da08, root=false, sign=true)
    at ../src/sat/tactic/goal2sat.cpp:312
#12 0x00000000015f182b in goal2sat::imp::process (this=0x7fff9528db80, n=0x6070003e9b88) at ../src/sat/tactic/goal2sat.cpp:366
#13 0x00000000015f26e7 in goal2sat::imp::operator() (this=0x7fff9528db80, g=...) at ../src/sat/tactic/goal2sat.cpp:429
#14 0x00000000015ed6d2 in goal2sat::operator() (this=0x7fff9528e098, g=..., p=..., t=..., m=..., dep2asm=..., default_external=false)
    at ../src/sat/tactic/goal2sat.cpp:498
#15 0x00000000015eb7f9 in sat_tactic::imp::operator() (this=0x7fff9528e090, g=..., result=..., mc=..., pc=..., core=...)
    at ../src/sat/tactic/sat_tactic.cpp:57
#16 0x00000000015ed177 in sat_tactic::operator() (this=0x60600000aac8, g=..., result=..., mc=..., pc=..., core=...)
    at ../src/sat/tactic/sat_tactic.cpp:192
#17 0x000000000170cc91 in cleanup_tactical::operator() (this=0x6030000033a8, in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactical.cpp:1124
#18 0x000000000170e214 in cond_tactical::operator() (this=0x604000006a98, in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactical.cpp:1255
#19 0x0000000001706144 in and_then_tactical::operator() (this=0x604000006158, in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactical.cpp:140
#20 0x0000000001706144 in and_then_tactical::operator() (this=0x604000006118, in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactical.cpp:140
#21 0x000000000170e17a in cond_tactical::operator() (this=0x6040000060d8, in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactical.cpp:1253
#22 0x000000000170e214 in cond_tactical::operator() (this=0x604000005fd8, in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactical.cpp:1255
#23 0x0000000001706144 in and_then_tactical::operator() (this=0x604000005f98, in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactical.cpp:140
#24 0x000000000170aa87 in unary_tactical::operator() (this=0x604000005f58, in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactical.cpp:915
#25 0x0000000001715cce in exec (t=..., in=..., result=..., mc=..., pc=..., core=...) at ../src/tactic/tactic.cpp:167
#26 0x00000000017160cf in check_sat (t=..., g=..., md=..., pr=..., core=..., reason_unknown="unknown")
    at ../src/tactic/tactic.cpp:189
#27 0x000000000149f23e in tactic2solver::check_sat_core (this=0x60d000004218, num_assumptions=0, assumptions=0x0)
    at ../src/solver/tactic2solver.cpp:148
#28 0x000000000149bd0d in solver_na2as::check_sat (this=0x60d000004218, num_assumptions=0, assumptions=0x0)
    at ../src/solver/solver_na2as.cpp:66
#29 0x00000000014a2b8d in combined_solver::check_sat (this=0x60600000a048, num_assumptions=0, assumptions=0x60b0000098f0)
    at ../src/solver/combined_solver.cpp:244
#30 0x00000000013929d8 in cmd_context::check_sat (this=0x7fff95291630, num_assumptions=0, assumptions=0x60b0000098f0)
    at ../src/cmd_context/cmd_context.cpp:1476
#31 0x00000000013490a8 in smt2::parser::parse_check_sat (this=0x7fff95290b10) at ../src/parsers/smt2/smt2parser.cpp:2176
#32 0x000000000134cf17 in smt2::parser::parse_cmd (this=0x7fff95290b10) at ../src/parsers/smt2/smt2parser.cpp:2506
#33 0x000000000134e409 in smt2::parser::operator() (this=0x7fff95290b10) at ../src/parsers/smt2/smt2parser.cpp:2661
#34 0x00000000013327c3 in parse_smt2_commands (ctx=..., is=..., interactive=false, ps=...) at ../src/parsers/smt2/smt2parser.cpp:2710
#35 0x0000000000433d29 in read_smtlib2_commands (file_name=0x7fff95293659 "../heap-buf-overflow.in")
    at ../src/shell/smtlib_frontend.cpp:127
#36 0x00000000004130a0 in main (argc=2, argv=0x7fff95291ab8) at ../src/shell/main.cpp:353

I know that at least 4.4.1 release has this issue on the same input, but it seems there was no assertion back then, so it was caught by address sanitizer as "heap-buffer-overflow" instead.

[delcypher]

@izbyshev The assert was added by me in 6c966bba59677589fbaf76d6c29a8aceab70eaa6 . There was a bug in the bounds check which meant out of bounds writes would happen.

Unfortunately I don't think usable ASan builds of Z3 on x86_64 are possible yet. I first reported the problem in #436 (sorry the issue is rather long because it took me rather a long time to find the underlying issue).

See https://github.com/Z3Prover/z3/issues/436#issuecomment-184713859

for an explanation of the issue.

@wintersteiger any progress on a fix?

[NikolajBjorner]

@delcypher, @izbyshev. I have somewhat limited ability to test this fix fully. Therefore, so far it is a pull request. If you get any chance to try it out, it will be appreciated.

[izbyshev]

@delcypher Thank you for your response! Sorry that I didn't mention that my debug build was with ASan. I've checked that a normal debug build doesn't fail on my test. @NikolajBjorner Thank you for the patch! I'll have a chance to test it tomorrow, but I've added several comments.

[izbyshev]

I confirm that #722 fixes debug+asan build on my tests as well. Thank you very much!

[izbyshev]

After moving to larger tests, I've found a problem in #722. When clause_allocator::del_clause() is called, mapping for cls->id() is not removed from m_last_seg_id2cls, so a stale pointer is reused when get_clause() is called with corresponding offset. I've checked that adding m_last_seg_id2cls.remove(cls->id()); to del_clause() fixed the problem.

[wintersteiger]

Sweet, thanks for the quick test, report, and fix! That was indeed a blatant omission on my part, I added that to the PR now.

[NikolajBjorner]

PR has been integrated.