Unwinding should use assertions as break condition

[cliffordwolf]

Consider the following code:

uint32_t bext(uint32_t rs1, uint32_t rs2)
{
        uint32_t c = 0, m = 1, mask = rs2;
        int iter = 0;
        while (mask)
        {
                assert(iter != 32);
                iter++;

                uint32_t b = mask & -mask;
                if (rs1 & b)
                        c |= m;
                mask -= b;
                m <<= 1;
        }
        return c;
}       

cbmc will unwind that loop forever.

Adding the following (unreachable) return will fix unwinding and cbmc will correctly verify the assertion:

uint32_t bext(uint32_t rs1, uint32_t rs2)
{
        uint32_t c = 0, m = 1, mask = rs2;
        int iter = 0;
        while (mask)
        {
                assert(iter != 32);
                if (iter == 32) return;   // <-- stop unwinding if assertion failed
                iter++;

                uint32_t b = mask & -mask;
                if (rs1 & b)
                        c |= m;
                mask -= b;
                m <<= 1;
        }
        return c;
}

I think assert(x); should be treated like if (!x) return; for the purpose of loop unwinding. There is nothing to gain from unwinding a loop beyond a failed assertion.

[tautschnig]

I'd refer to #88 and #2031, where in particular the latter has interesting input from @martin-cs: it is perfectly conceivable for assert not to abort an execution path. Further input is much appreciated!

[cliffordwolf]

hmm.... interesting. That's one reason why I have in Yosys $assert cells and $cover cells as different constructs. If I understand that correctly, only a "cover" assert would not abort execution, an "assert" assert always would, correct? Would it be possible to only use "assert" asserts (and assumptions) for loop unrolling?

[martin-cs]

Assorted thoughts:

*. See #2031 for discussion of the two possible semantics for ASSERT. From your description I would interpret your "assert" and "cover" to be each of these.

*. See
92b92d6
for why I think CPROVER's ASSERT should not alter executions.

*. Yes, we could use ASSUME (the recommended way of getting the other semantics) in unwinding but there is always the question of how far we should go with this. Whatever loop unwinding check you do, short of using the solver (see path-wise support, unwinding assertions and incremental BMC), you will wind up with "obvious" things that it doesn't get. So, how far down this road should we go? I wouldn't recommend solely using ASSUMEs though.

HTH

[martin-cs]

@clairexen do you have further thoughts on this issue?