Targetless verification of concurrentqueue.c with z3v4.5 produces unsound(?) behavior

[btj]

Running

bin/verifast -prover z3v4.5 -verbose 200 examples/shared_boxes/concurrentqueue.c

produces

[...]
  2.380867s: examples/shared_boxes/concurrentqueue.c(440,5-6): Closing box
[...]
  2.386937s: examples/shared_boxes/concurrentqueue.c(132,60-61): Consuming assertion
Z3#mk_eq I malloc_block_queue
  2.386987s: Z3 query (= I malloc_block_queue) returns true: 0.001225 seconds
Z3#mk_app (declare-fun index_of (inductive inductive) Int) [(|(intbox)| head1); (append nodes1 (cons (|(intbox)| h) nil))]
Z3#mk_app (declare-fun drop (Int inductive) inductive) [(let ((a!1 (index_of (|(intbox)| head1)
                     (append nodes1 (cons (|(intbox)| h) nil)))))
  (+ a!1 1)); (append vs1 (cons (|(intbox)| value) nil))]
Z3#mk_eq (let ((a!1 (index_of (|(intbox)| head1)
                     (append nodes1 (cons (|(intbox)| h) nil)))))
  (drop (+ a!1 1) (append vs1 (cons (|(intbox)| value) nil)))) q
Error: Sorts inductive and Int are incompatible
[...]

While closing the box as part of executing the first perform_action statement of try_dequeue, VeriFast tries to consume the box invariant conjunct I(drop(index_of(head, nodes) + 1, vs)). One of the heap chunks in the symbolic heap at that point is malloc_block_queue(q). VeriFast first checks if I == malloc_block_queue. One would expect that this Z3 query return false, but here it returns true.

(In a next step, VeriFast compares the argument of the predicate assertion with the argument of the heap chunk. Since they are of different prover types, this produces a Z3 error. But the root cause is the fact that the initial Z3 query returns true.)

[btj]

Reducing this problem is non-trivial: the issue does not occur when:

• running with -target 32bit
• removing either of the other two C functions, create_queue and enqueue
• removing the first ctxt#assert_term call in get_fresh_integer_type_limits_symbols in verifast1.ml

[btj]

The issue also does not occur when running with -prover ext_z3 instead of -prover z3v4.5.

[btj]

Running

verifast -prover z3v4.5+SMTLib ../examples/shared_boxes/concurrentqueue.c

produces

../examples/shared_boxes/concurrentqueue.c
Error: Sorts inductive and Int are incompatible

but then running

z3 -v:1 auto_config=false smt.mbqi=false model=false type_check=true well_sorted_check=true -smt2 z3_v4dot5_dump.smt2

produces

[...]
unknown

where z3_v4dot5_dump.smt2 ends in

; Query: (= I32 malloc_block_queue) 
(push) 
(assert (not (= I32 malloc_block_queue))) 
(check-sat) 
(pop 1) 

which I take to mean that the I == malloc_block_queue query returns false here.

[btj]

The above outcomes were obtained when running against Z3 4.5.0. If I compile VeriFast with OCaml 4.07.1 and Z3 4.8.4 (through Opam), I still get Error: Sorts inductive and Int are incompatible.

[btj]

I could get the same error message by generating a replay log by inserting let 1 = Z3native.open_log "z3.log" in immediately after the line class z3_context () = in z3v4dot5prover.ml, and then replaying it using z3 z3.log.

[btj]

I submitted a Z3 bug: https://github.com/Z3Prover/z3/issues/2244

[btj]

It turns out that above, when I thought I was running against Z3 4.8.4, I was in fact still running against Z3 4.5.0. I was not able to reproduce the problem against Z3 4.8.4, so the fix for this issue seems to be to upgrade to Z3 4.8.4.

[btj]

Since we have now moved to Z3 4.8.5, I am closing this issue.