1/*  Part of Extended Tools for SWI-Prolog
    2
    3    Author:        Edison Mera Menendez
    4    E-mail:        efmera@gmail.com
    5    WWW:           https://github.com/edisonm/xtools
    6    Copyright (C): 2015, 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(check_assertions, []).   36
   37:- use_module(library(apply)).   38:- use_module(library(lists)).   39:- use_module(library(option)).   40:- use_module(library(yall)).   41:- use_module(library(pairs)).   42:- use_module(library(checkers/checker)).   43:- use_module(library(assertions)).   44:- use_module(library(check), []).   45:- use_module(library(codewalk)).   46:- use_module(library(compact_pi_list)).   47:- use_module(library(intercept)).   48:- use_module(library(normalize_pi)).   49:- use_module(library(resolve_calln)).   50:- use_module(library(location_utils)).   51:- use_module(library(from_utils)).   52:- use_module(library(qualify_meta_goal)).   53:- use_module(library(assertions)).   54:- use_module(library(option_utils)).   55:- use_module(library(checkable_predicate)).   56:- use_module(library(ctrtchecks)).   57:- use_module(library(rtchecks_rt)).   58:- use_module(library(rtchecks_utils), []).   59
   60:- dynamic
   61       violations_db/3.   62
   63:- multifile
   64       ignore_predicate/2,
   65       prolog:message//1.   66
   67% :- table
   68%        generate_ctchecks/4,
   69%        do_check_property_ctcheck/2.
   70
   71checker:check(assertions, Result, Options) :-
   72    cleanup_db,
   73    check_assertions(Options, Result).
   74
   75cleanup_db :-
   76    retractall(violations_db(_, _, _)).
   77
   78check_assertions(Options1, Pairs) :-
   79    foldl(select_option_default,
   80          [method(Method1)-clause],
   81          Options1, Options2),
   82    ( \+ memberchk(Method1, [source, clause]) % only these methods are supported
   83    ->Method = clause,
   84      print_message(
   85          warning,
   86          format("Method `~w' not supported, using `~w' instead",
   87                 [Method1, Method]))
   88    ; Method = Method1
   89    ),
   90    merge_options(Options2,
   91                  [method(Method),
   92                   trace_variables([non_fresh]),
   93                   on_trace(collect_violations)
   94                  ], Options),
   95    option_module_files(Options, MFileD),
   96    walk_code([module_files(MFileD)|Options]),
   97    findall(error-Issue,
   98            ( retract(violations_db(CPI, CTChecks, From)),
   99              from_location(From, Loc),
  100              Issue = body(Loc-CPI)-CTChecks
  101            ; current_head_ctcheck(MFileD, Issue)
  102            ), Pairs, Props),
  103    prop_ctcheck(MFileD, Props).
  104
  105current_head_ctcheck(MFileD, head(Loc-PI)-AssrErrorL) :-
  106    PI=M:F/A,
  107    get_dict(M, MFileD, FileD),
  108    current_predicate(M:F/A),
  109    functor(H, F, A),
  110    MH = M:H,
  111    \+ predicate_property(MH, imported_from(_)),
  112    \+ is_built_in(MH),
  113    \+ predicate_property(MH, foreign),
  114    generate_ctchecks(H, M, [], CTCheck),
  115    CTCheck \= _:true,
  116    clause(MH, _, Clause),
  117    clause_property(Clause, file(File)),
  118    get_dict(File, FileD, _),
  119    do_check_property_ctcheck(CTCheck, AssrErrorL),
  120    % Although we have duplicated logic, we don't call check_property_ctcheck/3
  121    % here because is too slow:
  122    % check_property_ctcheck(H, M, CTChecks),
  123    AssrErrorL \= [],
  124    from_location(clause(Clause), Loc).
  125
  126prop_ctcheck(MFileD, Trans) :-
  127    findall(Pair, current_prop_ctcheck(MFileD, Pair), Pairs),
  128    sort(Pairs, Sorted),
  129    group_pairs_by_key(Sorted, Groups),
  130    maplist([K-L, (error-(prop(G)-K))]
  131            >>group_pairs_by_key(L, G), Groups, Trans).
  132
  133current_prop_ctcheck(MFileD, (Checker-PLoc/Issues)-(Loc-PI)) :-
  134    prop_asr(head, M:Head, From, Asr),
  135    get_dict(M, MFileD, FileD),
  136    from_to_file(From, File),
  137    get_dict(File, FileD, _),
  138    functor(Head, HF,HA),
  139    PI=M:HF/HA,
  140    ( member(Part, [comp, call, succ, glob]),
  141      curr_prop_asr(Part, PM:Prop, PFrom, Asr),
  142      resolve_head(Prop, PM, N:H)
  143    ),
  144    checker_t(Checker),
  145    term_variables(Head, Vars),
  146    '$expand':mark_vars_non_fresh(Vars),
  147    check_property(Checker, H, N, M:Head, Issues),
  148    numbervars(Issues, 0, _),
  149    from_location(PFrom, PLoc),
  150    from_location(From, Loc).
  151
  152resolve_head(V, M, M:V) :-
  153    var(V),
  154    % Note: this should not happen
  155    !,
  156    fail.
  157resolve_head(M:H1, _, H) :- !,
  158    resolve_head(H1, M, H).
  159resolve_head((A,B), M, H) :- !,
  160    ( resolve_head(A, M, H)
  161    ; resolve_head(B, M, H)
  162    ).
  163resolve_head((A;B), M, H) :-
  164    !,
  166    
  167    ( resolve_head(A, M, H)
  168    ; resolve_head(B, M, H)
  169    )
  169.
  170resolve_head(H, M, M:H).
  171
  172prolog:message(acheck(assertions)) -->
  173    ['Check asssertions',nl,
  174     '-----------------',nl,
  175     'The predicates contain assertions that are inconsistent', nl,
  176     'with the implementation.', nl, nl].
  177prolog:message(acheck(assertions, Type-IssueL)) -->
  178    type_message(Type),
  179    {type_issue_t(Type, IssueT)},
  180    foldl(prop_issue(IssueT), IssueL).
  181
  182type_issue_t(body(_), ctchecks).
  183type_issue_t(head(_), ctchecks).
  184type_issue_t(prop(_), property).
  185
  186prop_issue(ctchecks, CTChecks) -->
  187    prolog:message(acheck(checks, CTChecks)).
  188prop_issue(property, Checker-IssueL) -->
  189    foldl(property_issue(Checker), IssueL).
  190
  191property_issue(ctcheck, Loc/(PI-CTChecks)) -->
  192    ["    "], Loc, ["In call to ~w:"-[PI], nl],
  193    prop_issue(ctchecks, CTChecks).
  194property_issue(defined, Loc/Prop) -->
  195    ["    "], Loc, ["~w is undefined"-[Prop], nl].
  196property_issue(is_prop, Loc/Prop) -->
  197    ["    "], Loc, ["~w is not a property"-[Prop], nl].
  198
  199type_message(body(Loc-PI)) --> Loc, ['In the body of ~q:'-[PI], nl].
  200type_message(head(Loc-PI)) --> Loc, ['In the head of ~q:'-[PI], nl].
  201type_message(prop(LocPIL)) --> foldl(type_message_prop, LocPIL).
  202
  203type_message_prop(Loc-PIL) -->
  204    {compact_pi_list(PIL, PIC)},
  205    Loc, ['In assertions of ~q:'-[PIC], nl].
  206
  207ignore_predicate(assertion_head(_, _, _, _, _, _, _), assertions).
  208ignore_predicate(_, M) :- ignore_module(M).
  209
  210ignore_module(extend_args).
  211
  212% Issues in the assertion body will be reported when checking properties.
  213ignore_predicate(M:Call) :- ignore_predicate(Call, M).
  214
  215:- public collect_violations/3.
 collect_violations(+Module, :Goal, +Caller, +From)
Collect the assertion violations of a given Goal. Note that Module refer to the module of the source code, while Goal could have another context module, for instance, if module qualification was used in the body of a predicate.
  223:- meta_predicate collect_violations(0,0,+).  224collect_violations(M:Goal, Caller, From) :-
  225    ( \+ ignore_predicate(Caller),
  226      check_property_ctcheck(Goal, M, Caller, CTChecks),
  227      CTChecks \= []
  228    ->normalize_pi(Caller, CPI),
  229      update_fact_from(violations_db(CPI, CTChecks), From)
  230    ; true
  231    ).
  232
  233check_property_ctcheck(Goal, M, Caller, AssrErrorL) :-
  234    tabled_generate_ctchecks(Goal, M, Caller, CTCheck),
  235    CTCheck \= _:true,
  236    % Skip lack of assertions or assertions that will not
  237    % trigger violations
  238    do_check_property_ctcheck(CTCheck, AssrErrorL),
  239    ignore(( nb_current('$variable_names', VNL),
  240             maplist(set_variable_names, VNL)
  241           )).
  242
  243set_variable_names(Name=Variable) :- ignore(Variable = '$VAR'(Name)).
  244
  245do_check_property_ctcheck(CTCheck, AssrErrorL) :-
  246    SErrors = s([]),
  247    intercept(catch(CTCheck, Error, send_signal(Error)),
  248              AssrError, cpc_handler(AssrError), SErrors-CTCheck),
  249    SErrors = s(CAssrErrorL),
  250    maplist(collect_assr_error(CTCheck), CAssrErrorL, AssrErrorL).
  251
  252cpc_handler(AssrError, SErrors-CTCheck) :-
  253    SErrors = s(CAssrErrorL1),
  254    nb_setarg(1, SErrors, [CTCheck-AssrError|CAssrErrorL1]).
  255
  256collect_assr_error(CTCheck, CTCheck-AssrError, AssrError).
  257
  258checker_t(defined).
  259checker_t(is_prop).
  260checker_t(ctcheck).
  261
  262check_property(defined, H, M, _, M:F/A) :-
  263    % Also reported by check_undefined, but is here to avoid dependency with
  264    % other analysis.
  265    functor(H, F, A),
  266    \+ current_predicate(M:F/A).
  267check_property(is_prop, H, M, _, M:F/A) :-
  268    resolve_calln(M:H, M:G),
  269    functor(G, F, A),
  270    \+ verif_is_property(M, F, A).
  271check_property(ctcheck, H, M, Caller, (M:F/A)-CTChecks) :-
  272    % compile-time checks. Currently only compatibility checks.
  273    check_property_ctcheck(H, M, Caller, CTChecks),
  274    CTChecks \= [],
  275    resolve_calln(M:H, M:G),
  276    functor(G, F, A).
  277
  278var_info(A, P) -->
  279    ( { var_property(A, fresh(Fresh)) }
  280    ->[P=Fresh]
  281    ; []
  282    ).
 tabled_generate_ctchecks(+Head, ?Context, +Caller, -Goal) is det
  286tabled_generate_ctchecks(H, M, Caller, Goal) :-
  287    functor(H, F, A),
  288    functor(P, F, A),
  289    H =.. [F|Args],
  290    P =.. [F|PInf],
  291    foldl(var_info, Args, PInf, VInf, []),
  292    term_attvars(M:H, Vars),
  293    maplist(del_attrs, Vars),
  294    ( meta_call_goal(H, M, Caller, Meta)
  295    ->qualify_meta_goal(CM:P, Meta, G)
  296    ; G = P
  297    ),
  298    generate_ctchecks(G, M, VInf, Goal),
  299    CM = M,
  300    P = H.
 generate_ctchecks(+Goal, +Context, +VInf, -CTChecks) is det
Generate compile-time checks, currently only compatibility is checked, fails if no ctchecks can be applied to Pred. VInf contains information about fresh variables.
  308generate_ctchecks(Goal, M, VInf, CTChecks) :-
  309    collect_assertions(ct, Goal, M, AsrL),
  310    ( AsrL \= []
  311    ->maplist(wrap_asr_ctcheck(VInf), AsrL, PAsrL),
  312      CTChecks = ctrtchecks:check_call(ct, PAsrL, M:Goal)
  313    ; CTChecks = check_assertions:true
  314    ).
  315
  316wrap_asr_ctcheck(VInf, Asr, ctcheck(VInf, Asr)).
  317
  318assertions:asr_aprop(ctcheck(VInf, Asr), Key, Prop, From) :-
  319    asr_aprop_ctcheck(Key, VInf, Asr, Prop, From).
 asr_aprop_ctcheck(Asr, Section, Property, From)
Assertion abstraction: If we can not determine the mode at compile time, at least check for compatibility (instead of instantiation). This abstraction makes static check decidable, the tradeoff is that we lose precision but we gain computability of checks at compile-time.
  328asr_aprop_ctcheck(head, _, A, P, F) :- curr_prop_asr(head, P, F, A).
  329asr_aprop_ctcheck(stat, _, A, P, F) :- curr_prop_asr(stat, P, F, A).
  330asr_aprop_ctcheck(type, _, A, P, F) :- curr_prop_asr(type, P, F, A).
  331asr_aprop_ctcheck(dict, _, A, P, F) :- curr_prop_asr(dict, P, F, A).
  332asr_aprop_ctcheck(comm, _, A, P, F) :- curr_prop_asr(comm, P, F, A).
  333asr_aprop_ctcheck(comp, _, A, P, F) :- curr_prop_asr(comp, P, F, A).
  334asr_aprop_ctcheck(comp, _, A, P, F) :- curr_prop_asr(succ, P, F, A). % TBD: Key = succ
  335asr_aprop_ctcheck(Key,  L, Asr, Prop, From) :-
  336    asr_aprop_ctcheck_abstraction(Key, L, Asr, Prop, From).
  337
  338prop_abstraction(call, true).
  339% prop_abstraction(succ, false).
  340
  341asr_aprop_ctcheck_abstraction(Key, L, Asr, Prop, From) :-
  342    prop_abstraction(RKey, Fresh),
  343    curr_prop_asr(RKey, Prop, From, Asr),
  344    term_variables(Prop, Vars),
  345    ( member(Var=Fresh, L),
  346      member(Arg, Vars),
  347      Arg==Var
  348    ->Key = RKey
  349    ; Key = comp
  350    ).
  351
  352verif_is_property(system, true, 0) :- !. % ignore true (identity)
  353verif_is_property(M, F, A) :-
  354    functor(H, F, A),
  355    prop_asr(H, M, _, prop, _, _, _)