CBMC smybolic execution soundness issue; backwards goto missed in do ... while loop

[andreast271]

CBMC version: 5.12 (cbmc-5.12.6-17-g7d30335)
Operating system: GNU/Linux x86_64
Exact command line resulting in the issue: cbmc top.c
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead: VERIFICATION FAILED

Test case top.c:

#include "assert.h"
int main()
{
   int count = 0;
   do { 
     count = count +1 ; 
   } while(count < 5);

   assert(count == 5);
   assert(count == 17);
}

The first assertion should pass, the second should fail. However, CBMC reports SUCCESS for both assertions.
Looking at the program functions shows that simulating the loop is aborted via ASSUME(false) after one iteration:

cbmc top.c --program-only
[...]
// 1 file top.c line 5 function main
(36) count!0@1#2 == 0
// 2 file top.c line 7 function main
(37) count!0@1#3 == 1
// 3 file top.c line 8 function main
// 3 file top.c line 8 function main
(38) ASSUME(FALSE)

The problem is also present in cbmc-5.12.6
The last major version of CBMC where this test case works correctly is 5.7.

[martin-cs]

I confirm this is a real bug and that it is definitely a soundness issue.

$ cat top.c 
#include "assert.h"
int main()
{
   int count = 0;
   do { 
     count = count +1 ; 
   } while(count < 5);

   assert(count == 5);
   assert(count == 17);
}
$ cbmc top.c
CBMC version 5.12 (cbmc-5.12.4-345-ga41d2de7f) 64-bit x86_64 linux
Parsing top.c
Converting
Type-checking top
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 47 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification

** Results:
top.c function main
[main.assertion.1] line 9 assertion count == 5: SUCCESS
[main.assertion.2] line 10 assertion count == 17: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL

But it is not for the reason that you give. --program-only adds the assume(false) at the end so that the solving and trace generation mechanism can be used. It is an internal hack and maybe not the best one but ... it works. If you look at the goto-program you will see that it is correctly translated:

$ cbmc top.c --show-goto-functions
main /* main */
        // 0 file top.c line 4 function main
        signed int count;
        // 1 file top.c line 4 function main
        count = 0;
        // 2 file top.c line 6 function main
     1: count = count + 1;
        // 3 file top.c line 7 function main
        IF count < 5 THEN GOTO 1
        // 4 file top.c line 9 function main
        ASSERT count == 5 // assertion count == 5
        // 5 file top.c line 10 function main
        ASSERT count == 17 // assertion count == 17
        // 6 file top.c line 11 function main
        dead count;
        // 7 file top.c line 11 function main
        main#return_value = NONDET(signed int);
        // 8 file top.c line 11 function main
        END_FUNCTION

As no VCs are generated, that means the failing assertion is being discharged during symbolic execution so I suspect this might be an issue with constant folding in symbolic execution.

[martin-cs]

Correction -- this is definitely a symbolic execution bug but it is not necessarily constant folding. For some reason the loop is not being unwound at all. The branch is visited but ignored. Maybe @tautschnig or @peterschrammel have some insight here. There haven't been many changes to this area of the code recently and this sort of thing should be triggered quite easily by the test suite so I am somewhat surprised.

In the mean time; @andreast271 do you have time / inclination to try to find the offending PR by bisection?

$ cbmc top.c  --verbosity 10 --unwind 10
CBMC version 5.12 (cbmc-5.12.4-345-ga41d2de7f) 64-bit x86_64 linux
Parsing top.c
Converting
Type-checking top
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
...
BMC at file top.c line 2 (depth 22)
BMC at file top.c line 4 function main (depth 23)
Assignment to main::1::count!0@1 [32 bits]
BMC at file top.c line 6 function main (depth 25)
Assignment to main::1::count!0@1 [32 bits]
BMC at file top.c line 7 function main (depth 26)
BMC at file top.c line 9 function main (depth 27)
BMC at file top.c line 10 function main (depth 28)
BMC at file top.c line 11 function main (depth 29)
BMC at file top.c line 2 (depth 32)
size of program expression: 47 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification

** Results:
top.c function main
[main.assertion.1] line 9 assertion count == 5: SUCCESS
[main.assertion.2] line 10 assertion count == 17: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL

[andreast271]

This is the commit that introduced the bug:

commit e672e0d456e016d12fce489940d88220ee5e2b9a
Author: Michael Tautschnig <mt@debian.org>
Date:   Fri Dec 23 14:47:45 2016 +0100

    Turn "label: goto label;" or "while(cond);" into assume

    This pattern occurs in some SV-COMP benchmarks, but may also appear as
    busy-wait loops in realistic systems.

[tautschnig]

Taking a look as to why this condition is being applied here.