Partitioned Memory Models for Program Analysis
Partitioned Memory Models for Program Analysis
复制标题
用于程序分析的分区内存模型
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Thomas Wies
中科院分区：
文献类型：
--
作者：
Wen Wang;Clark W. Barrett;Thomas Wies
可伸缩性是静态分析中的一个关键挑战。对于像C这样的命令式语言，内存建模的方法在可伸缩性方面起着重要的作用。在本文中，我们探讨了一个家庭的内存模型，称为分区内存模型划分内存的基础上的一个点到分析的结果。我们回顾Steensgaard的原始和字段敏感的点，以分析以及数据结构分析（DSA），并引入一个新的基于单元格的点，以分析更精确地处理堆数据结构和类型不安全的操作，如指针算术和指针铸造。我们从软件验证比赛中使用的程序验证框架级联的基准测试的实验结果。我们表明，分区内存模型使用我们的基于单元格的点，以分析优于模型使用其他分析。
Scalability is a key challenge in static analysis. For imperative languages like C, the approach taken for modeling memory can play a significant role in scalability. In this paper, we explore a family of memory models called partitioned memory models which divide memory up based on the results of a points-to analysis. We review Steensgaard’s original and field-sensitive points-to analyses as well as Data Structure Analysis (DSA), and introduce a new cell-based points-to analysis which more precisely handles heap data structures and type-unsafe operations like pointer arithmetic and pointer casting. We give experimental results on benchmarks from the software verification competition using the program verification framework in Cascade. We show that a partitioned memory model using our cell-based points-to analysis outperforms models using other analyses.