search

Z3Prover / z3

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

Potential non-termination or bitvector performance #7352

Open dc-mak opened 3 weeks ago

dc-mak commented 3 weeks ago 
18:36 ➜  z3 --version
Z3 version 4.13.0 - 64 bit

mwe.smt.txt

contents of mwe.smt.txt ```smt (set-option :print-success true) (set-option :produce-models true) (declare-datatype cn_tuple_0 ((cn_tuple_0))) (declare-datatype cn_tuple_2 (par (a0 a1) ((cn_tuple_2 (cn_get_0_of_2 a0) (cn_get_1_of_2 a1))))) (declare-datatype pointer ((NULL) (AiA (alloc_id cn_tuple_0) (addr (_ BitVec 64))))) (declare-datatype int_list_498 ((int_list_498 (head_struct_fld (_ BitVec 32)) (tail_struct_fld pointer)))) (declare-datatype int_queue_520 ((int_queue_520 (front_struct_fld pointer) (back_struct_fld pointer)))) (declare-datatype int_queueCell_521 ((int_queueCell_521 (first_struct_fld (_ BitVec 32)) (next_struct_fld pointer)))) (declare-datatypes ((seq_472 0)) (((Seq_Nil_507) (Seq_Cons_508 (head_data_fld (_ BitVec 32)) (tail_data_fld seq_472))))) (declare-fun unpack_IntQueuePtr1_708 () (cn_tuple_2 int_queue_520 seq_472)) (assert (or (and (= (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) NULL) (= (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) NULL)) (and (not (= (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) NULL)) (not (= (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) NULL))))) (declare-fun default_uf_9 () pointer) ; A (assert (= (bvurem (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) (((NULL) #x0000000000000000) ((AiA alloc_id addr) addr))) #x0000000000000008) #x0000000000000000)) (declare-fun default_uf_10 () cn_tuple_0) (declare-fun ambiguous_719 () Bool) (assert (= ambiguous_719 (and (and (and ((_ is AiA) (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))) ((_ is AiA) (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)))) (not (= (match (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) (((NULL) default_uf_10) ((AiA alloc_id addr) alloc_id))) (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) (((NULL) default_uf_10) ((AiA alloc_id addr) alloc_id)))))) (= (match (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) (((NULL) #x0000000000000000) ((AiA alloc_id addr) addr))) (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) (((NULL) #x0000000000000000) ((AiA alloc_id addr) addr))))))) (declare-fun both_eq_720 () Bool) (assert (= both_eq_720 (= (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))))) (declare-fun neither_721 () Bool) (assert (= neither_721 (and (not both_eq_720) (not ambiguous_719)))) (declare-fun ptrEq_722 () Bool) (assert (and (=> both_eq_720 ptrEq_722) (=> neither_721 (not ptrEq_722)))) (push 1) (assert ptrEq_722) (push 1) ; B ; (assert ; (and ; (not ; (= ; (match (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) ; (((NULL) default_uf_9) ; ((AiA alloc_id addr) ; (AiA alloc_id ; addr)))) ; (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) ; (((NULL) default_uf_9) ; ((AiA alloc_id addr) ; (AiA alloc_id ; addr)))))))) (assert (and (not (= (match (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) (((NULL) default_uf_9) ((AiA alloc_id addr) (AiA alloc_id (bvadd addr (bvmul #x0000000000000001 #x0000000000000004)))))) (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) (((NULL) default_uf_9) ((AiA alloc_id addr) (AiA alloc_id (bvadd addr (bvmul #x0000000000000001 #x0000000000000004)))))))))) (check-sat) ```

The file as is doesn't seem to terminate (the original bigger file this was cut down for ran for about 6 hours on GitHub CI before being cancelled).

If you comment assertion "A", then it takes a while but does come back correctly with unsat.

If you uncomment assertion "B", then it will come back with unsat quickly.

This may be related to #7295

dc-mak commented 1 week ago

mwe2.smt.txt

another example exhibiting similar behaviour ```smt (set-option :print-success true) (set-option :produce-models true) (declare-datatype cn_tuple_0 ((cn_tuple_0))) (declare-datatype cn_tuple_1 (par (a0) ((cn_tuple_1 (cn_get_0_of_1 a0))))) (declare-datatype cn_tuple_2 (par (a0 a1) ((cn_tuple_2 (cn_get_0_of_2 a0) (cn_get_1_of_2 a1))))) (declare-datatype pointer ((NULL) (AiA (alloc_id Int) (addr (_ BitVec 64))))) (define-fun ptr_shift ((p pointer) (offset (_ BitVec 64)) (null_case pointer)) pointer (match p (((NULL) null_case) ((AiA alloc_id addr) (AiA alloc_id (bvadd addr offset)))))) (define-fun copy_alloc_id ((p pointer) (new_addr (_ BitVec 64)) (null_case pointer)) pointer (match p (((NULL) null_case) ((AiA alloc_id addr) (AiA alloc_id new_addr))))) (define-fun alloc_id_of ((p pointer) (null_case Int)) Int (match p (((NULL) null_case) ((AiA alloc_id addr) alloc_id)))) (define-fun bits_to_ptr ((bits (_ BitVec 64)) (alloc_id Int)) pointer (ite (= bits #x0000000000000000) NULL (AiA alloc_id bits))) (define-fun addr_of ((p pointer)) (_ BitVec 64) (match p (((NULL) #x0000000000000000) ((AiA alloc_id addr) addr)))) (push 1) (push 1) (push 1) (declare-fun &arr_699 () pointer) ; This seems to be the problematic assert (assert (= (bvurem (addr_of &arr_699) #x0000000000000004) #x0000000000000000)) (assert ((_ is AiA) &arr_699)) (declare-fun default_uf_15 () pointer) (assert (and (not (= (ptr_shift (ptr_shift &arr_699 (bvmul #x0000000000000001 #x0000000000000002) default_uf_15) (bvmul #x0000000000000001 ((_ sign_extend 32) (bvneg #x00000002))) default_uf_15) &arr_699)))) (check-sat) ```

My guess is that it's related to bvurem, since that was also an issue with the first example.