Automated verification of pointer programs in pointer logic

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic – Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool – plcc was implemented to automatically verify a number of non-trivial pointer programs.     

空指针解引用错误检测的静态方法研究

空指针解引用是C语言中的一类常见的动态内存错误。Manevich R等提出了一种适用于检测空指针解引用错误的后向分析方法。本文将后向分析的思想和流敏感、上下文敏感的指针分析结合在一起,给出了一种需求驱动的空指针解引用检测静态分析算法。该算法首先由指针分析获得别名信息,然后针对所关心的数据做后向数据流分析,追踪数据传递的源头,以确定程序中的表达式是否产生解引用错误。我们在SUIF2平台上实现了这一算法。实验结果表明,算法具有较高的检测精度。     

一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.     

Precise Call Graphs for C Programs with Function Pointers

The use of pointers presents serious problems for software productivity tools for software understanding, restructuring, and testing. Pointers enable indirect memory accesses through pointer dereferences, as well as indirect procedure calls (e.g., through function pointers in C). Such indirect accesses and calls can be disambiguated with pointer analysis. In this paper we evaluate the precision of one specific pointer analysis (the FA pointer analysis by Zhang et al.) for the purposes of call graph construction for C programs with function pointers. The analysis is incorporated in a production-strength code-browsing tool from Siemens Corporate Research in which the program call graph is used as a primary tool for code understanding.The FA pointer analysis uses an inexpensive, almost-linear, flow- and context-insensitive algorithm. To measure analysis precision, we compare the call graph constructed by this analysis with the most precise call graph obtainable by a large category of existing pointer analyses. Surprisingly, for all our data programs the FA analysis achieves the best possible precision. This result indicates that for the purposes of call graph construction, inexpensive pointer analyses may provide precision comparable to the precision of expensive pointer analyses.     

A bottom-up pointer analysis using the update history

Pointer analysis is an important part for the source code analysis of C programs. In this paper, we propose a bottom-up and flow- and context-sensitive pointer analysis algorithm, where bottom-up refers to the ability to perform the analysis from callee modules to caller modules. Our approach is based on a new modular pointer analysis domain named the update history that can abstract memory states of a procedure independently of the information on aliases between memory locations and keep the information on the order of side effects performed. Such a memory representation not only enables the analysis to be formalized as a bottom-up analysis, but also helps the analysis to effectively identify killed side effects and relevant alias contexts. The experiments performed on a pilot implementation of the method shows that our approach is effective for improving the precision of a client analysis.     

Efficient binary transfer of pointer structures

This paper presents a pair of algorithms for output and input of pointer structures in binary format. Both algorithms operate in linear space and time. They have been inspired by copying garbage collection algorithms, and make similar assumptions about the representations of pointer structures. In real programs, the transfer of entire pointer structures is often inappropriate. The algorithms are extended to transfer partitions of a pointer structure lazily: the receiver requests partitions when it needs them. A remote procedure call mechanism is presented that uses the binary transfer algorithms for communicating arguments and results. A use of this as an enabling mechanism in the implementation of a software engineering environment is discussed.     

A pointer logic and certifying compiler

Proof-Carrying Code brings two big challenges to the research field of programming languages. One is to seek more expressive logics or type systems to specify or reason about the properties of low-level or high-level programs. The other is to study the technology of certifying compilation in which the compiler generates proofs for programs with annotations. This paper presents our progress in the above two aspects. A pointer logic was designed for PointerC (a C-like programming language) in our research. As an extension of Hoare logic, our pointer logic expresses the change of pointer information for each statement in its inference rules to support program verification. Meanwhile, based on the ideas from CAP (Certified Assembly Programming) and SCAP (Stack-based Certified Assembly Programming), a reasoning framework was built to verify the properties of object code in a Hoare style. And a certifying compiler prototype for PointerC was implemented based on this framework. The main contribution of this paper is the design of the pointer logic and the implementation of the certifying compiler prototype. In our certifying compiler, the source language contains rich pointer types and operations and also supports dynamic storage allocation and deallocation.     

基于属性可靠分析的空指针引用缺陷检测

为实现基于静态分析技术充分地检测出C程序中的空指针引用缺陷,提出了一种基于属性可靠分析的缺陷检测方法。首先介绍了空指针引用缺陷模式及特征。然后针对空指针引用缺陷的检测特点提出了属性可靠分析理论,并将指针的指向属性描述为一个属性格。通过提出的抽象内存模型,基于给出的每种程序语句上的迁移实现指针指向属性的可靠分析,根据得到的每个被引用指针的指向属性进而实现空指针引用缺陷的检测。通过对五个实际工程的检测结果分析表明,方法可充分检测出C程序的空指针引用缺陷。     

A low-level memory model and an accompanying reachability predicate

Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks.     

Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic

While automated verification of imperative programs has been studied intensively, proving termination of programs with explicit pointer arithmetic fully automatically was still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that over-approximates all possible runs of a program and that can be used to prove memory safety. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.     

Goal-oriented test data generation for pointer programs

Automatic test data generation leads to the identification of input values on which a selected path or a selected branch is executed within a program (path-oriented vs. goal-oriented methods). In both cases, several approaches based on constraint solving exist, but in the presence of pointer variables only path-oriented methods have been proposed. Pointers are responsible for the existence of conditional aliasing problems that usually provoke the failure of the goal-oriented test data generation process. In this paper, we propose an overall constraint-based method that exploits the results of an intraprocedural points-to analysis and provides two specific constraint combinators for automatically generating goal-oriented test data. This approach correctly handles multi-levels stack-directed pointers that are mainly used in C programs. The method has been fully implemented in the test data generation tool INKA and first experiences in applying it to a variety of existing programs are presented.     

Acoustic control of mouse pointer

This paper describes the design and implementation of a system for controlling mouse pointer using non-verbal sounds such as whistling and humming. Two control modes have been implemented—an orthogonal mode (where the pointer moves with variable speed either horizontally or vertically at any one time) and a melodic mode (where the pointer moves with fixed speed in any direction). A preliminary user study with four users indicates that the orthogonal control was easier to operate and that the humming was less tiring for the users than whistling. The developed system may contribute as an inexpensive, alternative pointing device for people with motor disabilities.     

Simple algebraic data types for C

Adt is a simple tool in the spirit of Lex and Yacc that makes monomorphic algebraic data types, polymorphic built‐in types like the list and an efficient form of pattern matching available in C programs. C programs built with ADTs typically use NULL pointers only to indicate don't care values, and not as sentinels. This reduces the scope for errors involving NULL pointers. The Adt tool generates runtime checks, which catch many of the remaining NULL pointer dereferences. The runtime checks may consume a significant amount of CPU time; hence they can be switched off once the program is suitably debugged. Copyright © 2011 John Wiley & Sons, Ltd.     

Contribution-based call stack abstraction for call string based pointer analysis

Context

Different method calls may have different contributions to the precision of the final application when abstracted into the call strings. The existing call string based pointer analysis algorithms do not consider such contribution difference and hence may not achieve best cost-effectiveness.

Objective

To be more cost-effective, we try to leverage the contribution information of each method call in call string based pointer analysis.

Method

The paper firstly proposes a contribution-based call stack abstraction method which abstracts the call stacks into call strings with the contribution information under consideration. Then, we apply the new call stack abstraction method to the pointer analysis of AspectJ programs and propose a concern-sensitive points-to analysis method. Besides, the new abstraction method is also applied to multi-threaded Java programs and results in a thread-sensitive pointer analysis method.

Results

The experimental results show that the two pointer analysis methods with contribution-based call stack abstraction can be more cost-effective than the ordinary call string based approaches for an application that detects harmful advices and an application that detects inter-thread data flow.

Conclusion

These pointer analysis methods more concretely and more clearly show that the contribution-based call stack abstraction can lead to better cost-effectiveness for the given applications.     

A novel analysis space for pointer analysis and its application for bug finding

The size of today’s programs continues to grow, as does the number of bugs they contain. Testing alone is rarely able to flush out all bugs, and many lurk in difficult-to-test corner cases. An important alternative is static analysis, in which correctness properties of a program are checked without running it. While it cannot catch all errors, static analysis can catch many subtle problems that testing would miss.We propose a new space of abstractions for pointer analysis—an important component of static analysis for C and similar languages. We identify two main components of any abstraction—how to model statement order and how to model conditionals, then present a new model of programs that enables us to explore different abstractions in this space. Our assign-fetch graph represents reads and writes to memory instead of traditional points-to relations and leads to concise function summaries that can be used in any context. Its flexibility supports many new analysis techniques with different trade-offs between precision and speed.We present the details of our abstraction space, explain where existing algorithms fit, describe a variety of new analysis algorithms based on our assign-fetch graphs, and finally present experimental results that show our flow-aware abstraction for statement ordering both runs faster and produces more precise results than traditional flow-insensitive analysis.     

A new approach to pointer analysis for assignments

Pointer analysis is a technique to identify at copile-time the potential values of the pointer expressions in a program,which promises significant benefits for optimzing and parallelizing complilers.In this paper,a new approach to pointer analysis for assignments is presented.In this approach,assignments are classified into three categories:pointer assignments,structure(union)assignents and normal assignments which don‘t affect the point-to information.Pointer analyses for these three kinds of assignments respectively make up the integrated algorithm.When analyzing a pointer assigemtn.a new method called expression expansion is used to calculate both the left targets and the right targets.The integration of recursive data structure analysis into pointer analysis is a significant originality of this paper,which uniforms the pointer analysis for heap variables and the pointer analysis for stack variables.This algorithm is implemented in Agassiz,an analyzing tool for C programs developed by Institute of Parallel Processing,Fudan University,Its accuracy and effectiveness are illustrated by experimental data.     

Reasoning about memory layouts

Verification methods for memory-manipulating C programs need to address not only well-typed programs that respect invariants such as the split-heap memory model, but also programs that access through pointers arbitrary memory objects such as local variables, single struct fields, or array slices. We present a logic for memory layouts that covers these applications and show how proof obligations arising during the verification can be discharged automatically using the layouts. The framework developed in this way is also suitable for reasoning about data structures manipulated by algorithms, which we demonstrate by verifying the Schorr-Waite graph marking algorithm.     

指针式仪表读数的机器视觉智能识别方法

为快速准确地自动识别指针式仪表读数,采用机器视觉技术,结合减影法和Hough变换法对仪表读数进行智能识别.对指针式仪表图像进行图像二值化、形态学处理和边缘检测预处理;利用Hough变换检测仪表中的指针,计算得到指针方向和定位圆形,实现指针式仪表的智能识别.实验结果表明:读数识别的平均相对误差为0.91%,精度较高,能较好地识别指针式仪表读数.     

Alias analysis of pointers in Pascal and Fortran 90: dependence analysis between pointer references

 Vectorization and parallelization of programs written in languages where pointers are used is now a subject of increasing interest. The presence of pointers in programs, however, poses new problems to dependence analysis in vectorizing and parallelizing compilers which had been designed to target only at FORTRAN77 programs. In this paper, a new method to analyze dependencies between pointer references in Pascal is proposed, which can also be applied to Fortran 90. It is designed to handle programs with dynamic data structures, such as linear linked lists or trees, which are the most common use of pointers. The method divides into two stages. The first stage is a safe alias analysis which handles any kind of dynamic data structures. The second stage focuses on the specific data structures. It first detects linear linked lists, and then performs dependence analysis between pointer references to the same list. The paper also proposes ways to enhance the second stage. Tree structures are handled here. Loops which manipulate linked lists can now be considered for vectorization by the proposed analysis. Techniques to vectorize such loops are presented in this paper. Some of the proposed algorithms are implemented in V-Pascal, the automatic vectorizing Pascal compiler of our laboratory. The effectiveness of the vectorization of list operations is proved by an experiment on HITAC S-820/80. Received: August 5, 1994/January 17, 1995