search

Z3Prover / z3

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

Issues on arithmetic, string, and datatype formulas #5323

Closed rainoftime closed 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula, z3 e2c5e2e39cb1118b7d452e

(set-option :smt.random_seed 9)
(assert (exists ((x Real)) (= (* x x) 2.0)))
(push)
(check-sat)
(check-sat-using qfnia)
id: 271
Leaked: RootObject[@10]
id: 272
=================================================================
==77325==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 24 byte(s) in 1 object(s) allocated from:
    #0 0x50b2e8 in __interceptor_malloc /home//llvm-6/compiler-rt/lib/asan/asan_malloc_linux.cc:88
    #1 0x414faa0 in memory::allocate(unsigned long) /home/z3/build/../src/util/memory_manager.cpp:273:16
    #2 0x414f8bf in memory::allocate(char const*, int, char const*, unsigned long) /home/z3/build/../src/util/memory_manager.cpp:212:16
    #3 0x14fcd73 in smt::theory_lra::imp::mk_value(smt::enode*, smt::model_generator&) /home/z3/build/../src/smt/theory_lra.cpp:3278:20
    #4 0x14f3e20 in smt::theory_lra::mk_value(smt::enode*, smt::model_generator&) /home/z3/build/../src/smt/theory_lra.cpp:3838:19
    #5 0x193ba25 in smt::model_generator::mk_value_procs(obj_map<smt::enode, smt::model_value_proc*>&, ptr_vector<smt::enode>&, ptr_vector<smt::model_value_proc>&) /home/z3/build/../src/smt/smt_model_generator.cpp:115:40
    #6 0x193fd47 in smt::model_generator::mk_values() /home/z3/build/../src/smt/smt_model_generator.cpp:300:9
    #7 0x1945203 in smt::model_generator::mk_model() /home/z3/build/../src/smt/smt_model_generator.cpp:502:9
    #8 0x1c147b8 in smt::context::mk_proto_model() /home/z3/build/../src/smt/smt_context.cpp:4515:48
    #9 0x1c0c901 in smt::context::get_model(ref<model>&) /home/z3/build/../src/smt/smt_context.cpp:4550:13
    #10 0x1b2b9bc in smt::kernel::imp::get_model(ref<model>&) /home/z3/build/../src/smt/smt_kernel.cpp:136:22
    #11 0x1b2a484 in smt::kernel::get_model(ref<model>&) /home/z3/build/../src/smt/smt_kernel.cpp:352:16
    #12 0x1290561 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/smt/tactic/smt_tactic_core.cpp:224:28
    #13 0x2d2f3c3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:119:19
    #14 0x2d421d7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:948:18
    #15 0x2d313bf in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:291:24
    #16 0x2d2f3c3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:119:19
    #17 0x2d2f3c3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:119:19
    #18 0x2d4057c in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:775:14
    #19 0x2d824e6 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactic.cpp:150:9
    #20 0x2d82d94 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) /home/z3/build/../src/tactic/tactic.cpp:170:9
    #21 0x2bf4115 in check_sat_using_tactict_cmd::execute(cmd_context&) /home/z3/build/../src/cmd_context/tactic_cmds.cpp:216:25
    #22 0x2b771e7 in smt2::parser::parse_ext_cmd(int, int) /home/z3/build/../src/parsers/smt2/smt2parser.cpp:2906:33
    #23 0x2b6ef68 in smt2::parser::parse_cmd() /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3012:13
    #24 0x2b6959c in smt2::parser::operator()() /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3141:29
    #25 0x2b67e88 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3190:12
    #26 0x55b275 in read_smtlib2_commands(char const*) /home/z3/build/../src/shell/smtlib_frontend.cpp:142:18
    #27 0x547a19 in main /home/z3/build/../src/shell/main.cpp:371:28
    #28 0x7f56903f883f in __libc_start_main /build/glibc-e6zv40/glibc-2.23/csu/../csu/libc-start.c:291
rainoftime commented 3 years ago

(rewriter.expand_nested_stores) Assertion error src/smt/tactic/ctx_solver_simplify_tactic.cpp:138

(set-option :rewriter.expand_nested_stores true)
(declare-fun v6 () (_ BitVec 32))
(assert (forall ((v7 (_ BitVec 32))) (exists ((a1 (Array (_ BitVec 32) (_ BitVec 8)))) (not (= (_ bv0 1) (bvor (bvcomp (_ bv0 2) ((_ extract 1 0) v7)) (bvashr (bvnot (ite (= (store (store (store (store a1 v7 ((_ extract 15 8) v7)) (_ bv1 32) ((_ extract 7 0) v6)) (bvadd v6 (_ bv1 32)) ((_ extract 15 8) v6)) v6 ((_ extract 31 24) v6)) (store (store (store (store a1 (_ bv1 32) ((_ extract 7 0) v6)) (bvadd v6 (_ bv1 32)) ((_ extract 15 8) v6)) v6 ((_ extract 31 24) v6)) v7 ((_ extract 31 24) v7))) (_ bv1 1) (_ bv0 1))) (bvcomp (_ bv0 2) ((_ extract 1 0) v6)))))))))
(check-sat-using (then purify-arith ctx-solver-simplify))
z3 delta.out.smt2 
ASSERTION VIOLATION
File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp
Line: 138
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
rainoftime commented 3 years ago

(default) heap-use-after-free at ast.h:502

(declare-fun c () (Seq (Seq Int)))
(declare-fun b () (Seq (Seq Int)))
(assert (forall ((d (Seq (Seq Int)))) (forall ((f (Seq Int))) (exists ((a (Seq (Seq Int)))) (exists ((e (Seq Int))) (and (= a (seq.++ (seq.unit e) b)) (distinct (seq.++ (seq.unit f) d) a c)))))))
(check-sat)
==139830==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070001b9e34 at pc 0x0000005bcd67 bp 0x7ffd0a136470 sp 0x7ffd0a136468
READ of size 4 at 0x6070001b9e34 thread T0
    #0 0x5bcd66 in ast::hash() const /z3/build/../src/ast/ast.h:502:36
    #1 0x8988b3 in obj_ptr_pair_hash<expr, expr>::operator()(std::pair<expr*, expr*> const&) const /z3/build/../src/util/hash.h:176:38
    #2 0x8986ff in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::get_hash(std::pair<expr*, expr*> const&) const /hom
e/z3-debug/build/../src/util/hashtable.h:152:64
    #3 0x202a6c6 in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::remove(std::pair<expr*, expr*> const&) /z3-debug/build/../src/util/hashtable.h:558:25
    #4 0x200bdbc in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::erase(std::pair<expr*, expr*> const&) /z3-debug/build/../src/util/hashtable.h:591:34
    #5 0x2106427 in remove_obj_pair_map::undo() /z3/build/../src/smt/seq_eq_solver.cpp:1124:15
    #6 0xfaea1f in undo_trail_stack(ptr_vector<trail>&, unsigned int) /z3/build/../src/util/trail.h:388:16
    #7 0x18167e3 in smt::context::undo_trail_stack(unsigned int) /z3/build/../src/smt/smt_context.cpp:1944:9
    #8 0x181d90a in smt::context::pop_scope_core(unsigned int) /z3/build/../src/smt/smt_context.cpp:2429:13
    #9 0x183892b in smt::context::resolve_conflict() /z3/build/../src/smt/smt_context.cpp:4091:38
    #10 0x183103c in smt::context::bounded_search() /z3/build/../src/smt/smt_context.cpp:3799:22
    #11 0x182e0ab in smt::context::search() /z3/build/../src/smt/smt_context.cpp:3678:22
    #12 0x182d2a4 in smt::context::check(unsigned int, expr* const*, bool) /z3/build/../src/smt/smt_context.cpp:3561:17
    #13 0x182c6c2 in smt::context::setup_and_check(bool) /z3/build/../src/smt/smt_context.cpp:3497:20
    #14 0x13d54a9 in smt::kernel::imp::setup_and_check() /z3/build/../src/smt/smt_kernel.cpp:108:29
    #15 0x13d3d6c in smt::kernel::setup_and_check() /z3/build/../src/smt/smt_kernel.cpp:326:23
    #16 0x126de94 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /z3/build/../src/smt/tactic/smt_tactic_core.cpp:201:32
    #17 0x2cf44bf in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /z3/build/../src/tactic/tactical.cpp:119:19
    #18 0x2d08943 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /z3/build/../src/tactic/tactical.cpp:1038:19
    #19 0x2d08943 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /z3/build/../src/tactic/tactical.cpp:1038:19
rainoftime commented 3 years ago

z3 7c86134e856eb738886

(declare-fun f (Bool) Bool)
(assert (forall ((v8 Bool)) (forall ((v7 Bool)) (f (= v7 v8)))))
(check-sat-using (then simplify reduce-invertible ufbv-rewriter))
z3-debug/build/z3 delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/macros/macro_util.cpp
Line: 472
is_macro_head(head, head->get_num_args()) || is_quasi_macro_ok(head, head->get_num_args(), def)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
rainoftime commented 3 years ago

rewriter.eq2ineq + model_validate

(set-option :rewriter.eq2ineq true)
(assert (exists ((x Int)) (not (and (= x (bv2int ((_ int2bv 1) x))) (not (= x (bv2int ((_ int2bv 1) x))))))))
(push)
(check-sat)
(check-sat-using qffd)
sat
failed to verify: (exists ((x Int))
  (let ((a!1 (and (<= x (bv2int ((_ int2bv 1) x)))
                  (>= x (bv2int ((_ int2bv 1) x))))))
  (let ((a!2 (and (<= x (bv2int ((_ int2bv 1) x)))
                  (>= x (bv2int ((_ int2bv 1) x)))
                  (not a!1))))
    (not a!2))))
evaluated to (exists ((x Int))
  (let ((a!1 (and (<= x (bv2int ((_ int2bv 1) x)))
                  (>= x (bv2int ((_ int2bv 1) x))))))
  (let ((a!2 (and (<= x (bv2int ((_ int2bv 1) x)))
                  (>= x (bv2int ((_ int2bv 1) x)))
                  (not a!1))))
    (not a!2))))
(params keep_cardinality_constraints true pb.solver solver)

=================================================================
==49110==ERROR: LeakSanitizer: detected memory leaks
rainoftime commented 3 years ago 
(declare-datatypes ((A 0) (B 0)) (((a (sa B))) ((e1) (e2 (se2 A)))))
(assert (forall ((x1 A)) (exists ((x2 B)) (let (($x23 (= x1 (a x2))))))))
(check-sat-using qfufbv_ackr)
AddressSanitizer:DEADLYSIGNAL
=================================================================
==73595==ERROR: AddressSanitizer: stack-overflow on address 0x7fffe21e8ba8 (pc 0x0000004a5d17 
bp 0x7fffe21e9420 sp 0x7fffe21e8bb0 T0)
    #0 0x4a5d16 in __interceptor_strlen.part.32 /home/heqing/llvm-6/compiler-rt/lib/asan/../sa
nitizer_common/sanitizer_common_interceptors.inc:332
    #1 0x8f015b in str_hash_proc::operator()(char const*) const /home/peisen/test/tofuzz/z3-de
bug/build/../src/util/str_hashtable.h:27:93
    #2 0x40cff2c in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::ge
t_hash(char const* const&) const /z3/build/../src/util/hashtable
.h:152:64
    #3 0x40d0df1 in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::fi
nd_core(char const* const&) const /z3/build/../src/util/hashtabl
e.h:506:25
    #4 0x40cf02c in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::co
ntains(char const* const&) const /z3/build/../src/util/hashtable
.h:531:16
    #5 0x415f790 in is_debug_enabled(char const*) /z3/build/../s
rc/util/debug.cpp:75:34
    #6 0x3be448b in ast_manager::register_node_core(ast*) /z3/bu
ild/../src/ast/ast.cpp:1727:5
    #7 0x3c08b6c in app* ast_manager::register_node<app>(app*) /z3-deb
ug/build/../src/ast/ast.h:1659:33

    #12 0x2e2954e in datatype_factory::get_fresh_value(sort*) /h
rainoftime commented 3 years ago

z3 2138ef2ad05bacf3bc48836 heap-use-after-free at src/qe/mbp/mbp_arith.cpp:286:28

(declare-fun i5 () Int)
(declare-fun v41 () Bool)
(assert (distinct (forall ((q312 Bool) (q313 Int)) (or (not (= v41 q312)) (= q313 (abs (abs i5)))))))
(check-sat-using qe_rec)
rainoftime commented 3 years ago

heap-use-after-free at ./src/util/obj_hashtable.h:87:46 z3 d5c6abe14d3edc18667e

(declare-const x Bool)
(declare-datatypes ((ms 0)) (((e) (i) (t))))
(declare-sort d)
(declare-datatypes ((m 0)) (((c_ (m ms) (m_ d)))))
(declare-datatypes ((B 0)) (((T) (F))))
(declare-sort n)
(declare-fun r () n)
(declare-fun h () (Array n m))
(declare-fun s () (Array n B))
(assert (forall ((c (Array n m))) (and (distinct t (m (c r))) (= i (m (c r))) (forall ((n n)) (= i (m (c n)))) (= h (store c r (c_ e (m_ (select h r))))) (forall ((n n)) (or x (= (select s r) (ite (distinct n r) T F)))))))
(check-sat-using (then nnf unit-subsume-simplify ufbv))
rainoftime commented 3 years ago

Assertion error at src/util/obj_hashtable.h:174

(set-option :smt.phase_selection 5)
(declare-sort S)
(declare-datatypes ((lst 1)) ((par (k!00) ((nil) (cons (car k!00) (cdr (lst k!00)))))))
(declare-fun l1 () (lst S))
(assert (exists ((l2 (lst S))) (not (= l1 l2))))
(check-sat-using ctx-solver-simplify)
z3 delta.out.smt2 
ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 174
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
NikolajBjorner commented 3 years ago

qffd with non fd input (int2bv/bv2int) will not be fixed as it is outside qffd use. Other bugs that could be addressed have been