The CiaoPP low-level programming interface

Usage:current_pp_flag(Name,Value)

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.

Usage:set_pp_flag(Name,Value)

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.

(True) Usage:push_pp_flag(Flag,Value)

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.

(True) Usage:pop_pp_flag(Flag)

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.

• 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.

Usage:flag_value(V)

V is a value for a flag.

Usage:valid_flag_value(Name,Value)

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.

Usage 1:transform(Trans)

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)

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.

Usage 1:module(FileName)

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)

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.

Usage:

Checks assertions w.r.t. analysis information.

Usage 1:analyze(Analysis)

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)

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.

Usage:output(Output)

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.

Usage:

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

• 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)

Analysis is a valid analysis identifier.

• 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)

Transformation is a valid transformation identifier.