search

Z3Prover / z3

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

Bugs in smt.string_solver=seq #4613

Closed muchang closed 3 years ago

muchang commented 4 years ago

Z3 gives an invalid model on this formula:

[577] % z3release model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(model
 (define-fun b () String
  "")
 (define-fun c () String
  "")
 (define-fun a () String
  "\x00")
)
[578] %
[578] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (str.in_re (str.substr a 0 (str.len b)) (re.opt (str.to.re "m"))))
(assert (distinct b c))
(check-sat)
(get-model)
[579] %

Changing the "m" to "n" could still reproduce the bug, but changing it to most of the other string constants seems to hide the bug.

OS: Ubuntu 18.04 Commit: 7fa5b31

zhendongsu commented 4 years ago

Refutation unsoundness in the ctx-solver-simplify tactic: 

[538] % z3release small.smt2
unsat
sat
[539] % 
[539] % cat small.smt2
(declare-fun a () String)
(assert (str.in.re (str.++ a "z" a) (re.* (str.to.re "z"))))
(assert (str.in.re (str.++ "a" a) (re.opt (re.range "a" "u"))))
(check-sat-using ctx-solver-simplify)
(check-sat)
[540] %

OS: Ubuntu 18.04 Commit: https://github.com/Z3Prover/z3/commit/7eb05dd952a2f5de1d4be09436a97651c85dba18

zhendongsu commented 4 years ago

A (possibly interesting) performance regression:

[537] % time z3-4.8.8 small.smt2
sat

real    0m1.995s
user    0m1.874s
sys     0m0.099s
[538] % time z3release small.smt2
sat

real    0m33.911s
user    0m33.477s
sys     0m0.247s
[539] % 
[539] % time z3release smt.arith.solver=2 small.smt2
sat

real    0m3.291s
user    0m3.001s
sys     0m0.068s
[540] % 
[540] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () String)
(declare-fun d () Bool)
(declare-fun e () String)
(assert (= (distinct a (not (= b d))) (not (= "" (str.substr c 200 (str.len e))))))
(assert (not (= a (not (= b d)))))
(check-sat)
[541] %

OS: Ubuntu 18.04 Commit: 7eb05dd

zhendongsu commented 4 years ago

A performance issue and regression:

[516] % time cvc4 -q small.smt2
unsat

real    0m0.019s
user    0m0.005s
sys     0m0.005s
[517] % time z3-4.8.8 small.smt2
unsat

real    0m2.143s
user    0m2.088s
sys     0m0.016s
[518] % 
[518] % timeout -s 9 60 z3release smt.arith.solver=2 small.smt2
Killed
[519] % timeout -s 9 60 z3release smt.arith.solver=6 small.smt2
Killed
[520] % 
[520] % cat small.smt2
(declare-fun a () String)
(assert (not (str.contains (str.++ a "ab") (str.++ (str.substr a 5 (str.len a)) "a"))))
(check-sat)
[521] %

OS: Ubuntu 18.04 Commit: 7eb05dd

NikolajBjorner commented 4 years ago

Deleted assertion violation based on broken build.

rainoftime commented 4 years ago 
(set-logic QF_SLIA)
(declare-fun _substvar_461_ () String)
(set-option :smt.arith.bounded_expansion true)
(set-option :smt.string_solver seq)
(declare-const i10 Int)
(declare-const Str3 String)
(declare-const Str14 String)
(assert (>= (str.len Str3) 823))
(assert (>= (str.len Str14) (abs (- (div i10 952) 318 831 318 456))))
(assert (str.<= "" _substvar_461_))
(assert (distinct "" (int.to.str (mod i10 767))))
(check-sat)

=45297==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070001fd974 at pc 0x00000046857f bp 0x7fffeb908ad0 sp 0x7fffeb908ac0
READ of size 4 at 0x6070001fd974 thread T0
    #0 0x46857e in ast::hash() const ../src/ast/ast.h:501
    #1 0x5ccfc1 in obj_map<expr, expr*>::key_data::hash() const ../src/util/obj_hashtable.h:77
    #2 0x5cc399 in obj_map<expr, expr*>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:86
    #3 0x5caa4a in core_hashtable<obj_map<expr, expr*>::obj_map_entry, obj_hash<obj_map<expr, expr*>::key_data>, default_eq<obj_map<expr, expr*>::key_data> >::insert(obj_map<expr, expr*>::key_data&&) ../s
rc/util/hashtable.h:403
    #4 0x5c9bf8 in obj_map<expr, expr*>::insert(expr*, expr* const&) ../src/util/obj_hashtable.h:141
    #5 0x1215f31 in smt::theory_lra::imp::add_theory_assumptions(ref_vector<expr, ast_manager>&) ../src/smt/theory_lra.cpp:3934
    #6 0x11e3865 in smt::theory_lra::add_theory_assumptions(ref_vector<expr, ast_manager>&) ../src/smt/theory_lra.cpp:4123
    #7 0xfd6c30 in smt::context::add_theory_assumptions(ref_vector<expr, ast_manager>&) ../src/smt/smt_context.cpp:3480
    #8 0xfd6fb8 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3498
    #9 0xfd64db in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3438
    #10 0xd3e0f8 in smt::kernel::imp::setup_and_check() ../src/smt/smt_kernel.cpp:108
    #11 0xd3cbe7 in smt::kernel::setup_and_check() ../src/smt/smt_kernel.cpp:304
    #12 0xc6dcbd in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
    #13 0x1a791a3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #14 0x1a81888 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053

z3str3 is OK

rainoftime commented 4 years ago

A soundness issue of seq at commit 5aaa7e002

(set-logic QF_SLIA)
(declare-fun _substvar_67_ () Bool)
(declare-const v0 Bool)
(declare-const v2 Bool)
(declare-const v8 Bool)
(declare-const Str8 String)
(declare-const Str10 String)
(declare-const Str17 String)
(push 1)
(check-sat)
(assert (= v0 v8 v2 _substvar_67_))
(assert (not (= Str17 Str10)))
(push 1)
(pop 1)
(assert false)
(check-sat)
(pop 1)
(assert (>= (str.len Str8) 88))
(assert (= Str17 Str10))
(check-sat)

$ cvc4 -i yy.smt2 --strings-exp
sat
unsat
sat
$ z3 smt.string_solver=z3str3 yy.smt2
sat
unsat
sat
$ z3 smt.string_solver=seq yy.smt2
sat
unsat
unsat
rainoftime commented 4 years ago

UAF at smt_enode.h:179 (seq)

(set-logic QF_S)
(declare-const Str5 String)
(declare-const Str15 String)
(declare-const Str16 String)
(push 1)
(assert (= Str16 Str15))
(check-sat)
(pop 1)
(assert (str.in_re Str5 (str.to_re "")))
(push 1)
(assert false)
(check-sat)
(check-sat)
(pop 1)
(check-sat)

sat
unsat
unsat
=================================================================
==48576==ERROR: AddressSanitizer: heap-use-after-free on address 0x60c000009ac8 at pc 0x000000d29bf5 bp 0x7ffc04097500 sp 0x7ffc040974f0
READ of size 8 at 0x60c000009ac8 thread T0
    #0 0xd29bf4 in smt::enode::get_owner() const ../src/smt/smt_enode.h:179
    #1 0x151b653 in smt::theory_seq::check_extensionality() ../src/smt/theory_seq.cpp:558
    #2 0x1519083 in smt::theory_seq::final_check_eh() ../src/smt/theory_seq.cpp:400
    #3 0xff046f in smt::context::final_check() ../src/smt/smt_context.cpp:3995
    #4 0xfef478 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3911
    #5 0xfed1f0 in smt::context::search() ../src/smt/smt_context.cpp:3744
    #6 0xfeb7a7 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3627
    #7 0xd4f27a in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #8 0xd4cf23 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:342
    #9 0x113f522 in check_sat_core2 ../src/smt/smt_solver.cpp:195
    #10 0x1a3d21d in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #11 0x1a43c2e in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:241
    #12 0x1a41287 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #13 0x19f99d1 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1553
    #14 0x1989a71 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #15 0x198d9cd in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #16 0x198f0c5 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #17 0x196e11c in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #18 0x43d33f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:115
    #19 0x456124 in main ../src/shell/main.cpp:36
muchang commented 3 years ago

Invalid model on QF_S formula

[562] % z3release model_validate=true small.smt2
sat
(error "line 16 column 10: an invalid model was generated")
(
 (define-fun i () String
  "B")
 (define-fun f () String
  "DC")
 (define-fun g () String
  "efDCF")
 (define-fun a () String
  "ab")
 (define-fun b () String
  "DCfeF")
 (define-fun d () String
  "")
 (define-fun scr2_t2 () String
  "")
 (define-fun h () String
  "")
 (define-fun c () String
  "")
 (define-fun e () String
  "E")
 (define-fun j () String
  "DC")
)
[563] % 
[563] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun scr2_t2 () String)
(assert (distinct "-" (str.substr f 0 (str.len i))))
(assert (distinct i ""))
(assert (= j (str.replace (str.replace f i "") "fgomsicgrrddxntn" "")))
(assert (= (str.++ c "abdc" a b "ef" j d scr2_t2 e) (str.++ a "dcab" c j "fe" e g h)))
(check-sat)
(get-model)
[564] %

With unicode=false, the bug doesn't trigger.

Commit: 0a9ee6c

muchang commented 3 years ago

(rewriter.sort_sums) Assertion violation at ../src/smt/smt_context.h Line: 280

[560] % z3-4.8.10 small.smt2
unsat
[561] % z3release small.smt2
Segmentation fault
[562] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_context.h
Line: 280
e_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[563] %
[563] % cat small.smt2
(set-option :rewriter.sort_sums true)
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun n () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun o () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun k () String)
(declare-fun l () String)
(declare-fun m () String)
(assert (= b (str.++ (ite (str.suffixof g a) m a) "a")))
(assert (= c (str.++ (str.substr i 0 (str.len b)) d) h (str.++ c "a")))
(assert (= o
     (str.++ n (ite (str.in_re f (re.* (str.to_re f))) f k))
     (ite (>= 0 (str.len o)) o l)
     g
     (ite (str.in_re e (re.+ (str.to_re c))) e j)))
(check-sat)
[564] %

Commit: d9fb406

NikolajBjorner commented 3 years ago

moved unresolved to #5144