☰

Applying assertions during fixpoint

Author(s): Isabel Garcia-Contreras.

This module contains the logic of what assertions need to be applied depending on the analysis step.

This module reads the values of the following flags:

  • fixp_stick_to_success: whether to use the value of the success assertions instead of what was inferred for the fixpoint (not working for eterms).

    For a module: 

    :- module(_,[p/1],[assertions]).

:- pred p(X) => atm(X).
p(X) :- X = a.

    If fixp_stick_to_success is set to on, the analysis result will be: 

    :- module(_,[p/1],[assertions]).

:- true pred p(X) => atm(X).
p(X) :- X = a.

    Because the value of the assertion is used as it is. If it is set to off, it will use the assertion only when it allows to gain precision (useless in this case). 

    :- module(_,[p/1],[assertions,regtypes]).

:- true pred p(X) => rta(X).
p(X) :- X = a.

:- regtype rta/1.
rta(a).

  • fixp_stick_to_calls: not implemented yet, whether to use the value of the calls assertion instead of what was inferred by the fixpoint. This is harder than the success case since the heads of the analysis information may not be normalized.

    For example in the following module: 

    :- module(_,[main/0,p/1],[assertions]).

main :-
    p(a).

:- pred p(X) : atm(X).
p(X).

    Since the plai does not normalize heads it is imposible to generalize p(a) to p(X) : atm(X), the variables that the abstract substitution approximates must be in the head. However p(X) : rta(X) can be generalized only by changing the abstract substitution because the variable is already in the head.

    The fixpoint would have to be modified so that applying assertions can change the goals

  • use_check_as_trust: To activate the runtime semantics of the check assertions, i.e., use them as trust in the fixpoint.

Program point assertions are not processed here.

Documentation on exports

PREDICATEcall_asr/5
No further documentation available for this predicate. The predicate is of type data.

PREDICATEsuccess_asr/6
No further documentation available for this predicate. The predicate is of type data.

PREDICATEcleanup_applied_assertions/1
Cleans the cached assertions

PREDICATEapply_assrt_call_to_success/8

Usage:apply_assrt_call_to_success(AbsInt,Sg,Sv,Proj0,HvFv_u,Call,NewProj,NewCall)

NewProj and NewCall are the result of applying the assertions that correspond to the call_to_success analysis point.

Currently, the implementation has only one option which is applying true and trust call assertions, and true success assertions (that are applicable to Sg: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)Sv is currently a term which is not a free variable.
    (nonvar/1)Proj0 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.
    (var/1)NewProj is a free variable.
    (var/1)NewCall is a free variable.
    (atm/1)AbsInt is an atom.
    (list/1)Sv is a list.
    (list/1)HvFv_u is a list.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form apply_assrt_call_to_success(AbsInt,Sg,Sv,Proj0,HvFv_u,Call,NewProj,NewCall) do not fail.

PREDICATEapply_assrt_exit/7

Usage:apply_assrt_exit(AbsInt,Sg,Sv,Proj0,LPrime,NLPrime,Applied)

  • 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)Sv is currently a term which is not a free variable.
    (nonvar/1)Proj0 is currently a term which is not a free variable.
    (nonvar/1)LPrime is currently a term which is not a free variable.
    (var/1)NLPrime is a free variable.
    (atm/1)AbsInt is an atom.
    (list/1)Sv is a list.
    (list/1)LPrime is a list.
  • The following properties should hold upon exit:
    (list/1)NLPrime is a list.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form apply_assrt_exit(AbsInt,Sg,Sv,Proj0,LPrime,NLPrime,Applied) do not fail.
    (is_det/1)All calls of the form apply_assrt_exit(AbsInt,Sg,Sv,Proj0,LPrime,NLPrime,Applied) are deterministic.

PREDICATEapply_assrt_no_source/6

Usage:apply_assrt_no_source(SgKey,AbsInt,Sg,Sv,Proj,Prime)

Succeeds if there are applicable assertions to Sg:Proj understood by domain AbsInt and Prime is the answer pattern.

  • The following properties should hold at call time:
    (nonvar/1)SgKey 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)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.
    (var/1)Prime is a free variable.
    (atm/1)SgKey is an atom.
    (atm/1)AbsInt is an atom.
    (list/1)Sv is a list.
  • The following properties should hold upon exit:
    (nonvar/1)Prime is currently a term which is not a free variable.

PREDICATEget_call_assertions_asub/5

Usage:get_call_assertions_asub(Head,SgKey,Sts,AbsInt,AsrProj)

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

PREDICATEget_succ_assertion_asubs/7

Usage:get_succ_assertion_asubs(SgKey,Head,Hv,Sts,AbsInt,Proj,Prime)

This predicate succeeds if there are assertions that are applicable to Head:Proj (normalized). If no Sts is specified all trusted status are returned

  • The following properties should hold at call time:
    (nonvar/1)SgKey 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)Hv is currently a term which is not a free variable.
    (nonvar/1)Sts 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)Proj is currently a term which is not a free variable.
    (var/1)Prime is a free variable.
    (atm/1)SgKey is an atom.
    (list/1)Hv is a list.
    (list/1)Sts is a list.
    (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.

PREDICATEadd_success_asr/6

Usage:add_success_asr(SgKey,Head,Sts,AbsInt,AsrProj,AsrPrime)

Joins an abstract success pattern from an assertion with a previous value for the call pattern Head:AsrProj.

  • The following properties should hold at call time:
    (nonvar/1)SgKey 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)Sts 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)AsrProj is currently a term which is not a free variable.
    (nonvar/1)AsrPrime is currently a term which is not a free variable.
    (atm/1)SgKey is an atom.
    (list/1)Sts 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_success_asr(SgKey,Head,Sts,AbsInt,AsrProj,AsrPrime) do not fail.

PREDICATEabs_normalize/8

Usage:abs_normalize(AbsInt,Sg,Sv,ASub0,Head,Hv,ASub,ExtraInfo)

  • 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)Sv is currently a term which is not a free variable.
    (nonvar/1)ASub0 is currently a term which is not a free variable.
    (var/1)ASub is a free variable.
    (var/1)ExtraInfo is a free variable.
    (atm/1)AbsInt is an atom.
    (list/1)Sv is a list.
  • 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 abs_normalize(AbsInt,Sg,Sv,ASub0,Head,Hv,ASub,ExtraInfo) do not fail.

PREDICATEget_applicable_status/3
No further documentation available for this predicate.

Generated with LPdoc using Ciao