Feature request: Attempt to compute loop bounds. Unroll to bound if possible. Error if not.

[martinlester]

Firstly, it's not clear to me exactly how SMACK handles loop unrolling for bounded model-checking. But so far as I can see, loops can be unrolled either by LLVM (before translation to Boogie IVL), or by whatever Boogie verification backend is being used. There are some flags to control that, but it's not obvious to me which part of the process they affect. In any case, the usage notes suggest that I have to specify the unrolling bound myself, and warn me that verification will succeed if the bug I'm looking for is beyond that bound.

Compare this behaviour with CBMC, which by default attempts to compute loop bounds itself and unrolls to that limit. If it can't find a bound, it fails with an error. (Alternatively, for hard to compute bounds, you can specify a bound and have CBMC insert an assertion violation if the program goes beyond that.)

I would like the option for similar behaviour in SMACK. It looks like LLVM already has some ability to compute loop bounds through LoopInfo. So in the first instance, maybe SMACK could use that somehow, and (optionally) fail with an error message if there are any loops with no bound computable by LLVM?

[shaobo-he]

Thank you for the request.

We have an option that enables LLVM's static loop unrolling pass, which unrolls a loop completely if it can determine the loop bound. This option is not enabled by default. The backend verifiers' unrolling option unrolls the loops in the Boogie programs up to a specified bound. If this bound is lower than the actual loop bound, the verification is unsound, meaning SMACK can miss a bug.

You're right we should have assertion inserted at loop exit like what CBMC does. There's a pending PR (#601) that implements the feature. We hope it will be merged soon.

With respect to the option you propose, I also had it in mind for a while. I think a better version is to give a warning rather than fail the process.