ASAP Bottom-Up Analysis Tools

Bottom-up analysis has an elegant semantic basis based on the declarative semantics of logic programs, straightforward implementation, and flexible application. In addition, goal-directed or top-down analyses can be simulated through the use of query-answer transformations, of which the so-called "magic set" method is one. These transformations can also serve to increase precision with respect to bottom-up analysis. A toolkit of bottom-up analysis tools and query-answer transformations has been built up. Efficient algorithms for bottom-up analysis are at the heart of the toolkit. A systematic method for implementing analyses using the tools is then available.

The method is based on (i) abstract compilation of a program into a "domain program", (ii) computation of (an approximation to) the model of the domain program, and (iii) use of various query-answer transformations to simulate goal-directed analysis and improve precision. Stages (ii) and (iii) can also be used directly on the original program in some applications. If the domain program has a finite model, then a precise model can be computed in step (ii). If the model is infinite or very large, methods of approximation including regular approximation and others can be used.

Abstract compilation can be achieved very flexibly, based on the construction of pre-interpretations based on arbitrary regular types.

Bottom-Up Analysis Tools

• PolyTypes: The purpose of the PolyTypes tool is to compute a well-typing for a given module, namely, a set of type rules together with a type signature for each module predicate. A well-typing is interpreted in the usual sense of Hindley-Milner types. The types generated by PolyTypes are for example accepted by the type checker for Mercury, a typed logic programming language.
• NFTA: The NFTA (Nondeterministic Finite Tree Automata) tool computes a regular approximation of a given program and uses this to detect useless clauses. The tool computes descriptions of the sets of terms that can occur in the heads of clauses in computations of the program, as non-deterministic regular tree grammars (or NFTAs). These are both more complex and more accurate than classical regular approximations which compute (topdown) deterministic regular tree approximations.
• Domain Model The purpose of the Domain Model tool is to compute an abstract model of a program over a finite set of values such as types and modes. The abstraction is determined by an arbitrary set of regular type rules.

• An implementation of the least model computation, which is the least fixed point of the T_P function.
• Abstraction of a program with respect to a pre-interpretation.
• Derivation of a pre-interpretation by converting a non-deterministic finite tree automaton (NFTA) to a deterministic finite tree automaton (DFTA).
• Backwards analysis transformation.
• Query answer transformations, enabling top-down analysis to be handled in a bottom-up framework.
• Domain program transformation, enabling a program to be interpreted over any pre-interpretation.

Download