goto-instrument 5.84 crash when trying to use __CPROVER_pointer_in_range_dfcc contract #7760
Comments
|
Thanks, I'll take a look at the problem to diagnose it. |
|
Update: There's a superposition of issues:
In any case we should not trigger an assertion failure by using |
|
Thanks for the advice - I will update my code and try again. If the use of these contracts are specific to a particular context that can be automatically decided, then it seems just one contract will do, not two. Another piece of advice: Huffman code your name-space! e.g. the most frequently used contracts should have the shortest names, so are less typing for the user... |
|
OK... making progress now. Chaning to use __CPROVER_pointer_in_range fixes the crash, and I realized I had to tighten the upper-bound on my current_byte_ptr variable. See the latest commit to ar.c in the repo. above. I am now left with 2 FAILUREs: I don't understand the first one for sure... What is being checked? What's wrong? The loop body modifies 3 variables, and my "assigns" clause mentions all three of them. What did I do wrong? |
It checks if the assigns clause of the loop is included in the assigns clause of the function. That is, the loop should not write to any target that is not allowed to be written in the function. In this case, all three targets in the loop assigns are local targets and should not be checked in the inclusion check. It is a bug that we need to fix. Here is the minimal implementation of uint32_t arsum(const uint8_t *data, size_t num_blocks)
{
uint32_t sum = 0;
for(; num_blocks--;)
__CPROVER_assigns(num_blocks)
__CPROVER_loop_invariant(1==1)
{
}
return sum;
} |
|
|
Fix for the write set inclusion check #7763 |
|
OK... I switched to using a local variable for the loop counter rather than modifying the formal parameter. Good idea anyway - changing a scalar parameter is an abomination anyway... I now have 1 FAILURE left... on the loop invariant... but which one?!?! What is the exact sequencing of the loop invariant preservation check with respect to decrementing the loop counter the the evaluation of the condition that the loop exit? I agree that current_byte_ptr does get incremented once too many times, but that value is never dereferenced, so is that OK or not? |
|
Side effects of the guard are considered to be part of the loop (they are part of the natural loop in the control flow graph at the GOTO instruction level). The base case is checked before any of the guard's side effect take place, The step case and loop variant are checked after the very last instruction of the loop body. In the current form the invariant is too weak. To become inductive it needs to relate uint32_t arsum(const uint8_t *data, size_t num_blocks)
__CPROVER_requires(num_blocks >= 1)
__CPROVER_requires(__CPROVER_is_fresh(data, num_blocks * BLOCK_SIZE))
{
// Form uint32_t sum of bytes denoted by data.
// Counting in blocks of 4 bytes at a time.
uint8_t *current_byte_ptr = data;
const uint8_t *last_block_ptr = data + ((num_blocks - 1) * BLOCK_SIZE);
uint32_t sum = 0;
// current_byte_ptr should always be between data and last_block_ptr, so we
// should be able to assert...
__CPROVER_assert(__CPROVER_pointer_in_range(data, current_byte_ptr, last_block_ptr),
"Check current_byte_ptr initially in block range");
size_t num_blocks_old = num_blocks;
for(; num_blocks; num_blocks--)
__CPROVER_assigns(num_blocks, sum, current_byte_ptr)
__CPROVER_loop_invariant(num_blocks <= __CPROVER_loop_entry(num_blocks))
__CPROVER_loop_invariant(current_byte_ptr == (data + (__CPROVER_loop_entry(num_blocks) - num_blocks) * BLOCK_SIZE))
{
sum += *current_byte_ptr;
current_byte_ptr++;
sum += *current_byte_ptr;
current_byte_ptr++;
sum += *current_byte_ptr;
current_byte_ptr++;
sum += *current_byte_ptr;
current_byte_ptr++;
}
return sum;
}
void arsum_harness()
{
uint8_t *data;
uint32_t num_blocks;
uint32_t retval = arsum(data, num_blocks);
}You might need extra assumptions about the |
|
OK...I now have a version that proves OK. I have no idea what's going on with __CPROVER_loop_entry() there and the variable num_block_old .. it looks wrong to me! One thing also confused me... I need to have Why do I need the " * BLOCK_SIZE" there? I thought an addition of a pointer and an integer was automatically scaled in C? (Unless... num_blocks and blocks_to_go are both of type size_t, and automatic scaling is NOT applied when the RHS of the addition is size_t? Yuk!) I will commit and push my latest code now... |
|
Note - no need to worrying about overflow of the summation, since I am not using --unsigned-overflow-check. (I find this option strange anyway - unsigned types are supposed to overflow!) |
|
Sorry the
The unsigned overflow check is still worth using in general, as it catches cases where the result of an unsigned operation would wrap around unexpectedly, resulting for example in an allocation that is too small, an array index that is too large and would go out of bounds, etc. We usually keep all checks active but selectively disable them around operations using a pragma (cf https://diffblue.github.io/cbmc/cprover-manual/md_properties.html): #pragma CPROVER check push
#pragma CPROVER check disable "unsigned-overflow"
sum += *current_byte_ptr;
current_byte_ptr++;
sum += *current_byte_ptr;
current_byte_ptr++;
sum += *current_byte_ptr;
current_byte_ptr++;
sum += *current_byte_ptr;
current_byte_ptr++;
#pragma CPROVER pop |
I am using CBMC 5.84 on Apple M1 macOS.
I'm trying to verify a simple algorithms that loops over an array of data that is passed in as a parameter.
I think I need to use __CPROVER_pointer_in_range_dfcc to verify that my pointer(s) remain valid for the array of data that has been passed in to my function.
See https://github.com/rod-chapman/cbmc-examples/tree/main/arrays
In that directory,
yields
Any ideas where I went wrong?
The text was updated successfully, but these errors were encountered: