fixpo_dd (library)

Usage:query(AbsInt,QKey,Query,Qv,RFlag,N,Call,Succ)

The success pattern of Query with Call is Succ in the analysis domain AbsInt. The predicate called is identified by QKey, and RFlag says if it is recursive or not. The goal Query has variables Qv, and the call pattern is uniquely identified by N.

• The following properties should hold at call time:
  (nonvar/1)AbsInt is currently a term which is not a free variable.
  (nonvar/1)QKey is currently a term which is not a free variable.
  (nonvar/1)Query 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)RFlag 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.
  (atm/1)AbsInt is an atom.
  (atm/1)QKey is an atom.
  (term/1)Query is any term.
  (list/1)Qv is a list.
  (atm/1)RFlag is an atom.
  (term/1)N is any term.
  (term/1)Call is any term.
  (term/1)Succ is any term.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form query(AbsInt,QKey,Query,Qv,RFlag,N,Call,Succ) do not fail.

Usage:

Cleans up the database of analysis of temporary information.

Usage:cleanup_fixpoint(AbsInt)

Cleanups the database of analysis, of both temporary as well as permanent information regarding abstract domain AbsInt.

• The following properties should hold globally:
  (not_fails/1)All the calls of the form cleanup_fixpoint(AbsInt) do not fail.

Usage:entry_to_exit(Body,Key,Call,Exit,Vars_u,AbsInt,NewN)

Traverses the body of a clause (first argument) obtaining the Exit for a given Entry (represented by Call, since it is both the Entry of the clause and the Call for the first subgoal).

• The following properties should hold at call time:
  (nonvar/1)Body is currently a term which is not a free variable.
  (nonvar/1)Key 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)Exit is a free variable.
  (nonvar/1)Vars_u 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)NewN is currently a term which is not a free variable.
  (atm/1)Key is an atom.
  (list/1)Vars_u is a list.
  (atm/1)AbsInt is an atom.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form entry_to_exit(Body,Key,Call,Exit,Vars_u,AbsInt,NewN) do not fail.

Usage:proj_to_prime_nr(SgKey,Sg,Sv,Call,Proj,AbsInt,Clid,ListPrime,Id)

This predicate obtains the list of Prime corresponding to each non recursive clause of Sg for a given Call. It first reads those non recursive clauses by means of a bagof and then proccess each one with a loop. If there is no non recursive clause, the answer will be ['$bottom'].

• 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)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.
  (nonvar/1)AbsInt is currently a term which is not a free variable.
  (nonvar/1)Clid is currently a term which is not a free variable.
  (var/1)ListPrime is a free variable.
  (nonvar/1)Id is currently a term which is not a free variable.
  (atm/1)SgKey is an atom.
  (list/2)Sv is a list of vars.
  (atm/1)AbsInt is an atom.
  (plai_db_id/1)plai_db_id(Id)
• The following properties should hold upon exit:
  (list/1)ListPrime is a list.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form proj_to_prime_nr(SgKey,Sg,Sv,Call,Proj,AbsInt,Clid,ListPrime,Id) do not fail.
  (is_det/1)All calls of the form proj_to_prime_nr(SgKey,Sg,Sv,Call,Proj,AbsInt,Clid,ListPrime,Id) are deterministic.

Usage:

• The following properties should hold globally:
  (not_fails/1)All the calls of the form proj_to_prime_r(Arg1,Arg2,Arg3,Arg4,Arg5,Arg6,Arg7,Arg8) do not fail.

Usage:proj_to_prime(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,Prime,Id)

• The following properties should hold at call time:
  (nonvar/1)Clauses is currently a term which is not a free variable.
  (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)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.
  (nonvar/1)AbsInt is currently a term which is not a free variable.
  (nonvar/1)Id is currently a term which is not a free variable.
  (list/1)Clauses is a list.
  (atm/1)SgKey is an atom.
  (list/2)Sv is a list of vars.
  (atm/1)AbsInt is an atom.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form proj_to_prime(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,Prime,Id) do not fail.
  (is_det/1)All calls of the form proj_to_prime(Clauses,SgKey,Sg,Sv,Call,Proj,AbsInt,Prime,Id) are deterministic.

Usage:compute(Clauses,SgKey,Sg,Sv,Proj,AbsInt,TempPrime,Prime,Id)

It analyzes each recursive clause clause.

• The following properties should hold at call time:
  (nonvar/1)Clauses is currently a term which is not a free variable.
  (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)Sv 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)AbsInt is currently a term which is not a free variable.
  (nonvar/1)TempPrime is currently a term which is not a free variable.
  (var/1)Prime is a free variable.
  (nonvar/1)Id is currently a term which is not a free variable.
  (atm/1)SgKey is an atom.
  (list/2)Sv is a list of vars.
  (atm/1)AbsInt is an atom.
  (plai_db_id/1)plai_db_id(Id)
• 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 compute(Clauses,SgKey,Sg,Sv,Proj,AbsInt,TempPrime,Prime,Id) do not fail.
  (is_det/1)All calls of the form compute(Clauses,SgKey,Sg,Sv,Proj,AbsInt,TempPrime,Prime,Id) are deterministic.

Usage:td_mark_parents_change_list(Parents,AbsInt)

This complete has changed. So we add the change in the $change_list of all parents.

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

Usage:add_change(Id,Lit_Key,Literal,Parents,AbsInt)

Id: Id of the complete of the predicate that changed Lit_Key: Key of the Literal of the complete that needs recomputing. Literal: Literal with the term F/A/C/L. Parents: Program points in which the literal is called (0 means an entry) AbsInt: Abstract Domain.

• The following properties should hold at call time:
  (nonvar/1)Id is currently a term which is not a free variable.
  (nonvar/1)Literal is currently a term which is not a free variable.
  (nonvar/1)Parents is currently a term which is not a free variable.
  (nonvar/1)AbsInt is currently a term which is not a free variable.
  (plai_db_id/1)plai_db_id(Id)
  (atm/1)Lit_Key is an atom.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form add_change(Id,Lit_Key,Literal,Parents,AbsInt) do not fail.

Usage:mark_parents_change_list_scc(Parents,SCC,AbsInt)

This complete has changed. So we add the change in the $change_list of all parents. If the parent is in the same SCC then we recursively mark its parents as well.

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

Usage:add_change_scc(Id,Lit_Key,Literal,Parents,SCC,AbsInt)

Lit_Key may be free when a clause is marked to analyze from the begining (see second clause of compute_change).

• The following properties should hold at call time:
  (nonvar/1)Id is currently a term which is not a free variable.
  (nonvar/1)Literal is currently a term which is not a free variable.
  (nonvar/1)Parents is currently a term which is not a free variable.
  (nonvar/1)SCC is currently a term which is not a free variable.
  (nonvar/1)AbsInt is currently a term which is not a free variable.
  (int/1)Id is an integer.
  (atm/1)Lit_Key is an atom.
  (term/1)Literal is any term.
  (list/1)Parents is a list.
  (list/1)SCC is a list.
  (atm/1)AbsInt is an atom.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form add_change_scc(Id,Lit_Key,Literal,Parents,SCC,AbsInt) do not fail.
  (is_det/1)All calls of the form add_change_scc(Id,Lit_Key,Literal,Parents,SCC,AbsInt) are deterministic.

Usage:fixpoint_compute_change(Changes,SgKey,Sg,Sv,Proj,AbsInt,TempPrime,Prime,Id)

It obtains the Prime for the recursive predicate Sg with Call (which has been assigned to node Id), and the list of nodes it depends on In doing this it performs an iteration over the recursive clauses of Sg by calling to compute_change/13 and then checks if the fixpoint has been reached by calling to fixpoint/13. Fixpoint is reached if either NewList is empty (it means that Id does not depend on any node) or if Flag is a variable (it means that the information has not been modified within the iteration) LEntryInf is the list of (Entry,ExtraInfo) couples for each Clause. It will be computed in the first iteration and used in subsequent ones

• The following properties should hold at call time:
  (nonvar/1)Changes is currently a term which is not a free variable.
  (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)Sv 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)AbsInt is currently a term which is not a free variable.
  (nonvar/1)TempPrime is currently a term which is not a free variable.
  (var/1)Prime is a free variable.
  (nonvar/1)Id is currently a term which is not a free variable.
  (atm/1)SgKey is an atom.
  (list/2)Sv is a list of vars.
  (atm/1)AbsInt is an atom.
  (plai_db_id/1)plai_db_id(Id)
• 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 fixpoint_compute_change(Changes,SgKey,Sg,Sv,Proj,AbsInt,TempPrime,Prime,Id) do not fail.
  (is_det/1)All calls of the form fixpoint_compute_change(Changes,SgKey,Sg,Sv,Proj,AbsInt,TempPrime,Prime,Id) are deterministic.