1/*  Part of Run-Time Checker for Assertions
    2
    3    Author:        Edison Mera
    4    E-mail:        efmera@gmail.com
    5    WWW:           https://github.com/edisonm/refactor
    6    Copyright (C): 2017, Process Design Center, Breda, The Netherlands.
    7    All rights reserved.
    8
    9    Redistribution and use in source and binary forms, with or without
   10    modification, are permitted provided that the following conditions
   11    are met:
   12
   13    1. Redistributions of source code must retain the above copyright
   14       notice, this list of conditions and the following disclaimer.
   15
   16    2. Redistributions in binary form must reproduce the above copyright
   17       notice, this list of conditions and the following disclaimer in
   18       the documentation and/or other materials provided with the
   19       distribution.
   20
   21    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
   22    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
   23    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
   24    FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
   25    COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
   26    INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
   27    BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   28    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   29    CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   30    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
   31    ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   32    POSSIBILITY OF SUCH DAMAGE.
   33*/
   34
   35:- module(ctrtchecks,
   36          ['$with_asr'/2,
   37           '$with_gloc'/2,
   38           '$with_ploc'/2,
   39           assrt_op/4,
   40           check_call/3,
   41           check_goal/5,
   42           check_asrs_pre/5,
   43           collect_assertions/4,
   44           current_assertion/4,
   45           is_prop_check/5,
   46           is_valid_status_type/2,
   47           part_time/2,
   48           rtcheck_assr_status/1]).   49
   50:- use_module(library(apply)).   51:- use_module(library(intercept)).   52:- use_module(library(lists)).   53:- use_module(library(pairs)).   54:- use_module(library(assertions)).   55:- use_module(library(send_check)).   56:- use_module(library(extend_args)).   57:- use_module(library(clambda)).   58:- use_module(library(context_values)).   59:- use_module(library(rtcprops)).   60:- use_module(library(metaprops)).   61:- init_expansors.   62
   63:- meta_predicate checkif_modl(?, ?, 0, ?, 0).   64checkif_modl(M, M,    _,    _, Goal) :- !, call(Goal).
   65checkif_modl(_, _, GMod, Goal, Goal) :- call(GMod).
   66
   67is_prop_check(Step, Level, T, Part, Asr) :-
   68    part_time(Part, T),
   69    asr_aprop(Asr, type, Type,   _),
   70    asr_aprop(Asr, stat, Status, _),
   71    assrt_op(Part, Step, Level, Type),
   72    is_valid_status_type(Status, Type), !.
   73
   74part_time(call, _).
   75part_time(succ, _).
   76part_time(glob, rt).
 assrt_op(+Part, +Step, +Level, +Type)
   80assrt_op(call, step1, exports, calls).
   81assrt_op(call, step1, exports, pred).
   82assrt_op(call, step1, exports, prop).
   83assrt_op(call, step2, inner,   calls).
   84assrt_op(call, step2, inner,   pred).
   85assrt_op(call, step2, inner,   prop).
   86assrt_op(succ, step1, exports, success).
   87assrt_op(succ, step1, exports, pred).
   88assrt_op(succ, step1, exports, prop).
   89assrt_op(succ, step2, inner,   success).
   90assrt_op(succ, step2, inner,   pred).
   91assrt_op(succ, step2, inner,   prop).
   92assrt_op(glob, step1, exports, comp).
   93assrt_op(glob, step1, exports, pred).
   94assrt_op(glob, step1, exports, prop).
   95assrt_op(glob, step2, inner,   comp).
   96assrt_op(glob, step2, inner,   pred).
   97assrt_op(glob, step2, inner,   prop).
   98
   99is_valid_status_type(Status, Type) :-
  100        rtcheck_assr_type(Type),
  101        rtcheck_assr_status(Status).
  102
  103rtcheck_assr_status(Status) :-
  104            current_prolog_flag(rtchecks_status, StatusL),
  105            member(Status, StatusL).
  106
  107rtcheck_assr_type(calls).
  108rtcheck_assr_type(pred).
  109rtcheck_assr_type(prop).
  110rtcheck_assr_type(comp).
  111rtcheck_assr_type(success).
  112
  113/*
  114  Combination of status and rtcheck indicators, to control the compile
  115  and run-time checking:
  116
  117  ===========+============++===========+==========
  118  Status     | + Command  || ctchecked | rtchecked
  119  ===========+============++===========+==========
  120  true/trust | -          || no        | no
  121  true/trust | acheck     || no        | yes
  122  check      | no_acheck  || yes       | no
  123  check      | -          || yes       | yes
  124  ===========+============++===========+==========
  125  Note: This is weird to preserve ciao-compatibility
  126*/
  127
  128black_list_pred(_=_).
  129
  130assertion_is_valid(T, Status, Type, Asr) :-
  131    ( \+ prop_asr(glob, acheck(_), _, Asr),
  132      \+ prop_asr(glob, acheck(T, _), _, Asr)
  133    ->is_valid_status_type(Status, Type),
  134      \+ prop_asr(glob, no_acheck(_), _, Asr),
  135      \+ prop_asr(glob, no_acheck(T, _), _, Asr)
  136    ; true % Force run-time checking
  137    ).
  138
  139no_acheck_predicate(T, Pred, M) :-
  140    prop_asr(Pred, M, true, comp, _, _, Asr),
  141    \+ prop_asr(call, _, _, Asr),
  142    ( prop_asr(glob, no_acheck(_), _, Asr)
  143    ; prop_asr(glob, no_acheck(T, _), _, Asr)
  144    ).
  145
  146current_assertion(T, Pred, M, Asr) :-
  147    prop_asr(Pred, M, Status, Type, _, _, Asr),
  148    \+ ( T = rt,
  149         prop_asr(Pred, M, _, prop, _, _, _)
  150       ),
  151    \+ no_acheck_predicate(T, Pred, M),
  152    assertion_is_valid(T, Status, Type, Asr),
  153    ( current_prolog_flag(rtchecks_level, inner)
  154    ->true
  155    ; current_prolog_flag(rtchecks_level, exports),
  156      predicate_property(M:Pred, exported)
  157    ->true
  158    ),
  159    \+ black_list_pred(Pred).
  160
  161collect_assertions(T, Pred, M, AsrL) :-
  162    copy_term_nat(Pred, Head), % copy to avoid duplication of atributes
  163    findall(Head-Asr, current_assertion(T, Head, M, Asr), Pairs),
  164    maplist([Pred] +\ (Pred-T)^T^true, Pairs, AsrL).
  165
  166:- meta_predicate check_goal(+, 0, +, +, +).  167
  168check_goal(T, Call, M, CM, AsrL) :-
  169    current_prolog_flag(rtchecks_level, Level),
  170    checkif_modl(M, CM,
  171                 check_asrs(T, is_prop_check(step1, Level), AsrL, G2), G2,
  172                 check_asrs(T, is_prop_check(step2, Level), AsrL, Call)).
  173
  174:- meta_predicate
  175       check_asrs(+, 3, +, +),
  176       check_asrs_pre(+, 3, +, -, -).  177
  178check_asrs(T, IsPropCheck, AsrL, Goal) :-
  179    check_asrs_pre(T, IsPropCheck, AsrL, AsrGlobL, AsrSuccL),
  180    checkif_asrs_comp(AsrGlobL, T, Goal),
  181    checkif_asrs_props(T, success, AsrSuccL).
  182
  183check_asrs_pre(T, IsPropCheck, AsrL, AsrGlobL, AsrSuccL) :-
  184    prop_rtchecks(T, AsrL, IsPropCheck, call, AsrCallL),
  185    prop_rtchecks(T, AsrL, IsPropCheck, succ, AsrSuccL),
  186    subtract(AsrSuccL, AsrCallL, DAsrSuccL),
  187    prop_rtchecks(T, AsrL, IsPropCheck, glob, AsrGlobL),
  188    subtract(AsrGlobL, AsrCallL, DAsrGlobL),
  189    check_asrs_props_calls(T, AsrCallL),
  190    check_asrs_props(T, success, DAsrSuccL),
  191    check_asrs_props(T, comp,    DAsrGlobL).
  192
  193prop_rtchecks(T, AsrL1, IsPropCheck, Part, AsrPVL) :-
  194    include(call(IsPropCheck, T, Part), AsrL1, AsrL),
  195    pairs_keys_values(AsrPVL, AsrL, _PValuesL).
  196
  197:- meta_predicate checkif_asrs_comp(+, +, 0).  198checkif_asrs_comp([], _, Goal) :-
  199    call(Goal).
  200checkif_asrs_comp([Asr-PVL|AsrL], T, Goal1) :-
  201    checkif_asr_comp(T, PVL, Asr, Goal1, Goal),
  202    checkif_asrs_comp(AsrL, T, Goal).
  203
  204checkif_asr_comp(T, PropValues, Asr, M:Goal1, M:Goal) :-
  205    ( memberchk(PropValues, [[], [[]]]),
  206      copy_term_nat(Asr, NAsr),
  207      findall(g(NAsr, Glob, Loc),
  208              ( asr_aprop(NAsr, glob, Glob, Loc),
  209                valid_prop(T, Glob)
  210              ), GlobL),
  211      GlobL \= []
  212    ->comps_to_goal(GlobL, comp_pos_to_goal(Asr), Goal2, M:Goal1),
  213      Goal = '$with_asr'(Goal2, Asr)
  214    ; Goal = Goal1
  215    ).
  216
  217comp_pos_to_goal(Asr, g(Asr, M:Glob, Loc), '$with_gloc'(M:Glob, Loc), Goal) :-
  218    functor(Glob, _, N),
  219    arg(N, Glob, Goal).
  220
  221:- meta_predicate '$with_asr'(0, ?).  222'$with_asr'(Comp, Asr) :-
  223    with_value(Comp, '$with_asr', Asr).
  224
  225:- meta_predicate '$with_gloc'(0, ?).  226'$with_gloc'(Comp, GLoc) :-
  227    with_value(Comp, '$with_gloc', GLoc).
  228
  229:- meta_predicate '$with_ploc'(0, ?).  230'$with_ploc'(Comp, GLoc) :-
  231    with_value(Comp, '$with_ploc', GLoc).
 comps_to_goal(+Check:list, :Goal)//
This predicate allows to compound a list of global properties in to successive meta-calls, but in the third argument you can use your own selector:
?- comps_to_goal([not_fails(p(A)), is_det(p(A)), exception(p(A), exc)],G,p(A)).
G = not_fails(is_det(exception(p(A),exc)))
  243:- meta_predicate comps_to_goal(?, 3, ?, ?).  244comps_to_goal([],             _) --> [].
  245comps_to_goal([Check|Checks], Goal) -->
  246    comps_to_goal2(Checks, Check, Goal).
  247
  248:- meta_predicate comps_to_goal2(?, ?, 3, ?, ?).  249comps_to_goal2([], Check, Goal) -->
  250    call(Goal, Check).
  251comps_to_goal2([Check|Checks], Check1, Goal) -->
  252    call(Goal, Check1),
  253    comps_to_goal2(Checks, Check, Goal).
  254
  255:- meta_predicate check_call(+, +, 0).  256check_call(T, AsrL, Goal) :-
  257    predicate_property(Goal, implementation_module(M)),
  258    check_call(T, Goal, M, AsrL).
  259
  260% TBD: use a partial evaluator instead of true
  261check_call(ct, CM:_,    M, AsrL) :- check_goal(ct, CM:true, M, CM, AsrL).
  262check_call(rt, CM:Call, M, AsrL) :- check_goal(rt, CM:Call, M, CM, AsrL).
  263
  264check_asrs_props_calls(T, AsrPVL) :-
  265    check_asrs_props_all(T, calls, AsrPVL).
  266
  267check_asrs_props_all(T, PType, AsrPVL) :-
  268    check_asrs_props(T, PType, AsrPVL),
  269    ( \+ memberchk(_-[], AsrPVL)
  270    ->maplist(send_check_asr(PType), AsrPVL)
  271    ; true
  272    ).
  273
  274check_asrs_props(T, PType, AsrPVL) :-
  275    maplist(check_asr_props(T, PType), AsrPVL).
  276
  277checkif_asrs_props(T, PType, AsrPVL) :-
  278    maplist(checkif_asr_props(T, PType), AsrPVL).
  279
  280checkif_asr_props(T, PType, Asr-CondValues) :-
  281    checkif_asr_props(T, CondValues, Asr, PType).
  282
  283check_asr_props(T, PType, Asr-PropValues) :-
  284    check_asr_props(T, Asr, inco, PType, PropValues).
  285
  286send_check_asr(PType, Asr-PropValues) :-
  287    ( PropValues = [[]] % Skip property
  288    ->true
  289    ; once(asr_aprop(Asr, head, Pred, ALoc)),
  290      send_check(PropValues, PType, Pred, ALoc)
  291    ).
  292
  293checkif_asr_props(T, CondValues, Asr, PType) :-
  294    ( memberchk(CondValues, [[], [[]]])
  295    ->check_asr_props(T, Asr, cond, PType, PropValues),
  296      send_check_asr(PType, Asr-PropValues)
  297    ; true
  298    ).
  299
  300check_asr_props(T, Asr, Cond, PType, PropValues) :-
  301    copy_term_nat(Asr, NAsr),
  302    once(asr_aprop(NAsr, head, _:Pred, _)),
  303    term_variables(Pred, VU),
  304    sort(VU, VS),
  305    findall(NAsr-PropValue,
  306            current_asr_prop_value(VS, T, Cond, PType, NAsr, PropValue),
  307            AsrPropValues),
  308    maplist([Asr] +\ (Asr-PV)^PV^true, AsrPropValues, PropValues).
  309
  310current_asr_prop_value(VS, T, Cond, PType, NAsr, PropValue) :-
  311    ( type_cond_part_check_mult(Cond, PType, Part, Check, Mult),
  312      asr_aprop(NAsr, Part, Prop, From)
  313    *->
  314      make_valid_prop(T, Prop, VProp), % if not valid, ignore property
  315      \+ catch(check_prop(Check, VS, VProp),
  316               Error,
  317               send_signal(at_location(From, Error))),
  318      last_prop_failure(L),
  319      (Mult = once -> ! ; true),
  320      CheckProp =.. [Check, Prop],
  321      PropValue = (From/CheckProp-L)
  322    ; PropValue = [] % Skip property
  323    ).
  324
  325check_prop(compat, VS, Prop) :- compat(Prop, VS).
  326check_prop(instan, VS, Prop) :- instan(Prop, VS).
  327
  328make_valid_prop(T, M:Prop, M:Valid) :-
  329    make_valid_prop(Prop, M, T, Valid).
  330
  331disj_prop(true, A, A).
  332disj_prop(A, true, A).
  333disj_prop(A, B, (A;B)).
  334
  335conj_prop(true, _, true).
  336conj_prop(_, true, true).
  337conj_prop(A, B, (A,B)).
  338
  339make_valid_prop(A;B, M, T, V) :-
  340    !,
  341    make_valid_prop(A, M, T, VA),
  342    make_valid_prop(B, M, T, VB),
  343    once(disj_prop(VA, VB, V)).
  344make_valid_prop((A,B), M, T, V) :-
  345    !,
  346    make_valid_prop(A, M, T, VA),
  347    make_valid_prop(B, M, T, VB),
  348    once(conj_prop(VA, VB, V)).
  349make_valid_prop(list(Type, X), M, T, V) :-
  350    % TBD: generalize this example (i.e., consider meta predicates) --EMM
  351    !,
  352    ( extend_args(Type, [_], Type1),
  353      valid_prop(T, M, Type1)
  354    ->V = list(Type, X)
  355    ; V = list(X)
  356    ).
  357make_valid_prop(A, M, T, V) :-
  358    ( valid_prop(T, M, A)
  359    ->V = A
  360    ; V = true
  361    ).
  362
  363:- meta_predicate valid_prop(+, 0 ).  364
  365valid_prop(T, M:Prop) :- valid_prop(T, M, Prop).
  366
  367valid_prop(T, M, Prop) :-
  368    functor(Prop, F, A),
  369    tabled_valid_prop(T, M, F, A).
  370
  371:- table tabled_valid_prop/4.  372
  373tabled_valid_prop(T, M, F, A) :-
  374    functor(H, F, A),
  375    \+ (( prop_asr(head, M:H, _, Asr),
  376          ( prop_asr(glob, no_acheck(   _), _, Asr)
  377          ; prop_asr(glob, no_acheck(T, _), _, Asr)
  378          )
  379        )).
  380
  381type_cond_part_check_mult(inco, PType, Part, Check, Mult) :-
  382    type_inco_part_check_mult(PType, Part, Check, Mult).
  383type_cond_part_check_mult(cond, PType, Part, Check, Mult) :-
  384    type_cond_part_check_mult(PType, Part, Check, Mult).
  385
  386type_inco_part_check_mult(calls,   call, instan, call).
  387type_inco_part_check_mult(calls,   comp, compat, call).
  388type_inco_part_check_mult(success, call, instan, once).
  389type_inco_part_check_mult(success, comp, compat, once).
  390type_inco_part_check_mult(comp,    call, instan, once).
  391
  392type_cond_part_check_mult(success, comp, compat, call).
  393type_cond_part_check_mult(success, succ, instan, call)