Program Development using the CiaoPP Program Processor

Getting Started

In order to follow these examples you need to either:

• Install Ciao on your computer, including the development environment (see Installation for more information). This includes CiaoPP (and LPdoc). You can then access CiaoPP from the Emacs interface or the command line.

• Run CiaoPP directly on your browser through the Ciao playground. To this end, load the examples into the playground by pressing the ↗ button (''Load in playground''), and then CiaoPP can be run clicking the More... button and selecting Analyze and check assertions.

To follow this tutorial we recommend installing it as many of the advanced features are not yet included in the playground. The instructions below use the Emacs interface.

A CiaoPP session consists in the preprocessing of a file. The session is governed by a menu, where you can choose the kind of preprocessing you want to be done to your file among several analyses and program transformations available. This tutorial shows how to customize the preprocessing but some predefined preprocessing options are described in CiaoPP at a glance.

Clicking on the icon in the buffer containing the file to be preprocessed displays the menu, which will look (depending on the options available in the current CiaoPP version) something like the ''Preprocessor Option Browser'' shown in:

Except for the first line, which refers to selecting levels of customization. You can select analysis and assertion checking (analyze_check) or program optimization (optimize), and you can later combine the four kinds of preprocessing. The relevant options for the action selected are then shown, together with the relevant flags.

A description of the values for each option will be given as it is used in the corresponding section of this tutorial.

Static Analysis and Program Assertions

The fundamental functionality behind CiaoPP is static global program analysis, based on abstract interpretation. For this task CiaoPP uses the PLAI abstract interpreter [MH92,BGH99].

The system infers information on variable-level properties such as moded types, definiteness, freeness, independence, and grounding dependencies: essentially, precise data structure shape and pointer sharing. It can also infer bounds on data structure sizes, as well as procedure-level properties such as determinacy, termination, non-failure, and bounds on resource consumption (time or space cost). CiaoPP implements several techniques for dealing with ''difficult'' language features (such as side-effects, meta-programming, higher-order, etc.) and as a result can for example deal safely with arbitrary ISO-Prolog programs [BCHP96]. A unified language of assertions [BCHP96,PBH00b] is used to express the results of analysis, to provide input to the analyzer of program specifications for debugging and validation, as well as the results of the comparisons performed against the specifications.

:- module(_, [qsort/2], [assertions]).

:- pred qsort(A,B) : (list(num, A), var(B)).

qsort([],[]).
qsort([First|Rest],Result) :-
    partition(Rest,First,Sm,Lg),
    qsort(Sm,SmS), qsort(Lg,LgS),
    append(SmS,[First|LgS],Result).

partition([],_,[],[]).
partition([X|Y],F,[X|Y1],Y2):-
    X =< F, partition(Y,F,Y1,Y2).
partition([X|Y],F,Y1,[X|Y2]):-
    X > F, partition(Y,F,Y1,Y2).

append([],X,X).
append([H|X],Y,[H|Z]):- append(X,Y,Z).

:- true pred qsort(A,B)
   : ( mshare([[B]]),
       var(B), ground([A]) )
   => ground([A,B]).

:- true pred partition(_A,_1,Y1,Y2)
   : ( mshare([[Y1],[Y2]]),
       var(Y1), var(Y2), ground([_A,_1]) )
   => ground([_A,_1,Y1,Y2]).

:- true pred append(_A,X,_B)
   : ( mshare([[_B]]),
       var(_B), ground([_A,X]) )
   => ground([_A,X,_B]).

Type Analysis

CiaoPP can infer (parametric) types for programs both at the predicate level and at the literal level [GdW94,GP02,VB02]. Different type domains can be selected with the menu option Shape-Type Analysis. As shown in the following screenshot:

At the predicate level the inferred information is:

:- true pred qsort(A,B)
   : ( list(num,A), term(B) )
   => ( list(num,A), list(num,B) ).

:- true pred partition(_A,_1,Y1,Y2)
   : ( list(num,_A), num(_1), term(Y1), term(Y2) )
   => ( list(num,_A), num(_1), list(num,Y1), list(num,Y2) ).

:- true pred append(_A,X,_B)
   : ( list(num,_A), list1(num,X), term(_B) )
   => ( list(num,_A), list1(num,X), list1(num,_B) ).

where term is any term and prop list and list1 are defined in library(lists) as:

:- regtype list(T,L) #"@var{L} is a list of @var{T}'s.".
:- meta_predicate list(pred(1),?).
list(_T,[]).
list(T,[X|L]) :- T(X), list(T,L).

:- regtype list1(T,X) # "@var{X} is a list of @var{Y}s of at least one element.".
:- meta_predicate list1(pred(1),?).
list1(T,[X|R]) :- T(X), list(T,R).

Non-failure and Determinacy Analysis:

CiaoPP includes a non-failure analysis, based on [DLGH97] and [BLGH04], which can detect procedures and goals that can be guaranteed not to fail, i.e., to produce at least one solution or not terminate. It also can detect predicates that are ''covered'', i.e., such that for any input (included in the calling type of the predicate), there is at least one clause whose ''test'' (head unification and body builtins) succeeds. CiaoPP also includes a determinacy analysis based on [LGBH05], which can detect predicates which produce at most one solution, or predicates whose clause tests are mutually exclusive, even if they are not deterministic (because they call other predicates that can produce more than one solution). Programs can be analyzed with this kind of domains by selecting to perform Non-Failure Analysis with domain nf:

Analyzing qsort with the nf domain will produce (among others) the following assertion:

:- true pred qsort(A,B)
   : ( mshare([[B]]),
       var(B), ground([A]), list(num,A), term(B) )
   => ( ground([A,B]), list(num,A), list(num,B) )
   + ( not_fails, covered ).

:- true pred qsort(A,B)
   : ( mshare([[B]]),
       var(B), ground([A]), list(num,A), term(B) )
   => ( ground([A,B]), list(num,A), list(num,B) )
   + ( not_fails, covered ).

The + field in pred assertions can contain a conjunction of global properties of the computation of the predicate. not_fails states that if the precondition is met, the predicate will never fail.

Size, Resources, and Termination Analysis

CiaoPP can also infer lower and upper bounds on the sizes of terms and the computational cost of predicates [DLGHL94,DLGHL97]. The cost bounds are expressed as functions on the sizes of the input arguments and yield the number of resolution steps. Various measures are used for the ''size'' of an input, such as list-length, term-size, term-depth, integer-value, etc. Note that obtaining a non-infinite upper bound on cost also implies proving termination of the predicate.

Our resource analysis is parametric on the resources, therefore a package defining the resource to be used has to be imported in the module, in this case we use the default package that infers information about computation al steps. This is done by replacing the first line by:

:- module(qsort, [qsort/2], [assertions,predefres(res_steps)]).

As an example, the following assertions are part of the output of the upper bounds analysis:

:- true pred qsort(A,B)
   : ( list(num,A), var(B) )
   => ( list(num,A), list(num,B),
        size(ub,length,B,2**length(A)-1.0) )
   + cost(ub,steps,sum($(j),1,length(A),$(j)*2**(length(A)- $(j)))+2.0*2**length(A)+length(A)*2**(length(A)-1)-1.0).

:- true pred append(_A,X,_B)
   : ( list(num,_A), list1(num,X), var(_B) )
   => ( list(num,_A), list1(num,X), list1(num,_B),
        size(ub,length,_B,length(X)+length(_A)) )
   + cost(ub,steps,length(_A)+1).

For example, the second assertion is inferring on success size(ub,length,B,length(X)+length(A)), which means that an (upper) bound on the size of the third argument of append/3 is the sum of the sizes of the first and second arguments. The inferred upper bound on computational steps (+ cost(ub,steps,length(_A)+1)) is the length of the first argument of append/3.

The following is the output of the lower-bounds analysis:

:- true pred qsort(A,B)
   : ( list(num,A), var(B) )
   => ( list(num,A), list(num,B),
        size(lb,length,B,1) )
   + cost(lb,steps,0).

:- true pred append(_A,X,_B)
   : ( list(num,_A), list1(num,X), var(_B) )
   => ( list(num,_A), list1(num,X), list1(num,_B),
        size(lb,length,_B,length(X)+length(_A)) )
   + cost(lb,steps,0).

The lower-bounds analysis uses information from the non-failure analysis, without which a trivial lower bound of 0 would be derived.

In this case it is inferred that on success the lower bound of the third argument of append is size(lb,length,_B,length(X)+length(_A)) (the same as the upper bound!), and the upper bound on computational steps + cost(lb,steps,0), which represents the case in which the first list to concatenate is empty.

Decidability, Approximations, and Safety

As a final note on the analyses, it should be pointed out that since most of the inferred properties are in general undecidable at compile-time, the inference technique used, abstract interpretation, is necessarily approximate, i.e., possibly imprecise. On the other hand, such approximations are also always guaranteed to be safe, in the sense that (modulo bugs, of course) they are never incorrect: the properties stated in inferred assertions do always hold of the program.

Program Debugging and Assertion Checking

Hexagons represent the different tools involved and arrows indicate the communication paths among them.

Program verification and detection of errors is first performed at compile-time by inferring properties of the program via abstract interpretation-based static analysis and comparing this information against (partial) specifications written in terms of assertions (see [HPBLG05] for a detailed description of the sufficient conditions used for achieving this CiaoPP functionality).

The static checking is provably safe in the sense that all errors flagged are definite violations of the specifications.

Using analysis information for debugging

The idea of using analysis information for debugging comes naturally after observing analysis outputs for erroneous programs. Consider this buggy implementation of qsort:

:- module(qsort, [qsort/2], [assertions]).

:- pred qsort(A,B) : (list(num, A), var(B)).

qsort([],[]).
qsort([First|Rest],Result) :-
    partition(Rest,First,Sm,Lg),
    qsort(Sm,SmS), qsort(Lg,LgS),
    append(SmS,[x|LgS],Result).  % <-- 'x' should be X (variable)

partition([],_,[],[]).
partition([X|Y],F,[X|Y1],Y2):-
    X =< F, partition(Y,F,Y1,Y2).
partition([X|Y],F,Y1,[X|Y2]):-
    X > F, partition(Y,F,Y1,Y2).

append([],X,X).
append([H|X],Y,[H|Z]):- append(X,Y,Z).

:- true pred qsort(A,B)
   : ( term(A), term(B) )
   => ( list(num,A), list(^(x),B) ).

where list(^x,B) means ''B is a list of atoms x.''. The information inferred does not seem compatible with a correct definition of qsort, which clearly points to a bug in the program.

Static Checking of Assertions in System Libraries

In addition to manual inspection of the analyzer output, CiaoPP includes a number of automated facilities to help in the debugging task. For example, CiaoPP can find incompatibilities between the ways in which library predicates are called and their intended mode of use, expressed in the form of assertions in the libraries themselves. Also, the preprocessor can detect inconsistencies in the program and check the assertions present in other modules used by the program.

Consider a different implementation of qsort, also with bugs:

:- module(_, [qsort/2], [assertions]).

:- pred qsort(A,B) : (list(num, A), var(B)).

qsort([X|L],R) :-
    partition(L,L1,X,L2),         % <-- swapped second and third arguments
    qsort(L2,R2), qsort(L1,R1),
    append(R2,[X|R1],R).
qsort([],[]).

partition([],_B,[],[]).
partition([e|R],C,[E|Left1],Right):-  % <-- 'e' should be E (variable)
    E < C, !, partition(R,C,Left1,Right).
partition([E|R],C,Left,[E|Right1]):-
    E >= C, partition(R,C,Left,Right1).

append([],X,X).
append([H|X],Y,[H|Z]):- append(X,Y,Z).

Using the default options, and running CiaoPP, we obtain the following messages (and the system highlights the line which produces the first of them), as shown:

WARNING (preproc_errors): (lns 4-8) goal bugqsort2:partition(L,L1,X,L2) at literal 1 does not succeed!

WARNING (ctchecks_pp_messages): (lns 12-13) the head of clause 'bugqsort2:partition/4/2' is incompatible with its call type
     Head:      bugqsort2:partition([e|R],C,[E|Left1],Right)
     Call Type: bugqsort2:partition(basic_props:list(num),term,num,term)

WARNING (preproc_errors): (lns 14-15) goal arithmetic:>=(E,C) at literal 1 does not succeed!

ERROR (ctchecks_pp_messages): (lns 14-15) At literal 1 false assertion:
:- check calls B>=A
   : ( nonvar(B), nonvar(A), arithexpression(B), arithexpression(A) ).
because on call arithmetic:>=(A,B) :

[shfr] native_props:mshare([[B],[_],[A],[_],[A]]),term_typing:var(B),term_typing:var(A)

First and the last two messages warn that all calls to partition and >=/2 will fail, something normally not intended (e.g., in our case). The error message indicates a wrong call to a builtin predicate, which is an obvious error. This error has been detected by comparing the mode information obtained by global analysis, which at the corresponding program point indicates that the second argument to the call to >=/2 is a variable, with the assertion:

:- check calls B>=A
   : ( nonvar(B), nonvar(A), arithexpression(B), arithexpression(A) ).

After correcting this bug, we proceed to perform another round of compile-time checking, which continues producing the following message:

WARNING (ctchecks_pp_messages): (lns 12-13) the head of clause 'bugqsort3:partition/4/2' is incompatible with its call type
     Head:      bugqsort3:partition([e|R],C,[E|Left1],Right)
     Call Type: bugqsort3:partition(basic_props:list(num),num,term,term)

This time the error is in the second clause of partition. Checking this clause we see that in the first argument of the head there is an e which should be E instead. Compile-time checking of the program with this bug corrected does not produce any further warning or error messages.

Static Checking of User Assertions and Program Validation

Though, as seen above, it is often possible to detect error without adding assertions to user programs, if the program is not correct, the more assertions are present in the program the more likely it is for errors to be automatically detected. Thus, for those parts of the program which are potentially buggy or for parts whose correctness is crucial, the programmer may decide to invest more time in writing assertions than for other parts of the program which are more stable. In order to be more confident about our program, we add to it the following check assertions (the check prefix is assumed when no prefix is given, as in the example shown):

:- pred qsort(A,B) : (list(num, A), var(B)).

qsort([X|L],R) :-
    partition(L,L1,X,L2),
    qsort(L2,R2), qsort(L1,R1),
    append(R2,[x|R1],R).
qsort([],[]).

partition([],_B,[],[]).
partition([E|R],C,[E|Left1],Right):-
    E < C, !, partition(R,C,Left1,Right).
partition([E|R],C,Left,[E|Right1]):-
    E >= C, partition(R,C,Left,Right1).

append([],X,X).
append([H|X],Y,[H|Z]):- append(X,Y,Z).

:- calls   qsort(A,B)         : list(num, A).                     % A1
:- success qsort(A,B)         => (ground(B), sorted_num_list(B)). % A2
:- calls   partition(A,B,C,D) : (ground(A), ground(B)).           % A3
:- success partition(A,B,C,D) => (list(num, C),ground(D)).        % A4
:- calls   append(A,B,C)      : (list(num,A),list(num,B)).        % A5
:- comp    partition/4        + not_fails.                        % A6
:- comp    partition/4        + is_det.                           % A7
:- comp    partition(A,B,C,D) + terminates.                       % A8

:- prop sorted_num_list/1.
sorted_num_list([]).
sorted_num_list([X]):- number(X).
sorted_num_list([X,Y|Z]):-
    number(X), number(Y), X=<Y, sorted_num_list([Y|Z]).

CiaoPP can perform compile-time checking of the assertions above, by comparing them with the assertions inferred by analysis (see [HPBLG05,BDD97,PBH00c] for details), producing as output the following assertions:

:- checked calls qsort(A,B)
   : ( list(num,A) ).

:- check success qsort(A,B)
   => sorted_num_list(B).

:- checked calls partition(A,B,C,D)
   : ( ground(A), ground(B) ).

:- checked success partition(A,B,C,D)
   => ( list(num,C), ground(D) ).

:- checked comp partition(_A,_B,_C,_D)
   + not_fails.

:- checked comp partition(_A,_B,_C,_D)
   + det.

:- checked comp partition(A,B,C,D)
   + terminates.

:- check calls append(A,B,C)
   : list(num,B).

In order to produce this output, the CiaoPP menu must be set to the same options as those used for checking assertions in system libraries. Since the on mode has been used for the option Static assertion checking, CiaoPP has automatically detected that the program must be analyzed not only for types and modes domains, but also to check non-failure, determinism, and upper-bound cost. Note that a number of initial assertions have been marked as checked, i.e., they have been validated. If all assertions had been moved to this checked status, the program would have been verified. In these cases CiaoPP is capable of generating certificates which can be checked efficiently for, e.g., mobile code applications [APH04]. However, in our case assertion A5 has not been verified. This indicates a violation of the specification given, which is also flagged by CiaoPP as follows:

WARNING (ctchecks_pp_messages): (lns 18-18) the head of clause 'bugqsort_assertions:append/3/2' is incompatible with its call type
     Head:      bugqsort_assertions:append([H|X],Y,[H|Z])
     Call Type: bugqsort_assertions:append([],[^(x)],term)

The error is now in the call append(R2,[x|R1],R) in qsort (x instead of X). Assertions A1, A3, A4, A6, A7, and A8 have been detected to hold. Note that though the predicate partition may fail in general, in the context of the current program it can be proved not to fail (assertion A6). However, it was not possible to prove statically assertion also A2, which has remained with check status. Note also that A2 has been simplified, and this is because the mode analysis has determined that on success the second argument of qsort is ground, and thus this does not have to be checked at run-time. On the other hand the analyses used in our session (types, modes, non-failure, determinism, and upper-bound cost analysis) do not provide enough information to prove that the output of qsort is a sorted list of numbers, since this is not a native property of the analyses being used. While this property could be captured by including a more refined domain (such as constrained types), it is interesting to see what happens with the analyses selected for the example.

Note: Note that while property sorted_num_list cannot be proved with only (over approximations) of mode and regular type information, it may be possible to prove that it does not hold (an example of how properties which are not natively understood by the analysis can also be useful for detecting bugs at compile-time): while the regular type analysis cannot capture perfectly the property sorted_num_list, it can still approximate it (by analyzing the definition) as list(num, B). If type analysis for the program were to generate a type for B not compatible with list(num, B), then a definite error symptom would be detected.

Performance Debugging and Validation:

CiaoPP allows stating assertions about the efficiency of the program. This is done by stating lower and/or upper bounds on the computational cost of predicates (given in number of execution steps). Consider for example the naive reverse program:

:- module(_, [nrev/2], [assertions,predefres(res_steps)]).

:- use_module(library(assertions/native_props)).

:- pred nrev(A,B) : (ground(A), list(A), var(B)).
%:- check comp nrev(A,B) + steps_ub(length(A)+1).     % (1) false
%:- check comp nrev(A,B) + steps_o(length(A)).        % (2) false
%:- check comp nrev(A,B) + steps_o(exp(length(A),2)). % (3) checked

nrev([],[]).
nrev([H|L],R) :-
    nrev(L,R1),
    append(R1,[H],R).

append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]):- append(Xs,Ys,Zs).

:- module(_, [nrev/2], [assertions]).

:- use_module(library(assertions/native_props)).

:- pred nrev(A,B) : (ground(A), list(A), var(B)).
%! \begin{focus}
:- check comp nrev(A,B) + steps_ub(length(A)+1).   

nrev([],[]).
nrev([H|L],R) :-
    nrev(L,R1),
    append(R1,[H],R).

append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]):- append(Xs,Ys,Zs).
%! \end{focus}

As before, we set the option Action to analyze_check in the menu. We get the following error message:

ERROR (ctchecks_pred_messages): (lns 6-6) False assertion:
:- check comp nrev(A,B)
   + steps_ub(length(A)+1).
because the comp field is incompatible with inferred comp:
[generic_comp] covered,is_det,mut_exclusive,not_fails,steps_lb(0.5*exp(length(A),2)+1.5*length(A)+1),steps_ub(0.5*exp(length(A),2)+1.5*length(A)+1)

ERROR (auto_interface): Errors detected. Further preprocessing aborted.

This message states that nrev will take at least 0.5*(length(A))^2 + 1.5*length(A) + 1 resolution steps (which is the cost analysis output), while the assertion requires that it take at most length(A)+1 resolution steps. The cost function in the user-provided assertion is compared with the lower-bound cost assertion inferred by analysis. This allows detecting the inconsistency and proving that the program does not satisfy the efficiency requirements imposed. Upper-bound cost assertions can also be proved to hold, i.e., can be checked, by using upper-bound cost analysis rather than lower-bound cost analysis. In such case, it holds when the upper-bound computed by analysis is lower or equal than the upper-bound stated by the user in the assertion. The converse holds for lower-bound cost assertions.

CiaoPP can also verify or falsify cost assertions expressing worst case computational complexity orders (this is specially useful if the programmer does not want or does not know which particular cost function should be checked). For example, suppose now that the programmer adds the following ''check'' assertion:

:- check comp nrev(A,B) + steps_o(length(A)).

ERROR (ctchecks_pred_messages): (lns 6-6) False assertion:
:- check comp nrev(A,B)
   + steps_o(length(A)).
because the comp field is incompatible with inferred comp:
[generic_comp] covered,is_det,mut_exclusive,not_fails,steps_lb(0.5*exp(length(A),2)+1.5*length(A)+1),steps_ub(0.5*exp(length(A),2)+1.5*length(A)+1)

ERROR (auto_interface): Errors detected. Further preprocessing aborted.

This message states that nrev will take at least 0.5(length(A))^2 + 1.5length(A) + 1 resolution steps (which is the cost analysis output, as in the previous example), while the assertion requires that the worst case cost of nrev be linear on length(A) (the size of the input argument).

If the programmer adds now the following ''check'' assertion:

:- check comp nrev(A,B) + steps_o(exp(length(A),2)).

:- checked calls nrev(A,B)
   : ( ground(A), list(A), var(B) ).

:- checked comp nrev(A,B)
   + steps_o(exp(length(A),2)).

CiaoPP can certify programs with resource consumption assurances [HALGP04].