错误的依赖性：仅使用一个值时整个数组的依赖性
Wrong dependency: Dependency from whole array when only one value is being used
我正在使用 frama-c 对我们的代码库进行依赖性分析，我们已经 运行 进入了我在以下示例中总结的情况。
我们有一个入口点“运行nable”用于分析：
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];
}
在我们的示例中，我们使用局部变量 test_array[8] 来读取我们的 ReadFunction 给出的值然后只从该数组中取一个值 (test_array[4]) 并将其分配给外部值 test_return.
ReadFunction内部代码如下：
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));
}
其中 mem_copy 是：
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];
}
}
分析入口点运行nable时使用以下命令：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 运行nable 我们产生以下输出：
[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
现在，我们的主要函数的预期结果是从 test_return 到 test_interface[4 ] 因为据我了解像test_array这样的局部变量永远不会出现在依赖分析中。但是，我们不是从数组的一个值到 return 值的依赖性，而是从整个数组 (test_interface[0..7]) 到 return 值。
我已尝试进一步简化此示例，以排除自定义数据类型或函数调用导致此行为的任何可能性：
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];
}
产生以下输出：
[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
在这种情况下，我们仍然从整个数组而不是已使用的特定位置获得对 return 值的依赖。
我已经尝试通读所有 frama-c 手册和 eva 插件手册，以找到任何与我相似的案例或任何有助于获得更准确依赖性的分析选项。我尝试使用 -eva-precision 选项，但结果是一样的。
此处的 frama-c 是否正确，我误解了结果？
对于这种情况，有什么办法可以得到更精确的依赖关系吗？
有（也没有），目前没有。
Frama-C/Eva 是 correct，如 sound（它不会“忘记”考虑任何可能的值） ，但是当使用 From plug-in 时，其结果不如 Eva 自己计算的结果精确。特别是，-eva-auto-loop-unroll 等选项允许在 inside Eva 中拆分不同的分析上下文（从而保持最大精度），但是当分析终止时，每次调用都会按程序点合并结果堆栈，但不是每次循环迭代。也就是说，在 From 可以从 Eva 获得所需信息之前，循环内的不同迭代最终合并，这解释了为什么它显示不精确的结果。因此，目前无法获得更精确的结果。
请注意，From 计算的分析现在可以写成 Eva 抽象域，这将使它更加精确，因为它 运行 与 Eva 本身“同时”。但这需要相当多的时间和精力。
我正在使用 frama-c 对我们的代码库进行依赖性分析，我们已经 运行 进入了我在以下示例中总结的情况。
我们有一个入口点“运行nable”用于分析：
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];
}
在我们的示例中，我们使用局部变量 test_array[8] 来读取我们的 ReadFunction 给出的值然后只从该数组中取一个值 (test_array[4]) 并将其分配给外部值 test_return.
ReadFunction内部代码如下：
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));
}
其中 mem_copy 是：
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];
}
}
分析入口点运行nable时使用以下命令：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 运行nable 我们产生以下输出：
[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
现在，我们的主要函数的预期结果是从 test_return 到 test_interface[4 ] 因为据我了解像test_array这样的局部变量永远不会出现在依赖分析中。但是，我们不是从数组的一个值到 return 值的依赖性，而是从整个数组 (test_interface[0..7]) 到 return 值。
我已尝试进一步简化此示例，以排除自定义数据类型或函数调用导致此行为的任何可能性：
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];
}
产生以下输出：
[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
在这种情况下，我们仍然从整个数组而不是已使用的特定位置获得对 return 值的依赖。
我已经尝试通读所有 frama-c 手册和 eva 插件手册，以找到任何与我相似的案例或任何有助于获得更准确依赖性的分析选项。我尝试使用 -eva-precision 选项，但结果是一样的。
此处的 frama-c 是否正确，我误解了结果？ 对于这种情况，有什么办法可以得到更精确的依赖关系吗？
有（也没有），目前没有。
Frama-C/Eva 是 correct，如 sound（它不会“忘记”考虑任何可能的值） ，但是当使用 From plug-in 时，其结果不如 Eva 自己计算的结果精确。特别是，-eva-auto-loop-unroll 等选项允许在 inside Eva 中拆分不同的分析上下文（从而保持最大精度），但是当分析终止时，每次调用都会按程序点合并结果堆栈，但不是每次循环迭代。也就是说，在 From 可以从 Eva 获得所需信息之前，循环内的不同迭代最终合并，这解释了为什么它显示不精确的结果。因此，目前无法获得更精确的结果。
请注意，From 计算的分析现在可以写成 Eva 抽象域，这将使它更加精确，因为它 运行 与 Eva 本身“同时”。但这需要相当多的时间和精力。