Incorrect FALSE related to pointer outside dynamic object bounds

[lucasccordeiro]

./cbmc --graphml-witness witness.graphml --32 --propertyfile ../../sv-benchmarks/c/MemSafety.prp ../../sv-benchmarks/c/array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i

State 56 file ../../sv-benchmarks/c/array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i line 547 function cmemrchr thread 0
----------------------------------------------------
  cp=dynamic_object1 + -1 (00000000010111111111111111111111)

Violated property:
  file ../../sv-benchmarks/c/array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i line 547 function cmemrchr
  dereference failure: pointer outside dynamic object bounds in *cp
  !(POINTER_OBJECT(cp) == POINTER_OBJECT(__CPROVER_malloc_object)) || POINTER_OFFSET(cp) >= 0 && __CPROVER_malloc_size >= (unsigned int)POINTER_OFFSET(cp) + 1u

VERIFICATION FAILED
EC=10
FALSE(valid-deref)

[lucasccordeiro]

In this benchmark openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination from array-memsafety, if we replace the nondet functions:

int main() {
  int length = __VERIFIER_nondet_int();
  int n = __VERIFIER_nondet_int();
  int c = __VERIFIER_nondet_int();
  if (length < 1) {
      length = 1;
  }
  if (n < 1) {
      n = 1;
  }
  char* nondetArea = (char*) alloca(n * sizeof(char));
  cmemrchr(nondetArea, c, n);
  return 0;
}

by the concrete values:

int main() {
  int length = 8388608;
  int n = 2097152;
  int c = 0;
  if (length < 1) {
      length = 1;
  }
  if (n < 1) {
      n = 1;
  }
  char* nondetArea = (char*) alloca(n * sizeof(char));
  cmemrchr(nondetArea, c, n);
  return 0;
}

Then run Valgrind:

Lucass-MacBook-Pro:array-memsafety lucasccordeiro$ valgrind --tool=memcheck --leak-check=yes --leak-check=full --show-leak-kinds=all ./a.out 
==3830== Memcheck, a memory error detector
==3830== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==3830== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
==3830== Command: ./a.out
==3830== 
==3830== Warning: client switching stacks?  SP change: 0x104802880 --> 0x104602880
==3830==          to suppress, use: --max-stackframe=2097152 or greater
==3830== Invalid write of size 8
==3830==    at 0x100000F4E: main (in ./a.out)
==3830==  Address 0x104602878 is on thread 1's stack
==3830==  in frame #0, created by main (???:)
==3830== 
==3830== Conditional jump or move depends on uninitialised value(s)
==3830==    at 0x100000E8B: cmemrchr (in ./a.out)
==3830==    by 0x100000F52: main (in ./a.out)
==3830== 
==3830== Invalid read of size 8
==3830==    at 0x100000ECF: cmemrchr (in ./a.out)
==3830==    by 0x10013E5C8: start (in /usr/lib/system/libdyld.dylib)
==3830==  Address 0x104602878 is on thread 1's stack
==3830==  in frame #0, created by cmemrchr (???:)
==3830== 
==3830== Warning: client switching stacks?  SP change: 0x104602880 --> 0x1048028b0
==3830==          to suppress, use: --max-stackframe=2097200 or greater
==3830== 
==3830== HEAP SUMMARY:
==3830==     in use at exit: 34,850 bytes in 414 blocks
==3830==   total heap usage: 514 allocs, 100 frees, 41,826 bytes allocated
==3830== 
==3830== LEAK SUMMARY:
==3830==    definitely lost: 0 bytes in 0 blocks
==3830==    indirectly lost: 0 bytes in 0 blocks
==3830==      possibly lost: 0 bytes in 0 blocks
==3830==    still reachable: 0 bytes in 0 blocks
==3830==         suppressed: 34,850 bytes in 414 blocks
==3830== 
==3830== For counts of detected and suppressed errors, rerun with: -v
==3830== Use --track-origins=yes to see where uninitialised values come from
==3830== ERROR SUMMARY: 3 errors from 3 contexts (suppressed: 15 from 15)

We can see that there is undefined behaviour. In particular, the call to function __bultin_alloca fails at line 563 to allocate memory (i.e., returns null pointer), which then causes in the function cmemrchr at line 547 to dereference pointer to not allocated memory leading to undefined behaviour.

[lucasccordeiro]

@peterschrammel and @tautschnig: @marek-trtik and I have discussed about this issue (see report above). Since SV-COMP assumes that memory allocation never fails, it will be hard to exclude this benchmark from the evaluation. What do you think?

[tautschnig]

Would you nevertheless file an issue to kick off some discussion? The rules are questionable for malloc already, but doing an unbounded stack allocation (alloca) will fail on all systems (and you have concrete proof thereof). This benchmark should be modified to bound this with some reasonable number.

[lucasccordeiro]

I have just created an issue for discussion in https://github.com/sosy-lab/sv-benchmarks/issues/550.

[marek-trtik]

Please, consider also this "proof" of undefined behaviour (but frankly, it is really extreme solution; I do not like it myself):

1. At line 555 __VERIFIER_nondet_int returns 1, i.e. the size n of the memory to be allocated is 1.
2. At line 563 the __builtin_alloca returns the highest possible address on 32-bit platform which is 2^32-1=4294967295. At that address there is allocated our byte.
3. In function cmemrchr at line 545 there we compute address of pointer cp to be 2^32-1 + 1. According to standard pointer types are not integers, so we cannot say that overflow will occur, i.e. cp does not have to be 0. Instead, the pointer points behind the addressable space, which is an invalid value, perhaps without any representation (implementation specific).
   4. At line 547, the decrement of the pointer cp cannot fix the invalid value in cp, so the pointer is still invalid.
   5. The dereference of the invalid pointer cp at line 547 leads to an undefined behaviour.

[tautschnig]

Overflow on pointers is undefined behaviour: C11 6.5.6, paragraph 8 (If both the pointer operand and the result point to elements of the same array object, or one past the last element of the array object, the evaluation shall not produce an overflow; otherwise, the behavior is undefined.) Would you mind posting your analysis to the sv-benchmarks issue?

[marek-trtik]

@tautschnig : I am not 100% sure that the pointer overflow really applies here, because of the sentence you wrote:

... or one past the last element of the array object, ...

This is exactly what happen in the "proof" above. The pointer cp will indeed point to the byte one past the last element of the array. But the problem is, that no such byte exists, because the address in cp will point to behind the end of the addressable space. If we can say that address 0 is correct address one past the address 2^32-1, then no overflow occurs. Otherwise, we get pointer overflow and undefined behaviour.

Anyway, I far as I remember, the standard does not say that pointer types must be integer types. In that case the term overflow might be completely irrelevant. Nevertheless, the fact is that the "proof" above computes address behind the end of the addressable space, which might lead to invalid address.

[marek-trtik]

Shell I report the "proof" above to sosy-lab as is, or should I reformulate it in terms of overflow? In the second case we should first clarify, whether address 0 is the correct address one past 2^32-1 or not.

[tautschnig]

I’d raise both problems - it’s not clear to me how to interpret the standard in that sentence: does the “shall” mean that it should not be viewed as an overflow, or that it must not occur? I don’t know.