Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics
Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics
复制标题
使用联合类型和指针算术的嵌入式 C 程序的字段敏感值分析
DOI：
10.1145/1134650.1134659
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
A. Miné
中科院分区：
文献类型：
--
作者：
A. Miné
我们提出了一个能够将现有的数值分析提升到包含联合类型，指针铸件和任意指针算术的C程序的记忆。以字段敏感的方式，这些字段是否包含数字或指针值，并使用库存数值抽象域来查找所有可能的内存状态的过度应用 - 并且能够发现我们方法的主要新颖性。我们使用的动态映射方案将标量类型的抽象单元格的平坦集合与访问的存储位置集相关联，同时照顾字节级别的别名 - 即，在重叠存储器位置分配的不兼容类型的C变量不要依靠静态类型的信息在C程序中可能会产生误导，因为它不能解释所有用途的内存区域。嵌入式，关键的，数值密集型软件中的错误。程序，没有太多成本开销。
We propose a memory abstraction able to lift existing numerical static analyses to C programs containing union types, pointer casts, and arbitrary pointer arithmetics. Our framework is that of a combined points-to and data-value analysis. We abstract the contents of compound variables in a field-sensitive way, whether these fields contain numeric or pointer values, and use stock numerical abstract domains to find an overapproximation of all possible memory states---with the ability to discover relationships between variables. A main novelty of our approach is the dynamic mapping scheme we use to associate a flat collection of abstract cells of scalar type to the set of accessed memory locations, while taking care of byte-level aliases---i.e., C variables with incompatible types allocated in overlapping memory locations. We do not rely on static type information which can be misleading in C programs as it does not account for all the uses a memory zone may be put to.Our work was incorporated within the Astrée static analyzer that checks for the absence of run-time-errors in embedded, safety-critical, numerical-intensive software. It replaces the former memory domain limited to well-typed, union-free, pointer-cast free data-structures. Early results demonstrate that this abstraction allows analyzing a larger class of C programs, without much cost overhead.