improve the cbmc formal verification

[oreparaz]

There is a fantastic checklist we should use: https://github.com/model-checking/cbmc-starter-kit/blob/master/training-material/checklist.md

Also, we should totally use --unwinding-assertions:

• https://model-checking.github.io/cbmc-training/cbmc/overview/loop-unwinding.html#loop-unwinding-assertions
• https://github.com/model-checking/cbmc-starter-kit/wiki/Simple-proofs#unrolling-loops-soundly

[oreparaz]

Today the cbmc proof fails with --unwinding-assertions:

cbmc vrt_cbmc_harness.c ../../vrt.c     --function vrt_cbmc_harness     --unwind 5  --unwinding-assertions   --bounds-check     --pointer-check

[...] lots of output skipped [...]

Unwinding loop vrt_get_tag.5 iteration 4 file ../../vrt.c line 106 function vrt_get_tag thread 0
Not unwinding loop vrt_get_tag.5 iteration 5 file ../../vrt.c line 106 function vrt_get_tag thread 0
Unwinding loop vrt_get_tag.5 iteration 1 file ../../vrt.c line 106 function vrt_get_tag thread 0
Unwinding loop vrt_get_tag.5 iteration 2 file ../../vrt.c line 106 function vrt_get_tag thread 0
Unwinding loop vrt_get_tag.5 iteration 3 file ../../vrt.c line 106 function vrt_get_tag thread 0
Unwinding loop vrt_get_tag.5 iteration 4 file ../../vrt.c line 106 function vrt_get_tag thread 0
Not unwinding loop vrt_get_tag.5 iteration 5 file ../../vrt.c line 106 function vrt_get_tag thread 0
size of program expression: 29662 steps
simple slicing removed 752 assignments
Generated 10600 VCC(s), 2387 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
4523275 variables, 21764108 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
4523275 variables, 3686325 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
4523275 variables, 3436452 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
4523275 variables, 3353811 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 510.453s

** Results:
[memcmp.unwind.0] unwinding assertion loop 0: FAILURE
[vrt_get_tag.unwind.5] unwinding assertion loop 5: FAILURE
[vrt_verify_nonce.unwind.6] unwinding assertion loop 6: FAILURE
../../vrt.c function vrt_blob_init
[vrt_blob_init.pointer_dereference.1] line 38 dereference failure: pointer NULL in *b: SUCCESS
[vrt_blob_init.pointer_dereference.3] line 38 dereference failure: deallocated dynamic object in *b: SUCCESS
[vrt_blob_init.pointer_dereference.7] line 38 dereference failure: invalid integer address in *b: SUCCESS
[vrt_blob_init.pointer_dereference.6] line 38 dereference failure: pointer outside object bounds in *b: SUCCESS
[vrt_blob_init.pointer_dereference.5] line 38 dereference failure: pointer outside dynamic object bounds in *b: SUCCESS
[vrt_blob_init.pointer_dereference.4] line 38 dereference failure: dead object in *b: SUCCESS
[vrt_blob_init.pointer_dereference.2] line 38 dereference failure: pointer invalid in *b: SUCCESS

../../vrt.c function vrt_blob_r32
[vrt_blob_r32.pointer_dereference.7] line 46 dereference failure: invalid integer address in *((uint32_t **)(char *)((char

[...] lots of output skipped [...]

const char *)(const void *)srep->data + (signed long int)(__CPROVER_size_t)srep->size: SUCCESS
[__builtin___memcpy_chk.pointer.8] line 27 same object violation in (const char *)(void *)(msg + (signed long int)cert_sig->size) >= (const char *)(const void *)CONTEXT_CERT + (signed long int)(sizeof(const char [37l]) /*37ul*/  - (unsigned long int)1): SUCCESS
[__builtin___memcpy_chk.pointer.20] line 27 same object violation in (const char *)(void *)(msg + (signed long int)1) >= (const char *)(const void *)in + (signed long int)(__CPROVER_size_t)64: SUCCESS
[__builtin___memcpy_chk.pointer.22] line 27 same object violation in (const char *)(void *)(msg + (signed long int)1) >= (const char *)(const void *)left + (signed long int)(__CPROVER_size_t)nodesize: SUCCESS
[__builtin___memcpy_chk.pointer.2] line 27 same object violation in (const char *)(void *)out_query >= (const char *)(const void *)query_header + (signed long int)sizeof(const uint8_t [16l]) /*16ul*/ : SUCCESS
[__builtin___memcpy_chk.pointer.4] line 27 same object violation in (const char *)(void *)(out_query + (signed long int)sizeof(const uint8_t [16l]) /*16ul*/ ) >= (const char *)(const void *)nonce + (signed long int)(__CPROVER_size_t)64: SUCCESS

<builtin-library-memcmp> function memcmp
[memcmp.precondition.1] line 19 memcmp region 1 readable: SUCCESS
[memcmp.precondition.2] line 21 memcpy region 2 readable: SUCCESS
[memcmp.pointer_dereference.1] line 27 dereference failure: pointer NULL in *tmp_post: SUCCESS
[memcmp.pointer_dereference.2] line 27 dereference failure: pointer invalid in *tmp_post: SUCCESS
[memcmp.pointer_dereference.3] line 27 dereference failure: deallocated dynamic object in *tmp_post: SUCCESS
[memcmp.pointer_dereference.4] line 27 dereference failure: dead object in *tmp_post: SUCCESS
[memcmp.pointer_dereference.5] line 27 dereference failure: pointer outside dynamic object bounds in *tmp_post: SUCCESS
[memcmp.pointer_dereference.6] line 27 dereference failure: pointer outside object bounds in *tmp_post: SUCCESS
[memcmp.pointer_dereference.7] line 27 dereference failure: invalid integer address in *tmp_post: SUCCESS
[memcmp.pointer_dereference.8] line 27 dereference failure: pointer NULL in *tmp_post$0: SUCCESS
[memcmp.pointer_dereference.9] line 27 dereference failure: pointer invalid in *tmp_post$0: SUCCESS
[memcmp.pointer_dereference.10] line 27 dereference failure: deallocated dynamic object in *tmp_post$0: SUCCESS
[memcmp.pointer_dereference.11] line 27 dereference failure: dead object in *tmp_post$0: SUCCESS
[memcmp.pointer_dereference.12] line 27 dereference failure: pointer outside dynamic object bounds in *tmp_post$0: SUCCESS
[memcmp.pointer_dereference.13] line 27 dereference failure: pointer outside object bounds in *tmp_post$0: SUCCESS
[memcmp.pointer_dereference.14] line 27 dereference failure: invalid integer address in *tmp_post$0: SUCCESS

** 3 of 481 failed (4 iterations)
VERIFICATION FAILED

Sounds like we need to add a few __CPROVER_assume() to guide cbmc...