Automatic generation of path covers based on the control flowanalysis of computer programs

Branch testing a program involves generating a set of paths that will cover every arc in the program flowgraph, called a path cover, and finding a set of program inputs that will execute every path in the path cover. This paper presents a generalized algorithm that finds a path cover for a given program flowgraph. The analysis is conducted on a reduced flowgraph, called a ddgraph, and uses graph theoretic principles differently than previous approaches. In particular, the relations of dominance and implication which form two trees of the arcs of the ddgraph are exploited. These relations make it possible to identify a subset of ddgraph arcs, called unconstrained arcs, having the property that a set of paths exercising all the unconstrained arcs also cover all the arcs in the ddgraph. In fact, the algorithm has been designed to cover all the unconstrained arcs of a given ddgraph: the paths are derived one at a time, each path covering at least one as yet uncovered unconstrained arc. The greatest merits of the algorithm are its simplicity and its flexibility. It consists in just visiting recursively in combination the dominator and the implied trees, and is flexible in the sense that it can derive a path cover to satisfy different requirements, according to the strategy adopted for the selection of the unconstrained arc to be covered at each recursive iteration. This feature of the algorithm can be employed to address the problem of infeasible paths, by adopting the most suitable selection strategy for the problem at hand. Embedding of the algorithm into a software analysis and testing tool is recommended     

一种基于路径优化的推测多线程划分算法

推测多线程(speculative multithreading,简称SpMT)技术是一种实现非规则程序自动并行化的有效途径.然而,基于控制流图和分支预测技术的线程划分方法,不可避免地会受到划分路径上所存在的控制依赖和数据依赖的制约.目前,在传统的线程划分算法中存在的一个重要问题是,在对划分路径进行选取时只考虑了控制依赖影响却不能有效地综合考虑数据依赖的影响,进而导致不能选取最佳的划分路径.因此,针对传统方法中这种依赖评估方法效率低下的问题,设计并实现了一种基于路径优化的线程划分算法.该算法通过引入基于程序切片技术的预计算方法,建立一种路径评估方法来评估程序间的控制和数据依赖.同时,引入控制线程体大小的启发式规则,以便有效地解决负载不平衡的问题.基于Olden测试集的测试结果表明,所提出的算法可以有效地对非规则程序进行划分,其平均加速比可以达到1.83.     

Reachability Analysis of Synchronized PA Systems

We present a generic approach for the analysis of concurrent programs with (unbounded) dynamic creation of threads and recursive procedure calls. We define a model for such programs based on a set of term rewrite rules where terms represent control configurations. The reachability problem for this model is undecidable. Therefore, we propose a method for analyzing such models based on computing abstractions of their sets of computation paths. Our approach allows to compute such abstractions as least solutions of a system of (path language) constraints. More precisely, given a program and two regular sets of configurations (process terms) T and T^′, we provide (1) a construction of a system of constraints which characterizes the set of computation paths leading from T to T^′, and (2) a generic framework, based on abstract interpretation, allowing to solve this system in various abstract domains leading to abstract analysis with different precision and cost.     

Use-definition chains with applications

Methods of compile-time program analysis for automatic code optimization usually include control flow analysis, in which possible execution flow paths are modeled, and data flow analysis, in which data relatiohsips are modeled. One representation of data relations in a program, via use-definition chains, is examined in the light of a particular example problem—the global elimination of “useless” computation. Two elimination algorithms which use differently organized use-definition chains are presented and compared for space complexity on two pathologically different families of flow graphs. Algorithms to compute chains of both varieties are also developed.     

A method for detecting the theft of Java programs through analysis of the control flow information

A software birthmark refers to the inherent characteristics of a program that can be used to identify the program. In this paper, a method for detecting the theft of Java programs through a static software birthmark is proposed that is based on the control flow information. The control flow information shows the structural characteristics and the possible behaviors during the execution of program. Flow paths (FP) and behaviors in Java programs are formally described here, and a set of behaviors of FPs is used as a software birthmark. The similarity is calculated by matching the pairs of similar behaviors from two birthmarks. Experiments centered on the proposed birthmark with respect to precision and recall. The performance was evaluated by analyzing the F-measure curves. The experimental results show that the proposed birthmark is a more effective measure compared to earlier approaches for detecting copied programs, even in cases where such programs are aggressively modified.     

An application of compiler technology to the year 2000 problem

This paper describes our experience in developing techniques for repairing date affected programs using standard compiler technology. Starting with date‐ness information of certain variables based on their declarations, we propagate this information through all possible control paths, using date inference rules to traverse across individual statements. Our approach is fine grained enough to infer the date‐ness of each occurrence of a variable. After detecting date‐ness of variables, we renovate programs by applying a transformation using base year strategy. These techniques have been implemented as a tool set for renovating date affected COBOL programs. Copyright © 1999 John Wiley & Sons, Ltd.     

A Model for Representing Programs Using Hierarchical Graphs

In this paper a hierarchical graph model for programs based on the concepts of recursive graphs (RG's) and Codd relations is presented. The purpose of the model is to clearly represent the structure of a program implemented in a structured language, such as Pascal, Algol, or PL/1, so that the program can be analyzed and modifications to the program can be clearly specified. The model uses an RG representation for the control flow and the data flow with an equivalent relational representation. It also has a relational representation for the objects defmed within the program. The various aspects of the model are illustrated using Pascal constructs and a model for an example Pascal program is given.     

Learning Flow of Control: Recursive and Iterative Procedures

Two experiments were performed to study students' ability to write recursive and iterative programs and transfer between these two skills. Subjects wrote functions to accumulate instances into a list. Problems varied in terms of whether they were recursive or iterative, whether they operated on lists or numbers, whether they accumulated results in forward or backward manner, whether they accumulated on success or failure, and whether they simply skipped or ejected on failure to accumulate. Subjects had real difficulty only with the dimensions concerned with flow of control, namely, recursive versus iterative, and skip versus eject. We found positive transfer from writing iterative functions to writing recursive functions, but not vice versa. A subsequent protocol study revealed subjects had such a poor mental model of recursion that they developed poor learning strategies which hindered their understanding of iteration. It is argued that having an adequate model of the functionality of programming is prerequisite to learning to program, and that it is sensible pedagogical practice to base understanding of recursive flow of control on understanding iterative flow of control.     

A view of computability on term algebras

A framework of definitions for, and questions about, notions of computability, complexity, and logic for term algebras is built around known results in the literature and the current work. The term algebra for finite binary trees and various classes of programs for computing on them, a class similar to LISP being the most powerful, serve as a focus. Several interesting classes of programs less powerful than LISP are obtained by varying the functions and predicates available in the programming language. It is shown how they relate to one another and then some of their properties are explored. For example, there is a class powerful enough to compute all the partial recursive functions on the natural numbers that is neither sufficiently powerful to code the binary trees into the natural numbers nor to recognize any set that is both infinite and coinfinite. A simple logic sufficient to talk about trees and LISP-like computations is given and it is suggested that certain pebble games provide very reasonable measures of complexity of trees. It is also indicated how various particular results give further insight into such fundamental notions as Turing computable and recursively enumerable.     

防火墙规则间包含关系的解析方法

针对防火墙规则集中规则间的相互关系难以把握,从而导致防火墙无法正确地过滤数据包的问题,提出了一种基于集合理论的规则间包含关系的解析方法.该方法在不考虑规则动作的情况下,基于集合理论的包含关系来解析和分类规则之间的关系,简化了分析规则间相互关系的过程.并且使用高效的函数式编程语言Haskell实现了所提出的方法,整体代码简洁、易于维护和扩展.实验结果表明,对于中小规模的防火墙规则集,能够快速而有效地解析规则间的包含关系,并且能够为后续的规则间的异常检测提供重要的依据.     

Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming

The existing techniques for reachability analysis of linear hybrid automata do not scale well to problem sizes of practical interest. Instead of developing a tool to perform reachability check on all the paths of a linear hybrid automaton, a complementary approach is to develop an efficient path-oriented tool to check one path at a time where the length of the path being checked can be made very large and the size of the automaton can be made large enough to handle problems of practical interest. This approach of symbolic execution of paths can be used by design engineers to check important paths and thereby, increase the faith in the correctness of the system. Unlike simple testing, each path in our framework represents a dense set of possible trajectories of the system being analyzed. In this paper, we develop the linear programming based techniques towards an efficient path-oriented tool for the bounded reachability analysis of linear hybrid systems.     

一种面向生产系统的控制流异常检测算法

目前,针对生产系统的入侵攻击行为朝着规模化、分布化、复杂化等方向演变,传统的基于漏洞库、病毒库、规则匹配等被动式防护手段难以应付隐藏在生产系统内部的攻击行为。从生产系统的业务程序控制流出发,提出了一种基于路径匹配的生产系统控制流异常检测算法CFCPM。首先提出了一种基于关键路径匹配的基本组划分方法,通过扩大控制流分析的基本研究单元,降低了断言标签式控制流分析方法对系统运行造成的性能负担;然后,分别介绍了CFCPM算法的标准路径集获取阶段和路径匹配阶段,通过判断当前控制流路径是否偏离标准路径集,察觉生产系统所处的异常工作状态。最后,通过异常检测能力分析证明了该算法对业务程序控制流异常检测的有效性。     

Combining techniques of bounded model checking and constraint programming to aid for error localization

A model checker can produce a trace of counter-example for erroneous program, which is often difficult to exploit to locate errors in source code. In my thesis, we proposed an error localization algorithm from counter-examples, named LocFaults, combining approaches of Bounded Model-Checking (BMC) with constraint satisfaction problem (CSP). This algorithm analyzes the paths of CFG (Control Flow Graph) of the erroneous program to calculate the subsets of suspicious instructions to correct the program. Indeed, we generate a system of constraints for paths of control flow graph for which at most k conditional statements can be wrong. Then we calculate the MCSs (Minimal Correction Sets) of limited size on each of these paths. Removal of one of these sets of constraints gives a maximal satisfiable subset, in other words, a maximal subset of constraints satisfying the postcondition. To calculate the MCSs, we extend the generic algorithm proposed by Liffiton and Sakallah in order to deal with programs with numerical instructions more efficiently. This approach has been experimentally evaluated on a set of academic and realistic programs.     

An active set algorithm for tracing parametrized optima

Optimization problems often depend on parameters that define constraints or objective functions. It is often necessary to know the effect of a change in a parameter on the optimum solution. An algorithm is presented here for tracking paths of optimal solutions of inequality constrained nonlinear programming problems as a function of a parameter. The proposed algorithm employs homotopy zero-curve tracing techniques to track segments where the set of active constraints is unchanged. The transition between segments is handled by considering all possible sets of active constraints and eliminating nonoptimal ones based on the signs of the Lagrange multipliers and the derivatives of the optimal solutions with respect to the parameter. A spring-mass problem is used to illustrate all possible kinds of transition events, and the algorithm is applied to a well-known ten-bar truss structural optimization problem.     

命令式动态规划类算法程序推导及机械化验证

动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP (Minimalistic Imperative Programming Language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG (Verification Condition Generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证了所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.     

Model checking LTL with regular valuations for pushdown systems

Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has received special attention. However, all these works impose a strong restriction on the possible valuations of atomic propositions: whether a configuration of the pushdown system satisfies an atomic proposition or not can only depend on the current control state of the pushdown automaton and on its topmost stack symbol. In this paper we consider LTL with regular valuations: the set of configurations satisfying an atomic proposition can be an arbitrary regular language. The model-checking problem is solved via two different techniques, with an eye on efficiency. The resulting algorithms are polynomial in certain measures of the problem which are usually small, but can be exponential in the size of the problem instance. However, we show that this exponential blowup is inevitable. The extension to regular valuations allows to model problems in different areas; for instance, we show an application to the analysis of systems with checkpoints. We claim that our model-checking algorithms provide a general, unifying and efficient framework for solving them.     

Programs as partial graphs II: Recursion

In Part I of the paper, we have proposed a unified relational algebra approach using partial graphs for theoretical investigations on semantics, correctness and termination. This approach is extended here to systems of recursive programs, allowing not only sequencing and conditional branching as a control structure but also flow diagrams.An equivalence proof of operational and denotational semantics is obtained which is strictly based on axioms of relational algebra. A short new proof of an important completeness result is given in the generalized setting of systems of recursive flow diagram programs. Finally, Hitchcock-Park's theorem on derivatives is formulated in the general case of nondeterministic recursive flow diagram programs.     

A logic-based approach to program flow analysis

A formalism is presented for tracking assertions which hold universally, i.e., at the end of all the execution paths to a given program point, and assertions which hold existentially, i.e., at the end of some execution paths. In the formalism, the assertions which hold at a given execution path are uniformly defined by an entry environment which contains the assertions which hold when the execution of the program begins and an environment transformer for every program construct. The novel aspect of our formalism is that Horn clauses are used to specify the consistent environments and the meaning of program constructs. The best iterative algorithm (a notion defined by P. Cousot and R. Cousot) for tracking universal and existential assertions simultaneously is given. Conditions are presented under which the best iterative algorithm can be efficiently implemented. The formalism is applied to the pointer equality problem in Pascal. It is shown that universal pointer equalities may be used to reduce the number of superfluous existential equalities, and that existential equalities may be used to obtain more universal equalities. Recent empirical results indicate that tracking the combination of may and must equalities leads to substantial improvements in the result of the analysis. For programs without recursively defined records, the best iterative algorithm can be effectively implemented. These results apply to multiple levels of pointers and can be extended to handle possibly recursive procedures. However, for programs with recursively defined data types further approximations are necessary, e.g., by using a finite graph to model all the possible pointer equalities. For simplicity, this paper does not present an analysis algorithm for this case. Received: 2 September 1991 / 25 June 1997     

一种静态分析C^＋＋异常处理的方法

异常处理是现代程序设计语言提供的用来提高软件健壮性的一种机制。由于在C^＋＋的函数界面中并不要求声明该函数所能传播出的异常的类型，所以要想提高系统的健壮性，必须清楚在程序的执行过程中可能引发的异常、异常的传播路径等。然而在大型系统中，要想确定这些信息是非常困难的。本文针对C^＋＋的异常处理机制，首先提出了一个描述C^＋＋异常结构信息的模型，并把该模型应用于递归函数中。然后，描述了一个基于该模型的分析C^＋＋程序异常结构信息的工具CETool。该工具能提供所有显式引发异常的有关信息，为系统中异常处理结构的改进和程序的结构测试提供有价值的信息。最后给出了该工具的实现方法和应用实例。