Precise and efficient static array bound checking for large embedded C programs
Precise and efficient static array bound checking for large embedded C programs
复制标题
DOI：
10.1145/996841.996869
复制
发表时间：
2004-06
期刊：
影响因子：
--
通讯作者：
A. Venet;G. Brat
中科院分区：
文献类型：
--
作者：
A. Venet;G. Brat
在本文中，我们描述了一个家庭的嵌入式程序的静态数组绑定检查器的设计和实现：最近的火星任务的飞行控制软件。这些代码很大（高达280 Kbps），指针密集型，大量多线程，并以面向对象的风格编写，这使得它们的分析非常具有挑战性。我们设计了一个名为C Global Surveyor（CGS）的工具，它可以在几个小时内分析最大的代码，精度达到80%。分析器的可扩展性和精度是通过使用一个增量的框架，其中指针分析和数组索引的数值分析相互完善对方。CGS的设计使其可以将分析分布在机器集群中的多个处理器上。据我们所知，这是静态分析算法的第一个分布式实现。在本文中，我们将讨论我们在构建工具过程中遇到的可伸缩性挫折及其对初始设计决策的影响。
In this paper we describe the design and implementation of a static array-bound checker for a family of embedded programs: the flight control software of recent Mars missions. These codes are large (up to 280 KLOC), pointer intensive, heavily multithreaded and written in an object-oriented style, which makes their analysis very challenging. We designed a tool called C Global Surveyor (CGS) that can analyze the largest code in a couple of hours with a precision of 80%. The scalability and precision of the analyzer are achieved by using an incremental framework in which a pointer analysis and a numerical analysis of array indices mutually refine each other. CGS has been designed so that it can distribute the analysis over several processors in a cluster of machines. To the best of our knowledge this is the first distributed implementation of static analysis algorithms. Throughout the paper we will discuss the scalability setbacks that we encountered during the construction of the tool and their impact on the initial design decisions.