The CiaoPP low-level programming interface

Author(s): The CLIP Group.

This module includes low-level primitives for interacting with CiaoPP. The exported predicates of this module are intended for developers only.

Documentation on exports

PREDICATE

Usage: current_pp_flag(Name,Value)

  • Description: Preprocess flag Name has the value Value.
  • The following properties should hold at call time:
    (pp_flag/1)Name is a valid preprocessor flag.
  • The following properties should hold upon exit:
    (valid_flag_value/2)Value is a valid value for preprocessor flag Name.

PREDICATE

Usage: set_pp_flag(Name,Value)

  • Description: Sets Value for preprocessor flag Name.
  • The following properties should hold at call time:
    (pp_flag/1)Name is a valid preprocessor flag.
    (valid_flag_value/2)Value is a valid value for preprocessor flag Name.

PREDICATE

Usage: push_pp_flag(Flag,Value)

  • Description: Sets Value for preprocessor flag Flag, storing the current value to restore it with pop_pp_flag/1.
  • The following properties should hold at call time:
    (pp_flag/1)Flag is a valid preprocessor flag.
    (valid_flag_value/2)Value is a valid value for preprocessor flag Flag.

PREDICATE

Usage: pop_pp_flag(Flag)

  • Description: Restores the value of the preprocessor flag Flag previous to the last non-canceled push_pp_flag/2 on it.
  • The following properties should hold at call time:
    (pp_flag/1)Flag is a valid preprocessor flag.

PREDICATE
Valid flags:
  • for the output:
    • analysis_info (off, on) Whether to output the results of analysis.
    • point_info (off,on) Whether to output analysis information for program points within clauses.
    • collapse_ai_vers (off, on) to output all the versions of call/success patterns inferred by analysis or just one version (summing-up all of them).
    • type_output (defined, all) to output the types inferred for predicates in terms only of types defined by the user or including types inferred anew.
  • for analysis:
    • fixpoint (plai, dd, di, check_di, check_di2, check_di3, check_di4) The kind of fixpoint computation used.
    • multi_success (off, on) Whether to allow success multivariance.
    • widen (off, on) Whether to perform widening.
    • intermod (off, on, auto) The policy for inter-modular analysis.
    • success_policy (best, first, all, top, botfirst, botbest, botall, bottom) The policy for obtaining success information for imported predicates during inter-modular analysis.
    • entry_policy (all, top_level, force, force_assrt) The policy for obtaining entry call patterns for exported predicates during inter-modular analysis.
    • process_libraries (on, off, no_engine) Whether to perform the analysis of Ciao system libraries when a modular user program is analyzed.
    • initial_guess (botfirst, botbest, botall, bottom) The policy for obtaining initial guess when computing the analysis of a predicate from the current module.
    • use_check_assrt (off, on) Whether to use check assertions for imported predicates as if they were trust assertions.
    • depth (a non-negative integer) The maximum depth of abstractions in analyses based on term depth.
    • type_eval (on, off) Whether to attempt concrete evaluation of types being inferred.
    • type_precision (defined, all) to use during type analysis only types defined by the user or also types inferred anew.
  • for partial evaluation:
    • global_control (off, id, inst, hom_emb) The abstraction function to use to control the creation of new patterns to analyze as a result of unfolding.
    • comp_rule (leftmost, safe_jb, bind_ins_jb, no_sideff_jb, jump_builtin, eval_builtin, local_emb) The computation rule for the selection of atoms in a goal.
    • local_control (off, orig, inst, det, det_la, depth, first_sol, first_sol_d, all_sol, hom_emb, hom_emb_anc, hom_emb_as, df_hom_emb_as, df_tree_hom_emb, df_hom_emb) The unfolding rule to use during partial evaluation.
    • unf_depth (a non-negative integer) The depth limit for unfolding.
    • rem_use_cls (off, pre, post, both) Whether to remove useless clauses.
    • abs_spec_defs (off, rem, exec, all) Whether to exploit abstract substitutions while obtaining specialized definitions on unfolding.
    • filter_nums (off, on) Whether to filter away numbers in partial evaluation.
    • exec_unif (off, on) Whether to execute unifications during specialization time or not.
    • pres_inf_fail (off, on) Whether infinite failure should be preserved in the specialized program.
    • part_concrete (off, mono, multi) The kind of partial concretization to be performed.
  • for parallelization and granularity control:
    • granularity_threshold (a non-negative integer) The threshold on computational cost at which parallel execution pays off.

REGTYPE

Usage: flag_value(V)

  • Description: V is a value for a flag.

PROPERTY

Usage: valid_flag_value(Name,Value)

  • Description: Value is a valid value for preprocessor flag Name.
  • If the following properties should hold at call time:
    (pp_flag/1)Name is a valid preprocessor flag.
    (flag_value/1)Value is a value for a flag.

(UNDOC_REEXPORT)
ctcheck_sum/1:
Imported from driver (see the corresponding documentation for details).

PREDICATE

Usage 1: transform(Trans)

  • Description: Returns on backtracking all available program transformation identifiers.
  • The following properties should hold at call time:
    (var/1)Trans is a free variable.
  • The following properties should hold upon exit:
    (transformation/1)Trans is a valid transformation identifier.

Usage 2: transform(Trans)

  • Description: Performs transformation Trans on the current module.
  • The following properties should hold at call time:
    (nonvar/1)Trans is currently a term which is not a free variable.
    (transformation/1)Trans is a valid transformation identifier.

PREDICATE

Usage 1: module(FileName)

  • Description: Reads the code of FileName and its preprocessing unit, and sets it as the current module.
  • The following properties should hold at call time:
    (nonvar/1)FileName is currently a term which is not a free variable.
    (sourcename/1)FileName is a source name.

Usage 2: module(FileNameList)

  • Description: Reads the code of the list of file names FileNameList (and their preprocessing units), and sets them as the current modules.
  • The following properties should hold at call time:
    (nonvar/1)FileNameList is currently a term which is not a free variable.
    (list/2)FileNameList is a list of atms.

(UNDOC_REEXPORT)
acheck_summary/1:
Imported from driver (see the corresponding documentation for details).

PREDICATE

Usage:

  • Description: Checks assertions w.r.t. analysis information.

PREDICATE

Usage 1: analyze(Analysis)

  • Description: Returns on backtracking all available analyses.
  • The following properties should hold at call time:
    (var/1)Analysis is a free variable.
  • The following properties should hold upon exit:
    (analysis/1)Analysis is a valid analysis identifier.

Usage 2: analyze(Analysis)

  • Description: Analyzes the current module with Analysis.
  • The following properties should hold at call time:
    (nonvar/1)Analysis is currently a term which is not a free variable.
    (analysis/1)Analysis is a valid analysis identifier.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form analyze(Analysis) do not fail.
    (no_choicepoints/1)A call to analyze(Analysis) does not create choicepoints.

(UNDOC_REEXPORT)
menu_branch/4:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
menu_branch/3:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
true/2:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
true/1:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
functor1/2:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
output/2:
Imported from printer (see the corresponding documentation for details).

PREDICATE

Usage: output(Output)

  • Description: Outputs the current module preprocessing state to a file Output.
  • The following properties should hold at call time:
    (nonvar/1)Output is currently a term which is not a free variable.

PREDICATE

Usage:

  • Description: Outputs the current Module preprocessing state to a file named Module_opt.pl, where Module is the current module.

(UNDOC_REEXPORT)
menu_branch/4:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
menu_branch/3:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
true/2:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
true/1:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
functor1/2:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
customize_and_exec_java/1:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
customize_java/1:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
select_modules/1:
Imported from auto_interface (see the corresponding documentation for details).

(UNDOC_REEXPORT)
clean_aux_files/1:
Imported from auto_interface (see the corresponding documentation for details).

Documentation on internals

PROPERTY
Analyses can be integrated in CiaoPP in an ad-hoc way (see the Internals manual), in which the CiaoPP menu would not be aware of them. The current analyses supported in the menu are:
  • for groundness and sharing:
    • gr tracks groundness in a very simple way.
    • def tracks groundness dependencies, which improves the accuracy in inferring groundness.
    • share tracks sharing among (sets of) variables [MH92], which gives a very accurate groundness inference, plus information on dependencies caused by unification.
    • son tracks sharing among pairs of variables, plus variables which are linear (see [Son86]).
    • shareson is a combination of the above two [CMB93], which may improve on the accuracy of any of them alone.
    • shfr tracks sharing and variables which are free (see [MH91]).
    • shfrson is a combination of shfr and son.
    • shfrnv augments shfr with knowledge on variables which are not free nor ground.

  • for term structure:
    • depth tracks the structure of the terms bound to the program variables during execution, up to a certain depth; the depth is fixed with the depth flag.
    • path tracks sharing among variables which occur within the terms bound to the program variables during execution; the occurrence of run-time variables within terms is tracked up to a certain depth, fixed with the depth flag.
    • aeq tracks the structure of the terms bound to the program variables during execution plus the sharing among the run-time variables occurring in such terms, plus freeness and linearity. The depth of terms being tracked is set with the depth flag. Sharing can be selected between set-sharing or pair-sharing.

  • for types:

    Type analysis supports different degrees of precision. For example, with the flag type\_precision with value defined, the analysis restricts the types to the finite domain of predefined types, i.e., the types defined by the user or in libraries, without generating new types. Another alternative is to use the normal analysis, i.e., creating new type definitions, but having only predefined types in the output. This is handled through the type\_output flag.

    • eterms performs structural widening (see [VB02]).

      Greater precision can be obtained evaluating builtins like is/2 abstractly: eterms includes a variant which allows evaluation of the types, which is governed by the type\_eval flag.

    • ptypes uses the topological clash widening operator (see [VHCL95]).
    • svterms implements the rigid types domain of [JB92].
    • terms uses shortening as the widening operator (see [GdW94]), in several fashions, which are selected via the depth flag; depth 0 meaning the use of restricted shortening [SG94].

  • for partial evaluation:

    Partial evaluation is performed during analysis when the local\_control flag is set to other than off. Flag fixpoint must be set to di. Unfolding will take place while analyzing the program, therefore creating new patterns to analyze. The unfolding rule is governed by flag local\_control (see transformation(codegen)).

    For partial evaluation to take place, an analysis domain capable of tracking term structure should be used (e.g., eterms, pd, etc.). In particular:

    • pd allows to perform traditional partial evaluation but using instead abstract interpretation with specialized definitions [PAH04].
    • pdb improves the precision of pd by detecting calls which cannot succeed, i.e., either loop or fail.

    Note that these two analyses will not infer useful information on the program. They are intended only to enable (classical) partial evaluation.

  • for constraint domains:
    • fr [Dum94] determines variables which are not constraint to particular values in the constraint store in which they occur, and also keeps track of possible dependencies between program variables.
    • frdef is a combination of fr and def, determining at the same time variables which are not constraint to particular values and variables which are constraint to a definite value.
    • lsign [MS94] infers the signs of variables involved in linear constraints (and the possible number and form of such constraints).
    • difflsign is a simplified variant of lsign.

  • for properties of the computation:

    • det detects procedures and goals that are deterministic (i.e. that produce at most one solution), or predicates whose clause tests are mutually exclusive (which implies that at most one of their clauses will succeed) even if they are not deterministic (because they call other predicates that can produce more than one solution).

    • nfg detects procedures that can be guaranteed not to fail (i.e., to produce at least one solution or not to terminate). It is a mono-variant non-failure analysis, in the sense that it infers non-failure information for only a call pattern per predicate [DLGH97].

    • nf detects procedures and goals that can be guaranteed not to fail and is able to infer separate non-failure information for different call patterns [BLGH04].

    • seff marks predicates as having side-effects or not.

  • for size of terms:

    Size analysis yields functions which give bounds on the size of output data of procedures as a function of the size of the input data. The size can be expressed in various measures, e.g., term-size, term-depth, list-length, integer-value, etc.

    • size\_ub infers upper bounds on the size of terms.
    • size\_lb infers lower bounds on the size of terms.
    • size\_ualb infers both upper and lower bounds on the size of terms.
    • size\_o gives (worst case) complexity orders for term size functions (i.e. big O).

  • for the number of resolution steps of the computation:

    Cost (steps) analysis yields functions which give bounds on the cost (expressed in the number of resolution steps) of procedures as a function of the size of their input data.

    • steps\_ub infers upper bounds on the number of resolution steps. Incorporates a modified version of the CASLOG [DL93] system, so that CiaoPP analyzers are used to supply automatically the information about modes, types, and size measures needed by the CASLOG system.

    • steps\_lb infers lower bounds on the number of resolution steps. Implements the analysis described in [DLGHL97].

    • steps\_ualb infers both upper and lower bounds on the number of resolution steps.

    • steps\_o gives (worst case) complexity orders for cost functions (i.e. big O).

  • for the execution time of the computation:

    • time\_ap yields functions which give approximations on the execution time (expressed in milliseconds) of procedures as a function of the size of their input data.

Usage: analysis(Analysis)

  • Description: Analysis is a valid analysis identifier.

PROPERTY
Transformations can be integrated in CiaoPP in an ad-hoc way (see the Internals manual), in which the CiaoPP menu would not be aware of them. The current transformations supported in the menu are:
  • for program specialization:
    • simp This transformation tries to explote analysis information in order to simplify the program as much as possible. It includes optimizations such as abstract executability of literals, removal of useless clauses, and unfolding of literals for predicates which are defined by just a fact or a single clause with just one literal in its body (a bridge). It also propagates failure backwards in a clause as long as such propagation is safe.
    • spec This transformation performs the same optimizations as simp but it also performs multiple specialization when this improves the possibilities of optimization. The starting point for this transformation is not a program annotated with analysis information, as in the case above, but rather an expanded program which corresponds to the analysis graph computed by multi-variant abstract interpretation. A minimization algorithm is used in order to guarantee that the resulting program is minimal in the sense that further collapsing versions would represent losing opportunities for optimization.
    • vers This transformation has in common with spec that it takes as starting point the expanded program which corresponds to the analysis graph computed by abstract interpretation. However, this transformation performs no optimizations and does not minimize the program. As a result, it generates the expanded program.

  • for partial evaluation:
    • codegen This generates the specialized program resulting from partial evaluation, obtained by unfolding goals during analysis. The kind of unfolding performed is governed by the comp\_rule flag, as follows:

      • leftmost unfolds the leftmost clause literal;
      • eval\_builtin selects for unfolding first builtins which can be evaluated;
      • local\_emb tries to select first atoms which do not endanger the embedding ordering or evaluable builtins whenever possible;
      • jump\_builtin selects the leftmost goal but can `jump' over (ignore) builtins when they are not evaluable. A main difference with the other computation rules is that unfolding is performed `in situ', i.e., without reordering the atoms in the clause.

      • safe\_jb same as jump\_builtin with the difference that it only jumps over a call to a builtin iff the call is safe [APG06] (i.e., it is error free, binding insensitive and side effect free).

      • bind\_ins\_jb same as safe\_jb with the difference that it only jumps over a call to a builtin iff the call is binding insensitive and side effect free.

      • no\_sideff\_jb same as bind\_ins\_jb with the difference that it only jumps over a call to a builtin iff it is side effect free.

      Unfolding is performed continuously on the already unfolded clauses, until a condition for stopping the process is satisfied. This condition is stablished by the local control policy, governed by the local\_control flag, as follows:

      • inst allows goal instantiation but no actual unfolding is performed.
      • orig returns the clauses in the original program for the corresponding predicate.
      • det allows unfolding while derivations are deterministic and stops them when a non-deterministic branch is required. Note that this may not be terminating.
      • det\_la same as det, but with look-ahead. It can perform a number of non-deterministic steps in the hope that the computation will turn deterministic. This number is determined by flag unf\_depth.
      • depth always performs the same number of unfolding steps for every call pattern. The number is determined by flag unf\_depth.
      • first\_sol explores the SLD tree width-first and keeps on unfolding until a first solution is found. It can be non-terminating.
      • first\_sol\_d same as above, but allows terminating when a given depth bound is reached without obtaining any solution. The bound is determined by unf\_depth.
      • all\_sol tries to generate all solutions by exploring the whole SLD tree. This strategy only terminates if the SLD is finite.
      • hom\_emb keeps on unfolding until the selected atom is homeomorphically embedded in an atom previously selected for unfolding.
      • hom\_emb\_anc same as before, but only takes into account previously selected atoms which are ancestors of the currently selected atom.
      • hom\_emb\_as same as before, but efficiently implemented by using a stack to store ancestors.
      • df\_hom\_emb\_as same as before, but traverses the SLD tree on a depth-first fashion (all strategies above use wide-first search). This allows better performance.
      • df\_tree\_hom\_emb same as above, but does not use the efficient stack-based implementation for ancestors.
      • df\_hom\_emb same as above, but compares with all previously selected atoms, and not only ancestors. It is like hom\_emb but with depth-first traversal.

    • global\_control In order to guarantee termination of the partial evaluation process, it is often required to abstract away information before unfolding. This is usually known as global control. This flag can have the following values:

      • off unfolds always;
      • id unfolds patterns which are not equal (modulo renaming) to a formerly analyzed pattern.
      • inst unfolds patterns which are not an instance of a previous pattern.
      • hom\_emb unfolds patterns which are not covered under the homeomorphic embedding ordering [Leu98].
      • hom\_emb\_num same as hom\_emb, but also considers that any number embeds any other number.

      Only hom\_emb guarantees termination. However, id and inst are more efficient, and terminating in many practical cases.

    • arg\_filtering This transformation removes from program literals static values which are not needed any longer in the resulting program. This is typically the case when some information is known at compile-time about the run-time values of arguments.

    • codegen\_af This performs codegen and arg\_filtering in a single traversal of the code. Good for efficiency.

  • for code size reduction:
    • slicing This transformation is very useful for debugging programs since it isolates those predicates that are reachable from a given goal. The goals used are those exported by the module. The `slice' being obtained is controlled by the following local control policies (described above): df\_hom\_emb\_as, df\_hom\_emb, df\_tree\_hom\_emb. It is also necessary to analyze the program with any of the currently available analyses for partial evaluation. Slicing is also very useful in order to perform other software engineering tasks, such as program understanding, maintenance, specialization, code reuse, etc.

  • for program parallelization:

    Parallelization is performed by considering goals the execution of which can be deemed as independent [HR95,GHM00] under certain conditions. Parallel expressions (possibly conditional) are built from such goals, in the following fashions:

    • mel exploits parallel expressions which preserve the ordering of literals in the clauses;
    • cdg tries to exploit every possible parallel expression, without preserving the initial ordering;
    • udg is as above, but only exploits unconditional parallel expressions [MBdlBH99];
    • urlp exploits unconditional parallel expressions for NSIAP with a posteriori conditions [CH94].
    • crlp exploits conditional parallel expressions for NSIAP with a posteriori conditions.

    • granul This transformation allows to perform run-time task granularity control of parallelized code (see [LGHD96a]), so that the program will decide at run-time whether to run parallel expressions or not. The decision is based on the value of flag granularity\_threshold.

  • for instrumenting the code for run-time assertion checking:
    • rtchecks Transforms the program so that it will check the predicate-level assertions at run-time.

Usage: transformation(Transformation)

  • Description: Transformation is a valid transformation identifier.

PREDICATE

Other information

In this section the flags related with program analysis are explained in some detail. In particular, special attention is given to inter-modular program analysis and partial deduction (performed in CiaoPP during analysis).

Analysis with PLAI

Most of the analyses of CiaoPP are performed with the PLAI (Programming in Logic with Abstract Interpretation) framework [BGH94]. This framework is based on the computation of a fixed point for the information being inferred. Such a fixed point computation is governed by flag fixpoint, whose values are:

  • plai for the classical fixed point computation [MH89a];
  • dd for an incremental fixed point computation [HPMS00];
  • di for the depth independent fixed point algorithm of [HPMS00];
  • check\_di .

Inter-modular analysis

In inter-modular analysis CiaoPP takes into account the results of analyzing a module when other modules in the same program are analyzed. Thus, it collects analysis results (success patterns) for calls to predicates in other modules to improve the analysis of a given module. It also collects calls (call patterns) that are issued by the given module to other modules to reconsider them during analysis of such other modules.

Such flow of analysis information between modules while being analyzed can be performed when analyzing one single module. The information flow then affects only the modules imported by it. New call patterns will be taken into account when/if it is the turn for such imported modules to be analyzed. Improved success patterns will only be reused when/if the importing module is reanalyzed. However, CiaoPP can also iterate continuously over the set of modules of a given program, transferring the information from one module to others, and deciding which modules to analyze at which moment. This will be done until an inter-modular fixed point is reached in the analysis of the whole program (whereas analysis is performed one-module-at-a-time, anyway).

Inter-modular analysis is enabled with flag intermod. During inter-modular analysis there are several possible choices for selecting success patterns and call patterns. For example, when a success pattern is required for a given call pattern to an imported predicate, and there exist several that could be used, but none of them fit exactly with the given call pattern. Also, if, in that same case, there are no success patterns that fit (in which case CiaoPP has to make an initial guess). Finally, when there are new call patterns to a given module obtained during analysis of the modules that import it, which of them to use as entry points should be decided. All these features are governed by the following flags:

  • intermod to activate inter-modular analysis.
    • off disables inter-modular analysis. This is the default value.
    • on enables inter-modular analysis.
    • auto allows the analysis of a modular program, using intermod:auto\_analyze/2-3 with the main module of the program, iterating through the module graph until an inter-modular fixed point is reached. This value is set automatically by CiaoPP, and it should not be set by the user.

  • success\_policy to obtain success information for given call patterns to imported predicates.
    • best selects the success pattern which corresponds to the best over-approximation of the sought call pattern; if there are several non-comparable best over-approximations, one of them is chosen randomly.
    • first selects the first success pattern which corresponds to a call pattern which is an over-approximation of the sought call pattern.
    • all computes the greatest lower bound of the success patterns that correspond to over-approximating call patterns.
    • top selects Top (no information) as answer pattern for any call pattern.
    • botfirst selects the first success pattern which corresponds to a call pattern which is an under-approximation of the sought call pattern.
    • botbest selects the success pattern which corresponds to the best under-approximation of the sought call pattern; if there are several non-comparable best under-approximations, one of them is chosen randomly.
    • botall computes the least upper bound of the success patterns that correspond to under-approximating call patterns.
    • bottom selects Bottom (failure) as answer pattern for any call pattern.

  • initial\_guess to obtain an initial guess for the success pattern corresponding to a call pattern to an imported predicate when there is none that fully matches.
    • botfirst selects the success pattern already computed corresponding to the first call pattern which is an under-approximation of the given call pattern.
    • botbest selects the success pattern corresponding to the call pattern which best under-approximates the given call pattern (if there are several, non-comparable call patterns, one of them is selected randomly).
    • botall computes the least upper bound of the success patterns that correspond to under-approximating call patterns.
    • bottom selects Bottom as initial guess for any call pattern.

  • entry\_policy to obtain entry call patterns for exported predicates.
    • all selects all entry call patterns for the current module which have not been analyzed yet, either from entry assertions found in the source code, or from the analysis of other modules that import the current module.
    • top\_level is only meaningful during auto inter-modular analysis, and it is set automatically by CiaoPP. If the current module is the top-level module (the main module of the modular program being analyzed), the entry policy behaves like all. In any other case, it selects entry call patterns for the current module from the analysis of other modules that import it, ignoring entry assertions found in the source code.
    • force forces the analysis of all entries of the module (from both the module source code and calling modules), even if they have been already analyzed.
    • force\_assrt forces the analysis of all entries coming from the module source code, but does not analyze entries relative to calling modules, even if they need to be (re)analyzed.

  • process\_libraries to indicate that Ciao system libraries must also be analyzed when a modular user program is analyzed.
    • off disables the analysis of any Ciao system library.
    • on enables the analysis of all Ciao system libraries.
    • no\_engine enables the analysis of Ciao system libraries which are not engine libraries.

  • use\_check\_assrt to indicate that check assertions for imported predicates will be used as trust assertions. This is specially interesting when performing intermodular compile-time checking.

    • off disables the use of check assertions as trust assertions for imported predicates.
    • on enables the use of check assertions as trust assertions.

Abstract partial deduction

Partial deduction (or partial evaluation) is a program transformation technique which specializes the program w.r.t. information known at compile-time. In CiaoPP this is performed during analysis of the program, so that not only concrete information but also abstract information (from the analysis) can be used for specialization. With analysis domain pd (and pdb) only concrete values will be used; with other analysis domains the domain abstract values inferred will also be used. This feature is governed by the following flags:

  • abs\_spec\_defs to exploit abstract substitutions in order to:

    • rem try to eliminate clauses which are incompatible with the inferred substitution at each unfolding step;
    • exec perform abstract executability of atoms;
    • all do both.

  • part\_concrete to try to convert abstract information into concrete information if possible, so that:

    • mono one concrete atom is obtained;
    • multi multiple atoms are allowed when the information in the abstract substitution is disjunctive.

  • rem\_use\_cls to identify clauses which are incompatible with the abstract call substitution and remove them:

    • pre prior to performing any unfolding steps;
    • post after performing unfolding steps;
    • both both before and after performing unfolding steps.

  • filter\_nums to filter away during partial evaluation numbers which:

    • safe are not safe, i.e., do not appear in the original program, or
    • on all numbers.


Known bugs and planned improvements

  • 1 The ciaopp version number is now hardwired instead of being automatically updated