Available abstract domains

Groundness and sharing

• gr tracks groundness in a very simple way (see Simple groundness abstract domain).
• 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.

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.

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

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.

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.

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.

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

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

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.