Question: CBMC loop unwinding behaviours--programs fully unwound with just --unwind 2 takes forever if no parameter given

[hellotommmy]

CBMC version: 6.4.1
Operating system: Ubuntu 22.04 (on wsl 2)
Exact command line resulting in the issue: (After changing into the cbmcPlay directory (attached)) cbmc los_init.c --unwinding-assertions --function LOS_KernelInit los_debug.c los_memory.c los_task.c --object-bits 16 --unwind 2 v.s. cbmc los_init.c --unwinding-assertions --function LOS_KernelInit los_debug.c los_memory.c los_task.c --object-bits 16
What behaviour did you expect: If --unwind 2 already gives no unwinding assertions failure and returns quickly, then not giving unwinding depth should just return with the same amount of time taken.
What happened instead: Not giving the -unwind parameter causes cbmc to get stuck running forever.

cbmcPlay.zip

[tautschnig]

Addressing this would require invoking a solver during symbolic execution so that we can prove that a loop condition is necessarily false. We have partial support for this with --incremental-loop <loop id>. Beyond this some substantial re-architecting of CBMC is required to make this possible.

[hellotommmy]

Addressing this would require invoking a solver during symbolic execution so that we can prove that a loop condition is necessarily false. We have partial support for this with --incremental-loop <loop id>. Beyond this some substantial re-architecting of CBMC is required to make this possible.

Thank you for the quick reply! Could you elaborate a bit on why this happened? Is it the case that the loop has not been fully unwound, yet CBMC gives an incorrect answer saying it has been; or CBMC has fully unwound the loop in a few steps, but not able to find out itself? I would imagine the latter to be the case (incompleteness), or otherwise this would be a soundness issue.

[remi-delmas-3000]

Hi,

• --unwind 2 --unwinding-assertions tells CBMC to stop unwinding at depth 2 and to add a canary assertion assert(!loop_cond);. This assertion is checked with the full reasoning power of the SAT or SMT solver.
• without unwind parameters, CBMC unwinds until it detects by itself that the loop condition is necessary false (during symbolic execution). In that mode, CBMC only uses lightweight reasoning techniques and does not use the full power of a SAT/SMT engine. There are cases where it cannot detect that the loop condition becomes necessarily false, an it keeps unwinding.

[ChengsongTan]

Hi,

Thanks very much for this explanation! This makes sense. So to my understanding, in the design of CBMC, there is not a separate process that calls an smt solver on each iteration's assert(!loop_cond) formula, and stop the unrolling if its verification is successful. Was this because of the computation overhead (since loop conditions can have complex dependencies on the states, potentially leading to large formulas)?

Best,
Chengsong