Detecting deep bugs with CBMC

[martin...@gmail.com]

Hi all,

I am wondering how CBMC tries to detect deep counter-examples in simple loops.

For example, consider the following program:

_Bool nondet_bool();

int main() {

    int x = 0;

    while(1) {

        if (nondet_bool())

            x = x + 1;

        assert(x != 1000);

    }

}

This requires a thousand iteration of the loop to hit the assertion violation.

I am trying with CBMC 5.32.1.

If I run cbmc with no arguments, it keeps unwinding the loop as it cannot determine the bound in advance.

I found an option --incremental-loop which checks the assertion after every iteration, which seems to correspond to the classical BMC algorithm. This works, but takes some time to get to the 1000th iteration.

Are there any another options that could be used?

I am aware of the paper Under-approximating loops in C programs for fast counterexample detection (https://link.springer.com/article/10.1007/s10703-015-0228-1) and I would like to know if the current CBMC implementation supports that and if yes, how to enable it.

Note that I don't want to manually specify the bound in the command line (using --unwind) as that is not a general solution for situations when the correct bound is not obvious from the code.

Thanks in advance,

Martin

[Martin Nyx Brain]

On Wed, 2021-06-23 at 02:00 -0700, martin...@gmail.com wrote:
> Hi all,
>
> I am wondering how CBMC tries to detect deep counter-examples in
> simple
> loops.
> For example, consider the following program:
>
> _Bool nondet_bool();
>
> int main() {
> int x = 0;
> while(1) {
> if (nondet_bool())
> x = x + 1;
> assert(x != 1000);
> }
> }
>
> This requires a thousand iteration of the loop to hit the assertion
> violation.
> I am trying with CBMC 5.32.1.
> If I run cbmc with no arguments, it keeps unwinding the loop as it
> cannot
> determine the bound in advance.

Yes. This is somewhat unfortunate but it is expected behaviour.

> I found an option --incremental-loop which checks the assertion after
> every
> iteration, which seems to correspond to the classical BMC algorithm.
> This
> works, but takes some time to get to the 1000th iteration.

Yes, again, this is as expected.

> Are there any another options that could be used?

You could try --paths lifo but I don't think that it will gain you
much. Fundamentally the issue is that there is no short counter-
example trace.

> I am aware of the paper Under-approximating loops in C programs for
> fast
> counterexample detection
> (https://link.springer.com/article/10.1007/s10703-015-0228-1) and I
> would
> like to know if the current CBMC implementation supports that and if
> yes,
> how to enable it.

The code is still in CPROVER but I am not sure if it has been used in
quite a while. If you have a look in regression/acceleration,
particularly accelerate.sh, there are examples of use. A few of the
examples seem to have bit-rotted but it looks like the core of the code
still works.

> Note that I don't want to manually specify the bound in the command
> line
> (using --unwind) as that is not a general solution for situations
> when the
> correct bound is not obvious from the code.

HTH

Cheers,
- Martin