Feature request: Add support to Poison value #7014
Description
As a user, I would like to be able to verify that my program only reads initialized memory. For example, I should be able to verify that the following testcase reads uninitialized memory:
// undef.c
struct Two {
int first;
int second;
};
int equal(struct Two* obj) {
return obj->first == obj->second;
}
int main() {
struct Two object;
return equal(&object);
}CBMC's verification in the example above succeeds.
$ cbmc --bounds-check --pointer-check --memory-leak-check --div-by-zero-check --pointer-overflow-check --conversion-check --undefined-shift-check --nan-check --enum-range-check --pointer-primitive-check --signed-overflow-check --unsigned-overflow-check undef.c
CBMC version 5.61.0 (cbmc-5.61.0) 64-bit x86_64 linux
Parsing undef.c
Converting
Type-checking undef
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
Runtime Symex: 0.00119599s
size of program expression: 48 steps
simple slicing removed 0 assignments
Generated 13 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 1.631e-05s
** Results:
function __CPROVER__start
[__CPROVER__start.memory-leak.1] dynamically allocated memory never freed in __CPROVER_memory_leak == NULL: SUCCESS
undef.c function equal
[equal.pointer_dereference.1] line 7 dereference failure: pointer NULL in obj->first: SUCCESS
[equal.pointer_dereference.2] line 7 dereference failure: pointer invalid in obj->first: SUCCESS
[equal.pointer_dereference.3] line 7 dereference failure: deallocated dynamic object in obj->first: SUCCESS
[equal.pointer_dereference.4] line 7 dereference failure: dead object in obj->first: SUCCESS
[equal.pointer_dereference.5] line 7 dereference failure: pointer outside object bounds in obj->first: SUCCESS
[equal.pointer_dereference.6] line 7 dereference failure: invalid integer address in obj->first: SUCCESS
[equal.pointer_dereference.7] line 7 dereference failure: pointer NULL in obj->second: SUCCESS
[equal.pointer_dereference.8] line 7 dereference failure: pointer invalid in obj->second: SUCCESS
[equal.pointer_dereference.9] line 7 dereference failure: deallocated dynamic object in obj->second: SUCCESS
[equal.pointer_dereference.10] line 7 dereference failure: dead object in obj->second: SUCCESS
[equal.pointer_dereference.11] line 7 dereference failure: pointer outside object bounds in obj->second: SUCCESS
[equal.pointer_dereference.12] line 7 dereference failure: invalid integer address in obj->second: SUCCESS
** 0 of 13 failed (1 iterations)
VERIFICATION SUCCESSFUL
While `valgrind` is able to detect an error.
$ clang undef.c -o undef && valgrind --track-origins=yes ./undef
==5651== Memcheck, a memory error detector
==5651== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==5651== Using Valgrind-3.13.0 and LibVEX; rerun with -h for copyright info
==5651== Command: ./undef
==5651==
==5651== Syscall param exit_group(status) contains uninitialised byte(s)
==5651== at 0x4F22AB6: _Exit (_exit.c:31)
==5651== by 0x4E81101: __run_exit_handlers (exit.c:132)
==5651== by 0x4E81129: exit (exit.c:139)
==5651== by 0x4E5FC8D: (below main) (libc-start.c:344)
==5651== Uninitialised value was created by a stack allocation
==5651== at 0x4004A0: main (in /tmp/undef)
==5651==
==5651==
==5651== HEAP SUMMARY:
==5651== in use at exit: 0 bytes in 0 blocks
==5651== total heap usage: 0 allocs, 0 frees, 0 bytes allocated
==5651==
==5651== All heap blocks were freed -- no leaks are possible
==5651==
==5651== For counts of detected and suppressed errors, rerun with: -v
==5651== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 0 from 0)
For that, it would be great if CBMC could:
- Allow users to model uninitialized memory with
poisonvalue. - Allow users explicitly assign
poisonto a variable in their proof harnesses. - Explicitly check for
poison.