Assumption on array causes malfunctioning checks

[kofyou]

Hi, I would like to have an arbitrary memory except that, within a fixed range, there are at least two non-zero elements. However, such an assumption makes the checks behave incorrectly. They always pass no matter what I assert.

The code:

module test {
    const RANGE_START: bv4;
    const RANGE_SIZE: bv4;

    var mem: [bv4]bv4;

    init {
        assume(RANGE_START == 1bv4);
        assume(RANGE_SIZE == 8bv4);

        havoc mem;

        // within range [1bv4, 8bv4], 
        // there are at least two non zero elements in mem
        assume(exists (mix, miy: bv4):: 
            (mix >= RANGE_START) && (mix <= RANGE_START + RANGE_SIZE - 1bv4) &&
            (miy >= RANGE_START) && (miy <= RANGE_START + RANGE_SIZE - 1bv4) &&
            (mix != miy) && (mem[mix] != 0bv4) && (mem[miy] != 0bv4));
    }

    next {
    }

    // the invariant shall not hold
    invariant assert_false: (false);

    control {
        vobj = bmc(6);
        check;
        vobj.print_cex();
    }
}

In the code above, I assert false but all checks pass:

Successfully instantiated 1 module(s).
7 assertions passed.
0 assertions failed.
0 assertions indeterminate.
  PASSED -> vobj [Step #0] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #1] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #2] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #3] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #4] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #5] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #6] property assert_false @ ./example.v, line 25
Finished execution for module: test.

But if I comment out those two lines about the range,

        assume(exists (mix, miy: bv4)::
            // (mix >= RANGE_START) && (mix <= RANGE_START + RANGE_SIZE - 1bv4) &&
            // (miy >= RANGE_START) && (miy <= RANGE_START + RANGE_SIZE - 1bv4) &&
            (mix != miy) && (mem[mix] != 0bv4) && (mem[miy] != 0bv4));

Then the checks work again:

0 assertions passed.
7 assertions failed.
0 assertions indeterminate.
  FAILED -> vobj [Step #0] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #1] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #2] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #3] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #4] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #5] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #6] property assert_false @ ./example.v, line 25

I wonder if I am misusing havoc and assumptions. Thank you!

[kofyou]

I tried another way of doing so, but the assertion on false still passes:

module test {
    const RANGE_START: bv4;
    const RANGE_SIZE: bv4;

    var mem: [bv4]bv4;

    var non_zero_index1: bv4;
    var non_zero_index2: bv4;
    var non_zero_value1: bv4;
    var non_zero_value2: bv4;

    init {
        assume(RANGE_START == 1bv4);
        assume(RANGE_SIZE == 8bv4);

        // get an arbitrary index within range
        havoc non_zero_index1;
        assume((non_zero_index1 >= RANGE_START) && 
                (non_zero_index1 <= RANGE_START + RANGE_SIZE - 1bv4));
        
        // get another arbitrary index within range
        havoc non_zero_index2;
        assume((non_zero_index2 >= RANGE_START) && 
                (non_zero_index2 <= RANGE_START + RANGE_SIZE - 1bv4) &&
                (non_zero_index2 != non_zero_index1));

        // get an arbitrary non-zero value
        havoc non_zero_value1;
        assume(non_zero_value1 != 0bv4);

        // get an arbitrary non-zero value
        havoc non_zero_value2;
        assume(non_zero_value2 != 0bv4);

        havoc mem;

        mem[non_zero_index1] = non_zero_value1;
        mem[non_zero_index2] = non_zero_value2; 
    }

    next {
    }

    // the invariant shall not hold
    invariant assert_false: (false);

    control {
        vobj = bmc(6);
        check;
        vobj.print_cex();
    }
}

And again if I comment out the assumptions on non_zero_index1 and non_zero_index2, the assertion on false will fail.

[kofyou]

I feel that this is related to #159. If so, feel free to close this one. Thanks!

[polgreen]

Thanks for the example. Actually the behavior you are seeing is expected: the assumption is false because your bitvectors aren't big enough to fit in the values you are expecting as well as the sign bit, but you are using signed comparison operators which assume the first bit is a sign bit. Thus the values get read as negative values, and the assumption then turns out to be equivalent to "assume false", which means every property will pass.

Specifically RANGE_START + RANGE_SIZE - 1bv4 evaluates to 1000, which is 8 as an unsigned bitvector (as you expect), but -8 as a signed bitvector. That means that it's not possible for there to be 2 numbers that are <= RANGE_START + RANGE_SIZE - 1bv4 and distinct when you used a signed comparison operator.

Try this:

(declare-fun x () (_ BitVec 4))
(declare-fun y () (_ BitVec 4))
(assert (bvsle x #x8))
(assert (bvsle y #x8))
(assert (distinct y x))

(check-sat)
(get-model)

It's unsat as written. If you comment out the distinct assertion, it becomes sat but x and y are both equal to #x8.

To fix your file, you either need to use unsigned comparators (e.g., <=_u) or make the bitvectors bigger.

(the other issue you linked isn't related, it's about what the counterexamples look like with arrays)

[kofyou]

Thank you so much for the detailed explanation! Once I use unsigned comparators instead, it works!

And also am I correct that, for unsigned bitvectors division, I should use /_u? I ran a small example and it seems yes. Thanks again!

[polgreen]

Yep, _u makes the operators that are affected by signed-ness unsigned.