Types and trace effects for object orientation

Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented programs in Featherweight Java. We observe that the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, particularly overridden methods, dynamic dispatch, and downcasting. We propose an expressive type and effect inference algorithm combining polymorphism and subtyping/subeffecting constraints to obtain a flexible trace effect analysis in this setting, and show how these techniques are applicable to Object Oriented features. We also extend the basic language model with exceptions and stack-based event contexts, and show how trace effects scale to these extensions by structural transformations.     

Double dispatch in C++

Double dispatch is the ability to dynamically select a method not only according to the run‐time type of the receiver (single dispatch), but also according to the run‐time type of the argument. This mechanism unleashes the power of dynamic binding in object‐oriented languages, so enhancing re‐usability and separation of responsibilities. However, many mainstream languages, such as, e.g., C++ and Java, do not provide it, resorting only to single dispatch. In this paper we propose an extension of C++ (also applicable to other object‐oriented languages) that enables double dispatch as a language feature. This yields dynamic overloading and covariant specialization of methods. We define a translation from the new constructs to standard C++ and we present the preprocessor implementing this translation, called doublecpp . The translated code enjoys static type safety and implements the semantics of double dispatch by using only standard mechanisms of static overloading and dynamic binding, with minimal impact on the performance of the program. Copyright © 2006 John Wiley & Sons, Ltd.     

A class loading sensitive approach to detection of runtime type errors in component-based Java programs

ContextThe employment of class loaders in component-based Java programs may introduce runtime type errors, which may happen at any statement related to class loading, and may be wrapped into various types of exceptions raised by JVM. Traditional static analysis approaches are inefficient to detect them.ObjectiveOur previous work proposed a semi-static detection work based on points-to analysis to detect such runtime type errors. In this paper, we extend previous work by referencing the information obtained from class loading to detect runtime type errors in component-based Java programs, without the need to running them.MethodOur approach extends the typical points-to analysis by gathering the behavior information of Java class loaders and figuring out the defining class loader of the allocation sites. By doing that, we obtain the runtime types of objects a reference variable may point to, and make use of such information to facilitate runtime type error detecting.ResultsResults on four case studies show that our approach is feasible, can effectively detect runtime errors missed by traditional static checking methods, and performs acceptably in both false negative test and scalability test.     

流非敏感的跨过程的别名分析

数据流分析算法可以分类成流敏感和流非敏感两类。为了提高效率,流非敏感的跨过程分析没有利用与每个过程相关的过程内的控制流信息。文中,提出了一种流非敏感的数据流分析算法来计算指针引起的跨过程的别名问题。通过如下方法来提高了分析的精度:利用某些特定类型的注销(kill)信息,这些信息可以提前计算;计算每个过程内产生的别名信息,而不是只计算每个过程的出口点产生的别名信息。     

流敏感的跨过程指针别名分析

对指针别名及其表示方式进行了阐述。描述了跨过程指针别名分析的框架，通过在分析时创建PCG(程序调用图)来处理函数指针。研究了基于此框架的一个流敏感的跨过程指针别名分析算法，算法是跨过程阶段和过程内阶段交叉进行的。最后对算法进行了实例分析和验证。     

Second Order Bounded Quantification with If-Expression

The full combination of if-expression and subtyping was known as a challenging problem for a long time. The difficulty comes from the fact that two branches of an if-expression might have different types and these types might not have a unique least upper bound. Such situation could happen in real object oriented languages such as Java. In our previous work, we investigated this problem in a simply typed lambda calculus extended with subtyping and if-expression and solved the type checking problem in that system. In this paper, we extend the result to bounded quantification combined with if-expression.     

Translating Double Dispatch into Single Dispatch

Goals of flexibility and re-usability in typed object-oriented languages suggest the requirement of double dispatch, i.e., the mechanism of dynamically selecting a method not only according to the run-time type of the receiver (single dispatch), but also to the run-time type of the argument. However, many mainstream languages, such as, e.g., C++ and Java, do not provide it, resorting to only single dispatch. In this paper we present a general technique for adding double dispatch as a type-safe language feature, so yielding dynamic overloading and covariant specialization of methods, without extending basic semantics. To this aim we introduce a toy core language, extended to a full form of (non encapsulated) multi methods. Then we define a translation algorithm from multi methods to the core language, that implements double dispatch by using only standard mechanisms of static overloading and single dispatch. As a main feature, our translation preserves type safety, it uses neither RTTI nor type downcasts and does not introduce crucial overhead during method selection.     

Multilevel static analysis for improving program quality

In this paper, we discuss some program analysis methods for finding defects in source code that are combined to form a multilevel analysis system. The first level consists of the checks using abstract syntax tree (AST) walks and intraprocedural dataflow; this level also builds a memory model for the subsequent levels. The memory model requires evaluating integer expressions and points-to sets. The second level is an interprocedural summary-based approach whereby the program features of interest are calculated as attributes of value classes that are formed in the program. Finally, the third level is a path-sensitive analysis that builds reachability formulas for program points and tracks the predicates that should hold for the desired features to be observable. The errors are found by testing the formulas for satisfiability with an SMT solver. All these levels of analysis are implemented in the Svace analyzer toolset, which demonstrates scalability up to millions of lines of code and precision of 60–90% true positives.     

Static Analysis of Object References in RMI-Based Java Software

Distributed applications provide numerous advantages related to software performance, reliability, interoperability, and extensibility. This paper focuses on distributed Java programs built with the help of the remote method invocation (RMI) mechanism. We consider points-to analysis for such applications. Points-to analysis determines the objects pointed to by a reference variable or a reference object field. Such information plays a fundamental role as a prerequisite for many other static analyses. We present the first theoretical definition of points-to analysis for RMI-based Java applications, and we present an algorithm for implementing a flow- and context-insensitive points-to analysis for such applications. We also discuss the use of points-to information for corrupting call graph information, for understanding data dependencies due to remote memory locations, and for identifying opportunities for improving the performance of object serialization at remote calls. The work described in this paper solves one key problem for static analysis of RMI programs and provides a starting point for future work on improving the understanding, testing, verification, and performance of RMI-based software     

Java 指针指向分析优化

指针指向分析的主要目的是静态地获取程序在运行时刻的指针指向信息.基于Andersen算法,设计了一种有效的、上下文敏感的指针指向分析算法,支持继承、字段对象等语言特性.不同对象的字段在算法中被分别处理,同时,算法对复合类型的对象实现了基于字段的处理.为了提高算法的效率和可扩展性,引入了两种优化方式:一种是结点间的拓扑排序以降低分析过程中的迭代次数;另一种是在线的环路侦测与消除,它与拓扑排序过程同步实现,有效地提高了处理效率.实验数据表明,该算法可以用来为较大规模的Java代码生成精确的指向关系集合.     

A complete algebraic characterization of behavioral subtyping

We present a model-theoretic study of correct behavioral subtyping for first-order, deterministic, abstract data types with immutable objects. For such types, we give a new algebraic criterion for proving correct behavioral subtyping that is both necessary and sufficient. This proof technique handles incomplete specifications by allowing proofs of correct behavioral subtyping to be based on comparison with one of several paradigmatic models. It compares a model to a selected paradigm with a generalization of the usual notion of simulation relations. This generalization is necessary for specifications that are not term-generated and that use multiple dispatch. However, we also show that the usual notion of simulation gives a necessary and sufficient proof technique for the special cases of term-generated specifications and specifications that only use single dispatch. Received: 12 November 1997 / 12 November 1999     

A critical analysis of incremental iterative data flow analysisalgorithms

A model of data flow analysis and fixed point iteration solution procedures is presented. The faulty incremental iterative algorithm is introduced. Examples of the imprecision of restarting iteration from the intraprocedural and interprocedural domains are given. Some incremental techniques which calculate precise data flow information are summarized     

基于方法调用一般化模型的并行性分析

该文给出了一种考虑了面向对象语言的多态和对象引用别名问题的对象方法间并行性的分析方法，这种方法用于面向对象语言并行化中的并行性分析，文中首先给出了一般化的方法调用模型，然后基于该模型给出了表达式化简，过程和过程间分析的算法，该算法可以求出变量的定义和使用集合，由于并行性分析，该文给出的简单例子即可以将该文的和相关的工作加以区别。其技术已经在作者研制的Java并行化编译器JAPS－Ⅱ中实现。     

Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code

The explicit memory management and type conversion endow the C language with flexibility and performance that render it the de facto language for system programming. However, these appealing features come at the cost of programs’ safety. Due to the C language permissiveness, highly skilled but inadvertent programmers often spawn insidious programming errors that yield exploitable code. In this paper, we present a novel type and effect analysis for detecting memory and type errors in C source code. We extend the standard C type system with effect, region, and host annotations that hold valuable safety information. We also define static safety checks to detect safety errors using the aforementioned annotations. Our analysis performs in an intraprocedural phase and an interprocedural phase. The flow-sensitive and alias-sensitive intraprocedural phase propagates type annotations and applies safety checks at each program point. The interprocedural phase generates and propagates unification constraints on type annotations across function boundaries. We present an inference algorithm that automatically infers type annotations and applies safety checks to programs without programmers’ interaction.     

A constraint-weaving approach to points-to analysis for AspectJ

Points-to analysis is a static code analysis technique that establishes the relationships between variables of references and allocated objects. A number of points-to analysis algorithms have been proposed for procedural and object-oriented languages like C and Java, while few of them can be used for AspectJ as we know so far. One main reason is that AspectJ is an aspect-oriented language which implements the separation of crosscutting concerns by advices, pointcuts, and inter-type declarations, while a points-to analysis of AspectJ programs may be imprecise because any aspect woven into the base code may change the points-to relations in the program and thus a conservative analysis has to be taken in order to handle the aspects. In this paper, we propose a context-sensitive points-to analysis technique called AJPoints for AspectJ. Similar to the weaving mechanism for AspectJ, AJPoints obtains the constraints and templates on the points-to relations for the base code and the aspects, respectively, but weaves and solves them in an iterative manner in order to cross the boundary between the base code and the aspects. We have implemented AJPoints on abc AspectJ compiler and evaluated it by using twelve AspectJ benchmark programs. The experimental results show that our technique can achieve a high precision about points-to relations in AspectJ programs.     

Tokenisation and compression of Java class files

Method calls in object oriented languages, such as Java, are bound at run-time, making the method binding technique very important for the performance of the language. Efficient implementations can rely on having additional memory and/or processing power available either to store lookup tables or to allow for the construction of caches or rewriting of instructions during runtime. These are luxuries not always available on mobile devices such as mobile phones, tablets, etc. In this paper we describe a novel way of tokenising and compressing method dispatch tables to provide an efficient dispatch process which could be implemented in hardware in only a few operations. We demonstrate this in the context of Java, also showing a significant reduction in size for the resulting class files.     

Constructing the Call Graph of a Program

The proliferation of large software systems written in high level programming languages insures the utility of analysis programs which examine interprocedural communications. Often these analysis programs need to reduce the dynamic relations between procedures to a static data representation. This paper presents one such representation, a directed, acyclic graph named the call graph of a program. We delineate the programs representable by an acyclic call graph and present an algorithm for constructing it using the property that its nodes may be linearly ordered. We prove the correctness of the algorithm and discuss the results obtained from an implementation of the algorithm in the PFORT Verifier [1].     

一种面向对象程序的过程间切片算法

程序切片是一种程序分析技术，它通过把程序减少到只包含与某个特定计算相关的那些语句来分析程序，过程间切片作为图形可达性问题时，需要扩展过程内切片所用的程序依赖图（PDG）成系统依赖图（SDG），然后利用两阶段图形可达性算法计算比较精确的切片，目前程序切片技术的研究以面向对象程序切片为主，文中讨论了一种合适面向对象程序的分层切片方法，并综合分层切片方法和两阶段图形可达性算法提出了一种简化的计算面向对象程序过程间切片的算法。