栈 - 堆与值抽象的模块化框架（扩展版）
A Modular Framework for Stack-Heap and Value Abstractions (Extended Version)
浏览论文内容
中文总结 AI 辅助
本文针对高级静态程序分析中不同编程语言内存管理问题，提出并形式化通用内存框架，基于抽象解释理论，通过分裂状态抽象将值与内存分析分离到模块化域，可支持多种语言行为，独立组合不同分析。
中文摘要 AI 辅助
高级静态程序分析需要对非平凡程序行为（如指针、列表和集合等复杂数据结构、函数和对象）的语义及其对内存的影响进行推理。在大多数编程语言中，静态和动态分配通常分别由栈和堆管理。然而，运行时分配行为和内存管理方式因分析的编程语言而异。正确处理这些方面至关重要，准确的内存模型能在执行前检测关键问题。本文提出并形式化了一个通用内存框架，用于分析时处理栈和堆内存，能支持不同编程语言行为，保持参数化，允许独立选择和组合不同内存和值分析。它依赖抽象解释理论，实现不同内存模型和程序行为的合理近似。引入了分裂状态抽象，将值和内存分析分离到两个模块化抽象域。这些域通过一组内存标识符以及域定义的操作相互作用，以捕获值信息和结构内存关系。
英文摘要
Advanced static program analysis requires reasoning on the semantics of non-trivial program behaviors (e.g., pointers and complex data structures such as lists and sets, functions, and objects) and how they affect the memory. In most programming languages, static and dynamic allocations are typically managed by the stack and the heap, respectively. However, how allocations behave and how the memory is managed at runtime can vary significantly depending on the programming language being analyzed. Proper handling of these aspects is essential, as an accurate memory model enables the detection of critical issues such as buffer overflows and underflows, use-after-free errors, and null pointer exceptions prior to execution, that is, before such erroneous behaviors occur. In this paper, we propose and formalize a generic memory framework to handle stack and heap memory during the analysis, that is able to support various behaviors from different programming languages (e.g., C, C++, Java, and Python), while remaining parametric, allowing different memory and value analyses to be independently chosen and combined. It relies on the Abstract Interpretation theory and enables sound approximation of different memory models and program behaviors. We introduce a split state abstraction that separates value and memory analyses into two modular abstract domains. These domains interact through a set of memory identifiers, along with a set of operations defined by the domains to manipulate them, allowing the framework to capture both value information and structural memory relationships.
