Extend stackpointer support

[woosh]

Currently TriCera does not support ACSL contracts together with functions where calls to the function involves arguments that are pointers to data on the stack. It would be valuable to add support for this to permit a wider set of usecases, typically for embedded real-time applications where heap allocation is avoided.

Problem illustration

Below is a code snippet to illustrate the problem. The idea is that there is a large data structure that keeps some common state. A function (incr) modifies this state. However, in order to, among other things, have a well defined interface, the function acts upon a structure allocated on the stack instead of the global structure directly.

typedef struct {
    unsigned int val1;
    int val2;
    long int val3;
    /* a lot more values goes here ... */
} tLargeDataSet;

typedef struct {
    unsigned int val;
    /* some other values goes here */
} tMyStruct;
 
void incr(tMyStruct* s) {
    s->val++;
}

/* Think about this as a large set of common data. */
tLargeDataSet g_commonData;

 
/*@
    requires g_commonData.val1 <= 1000;
    requires g_commonData.val1 >= 0;

    assigns g_commonData;
 
    ensures g_commonData.val1 == \old(g_commonData.val1) + 1;
*/
int main() {
    tMyStruct myStruct;
 
    myStruct.val = g_commonData.val1;
 
    incr(&myStruct);

    g_commonData.val1 = myStruct.val;
 
    return 0;
}

Possible solution

One solution would be to let TriCera, during e.g. parsing or some other pass over the code, create the equivalent of the following snippet. The idea is to, in addition to the original function, construct a similar function (g_incr) acting on global variables instead of function pointer arguments, and at the call site "replace" the call to the original function with a call to the constructed function plus some book-keeping assignments. Of course, in the general case we still want to keep the original function around in case there are also calls where the heap is involved.

typedef struct {
    unsigned int val1;
    int val2;
    long int val3;
    /* a lot more values goes here ... */
} tLargeDataSet;

typedef struct {
    unsigned int val;
    /* some other values goes here */
} tMyStruct;
 
void incr(tMyStruct* s) {
    s->val++;
}

/* Constructed function with pointer arguments replaced by global variables specific to this function. */
tMyStruct g_incr_myStruct;
void g_incr() {
    g_incr_myStruct.val++;
}

/* Think about this as a large set of common data. */
tLargeDataSet g_commonData;

 
/*@
    requires g_commonData.val1 <= 1000;
    requires g_commonData.val1 >= 0;

    assigns g_commonData;
 
    ensures g_commonData.val1 == \old(g_commonData.val1) + 1;
*/
int main() {
    tMyStruct myStruct;
 
    myStruct.val = g_commonData.val1;
 
    tMyStruct saved_myStruct = g_incr_myStruct;  /* Needed in the general case to allow for recursion */
    g_incr_myStruct = myStruct;
    g_incr();
    myStruct = g_incr_myStruct;
    g_incr_myStruct = saved_myStruct;

    g_commonData.val1 = myStruct.val;
 
    return 0;
}

This suggested solution would still have some limitations with regards to e.g. aliasing.

Another option

Another option would be to, in a similar but reverse fashion, at the call site copy stack allocated data into a structure allocated on the heap, and then call the original function with the heap allocated data structure. While this would solve issues with aliasing, it may not be as straight forward to handle the contract.

[zafer-esen]

Thank you for the issue and the detailed explanation @woosh.

We should probably go with the first option for easier contracts as you stated. Using heaps for this purpose might also not be ideal in terms of solving, as TriCera will check for the memory safety of stack pointer accesses (when that property is being checked), which is implicit in the first solution.

[zafer-esen]

Created #24 to address this issue.