Structuring Optimizing Transformations and Proving Them Sound

A compiler optimization is sound if the optimized program that it produces is semantically equivalent to the input program. The proofs of semantic equivalence are usually tedious. To reduce the efforts required, we identify a set of common transformation primitives that can be composed sequentially to obtain specifications of optimizing transformations. We also identify the conditions under which the transformation primitives preserve semantics and prove their sufficiency. Consequently, proving the soundness of an optimization reduces to showing that the soundness conditions of the underlying transformation primitives are satisfied.The program analysis required for optimization is defined over the input program whereas the soundness conditions of a transformation primitive need to be shown on the version of the program on which it is applied. We express both in a temporal logic. We also develop a logic called temporal transformation logic to correlate temporal properties over a program (seen as a Kripke structure) and its transformation.An interesting possibility created by this approach is a novel scheme for validating optimizer implementations. An optimizer can be instrumented to generate a trace of its transformations in terms of the transformation primitives. Conformance of the trace with the optimizer can be checked through simulation. If soundness conditions of the underlying primitives are satisfied by the trace then it preserves semantics.     

Unfolding-based Improvements on Fuzzy Logic Programs

Unfolding is a semantics-preserving program transformation technique that consists in the expansion of subexpressions of a program using their own definitions. In this paper we define two unfolding-based transformation rules that extend the classical definition of the unfolding rule (for pure logic programs) to a fuzzy logic setting. We use a fuzzy variant of Prolog where each program clause can be interpreted under a different (fuzzy) logic. We adapt the concept of a computation rule, a mapping that selects the subexpression of a goal involved in a computation step, and we prove the independence of the computation rule. We also define a basic transformation system and we demonstrate its strong correctness, that is, original and transformed programs compute the same fuzzy computed answers. Finally, we prove that our transformation rules always produce an improvement in the efficiency of the residual program, by reducing the length of successful Fuzzy SLD-derivations.     

部分计值综述

部分计值是一种程序转换技术．在给定程序部分输入的情况下,可使用该技术对程序进行例化,完成程序中尽可能多的计算,最终得到高效的剩余代码。人们已经研究了许多程序设计语言的部分计值系统,并把它们应用到编译和编译器生成、计算机图形学等领域。本文介绍了部分计值理论及其应用．讨论了Java部分计值器的研究现状．并简单描述了本课题组设计的一个Java分布式部分计值系统DJmix。     

Automated Derivation of Translators From Annotated Grammars

In this paper we propose a technique to automate the process of building translators between operations languages, a family of DSLs used to program satellite operations procedures. We exploit the similarities between those languages to semi-automatically build a transformation schema between them, through the use of annotated grammars. To improve the overall translation process even more, reducing its complexity, we also propose an intermediate representation common to all operations languages. We validate our approach by semi-automatically deriving translators between some operations languages, using a prototype tool which we implemented for that purpose.     

关于递归程序变换模式的设计方法

本文提出递归程序变换模式的一般设计方法，并以具体示例说明之。此外，还对递归程序变换的有关问题作了讨论。     

基于IDA-Pro的软件逆向分析方法

二进制程序转换作为软件逆向分析的主要手段发挥着积极作用。该文给出一种程序转换方法,应用软件二进制程序经IDA Pro反汇编得汇编语言程序,依据下推自动机原理设计汇编文法识别该汇编文件、制定相应的转换规则和优化措施将汇编语言转换成中间语言。转换所得中间语言可读性较强,具有通用性且易于理解。该方法达到了较高的自动化程度,缩小了目标程序的代码量,其应用可有效地减少软件分析和调试人员在追踪代码时所需的时间和工作量。给出应用上述方法进行程序转换的实例。     

Tiling on systems with communication/computation overlap

In the framework of fully permutable loops, tiling is a compiler technique (also known as ‘loop blocking’) that has been extensively studied as a source-to-source program transformation. Little work has been devoted to the mapping and scheduling of the tiles on to physical parallel processors. We present several new results in the context of limited computational resources and assuming communication–computation overlap. In particular, under some reasonable assumptions, we derive the optimal mapping and scheduling of tiles to physical processors. Copyright © 1999 John Wiley & Sons, Ltd.     

Dynamic slicing of concurrent specification languages

Dynamic slicing is a technique to extract the part of the program (called slice) that influences or is influenced, in a particular execution, by a given point of interest in the source code (called slicing criterion). Since a single execution is considered, the technique often uses a trace of this execution to analyze data and control dependencies. In this work we present the first formulation and implementation of dynamic slicing in the context of CSP. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. We base our technique on a new data structure to represent CSP computations called track. A track is a data structure which represents the sequence of expressions that have been evaluated during the computation, and moreover, it is labeled with the location of these expressions in the specification. The implementation of a dynamic slicer for CSP is useful for debugging, program comprehension, and program specialization, and it is also interesting from a theoretical perspective because CSP introduces difficulties such as heavy concurrency and non-determinism, synchronizations, frequent absence of data dependence, etc.     

Transformation parameter estimation using parallel output based neural network

One of the challenging tasks in image registration is to estimate transformation parameters automatically and efficiently. In this paper, we propose a task decomposition based parallel trained neural network to estimate transformation parameters as well as order of transformations. This parameter estimation problem can be divided into several subproblems like rotation, translation and scaling estimation. Each subproblem or module consists of decomposed input datasets, as well as a part of the output vector. Each module is trained in parallel for some specific and fixed input–output vector pattern. Feature vectors are used as input dataset of the proposed neural network. 2D PCA (two dimensional principal component analysis) feature extraction technique is used to build feature vector. This modular technique requires effectively less computation time in comparison to non-modular network. Moreover, this technique can robustly estimate different transformational parameters. The added advantage of this technique is that it can identify order of the transformation. Experimental results justify the effectiveness of the proposed technique.     

基于抽象解释的代码迷惑有效性比较框架

代码迷惑是一种以增加理解难度为目的的程序变换技术,用来保护软件免遭逆向剖析.代码迷惑是否有效是代码迷惑研究中首要解决的问题.目前对有效性证明的研究大都是基于非语义的方式.文章将语义与有效性证明联系起来,建立了基于语义的代码迷惑有效性比较框架,该框架能够为迷惑算法在静态分析这样的限定环境下提供有效性证明,而且也能严格比较迷惑算法之间的有效性,最后使用实例描述比较框架如何应用到证明代码迷惑的有效性.     

A survey of new trends in symbolic execution for software testing and analysis

Symbolic execution is a well-known program analysis technique which represents program inputs with symbolic values instead of concrete, initialized, data and executes the program by manipulating program expressions involving the symbolic values. Symbolic execution has been proposed over three decades ago but recently it has found renewed interest in the research community, due in part to the progress in decision procedures, availability of powerful computers and new algorithmic developments. We provide here a survey of some of the new research trends in symbolic execution, with particular emphasis on applications to test generation and program analysis. We first describe an approach that handles complex programming constructs such as input recursive data structures, arrays, as well as multithreading. Furthermore, we describe recent hybrid techniques that combine concrete and symbolic execution to overcome some of the inherent limitations of symbolic execution, such as handling native code or availability of decision procedures for the application domain. We follow with a discussion of techniques that can be used to limit the (possibly infinite) number of symbolic configurations that need to be analyzed for the symbolic execution of looping programs. Finally, we give a short survey of interesting new applications, such as predictive testing, invariant inference, program repair, analysis of parallel numerical programs and differential symbolic execution.     

基于F—logic的概念语义网

该文用Ｆ－ｌｏｇｉｃ程序写出了一个概念语义网Ｆ－Ｎｅｔ，从而指出了实现语义网的一种可能的新方法，用Ｆ－ｌｏｇｉｃ来实现语义网的优点是；可以利用Ｆ－ｌｏｇｉｃ程序对该语义网的语义网的语义模型进行了研究。而这一点现有的其它语义网实现方法都无法做到。     

Shortcut fusion rules for the derivation of circular and higher-order programs

Functional programs often combine separate parts using intermediate data structures for communicating results. Programs so defined are modular, easier to understand and maintain, but suffer from inefficiencies due to the generation of those gluing data structures. To eliminate such redundant data structures, some program transformation techniques have been proposed. One such technique is shortcut fusion, and has been studied in the context of both pure and monadic functional programs. In this paper, we study several shortcut fusion extensions, so that, alternatively, circular or higher-order programs are derived. These extensions are also provided for effect-free programs and monadic ones. Our work results in a set of generic calculation rules, that are widely applicable, and whose correctness is formally established.     

Algebraic reasoning for probabilistic action systems and while-loops

Back and von Wright have developed algebraic laws for reasoning about loops in a total correctness framework using the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems and probabilistic while-loops. In particular we focus on developing data refinement rules for these two constructs. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible.     

Calcolo degli autovalori di un parametro nei problemi differenziali ordinari con condizioni ai limiti contenenti il parametro stesso

In this paper we present a numerical method for the computation of eigenvalues (real or complex) of one parameter contained in a 2^nd order linear homogeneous differential equation, with Sturm-Liouville boundary conditions. This method, particularly apt for a computer, shortens considerably the calculation time thanks to an algorithm which quickly transforms a determinant, containing the eigenvalue in all its elements, into an equivalent determinant which contains the eingenvalue only in the elements of the principal diagonal; we think that the suggested transformation has some new points and advantages in comparison with the method based on the inversion of a matrix. The method, used to computer the roots of an algebraic equation with real coefficients, shortens further the calculation time when we have to find the eigenvalues of smaller modulus. If initially the eigenvalue is also found in the boundary conditions, the calculation are carried out in a similar way. This paper ends with some examples and notes about the program in «FORTRAN» language.     

An automated reasoning problem associated with proving claims about programs using Floyd-Hoare inductive assertion methods

Proving claims about behavior of software is essential for the qualification of computer-based systems used in the control of nuclear reactors. For this Problem Corner, we select one of the verification conditions for a C program that initializes an array to zero. We add assertions about the initial conditions and state of the program and about the expected behavior of the program in terms of its state. The modeling and specification technique is the inductive assertion technique of Floyd-Hoare. The program with assertions is then transformed by the source-to-source program transformation system TAMPR into a set of separate verification conditions to be proven by the automated reasoning system. Our experience with this program demonstrates the typical automated reasoning problems we have encountered and illustrates how we have approached solutions to the problems.Work supported by the Civilian Reactor Development Program and the Applied Mathematical Sciences Research subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract No. W-31-109-ENG-38.     

The Least Fixpoint Transformation for Disjunctive Logic Programs

The paradigm of disjunctive logic programming(DLP)enhances greatly the expressive power of normal logic programming(NLP)and many(declarative)semantics have been defined for DLP to cope with various problems of knowledge representation in artificial intelligence.However,the expressive ability of the semantics and the soundness of program transformations for DLP have been rarely explored.This paper defines an immediate consequence operatro T^GP for each disjunctive program and shows that T^GP has the least and computable fixpoint Lft(P),Lft is,in fact,a program transformation for DLP,which transforms all disjunctive programs into negative programs.It is shown that Lft preserves many key semantics,including the disjunctive stable models,well-founded model,disjunctive argunent semantics DAS,three-valued models,ect.Thic means that every disjunctive program P has a unique canonical form Lft(P)with respect to these semantics.As a result,the work in this paper provides a unifying framework for studying the expressive ability of various semantics for DLP On the other hand,the computing of the above semantics for negative programs is ust a trivial task,therefore,Lft(P)is also an optimization method for DLP.Another application of Lft is to derive some interesting semantic results for DLP.     

State‐saving transformations for efficient bottom‐up evaluation of logic programs and rule‐based systems

Redundant computations in bottom‐up evaluation of logic programs and rule‐based systems can be avoided by caching intermediate joins – i.e., partial rule instantiations – for later use. Joins can be cached either at representation level by program transformation techniques introducing supplementary predicates or at implementation level by specialized implementation techniques using internal memory cells. The efficiency of these state‐saving techniques depends on the selection of premises for storing the joins. In this paper we first present a general program transformation technique for saving joins which heuristically reorders subgoals and performs predicate splitting optimization, an extension of unfolding. This state‐saving transformation can be applied for any goal‐directed and model‐generation evaluation. It does not require any information about the query. We show that the program transformation approach is equivalent to the specialized state‐saving implementations known from production systems and model‐generation theorem provers. To use the efficient and complete bottom‐up evaluation also for query answering, we improve the supplementary extensions of Generalized Magic Sets and Magic Templates rewriting strategies by the presented state‐saving transformation. This revised version was published online in June 2006 with corrections to the Cover Date.