Programming Tools Group

Research Meetings (Hilary Term 2002)

14 January: Ganesh Sittampalam, Recovering structure from IL programs

Following on from his previous talk about using meet over all paths analysis to recover expressions from programs in .NET IL, Ganesh discussed how he is now also recovering loops and if/switch statements using an algorithm by Brenda Baker. Theoretically, all gotos can be removed from a program if its flow graph is reducible (which means that every loop is only entered in one place), but doing this sometimes involves introducing loops whose bodies are executed at most once; Baker's technique avoids this and therefore sometimes leaves gotos even in reducible flow graphs.

22 January: Oege de Moor, Towards an incremental solver for regular path queries

Oege talked about his draft paper on solving regular path queries in an incremental manner using work by John Horton Conway on factors of regular expressions.

28 January: Yorck Hünke, Type-checking dependent types with rewrite rules

Yorck talked about the details of his algorithm for type checking dependent types with rewrite rules. The key parts of the algorithm are the treatment of general recursion and the integration of rewrite rules into the type checking process. Rewrite rules are currently treated globally, and one rewrite step is attempted whenever type checking fails; upon successful application of a rewrite rule, type checking proceeds.

4 February: Rani Ettinger, Introduction to Program Slicing

Program slicing is a powerful method for automatically decomposing a program by analysing its control and data flow. The slice (or backward slice) of a program with respect to point p and variable x consists of all statements and predicates of the program that might affect the value of variable x at point p. This concept, originally discussed by Mark Weiser [Program Slicing, IEEE TSE, 10, 352-357, 1984], can be used to debug programs, maintain programs and understand programs behavior. This talk is an introduction to Program Slicing and the Program Dependence Graph (PDG), which is a program representation that enables an efficient computation of a slice.

11 February: Will Greenland, Region analysis

Will gave us an introduction to how a small functional language can be annotated with regions which indicate where intermediate values should be stored. Since the lifetime of each region can be determined statically, this allows us to do without garbage collection.

18 February: David Lacey, Debugging optimised code

David surveyed a small selection of papers covering the debugging of optimised code and relating transformed code back to the original source. The papers looked at were:

A. van Deursen and T.B. Dinesh, Origin Tracking for Higher-Order Term Rewriting Systems

Clara Jaramillo, Rajiv Gupta and Mary Lou Soffa, Comparison Checking: An Approach to Avoid Debugging of Optimized Code

Gary Brooks, Gilbert J. Hansen, Steve Simmons, A New Approach to Debugging Optimized Code

25 February: Ganesh Sittampalam, Eliminating goto statements

Baker's technique for recovering structured programs (as discussed earlier in the term) does not necessarily remove every single goto from a program. For some transformations it is essential that no gotos remain, and so Ganesh described an algorithm by Erosa and Hendren that can always eliminate a goto statement.

This algorithm introduces extra program variables to "flag" when the goto should have been executed, and adds dynamic tests to the code to carry out the necessary transfer of control. Since this technique is necessarily more intrusive in terms of its effect on the original program code, it would be mostly appropriately used to "mop up" gotos left by Baker's algorithm.

4 March: Oege de Moor, Incremental model checking revisited.

Earlier this term, Oege explained an algorithm for testing whether all paths in a program satisfy a given regular pattern:

test Prog = Prog < Pat

He furthermore showed how the algorithm could be structured as a homomorphism of regular algebras on Prog. Assuming this algorithm, we discussed how it can be used to conduct backward and forward dataflow analysis in an incremental fashion while transforming a program.

A number of restrictions are necessary to make this work. First, the programming language is structured, and there are no goto statements at all. This allows the relevant analyses to be written as a simple attribute grammar, using the homomorphic model checker. Furthermore, the transformations are applied in a top-down or bottom-up strategy that visits all nodes in the tree.

Given these constraints, the updating can be done efficiently with respect to movements of a cursor in the syntax tree, and subtree replacement. Oege is working on an implementation as part of the IL trafo toolkit.

11 March: Yorck Hünke, Data refinement

This talk was a brain-storming session about data refinement in the context of dependently typed programs. It would be useful to be able to annotate programs with refinements between data types such as lists and vectors (lists of given length) using existential types. Conversion functions could be used to switch from one representation to another in order to refine functions operating on these data types. Ideally, the conversions should only be used during type checking and eliminated before run-time whenever possible.

18 March: David Lacey, PVS

We discussed David's efforts to prove the correctness of certain program transformations using the PVS theorem prover. PVS seems to benefit from a very rich specification language and a reasonable interactive theorem prover. The discussion turned to whether PVS could be incorporated into a toolkit to give semantic guarantees about user specified transformations. It seems, given this preliminary investigation that PVS generality means that the system is a bit too slow and unwieldy for this type of application and perhaps a specialised verifier would be better.