Meta-Circular Abstract Interpretation in Prolog

Michael Codish and Harald Søndergaard

1. Introduction

This page accompanies our paper with the same title (press here to access the paper). It provides code for the analysers described in the paper (and a few others) as well as several example programs to analyse.

still to do

2. Interpretation and Abstraction

In the paper we demonstrate (in Figure 1) a standard meta-circular interpreter for Prolog. The interpreter assumes that clauses are represented internally as facts. For example, the following program for the Ackermann function 

  ackermann(0,N,s(N)).
  ackermann(s(M),0,Res) :- 
      ackermann(M,s(0),Res).

  ackermann(s(M),s(N),Res) :-
      ackermann(s(M),N,Res1), 
      ackermann(M,Res1,Res).
is represented as three facts, one per clause: 

  my_clause(ack(0,N,s(N)), []).
  my_clause(ack(s(M),0,Res), [ack(M,s(0),Res)]).
  my_clause(ack(s(M),s(N),Res), [ack(s(M),N,Res1),ack(M,Res1,Res)]).

The predicate load_file in the program input.pl will read the clauses from a file and assert the corresponding my_clause representation to the Prolog database.

To support flexibility in the interpretation of unification we make unification explicit when reading in the program. For example the clause, 

    ackermann(s(M),0,Res) :- ackermann(M,s(0),Res).
is represented internally (in my_clause representation) as 
 
    ackermann(A,B,C) :- unify(A,s(M)), unify(B,0),
          unify(C,Res), unify(D,M), unify(E,s(0)),
          unify(F,Res), ackermann(D,E,F).
This can be done when inputting the program's clauses by the predicate load_file in the program input_normalize.pl

The usual interpretation of unification is defined by 

    unify(X,Y) :- X=Y
Making unification explicit gives a first step towards obtaining an analyser. In the paper we discuss why this is not sufficient and use the ackermann function as an example. The unification for the (extended) parity domain described in the paper (click to recall the definition) is defined by ( Figure 2 in the paper)

The simple concrete interpreter of Figure 1 (in the paper) is then enhanced to interpret the unify/2 predicate. The interpreter involves the following modules:

For an example run of the interpreter on the two domains for the Ackermann example check here.

3. Concrete Semantics and Interpreters

4. Meta-Circular Abstract Interpretation

We demonstrate how the operations in the concrete interpreter can be replaced by abstract operations and an abstract interpreter is obtained. The various unification operations and the various lub operations have been collected together in unification_operations.pl and lub_operations.pl respectively. The basic idea is to make unification explicit (the same as demonstrated above using the predicate load_file in the program input_normalize.pl and to enhance the bottom-up interpreter accordingly.

The interpreter is given as tp_abs.pl. The evaluation for the ackermann program using the unification algorithm for the enhanced parity domain (click to recall the definition) defined in ( Figure 2 of the paper), gives 

          ack(zero, zero,  one)           ack(even, zero, odd)
          ack(zero,  one, even)           ack(even,  one, odd)
          ack(zero, even,  odd)           ack(even, even, odd)
          ack(zero,  odd, even)           ack(even,  odd, odd)    
          ack( one, zero, even)           ack( odd, zero, odd)
          ack( one,  one,  odd)           ack( odd,  one, odd)
          ack( one, even, even)           ack( odd, even, odd)
          ack( one,  odd,  odd)           ack( odd,  odd, odd)

Note that this output exposes non-trivial parity dependencies amongst the arguments of ack. For example, the last column on the right tells us that ack(i,j) is indeed odd (and greater than 1) for all i>1.

The example run of the interpreter for this example is given here (the query to the analyzer specifies the program and the domain).

We illustrate three interpreters: for goal independent analysis; for goal dependent analysis (with program points); and for goal dependent analysis (ignoring program points);

5. Evaluation strategies

6. More Applications

6. Conclusion

An "all in one file" analyser based on one of the eager evaluation strategy, can be found here . This analyser will load a file to be analysed and perform a goal dependent or independent analysis applying various options and abstract domains.