Plug-in points for abstract domains

Author(s): Maria Garcia de la Banda, Francisco Bueno.

This module contains the predicates for selecting the abstract operations that correspond to an analysis domain. The selection depends on the name of the domain given as first argument to all predicates. Whenever a new domain is added to the system, a new clause for each predicate exported here will be needed to call the corresponding domain operation in the domain module. Some local operations used but not exported by this module would have to be defined, too. See the following chapter for an example domain module.

Adding an analysis domain to PLAI requires only changes in this module. However, in order for other CiaoPP operations to work, you may need to change other modules. See, for example, module infer_dom.

In this chapter, arguments referred to as Sv, Hv, Fv, Qv, Vars are lists of program variables and are supposed to always be sorted. Abstract substitutions are referred to as ASub, and are also supposed sorted (except where indicated), although this depends on the domain.

Usage and interface

Documentation on exports

PREDICATE
init_abstract_domain(AbsInt,Norm)

Initializes abstract domain AbsInt. Tells whether AbsInt requires a normalized program.

PREDICATE
amgu(AbsInt,Sg,Head,ASub,AMGU)

Perform the abstract unification AMGU between Sg and Head given an initial abstract substitution ASub and abstract domain AbsInt.

PREDICATE
call_to_entry(AbsInt,Sv,Sg,Hv,Head,Fv,Proj,Entry,ExtraInfo)

Obtains the abstract substitution Entry which results from adding the abstraction of the unification Sg = Head to abstract substitution Proj (the call substitution for Sg projected on its variables Sv) and then projecting the resulting substitution onto Hv (the variables of Head) plus Fv (the free variables of the relevant clause). ExtraInfo is information which may be reused later in other abstract operations.

PREDICATE
exit_to_prime(AbsInt,Sg,Hv,Head,Sv,Exit,ExtraInfo,Prime)

Computes the abstract substitution Prime which results from adding the abstraction of the unification Sg = Head to abstract substitution Exit (the exit substitution for a clause Head projected over its variables Hv), projecting the resulting substitution onto Sv.

PREDICATE
project(AbsInt,Vars,HvFv_u,ASub,Proj)

Projects the abstract substitution ASub onto the variables of list Vars resulting in the projected abstract substitution Proj.

PREDICATE
extend(AbsInt,Prime,Sv,Call,Succ)

Succ is the extension the information given by Prime (success abstract substitution over the goal variables Sv) to the rest of the variables of the clause in which the goal occurs (those over which abstract substitution Call is defined on). I.e., it is like a conjunction of the information in Prime and Call, except that they are defined over different sets of variables, and that Prime is a successor substitution to Call in the execution of the program.

PREDICATE
widen(AbsInt,ASub0,ASub1,ASub)

ASub is the result of widening abstract substitution ASub0 and ASub1, which are supposed to be consecutive approximations to the same abstract value.

PREDICATE
widencall(AbsInt,ASub0,ASub1,ASub)

ASub is the result of widening abstract substitution ASub0 and ASub1, which are supposed to be consecutive call patterns in a fixpoint computation.

PREDICATE
normalize_asub(AbsInt,ASub0,ASub1)

ASub1 is the result of normalizing abstract substitution ASub0. This is required in some domains, specially to perform the widening.

PREDICATE
compute_lub(AbsInt,ListASub,LubASub)

LubASub is the least upper bound of the abstract substitutions in list ListASub.

PREDICATE
glb(AbsInt,ASub0,ASub1,GlbASub)

GlbASub is the greatest lower bound of abstract substitutions ASub0 and ASub1.

PREDICATE
less_or_equal(AbsInt,ASub0,ASub1)

Succeeds if ASub1 is more general or equivalent to ASub0.

PREDICATE
less_or_equal_proj(AbsInt,Sg,Proj,Sg1,Proj1)

Abstract pattern Sg:Proj is less general or equivalent to abstract pattern Sg1:Proj1 in domain AbsInt.

PREDICATE
identical_abstract(AbsInt,ASub1,ASub2)

Succeeds if, in the particular abstract domain, the two abstract substitutions ASub1 and ASub2 are defined on the same variables and are equivalent.

PREDICATE
identical_proj(AbsInt,Sg,Proj,Sg1,Proj1)

Abstract patterns Sg:Proj and Sg1:Proj1 are equivalent in domain AbsInt. Note that Proj is assumed to be already sorted.

PREDICATE
identical_proj_1(AbsInt,Sg,Proj,Sg1,Proj1,Prime1,Prime2)

Abstract patterns Sg:Proj and Sg1:Proj1 are equivalent in domain AbsInt. Note that Proj is assumed to be already sorted. It is different from identical_proj/5 because it can be true although Sg and Sg1 are not variant

PREDICATE
abs_sort(AbsInt,ASub_u,ASub)

ASub is the result of sorting abstract substitution ASub_u.

PREDICATE
augment_asub(AbsInt,ASub,Vars,ASub0)

Augment the abstract substitution ASub adding the variables Vars and then resulting the abstract substitution ASub0.

PREDICATE
augment_two_asub(AbsInt,ASub0,ASub1,ASub)

ASub is an abstract substitution resulting of augmenting two abstract substitutions: ASub0 and ASub1 whose domains are disjoint.

PREDICATE
abs_subset(AbsInt,LASub1,LASub2)

Succeeds if each abstract substitution in list LASub1 is equivalent to some abstract substitution in list LASub2.

PREDICATE
eliminate_equivalent(AbsInt,TmpLSucc,LSucc)

The list LSucc is reduced wrt the list TmpLSucc in that it does not contain abstract substitutions which are equivalent.

PREDICATE
call_to_success_fact(AbsInt,Sg,Hv,Head,Sv,Call,Proj,Prime,Succ)

Specialized version of call_to_entry + entry_to_exit + exit_to_prime for a fact Head.

PREDICATE
body_succ_builtin(Type,AbsInt,Sg,Vs,Sv,Hv,Call,Proj,Succ)

Specialized version of call_to_entry + entry_to_exit + exit_to_prime + extend for predicate Sg considered a "builtin" of type Type in domain AbsInt. Whether a predicate is "builtin" in a domain is determined by special_builtin/5. There are two different ways to treat these predicates, depending on Type: success_builtin handles more usual types of "builtins", call_to_success_builtin handles particular predicates. The later is called when Type is of the form special(SgKey).

PREDICATE
special_builtin(AbsInt,SgKey,Sg,Subgoal,Type,Condvars)

Predicate Sg is considered a "builtin" of type Type in domain AbsInt. Types are domain dependent. Domains may have two different ways to treat these predicates: see body_succ_builtin/9.

PREDICATE
concrete(AbsInt,Var,ASub,List)

List are (all) the terms to which Var can be bound in the concretization of ASub, if they are a finite number of finite terms. Otherwise, the predicate fails.

PREDICATE
part_conc(AbsInt,Sg,Subs,NSg,NSubs)

This operation returns in NSg an instance of Sg in which the deterministic structure information available in Subs is materialized. The substitution NSubs refers to the variables in NSg.

PREDICATE
multi_part_conc(AbsInt,Sg,Subs,List)

Similar to part_conc but it gives instantiations of goals even in the case types are not deterministic, it generates a List of pairs of goals and substitutions. It stops unfolding types as soon as they are recursive.

PREDICATE
obtain_info(AbsInt,Prop,Vars,ASub,Info)

Obtains variables Info for which property Prop holds given abstract substitution ASub on variables Vars for domain AbsInt.

PREDICATE
info_to_asub(AbsInt,Kind,InputUser,Qv,ASub)

Obtains the abstract substitution ASub on variables Qv for domain AbsInt from the user supplied information InputUser refering to properties on Qv. It works by calling input_interface/5 on each property of InputUser which is a native property, so that they are accumulated, and then calls input_user_interface/4.

PREDICATE
full_info_to_asub(AbsInt,InputUser,Qv,ASub)

Same as info_to_asub(AbsInt,InputUser,Qv,ASub) except that it fails if some property in InputUser is not native or not relevant to the domain AbsInt.

PREDICATE
asub_to_info(AbsInt,ASub,Qv,OutputUser,CompProps)

Transforms an abstract substitution ASub on variables Qv for a domain AbsInt to a list of state properties OutputUser and computation properties CompProps, such that properties are visible in the preprocessing unit. It fails if ASub represents bottom. It works by calling asub_to_native/4.

PREDICATE
asub_to_native(AbsInt,ASub,Qv,NativeStat,NativeComp)

NativeStat and NativeComp are the list of native (state and computational, resp.) properties that are the concretization of abstract substitution ASub on variables Qv for domain AbsInt. These are later translated to the properties which are visible in the preprocessing unit.

PREDICATE
unknown_call(AbsInt,Sg,Vars,Call,Succ)

Succ is the result of adding to Call the "topmost" abstraction in domain AbsInt of the variables Vars involved in a literal Sg whose definition is not present in the preprocessing unit. I.e., it is like the conjunction of the information in Call with the top for a subset of its variables.

PREDICATE
unknown_call(AbsInt,Vars,Call,Succ)

Succ is the result of adding to Call the "topmost" abstraction in domain AbsInt of the variables Vars involved in a literal whose definition is not present in the preprocessing unit. I.e., it is like the conjunction of the information in Call with the top for a subset of its variables.

PREDICATE
unknown_entry(AbsInt,Sg,Vars,Entry)

Entry is the "topmost" abstraction in domain AbsInt of variables Vars corresponding to literal Sg.

PREDICATE
unknown_entry(AbsInt,Vars,Entry)

Entry is the "topmost" abstraction in domain AbsInt of variables Vars.

PREDICATE
empty_entry(AbsInt,Vars,Entry)

Entry is the "empty" abstraction in domain AbsInt of variables Vars. I.e., it is the abstraction of a substitution on Vars in which all variables are unbound: free and unaliased.

PREDICATE
collect_types_in_abs(ASub,AbsInt,Types,Tail)

Collects the type symbols occurring in ASub of domain AbsInt in a difference list Types-Tail.

PREDICATE
rename_types_in_abs(ASub0,AbsInt,Dict,ASub1)

Renames the type symbols occurring in ASub0 of domain AbsInt for the corresponding symbols as in (avl-tree) Dict yielding ASub1.

PREDICATE
dom_statistics(AbsInt,Info)

Obtains in list Info statistics about the results of the abstract interpreter AbsInt.

PREDICATE

Usage: abstract_instance(AbsInt,Sg1,Proj1,Sg2,Proj2)

  • Description: The pair <Sg1,Proj1> is an abstract instance of the pair <Sg2,Proj2>, i.e., the concretization of <Sg1,Proj1> is included in the concretization of <Sg2,Proj2>.

PREDICATE
contains_parameters(AbsInt,Subst)

True if an abstract substitution Subst contains type parameters

Documentation on multifiles

PREDICATE
aidomain(AbsInt)

Declares that AbsInt identifies an abstract domain.
The predicate is multifile.

Documentation on internals

PREDICATE
success_builtin(AbsInt,Type,Sv,Condvars,HvFv_u,Call,Succ)

Succ is the success substitution on domain AbsInt for a call Call to a goal of a "builtin" (domain dependent) type Type with variables Sv. Condvars can be used to transfer some information from special_builtin/5.

PREDICATE
call_to_success_builtin(AbsInt,Type,Sg,Sv,Call,Proj,Succ)

Succ is the success substitution on domain AbsInt for a call Call to a goal Sg with variables Sv considered of a "builtin" (domain dependent) type Type. Proj is Call projected on Sv.

PREDICATE
input_interface(AbsInt,Prop,Kind,Struc0,Struc1)

Prop is a native property that is relevant to domain AbsInt (i.e., the domain knows how to fully --+Kind=perfect-- or approximately ---Kind=approx-- abstract it) and Struct1 is a (domain defined) structure resulting of adding the (domain dependent) information conveyed by Prop to structure Struct0. This way, the properties relevant to a domain are being accumulated.

PREDICATE
input_user_interface(AbsInt,Struct,Qv,ASub)

ASub is the abstraction in AbsInt of the information collected in Struct (a domain defined structure) on variables Qv.

Known bugs and planned improvements

  • When interpreting assertions (and native) should take into account things like sourcename(X):- atom(X) and true pred atom(X) => atm(X).
  • body_succ_builtin/9 seems to introduce spurious choice-points.
  • Property covered/2 is not well understood by the domains.
  • Operation amgu/5 is missing.