search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

z3str3 assertion violation #2671

Closed wintered closed 4 years ago

wintered commented 4 years ago

Hi,

the following formula causes an assertion failure when calling "z3 --smt.string_solver=z3str3".

EDIT: we could it reduce the bug to the following:

(declare-fun s () String)
(declare-fun x () Int)
(assert (> x 6))
(assert (>= (str.indexof s "good" x) 0))
(check-sat
ASSERTION VIOLATION
File: ../src/smt/smt_justification.h
Line: 184
n1 != n2
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

Revision: 18b8089 OS: Ubuntu 18.04

mtrberzi commented 4 years ago

I'm having trouble reproducing this on the latest version of Z3. It returns SAT for me on the release build almost immediately. Would you be able to test this with your original instance?

What would also be very helpful is to see the stack trace on the assertion violation. If you are able to get this error again, please press G to invoke GDB, then enter the command "bt" and paste the output of that command (it will be very long!)

wintered commented 4 years ago

Here is another formula that triggered the bug as well as the gdb stacktrace.

Formula:

(declare-fun WDFQvmj_new () String)
(declare-fun d () String)
(declare-fun shifted1_T0_2 () String)
(declare-fun b () String)
(declare-fun shifted1_T2_2 () String)
(declare-fun shifted2_value () String)
(declare-fun c () String)
(assert (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and
(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and
(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and
(and
  (and (>= 1 0))
  (>= (- (str.len (str.replace d shifted1_T2_2 (str.at d 0))) 1) 0))
)
(>=
  (- (str.indexof (str.substr
                  (str.substr WDFQvmj_new (str.len shifted1_T0_2) (str.len (str.replace d shifted1_T2_2 (str.at d 0))))
                  1
                  (-
                    (str.len (str.substr WDFQvmj_new (str.len shifted1_T0_2) (str.len (str.replace d shifted1_T2_2 (str.at d (str.len d))))))
                    1))
                  " " 0)
     0)
  0))))))))))))))))
(>= 1 0)))))))))))))))))
(>=
  (+ (str.indexof (str.substr (str.substr WDFQvmj_new (str.len shifted1_T0_2) (str.len shifted2_value))
                              1
                              (- (str.len (str.replace d shifted1_T2_2 (str.at d (str.len d))))))
                  " " 0) 1)
  0))
(>=
  (- (str.len (str.substr (str.substr WDFQvmj_new (str.len shifted1_T0_2) (str.len shifted2_value))
                          1
                          (- (str.len (str.substr
                                        WDFQvmj_new
                                        (str.len shifted1_T0_2)
                                        (str.len (str.replace d shifted1_T2_2 (str.at d (str.len d))))))
                             1)))
     (+ (str.indexof (str.substr (str.substr WDFQvmj_new (str.len shifted1_T0_2) (str.len (str.replace d shifted1_T2_2 (str.at d (str.len d)))))
                                 1
                                 (- (str.len (str.substr WDFQvmj_new (str.len shifted1_T0_2) (str.len shifted2_value))) 1))
                     " " 0) 1))
  0)))))
(>= 0 0)))))))))
(>= 0 0)))))))))
(>= 0 0)))))))))))
(>= 0 0)))
(>= 0 0))
(>= 1 0))))))))
(>= 0 0)))))))))
(assert (= WDFQvmj_new (str.++ shifted1_T0_2 (str.++ b "") shifted1_T2_2 shifted2_value)))
(check-sat)

Stacktrace:

#0  0x00007f68f5abe687 in __GI___waitpid (pid=93152,
    stat_loc=stat_loc@entry=0x7ffc30b6bee8, options=options@entry=0)
    at ../sysdeps/unix/sysv/linux/waitpid.c:30
#1  0x00007f68f5a29067 in do_system (line=<optimized out>)
    at ../sysdeps/posix/system.c:149
#2  0x00005580597338e6 in invoke_gdb () at ../src/util/debug.cpp:100
#3  0x000055805891d898 in smt::eq_propagation_justification::eq_propagation_justification (this=0x7ffc30b6c570, n1=0x55805b72aef8, n2=0x55805b72aef8)
    at ../src/smt/smt_justification.h:184
#4  0x0000558058a0554e in smt::context::mk_enode (this=0x55805b4cd888,
    n=0x55805b9cc8d8, suppress_args=false, merge_tf=false, cgc_enabled=true)
    at ../src/smt/smt_internalizer.cpp:954
#5  0x0000558058a02967 in smt::context::internalize_formula_core (
    this=0x55805b4cd888, n=0x55805b9cc8d8, gate_ctx=true)
    at ../src/smt/smt_internalizer.cpp:607
#6  0x0000558058a00bfd in smt::context::internalize_eq (this=0x55805b4cd888,
    n=0x55805b9cc8d8, gate_ctx=true) at ../src/smt/smt_internalizer.cpp:418
#7  0x0000558058a008ce in smt::context::internalize_formula (
    this=0x55805b4cd888, n=0x55805b9cc8d8, gate_ctx=true)
    at ../src/smt/smt_internalizer.cpp:400
#8  0x00005580589fffe1 in smt::context::internalize (this=0x55805b4cd888,
    n=0x55805b9cc8d8, gate_ctx=true) at ../src/smt/smt_internalizer.cpp:341
#9  0x0000558058a026f7 in smt::context::internalize_formula_core (
    this=0x55805b4cd888, n=0x55805b9e0ac8, gate_ctx=false)
    at ../src/smt/smt_internalizer.cpp:579
#10 0x0000558058a009b9 in smt::context::internalize_formula (
    this=0x55805b4cd888, n=0x55805b9e0ac8, gate_ctx=false)
    at ../src/smt/smt_internalizer.cpp:408
#11 0x00005580589fffe1 in smt::context::internalize (this=0x55805b4cd888,
    n=0x55805b9e0ac8, gate_ctx=false) at ../src/smt/smt_internalizer.cpp:341
#12 0x0000558058a42744 in smt::theory_str::add_theory_aware_branching_info (
    this=0x55805b6b4d08, term=0x55805b9e0ac8, priority=0.10000000000000001,
    phase=l_true) at ../src/smt/theory_str.cpp:2799
#13 0x0000558058a52310 in smt::theory_str::process_concat_eq_type3 (
    this=0x55805b6b4d08, concatAst1=0x55805ba4a178, concatAst2=0x55805b845678)
    at ../src/smt/theory_str.cpp:4294
#14 0x0000558058a45a13 in smt::theory_str::simplify_concat_equality (
    this=0x55805b6b4d08, nn1=0x55805ba4a178, nn2=0x55805b845678)
    at ../src/smt/theory_str.cpp:3043
#15 0x0000558058a7286c in smt::theory_str::check_eqc_concat_concat (
    this=0x55805b6b4d08, eqc_concat_lhs=std::set with 1 element = {...},
---Type <return> to continue, or q <return> to quit---
    eqc_concat_rhs=std::set with 1 element = {...})
    at ../src/smt/theory_str.cpp:7536
#16 0x0000558058a716c4 in smt::theory_str::handle_equality (
    this=0x55805b6b4d08, lhs=0x55805b7b2428, rhs=0x55805b845678)
    at ../src/smt/theory_str.cpp:7420
#17 0x0000558058a74e5f in smt::theory_str::new_eq_eh (this=0x55805b6b4d08,
    x=170, y=309) at ../src/smt/theory_str.cpp:7749
#18 0x0000558058909191 in smt::context::propagate_th_eqs (this=0x55805b4cd888)
    at ../src/smt/smt_context.cpp:1661
#19 0x000055805890980d in smt::context::propagate (this=0x55805b4cd888)
    at ../src/smt/smt_context.cpp:1728
#20 0x0000558058916d40 in smt::context::bounded_search (this=0x55805b4cd888)
    at ../src/smt/smt_context.cpp:3670
#21 0x0000558058915d2c in smt::context::search (this=0x55805b4cd888)
    at ../src/smt/smt_context.cpp:3553
#22 0x0000558058914e96 in smt::context::check (this=0x55805b4cd888,
    num_assumptions=0, assumptions=0x0, reset_cancel=true)
    at ../src/smt/smt_context.cpp:3440
#23 0x0000558058914846 in smt::context::setup_and_check (this=0x55805b4cd888,
    reset_cancel=true) at ../src/smt/smt_context.cpp:3384
#24 0x0000558058c2e4b3 in smt::kernel::imp::setup_and_check (
    this=0x55805b4cd888) at ../src/smt/smt_kernel.cpp:108
#25 0x0000558058c2d6e7 in smt::kernel::setup_and_check (this=0x55805b4d8d78)
    at ../src/smt/smt_kernel.cpp:292
#26 0x000055805882ec63 in smt_tactic::operator() (this=0x55805b3f22a8, in=...,
    result=...) at ../src/smt/tactic/smt_tactic.cpp:201
#27 0x00005580591345fb in and_then_tactical::operator() (this=0x55805b403528,
    in=..., result=...) at ../src/tactic/tactical.cpp:120
#28 0x00005580591396ef in cond_tactical::operator() (this=0x55805b444c28,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#29 0x00005580591396ef in cond_tactical::operator() (this=0x55805b4867b8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#30 0x00005580591396ef in cond_tactical::operator() (this=0x55805b4caaa8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#31 0x00005580591396ef in cond_tactical::operator() (this=0x55805b55bd38,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#32 0x00005580591396ef in cond_tactical::operator() (this=0x55805b57d378,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#33 0x00005580591396ef in cond_tactical::operator() (this=0x55805b5b67d8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#34 0x00005580591396ef in cond_tactical::operator() (this=0x55805b5b6e48,
---Type <return> to continue, or q <return> to quit---
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#35 0x00005580591396ef in cond_tactical::operator() (this=0x55805b5bc5a8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#36 0x00005580591396ef in cond_tactical::operator() (this=0x55805b5c4f28,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#37 0x00005580591396ef in cond_tactical::operator() (this=0x55805b6035e8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#38 0x00005580591396ef in cond_tactical::operator() (this=0x55805b611d98,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#39 0x00005580591396ef in cond_tactical::operator() (this=0x55805b61f0b8,
    in=..., result=...) at ../src/tactic/tactical.cpp:1025
#40 0x00005580591345fb in and_then_tactical::operator() (this=0x55805b6204b8,
    in=..., result=...) at ../src/tactic/tactical.cpp:120
#41 0x0000558059137c6b in unary_tactical::operator() (this=0x55805b6204e8,
    in=..., result=...) at ../src/tactic/tactical.cpp:763
#42 0x00005580591275e4 in exec (t=..., in=..., result=...)
    at ../src/tactic/tactic.cpp:144
#43 0x00005580591278da in check_sat (t=..., g=..., md=..., labels=..., pr=...,
    core=..., reason_unknown="unknown") at ../src/tactic/tactic.cpp:164
#44 0x00005580590d3072 in (anonymous namespace)::tactic2solver::check_sat_core2
    (this=0x55805b4d8778, num_assumptions=0, assumptions=0x0)
    at ../src/solver/tactic2solver.cpp:174
#45 0x00005580590c45a5 in solver_na2as::check_sat_core (this=0x55805b4d8778,
    num_assumptions=0, assumptions=0x55805b3ec950)
    at ../src/solver/solver_na2as.cpp:67
#46 0x00005580590c5c20 in combined_solver::check_sat_core (this=0x55805b661328,
    num_assumptions=0, assumptions=0x55805b3ec950)
    at ../src/solver/combined_solver.cpp:246
#47 0x00005580590d9051 in solver::check_sat (this=0x55805b661328,
    num_assumptions=0, assumptions=0x55805b3ec950)
    at ../src/solver/solver.cpp:327
#48 0x00005580590a34ab in cmd_context::check_sat (this=0x7ffc30b6f690,
    num_assumptions=0, assumptions=0x55805b3ec950)
    at ../src/cmd_context/cmd_context.cpp:1569
#49 0x000055805905f611 in smt2::parser::parse_check_sat (this=0x7ffc30b6ebc0)
    at ../src/parsers/smt2/smt2parser.cpp:2595
#50 0x000055805906181f in smt2::parser::parse_cmd (this=0x7ffc30b6ebc0)
    at ../src/parsers/smt2/smt2parser.cpp:2937
#51 0x0000558059062a4a in smt2::parser::operator() (this=0x7ffc30b6ebc0)
    at ../src/parsers/smt2/smt2parser.cpp:3129
#52 0x000055805904c614 in parse_smt2_commands (ctx=..., is=...,
---Type <return> to continue, or q <return> to quit---
    interactive=false, ps=..., filename=0x0)
    at ../src/parsers/smt2/smt2parser.cpp:3178
#53 0x000055805832e2f3 in read_smtlib2_commands (
    file_name=0x7ffc30b7055a "bug.smt2") at ../src/shell/smtlib_frontend.cpp:89
#54 0x00005580583258fd in main (argc=3, argv=0x7ffc30b6fb08)
    at ../src/shell/main.cpp:358
NikolajBjorner commented 4 years ago

@mtrberzi "It returns SAT for me on the release build almost immediately. " but to reproduce assertion violations you need to run the debug build.

NikolajBjorner commented 4 years ago

I get leak reports.

C:\z3\build>z3 2671.smt2 smt.string_solver=z3str3
sat
ast_manager LEAKED: 9
Leaked: (= x3!tmp12[x3!tmp12] $$_str3!tmp26[$$_str3!tmp26])
id: 2800

C:\z3\build>z3 2671.smt2 smt.string_solver=z3str3
sat
ast_manager LEAKED: 9
Leaked: (= x3!tmp12[x3!tmp12] $$_str3!tmp26[$$_str3!tmp26])
id: 2804

What is troubling is that the repros are not reliable. It is almost for sure due to the (extensive) use of std::map on expr and std::set on expr as well. The values of heap allocated pointers change between executions. Some uses of std::map were replaced by obj_map, but far from all.

Unrelated, but close to the code that relates to the leak:

                if (u.str.is_concat(aCurr)) {
                    expr * arg0 = aCurr->get_arg(0);
                    expr * arg1 = aCurr->get_arg(1);

can be replaced by a match u.is_concat(aCurr, arg0, arg1), assuming arg0 and arg1 are declared before.

mtrberzi commented 4 years ago

I am seeing the leak now as well, taking a look to see if that can be addressed

mtrberzi commented 4 years ago

The assertion violation may be a duplicate of #2743

mtrberzi commented 4 years ago

@NikolajBjorner related to removing STL containers over std::map and std::set, is there a better alternative to storing expr as the value in an obj_map (for example `obj_map<expr, expr>) and if not, should I be manually incrementing the reference count of the value, as is done in e.g.expr_substitution::insert`?

NikolajBjorner commented 4 years ago

Most places uses separate reference counting management on top of obj_map. Note that the range of maps is polymorphic and could also maintain pointers. If you need a substitution, then expr_safe_replace can be used. It maintains reference counts.

From: Murphy Berzish notifications@github.com Sent: Thursday, December 5, 2019 2:41:39 AM To: Z3Prover/z3 z3@noreply.github.com Cc: Nikolaj Bjorner nbjorner@microsoft.com; Mention mention@noreply.github.com Subject: Re: [Z3Prover/z3] z3str3 assertion violation (#2671)

@NikolajBjornerhttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FNikolajBjorner&data=02%7C01%7Cnbjorner%40microsoft.com%7C86e7288b2109407e7b8208d7791382ce%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637110997018550092&sdata=0IxBtvgvbz7ju3tFcZQAL78QZNyBtwLm9k6nZkTUNx0%3D&reserved=0 related to removing STL containers over std::map and std::set, is there a better alternative to storing expr as the value in an obj_map (for example obj_map<expr, expr>) and if not, should I be manually incrementing the reference count of the value, as is done in e.g. expr_substitution::insert?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FZ3Prover%2Fz3%2Fissues%2F2671%3Femail_source%3Dnotifications%26email_token%3DAAXRHZA47CU44TBC3222CTDQXA53HA5CNFSM4JHXRPZKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEF65GLI%23issuecomment-561894189&data=02%7C01%7Cnbjorner%40microsoft.com%7C86e7288b2109407e7b8208d7791382ce%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637110997018550092&sdata=%2B%2Buj%2FkrKnqhzPeHqwcuEyLZI%2BcgAUaoSgQ%2Fj%2FqSnEHQ%3D&reserved=0, or unsubscribehttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAAXRHZGEQHYXJTB33YS3I4DQXA53HANCNFSM4JHXRPZA&data=02%7C01%7Cnbjorner%40microsoft.com%7C86e7288b2109407e7b8208d7791382ce%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637110997018560049&sdata=BDJuVyQXSrA4MOtb4JvHWIVXWpoXIHeTLdrNVzxnJ0Y%3D&reserved=0.

mtrberzi commented 4 years ago

This has since been fixed