No verification condition is generated

[sepideha]

CBMC version: cbmc-5.12-d8598f8
Operating system: 64-bit x86_64 macos
Exact command line resulting in the issue: /cbmc --unwind 2 008.493977f.43_1a.cil_safe.i
What behaviour did you expect: generated VCC = 1
What happened instead: generated VCC =0

In the above benchmark, I added assert(0) in the following function:

__inline static void ( __attribute__((__always_inline__)) ldv_error)(void) { { LDV_ERROR: assert(0); goto LDV_ERROR; } }

I am wondering why any VCC has not been generated?

Here is the logs:

➜ ./cbmc --unwind 2 008.493977f.43_1a.cil_safe.i

CBMC version 5.12 (cbmc-5.12-d8598f8) 64-bit x86_64 macos
Parsing 008.493977f.43_1a.cil_safe.i
Converting
Type-checking 008.493977f.43_1a.cil_safe
file /home/ldvuser/ldv/inst/kernel-rules/verifier/rcv.h line 15 function ldv_error: function `assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
file /work/ldvuser/novikov/work/current--X--drivers/media/video/videobuf-vmalloc.ko--X--defaultlinux--X--43_1a--X--cpachecker/linux/csd_deg_dscv/10/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/videobuf-vmalloc.c.prepared line 96 function videobuf_vm_close: replacing function pointer by 2 possible targets
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
**** WARNING: no body for function ldv_initialize
Unwinding loop main.0 iteration 1 file /work/ldvuser/novikov/work/current--X--drivers/media/video/videobuf-vmalloc.ko--X--defaultlinux--X--43_1a--X--cpachecker/linux/csd_deg_dscv/10/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/videobuf-vmalloc.c.prepared line 564 function main thread 0
**** WARNING: no body for function ldv_handler_precall
**** WARNING: no body for function printk
**** WARNING: no body for function vmalloc_user
Unwinding loop __videobuf_mmap_free.0 iteration 1 file /work/ldvuser/novikov/work/current--X--drivers/media/video/videobuf-vmalloc.ko--X--defaultlinux--X--43_1a--X--cpachecker/linux/csd_deg_dscv/10/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/videobuf-vmalloc.c.prepared line 200 function __videobuf_mmap_free thread 0
Not unwinding loop __videobuf_mmap_free.0 iteration 2 file /work/ldvuser/novikov/work/current--X--drivers/media/video/videobuf-vmalloc.ko--X--defaultlinux--X--43_1a--X--cpachecker/linux/csd_deg_dscv/10/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/videobuf-vmalloc.c.prepared line 200 function __videobuf_mmap_free thread 0
Unwinding loop __videobuf_mmap_mapper.0 iteration 1 file /work/ldvuser/novikov/work/current--X--drivers/media/video/videobuf-vmalloc.ko--X--defaultlinux--X--43_1a--X--cpachecker/linux/csd_deg_dscv/10/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/videobuf-vmalloc.c.prepared line 223 function __videobuf_mmap_mapper thread 0
Not unwinding loop __videobuf_mmap_mapper.0 iteration 2 file /work/ldvuser/novikov/work/current--X--drivers/media/video/videobuf-vmalloc.ko--X--defaultlinux--X--43_1a--X--cpachecker/linux/csd_deg_dscv/10/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/videobuf-vmalloc.c.prepared line 223 function __videobuf_mmap_mapper thread 0
**** WARNING: no body for function copy_to_user
Not unwinding loop main.0 iteration 2 file /work/ldvuser/novikov/work/current--X--drivers/media/video/videobuf-vmalloc.ko--X--defaultlinux--X--43_1a--X--cpachecker/linux/csd_deg_dscv/10/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/videobuf-vmalloc.c.prepared line 564 function main thread 0
**** WARNING: no body for function ldv_check_final_state
size of program expression: 613 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification

** Results:
/home/ldvuser/ldv/inst/kernel-rules/verifier/rcv.h function ldv_error
[ldv_error.assertion.1] line 15 assertion 0: SUCCESS

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

➜
./cbmc --unwind 2 008.493977f.43_1a.cil_safe.i --show-properties
CBMC version 5.12 (cbmc-5.12-d8598f8) 64-bit x86_64 macos
Parsing 008.493977f.43_1a.cil_safe.i
Converting
Type-checking 008.493977f.43_1a.cil_safe
file /home/ldvuser/ldv/inst/kernel-rules/verifier/rcv.h line 15 function ldv_error: function `assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
file /work/ldvuser/novikov/work/current--X--drivers/media/video/videobuf-vmalloc.ko--X--defaultlinux--X--43_1a--X--cpachecker/linux/csd_deg_dscv/10/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/videobuf-vmalloc.c.prepared line 96 function videobuf_vm_close: replacing function pointer by 2 possible targets
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Property ldv_error.assertion.1:
file /home/ldvuser/ldv/inst/kernel-rules/verifier/rcv.h line 15 function ldv_error
assertion 0
(__CPROVER_bool)0

[hannes-steffenhagen-diffblue]

Hello, thanks for letting us know about a potential problem.

We will however needs some more information to answer the question here or determine if this might be a bug. Ideally this would be a short program exemplifying the same issue.

FWIW VCCs are not generated for assertions which can be shown to never fail (e.g. unreachable (from the entry point) assertions or assertions whose condition can be simplified to TRUE via constant folding, so there being fewer VCCs than there are assertions in the input program is not indicative of a problem on its own.

[martin-cs]

To add to what @hannes-steffenhagen-diffblue has said : --show-properties finds the assertion in the program, it does not check if they are reachable. So it is possible for a program to have assertions but running CBMC never reaches them. Please can you make sure that it is actually reachable.

Also, minor pedantry, have you #include <assert.h>? One of the warnings suggest that you might not have done so.

[tautschnig]

@sepideha Would you be able to share the benchmark you are looking at? It is possible that work I'm doing on #5845 would address the problem, but it's really hard to tell without the code in front of us.

[sepideha]

Thanks all for the insights! Then it's very likely that the assertion is unreachable and thus VCC is zero but I am not sure if it's really the case since the original benchmark is 3k LOC and I don't have the minimal version.
I am sharing the original benchmark here.

[tautschnig]

It seems those lines invoking ldv_error are never reached. You can check this by adding --cover locations | egrep -w 'line (28|37|46)' to your command line, although the results are somewhat ambiguous as whoever pre-processed that file decided that duplicate line markers were a good idea.

[sepideha]

Thank you very much for your elaboration.

[sepideha]

Does CBMC differentiate between the "unreachable assertion" and "TRUE assertion via constant propagation"?
When we get VCC = 0 in cbmc, is there some debugging prints to show which category was it?

[tautschnig]

The "unreachable" part might even require further distinguishing: there is the case of symbolic execution not even simulating the assertion (because constant propagation helped determine that a branch towards the assertion couldn't be taken, or perhaps there isn't even a control-flow path to the assertion), or the SAT solver determining unreachability. These cases can be distinguished using coverage reports:

• --symex-coverage-report will tell you about instructions seen/not seen by symbolic execution.
• --cover location will tell you about instructions determined (un)reachable with the help of the SAT solver.

Once you have determined (via the above) that an instruction is reachable, the "SUCCESS" label in CBMC's usual output tells you about the assertion being valid (under a given loop unwinding).

It may be desirable to have CBMC answer all these questions in a single run, but we don't currently have provisions for that. Given the cost of coverage checking is quite substantial (a lot more SAT solver invocations are required), however, I'm not sure it's desirable to merge all these.

[sepideha]

Thanks again for the thorough response!

[hannes-steffenhagen-diffblue]

I believe the question has been sufficiently addressed for now, so I'm closing this. @sepideha feel free to ask any further follow up questions in a new ticket.