基于符号执行框架分析了程序堆内存使用量的符号化上界.首先扩展了经典符号执行技术中的内存模型,针对堆内存分配与释放操作进行建模,维护堆内存的使用量信息,然后针对"平板循环"、带分支循环等常见循环结构给出了特殊处理策略,并采用程序切片技术缩减程序分析的规模.最后基于开源符号执行工具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.