1/*  Part of Extended Libraries for Prolog
    2
    3    Author:        Edison Mera
    4    E-mail:        efmera@gmail.com
    5    WWW:           https://github.com/edisonm/xlibrary
    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(abstract_interpreter,
   36          [ abstract_interpreter/3,
   37            abstract_interpreter/4,
   38            abstract_interpreter_body/5,
   39            extra_clauses/4,              % +Goal, +Module, -Body, -From
   40            get_state/3,
   41            put_state/3,
   42            match_head/4,
   43            match_head_body/3,
   44            bottom/2,
   45            call_ai/1,
   46            eval_ai/1,
   47            skip_ai/1,
   48            intr_ai/1,
   49            match_noloops/4
   50          ]).   51
   52:- use_module(library(apply)).   53:- use_module(library(lists)).   54:- use_module(library(option)).   55:- use_module(library(prolog_stack)).   56:- use_module(library(qualify_meta_goal)).   57:- use_module(library(resolve_calln)).   58:- use_module(library(solution_sequences)).   59:- use_module(library(term_size)).   60:- use_module(library(terms_share)).   61:- use_module(library(neck)).   62:- use_module(library(interface), []).   63
   64:- init_expansors.

   76:- meta_predicate
   77    abstract_interpreter(0,4,?),
   78    abstract_interpreter(0,4,+,-),
   79    abstract_interpreter_body(+,+,4,?,?),
   80    extra_clauses(+,+,-,-),
   81    match_head(0,*,*,*),
   82    match_head_body(0,*,*),
   83    match_noloops(0,*,*,*),
   84    call_ai(0),
   85    eval_ai(0),
   86    skip_ai(0).   87
   88:- multifile
   89    replace_goal_hook/3,
   90    replace_body_hook/3,
   91    evaluable_goal_hook/2,
   92    evaluable_body_hook/3.   93
   94:- dynamic
   95    evaluable_goal_hook/2.   96
   97:- discontiguous
   98    abstract_interpreter_body/5.   99
  100evaluable_body_hook(absolute_file_name(A, _, O), _, (ground(A), ground(O))).
  101evaluable_body_hook(atom_concat(A, B, C), _,
  102                    ( nonvar(A), nonvar(B)
  103                    ; nonvar(A), nonvar(C)
  104                    ; nonvar(B), nonvar(C)
  105                    )).
  106evaluable_body_hook(atomic_list_concat(A, _), _, ground(A)).
  107evaluable_body_hook(atomic_list_concat(A, B, C), _,
  108                    ( ground(A), ground(B)
  109                    ; ground(B), ground(C)
  110                    )).
  111evaluable_body_hook(thread_self(_), _, true).
  112evaluable_body_hook(atom_length(A, _), _, ground(A)).
  113evaluable_body_hook(upcase_atom(A, _), _, ground(A)).
  114evaluable_body_hook(downcase_atom(A, _), _, ground(A)).
  115evaluable_body_hook(string_lower(A, _), _, ground(A)).
  116evaluable_body_hook(string_upper(A, _), _, ground(A)).
  117evaluable_body_hook(nb_current(A, _), _, ground(A)).
  118evaluable_body_hook(_ is A, _, ground(A)).
  119evaluable_body_hook(A > B, _, (ground(A),ground(B))).
  120evaluable_body_hook(A >= B, _, (ground(A),ground(B))).
  121evaluable_body_hook(A < B, _, (ground(A),ground(B))).
  122evaluable_body_hook(A =< B, _, (ground(A),ground(B))).
  123evaluable_body_hook(A =:= B, _, (ground(A),ground(B))).
  124evaluable_body_hook(atom_codes(A, B), _, (ground(A);ground(B))).
  125evaluable_body_hook(atom_chars(A, B), _, (ground(A);ground(B))).
  126evaluable_body_hook(member(_, L), _, is_list(L)).
  127evaluable_body_hook(current_predicate(P), _, ground(P)).
  128evaluable_body_hook(current_module(M), _, ground(M)).
  129evaluable_body_hook(select(_, L, _), _, is_list(L)).
  130evaluable_body_hook(option(O, L), _, (is_list(L), nonvar(O))).
  131evaluable_body_hook(nth0(I, L, _), _, (is_list(L);nonvar(I))).
  132evaluable_body_hook(nth1(I, L, _), _, (is_list(L);nonvar(I))).
  133evaluable_body_hook(arg(_, C, _), _, nonvar(C)).
  134evaluable_body_hook(var(V),     _, nonvar(V)).
  135evaluable_body_hook(nonvar(V),  _, nonvar(V)).
  136evaluable_body_hook(atomic(A),  _, nonvar(A)).
  137evaluable_body_hook(atom(A),    _, nonvar(A)).
  138evaluable_body_hook(is_list(A), _, (ground(A);is_list(A))).
  139evaluable_body_hook(number(A),  _, nonvar(A)).
  140evaluable_body_hook(float(A),   _, nonvar(A)).
  141evaluable_body_hook(integer(A), _, nonvar(A)).
  142evaluable_body_hook(strip_module(A, _, _), _, nonvar(A)).
  143evaluable_body_hook(clause(A, _),    _, (strip_module(A, M, B), atom(M), callable(B))).
  144evaluable_body_hook(clause(A, _, _), _, (strip_module(A, M, B), atom(M), callable(B))).
  145evaluable_body_hook(nth_clause(H, _, R), _, (ground(R);strip_module(H, _, P), nonvar(P))).
  146evaluable_body_hook(format(Out, Format, Args), _,
  147                    (compound(Out), nonvar(Format), ground(Args))).
  148evaluable_body_hook(sort(A, _), _, (is_list(A), maplist(nonvar, A))).
  149evaluable_body_hook(A==B, _, (A==B;A\=B)).
  150evaluable_body_hook(A=..B, _, (is_list(B),B=[E|_],atomic(E);atomic(A);compound(A))).
  151
  152replace_goal_hook(retractall(_), _, true).
  153replace_goal_hook(retract(_),    _, true).
  154replace_goal_hook(assertz(_),    _, true).
  155replace_goal_hook(asserta(_),    _, true).
  156replace_goal_hook(assert( _),    _, true).
  157replace_goal_hook(erase(  _),    _, true).
  158replace_goal_hook(gtrace, _, true).
  159replace_goal_hook(write(_, _), _, true).
  160replace_goal_hook(writeq(_, _), _, true).
  161replace_goal_hook(writeln(_, _), _, true).
  162replace_goal_hook(write(_), _, true).
  163replace_goal_hook(writeq(_), _, true).
  164replace_goal_hook(writeln(_), _, true).
  165replace_goal_hook(write_term(_, _), _, true).
  166replace_goal_hook(write_term(_, _, _), _, true).
  167replace_goal_hook(nl, _, true).
  168replace_goal_hook(nl(_), _, true).
  169replace_goal_hook(call_ai(G), abstract_interpreter, G).
  170replace_goal_hook(eval_ai(G), abstract_interpreter, G).
  171replace_goal_hook(skip_ai(_), abstract_interpreter, true).
  172replace_goal_hook(V is A, _, (ground(A)->V is A; var(V))).
  173replace_goal_hook(nb_getval(A, V), _, ignore((nonvar(A), nb_current(A, V)))).
  174replace_goal_hook(nb_setarg(_, _, _), _, true).
  175
  176replace_body_hook(with_value(G, _, _), context_values, G).
  177replace_body_hook(with_value(G, _, _, _), context_values, G).
  178replace_body_hook(with_context_value(G, _, _), context_values, G).
  179replace_body_hook(with_context_value(G, _, _, _), context_values, G).
  180replace_body_hook(with_context_values(G, _, _), context_values, G).
  181replace_body_hook(with_context_values(G, _, _, _), context_values, G).
  182replace_body_hook('$with_asr'( G, _), ctrtchecks, G).
  183replace_body_hook('$with_gloc'(G, _), ctrtchecks, G).
  184replace_body_hook('$with_ploc'(G, _), ctrtchecks, G).
  185replace_body_hook(intr_ai(G), _, G).

 call_ai(:Goal)

Calls Goal during abstract interpretation and execution

  191call_ai(G) :- call(G).

 eval_ai(Goal)

Calls Goal during abstract interpretation but ignore during execution

  197eval_ai(_).

 skip_ai(Goal)

Calls Goal during execution bug ignore during abstract interpretation

  203skip_ai(G) :- call(G).

 intr_ai(Goal)

Abstract interpret Goal but ignore during execution

  209intr_ai(_).
  210
  211mod_qual(M, G as R, I:H as B:C) :- !,
  212    strip_module(M:G, N, H),
  213    predicate_property(N:H, implementation_module(I)),
  214    strip_module(M:R, A, C),
  215    predicate_property(A:C, implementation_module(B)).
  216mod_qual(M, G :- B, I:H :- B) :-
  217    strip_module(M:G, N, H),
  218    predicate_property(N:H, implementation_module(I)).
  219mod_qual(M, G, I:F/A) :-
  220    strip_module(M:G, N, F/A),
  221    functor(H, F, A),
  222    predicate_property(N:H, implementation_module(I)).
  223
  224:- public
  225    default_on_error/1.  226
  227default_on_error(Error) :-
  228    print_message(error, Error),
  229    backtrace(40 ).

 abstract_interpreter(:Goal, :Abstraction, +Options, -State) is multi

Abstract interpret :Goal, call(Abstraction, Literal, Body, State1, State2) is called over each found Literal to get an abstraction of the body of such literal. For instance, if abstraction is: abstraction(Literal, Body, State, State) :- clause(Literal, Body), the abstract interpreter becomes a typical prolog interpreter, although some optimizations makes that not accurate.

Valid options are:

location(Loc)

A location of the given Goal, used to report the location in case of error

evaluable(Eval)

Eval is a term or a list of term of the form:

M:G as Repl

if the literal being interpreted match with G, and M with the implementation module of literal, then Repl is called.

M:F/A

equivalent to M:G as R, where functor(R, F, A) succeeds.

M:G :- Body

if the literal being interpreted match with G, and M with the implementation module of literal, then continue with the interpretation of Body.

on_error(OnErr)

Calls call(OnErr, at_location(Loc, Error)) if Error is raised

  261abstract_interpreter(M:Goal, Abstraction, Options, State) :-
  262    option(location(Loc),   Options, context(toplevel, Goal)),
  263    option(evaluable(Eval), Options, []),
  264    option(on_error(OnErr), Options, abstract_interpreter:default_on_error),
  265    flatten(Eval, EvalL), % make it easy
  266    maplist(mod_qual(M), EvalL, MEvalL),
  267    abstract_interpreter_body(Goal, M, Abstraction,
  268                              state(Loc, MEvalL, M:OnErr, [], [], [], []),
  269                              State).

 abstract_interpreter(:Goal, :Abstraction, +Options) is multi

Same as abstract_interpreter(Goal, Abstraction, Options, _)

  275abstract_interpreter(MGoal, Abstraction, Options) :-
  276    abstract_interpreter(MGoal, Abstraction, Options, _).
  277
  278:- meta_predicate catch(2, ?, ?, ?, ?).  279catch(DCG, Ex, H, S1, S) :-
  280    catch(call(DCG, S1, S), Ex, H).
  281
  282
  283:- meta_predicate cut_to(2, ?, ?).

 cut_to(:Goal, ?State0, ?State)

Mark a place to where cut_from will come back.

  289cut_to(Goal) --> catch(Goal, cut_from, true).

 cut_from

Jump to where the cut_to was called

  295cut_from.
  296cut_from :- throw(cut_from).
  297
  298/*
  299% alternative (and more efficient) implementation follows:
  300% Note: this does not work since the choice points could be removed
  301% by a further cut operation, causing odd behavior
  302%
  303:- use_module(library(intercept)).
  304:- use_module(library(safe_prolog_cut_to)).
  305
  306:- meta_predicate intercept(2, ?, ?, ?, ?).
  307intercept(DCG, Ex, H, S1, S) :-
  308    intercept(call(DCG, S1, S), Ex, H).
  309
  310cut_to(Goal) -->
  311    {prolog_current_choice(CP)},
  312    intercept(Goal, cut_from, catch(safe_prolog_cut_to(CP), _, true)).
  313
  314cut_from :- send_signal(cut_from).
  315*/

 bottom(State1, State) is det

Sets the state of the analysis to bottom, which means that the analysis is unable to determine a solution to the Goal (universe set). Note that this could be due to a lack of precision of the analysis or simply being mathematically impossible to get a solution statically.

  324bottom(state(Loc, EvalL, OnErr, CallL, D, Cont, _),
  325       state(Loc, EvalL, OnErr, CallL, D, Cont, bottom)).

 abstract_interpreter_body(+Goal, +M, :Abstraction, ?State1, ?State) is multi

Like abstract_interpret(M:Goal, Abstraction, Options, State), where State1 is determined using Options, but intended to be called recursivelly during the interpretation.

  333abstract_interpreter_body(Goal, M, _) -->
  334    {var(Goal) ; var(M)}, bottom, !.
  335abstract_interpreter_body(M:Goal, _, Abs) -->
  336    !,
  337    abstract_interpreter_body(Goal, M, Abs).
  338abstract_interpreter_body(@(M:Goal, CM), _, Abs) -->
  339    !,
  340    cut_to(abstract_interpreter_lit(Goal, M, CM, Abs)).
  341
  342abstract_interpreter_body(call(Goal), M, Abs) --> !,
  343    cut_to(abstract_interpreter_body(Goal, M, Abs)).
  344abstract_interpreter_body(\+ A, M, Abs) --> !,
  345    abstract_interpret_body_not(A, M, Abs).
  346
  347abstract_interpret_body_not(A, M, Abs) -->
  348    ( cut_to(abstract_interpreter_body(A, M, Abs))
  349    ->( \+ is_bottom
  350      ->!,
  351        {fail}
  352      ; {fail}
  353      )
  354    ; !
  355    ).
  356abstract_interpret_body_not(_, _, _) --> bottom.
  357
  358get_conts(Conts, State, State) :-
  359    State = state(_, _, _, _, _, Conts, _).
  360
  361put_conts(Conts,
  362          state(Loc, EvalL, OnErr, CallL, Data, _, Result),
  363          state(Loc, EvalL, OnErr, CallL, Data, Conts, Result)).
  364
  365abstract_interpreter_body(catch(Goal, Ex, Handler), M, Abs, S1, S) :-
  366    !,
  367    catch(abstract_interpreter_body(Goal, M, Abs, S1, S), Ex,
  368          ( Handler,
  369            S = S1
  370          )).
  371abstract_interpreter_body(once(Goal), M, Abs, S1, S) :- !,
  372    once(abstract_interpreter_body(Goal, M, Abs, S1, S)).
  373abstract_interpreter_body(distinct(Goal), M, Abs, S1, S) :-
  374    predicate_property(M:distinct(_), implementation_module(solution_sequences)), !,
  375    distinct(Goal, abstract_interpreter_body(Goal, M, Abs, S1, S)).
  376abstract_interpreter_body(distinct(Witness, Goal), M, Abs, S1, S) :-
  377    predicate_property(M:distinct(_, _), implementation_module(solution_sequences)), !,
  378    distinct(Witness, abstract_interpreter_body(Goal, M, Abs, S1, S)).
  379
  380ord_spec(asc(_)).
  381ord_spec(desc(_)).
  382
  383abstract_interpreter_body(order_by(Spec, Goal), M, Abs, S1, S) :- !,
  384    ( is_list(Spec),
  385      Spec \= [],
  386      maplist(nonvar, Spec),
  387      maplist(ord_spec, Spec)
  388    ->order_by(Spec, abstract_interpreter_body(Goal, M, Abs, S1, S))
  389    ; abstract_interpreter_body(Goal, M, Abs, S1, S)
  390    ).
  391abstract_interpreter_body(setup_call_cleanup(S, C, E), M, Abs, State1, State) :- !,
  392    setup_call_cleanup(abstract_interpreter_body(S, M, Abs, State1, State2),
  393                       abstract_interpreter_body(C, M, Abs, State2, State3),
  394                       abstract_interpreter_body(E, M, Abs, State3, State)),
  395    ignore((var(State), State = State2)).
  396abstract_interpreter_body(call_cleanup(C, E), M, Abs, State1, State) :- !,
  397    call_cleanup(abstract_interpreter_body(C, M, Abs, State1, State2),
  398                 abstract_interpreter_body(E, M, Abs, State2, State)),
  399    ignore((var(State), State = State2)).
  400abstract_interpreter_body((A, B), M, Abs) -->
  401    !,
  402    { \+ terms_share(A, B)
  403    ->CutOnFail = true
  404    ; CutOnFail = fail
  405    },
  406    get_conts(ContL),
  407    put_conts([B|ContL]),
  408    abstract_interpreter_body(A, M, Abs),
  409    put_conts(ContL),
  410    ( abstract_interpreter_body(B, M, Abs)
  411    *->[]
  412    ; { CutOnFail = true
  413      ->!, fail                 % The whole body will fail
  414      }
  415    ).
  416abstract_interpreter_body((A*->B;C), M, Abs) -->
  417    !,
  418    { \+ terms_share(A, B)
  419    ->CutOnFail = true
  420    ; CutOnFail = fail
  421    },
  422    ( get_conts(ContL),
  423      put_conts([B|ContL]),
  424      abstract_interpreter_body(A, M, Abs),
  425    % *->
  426      put_conts(ContL),
  427      ( abstract_interpreter_body(B, M, Abs)
  428      *->[]
  429      ; { CutOnFail = true
  430        ->!, fail                 % The whole body will fail
  431        }
  432      )
  433    ; abstract_interpreter_body(C, M, Abs)
  434    ).
  435abstract_interpreter_body((A->B;C), M, Abs) --> !,
  436    {SCE = s(no)},
  437    ( interpret_local_cut(A, B, M, Abs, CutElse),
  438      {nb_setarg(1, SCE, CutElse)}
  439    ; ( {SCE = s(no)}
  440      ->abstract_interpreter_body(C, M, Abs)
  441      )
  442    ).
  443abstract_interpreter_body((A;B), M, Abs) --> !,
  444    ( abstract_interpreter_body(A, M, Abs)
  445    ; abstract_interpreter_body(B, M, Abs)
  446    ).
  447abstract_interpreter_body(A->B, M, Abs) --> !,
  448    interpret_local_cut(A, B, M, Abs, _).
  449abstract_interpreter_body(CallN, M, Abs) -->
  450    {do_resolve_calln(CallN, Goal)}, !,
  451    cut_to(abstract_interpreter_body(Goal, M, Abs)).
  452
  453push_top(Prev,
  454         state(Loc, EvalL, OnErr, CallL, Data, Cont, Prev),
  455         state(Loc, EvalL, OnErr, CallL, Data, Cont, [])).
  456
  457pop_top(bottom,
  458        state(Loc, EvalL, OnErr, CallL, Data, Cont, _),
  459        state(Loc, EvalL, OnErr, CallL, Data, Cont, bottom)).
  460pop_top([]) --> [].
  461
  462% CutElse make the failure explicit wrt. B
  463interpret_local_cut(A, B, M, Abs, CutElse) -->
  464    { \+ terms_share(A, B)
  465    ->CutOnFail = true
  466    ; CutOnFail = fail
  467    },
  468    push_top(Prev),
  469    get_conts(ContL),
  470    put_conts([B|ContL]),
  471    cut_to(abstract_interpreter_body(A, M, Abs)), % loose of precision
  472    put_conts(ContL),
  473    ( \+ is_bottom
  474    ->!,
  475      { CutElse = yes }
  476    ; { CutElse = no  }
  477    ),
  478    pop_top(Prev),
  479    ( abstract_interpreter_body(B, M, Abs)
  480    *->
  481      []
  482    ; ( {CutOnFail = true}
  483      ->cut_if_no_bottom
  484      ; []
  485      )
  486    ).
  487abstract_interpreter_body(!,    _, _) --> !, cut_if_no_bottom.
  488abstract_interpreter_body(A=B,  _, _) --> !, {A=B}.
  489abstract_interpreter_body(A\=B, _, _) -->
  490    !,
  491    ( {A\=B}
  492    ->[]
  493    ; {A==B}
  494    ->{fail}
  495    ; bottom
  496    ).
  497abstract_interpreter_body(BinExpr, _, _) -->
  498    { member(BinExpr, [A=\=B,
  499                       A=:=B,
  500                       A>B,
  501                       A<B,
  502                       A>=B,
  503                       A=<B])
  504    },
  505    necki,
  506    !,
  507    ( { ground(A),
  508        ground(B)
  509      }
  510    ->{BinExpr}
  511    ; bottom
  512    ).
  513abstract_interpreter_body(memberchk(A, B), _, _) -->
  514    !,
  515    ( {is_list(B)}
  516    ->( {nonvar(A)}
  517      ->{memberchk(A, B)}
  518      ; {member(A, B)},
  519        bottom
  520      )
  521    ; { append(_, [A|T], B),
  522        ( var(T)
  523        ->!
  524        ; true
  525        )
  526      },
  527      bottom
  528    ).
  529abstract_interpreter_body(true, _, _) --> !.
  530abstract_interpreter_body(fail, _, _) --> !, {fail}.
  531abstract_interpreter_body(A, M, _) -->
  532    get_state(state(Loc, _, OnError, CallL, _, _, _)),
  533    {evaluable_body_hook(A, M, Condition)},
  534    !,
  535    ( {call(Condition)}
  536    ->{catch(M:A,
  537             Error,
  538             ( call(OnError, at_location(Loc, Error)),
  539               call(OnError, call_stack(CallL)),
  540               fail
  541             ))
  542      }
  543    ; bottom
  544    ).
  545
  546abstract_interpreter_body(G, M, _) -->
  547    get_state(state(_, EvalL, _, _, _, _, _)),
  548    {get_body_replacement(G, M, EvalL, MR)},
  549    !,
  550    {call(MR)}.
  551abstract_interpreter_body(H, M, Abs) -->
  552    cut_to(abstract_interpreter_lit(H, M, M, Abs)).
  553
  554get_body_replacement(G, M, EvalL, MR) :-
  555    predicate_property(M:G, implementation_module(IM)),
  556    ( ( evaluable_goal_hook(G, IM)
  557      ; functor(G, F, A),
  558        memberchk(IM:F/A, EvalL)
  559      ),
  560      MR = M:G
  561    ; replace_goal_hook(G, IM, R),
  562      MR = M:R
  563    ; copy_term(EvalL, EvalC),
  564      memberchk((IM:G as I:R), EvalC),
  565      % This weird code is used because we can not use @/2 here
  566      qualify_meta_goal(M:R, MQ),
  567      strip_module(MQ, _, Q),
  568      MR = I:Q
  569    ).
  570
  571is_bottom(State, State) :-
  572    State = state(_, _, _, _, _, _, bottom),
  573    neck.
  574
  575cut_if_no_bottom -->
  576    ( \+ is_bottom
  577    ->{cut_from}
  578    ; []
  579    ).

 get_state(State, State, State)

Used in DCG's to get the current State

  585get_state(State, State, State).

 put_state(State, _, State)

Used in DCG's to set the current State

  591put_state(State, _, State).
  592
  593abstract_interpreter_lit(H, M, CM, Abs) -->
  594    { predicate_property(M:H, meta_predicate(Meta))
  595    ->qualify_meta_goal(CM:H, Meta, Goal)
  596    ; Goal = H
  597    },
  598    {predicate_property(M:Goal, implementation_module(IM))},
  599    get_state(state(Loc, EvalL, OnError, CallL, Data, Cont, Result)),
  600    ( {member(MCall-_, CallL),
  601       MCall =@= IM:Goal
  602      }
  603    ->bottom
  604    ; {copy_term(IM:Goal, MCall)},
  605      put_state(state(Loc, EvalL, OnError, [MCall-Loc|CallL], Data, Cont, Result)),
  606      ( { copy_term(EvalL, EvalC), % avoid undesirable unifications
  607          memberchk((IM:Goal :- Body), EvalC)
  608        ; replace_body_hook(Goal, IM, Body)
  609        }
  610      ->cut_to(abstract_interpreter_body(Body, M, Abs))
  611      ; { \+ predicate_property(M:Goal, defined) }
  612      ->{ call(OnError, error(existence_error(procedure, M:Goal), Loc)),
  613          call(OnError, call_stack(CallL)),
  614          % TBD: information to error
  615          fail
  616        }
  617      ; call(Abs, M:Goal, BM:Body),
  618        cut_to(abstract_interpreter_body(Body, BM, Abs))
  619      )
  620    ).

 match_head(:Goal, :Body, ?State1, ?State) is multi

Implements the next abstraction: Only test matches of literals with heads of clauses, without digging into the body.

  627match_head(MGoal, M:true) -->
  628    {predicate_property(MGoal, interpreted)},
  629    !,
  630    {strip_module(MGoal, M, _)},
  631    get_state(state(_,   EvalL, OnErr, CallL, D, Cont, Result)),
  632    put_state(state(Loc, EvalL, OnErr, CallL, D, Cont, Result)),
  633    {match_head_body(MGoal, Body, Loc)},
  634    ( {Body = _:true}
  635    ->[]
  636    ; bottom

  637    )

  637.
  638match_head(MGoal, M:true) -->
  639    {strip_module(MGoal, M, _)},
  640    bottom.

 match_head_body(:Goal, -Body, -From) is multi

Auxiliar predicate used to implement some abstractions. Given a Goal, unifies Body with the body of the matching clauses and From with the location of the clause.

  648match_head_body(MGoal, CMBody, From) :-
  649    ( extra_clauses(MGoal, CMBody, From)
  650    ; From = clause(Ref),
  651      clause(MGoal, Body, Ref),
  652      clause_property(Ref, module(CM)),
  653      CMBody = CM:Body
  654    ).
  655
  656extra_clauses(M:Goal, Body, From) :-
  657    extra_clauses(Goal, M, Body, From).

 extra_clauses(Goal, Module, :Body, -From) is multi

Called inside match_head_body/3 to increase the precision of the interpreter, it will define 'semantic' extra clauses, allowing for instance, analysis of dynamic predicates, interfaces, etc.

  665:- multifile extra_clauses/4.  666
  667extra_clauses(Goal, CM, I:Goal, _From) :-
  668    predicate_property(CM:Goal, implementation_module(M)),
  669    functor(Goal, F, A),
  670    ( interface:'$interface'(M, DIL),
  671      memberchk(F/A, DIL)
  672    ->interface:'$implementation'(I, M)
  673    ).

 match_noloops(:Goal, :Body, ?State1, ?State) is multi

Implements the next abstraction: Only test matches of literals with heads of clauses, and digs into the body provided that there are not recursive calls, in such a case the analysis reach bottom and we stop the recursion.

  681match_noloops(MGoal, Body) -->
  682    {predicate_property(MGoal, interpreted)},
  683    !,
  684    {strip_module(MGoal, M, Goal)},
  685    get_state(state(Loc1, EvalL, OnErr, CallL, S, Cont, Result1)),
  686    { functor(Goal, F, A),
  687      term_size(Goal, Size),
  688      \+ ( memberchk(M:F/A-Size1, S),
  689           Size1=<Size
  690         )
  691    ->match_head_body(MGoal, Body, Loc),
  692      Result = Result1
  693    ; Loc = Loc1,
  694      Result = bottom

  695    }

  695,
  696    put_state(state(Loc, EvalL, OnErr, CallL, [M:F/A-Size|S], Cont, Result))

  696.
  697match_noloops(MGoal, M:true) -->
  698    {strip_module(MGoal, M, _)},
  699    bottom