def: definiteness (abstract domain)

Author(s): Maria Garcia de la Banda, Manuel Hermenegildo.

Stability: [beta] Most of the functionality is there but it is still missing some testing and/or verification.

This file contains the definiteness abstract domain and abstract unctions for CLP languages.

The abstract constraint is kept as a(Ground,Set) in which:

Ground is a sorted list of uniquely defined variables
Set is a sorted list of elements with format (X,SS) in which X is a variable and SS is a sorted set of set of variables such that for each S in SS, uniquely defining all variables in S, uniquely defines X, and there is no S' in SS, such that S' subseteq S.
Not that top variables (variables from which nothing is known) cannot appear in Ground but can appear in some SS.

Meaning of the Program Variables

AbsInt : identifier of the abstract interpreter being used.
Sg : Subgoal being analysed.
SgKey : Subgoal key (represented by functor/arity).
Sv : Subgoal variables.
Call : Abstract call constraint.
Proj : Call projected onto Sv.
Head : Head of one of the clauses which define the Sg predicate.
Hv : Head variables.
Fv : Free variables in the body of the clause being considered
Entry : Abstract entry constraint (i.e. the abstract subtitution obtained after the abstract unification of Sg and Head projected onto Hv + Fv).
BothEntry: Similar to the abstract entry constraint: the abstract subtitution obtained after the abstract unification of Sg and Head but without being projected onto Hv + Fv).
Exit : Abstract exit constraint (i.e. the abstract subtitution obtained after the analysis of the clause being considered projected onto Hv).
Prime : Abstract prime constraint (i.e. the abstract subtitution obtained after the analysis of the clause being considered projected onto Sv).
BPrime : similar to the abstract prime constraint: abstract subtitution obtained after the analysis of the clause being considered still projected onto Hv (i.e. just before going Sv and thus, to Prime).
Succ : Abstract success constraint (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).
Constr : Any abstract constraint.

Usage and interface

Documentation on exports

PREDICATEcall_to_entry/9

Usage:call_to_entry(Sv,Sg,Hv,Head,K,Fv,Proj,Entry,BothEntry)

It obtains the abstract constraint (Entry) which results from adding the abstraction of the constraint Sg = Head to Proj, later projecting the resulting constraint onto Hv. This is done as follows:

It will add to Call the information corresponding to the set of equations =(ArgSg,ArgHead) resulting from the unification Sg = Head by calling to def_herbrand_equation/6, obtaining NewProj.
If NewProj is $bottom (i.e. if Sg and Head are not unifiables) then Entry = bottom. Otherwise, it will project NewProj onto Hv and it will add the free variables in the body of the clause to the projected constraint, obtaining Entry.

The following properties should hold at call time:
(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)K 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.
The following properties should hold upon exit:
(nonvar/1)Entry is currently a term which is not a free variable.
(nonvar/1)BothEntry is currently a term which is not a free variable.

PREDICATEexit_to_prime/7

Usage:exit_to_prime(Sg,Hv,Head,Sv,Exit,BothEntry,Prime)

It computes the prime abstract constraint Prime, i.e. the result of going from the abstract constraint over the head variables (Exit), to the abstract constraint over the variables in the subgoal. If Exit is $bottom, Prime will be also $bottom. Otherwise Prime is the result of projecting Exit onto Hv obtaining BPrime, then adding the information in BPrime to the BothEntry (the abstract constraint obtained during the call to entry over all variables in Sg and Head and later projecting onto Sv.

The following properties should hold at call time:
(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.
(nonvar/1)BothEntry is currently a term which is not a free variable.
The following properties should hold upon exit:
(nonvar/1)Prime is currently a term which is not a free variable.

PREDICATEproject/5

Usage:project(Sg,Vars,HvFv_u,Constr,Projected)

It projects the ordered abstract subtitution given in the first argument on the ordered list of variables Vars in the second argument. All the variables in the second argument are assumed to appear also in the abstract constraint.

If the abstract constraint is $bottom the projected abstract constraint will be also $bottom
Otherwise: let a(Ground,Set) be the abstract constraint and a(PGround, PSet) be the result of the projection
- PGround will be the intersection of Ground and Vars
- PSet will be the result of for each (X,SS) in Set s.t.X in Vars remove from SS those sets which are not subsetseq of Vars obtaining NewSS. This will be done by calling project_vars/5. Note that if NewSS is [], (X,NewSS) will not be in PSet

The following properties should hold at call time:
(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)Constr is currently a term which is not a free variable.
The following properties should hold upon exit:
(nonvar/1)Projected is currently a term which is not a free variable.

PREDICATEproject_vars/4

Usage:project_vars(Vars1,Set,Vars2,PSet)

It will project the list of (X,SS) in Set onto Vars2 obtaining PSet. This will be done in the following way, for each (X,SS) in Set:

If X not in Vars1, (X,SS) will be eliminated.
Otherwise, we will compute NewSS = { S in SS| S in Vars2 }.
- If NewSS = [], X becomes top and it will be ignored.
- Otherwise, (X,NewSS) will be added to PSet.

The following properties should hold at call time:
(nonvar/1)Vars1 is currently a term which is not a free variable.
(nonvar/1)Set is currently a term which is not a free variable.
(nonvar/1)Vars2 is currently a term which is not a free variable.
The following properties should hold upon exit:
(nonvar/1)PSet is currently a term which is not a free variable.

PREDICATEcompute_lub/2

Usage:compute_lub(ListConstr,Lub)

It obtains the lub between all abstract constraints which are elements of the list given in the first argument. We assume that the abstract constraints are ordered and defined over the same set of variables. It will be computed recursively by obtaining the lub of 2 abstract constraints in each iteration in the following way:

The lub between two abstract constraints one of which is $bottom will result in the other abstract constraint
Otherwise, let Constr1 = a(G1,T1,S1) and Constr2 = a(G2,T2,S2)
- NewG will be the intersection between G1 and G2.
- NewT will be the union of T1 and T2.
- NewS will be computed by lub_set/4.

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

PREDICATEcompute_lub_el/3

No further documentation available for this predicate.

PREDICATEglb/3

Usage:glb(Constr1,Constr2,Constr)

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

PREDICATEabs_sort/2

Usage 1:abs_sort(Constr,SortedConstr)

It sorts the abstract constraint a(Ground,Set) received as first argument. In doing this it will:

sort the list of variables in Ground
for each (X,SS) in Set:
- sort each S in SS obtaining TempSet.
- sort TempSet.

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

Usage 2:abs_sort(Set1,Set2)

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

PREDICATEextend/5

Usage:extend(Sg,Prime,Sv,Call,Succ)

It extends the information given by the new abstract constraint on the subgoal Prime (first argument) to the original information about all the clause variables which is contained in Call, obtaining Succ.

If Prime is $bottom, Succ = $bottom.
Otherwise, the result will be the same as conjunting the new abstract constraint Prime with Call.

The following properties should hold at call time:
(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.
The following properties should hold upon exit:
(nonvar/1)Succ is currently a term which is not a free variable.

PREDICATEcall_to_success_fact/9

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

It obtains the prime and success constraint for a fact. However, since the program are assumed to be normilised, a fact should have all their arguments as voids, and therefore Prime = Proj, and Succ = Call.

The following properties should hold at call time:
(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.
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.

PREDICATEspecial_builtin/5

Usage:special_builtin(SgKey,Sg,Subgoal,Type,Condvars)

The predicate succeeds if the Sgkey indicates a builtin or a constraint Type indicates the kind of builtin and Condvars contains the info needed for their abstraction.

Type: '$fd_=/2' | Condvars: Sg | Meaning: =/2 builtin
Type: '$fd_comp/2' | Condvars: _ | Meaning: comparisons like <,>,etc
Type: '$fd_piii/2' | Condvars: Sg | Meaning: PrologIII list
Type: '$fd_fail' | Condvars: _ | Meaning: fail, abort,etc
Type: '$fd_unchanged' | Condvars: _ | Meaning: does not affect the info
....

The following properties should hold at call time:
(nonvar/1)SgKey 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)Subgoal is currently a term which is not a free variable.
(var/1)Condvars is a free variable.
The following properties should hold upon exit:
(nonvar/1)Type is currently a term which is not a free variable.

PREDICATEsuccess_builtin/6

Usage:success_builtin(Type,Sv_uns,Term,HvFv_u,Call,Succ)

By now, it is tricky since it assumes the following things:

booleans are still not allowed

The following properties should hold at call time:
(nonvar/1)Type is currently a term which is not a free variable.
(nonvar/1)Sv_uns 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)Call is currently a term which is not a free variable.
The following properties should hold upon exit:
(nonvar/1)Succ is currently a term which is not a free variable.

PREDICATEinput_user_interface/5

Usage:input_user_interface(InputUser,Qv,ASub,Sg,MaybeCallASub)

It translate the query mode given by the user into the internal structure.

The following properties should hold at call time:
(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.
(term/1)InputUser is any term.
(list/1)Qv is a list.
(term/1)ASub is any term.
(term/1)Sg is any term.
(term/1)MaybeCallASub is any term.
The following properties should hold upon exit:
(nonvar/1)ASub is currently a term which is not a free variable.

PREDICATEinput_interface/4

No further documentation available for this predicate.

PREDICATEasub_to_native/5

Usage:asub_to_native(ASub,Qv,OutFlag,ASub_user,Comps)

It translates an internal abstract constraint into something friendly for the user.

The following properties should hold at call time:
(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)ASub_user is currently a term which is not a free variable.
(nonvar/1)Comps is currently a term which is not a free variable.

PREDICATEunknown_call/4

Usage:unknown_call(Sg,Vars,Call,Succ)

Gives the top value for the variables Vars involved in a literal whose definition is not present, and adds this top value to Call (it is like conjunting the information in Call with the top for a subset of variables) In the definiteness analyser, nothing needs to be done.

The following properties should hold at call time:
(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.
The following properties should hold upon exit:
(nonvar/1)Succ is currently a term which is not a free variable.

PREDICATEunknown_entry/3

Usage:unknown_entry(Sg,Vars,Call)

Gives the top value for a given set of variables, resulting in the abstract constraint Call. In the definiteeness domain the top abstraction for a set of variables Vars is T = a({},{}).

The following properties should hold at call time:
(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.
The following properties should hold upon exit:
(nonvar/1)Call is currently a term which is not a free variable.

PREDICATEempty_entry/3

Usage:empty_entry(Sg,Vars,Entry)

The following properties should hold at call time:
(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.
The following properties should hold upon exit:
(nonvar/1)Entry is currently a term which is not a free variable.

PREDICATEless_or_equal/2

Usage:less_or_equal(ASub0,ASub1)

Succeeds if ASub0 = (G0,T0,R0) is less or equal than ASub1 = a(G1,T1,R1) i.e. if ASub0 is more concrete or equal than ASub1. This will be true if either ASub0 is bottom or:

G1 subseteq G0.
forall (X,SS1) in R1, X in G0, or exists (X,SS0) in R0, such that forall S1 in SS1, exists S0 in SS0 such that S0 in S1.

The following properties should hold at call time:
(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.