search

Z3Prover / z3

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

Z3 seq solver segfaults on a large test formula with long strings #4894

Closed muchang closed 3 years ago

muchang commented 3 years ago 
[521] % z3release smt.string_solver=z3str3 z3seq-long-strings-segfault.smt2 
unsat
[522] % cvc4 -q z3seq-long-strings-segfault.smt2 
unsat
[523] % 
[523] % z3release small.smt2
Segmentation fault
[524] %

Here is the file: z3seq-long-strings-segfault.smt2.zip

Commit: 7fe8298

rainoftime commented 3 years ago

asan stack is 

ASAN:SIGSEGV
=================================================================
==85707==ERROR: AddressSanitizer: stack-overflow on address 0x7fffa1365ff8 (pc 0x000001b881b8 bp 0x7fffa1366010 sp 0x7fffa1365ff0 T0)
    #0 0x1b881b7 in std::atomic<bool>::operator bool() const /usr/include/c++/5/atomic:80
    #1 0x2765c23 in assertions_enabled() ../src/util/debug.cpp:36
    #2 0x47c9c2 in to_app(ast const*) ../src/ast/ast.h:936
    #3 0x4c6de7 in is_app_of(expr const*, int, int) ../src/ast/ast.h:1370
    #4 0x14d54a4 in seq_util::str::is_unit(expr const*) const ../src/ast/seq_decl_plugin.h:363
    #5 0x14d5c86 in seq_util::str::is_unit(expr const*, expr*&) const ../src/ast/seq_decl_plugin.h:404
    #6 0x1dcee91 in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2202
    #7 0x1dcf08d in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2212
    #8 0x1dcf08d in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2212
    #9 0x1dcf08d in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2212
    #10 0x1dcf08d in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2212
    #11 0x1dcf08d in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2212
    #12 0x1dcf08d in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2212
    #13 0x1dcf08d in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2212
    #14 0x1dcf08d in seq_rewriter::get_head_tail_reversed(expr*, obj_ref<expr, ast_manager>&, obj_ref<expr, 
,,,,,

SUMMARY: AddressSanitizer: stack-overflow /usr/include/c++/5/atomic:80 std::atomic<bool>::operator bool() const
==85707==ABORTING
rainoftime commented 3 years ago

A possibly related instance

(declare-fun i2 () Int)
(declare-fun str0 () String)
(declare-fun str1 () String)
(declare-fun str2 () String)
(declare-fun str4 () String)
(declare-fun str5 () String)
(declare-fun str6 () String)
(declare-fun str7 () String)
(declare-fun str11 () String)
(declare-fun str12 () String)
(declare-fun str13 () String)
(declare-fun str14 () String)
(assert (=> (or (distinct 0) false) (str.in_re (str.++ (str.++ str4 "WPpOAuffBa0tcuvao0MgqAgXKXI7vGDn9e6BGgePvrMmtQ6nxujra8eGqU49WVPR3dmJxjiHGx1np0Wzfn8KJcrjBRG7YMBxY5aDAAWazTwnHnM2s8eLjGQVpjrGyJFFw2Otyf4YGSay7nCe1OWknQJpqMm1W0iEqnabjauDkyzfysxOkyuaF43miA1OmBhFA9t7F5DosG3bRyNioYeOox9JCe0F7xNNa0vRQVoVE8Z1ml2QcYhnL5dKMNsD4H06rl1CFH50InhALR3YacDXkQ7a155LY9xXcGJISXcTMpb8jkvtiV4sbVZDben14dgZeVvCxHRdoAJsGRl68iJW8BBDk0PlEXxIdwpJhl1t8biJyThVs2kjQ03wfpVdilzztQHhp0UhONQ9BKQlriWrc0ncVZVQUXvmq6VazAaNNDqMSGtUakpzWQFrg0R4Wk0rGM2y5meWJlcNg5E5WRr5SA5mIZfHyr0G03MqojOIY4obpqys02S1jIgNzF2fpk6TxAfSeTiRkw01HLLyCilTm2m2AC2hjkNCTF55n2wW7ZARSvMCyxfhFr2HgJYbL2Op5MQTy7CMgT5N1S58FrkpMUxMAQ9bSNt6Ng8NvscNMoMEI6WBWuvzpnSDKTNrB5ZWbQBWV0F0fIvWwyCzxlgTUUuwrwNSN3TFPuY6xOD4c7CEe52fz6x0GLbm6d22tQhnpRBo6wZuPqae50AYekthkOUsOtOtCchA5BOySkXt15za449JEyUjOuxyi8ZrHdjniqqly5hHkn6QahycMt0HP3dCCuT3CQcG6EVS9iVI5YmgeAHzxt7Y0OwTSwHtZR9vmuLn0xFgCiToMcRicGyhMGgpEaN9k3L68mfp0MsVq9DOCA7giCYALjrDpZFnkCipEbtT7BvfO8PMiGQLpw0opsDchwKcHZptL3wkni15b4uDWwNcwpDxMFB5y38he3ePoZTTVzqP8nZeBw2clfh0eagDT2xclcg" (str.++ (str.++ str4 str13 "") "aHr4MHX7SGe1SmMjw7VgAgj7wiEJAdT3PenqlG7MS2ATtk5sHKhEgDaKTqHNtKhlbCpk0mBvBAA9ANeLL1IGmnrIiaNyFyYew66c4uM9ntnWv9EuxhYBOy94RldI2LzDYjXSk51ZWmE1zza2Qd2dxzWV1Faq7AdI6XIMaLMgPC81ghbs5j" (str.from_int (str.len str12)) "T3LOdOiyRFT8jUAH85SBT6tPrLxJWfKpsewjzIdVIIVkyeUdDR8EfW5h7pqpCtMOHjNWbK4QhoaTLqydGEE1Ojvrh5fiauaFFJUcFFwuopPvveJ1n5DRQ1oBNkVPWlERGjIbLDrvFQ50nCgqSrdZiejOjkPG2cnc7L6uLmcjm1CjN9DsShIEoVXXtTVUwBNAOdLWDfYl2VRl5gPUbSWfqqlRLyKvOBDLViVwMgqFQbNeTyw9ZzvgcSGhDkPguFvFNKlhG45mw0rap3Sr75kImlWD4yROLTlZCVFiKu1jD8u044CLf1QdbPnAVqh5QRro7JMxsvK8aLbJRQPK8I6U2me3fBwULF7uHRlMrOchqOhgMbE01gtAbWS3U4tiouc93e96hN0dm5VICRe9oBtTIUqWVfJmJG8QZ83cEz0iNgsdmqopbTzUtoOgPHRmz11nmZSmrqYTw9iUtP7XksKjgIdn2homJRSgTjDNlNLORXz8UqSuNKGT5sUj9jniVm5OoKwkE94AWTTG8fA31Tyr5RdDgr7C1RJwe8tikhKKnjNCO8BeQQjE0XTEgSI0LjcKGmiC3OM9MvX19Rb8iTydjOI3jAFlnEJPFVrEJVcjJvdHzVu4GCgGUpEI1hr63W1ZRQ3NMFZxkfxEAn5sGFLv4fp7gxoDgEDKRWnMMonRBiyB74hsM0hFWDzz7gKkyorTyiiGu3xsMaszHKI2dpinihImZOhqoUFwhHDf7CJz9E5EEnWgrcqlRhmFsFvLeuLQzN3LSK4wgOVw54BFeBfmDmjEUDaD56AbW02E3wjzy8RYE623EcfDLiHSiowWw9Y01uOFyC6WZcixFRr2VeckOpfDKPCPmjJr6ku9WYDsoirYPkDBk6B8sU14GPy4i9nJlVT0Bv0hiPoy7EbN9VGHHJZ84xWmgizD79u0AzXIqHp6EkuIP" "DIYX2TJymJT3DalgEw1k5UCaxFrYzqLLNEfyvgvpdO6isDL4wDRzNuK0m3NIq7BuYGykla48haYaXOoAK4YEtz9MayvzirhkgdcSOjm12Hk4t9IYrf7W8pLrrFmz1RbHWogfwxfFNUkfbXVtqMrGWkDG8jXDayenKrICU034NKX4QP01FhUKpk3Z3bSjdTzAIohBnEPhWGk3hEsJg0caEh1mqAMsp43VuzP9idUCHmQZaAB6d2ZDt8trGEbtZUKDUij2FJgFd8uLoPrev3vInk6bx9R7m0FQAgvRsLsQen3k4JsIpXOuyywstirJFCRHsgV2UIZKi4OItrAvqsPQL7Xc7vXC1Ofqy7cYWaWxTOYwOPoxNKdy1DDnRhXXK4OTmL03XVU6XxaDZjush4ciRNXgVNwuOqCO5YdelAuC4eZYQWzZ0QyKetFwFOk4PW9evfi7ANkTkKSCBh2UHnkqbi5FWRITMWinxKDyD9TXh3rx7y2ZHebuqaQD3kbj1phYBExHhNKSKOyZVRdlBhyb8oRJwk42FuuCkEDnRQBZApvk4l3SDMEYst0jKDzPNboW4tvw2vuQ")) "sMLRSkk9Nvtlb9fwmokFDhIl5FgN9VF3IEwNq1sL5QoNchVXldxdsekNyVrMRjjGeLzZ256e7NfSbc3duwDjGEuQZYmA9Y696XzbKHXshJrfWmiilIUEY6bEXAw2PzZaccnFhPT22JifsZ4ysBiBWnH2zbrkwn8xFFpjXK2wEcFFd4rhkqegzlyWwiOoQqOLKnUP2Mnv5ppxenRsFVWbMGZqGYXqxeG94BOfprBSIwQzKxRWQZTj87zN09PtnVmQ0qVsqFoSn5mhnewKJGLsd8Y2JX5bKu0RYuF0n4fdRzxADVZsHimNpW2Jydm2B2rdDAfVqnp0EEiOv6zDlT2YsAX8fHx1K8IeX3jzOmYu1gEgaxea7KWZ9EhqdFZqpOdgFVUBXdEbR3BHMQqBkqLozIfr5TP2q9vdTu6f8K4fzC2bLtyUnUAW0ZMiQdW9K4PzVFJoVwjYPrPvdbNMFcbac7kXqDt2K6jz1uSnlJNaFvemFZVHsda4H1w0YOIhszZyfQV7NButnNxWCcKT7SmzByza3ClsGspV8otqzLELQs2pIw9uHvIyRSG3Q2RFufkSoWRwquvaIkHy8sPRizB7MjMlr0TwMgcpDrLkDXZnOy0WFbxoT7XhHS70egr5Oh0ReMU39RYpJQCaenF0hDlLTsACNTF8wNeNe0i2nS5ThHyYXxCDTLN7i9goV2hQuWuDRbLquNkPlQexWPCktkfTMEQLzAP4ZFqahyt3sB5YqIBYelaLBCYt3LbvMTJvfxYqpPsDA9cnFJYk6ZW2z3lIwXlZYCE2g5dfwuRwlo8E9UBt9UwjxwONaciH9vEmubeHDypqKJ7AOIC5uV1Z7UTj4aXQLyCR1s5k8iOAIH6QL6ny39Klsg5T4szgzMvfTmBYYc8U2vC4V9lhRnrdgxhwdnb14AJjDTqOIxZtNtDNOcxsdJUMDkuC6hNQLD5cvIYI33x1y7QdQGuc0nGZ7c8kaToSawhq0TTCXZjRFkI19A4Y2j99dYIYPVGDBQiPcbuJuiZnKpMHffIakuZXtjZu3Ipvp4tHVxYWG6f43GMmA6MMWC95hj86Lfpw5r4C8kZtYUXv4phCjdzpvjWJtEFxxwkKySslkzBf2Sh4KjCoFceZHbFdH7QuhoPg4yzK24bB0MsBHLFh9NK1WTz4XupETQjiMXqYpq1Obof4u3aZ2rDfIhj4DES6yOg5fEmZI8CgzyqkRRtep9GlDnZPnS5USPQdYMG1wtvFW5ycxwHkqmCnDpwmZj7lT7qJG6D2LCJYFhhQ4LRWDrt7yW3Ba5Yg7onDjfzjfOj2rHhjIBaWXnxVg1Tn6pY1Fydbohq0gbHbCmzbcWis" str12) (re.++ (re.comp (str.to_re "sjPG8h07kkXZ9UuvD01InLOT5XPpvxObntNvIbLTu0b2dCEH3VP9mLPEoqAl1xWVkjwvp1TvmwdQAXnTOpsI12MXnw4WyTfTyYIYae2vRqfXvLcYV2s4irgEIVJdOWPvYYppzOlTw6vXYNxsWSS8PHI9DCzue7usLKne4nh5Rmc9nWZAkl6x9sWnWVrsBhkU7OQVG8Zb86husPg9ffhoKoaLM4LsOAVZ7tHBxftefIfCwFX8rlwViRFmxHuFMlnZNKm7XN87MA88jaofrFrGQENkyN0mRnuWzSfocCnDULXShXxaIHyDelDrfaa6FMEbyvB4FRE3p95R40B0ldhvBHBd2rf2ixyeD99lxOKZsXcInw2bOyXfUXqbPRFzAaVGF5vwm8Sj2p1")) (re.++ (str.to_re "yNeQLNV3mzh32IDHznFmVqPbAjYZqyc2KJHv0OjGimuPOd1mGpWdagBD9Xr16V7slfcCinudXnVNPLowihVakTH765vfcTrXo2nyUqaDV8uqoGJ89kfCLCbUcjCEKZUHiXbmWXWhhZtzXIGSTjLfTBz4aE8qv94T0QzisgoKeufoUwZLNBKCR5L") (str.to_re "qv1sujhzYvQ6ucaFGFex0KMZwzB01fsheinvrdjqZ0yP1QW0GeQmmmL0UVMZTSUpakCJ84tu2yWYqjlH5Vfulda3u819gZxLTbuB9ImBYUDZscnsTk7rVbSys4h1fde3rDwWfIkpbCzgd5nNaEVwjDoRcISACxEFxLIUaHAl4WDyfcVc93W3PiVM3V0UVM7Gsj0N8TMOCQOMYTUdZatvxsXyPy02B38D6N3dW7Az64kL6xYwu9ANSSC3aZb5uzT5aoSYi5B3Lfz6NPpu9JxP24EqFguLhnA9bTC4spBa0V2NE4rlwKuSAJy1aZutFHH3c4jLLpsfTysjy7h8VA0KOwtz7OSbUwoa9zIKdtrhrpsT58mRUGxjqIesOPoAaGWD296Bfj0Ws9D5Du9a1iHJDBeLRzLLq0wTHr17noL9O20CCBwWB66H45KUg8xZ8zeNzzWyUDxhWIQrQmKYrAHQyrtuTmOfGio2RaBHCbNnubFRSkJsTKdygPAkln3fmV3cYlXemNp5A0dCrw3SBjSk0GDqK4YVatpYkZGuqkbQ3GQZg1Rxlo528Pu5NvGUcTXf7t6xWd9tEtsbOzHfHotwzuNhnB2BsyVQgGp7eqGXcI8rGXsNHKsXKI95YWX1Y67wfZqi28e21zFJS26DMJtHEVIlz3rbQLkR8CQqTLs0uvBFJpF6VusZKxv9rzriXgxZyHFg8FSG4khCOsMtim7pHdCcqS5JXELtNecJc9mwPI3KAxwePfY8nZRm1Rw26CttTtwFmdVhHDf88A9bxW6B0N4UgfcqsOr7WhOLlocNGwJ3OjDLV7f2TLq98uItIL7z1yb9yIJ4ku9gj6XdGk1tyHpvFtzZe4X4lObRipSAgxFOsEzyv6LGmOOXmguNQbNqZjr06zqQyQGFBvbxTbgbWO7b1yQTHv7dmtnZrUSimMro9JShf11jddyGEizz2BKa14RgHzHV3SYkwXgSXWKcY40QaCFaV70twB3A3dryqsbqLXPSrZOyC066eX9QPySXduzLPYYayXMiyplxWxtNDlVDNwUodCg8pnHxCmDN7KVS0XhRbSsIJFHptiN") (str.to_re str12)) (re.diff (str.to_re "") (str.to_re str2))))))
(check-sat)
ASAN:SIGSEGV
=================================================================
==85808==ERROR: AddressSanitizer: stack-overflow on address 0x7fff9fa90f08 (pc 0x000001dd7560 bp 0x7fff9fa91620 sp 0x7fff9fa90ee0 T0)
    #0 0x1dd755f in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2951
    #1 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #2 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #3 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #4 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #5 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #6 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #7 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #8 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #9 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #10 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #11 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #12 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #13 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #14 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #15 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #16 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #17 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #18 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #19 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #20 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #21 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #22 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
    #23 0x1dd3018 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2585
    #24 0x1dd79dc in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2962
.....

SUMMARY: AddressSanitizer: stack-overflow ../src/ast/rewriter/seq_rewriter.cpp:2951 seq_rewriter::mk_derivative_rec(expr*, expr*)
==85808==ABORTING
NikolajBjorner commented 3 years ago

@veanes @cdstanford The stack overflow scenarios seem artificial and detached from what is relevant for applications so I am inclined to close these. You could assign the bugs to yourself if you think they are useful.

cdstanford commented 3 years ago

I agree with closing for the reasons you stated. Recursion is currently fundamental to how derivatives are calculated, and it would be nontrivial to rewrite the code to use incremental rewrites. Aside from increasing the stack limit there is probably no other easy solution. If it is possible to catch the error and provide a more friendly result at the Z3 level (e.g. return Unknown), that would also make sense but that is not really specific to the re/str solvers.

NikolajBjorner commented 3 years ago

Most places where we handle expressions in Z3, we don't recurse top-down, but attempt to force bottom-up processing with dynamic programming caching. This takes care of typical stack overflow scenarios that do happen for realistic scenarios, especially bit-vector problems. But clearly, these fuzz examples seem somewhat aimless.