基于抽象域和数值熵协同的数值程序分析

Value range analysis based on abstract domain and value entropy

在软件日益丰富的信息时代,程序的正确性验证问题需要深入地研究。提出了基于抽象解释和数值熵协同的数值程序正确性分析方法。利用抽象解释理论框架对数值程序进行抽象解释分析,提取不变量的抽象域区间;在抽象域区间上进行数值熵运算;运行程序获取数值变量的实际取值,计算数值熵;将抽象域区间数值熵和实际数值熵信息进行对比分析,准确地判断程序的正确性等性质。单纯的抽象解释分析只可以近似得到数值变量的取值范围,而引入数值熵算法,在取值范围的基础上对程序静态分析的准确性进一步检验,同时也做到了对程序的正确性验证。通过C语言程序实例,对抽象解释基础上的熵值分析方法进行了验证,证明了该分析方法的可行性和正确性。

In the information age, software is highly dependent, thus the correctness of the program validation issues need to be further studied. This paper introduces the value range analysis method based on abstract interpretation and value information entropy. The value program is analyzed by the abstract interpretation which is an important method of the static analysis, to obtain the abstract interpretation domain. Then it calculates the value information entropy, and runs the program to get the real values, in order to calculate the entropy. It compares the domain＇s entropy with the values＇ entropy, to accurately judge the correctness of the program, etc. The abstract interpretation analysis can only acquire the scope of variables, by introducing the value information entropy, this paper can make further inspection of the program static analysis based on the value range, and also verifies the correctness of the program. Through validating this method with C program,it verifies the practicality and correctness of this method.