精确的堆内存使用量上界分析

精确的堆内存使用量上界分析 Precise Heap Usage Bound Analysis 李仁见 LI Renjian1 1 first-author 刘万伟 LIU Wanwei2 2 王昭飞 WANG Zhaofei1 1 吴学光 WU Xueguang1 1 国防科技大学并行与分布处理国家重点实验室 国防科技大学并行与分布处理国家重点实验室 National Laboratory for Parallel and Distributed Processing,National University of Defense Technology National Laboratory for Parallel and Distributed Processing,National University of Defense Technology 国防科技大学计算机学院 国防科技大学计算机学院 College of Computer,National University of Defense Technology College of Computer,National University of Defense Technology 基于符号执行框架分析了程序堆内存使用量的符号化上界.首先扩展了经典符号执行技术中的内存模型,针对堆内存分配与释放操作进行建模,维护堆内存的使用量信息,然后针对"平板循环"、带分支循环等常见循环结构给出了特殊处理策略,并采用程序切片技术缩减程序分析的规模.最后基于开源符号执行工具KLEE设计实现了一个堆内存使用量上界分析原型工具.实验结果证明,该工具能够针对很多常见程序给出精确可靠的堆内存使用量上界. Symbolic heap bound is analyzed based on the symbolic execution framework.The memory model in classic symbolic execution is extended;and the heap allocation and free operations are specially modeled in order to model the change of heap usage.Special handling schema for flat loops and loops with conditional paths are also presented.Program slicing technique is adopted to reduce the scale of program analysis.A prototype tool for analyzing heap usage bound is also implemented based on the open source tools KLEE and the experimental results prove that it can get precise heap usage bounds for practical programs. 堆内存使用量上界 符号执行 循环处理 程序切片 heap usage bounds symbolic execution loop handling program slicing 10.14188/j.1671-8836.2011.06.002 TP333.1 国家自然科学基金资助项目（60725206,90818024） 2011-06-01 2021-04-01 6 57