☰

Domain Interface for Defining Abstract Domains

Author(s): Maria Garcia de la Banda, Francisco Bueno, Jose F. Morales (aidomain package).

This module contains the predicates that can be used to define the abstract operations that correspond to an analysis domain. The name of the domain is given as first argument to all predicates. Thus, whenever a new domain is added to the system, a new clause for each predicate exported here will be needed to be defined in the new domain's module without featuring the first argument.

Notice that not all the operations need to be implemented in order to define an abstract domain in PLAI. Some are optional and only required to accelerate or guarantee the convergence (for instance widen/3) while other are only required if some special fixpoints. 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. 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.

Variable naming convention for CiaoPP domains

Both in the PLAI fixpoints and domains, for simplicity, we use the following variable name meanings:

  • AbsInt : Identifier of the abstract domain being used.
  • Sg : Subgoal being analysed.
  • SgKey : Subgoal key (represented by functor/arity).
  • Head : Head of the clause being analysed.
  • Sv : Subgoal variables.
  • Hv : Head variables.
  • Fv : Free variables in the body of the clause being considered.
  • Vars : Any possible set of variables.
  • Call : Abstract call substitution.
  • Proj : Call projected onto Sv.
  • Entry : Abstract entry substitution (i.e. the abstract subtitution obtained after the abstract unification of Sg and Head projected onto Hv + Fv).
  • Exit : Abstract exit substitution (i.e. the abstract subtitution obtained after the analysis of the clause being considered projected onto Hv).
  • Prime : Abstract prime substitution (i.e. the abstract subtitution obtained after the analysis of the clause being considered projected onto Sv).
  • Succ : Abstract success substitution (i.e. the abstract subtitution obtained after the analysis of the clause being considered extended to the variables of the clause in which Sg appears).
  • ASub : Any possible abstract substitution.
  • R_flag : Flag which represents the recursive characteristics of a predicate. It will be ``nr'' in case the predicate be non recursive. Otherwise it will be r (recursive).
  • List : (can be represented as OldList,List,AddList,IdList,NewList) current the list of nodes which a given node depends on.
  • _s : The suffix _s means that the term to which the variable is bound to has been sorted. By default they are always sorted thus _s is added only when it appears neccessary to say it explicitely.
  • _uns : The suffix _uns means that the term to which the variable is bound is not sorted.
  • ExtraInfo: Info computed during the call_to_entry that can be reused during the exit_to_prime step.

Usage and interface

Documentation on exports

PREDICATEinit_abstract_domain/2

Usage:init_abstract_domain(AbsInt,PushedFlags)

Initializes abstract domain AbsInt. Tells the list of modified (pushed) PP flags to pop afterwards.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)PushedFlags is currently a term which is not a free variable.

PREDICATEamgu/5

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Head is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)AMGU is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form amgu(AbsInt,Sg,Head,ASub,AMGU) do not fail.

PREDICATEaugment_asub/4

Usage:augment_asub(AbsInt,ASub,Vars,ASub0)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)ASub0 is currently a term which is not a free variable.

PREDICATEaugment_two_asub/4

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (nonvar/1)ASub1 is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)ASub is currently a term which is not a free variable.

PREDICATEcall_to_entry/10

Usage:call_to_entry(AbsInt,Sv,Sg,Hv,Head,ClauseKey,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.

Assumtions: This predicate assumes that the variables in Sv and Proj are sorted (see sortedness for each domain).

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sv is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Hv is currently a term which is not a free variable.
    (nonvar/1)Head is currently a term which is not a free variable.
    (nonvar/1)ClauseKey is currently a term which is not a free variable.
    (nonvar/1)Fv is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
    (list/1)Sv is a list.
    (list/1)Hv is a list.
    (list/1)Fv is a list.
  • The following properties should hold upon exit:
    (nonvar/1)Entry is currently a term which is not a free variable.
    (nonvar/1)ExtraInfo is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form call_to_entry(AbsInt,Sv,Sg,Hv,Head,ClauseKey,Fv,Proj,Entry,ExtraInfo) do not fail.
    (is_det/1)All calls of the form call_to_entry(AbsInt,Sv,Sg,Hv,Head,ClauseKey,Fv,Proj,Entry,ExtraInfo) are deterministic.

PREDICATEexit_to_prime/8

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Hv is currently a term which is not a free variable.
    (nonvar/1)Head is currently a term which is not a free variable.
    (nonvar/1)Sv is currently a term which is not a free variable.
    (nonvar/1)Exit is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
    (list/2)Hv is a list of vars.
    (list/2)Sv is a list of vars.
  • The following properties should hold upon exit:
    (nonvar/1)Prime is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form exit_to_prime(AbsInt,Sg,Hv,Head,Sv,Exit,ExtraInfo,Prime) do not fail.

PREDICATEproject/5

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
    (nonvar/1)HvFv_u is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
    (list/1)Vars is a list.
    (list/1)HvFv_u is a list.
    (term/1)ASub is any term.
    (term/1)Proj is any term.
  • The following properties should hold upon exit:
    (nonvar/1)Proj is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form project(AbsInt,Vars,HvFv_u,ASub,Proj) do not fail.
    (is_det/1)All calls of the form project(AbsInt,Vars,HvFv_u,ASub,Proj) are deterministic.

PREDICATEproject/6

Usage:project(AbsInt,Sg,Vars,HvFv_u,ASub,Proj)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
    (nonvar/1)HvFv_u is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
    (term/1)Sg is any term.
    (list/1)Vars is a list.
    (list/1)HvFv_u is a list.
    (term/1)ASub is any term.
    (term/1)Proj is any term.
  • The following properties should hold upon exit:
    (nonvar/1)Proj is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form project(AbsInt,Sg,Vars,HvFv_u,ASub,Proj) do not fail.
    (is_det/1)All calls of the form project(AbsInt,Sg,Vars,HvFv_u,ASub,Proj) are deterministic.

PREDICATEneeds/2

Usage:needs(AbsInt,Op)

Succeeds if AbsInt needs operation Op for correctness/termination. It must only be used for checking, not enumerating. The supported operations are: widen (whether widening is necessary for termination), clauses_lub (whether the lub must be performed over the abstract substitution split by clase), split_combined_domain (whether the domain contains information of several domains and it needs to be split), and aux_info (whether the information in the abstract substitutions is not complete and an external solver may be needed, currently only used when outputing the analysis in a .dump file)

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Op is currently a term which is not a free variable.
  • The following properties should hold globally:
    (is_det/1)All calls of the form needs(AbsInt,Op) are deterministic.

PREDICATEwidencall/4

Usage: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.

This predicate is allowed to fail and it fails if the domain does not define a widening on calls.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (nonvar/1)ASub1 is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)ASub is currently a term which is not a free variable.

PREDICATEdual_widencall/4

Usage:dual_widencall(AbsInt,ASub0,ASub1,ASub)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (nonvar/1)ASub1 is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)ASub is currently a term which is not a free variable.

PREDICATEwiden/4

Usage: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. I.e., less_or_equal(AbsInt,ASub0,ASub1) succeeds.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (nonvar/1)ASub1 is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)ASub is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form widen(AbsInt,ASub0,ASub1,ASub) do not fail.

PREDICATEdual_widen/4

Usage:dual_widen(AbsInt,ASub0,ASub1,ASub)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (nonvar/1)ASub1 is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)ASub is currently a term which is not a free variable.

PREDICATEnormalize_asub/3

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)ASub1 is currently a term which is not a free variable.

PREDICATEcompute_lub/3

Usage:compute_lub(AbsInt,ListASub,LubASub)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ListASub is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
    (list/1)ListASub is a list.
    (term/1)LubASub is any term.
  • The following properties should hold upon exit:
    (nonvar/1)LubASub is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form compute_lub(AbsInt,ListASub,LubASub) do not fail.
    (is_det/1)All calls of the form compute_lub(AbsInt,ListASub,LubASub) are deterministic.

PREDICATEcompute_glb/3

Usage:compute_glb(AbsInt,ListASub,GlbASub)

GlbASub is the greatest lower bound of the abstract substitutions in list ListASub.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ListASub is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)GlbASub is currently a term which is not a free variable.

PREDICATEidentical_proj/5

Usage: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.

This predicate unifies Sg and Sg1.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (nonvar/1)Sg1 is currently a term which is not a free variable.
    (nonvar/1)Proj1 is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.

PREDICATEidentical_proj_1/7

Usage: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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (nonvar/1)Sg1 is currently a term which is not a free variable.
    (nonvar/1)Proj1 is currently a term which is not a free variable.
    (nonvar/1)Prime1 is currently a term which is not a free variable.
    (nonvar/1)Prime2 is currently a term which is not a free variable.

PREDICATEidentical_abstract/3

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub1 is currently a term which is not a free variable.
    (nonvar/1)ASub2 is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.

PREDICATEabs_sort/3

Usage:abs_sort(AbsInt,ASub_u,ASub)

ASub is the result of sorting abstract substitution ASub_u.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub_u is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form abs_sort(AbsInt,ASub_u,ASub) do not fail.
    (is_det/1)All calls of the form abs_sort(AbsInt,ASub_u,ASub) are deterministic.

PREDICATEextend/6

Usage:extend(AbsInt,Sg,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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Prime is currently a term which is not a free variable.
    (nonvar/1)Sv is currently a term which is not a free variable.
    (nonvar/1)Call is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)Succ is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form extend(AbsInt,Sg,Prime,Sv,Call,Succ) do not fail.
    (is_det/1)All calls of the form extend(AbsInt,Sg,Prime,Sv,Call,Succ) are deterministic.

PREDICATEless_or_equal_proj/5

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (nonvar/1)Sg1 is currently a term which is not a free variable.
    (nonvar/1)Proj1 is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.

PREDICATEless_or_equal/3

Usage:less_or_equal(AbsInt,ASub0,ASub1)

Succeeds if ASub1 is more general or equivalent to ASub0.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (nonvar/1)ASub1 is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.

PREDICATEglb/4

Usage:glb(AbsInt,ASub0,ASub1,GlbASub)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (nonvar/1)ASub1 is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)GlbASub is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form glb(AbsInt,ASub0,ASub1,GlbASub) do not fail.
    (is_det/1)All calls of the form glb(AbsInt,ASub0,ASub1,GlbASub) are deterministic.

PREDICATEeliminate_equivalent/3

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)TmpLSucc is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)LSucc is currently a term which is not a free variable.

PREDICATEabs_subset/3

Usage:abs_subset(AbsInt,LASub1,LASub2)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)LASub1 is currently a term which is not a free variable.
    (nonvar/1)LASub2 is currently a term which is not a free variable.

PREDICATEcall_to_success_fact/10

Usage:call_to_success_fact(AbsInt,Sg,Hv,Head,K,Sv,Call,Proj,Prime,Succ)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Hv is currently a term which is not a free variable.
    (nonvar/1)Head is currently a term which is not a free variable.
    (nonvar/1)K is currently a term which is not a free variable.
    (nonvar/1)Sv is currently a term which is not a free variable.
    (nonvar/1)Call is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)Prime is currently a term which is not a free variable.
    (nonvar/1)Succ is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form call_to_success_fact(AbsInt,Sg,Hv,Head,K,Sv,Call,Proj,Prime,Succ) do not fail.

PREDICATEspecial_builtin/6

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)SgKey is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)Type is currently a term which is not a free variable.

PREDICATEbody_succ_builtin/9

Usage:body_succ_builtin(AbsInt,Type,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).

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Type is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Sv is currently a term which is not a free variable.
    (nonvar/1)Hv is currently a term which is not a free variable.
    (nonvar/1)Call is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)Succ is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form body_succ_builtin(AbsInt,Type,Sg,Vs,Sv,Hv,Call,Proj,Succ) do not fail.

PREDICATEsuccess_builtin/7

Usage: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.

  • The following properties should hold at call time:
    (atm/1)AbsInt is an atom.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form success_builtin(AbsInt,Type,Sv,Condvars,HvFv_u,Call,Succ) do not fail.

PREDICATEobtain_info/5

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Prop is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
  • The following properties should hold upon exit:
    (nonvar/1)Info is currently a term which is not a free variable.

PREDICATEinfo_to_asub/7

Usage:info_to_asub(AbsInt,Kind,InputUser,Qv,ASub,Sg,MaybeCallASub)

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/6.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)InputUser is currently a term which is not a free variable.
    (nonvar/1)Qv is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)MaybeCallASub is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)ASub is currently a term which is not a free variable.

PREDICATEfull_info_to_asub/5

Usage:full_info_to_asub(AbsInt,InputUser,Qv,ASub,Sg)

Behaves similar as info_to_asub/7 except that it fails if some property in InputUser is not native or not relevant to the domain AbsInt.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)InputUser is currently a term which is not a free variable.
    (nonvar/1)Qv is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)ASub is currently a term which is not a free variable.

PREDICATEasub_to_info/5

Usage: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/6.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
    (nonvar/1)Qv is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)OutputUser is currently a term which is not a free variable.
    (nonvar/1)CompProps is currently a term which is not a free variable.

PREDICATEasub_to_native/6

Usage:asub_to_native(AbsInt,ASub,Qv,OutFlag,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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
    (nonvar/1)Qv is currently a term which is not a free variable.
    (nonvar/1)OutFlag is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)NativeStat is currently a term which is not a free variable.
    (nonvar/1)NativeComp is currently a term which is not a free variable.

PREDICATEconcrete/4

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Var is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)List is currently a term which is not a free variable.

PREDICATEunknown_call/5

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
    (nonvar/1)Call is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
    (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Vars is a list.
  • The following properties should hold upon exit:
    (nonvar/1)Succ is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form unknown_call(AbsInt,Sg,Vars,Call,Succ) do not fail.

PREDICATEunknown_entry/4

Usage:unknown_entry(AbsInt,Sg,Vars,Entry)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
    (list/1)Vars is a list.
  • The following properties should hold upon exit:
    (nonvar/1)Entry is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form unknown_entry(AbsInt,Sg,Vars,Entry) do not fail.

PREDICATEempty_entry/4

Usage:empty_entry(AbsInt,Sg,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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
    (atm/1)AbsInt is an atom.
    (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Vars is a list.
    (term/1)Entry is any term.
  • The following properties should hold upon exit:
    (nonvar/1)Entry is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form empty_entry(AbsInt,Sg,Vars,Entry) do not fail.

PREDICATEpart_conc/5

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Subs is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)NSg is currently a term which is not a free variable.
    (nonvar/1)NSubs is currently a term which is not a free variable.

PREDICATEmulti_part_conc/4

Usage:multi_part_conc(AbsInt,Sg,Subs,List)

Similar to part_conc/5 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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Subs is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)List is currently a term which is not a free variable.

PREDICATEcollect_types_in_abs/4

Usage:collect_types_in_abs(ASub,AbsInt,Types,Tail)

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

  • The following properties should hold at call time:
    (nonvar/1)ASub is currently a term which is not a free variable.
    (nonvar/1)AbsInt is currently a term which is not a free variable.
  • The following properties should hold globally:
    (is_det/1)All calls of the form collect_types_in_abs(ASub,AbsInt,Types,Tail) are deterministic.
    (not_fails/1)All the calls of the form collect_types_in_abs(ASub,AbsInt,Types,Tail) do not fail.

PREDICATErename_types_in_abs/4

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Dict is currently a term which is not a free variable.
  • The following properties should hold globally:
    (is_det/1)All calls of the form rename_types_in_abs(ASub0,AbsInt,Dict,ASub1) are deterministic.
    (not_fails/1)All the calls of the form rename_types_in_abs(ASub0,AbsInt,Dict,ASub1) do not fail.

PREDICATEdom_statistics/2

Usage:dom_statistics(AbsInt,Info)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)Info is currently a term which is not a free variable.

PREDICATEabstract_instance/5

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

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Sg1 is currently a term which is not a free variable.
    (nonvar/1)Proj1 is currently a term which is not a free variable.
    (nonvar/1)Sg2 is currently a term which is not a free variable.
    (nonvar/1)Proj2 is currently a term which is not a free variable.

PREDICATEcontains_parameters/2

Usage:contains_parameters(AbsInt,Subst)

True if an abstract substitution Subst contains type parameters

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Subst is currently a term which is not a free variable.

PREDICATEabsub_eliminate_equivalent/3

Usage:absub_eliminate_equivalent(ASubList,AbsInt,NewASubList)

This predicate is already defined and should not be redefined. Given a list of abstractions ASubList for the domain AbsInt, NewASubList is a list of abstractions such that for each element in AsubList it is in NewASubList or there exists an equivalent abstraction in NewASubList. And for each two elements in NewASubList they are not equivalent abstractions.

  • The following properties should hold at call time:
    (nonvar/1)ASubList is currently a term which is not a free variable.
    (nonvar/1)AbsInt is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)NewASubList is currently a term which is not a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form absub_eliminate_equivalent(ASubList,AbsInt,NewASubList) do not fail.

Documentation on multifiles

PREDICATEaidomain/1
aidomain(AbsInt)

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

PREDICATEaidom.init_abstract_domain/2
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.amgu/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.augment_asub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.augment_two_asub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.call_to_entry/10
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.exit_to_prime/8
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.project/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.widencall/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.needs/2
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.widen/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.compute_lub/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.compute_clauses_lub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.compute_clauses_glb/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.fixpoint_covered/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.fixpoint_covered_gfp/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.identical_abstract/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.abs_sort/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.extend/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.less_or_equal/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.glb/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.eliminate_equivalent/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.abs_subset/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.call_to_success_fact/10
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.special_builtin/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.combined_special_builtin0/3
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.body_succ_builtin/9
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.split_combined_domain/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.success_builtin/7
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.call_to_success_builtin/7
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.obtain_info/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.input_interface/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.input_user_interface/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.asub_to_native/6
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.concrete/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.unknown_call/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.unknown_entry/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.empty_entry/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.part_conc/5
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.multi_part_conc/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.collect_auxinfo_asub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.rename_auxinfo_asub/4
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.dom_statistics/2
No further documentation available for this predicate. The predicate is multifile.

PREDICATEaidom.contains_parameters/2
No further documentation available for this predicate. The predicate is multifile.

Documentation on internals

PREDICATEcall_to_success_builtin/7

Usage: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.

  • The following properties should hold globally:
    (not_fails/1)All the calls of the form call_to_success_builtin(AbsInt,Type,Sg,Sv,Call,Proj,Succ) do not fail.

PREDICATEinput_interface/5

Usage: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.

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Prop is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)Struc1 is currently a term which is not a free variable.

PREDICATEinput_user_interface/6

Usage:input_user_interface(AbsInt,Struct,Qv,ASub,Sg,MaybeCallASub)

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

  • The following properties should hold at call time:
    (nonvar/1)AbsInt is currently a term which is not a free variable.
    (nonvar/1)Qv is currently a term which is not a free variable.
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)MaybeCallASub is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)ASub is currently a term which is not a free variable.

Generated with LPdoc using Ciao