SV-COMP 2018: diff "CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr: Fixing `ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i`

[marek-trtik]

The goal is to fix the benchmark ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i in the CBMC version (left tool)

https://github.com/marek-trtik/cbmc/tree/sv-comp-2018-patches

The original CBMC version (right tool) is here:

https://github.com/tautschnig/cbmc/tree/sv-comp-2017

Here is the diff file:

diff_CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr.json.zip

And here is the CBMC package of SV-COMP 2017:

CBMC-sv-comp-2017.tar.gz

[lucasccordeiro]

I was able to reproduce this issue. I'm looking at the pointer-analysis code to try understanding how VCs related to bifields are actually encoded in CBMC. In particular, if we run:

$cbmc test-bitfields-1_true-valid-memsafety.i --pointer-check

Then all VCs are shown as SUCCESS, but there are 4 that fail and are not shown in the results:

** Results:
[main.pointer_dereference.1] dereference failure: pointer NULL in *p: SUCCESS
[main.pointer_dereference.2] dereference failure: pointer invalid in *p: SUCCESS
[main.pointer_dereference.3] dereference failure: deallocated dynamic object in *p: SUCCESS
[main.pointer_dereference.4] dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.5] dereference failure: pointer outside dynamic object bounds in *p: SUCCESS
[main.pointer_dereference.6] dereference failure: pointer outside object bounds in *p: SUCCESS
[main.pointer_dereference.7] dereference failure: pointer NULL in *p: SUCCESS
[main.pointer_dereference.8] dereference failure: pointer invalid in *p: SUCCESS
[main.pointer_dereference.9] dereference failure: deallocated dynamic object in *p: SUCCESS
[main.pointer_dereference.10] dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.11] dereference failure: pointer outside dynamic object bounds in *p: SUCCESS
[main.pointer_dereference.12] dereference failure: pointer outside object bounds in *p: SUCCESS
[main.precondition_instance.1] free argument must be dynamic object: SUCCESS
[main.precondition_instance.2] free argument has offset zero: SUCCESS
[main.pointer_dereference.13] dereference failure: pointer NULL in *p: SUCCESS
[main.pointer_dereference.14] dereference failure: pointer invalid in *p: SUCCESS
[main.pointer_dereference.15] dereference failure: deallocated dynamic object in *p: SUCCESS
[main.pointer_dereference.16] dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.17] dereference failure: pointer outside dynamic object bounds in *p: SUCCESS
[main.pointer_dereference.18] dereference failure: pointer outside object bounds in *p: SUCCESS
[main.pointer_dereference.19] dereference failure: pointer NULL in *p: SUCCESS
[main.pointer_dereference.20] dereference failure: pointer invalid in *p: SUCCESS
[main.pointer_dereference.21] dereference failure: deallocated dynamic object in *p: SUCCESS
[main.pointer_dereference.22] dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.23] dereference failure: pointer outside dynamic object bounds in *p: SUCCESS
[main.pointer_dereference.24] dereference failure: pointer outside object bounds in *p: SUCCESS
[main.precondition_instance.3] free argument must be dynamic object: SUCCESS
[main.precondition_instance.4] free argument has offset zero: SUCCESS
[main.pointer_dereference.25] dereference failure: pointer NULL in *p: SUCCESS
[main.pointer_dereference.26] dereference failure: pointer invalid in *p: SUCCESS
[main.pointer_dereference.27] dereference failure: deallocated dynamic object in *p: SUCCESS
[main.pointer_dereference.28] dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.29] dereference failure: pointer outside dynamic object bounds in *p: FAILURE
[main.pointer_dereference.30] dereference failure: pointer outside object bounds in *p: SUCCESS
[main.pointer_dereference.31] dereference failure: pointer NULL in *p: SUCCESS
[main.pointer_dereference.32] dereference failure: pointer invalid in *p: SUCCESS
[main.pointer_dereference.33] dereference failure: deallocated dynamic object in *p: SUCCESS
[main.pointer_dereference.34] dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.35] dereference failure: pointer outside dynamic object bounds in *p: FAILURE
[main.pointer_dereference.36] dereference failure: pointer outside object bounds in *p: SUCCESS
[main.precondition_instance.5] free argument must be dynamic object: SUCCESS
[main.precondition_instance.6] free argument has offset zero: SUCCESS
[main.pointer_dereference.37] dereference failure: pointer NULL in *p: SUCCESS
[main.pointer_dereference.38] dereference failure: pointer invalid in *p: SUCCESS
[main.pointer_dereference.39] dereference failure: deallocated dynamic object in *p: SUCCESS
[main.pointer_dereference.40] dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.41] dereference failure: pointer outside dynamic object bounds in *p: FAILURE
[main.pointer_dereference.42] dereference failure: pointer outside object bounds in *p: SUCCESS
[main.pointer_dereference.43] dereference failure: pointer NULL in *p: SUCCESS
[main.pointer_dereference.44] dereference failure: pointer invalid in *p: SUCCESS
[main.pointer_dereference.45] dereference failure: deallocated dynamic object in *p: SUCCESS
[main.pointer_dereference.46] dereference failure: dead object in *p: SUCCESS
[main.pointer_dereference.47] dereference failure: pointer outside dynamic object bounds in *p: FAILURE
[main.pointer_dereference.48] dereference failure: pointer outside object bounds in *p: SUCCESS
[main.precondition_instance.7] free argument must be dynamic object: SUCCESS
[main.precondition_instance.8] free argument has offset zero: SUCCESS
[main.precondition_instance.9] free argument must be dynamic object: SUCCESS
[main.precondition_instance.10] free argument has offset zero: SUCCESS
[free.assertion.1] double free: SUCCESS
[free.assertion.2] free called for new[] object: SUCCESS

** 4 of 60 failed (2 iterations)
VERIFICATION FAILED

If we also look at the results of CBMC v5.7, both versions produce the same amount of VCs:

Generated 67 VCC(s), 18 remaining after simplification

However, CBMC v5.7 produces:

** 0 of 69 failed (1 iteration)

And CBMC v5.8 produces:

** 4 of 60 failed (2 iterations)

[peterschrammel]

Grep for FAILURE in the output. There are 4 failed properties shown in the list.

[lucasccordeiro]

This is the most reduced code that exposes the bug:

struct A {
        unsigned char a;
        unsigned char b:2;
        unsigned char c:2;
} __attribute__((packed));

int main(void)
{
        struct A *p;
        p = malloc(2);
        p->c = 3;
        if (p->c != 3) {
                free(p);
        }
        free(p);
}

These are the VCs that are failing:

[main.pointer_dereference.5] dereference failure: pointer outside dynamic object bounds in *p: FAILURE
[main.pointer_dereference.11] dereference failure: pointer outside dynamic object bounds in *p: FAILURE

I have also noted two main differences in CBMC v5.7 and v5.8 when analysing this benchmark:

(1) CBMC v5.7 uses partial Inlining (and CBMC v5.8 does not use it as default)
(2) CBMC v5.8 defines object and offset bits (and CBMC v5.7 does not define them)

Additionally, if we look at the VCCs of both versions, new variables (e.g., record_malloc, record_may_leak) are added to the set of constraints in CBMC v5.8.

[lucasccordeiro]

The VCs (in SSA form) produced by both versions (i.e., CBMC v5.7 and v5.8) look slightly different, mainly due to the fact that CBMC v5.8 defines object and offset bits; this has also led to a new model of the malloc function in ansi-c/library/stdlib.c. I was able to propose one fix for ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i related to an off-by-one, but it breaks one of our regression tests Pointer_byte_extract5 from the cbmc regression suite.

[lucasccordeiro]

Find below fragments of the SSA for both CBMC v5.7 (used in SV-COMP 2017) and CBMC v5.8 (which contains the patches of SV-COMP 2017), respectivelly:

CBMC v5.7, which produces the correct result:

-16} __CPROVER_malloc_object#2 == (record_malloc!0@1#1 ? (const void *)dynamic_object1 : NULL)
{-17} __CPROVER_malloc_size#2 == (record_malloc!0@1#1 ? 2ul : 0ul)
{-18} __CPROVER_malloc_is_new_array#2 == FALSE
{-19} __CPROVER_memory_leak#2 == (record_may_leak!0@1#1 ? (const void *)dynamic_object1 : NULL)
{-20} return_value_malloc$1!0@1#2 == (const void *)dynamic_object1
{-21} p!0@1#2 == (struct A *)dynamic_object1
{-22} dynamic_object1#1 == byte_extract_little_endian(byte_extract_little_endian(dynamic_object1#0, 0l, struct A) WITH [.c:=3], 0l, unsigned char [2ul])

CBMC v5.8, which produces the incorrect result:

{-16} record_malloc!0@1#2 == nondet_symbol(symex::nondet0)
{-17} __CPROVER_malloc_object#2 == (record_malloc!0@1#2 ? (const void *)dynamic_object1 : NULL)
{-18} __CPROVER_malloc_size#2 == (record_malloc!0@1#2 ? 2ul : 0ul)
{-19} __CPROVER_malloc_is_new_array#2 == FALSE
{-20} record_may_leak!0@1#2 == nondet_symbol(symex::nondet1)
{-21} __CPROVER_memory_leak#2 == (record_may_leak!0@1#2 ? (const void *)dynamic_object1 : NULL)
{-22} malloc#return_value!0#1 == (const void *)dynamic_object1
{-23} return_value_malloc$1!0@1#2 == (const void *)dynamic_object1
{-24} p!0@1#2 == (struct A *)dynamic_object1
{-25} dynamic_object1#1 == byte_extract_little_endian(byte_extract_little_endian(dynamic_object1#0, 0l, struct A) WITH [.c:=3], 0l, unsigned char [2ul])
|--------------------------

[peterschrammel]

Up to the assignment (-22/-25) things look correct. How does the property constraint look like? @lucasccordeiro, can you share the whole output please?

[lucasccordeiro]

@peterschrammel: Find attached the full SSA for both versions of CBMC. buggy.txt correct.txt

[peterschrammel]

@lucasccordeiro,

{1} !(POINTER_OBJECT(&dynamic_object1) == POINTER_OBJECT(CPROVER_malloc_object#2)) || CPROVER_malloc_size#2 >= 1ul

vs

{1} !(POINTER_OBJECT(&dynamic_object1) == POINTER_OBJECT(CPROVER_malloc_object#2)) || CPROVER_malloc_size#2 >= 3ul

looks very suspicous.

[lucasccordeiro]

@peterschrammel: I have tried to change the modelling of the malloc function in ansi-c/libraries/stdlib.c. Apparently, this change fixes the problem, but when I run the cbmc regresssion suite, then this test case fails Pointer_byte_extract5. I'll investigate it further.

[lucasccordeiro]

@peterschrammel and @tautschnig:

The following piece of code in src/util/pointer-predicates.cpp fixes the bug in the SV-COMP benchmark and keeps our regression:

exprt dynamic_object_upper_bound(
  const exprt &pointer,
  const typet &dereference_type,
  const namespacet &ns,
  const exprt &access_size)
{
  // this is
  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size

  exprt malloc_size=dynamic_size(ns);

  exprt object_offset=pointer_offset(pointer);

  exprt size=size_of_expr(dereference_type, ns);

  // need to add size
  exprt sum=plus_exprt(object_offset, size);
  if(ns.follow(sum.type())!=
     ns.follow(malloc_size.type()))
    sum.make_typecast(malloc_size.type());

  return binary_relation_exprt(sum, ID_gt, malloc_size);
}

There is something wrong with the previous code; in particular, the access_size variable, which does not seem to be set appropriately.

[lucasccordeiro]

I have just pushed this fix to your branch. The bug was fixed and still keep our regression.