Broken array representation with theory-of-heaps.

[woosh]

This issue is about problems with the theory of heaps representation of arrays.

Two different command lines are used throughout this report. One is using option -mathArrays the other is not.

tri -mathArrays -cex -dev arrays.c

tri -cex -dev arrays.c

Arrays of scalars

// Example 1 - Working  
void main() {
    int arr[3];
    int old;

    assume(arr[2] >= 10);
    assume(old == arr[2]);
    
    arr[2] = arr[2] * 2;

    assert(arr[2] == old * 2);
}

Example 1 works with both command lines.

// Example 2a - Working  with option -mathArrays
void main(void) {
    int arr[3];
    int old_arr[3];

    assume(arr[2] >= 10);
    assume(old_arr == arr);
    
    arr[2] = arr[2] * 2;

    assert(arr[2] == old_arr[2] * 2);
}

// Example 2b - Working  with option -mathArrays
void main(void) {
    int arr[3];
    int old_arr[3];

    assume(old_arr[0] == arr[0]);
    assume(old_arr[1] == arr[1]);
    assume(old_arr[2] == arr[2]);
    assume(arr[2] >= 10);
    
    arr[2] = arr[2] * 2;

    assert(arr[2] == old_arr[2] * 2);
    assert(arr[1] == old_arr[1]);
}

Either of Example 2a or 2b gives the expected SAFE result only with -mathArrays option. Without -mathArrays the result in both cases (with a minor difference in predicate names) is

Warning: The following clause has different terms with the same name (term: _)
main23_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(_), 3)), arr:20, newAddrRange(batchAlloc(emptyHeap, O_Int(_), 3))) :- @h = emptyHeap & @h = newBatchHeap(batchAlloc(emptyHeap, O_Int(_), 3)) & arr:20 = newAddrRange(batchAlloc(emptyHeap, O_Int(_), 3)).

Warning: The following clause has different terms with the same name (term: @h)
main23_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(_), 3)), arr:20, newAddrRange(batchAlloc(emptyHeap, O_Int(_), 3))) :- @h = emptyHeap & @h = newBatchHeap(batchAlloc(emptyHeap, O_Int(_), 3)) & arr:20 = newAddrRange(batchAlloc(emptyHeap, O_Int(_), 3)).


------------------------------------------------------------------------------------------------------------------------------------------
Init:
             main23_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(10), 3)), AddrRange(nthAddr(1), 3), AddrRange(nthAddr(1), 3))              
------------------------------------------------------------------------------------------------------------------------------------------
                                                                    |                                                                     
                                                                    |                                                                     
                                                                    V                                                                     
 main_2(newHeap(alloc(newBatchHeap(batchAlloc(emptyHeap, O_Int(10), 2)), O_Int(20))), AddrRange(nthAddr(1), 3), AddrRange(nthAddr(1), 3)) 
------------------------------------------------------------------------------------------------------------------------------------------
Final:
 main_2(newHeap(alloc(newBatchHeap(batchAlloc(emptyHeap, O_Int(10), 2)), O_Int(20))), AddrRange(nthAddr(1), 3), AddrRange(nthAddr(1), 3)) 
------------------------------------------------------------------------------------------------------------------------------------------
Failed assertion:
false :- main_2(@h, arr:20, old_arr:21), getInt(read(@h, nthAddrRange(arr:20, 2))) != 2*getInt(read(@h, nthAddrRange(old_arr:21, 2))). (line:31 col:5) (property: user-assertion)

UNSAFE

I have to admit that the meaning of assume(old_arr == arr) in Example 2a is a bit unclear. Does it mean that all elements in the array are assumed to be equal (seems to be the case with -mathArrays) or does it mean that the addresses of the arrays are equal (which would be the natural interpretation in C)? While this ambiguity is removed in Example 2b, the result without the -mathArrays option is the same. As mentioned above, with -mathArrays both examples produces SAFE result, although with different solutions.

If Example 2b is changed slightly, to

// Example 3 - Working
void main(void) {
    int arr[3] = malloc(3*sizeof(int)); // Not valid C!
    int old_arr[3] = malloc(3*sizeof(int)); // Not valid C!

    assume(old_arr[0] == arr[0]);
    assume(old_arr[1] == arr[1]);
    assume(old_arr[2] == arr[2]);
    assume(arr[2] >= 10);
    
    arr[2] = arr[2] * 2;

    assert(arr[2] == old_arr[2] * 2);
    assert(arr[1] == old_arr[1]);
}

Note the added malloc initialization statements. This gives the expected SAFE result with both command lines. I think this suggests that there is something strange going on with array initialization when modeled with the theory of heaps. Or rather, there is something missing when handling non-initialized arrays. (As a sidenote, Example 2a with similar modifications also gives SAFE with both command lines. However, without -mathArrays the assume(old_Arr == arr) seems to be interpreted in the C way and thus this assumption will always be false.)

A similar problem exists when working with arrays of struct types. However, as reported in issues #34, option -mathArrays throws an exception when used with struct types.

Trying yet another modification of Example 2b, this time with proper C array initialization:

// Example 4 - Not working
void main(void) {
    int arr[3] = {1,2,13};
    int old_arr[3] = {1,2,13};

    assume(old_arr[0] == arr[0]);
    assume(old_arr[1] == arr[1]);
    assume(old_arr[2] == arr[2]);
    assume(arr[2] >= 10);
    
    arr[2] = arr[2] * 2;

    assert(arr[2] == old_arr[2] * 2);
    assert(arr[1] == old_arr[1]);
}

again gives an UNSAFE result like the following

Warning: The following clause has different terms with the same name (term: @h)
main24_5(write(write(write(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 3)), nthAddrRange(newAddrRange(batchAlloc(emptyHeap, O_Int(0), 3)), 0), O_Int(1)), nthAddrRange(newAddrRange(batchAlloc(emptyHeap, O_Int(0), 3)), 1), O_Int(2)), nthAddrRange(newAddrRange(batchAlloc(emptyHeap, O_Int(0), 3)), 2), O_Int(13)), arr:20, newAddrRange(batchAlloc(emptyHeap, O_Int(0), 3))) :- @h = emptyHeap & @h = write(write(write(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 3)), nthAddrRange(newAddrRange(batchAlloc(emptyHeap, O_Int(0), 3)), 0), O_Int(1)), nthAddrRange(newAddrRange(batchAlloc(emptyHeap, O_Int(0), 3)), 1), O_Int(2)), nthAddrRange(newAddrRange(batchAlloc(emptyHeap, O_Int(0), 3)), 2), O_Int(13)) & arr:20 = newAddrRange(batchAlloc(emptyHeap, O_Int(0), 3)).


--------------------------------------------------------------------------------------------------------------------------------------------------------
Init:
 main24_5(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(1))), O_Int(2))), O_Int(13))), AddrRange(nthAddr(1), 3), AddrRange(nthAddr(1), 3)) 
--------------------------------------------------------------------------------------------------------------------------------------------------------
                                                                           |                                                                            
                                                                           |                                                                            
                                                                           V                                                                            
  main_4(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(1))), O_Int(2))), O_Int(26))), AddrRange(nthAddr(1), 3), AddrRange(nthAddr(1), 3))  
--------------------------------------------------------------------------------------------------------------------------------------------------------
Final:
  main_4(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(1))), O_Int(2))), O_Int(26))), AddrRange(nthAddr(1), 3), AddrRange(nthAddr(1), 3))  
--------------------------------------------------------------------------------------------------------------------------------------------------------
Failed assertion:
false :- main_4(@h, arr:20, old_arr:21), getInt(read(@h, nthAddrRange(arr:20, 2))) != 2*getInt(read(@h, nthAddrRange(old_arr:21, 2))). (line:31 col:5) (property: user-assertion)

UNSAFE

Example 4 can't be tested with -mathArrays since array initialization is not supported in that case.

Non-deterministic initialization

When working with option -mathArrays the _ can be used for non-deterministic initialization of arrays, like

// Example --
int zeroInit[3];        // This will be zero initialized.
int randomInit[3] = _ ; // This will be non-deterministically initialized.

void main(void) {
    int local1[3];      // This will be non-deterministically initialized.
    int local2[3] = _ ; // And so is this.
    ...
}

That is not the case when working without -mathArrays option, i.e using theory of heaps when modelling arrays. In this case it is not clear what either randomInit[3] == _ or local2[3] == _ mean, but they are treated differently than the statements without an initializer. The reason is clear in the in
CCReader.collectVarDecls(,,,,_):

tricera/src/tricera/concurrency/CCReader.scala

Line 1552 in 8128adc

(lhsVar, CCTerm(lhsVar.term, varDec.typ, srcInfo),

and forward. The cases Enondet and None differs in how CCHeapArrayPointer type is treated.

The expected behavior would be to either throw a "Not supported" error of some kind, or that it mirrors that of -mathArrays option.

[zafer-esen]

#36 explains why examples 2a and 2b were not working when using the default options, which is now fixed.

There are other sub-issues related to this issue, in particular the non-deterministic initialization of arrays (both with and without -mathArrays), so let's keep this issue open for now. We can either create other (sub-)issues for those, or document them here.

[woosh]

Great that the heap issue is fixed. I think we should create a new issue for the non-deterministic initialization of arrays in order to keep the issues separate and "clean". (It is confusing with "half done" issues.)