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
- Library usage:
:- use_module(library(domains)). - Exports:
- Predicates:
init_abstract_domain/2, amgu/5, call_to_entry/9, exit_to_prime/8, project/5, extend/5, widen/4, widencall/4, normalize_asub/3, compute_lub/3, glb/4, less_or_equal/3, less_or_equal_proj/5, identical_abstract/3, identical_proj/5, identical_proj_1/7, abs_sort/3, augment_asub/4, augment_two_asub/4, abs_subset/3, eliminate_equivalent/3, call_to_success_fact/9, body_succ_builtin/9, special_builtin/6, concrete/4, part_conc/5, multi_part_conc/4, obtain_info/5, info_to_asub/5, full_info_to_asub/4, asub_to_info/5, asub_to_native/5, unknown_call/5, unknown_call/4, unknown_entry/4, unknown_entry/3, empty_entry/3, collect_types_in_abs/4, rename_types_in_abs/4, dom_statistics/2, abstract_instance/5, contains_parameters/2. - Multifiles:
aidomain/1.
- Predicates:
- Imports:
- Application modules:
program(p_unit), ciaopp(preprocess_flags), plai(plai_errors), plai(fixpo_ops), domain(pd), domain(pdb), domain(gr), domain(java_nullity), domain(def), domain(fd), domain(fr_top), domain(lsign), domain(share), domain(shfret), domain(shareson), domain(shfrson), domain(sondergaard), domain(oo_son), domain(oo_shnltau), domain(share_amgu), domain(share_clique), domain(bshare(bshare)), domain(aeq_top), domain(depthk), domain(top_path_sharing), domain(eterms), domain(svterms), domain(termsd), domain(ptypes), domain(polyhedra), domain(oo_types), domain(deftypes), domain(java_cha), domain(nfplai), domain(detplai), infer(low_level_props). - System library modules:
terms_check, terms_vars, sets, sort, messages, assertions/native_props. - Internal (engine) modules:
term_basic, arithmetic, atomic_basic, basic_props, basiccontrol, data_facts, exceptions, io_aux, io_basic, prolog_flags, streams_basic, system_info, term_compare, term_typing, hiord_rt, debugger_support. - Packages:
prelude, nonpure, assertions, regtypes.
- Application modules:
Documentation on exports
Initializes abstract domain AbsInt. Tells whether AbsInt requires a normalized program.
Perform the abstract unification AMGU between Sg and Head given an initial abstract substitution ASub and abstract domain AbsInt.
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.
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.
Projects the abstract substitution ASub onto the variables of list Vars resulting in the projected abstract substitution Proj.
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.
ASub is the result of widening abstract substitution ASub0 and ASub1, which are supposed to be consecutive approximations to the same abstract value.
ASub is the result of widening abstract substitution ASub0 and ASub1, which are supposed to be consecutive call patterns in a fixpoint computation.
ASub1 is the result of normalizing abstract substitution ASub0. This is required in some domains, specially to perform the widening.
LubASub is the least upper bound of the abstract substitutions in list ListASub.
GlbASub is the greatest lower bound of abstract substitutions ASub0 and ASub1.
Succeeds if ASub1 is more general or equivalent to ASub0.
Abstract pattern Sg:Proj is less general or equivalent to abstract pattern Sg1:Proj1 in domain AbsInt.
Succeeds if, in the particular abstract domain, the two abstract substitutions ASub1 and ASub2 are defined on the same variables and are equivalent.
Abstract patterns Sg:Proj and Sg1:Proj1 are equivalent in domain AbsInt. Note that Proj is assumed to be already sorted.
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
ASub is the result of sorting abstract substitution ASub_u.
Augment the abstract substitution ASub adding the variables Vars and then resulting the abstract substitution ASub0.
ASub is an abstract substitution resulting of augmenting two abstract substitutions: ASub0 and ASub1 whose domains are disjoint.
Succeeds if each abstract substitution in list LASub1 is equivalent to some abstract substitution in list LASub2.
The list LSucc is reduced wrt the list TmpLSucc in that it does not contain abstract substitutions which are equivalent.
Specialized version of call_to_entry + entry_to_exit + exit_to_prime for a fact Head.
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 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.
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.
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.
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.
Obtains variables Info for which property Prop holds given abstract substitution ASub on variables Vars for domain AbsInt.
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.
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.
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.
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.
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.
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.
Entry is the "topmost" abstraction in domain AbsInt of variables Vars corresponding to literal Sg.
Entry is the "topmost" abstraction in domain AbsInt of variables Vars.
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.
Collects the type symbols occurring in ASub of domain AbsInt in a difference list Types-Tail.
Renames the type symbols occurring in ASub0 of domain AbsInt for the corresponding symbols as in (avl-tree) Dict yielding ASub1.
Obtains in list Info statistics about the results of the abstract interpreter AbsInt.
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>.
True if an abstract substitution Subst contains type parameters
Documentation on multifiles
Declares that AbsInt identifies an abstract domain.
The predicate is multifile.
Documentation on internals
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.
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.
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.
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.
