Potential non-termination or bitvector performance #7352

dc-mak · 2024-08-23T17:48:11Z

18:36 ➜  z3 --version
Z3 version 4.13.0 - 64 bit

mwe.smt.txt

contents of mwe.smt.txt

(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

The text was updated successfully, but these errors were encountered:

rems-project/cerberus#494 exposed an issue in the Z3 which is a bit difficult to work around in the implementation itself and so we have this hacky work-around instead whilst it is fixed upstream Z3Prover/z3#7352

@i

This is to more closely match VIP and also probably remove the need to specify `is_null(x) || !addr_eq(x, NULL` which is just silly. This uses match (for future-proofing against the addition of a `funcptr` constructor) and default<loc> for morally partial index terms. It also rejects more programs as a result. HasAllocId is a positive way to check that a pointer is in the `(@i, a)` datatype case rather than not NULL. Whilst the two are equivalent right now, this change is is mainly to future-proof against the addition of `funcptr` constructor for function pointers as in VIP/PNVI-*. The implementation relies on a few design choices: 1. Shifting on NULL is forbidden (implicitly) by the ISO C standard (it requires pointers which point to objects, hence cannot be NULL). Also, we believe real-world code only relies on this idiom for hand-implementing `offsetof`, so we forbid it. This is enforced in the typing rules. 2. It doesn't enforce that NULL is the same as/has address 0, although if need be, the implementation could use this info since no known optimisations/compilers etc. rely on NULL not being 0. Note that casting 0 to a pointer gives NULL, and casting a NULL pointer to an integer gives 0. 3. Shifting NULL in the specification language results in `default<Loc>`. Representing it as an provenance-address pair with an empty provenance would also be fine but would raise further questions on how to represent the empty provenance (an unconstrained variable, or a special value, the latter of which would require constraints on all Owned pointers to not have that special value as their provenance). For any choice here, one could construct a program in which proof and runtime testing diverge. 4. `each (u64 i; ..) { Owned(array_shift(p,i); }` is defined to imply `has_alloc_id(p)`. 5. Addresses of global variables are also constrained with `has_alloc_id(&global)`. It uses SMT functions for a more readable SMT file output. Unfortunately it also triggers: Z3Prover/z3#7352 which is worked-around by using modifying the simplifier and calling it at exactly the right moment (comments in the code). The test for this is added in tests/cn/simplify_array_shift.c

@i

This is to more closely match VIP and also probably remove the need to specify `is_null(x) || !addr_eq(x, NULL` which is just silly. This uses match (for future-proofing against the addition of a `funcptr` constructor) and default<loc> for morally partial index terms. It also rejects more programs as a result. HasAllocId is a positive way to check that a pointer is in the `(@i, a)` datatype case rather than not NULL. Whilst the two are equivalent right now, this change is is mainly to future-proof against the addition of `funcptr` constructor for function pointers as in VIP/PNVI-*. The implementation relies on a few design choices: 1. Shifting on NULL is forbidden (implicitly) by the ISO C standard (it requires pointers which point to objects, hence cannot be NULL). Also, we believe real-world code only relies on this idiom for hand-implementing `offsetof`, so we forbid it. This is enforced in the typing rules. 2. It doesn't enforce that NULL is the same as/has address 0, although if need be, the implementation could use this info since no known optimisations/compilers etc. rely on NULL not being 0. Note that casting 0 to a pointer gives NULL, and casting a NULL pointer to an integer gives 0. 3. Shifting NULL in the specification language results in `default<Loc>`. Representing it as an provenance-address pair with an empty provenance would also be fine but would raise further questions on how to represent the empty provenance (an unconstrained variable, or a special value, the latter of which would require constraints on all Owned pointers to not have that special value as their provenance). For any choice here, one could construct a program in which proof and runtime testing diverge. 4. `each (u64 i; ..) { Owned(array_shift(p,i); }` is defined to imply `has_alloc_id(p)`. 5. Addresses of global variables are also constrained with `has_alloc_id(&global)`. It uses SMT functions for a more readable SMT file output. Unfortunately it also triggers: Z3Prover/z3#7352 which is worked-around by using modifying the simplifier and calling it at exactly the right moment (comments in the code). The test for this is added in tests/cn/simplify_array_shift.c

@i

This is to more closely match VIP and also probably remove the need to specify `is_null(x) || !addr_eq(x, NULL` which is just silly. This uses match (for future-proofing against the addition of a `funcptr` constructor) and default<loc> for morally partial index terms. It also rejects more programs as a result. HasAllocId is a positive way to check that a pointer is in the `(@i, a)` datatype case rather than not NULL. Whilst the two are equivalent right now, this change is is mainly to future-proof against the addition of `funcptr` constructor for function pointers as in VIP/PNVI-*. The implementation relies on a few design choices: 1. Shifting on NULL is forbidden (implicitly) by the ISO C standard (it requires pointers which point to objects, hence cannot be NULL). Also, we believe real-world code only relies on this idiom for hand-implementing `offsetof`, so we forbid it. This is enforced in the typing rules. 2. It doesn't enforce that NULL is the same as/has address 0, although if need be, the implementation could use this info since no known optimisations/compilers etc. rely on NULL not being 0. Note that casting 0 to a pointer gives NULL, and casting a NULL pointer to an integer gives 0. 3. Shifting NULL in the specification language results in `default<Loc>`. Representing it as an provenance-address pair with an empty provenance would also be fine but would raise further questions on how to represent the empty provenance (an unconstrained variable, or a special value, the latter of which would require constraints on all Owned pointers to not have that special value as their provenance). For any choice here, one could construct a program in which proof and runtime testing diverge. 4. `each (u64 i; ..) { Owned(array_shift(p,i); }` is defined to imply `has_alloc_id(p)`. 5. Addresses of global variables are also constrained with `has_alloc_id(&global)`. It uses SMT functions for a more readable SMT file output. Unfortunately it also triggers: Z3Prover/z3#7352 which is worked-around by using modifying the simplifier and calling it at exactly the right moment (comments in the code). The test for this is added in tests/cn/simplify_array_shift.c

@i

This is to more closely match VIP and also probably remove the need to specify `is_null(x) || !addr_eq(x, NULL` which is just silly. This uses match (for future-proofing against the addition of a `funcptr` constructor) and default<loc> for morally partial index terms. It also rejects more programs as a result. HasAllocId is a positive way to check that a pointer is in the `(@i, a)` datatype case rather than not NULL. Whilst the two are equivalent right now, this change is is mainly to future-proof against the addition of `funcptr` constructor for function pointers as in VIP/PNVI-*. The implementation relies on a few design choices: 1. Shifting on NULL is forbidden (implicitly) by the ISO C standard (it requires pointers which point to objects, hence cannot be NULL). Also, we believe real-world code only relies on this idiom for hand-implementing `offsetof`, so we forbid it. This is enforced in the typing rules. 2. It doesn't enforce that NULL is the same as/has address 0, although if need be, the implementation could use this info since no known optimisations/compilers etc. rely on NULL not being 0. Note that casting 0 to a pointer gives NULL, and casting a NULL pointer to an integer gives 0. 3. Shifting NULL in the specification language results in `default<Loc>`. Representing it as an provenance-address pair with an empty provenance would also be fine but would raise further questions on how to represent the empty provenance (an unconstrained variable, or a special value, the latter of which would require constraints on all Owned pointers to not have that special value as their provenance). For any choice here, one could construct a program in which proof and runtime testing diverge. 4. `each (u64 i; ..) { Owned(array_shift(p,i); }` is defined to imply `has_alloc_id(p)`. 5. Addresses of global variables are also constrained with `has_alloc_id(&global)`. It uses SMT functions for a more readable SMT file output. Unfortunately it also triggers: Z3Prover/z3#7352 which is worked-around by using modifying the simplifier and calling it at exactly the right moment (comments in the code). The test for this is added in tests/cn/simplify_array_shift.c

@i

This is to more closely match VIP and also probably remove the need to specify `is_null(x) || !addr_eq(x, NULL` which is just silly. This uses match (for future-proofing against the addition of a `funcptr` constructor) and default<loc> for morally partial index terms. It also rejects more programs as a result. HasAllocId is a positive way to check that a pointer is in the `(@i, a)` datatype case rather than not NULL. Whilst the two are equivalent right now, this change is is mainly to future-proof against the addition of `funcptr` constructor for function pointers as in VIP/PNVI-*. The implementation relies on a few design choices: 1. Shifting on NULL is forbidden (implicitly) by the ISO C standard (it requires pointers which point to objects, hence cannot be NULL). Also, we believe real-world code only relies on this idiom for hand-implementing `offsetof`, so we forbid it. This is enforced in the typing rules. 2. It doesn't enforce that NULL is the same as/has address 0, although if need be, the implementation could use this info since no known optimisations/compilers etc. rely on NULL not being 0. Note that casting 0 to a pointer gives NULL, and casting a NULL pointer to an integer gives 0. 3. Shifting NULL in the specification language results in `default<Loc>`. Representing it as an provenance-address pair with an empty provenance would also be fine but would raise further questions on how to represent the empty provenance (an unconstrained variable, or a special value, the latter of which would require constraints on all Owned pointers to not have that special value as their provenance). For any choice here, one could construct a program in which proof and runtime testing diverge. 4. `each (u64 i; ..) { Owned(array_shift(p,i); }` is defined to imply `has_alloc_id(p)`. 5. Addresses of global variables are also constrained with `has_alloc_id(&global)`. It uses SMT functions for a more readable SMT file output. Unfortunately it also triggers: Z3Prover/z3#7352 which is worked-around by using modifying the simplifier and calling it at exactly the right moment (comments in the code). The test for this is added in tests/cn/simplify_array_shift.c

@i

This is to more closely match VIP and also probably remove the need to specify `is_null(x) || !addr_eq(x, NULL` which is just silly. This uses match (for future-proofing against the addition of a `funcptr` constructor) and default<loc> for morally partial index terms. It also rejects more programs as a result. HasAllocId is a positive way to check that a pointer is in the `(@i, a)` datatype case rather than not NULL. Whilst the two are equivalent right now, this change is is mainly to future-proof against the addition of `funcptr` constructor for function pointers as in VIP/PNVI-*. The implementation relies on a few design choices: 1. Shifting on NULL is forbidden (implicitly) by the ISO C standard (it requires pointers which point to objects, hence cannot be NULL). Also, we believe real-world code only relies on this idiom for hand-implementing `offsetof`, so we forbid it. This is enforced in the typing rules. 2. It doesn't enforce that NULL is the same as/has address 0, although if need be, the implementation could use this info since no known optimisations/compilers etc. rely on NULL not being 0. Note that casting 0 to a pointer gives NULL, and casting a NULL pointer to an integer gives 0. 3. Shifting NULL in the specification language results in `default<Loc>`. Representing it as an provenance-address pair with an empty provenance would also be fine but would raise further questions on how to represent the empty provenance (an unconstrained variable, or a special value, the latter of which would require constraints on all Owned pointers to not have that special value as their provenance). For any choice here, one could construct a program in which proof and runtime testing diverge. 4. `each (u64 i; ..) { Owned(array_shift(p,i); }` is defined to imply `has_alloc_id(p)`. 5. Addresses of global variables are also constrained with `has_alloc_id(&global)`. It uses SMT functions for a more readable SMT file output. Unfortunately it also triggers: Z3Prover/z3#7352 which is worked-around by using modifying the simplifier and calling it at exactly the right moment (comments in the code). The test for this is added in tests/cn/simplify_array_shift.c

dc-mak · 2024-09-04T09:59:16Z

mwe2.smt.txt

another example exhibiting similar behaviour

(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.

NikolajBjorner · 2024-10-09T20:09:00Z

C:\z3\release>z3 mwe.smt.txt /v:2 smt.relevancy=0
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
success
(smt.searching)
(smt.stats :restarts     :decisions :clauses/bin/units    :simplify   :memory)
(smt.stats        :conflicts    :propagations     :lemmas      :deletions   )
(smt.stats    0      0      0      1   883/21/2       0/0     0    0   17.42)
(smt.stats    0    102   2758   8527  1128/21/2     102/45     1    0   17.52)
unsat

dc-mak mentioned this issue Aug 26, 2024

Work-around Z3 bug rems-project/cn-tutorial#81

Merged

NikolajBjorner closed this as completed Oct 9, 2024

dc-mak mentioned this issue Nov 4, 2024

Specify explicit theory in SMT solver backend rems-project/cerberus#571

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Potential non-termination or bitvector performance #7352

Potential non-termination or bitvector performance #7352

dc-mak commented Aug 23, 2024 •

edited

Loading

dc-mak commented Sep 4, 2024 •

edited

Loading

NikolajBjorner commented Oct 9, 2024

Potential non-termination or bitvector performance #7352

Potential non-termination or bitvector performance #7352

Comments

dc-mak commented Aug 23, 2024 • edited Loading

dc-mak commented Sep 4, 2024 • edited Loading

NikolajBjorner commented Oct 9, 2024

dc-mak commented Aug 23, 2024 •

edited

Loading

dc-mak commented Sep 4, 2024 •

edited

Loading