I'm working with frama-c to make a dependency analysis of our code base and we have run into a situation that I have summarized in the following example.
We have a our entry point "runnable" for the analysis:
typedef unsigned char uint8;
typedef unsigned short uint16;
void ReadFunction(uint16 *const data);
extern uint16 test_return;
void runnable(void){
uint16 test_array[8];
ReadFunction(test_array);
test_return = test_array[4];
}
In our example we are using a local variable test_array[8] to read a value given by our ReadFunction and then taking only one value from that array (test_array[4]) and assigning it to the external value test_return.
Inside of ReadFunction the code is as follows:
typedef unsigned short uint16;
typedef uint16 custom_arr_type[8];
extern custom_arr_type test_interface;
extern void mem_copy(void * dst, const void * src, uint16 length);
void ReadFunction(uint16 *const data)
{
mem_copy(data, test_interface, sizeof(custom_arr_type));
}
where mem_copy is:
void mem_copy(void * dst,
const void * src,
uint16 length)
{
uint8 * d = (uint8 *)dst;
const uint8 * s = (const uint8 *)src;
uint16 i;
for (i = 0; i < (length); i++)
{
d[i] = s[i];
}
}
When analyzing the entrypoint runnable with the following command: frama-c -eva -deps -inout -lib-entry -no-annot -eva-initialized-locals -eva-auto-loop-unroll 10 -c11 example.i read_example.i lib_example.i -main runnable we produce the following output:
[kernel] Parsing example.i (no preprocessing)
[kernel] Parsing read_example.i (no preprocessing)
[kernel] Parsing lib_example.i (no preprocessing)
[eva] Analyzing an incomplete application starting at runnable
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
test_return ∈ [--..--]
test_interface[0..7] ∈ [--..--]
[eva] lib_example.i:21: starting to merge loop iterations
[eva] done for function runnable
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function mem_copy:
test_array[0..7] ∈ [--..--]
d ∈ {{ (uint8 *)&test_array }}
s ∈ {{ (uint8 const *)&test_interface }}
i ∈ [16..32767]
[eva:final-states] Values at end of function ReadFunction:
test_array[0..7] ∈ [--..--]
[eva:final-states] Values at end of function runnable:
test_return ∈ [--..--]
test_array[0..7] ∈ [--..--]
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
3 functions analyzed (out of 3): 100% coverage.
In these functions, 15 statements reached (out of 15): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
0 alarms generated by the analysis.
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
[from] Computing for function mem_copy
[from] Done for function mem_copy
[from] Computing for function ReadFunction
[from] Done for function ReadFunction
[from] Computing for function runnable
[from] Done for function runnable
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function mem_copy:
test_array[0..7] FROM test_interface[0..7]; dst; src; length (and SELF)
[from] Function ReadFunction:
test_array[0..7] FROM test_interface[0..7]; data (and SELF)
[from] Function runnable:
test_return FROM test_interface[0..7]
[from] ====== END OF DEPENDENCIES ======
[inout] InOut (internal) for function mem_copy:
Operational inputs:
test_interface[0..7]; dst; src; length
Operational inputs on termination:
test_interface[0..7]; dst; src; length
Sure outputs:
d; s; i
[inout] InOut (internal) for function ReadFunction:
Operational inputs:
test_interface[0..7]; data
Operational inputs on termination:
test_interface[0..7]; data
Sure outputs:
\nothing
[inout] InOut (internal) for function runnable:
Operational inputs:
test_array[4]; test_interface[0..7]
Operational inputs on termination:
test_array[4]; test_interface[0..7]
Sure outputs:
test_return
Now, the expected result here four our main function would be to have a dependency from test_return to test_interface[4] since it is my understanding that local variables like test_array will never appear in the dependency analysis. However, instead of having a dependency from one value of our array to our return value, we get a dependency from the whole array (test_interface[0..7]) to the return value.
I have tried simplifying even more this example, to rule out any possibility of the custom data types or the function calls to be causing this behavior:
int test_return;
int test_extern_array[8];
void runnable(void){
int test_array[8];
for (int i = 0; i < 8; i++){
test_array[i] = test_extern_array[i];
}
test_return = test_array[4];
}
Which produces the following output:
[kernel] Parsing example.i (no preprocessing)
[eva] Analyzing an incomplete application starting at runnable
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
test_return ∈ [--..--]
test_extern_array[0..7] ∈ [--..--]
[eva:loop-unroll] example.i:8: Automatic loop unrolling.
[eva] done for function runnable
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function runnable:
test_return ∈ [--..--]
test_array[0..7] ∈ [--..--]
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
1 function analyzed (out of 1): 100% coverage.
In this function, 10 statements reached (out of 10): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
0 alarms generated by the analysis.
----------------------------------------------------------------------------
No logical properties have been reached by the analysis.
----------------------------------------------------------------------------
[from] Computing for function runnable
[from] Done for function runnable
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function runnable:
test_return FROM test_extern_array[0..7]
[from] ====== END OF DEPENDENCIES ======
[inout] InOut (internal) for function runnable:
Operational inputs:
test_extern_array[0..7]; test_array[4]
Operational inputs on termination:
test_extern_array[0..7]; test_array[4]
Sure outputs:
test_return; i
And still in this case we obtain a dependency to our return value from the whole array instead of the specific position that has been used.
I have tried reading through all the frama-c manual and the eva plugin manual to find any cases similar to mine or any analysis option that could help get a more accurate dependency. I tried using the -eva-precision option but the results are the same.
Is frama-c correct here and I'm misinterpreting the results? Is there any way to get a more precise dependency for this case?
Yes (and no), and not currently.
Frama-C/Eva is correct, as in, sound (it does not "forget" to consider any possible value), but when the From plug-in is used, its result is less precise than what Eva computes itself. In particular, options such as -eva-auto-loop-unroll allow splitting different analysis contexts inside Eva (thus keeping maximum precision), but when the analysis terminates, results are consolidated by program point, per call stack, but not per loop iteration. That is, the different iterations inside a loop end up merged before From can get the information it needs from Eva, which explains why it shows the imprecise result. So, currently, it is not possible to get a more precise result.
Note that the analysis computed by From could nowadays be written as an Eva abstract domain, which would allow it to be more precise, since it would run "at the same time as" Eva itself. But that will require considerable time and effort.