search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Segmentation Fault when calling get-value #403

Open ekiwi opened 2 years ago

ekiwi commented 2 years ago

In the following SMT file, the call to get-value in the last line causes yices to crash.

I am using a recent build of yices2 from oss-cad-suite:

> yices-smt2 --version
Yices 2.6.4
Copyright SRI International.
Linked with GMP 6.2.0
Copyright Free Software Foundation, Inc.
Build date: 2022-07-09
Platform: x86_64-pc-linux-gnu (release)
Revision: ca25c22fbbc602b6872f7e26e4426b42600e7cfd

The SMT file:

(set-logic QF_AUFBV)
(declare-sort QueueFormalTest_s 0)
(declare-fun reset_f (QueueFormalTest_s) Bool)
(declare-fun io_enq_valid_f (QueueFormalTest_s) Bool)
(declare-fun io_enq_bits_f (QueueFormalTest_s) (_ BitVec 32))
(declare-fun io_deq_ready_f (QueueFormalTest_s) Bool)
(declare-fun startTracking_f (QueueFormalTest_s) Bool)
(declare-fun dut_entries_io_deq_bits_MPORT_rand_data_f (QueueFormalTest_s) (_ BitVec 32))
(declare-fun dut__GEN_4_invalid_f (QueueFormalTest_s) (_ BitVec 2))
(declare-fun dut__GEN_7_invalid_f (QueueFormalTest_s) Bool)
(declare-fun dut__GEN_8_invalid_f (QueueFormalTest_s) (_ BitVec 32))
(declare-fun dut_entries_f (QueueFormalTest_s) (Array (_ BitVec 2) (_ BitVec 32)))
(declare-fun dut_deqIndex_value_f (QueueFormalTest_s) (_ BitVec 2))
(declare-fun dut_enqIndex_value_f (QueueFormalTest_s) (_ BitVec 2))
(declare-fun dut_maybeFull_f (QueueFormalTest_s) Bool)
(declare-fun tracker_elementCount_f (QueueFormalTest_s) (_ BitVec 2))
(declare-fun tracker_isActive_f (QueueFormalTest_s) Bool)
(declare-fun tracker_packetValue_f (QueueFormalTest_s) (_ BitVec 32))
(declare-fun tracker_packetCount_f (QueueFormalTest_s) (_ BitVec 2))
(declare-fun _resetCount_f (QueueFormalTest_s) Bool)
(define-fun dut_entries.io_deq_bits_MPORT.addr_f ((state QueueFormalTest_s)) (_ BitVec 2) (dut_deqIndex_value_f state))
(define-fun dut_entries.io_deq_bits_MPORT.data_f ((state QueueFormalTest_s)) (_ BitVec 32) (select (dut_entries_f state) (dut_entries.io_deq_bits_MPORT.addr_f state)))
(define-fun dut_entries_io_deq_bits_MPORT_addr_f ((state QueueFormalTest_s)) (_ BitVec 2) (dut_deqIndex_value_f state))
(define-fun dut_entries_io_deq_bits_MPORT_oob_f ((state QueueFormalTest_s)) Bool (not (bvugt (_ bv3 2) (dut_entries_io_deq_bits_MPORT_addr_f state))))
(define-fun dut_entries_io_deq_bits_MPORT_rand_data.en_f ((state QueueFormalTest_s)) Bool (dut_entries_io_deq_bits_MPORT_oob_f state))
(define-fun dut_indicesEqual_f ((state QueueFormalTest_s)) Bool (= (dut_enqIndex_value_f state) (dut_deqIndex_value_f state)))
(define-fun dut__empty_T_f ((state QueueFormalTest_s)) Bool (not (dut_maybeFull_f state)))
(define-fun dut_empty_f ((state QueueFormalTest_s)) Bool (and (dut_indicesEqual_f state) (dut__empty_T_f state)))
(define-fun dut_full_f ((state QueueFormalTest_s)) Bool (and (dut_indicesEqual_f state) (dut_maybeFull_f state)))
(define-fun dut__io_enq_ready_T_f ((state QueueFormalTest_s)) Bool (not (dut_full_f state)))
(define-fun dut_io_deq_ready_f ((state QueueFormalTest_s)) Bool (io_deq_ready_f state))
(define-fun dut_io_deq_valid_f ((state QueueFormalTest_s)) Bool (not (dut_empty_f state)))
(define-fun dut__T_f ((state QueueFormalTest_s)) Bool (and (dut_io_deq_ready_f state) (dut_io_deq_valid_f state)))
(define-fun dut_io_enq_ready_f ((state QueueFormalTest_s)) Bool (or (dut__io_enq_ready_T_f state) (dut_io_deq_ready_f state)))
(define-fun dut_io_enq_valid_f ((state QueueFormalTest_s)) Bool (io_enq_valid_f state))
(define-fun dut__T_1_f ((state QueueFormalTest_s)) Bool (and (dut_io_enq_ready_f state) (dut_io_enq_valid_f state)))
(define-fun dut__T_2_f ((state QueueFormalTest_s)) Bool (distinct (dut__T_f state) (dut__T_1_f state)))
(define-fun dut__T_3_f ((state QueueFormalTest_s)) Bool (and (dut_indicesEqual_f state) (dut__T_2_f state)))
(define-fun dut__GEN_0_f ((state QueueFormalTest_s)) Bool (ite (dut__T_3_f state) (dut__empty_T_f state) (dut_maybeFull_f state)))
(define-fun dut_wrap_f ((state QueueFormalTest_s)) Bool (= (dut_deqIndex_value_f state) (_ bv2 2)))
(define-fun dut__value_T_f ((state QueueFormalTest_s)) (_ BitVec 3) (bvadd ((_ zero_extend 1) (dut_deqIndex_value_f state)) (_ bv1 3)))
(define-fun dut__value_T_1_f ((state QueueFormalTest_s)) (_ BitVec 2) ((_ extract 1 0) (dut__value_T_f state)))
(define-fun dut__GEN_1_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (dut_wrap_f state) (_ bv0 2) (dut__value_T_1_f state)))
(define-fun dut__GEN_2_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (dut__T_f state) (dut__GEN_1_f state) (dut_deqIndex_value_f state)))
(define-fun dut_wrap_1_f ((state QueueFormalTest_s)) Bool (= (dut_enqIndex_value_f state) (_ bv2 2)))
(define-fun dut__value_T_2_f ((state QueueFormalTest_s)) (_ BitVec 3) (bvadd ((_ zero_extend 1) (dut_enqIndex_value_f state)) (_ bv1 3)))
(define-fun dut__value_T_3_f ((state QueueFormalTest_s)) (_ BitVec 2) ((_ extract 1 0) (dut__value_T_2_f state)))
(define-fun dut__GEN_3_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (dut_wrap_1_f state) (_ bv0 2) (dut__value_T_3_f state)))
(define-fun dut__GEN_4_invalid.en_f ((state QueueFormalTest_s)) Bool (not (dut__T_1_f state)))
(define-fun dut__GEN_7_invalid.en_f ((state QueueFormalTest_s)) Bool (not (dut__T_1_f state)))
(define-fun dut__GEN_8_invalid.en_f ((state QueueFormalTest_s)) Bool (not (dut__T_1_f state)))
(define-fun dut__GEN_9_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (dut__T_1_f state) (dut__GEN_3_f state) (dut_enqIndex_value_f state)))
(define-fun dut_io_deq_bits_f ((state QueueFormalTest_s)) (_ BitVec 32) (ite (dut_entries_io_deq_bits_MPORT_oob_f state) (dut_entries_io_deq_bits_MPORT_rand_data_f state) (dut_entries.io_deq_bits_MPORT.data_f state)))
(define-fun dut_entries.io_deq_bits_MPORT.en_f ((state QueueFormalTest_s)) Bool true)
(define-fun dut_entries.MPORT.en_f ((state QueueFormalTest_s)) Bool (and (dut_io_enq_ready_f state) (dut_io_enq_valid_f state)))
(define-fun dut_entries.MPORT.addr_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (not (dut__T_1_f state)) (dut__GEN_4_invalid_f state) (dut_enqIndex_value_f state)))
(define-fun dut_entries.MPORT.mask_f ((state QueueFormalTest_s)) Bool (ite (not (dut__T_1_f state)) (dut__GEN_7_invalid_f state) true))
(define-fun dut_io_enq_bits_f ((state QueueFormalTest_s)) (_ BitVec 32) (io_enq_bits_f state))
(define-fun dut_entries.MPORT.data_f ((state QueueFormalTest_s)) (_ BitVec 32) (ite (not (dut__T_1_f state)) (dut__GEN_8_invalid_f state) (dut_io_enq_bits_f state)))
(define-fun tracker_deq_valid_f ((state QueueFormalTest_s)) Bool (and (dut_io_deq_ready_f state) (dut_io_deq_valid_f state)))
(define-fun tracker__nextElementCount_T_f ((state QueueFormalTest_s)) Bool (not (tracker_deq_valid_f state)))
(define-fun tracker_enq_valid_f ((state QueueFormalTest_s)) Bool (and (dut_io_enq_ready_f state) (dut_io_enq_valid_f state)))
(define-fun tracker__nextElementCount_T_1_f ((state QueueFormalTest_s)) Bool (and (tracker_enq_valid_f state) (tracker__nextElementCount_T_f state)))
(define-fun tracker__nextElementCount_T_2_f ((state QueueFormalTest_s)) (_ BitVec 3) (bvadd ((_ zero_extend 1) (tracker_elementCount_f state)) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_3_f ((state QueueFormalTest_s)) (_ BitVec 2) ((_ extract 1 0) (tracker__nextElementCount_T_2_f state)))
(define-fun tracker__nextElementCount_T_4_f ((state QueueFormalTest_s)) Bool (not (tracker_enq_valid_f state)))
(define-fun tracker__nextElementCount_T_5_f ((state QueueFormalTest_s)) Bool (and (tracker__nextElementCount_T_4_f state) (tracker_deq_valid_f state)))
(define-fun tracker__nextElementCount_T_6_f ((state QueueFormalTest_s)) (_ BitVec 3) (bvsub ((_ zero_extend 1) (tracker_elementCount_f state)) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_7_f ((state QueueFormalTest_s)) (_ BitVec 2) ((_ extract 1 0) (tracker__nextElementCount_T_6_f state)))
(define-fun tracker__nextElementCount_T_8_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (tracker__nextElementCount_T_5_f state) (tracker__nextElementCount_T_7_f state) (tracker_elementCount_f state)))
(define-fun tracker_nextElementCount_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (tracker__nextElementCount_T_1_f state) (tracker__nextElementCount_T_3_f state) (tracker__nextElementCount_T_8_f state)))
(define-fun tracker__T_f ((state QueueFormalTest_s)) Bool (not (tracker_isActive_f state)))
(define-fun tracker__T_1_f ((state QueueFormalTest_s)) Bool (and (tracker__T_f state) (tracker_enq_valid_f state)))
(define-fun tracker_startTracking_f ((state QueueFormalTest_s)) Bool (startTracking_f state))
(define-fun tracker__T_2_f ((state QueueFormalTest_s)) Bool (and (tracker__T_1_f state) (tracker_startTracking_f state)))
(define-fun tracker__T_3_f ((state QueueFormalTest_s)) Bool (= (tracker_elementCount_f state) (_ bv0 2)))
(define-fun tracker__T_4_f ((state QueueFormalTest_s)) Bool (and (tracker_deq_valid_f state) (tracker__T_3_f state)))
(define-fun tracker_enq_bits_f ((state QueueFormalTest_s)) (_ BitVec 32) (dut_io_enq_bits_f state))
(define-fun tracker_deq_bits_f ((state QueueFormalTest_s)) (_ BitVec 32) (dut_io_deq_bits_f state))
(define-fun tracker__T_5_f ((state QueueFormalTest_s)) Bool (= (tracker_enq_bits_f state) (tracker_deq_bits_f state)))
(define-fun tracker_reset_f ((state QueueFormalTest_s)) Bool (reset_f state))
(define-fun tracker__T_7_f ((state QueueFormalTest_s)) Bool (not (tracker_reset_f state)))
(define-fun tracker__T_8_f ((state QueueFormalTest_s)) Bool (not (tracker__T_5_f state)))
(define-fun tracker__GEN_0_f ((state QueueFormalTest_s)) Bool (ite (tracker__T_4_f state) (tracker_isActive_f state) true))
(define-fun tracker__GEN_1_f ((state QueueFormalTest_s)) (_ BitVec 32) (ite (tracker__T_4_f state) (tracker_packetValue_f state) (tracker_enq_bits_f state)))
(define-fun tracker__GEN_2_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (tracker__T_4_f state) (tracker_packetCount_f state) (tracker_nextElementCount_f state)))
(define-fun tracker__GEN_3_f ((state QueueFormalTest_s)) Bool (ite (tracker__T_2_f state) (tracker__GEN_0_f state) (tracker_isActive_f state)))
(define-fun tracker__GEN_5_f ((state QueueFormalTest_s)) (_ BitVec 2) (ite (tracker__T_2_f state) (tracker__GEN_2_f state) (tracker_packetCount_f state)))
(define-fun tracker__T_9_f ((state QueueFormalTest_s)) Bool (and (tracker_isActive_f state) (tracker_deq_valid_f state)))
(define-fun tracker__packetCount_T_f ((state QueueFormalTest_s)) (_ BitVec 3) (bvsub ((_ zero_extend 1) (tracker_packetCount_f state)) (_ bv1 3)))
(define-fun tracker__packetCount_T_1_f ((state QueueFormalTest_s)) (_ BitVec 2) ((_ extract 1 0) (tracker__packetCount_T_f state)))
(define-fun tracker__T_10_f ((state QueueFormalTest_s)) Bool (= (tracker_packetCount_f state) (_ bv1 2)))
(define-fun tracker__T_11_f ((state QueueFormalTest_s)) Bool (= (tracker_packetValue_f state) (tracker_deq_bits_f state)))
(define-fun tracker__T_14_f ((state QueueFormalTest_s)) Bool (not (tracker__T_11_f state)))
(define-fun tracker__GEN_6_f ((state QueueFormalTest_s)) Bool (ite (tracker__T_10_f state) false (tracker__GEN_3_f state)))
(define-fun tracker__GEN_8_f ((state QueueFormalTest_s)) Bool (ite (tracker__T_9_f state) (tracker__GEN_6_f state) (tracker__GEN_3_f state)))
(define-fun tracker__T_15_f ((state QueueFormalTest_s)) Bool (= (tracker_elementCount_f state) (_ bv3 2)))
(define-fun tracker__T_16_f ((state QueueFormalTest_s)) Bool (not (tracker__nextElementCount_T_1_f state)))
(define-fun tracker__T_19_f ((state QueueFormalTest_s)) Bool (not (tracker__T_16_f state)))
(define-fun tracker_assert_f ((state QueueFormalTest_s)) Bool (=> (and (and (tracker__T_2_f state) (tracker__T_4_f state)) (tracker__T_7_f state)) (tracker__T_5_f state)))
(define-fun tracker_assert_1_f ((state QueueFormalTest_s)) Bool (=> (and (and (tracker__T_9_f state) (tracker__T_10_f state)) (tracker__T_7_f state)) (tracker__T_11_f state)))
(define-fun tracker_assert_2_f ((state QueueFormalTest_s)) Bool (=> (and (tracker__T_15_f state) (tracker__T_7_f state)) (tracker__T_16_f state)))
(define-fun _resetPhase_f ((state QueueFormalTest_s)) Bool (not (bvuge (ite (_resetCount_f state) (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun io_enq_ready_f ((state QueueFormalTest_s)) Bool (dut_io_enq_ready_f state))
(define-fun io_deq_valid_f ((state QueueFormalTest_s)) Bool (dut_io_deq_valid_f state))
(define-fun io_deq_bits_f ((state QueueFormalTest_s)) (_ BitVec 32) (dut_io_deq_bits_f state))
(define-fun dut_reset_f ((state QueueFormalTest_s)) Bool (reset_f state))
(define-fun _resetActive_f ((state QueueFormalTest_s)) Bool (=> (_resetPhase_f state) (reset_f state)))
(define-fun dut_entries_next ((state QueueFormalTest_s)) (Array (_ BitVec 2) (_ BitVec 32)) (ite (and (dut_entries.MPORT.en_f state) (dut_entries.MPORT.mask_f state)) (store (dut_entries_f state) (dut_entries.MPORT.addr_f state) (dut_entries.MPORT.data_f state)) (dut_entries_f state)))
(define-fun dut_deqIndex_value_next ((state QueueFormalTest_s)) (_ BitVec 2) (ite (dut_reset_f state) (_ bv0 2) (dut__GEN_2_f state)))
(define-fun dut_enqIndex_value_next ((state QueueFormalTest_s)) (_ BitVec 2) (ite (dut_reset_f state) (_ bv0 2) (dut__GEN_9_f state)))
(define-fun dut_maybeFull_next ((state QueueFormalTest_s)) Bool (ite (dut_reset_f state) false (dut__GEN_0_f state)))
(define-fun tracker_elementCount_next ((state QueueFormalTest_s)) (_ BitVec 2) (ite (tracker_reset_f state) (_ bv0 2) (tracker_nextElementCount_f state)))
(define-fun tracker_isActive_next ((state QueueFormalTest_s)) Bool (ite (tracker_reset_f state) false (tracker__GEN_8_f state)))
(define-fun tracker_packetValue_next ((state QueueFormalTest_s)) (_ BitVec 32) (ite (tracker__T_2_f state) (tracker__GEN_1_f state) (tracker_packetValue_f state)))
(define-fun tracker_packetCount_next ((state QueueFormalTest_s)) (_ BitVec 2) (ite (tracker__T_9_f state) (tracker__packetCount_T_1_f state) (tracker__GEN_5_f state)))
(define-fun _resetCount_next ((state QueueFormalTest_s)) Bool (ite (_resetPhase_f state) (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite (_resetCount_f state) (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) (_resetCount_f state)))
(define-fun _resetCount_init ((state QueueFormalTest_s)) Bool false)
(define-fun QueueFormalTest_t ((state QueueFormalTest_s) (state_n QueueFormalTest_s)) Bool (and (= (dut_entries_f state_n) (dut_entries_next state)) (and (= (dut_deqIndex_value_f state_n) (dut_deqIndex_value_next state)) (and (= (dut_enqIndex_value_f state_n) (dut_enqIndex_value_next state)) (and (= (dut_maybeFull_f state_n) (dut_maybeFull_next state)) (and (= (tracker_elementCount_f state_n) (tracker_elementCount_next state)) (and (= (tracker_isActive_f state_n) (tracker_isActive_next state)) (and (= (tracker_packetValue_f state_n) (tracker_packetValue_next state)) (and (= (tracker_packetCount_f state_n) (tracker_packetCount_next state)) (= (_resetCount_f state_n) (_resetCount_next state)))))))))))
(define-fun QueueFormalTest_i ((state QueueFormalTest_s)) Bool (= (_resetCount_f state) (_resetCount_init state)))
(define-fun QueueFormalTest_a ((state QueueFormalTest_s)) Bool (and (tracker_assert_f state) (and (tracker_assert_1_f state) (tracker_assert_2_f state))))
(define-fun QueueFormalTest_u ((state QueueFormalTest_s)) Bool (_resetActive_f state))
(declare-fun s0 () QueueFormalTest_s)
(assert (QueueFormalTest_i s0))
(assert (_resetActive_f s0))
(declare-fun s1 () QueueFormalTest_s)
(assert (QueueFormalTest_t s0 s1))
(assert (_resetActive_f s1))
(declare-fun s2 () QueueFormalTest_s)
(assert (QueueFormalTest_t s1 s2))
(assert (_resetActive_f s2))
(declare-fun s3 () QueueFormalTest_s)
(assert (QueueFormalTest_t s2 s3))
(assert (_resetActive_f s3))
(assert (not (and (tracker_assert_f s3) (and (tracker_assert_1_f s3) (tracker_assert_2_f s3)))))
(check-sat)
(get-value ((dut_entries_f s0)))

I get the following output when calling yices with this input:

> yices-smt2 yices_test.smt
sat
fish: Job 1, 'yices-smt2 yices_test.smt' terminated by signal SIGSEGV (Address boundary error)