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

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

Closed
chinggg opened this issue Mar 6, 2025 · 0 comments
Closed

Comments

@chinggg
Copy link

chinggg commented Mar 6, 2025

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)
  1. 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
  1. 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)
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