Description
CBMC version: 5.67.0
Operating system: N/A
Problem description
History variables in loop contracts (maybe also in function contracts?) only make shallow copies. This is sufficient for scalars, but arrays and pointers may require a deep copy, like in the example below.
Example
This example shows a case where we wrote function contracts to specify the behavior of the loop. However, the term __CPROVER_loop_entry(listData)[j-1] requires a deep copy of the listData array.
This example is a simplified version of one of the loop contracts I was trying to write for the FreeRTOS Task-Scheduler, but couldn't write, since there was no support for this feature. Further, this feature will likely be necessary for any kind of unbounded functional correctness proofs.
#include <stdlib.h>
main() {
// A 1d array of integer pointers.
int ** listData = (int **) malloc (4 * sizeof(int *));
if (listData == NULL){
exit(1);
}
//Each integer pointer points to a single integer.
int b1;
int b2;
listData[0] = &b1;
listData[1] = &b2;
// Move all elements to the left by 1
for (int i = 1 ; i < 4; i++)
__CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(listData))
__CPROVER_loop_invariant(i>=1 && i<=4)
__CPROVER_loop_invariant(__CPROVER_forall { int j;
(1 <= j && j <= 4) ==>
( (j >= i) ==> (listData[j-1]==__CPROVER_loop_entry(listData)[j-1]) )
})
__CPROVER_loop_invariant(__CPROVER_forall { int j;
(1 <= j && j <= 3) ==>
((j < i) ==>(listData[j-1]==__CPROVER_loop_entry(listData)[j]))
})
__CPROVER_decreases (4-i)
{
listData[i-1] = listData[i];
}
assert(listData[0] == &b2);
}
Challenges
- Deep copies are expensive. They can potentially touch a large amount of memory.
- Since C supports type-casting and type-unsafe code, it may be hard to compute the correct deep-copy. For example, we cannot deep copy of a (void *) pointer because we don't know how many bytes to copy.
Possible practical compromise
A practical compromise could be to add new syntax (similar to the __CPROVER_POINTER_OBJECT(listData) from the assigns clause, which performs a 1-level deep havoc) to do a 1-level deep copy, and reject code where we cannot figure out what the deep copy should be (like for a (void*) pointer). This will be sufficient for the example above.
However, this is not the perfect solution since we can construct cases where we need deep copies up to more levels. But this may be the best we can do to avoid the challenges listed above.