Segmentation Fault (Heap-Use-After-Free) in Z3 when Parsing Invalid SMT2 Rule

[chinggg]

Summary

A segmentation fault (heap-use-after-free when built with AddressSanitizer) occurs in the latest Z3 release shipped on Arch Linux (4.13.4) and the latest master branch today 8df45b4 when processing a minimal two-line SMT2 file. This issue is reproducible with a simple command-line invocation of Z3.

Steps to Reproduce

1. Create a poc file with the following content:

(rule 80 (x))
(rule)

2. Reproduce on latest Z3 release shipped on Arch Linux (4.13.4)

[Archlinux] $ z3 --version
Z3 version 4.13.4 - 64 bit - build hashcode 6f24123f0c9d1d8bd84dec275c5c7aea939a19fe

[Archlinux] $ z3 poc    
(error "line 1 column 10: invalid command argument, symbol expected")
zsh: segmentation fault (core dumped)  z3 poc

3. Reproduce on latest master branch today 8df45b4

• Build Z3 from source with AddressSanitizer enabled

CXXFLAGS="-fsanitize=address" cmake -G Ninja -B buildasan -DCMAKE_BUILD_TYPE=Debug
ninja -C buildasan

• Run Z3 on the input file:

[Ubuntu22.04] $ ./buildasan/z3 poc 
(error "line 1 column 10: invalid command argument, symbol expected")
=================================================================
==39835==ERROR: AddressSanitizer: heap-use-after-free on address 0x60400000cd98 at pc 0x55efb113acb0 bp 0x7fff77f08a40 sp 0x7fff77f08a30
READ of size 4 at 0x60400000cd98 thread T0
    #0 0x55efb113acaf in ast::inc_ref() /clever/z3/src/ast/ast.h:491
    #1 0x55efb113aef2 in ast_manager::inc_ref(ast*) /clever/z3/src/ast/ast.h:1658
    #2 0x55efb116d278 in ref_manager_wrapper<expr, ast_manager>::inc_ref(expr*) /clever/z3/src/util/ref_vector.h:226
    #3 0x55efb116c10a in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::inc_ref(expr*) /clever/z3/src/util/ref_vector.h:36
    #4 0x55efb116a490 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::push_back(expr*) /clever/z3/src/util/ref_vector.h:105
    #5 0x55efb3d5bca0 in datalog::context::add_rule(expr*, symbol const&, unsigned int) /clever/z3/src/muz/base/dl_context.cpp:460
    #6 0x55efb43765b5 in dl_context::add_rule(expr*, symbol const&, unsigned int) /clever/z3/src/muz/fp/dl_cmds.cpp:117
    #7 0x55efb4377281 in dl_rule_cmd::execute(cmd_context&) /clever/z3/src/muz/fp/dl_cmds.cpp:202
    #8 0x55efb25198d7 in smt2::parser::parse_ext_cmd(int, int) /clever/z3/src/parsers/smt2/smt2parser.cpp:2930
    #9 0x55efb251a1aa in smt2::parser::parse_cmd() /clever/z3/src/parsers/smt2/smt2parser.cpp:3040
    #10 0x55efb251bd7d in smt2::parser::operator()() /clever/z3/src/parsers/smt2/smt2parser.cpp:3191
    #11 0x55efb24f04ca in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /clever/z3/src/parsers/smt2/smt2parser.cpp:3242
    #12 0x55efb462b697 in read_smtlib2_commands(char const*) /clever/z3/src/shell/smtlib_frontend.cpp:182
    #13 0x55efb462627a in main /clever/z3/src/shell/main.cpp:395
    #14 0x7fde9a5c0d8f  (/lib/x86_64-linux-gnu/libc.so.6+0x29d8f)
    #15 0x7fde9a5c0e3f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x29e3f)
    #16 0x55efb0b7bbc4 in _start (/clever/z3/buildasan_8df45b4/z3+0x812bc4)