基于联合类型和指针算法的嵌入式C程序的字段敏感值分析
Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics
摘要：
我们提出了一个内存抽象，能够提升现有的数值静态分析的C程序包含工会类型，指针铸造，和任意指针算术。我们的框架是一个结合点和数据价值分析。我们以字段敏感的方式抽象复合变量的内容，无论这些字段包含数值还是指针值，并使用股票数值抽象域来找到所有可能的内存状态的过度近似-能够发现变量之间的关系。我们的方法的一个主要新颖之处是动态映射方案，我们使用它将标量类型的抽象单元的平面集合与访问的内存位置集合相关联，同时照顾字节级别名-即，在重叠的内存位置中分配了不兼容类型的C变量。我们不依赖于静态类型信息，这在C程序中可能会产生误导，因为它不能解释内存区域的所有用途。我们的工作被纳入了Astrée静态分析器中，该分析器可以检查嵌入式、安全关键型、数值密集型软件中是否存在运行时错误。它取代了以前的内存域，仅限于良好类型，无联合，无指针转换的数据结构。早期的结果表明，这种抽象允许分析更大类的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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
