Types Abstract Domain

Author(s): Claudio Vaucheret, Francisco Bueno.

This module implements the abstract operations of a types domain within the PLAI abstract interpretation framework. An abstract substitution is list of Var:Type elements, where Var is a variable and Type is a pure type term [DZ92].


Documentation on exports

Usage:eterms_call_to_entry(Sg,Hv,Head,Fv,Proj,Entry,ExtraInfo)

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

  • If Sg and Head are identical up to renaming it is just renaming Proj and adding the Fv
  • Otherwise, it will
    • obtain the abstract substitution from unifying Sg and Head calling “unify_term_and_type_term”
    • add to this abstract substitution the variables in Fv as term type.

The meaning of the variables is

  • Sg is the subgoal being analysed.
  • Head is the Head of the clause being analysed.
  • Fv is a list of free variables in the body of the clause being considered.
  • Proj is the abstract substitution Call projected onto Sv.
  • Entry is the Abstract entry substitution (i.e. the abstract subtitution obtained after the abstract unification of Sg and Head projected onto Hv + Fv).
  • ExtraInfois a flag “yes” when no unification is required, i.e., Entry=Proj upto names of vars. and ignoring Fv. It is “no” if unification fails.

  • 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)Fv is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (var/1)Entry is a free variable.
    (var/1)ExtraInfo is a free variable.
    (callable/1)Sg is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Hv is a list.
    (callable/1)Head is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Fv is a list.
    (absu/1)Proj is an abstract substitution
    (absu/1)Entry is an abstract substitution
    (extrainfo/1)ExtraInfo is a par (absu,binds)

Usage:eterms_exit_to_prime(Sg,Hv,Head,Sv,Exit,ExtraInfo,Prime)

It computes the prime abstract substitution Prime, i.e. the result of going from the abstract substitution over the head variables Exit, to the abstract substitution over the variables in the subgoal. It will:

  • If Exit is '$bottom', Prime will be also '$bottom'.
  • If ExtraInfo = yes (Head and Sg identical up to renaming) it is just renaming Exit %
  • Otherwise: it will
    • projects Exit onto Hv obtaining BPrime.
    • obtain the abstract substitution from unifying Sg and Head calling “unify_term_and_type_term”

  • 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.
    (var/1)ExtraInfo is a free variable.
    (var/1)Prime is a free variable.
    (list/1)Sg is a list.
    (list/1)Hv is a list.
    (callable/1)Head is a term which represents a goal, i.e., an atom or a structure.
    (callable/1)Sv is a term which represents a goal, i.e., an atom or a structure.
    (absu/1)Exit is an abstract substitution
    (extrainfo/1)ExtraInfo is a par (absu,binds)
    (absu/1)Prime is an abstract substitution

Usage:eterms_project(Vars,Asub,Proj)

Proj is the result of eliminating from Asub all X:Value such that X is not in Vars

  • The following properties should hold at call time:
    (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.
    (var/1)Proj is a free variable.
    (list/1)Vars is a list.
    (absu/1)Asub is an abstract substitution
    (absu/1)Proj is an abstract substitution

Usage:eterms_compute_lub(ListASub,Lub)

It computes the least upper bound of a set of abstract substitutions. For each two abstract substitutions ASub1 and ASub2 in ListASub, obtaining the lub is foreach X:Type1 in ASub1 and X:Type2 in ASub2, X:TypeUnion is in Lub, and TypeUnion is the deterministic union of Type1 an Type2.

  • The following properties should hold at call time:
    (nonvar/1)ListASub is currently a term which is not a free variable.
    (var/1)Lub is a free variable.
    (list/2)ListASub is a list of absus.
    (absu/1)Lub is an abstract substitution

No further documentation available for this predicate.

PREDICATEeterms_sort/2

Usage:eterms_sort(Asub,Asub_s)

It sorts the set of X:Type in Asub ontaining Asub_s

  • The following properties should hold at call time:
    (nonvar/1)Asub is currently a term which is not a free variable.
    (var/1)Asub_s is a free variable.
    (absu/1)Asub is an abstract substitution
    (absu/1)Asub_s is an abstract substitution

Usage:eterms_extend(Prime,Sv,Call,Succ)

If Prime = '$bottom', Succ = '$bottom' otherwise, Succ is computed updating the values of Call with those in Prime

  • The following properties should hold at call time:
    (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.
    (var/1)Succ is a free variable.
    (absu/1)Prime is an abstract substitution
    (list/1)Sv is a list.
    (absu/1)Call is an abstract substitution
    (absu/1)Succ is an abstract substitution

Usage:eterms_less_or_equal(ASub0,ASub1)

Succeeds if ASub1 is more general or equal to ASub0. it's assumed the two abstract substitutions are defined on the same variables

  • 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.
    (absu/1)ASub0 is an abstract substitution
    (absu/1)ASub1 is an abstract substitution

PREDICATEeterms_glb/3

Usage:eterms_glb(ASub0,ASub1,Glb)

Glb is the great lower bound of ASub0 and ASub1

  • 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.
    (var/1)Glb is a free variable.
    (absu/1)ASub0 is an abstract substitution
    (absu/1)ASub1 is an abstract substitution
    (absu/1)Glb is an abstract substitution

Usage:eterms_unknown_call(Call,Vars,Succ)

Gives the “top” value for the variables involved in a literal whose definition is not present, and adds this top value to Call

  • The following properties should hold at call time:
    (nonvar/1)Call is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
    (var/1)Succ is a free variable.
    (absu/1)Call is an abstract substitution
    (list/1)Vars is a list.
    (absu/1)Succ is an abstract substitution

Usage:eterms_unknown_entry(Qv,Call)

Gives the “top” value for the variables involved in a literal whose definition is not present, and adds this top value to Call. In this domain the top value is X:term forall X in the set of variables

  • The following properties should hold at call time:
    (nonvar/1)Qv is currently a term which is not a free variable.
    (var/1)Call is a free variable.
    (list/1)Qv is a list.
    (absu/1)Call is an abstract substitution

Usage:eterms_empty_entry(Vars,Entry)

Gives the "empty" value in this domain for a given set of variables Vars, resulting in the abstract substitution Entry. I.e., obtains the abstraction of a substitution in which all variables Vars are unbound: free and unaliased. In this domain the empty value is giving the variable type to each variable

  • The following properties should hold at call time:
    (nonvar/1)Vars is currently a term which is not a free variable.
    (var/1)Entry is a free variable.
    (list/1)Vars is a list.
    (absu/1)Entry is an abstract substitution

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

Specialized version of call_to_entry + exit_to_prime + extend for facts

  • 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)Call is currently a term which is not a free variable.
    (nonvar/1)Proj is currently a term which is not a free variable.
    (var/1)Prime is a free variable.
    (var/1)Succ is a free variable.
    (callable/1)Sg is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Hv is a list.
    (callable/1)Head is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Sv is a list.
    (absu/1)Call is an abstract substitution
    (absu/1)Proj is an abstract substitution
    (absu/1)Prime is an abstract substitution
    (absu/1)Succ is an abstract substitution

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

Usage:eterms_widen(Prime0,Prime1,NewPrime)

Induction step on the abstract substitution of a fixpoint. Prime0 corresponds to non-recursive and Prime1 to recursive clauses. NewPrime is the result of apply one widening operation to the least upper bound of the formers.

  • The following properties should hold at call time:
    (nonvar/1)Prime0 is currently a term which is not a free variable.
    (nonvar/1)Prime1 is currently a term which is not a free variable.
    (var/1)NewPrime is a free variable.
    (absu/1)Prime0 is an abstract substitution
    (absu/1)Prime1 is an abstract substitution
    (absu/1)NewPrime is an abstract substitution

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

PREDICATEget_type/3
No further documentation available for this predicate.

PREDICATEresetunion/0
No further documentation available for this predicate.

PREDICATEtype_union/3

Usage:type_union(Type1,Type2,Type3)

Type3 is the union of Type1 and Type2 and is defined by a deterministic type rule. This is done as follows:

  • if Type1 is included in Type2 the union is Type2.
  • if Type2 is included in Type1 the union is Type1.
  • Otherwise, if (Type1,Type2,Type3) in Seen (i.e. the union of Type1 and Type2 was previously evaluated) the union is Type3. Otherwise, it will create a new type simbol Type3, merge the definitions of Type1 and Type2 in a deterministic way, unfold the new definition, and insert the new rule.

  • The following properties should hold at call time:
    (nonvar/1)Type1 is currently a term which is not a free variable.
    (nonvar/1)Type2 is currently a term which is not a free variable.
    (var/1)Type3 is a free variable.
    (pure_type_term/1)Type1 is a term defining a regular type
    (pure_type_term/1)Type2 is a term defining a regular type
    (pure_type_term/1)Type3 is a term defining a regular type

Usage:make_deterministic(Def1,Def2)

Def1 and Def2 are two sorted lists of type terms with compound type terms of different functor/arity. Def1 is the merge of both definitions, if two compound type terms have the same functor/arity, both are replaced by a new compound type terms whose arguments are the deterministic union of the formers.

  • The following properties should hold at call time:
    (nonvar/1)Def1 is currently a term which is not a free variable.
    (nonvar/1)Def2 is currently a term which is not a free variable.
    (list/2)Def1 is a list of pure_type_terms.
    (list/2)Def2 is a list of pure_type_terms.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

PREDICATEgetargtypes/6
No further documentation available for this predicate.

No further documentation available for this predicate.