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(lists)).   53:- use_module(library(qualify_meta_goal)).   54:- use_module(library(resolve_calln)).   55:- use_module(library(term_size)).   56:- use_module(library(terms_share)).   57:- use_module(library(neck)).   58:- use_module(library(interface), []).   59
   60:- init_expansors.

An abstract interpreter

This module provides support to implement some abstract interpreter-based code scanner. It tests statically an oversimplification of the possible unification of terms and call hooks over head and literals in the body of a clause to collect certain information.

author
- Edison Mera */
   72:- meta_predicate
   73    abstract_interpreter(0,4,?),
   74    abstract_interpreter(0,4,+,-),
   75    abstract_interpreter_body(+,+,4,?,?),
   76    extra_clauses(+,+,-,-),
   77    match_head(0,*,*,*),
   78    match_head_body(0,*,*),
   79    match_noloops(0,*,*,*),
   80    call_ai(0),
   81    eval_ai(0),
   82    skip_ai(0).   83
   84:- multifile
   85    replace_goal_hook/3,
   86    replace_body_hook/3,
   87    evaluable_goal_hook/2,
   88    evaluable_body_hook/3.   89
   90:- dynamic
   91    evaluable_goal_hook/2.   92
   93:- discontiguous
   94    abstract_interpreter_body/5.   95
   96evaluable_body_hook(absolute_file_name(A, _, O), _, (ground(A), ground(O))).
   97evaluable_body_hook(atom_concat(A, B, C), _,
   98                    ( nonvar(A), nonvar(B)
   99                    ; nonvar(A), nonvar(C)
  100                    ; nonvar(B), nonvar(C)
  101                    )).
  102evaluable_body_hook(atomic_list_concat(A, _), _, ground(A)).
  103evaluable_body_hook(atomic_list_concat(A, B, C), _,
  104                    ( ground(A), ground(B)
  105                    ; ground(B), ground(C)
  106                    )).
  107evaluable_body_hook(thread_self(_), _, true).
  108evaluable_body_hook(atom_length(A, _), _, ground(A)).
  109evaluable_body_hook(upcase_atom(A, _), _, ground(A)).
  110evaluable_body_hook(downcase_atom(A, _), _, ground(A)).
  111evaluable_body_hook(string_lower(A, _), _, ground(A)).
  112evaluable_body_hook(string_upper(A, _), _, ground(A)).
  113evaluable_body_hook(nb_current(A, _), _, ground(A)).
  114evaluable_body_hook(_ is A, _, ground(A)).
  115evaluable_body_hook(A > B, _, (ground(A),ground(B))).
  116evaluable_body_hook(A >= B, _, (ground(A),ground(B))).
  117evaluable_body_hook(A < B, _, (ground(A),ground(B))).
  118evaluable_body_hook(A =< B, _, (ground(A),ground(B))).
  119evaluable_body_hook(A =:= B, _, (ground(A),ground(B))).
  120evaluable_body_hook(atom_codes(A, B), _, (ground(A);ground(B))).
  121evaluable_body_hook(atom_chars(A, B), _, (ground(A);ground(B))).
  122evaluable_body_hook(member(_, L), _, is_list(L)).
  123evaluable_body_hook(current_predicate(P), _, ground(P)).
  124evaluable_body_hook(current_module(M), _, ground(M)).
  125evaluable_body_hook(select(_, L, _), _, is_list(L)).
  126evaluable_body_hook(option(O, L), _, (is_list(L), nonvar(O))).
  127evaluable_body_hook(nth0(I, L, _), _, (is_list(L);nonvar(I))).
  128evaluable_body_hook(nth1(I, L, _), _, (is_list(L);nonvar(I))).
  129evaluable_body_hook(arg(_, C, _), _, nonvar(C)).
  130evaluable_body_hook(var(V),     _, nonvar(V)).
  131evaluable_body_hook(nonvar(V),  _, nonvar(V)).
  132evaluable_body_hook(atomic(A),  _, nonvar(A)).
  133evaluable_body_hook(atom(A),    _, nonvar(A)).
  134evaluable_body_hook(is_list(A), _, (ground(A);is_list(A))).
  135evaluable_body_hook(number(A),  _, nonvar(A)).
  136evaluable_body_hook(float(A),   _, nonvar(A)).
  137evaluable_body_hook(integer(A), _, nonvar(A)).
  138evaluable_body_hook(strip_module(A, _, _), _, nonvar(A)).
  139evaluable_body_hook(clause(A, _),    _, (strip_module(A, M, B), atom(M), callable(B))).
  140evaluable_body_hook(clause(A, _, _), _, (strip_module(A, M, B), atom(M), callable(B))).
  141evaluable_body_hook(nth_clause(H, _, R), _, (ground(R);strip_module(H, _, P), nonvar(P))).
  142evaluable_body_hook(format(Out, Format, Args), _,
  143                    (compound(Out), nonvar(Format), ground(Args))).
  144evaluable_body_hook(sort(A, _), _, (is_list(A), maplist(nonvar, A))).
  145evaluable_body_hook(A==B, _, (A==B;A\=B)).
  146evaluable_body_hook(A=..B, _, (is_list(B),B=[E|_],atomic(E);atomic(A);compound(A))).
  147
  148replace_goal_hook(retractall(_), _, true).
  149replace_goal_hook(retract(_),    _, true).
  150replace_goal_hook(assertz(_),    _, true).
  151replace_goal_hook(asserta(_),    _, true).
  152replace_goal_hook(assert( _),    _, true).
  153replace_goal_hook(erase(  _),    _, true).
  154replace_goal_hook(gtrace, _, true).
  155replace_goal_hook(write(_, _), _, true).
  156replace_goal_hook(writeq(_, _), _, true).
  157replace_goal_hook(writeln(_, _), _, true).
  158replace_goal_hook(write(_), _, true).
  159replace_goal_hook(writeq(_), _, true).
  160replace_goal_hook(writeln(_), _, true).
  161replace_goal_hook(write_term(_, _), _, true).
  162replace_goal_hook(write_term(_, _, _), _, true).
  163replace_goal_hook(nl, _, true).
  164replace_goal_hook(nl(_), _, true).
  165replace_goal_hook(call_ai(G), abstract_interpreter, G).
  166replace_goal_hook(eval_ai(G), abstract_interpreter, G).
  167replace_goal_hook(skip_ai(_), abstract_interpreter, true).
  168replace_goal_hook(V is A, _, (ground(A)->V is A; var(V))).
  169replace_goal_hook(nb_getval(A, V), _, ignore((nonvar(A), nb_current(A, V)))).
  170replace_goal_hook(nb_setarg(_, _, _), _, true).
  171
  172replace_body_hook(with_value(G, _, _), context_values, G).
  173replace_body_hook(with_value(G, _, _, _), context_values, G).
  174replace_body_hook(with_context_value(G, _, _), context_values, G).
  175replace_body_hook(with_context_value(G, _, _, _), context_values, G).
  176replace_body_hook(with_context_values(G, _, _), context_values, G).
  177replace_body_hook(with_context_values(G, _, _, _), context_values, G).
  178replace_body_hook('$with_asr'( G, _), ctrtchecks, G).
  179replace_body_hook('$with_gloc'(G, _), ctrtchecks, G).
  180replace_body_hook('$with_ploc'(G, _), ctrtchecks, G).
  181replace_body_hook(intr_ai(G), _, G).
 call_ai(:Goal)
Calls Goal during abstract interpretation and execution
  187call_ai(G) :- call(G).
 eval_ai(Goal)
Calls Goal during abstract interpretation but ignore during execution
  193eval_ai(_).
 skip_ai(Goal)
Calls Goal during execution bug ignore during abstract interpretation
  199skip_ai(G) :- call(G).
 intr_ai(Goal)
Abstract interpret Goal but ignore during execution
  205intr_ai(_).
  206
  207mod_qual(M, G as R, I:H as B:C) :- !,
  208    strip_module(M:G, N, H),
  209    predicate_property(N:H, implementation_module(I)),
  210    strip_module(M:R, A, C),
  211    predicate_property(A:C, implementation_module(B)).
  212mod_qual(M, G :- B, I:H :- B) :-
  213    strip_module(M:G, N, H),
  214    predicate_property(N:H, implementation_module(I)).
  215mod_qual(M, G, I:F/A) :-
  216    strip_module(M:G, N, F/A),
  217    functor(H, F, A),
  218    predicate_property(N:H, implementation_module(I)).
  219
  220:- public
  221    default_on_error/1.  222
  223default_on_error(Error) :-
  224    print_message(error, Error),
  225    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
  257abstract_interpreter(M:Goal, Abstraction, Options, State) :-
  258    option(location(Loc),   Options, context(toplevel, Goal)),
  259    option(evaluable(Eval), Options, []),
  260    option(on_error(OnErr), Options, abstract_interpreter:default_on_error),
  261    flatten(Eval, EvalL), % make it easy
  262    maplist(mod_qual(M), EvalL, MEvalL),
  263    abstract_interpreter_body(Goal, M, Abstraction,
  264                              state(Loc, MEvalL, M:OnErr, [], [], [], []),
  265                              State).
 abstract_interpreter(:Goal, :Abstraction, +Options) is multi
Same as abstract_interpreter(Goal, Abstraction, Options, _)
  271abstract_interpreter(MGoal, Abstraction, Options) :-
  272    abstract_interpreter(MGoal, Abstraction, Options, _).
  273
  274:- meta_predicate catch(2, ?, ?, ?, ?).  275catch(DCG, Ex, H, S1, S) :-
  276    catch(call(DCG, S1, S), Ex, H).
  277
  278
  279:- meta_predicate cut_to(2, ?, ?).
 cut_to(:Goal, ?State0, ?State)
Mark a place to where cut_from will come back.
  285cut_to(Goal) --> catch(Goal, cut_from, true).
 cut_from
Jump to where the cut_to was called
  291cut_from.
  292cut_from :- throw(cut_from).
  293
  294/*
  295% alternative (and more efficient) implementation follows:
  296% Note: this does not work since the choice points could be removed
  297% by a further cut operation, causing odd behavior
  298%
  299:- use_module(library(intercept)).
  300:- use_module(library(safe_prolog_cut_to)).
  301
  302:- meta_predicate intercept(2, ?, ?, ?, ?).
  303intercept(DCG, Ex, H, S1, S) :-
  304    intercept(call(DCG, S1, S), Ex, H).
  305
  306cut_to(Goal) -->
  307    {prolog_current_choice(CP)},
  308    intercept(Goal, cut_from, catch(safe_prolog_cut_to(CP), _, true)).
  309
  310cut_from :- send_signal(cut_from).
  311*/
 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.
  320bottom(state(Loc, EvalL, OnErr, CallL, D, Cont, _),
  321       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.
  329abstract_interpreter_body(Goal, M, _) -->
  330    {var(Goal) ; var(M)}, bottom, !.
  331abstract_interpreter_body(M:Goal, _, Abs) -->
  332    !,
  333    abstract_interpreter_body(Goal, M, Abs).
  334abstract_interpreter_body(@(M:Goal, CM), _, Abs) -->
  335    !,
  336    cut_to(abstract_interpreter_lit(Goal, M, CM, Abs)).
  337
  338abstract_interpreter_body(call(Goal), M, Abs) --> !,
  339    cut_to(abstract_interpreter_body(Goal, M, Abs)).
  340abstract_interpreter_body(\+ A, M, Abs) --> !,
  341    abstract_interpret_body_not(A, M, Abs).
  342
  343abstract_interpret_body_not(A, M, Abs) -->
  344    ( cut_to(abstract_interpreter_body(A, M, Abs))
  345    ->( \+ is_bottom
  346      ->!,
  347        {fail}
  348      ; {fail}
  349      )
  350    ; !
  351    ).
  352abstract_interpret_body_not(_, _, _) --> bottom.
  353
  354get_conts(Conts, State, State) :-
  355    State = state(_, _, _, _, _, Conts, _).
  356
  357put_conts(Conts,
  358          state(Loc, EvalL, OnErr, CallL, Data, _, Result),
  359          state(Loc, EvalL, OnErr, CallL, Data, Conts, Result)).
  360
  361abstract_interpreter_body(catch(Goal, Ex, Handler), M, Abs, S1, S) :-
  362    !,
  363    catch(abstract_interpreter_body(Goal, M, Abs, S1, S), Ex,
  364          ( Handler,
  365            S = S1
  366          )).
  367abstract_interpreter_body(once(Goal), M, Abs, S1, S) :- !,
  368    once(abstract_interpreter_body(Goal, M, Abs, S1, S)).
  369abstract_interpreter_body(distinct(Goal), M, Abs, S1, S) :-
  370    predicate_property(M:distinct(_), implementation_module(solution_sequences)), !,
  371    distinct(Goal, abstract_interpreter_body(Goal, M, Abs, S1, S)).
  372abstract_interpreter_body(distinct(Witness, Goal), M, Abs, S1, S) :-
  373    predicate_property(M:distinct(_, _), implementation_module(solution_sequences)), !,
  374    distinct(Witness, abstract_interpreter_body(Goal, M, Abs, S1, S)).
  375
  376ord_spec(asc(_)).
  377ord_spec(desc(_)).
  378
  379abstract_interpreter_body(order_by(Spec, Goal), M, Abs, S1, S) :- !,
  380    ( is_list(Spec),
  381      Spec \= [],
  382      maplist(nonvar, Spec),
  383      maplist(ord_spec, Spec)
  384    ->order_by(Spec, abstract_interpreter_body(Goal, M, Abs, S1, S))
  385    ; abstract_interpreter_body(Goal, M, Abs, S1, S)
  386    ).
  387abstract_interpreter_body(setup_call_cleanup(S, C, E), M, Abs, State1, State) :- !,
  388    setup_call_cleanup(abstract_interpreter_body(S, M, Abs, State1, State2),
  389                       abstract_interpreter_body(C, M, Abs, State2, State3),
  390                       abstract_interpreter_body(E, M, Abs, State3, State)),
  391    ignore((var(State), State = State2)).
  392abstract_interpreter_body(call_cleanup(C, E), M, Abs, State1, State) :- !,
  393    call_cleanup(abstract_interpreter_body(C, M, Abs, State1, State2),
  394                 abstract_interpreter_body(E, M, Abs, State2, State)),
  395    ignore((var(State), State = State2)).
  396abstract_interpreter_body((A, B), M, Abs) -->
  397    !,
  398    { \+ terms_share(A, B)
  399    ->CutOnFail = true
  400    ; CutOnFail = fail
  401    },
  402    get_conts(ContL),
  403    put_conts([B|ContL]),
  404    abstract_interpreter_body(A, M, Abs),
  405    put_conts(ContL),
  406    ( abstract_interpreter_body(B, M, Abs)
  407    *->[]
  408    ; { CutOnFail = true
  409      ->!, fail                 % The whole body will fail
  410      }
  411    ).
  412abstract_interpreter_body((A*->B;C), M, Abs) -->
  413    !,
  414    { \+ terms_share(A, B)
  415    ->CutOnFail = true
  416    ; CutOnFail = fail
  417    },
  418    ( get_conts(ContL),
  419      put_conts([B|ContL]),
  420      abstract_interpreter_body(A, M, Abs),
  421    % *->
  422      put_conts(ContL),
  423      ( abstract_interpreter_body(B, M, Abs)
  424      *->[]
  425      ; { CutOnFail = true
  426        ->!, fail                 % The whole body will fail
  427        }
  428      )
  429    ; abstract_interpreter_body(C, M, Abs)
  430    ).
  431abstract_interpreter_body((A->B;C), M, Abs) --> !,
  432    {SCE = s(no)},
  433    ( interpret_local_cut(A, B, M, Abs, CutElse),
  434      {nb_setarg(1, SCE, CutElse)}
  435    ; ( {SCE = s(no)}
  436      ->abstract_interpreter_body(C, M, Abs)
  437      )
  438    ).
  439abstract_interpreter_body((A;B), M, Abs) --> !,
  440    ( abstract_interpreter_body(A, M, Abs)
  441    ; abstract_interpreter_body(B, M, Abs)
  442    ).
  443abstract_interpreter_body(A->B, M, Abs) --> !,
  444    interpret_local_cut(A, B, M, Abs, _).
  445abstract_interpreter_body(CallN, M, Abs) -->
  446    {do_resolve_calln(CallN, Goal)}, !,
  447    cut_to(abstract_interpreter_body(Goal, M, Abs)).
  448
  449push_top(Prev,
  450         state(Loc, EvalL, OnErr, CallL, Data, Cont, Prev),
  451         state(Loc, EvalL, OnErr, CallL, Data, Cont, [])).
  452
  453pop_top(bottom,
  454        state(Loc, EvalL, OnErr, CallL, Data, Cont, _),
  455        state(Loc, EvalL, OnErr, CallL, Data, Cont, bottom)).
  456pop_top([]) --> [].
  457
  458% CutElse make the failure explicit wrt. B
  459interpret_local_cut(A, B, M, Abs, CutElse) -->
  460    { \+ terms_share(A, B)
  461    ->CutOnFail = true
  462    ; CutOnFail = fail
  463    },
  464    push_top(Prev),
  465    get_conts(ContL),
  466    put_conts([B|ContL]),
  467    cut_to(abstract_interpreter_body(A, M, Abs)), % loose of precision
  468    put_conts(ContL),
  469    ( \+ is_bottom
  470    ->!,
  471      { CutElse = yes }
  472    ; { CutElse = no  }
  473    ),
  474    pop_top(Prev),
  475    ( abstract_interpreter_body(B, M, Abs)
  476    *->
  477      []
  478    ; ( {CutOnFail = true}
  479      ->cut_if_no_bottom
  480      ; []
  481      )
  482    ).
  483abstract_interpreter_body(!,    _, _) --> !, cut_if_no_bottom.
  484abstract_interpreter_body(A=B,  _, _) --> !, {A=B}.
  485abstract_interpreter_body(A\=B, _, _) -->
  486    !,
  487    ( {A\=B}
  488    ->[]
  489    ; {A==B}
  490    ->{fail}
  491    ; bottom
  492    ).
  493abstract_interpreter_body(BinExpr, _, _) -->
  494    { member(BinExpr, [A=\=B,
  495                       A=:=B,
  496                       A>B,
  497                       A<B,
  498                       A>=B,
  499                       A=<B])
  500    },
  501    necki,
  502    !,
  503    ( { ground(A),
  504        ground(B)
  505      }
  506    ->{BinExpr}
  507    ; bottom
  508    ).
  509abstract_interpreter_body(memberchk(A, B), _, _) -->
  510    !,
  511    ( {is_list(B)}
  512    ->( {nonvar(A)}
  513      ->{memberchk(A, B)}
  514      ; {member(A, B)},
  515        bottom
  516      )
  517    ; { append(_, [A|T], B),
  518        ( var(T)
  519        ->!
  520        ; true
  521        )
  522      },
  523      bottom
  524    ).
  525abstract_interpreter_body(true, _, _) --> !.
  526abstract_interpreter_body(fail, _, _) --> !, {fail}.
  527abstract_interpreter_body(A, M, _) -->
  528    get_state(state(Loc, _, OnError, CallL, _, _, _)),
  529    {evaluable_body_hook(A, M, Condition)},
  530    !,
  531    ( {call(Condition)}
  532    ->{catch(M:A,
  533             Error,
  534             ( call(OnError, at_location(Loc, Error)),
  535               call(OnError, call_stack(CallL)),
  536               fail
  537             ))
  538      }
  539    ; bottom
  540    ).
  541
  542abstract_interpreter_body(G, M, _) -->
  543    get_state(state(_, EvalL, _, _, _, _, _)),
  544    {get_body_replacement(G, M, EvalL, MR)},
  545    !,
  546    {call(MR)}.
  547abstract_interpreter_body(H, M, Abs) -->
  548    cut_to(abstract_interpreter_lit(H, M, M, Abs)).
  549
  550get_body_replacement(G, M, EvalL, MR) :-
  551    predicate_property(M:G, implementation_module(IM)),
  552    ( ( evaluable_goal_hook(G, IM)
  553      ; functor(G, F, A),
  554        memberchk(IM:F/A, EvalL)
  555      ),
  556      MR = M:G
  557    ; replace_goal_hook(G, IM, R),
  558      MR = M:R
  559    ; copy_term(EvalL, EvalC),
  560      memberchk((IM:G as I:R), EvalC),
  561      % This weird code is used because we can not use @/2 here
  562      qualify_meta_goal(M:R, MQ),
  563      strip_module(MQ, _, Q),
  564      MR = I:Q
  565    ).
  566
  567is_bottom(State, State) :-
  568    State = state(_, _, _, _, _, _, bottom),
  569    neck.
  570
  571cut_if_no_bottom -->
  572    ( \+ is_bottom
  573    ->{cut_from}
  574    ; []
  575    ).
 get_state(State, State, State)
Used in DCG's to get the current State
  581get_state(State, State, State).
 put_state(State, _, State)
Used in DCG's to set the current State
  587put_state(State, _, State).
  588
  589abstract_interpreter_lit(H, M, CM, Abs) -->
  590    { predicate_property(M:H, meta_predicate(Meta))
  591    ->qualify_meta_goal(CM:H, Meta, Goal)
  592    ; Goal = H
  593    },
  594    {predicate_property(M:Goal, implementation_module(IM))},
  595    get_state(state(Loc, EvalL, OnError, CallL, Data, Cont, Result)),
  596    ( {member(MCall-_, CallL),
  597       MCall =@= IM:Goal
  598      }
  599    ->bottom
  600    ; {copy_term(IM:Goal, MCall)},
  601      put_state(state(Loc, EvalL, OnError, [MCall-Loc|CallL], Data, Cont, Result)),
  602      ( { copy_term(EvalL, EvalC), % avoid undesirable unifications
  603          memberchk((IM:Goal :- Body), EvalC)
  604        ; replace_body_hook(Goal, IM, Body)
  605        }
  606      ->cut_to(abstract_interpreter_body(Body, M, Abs))
  607      ; { \+ predicate_property(M:Goal, defined) }
  608      ->{ call(OnError, error(existence_error(procedure, M:Goal), Loc)),
  609          call(OnError, call_stack(CallL)),
  610          % TBD: information to error
  611          fail
  612        }
  613      ; call(Abs, M:Goal, BM:Body),
  614        cut_to(abstract_interpreter_body(Body, BM, Abs))
  615      )
  616    ).
 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.
  623match_head(MGoal, M:true) -->
  624    {predicate_property(MGoal, interpreted)},
  625    !,
  626    {strip_module(MGoal, M, _)},
  627    get_state(state(_,   EvalL, OnErr, CallL, D, Cont, Result)),
  628    put_state(state(Loc, EvalL, OnErr, CallL, D, Cont, Result)),
  629    {match_head_body(MGoal, Body, Loc)},
  630    ( {Body = _:true}
  631    ->[]
  632    ; bottom
  633    )
  633.
  634match_head(MGoal, M:true) -->
  635    {strip_module(MGoal, M, _)},
  636    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.
  644match_head_body(MGoal, CMBody, From) :-
  645    ( extra_clauses(MGoal, CMBody, From)
  646    ; From = clause(Ref),
  647      clause(MGoal, Body, Ref),
  648      clause_property(Ref, module(CM)),
  649      CMBody = CM:Body
  650    ).
  651
  652extra_clauses(M:Goal, Body, From) :-
  653    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.
  661:- multifile extra_clauses/4.  662
  663extra_clauses(Goal, CM, I:Goal, _From) :-
  664    predicate_property(CM:Goal, implementation_module(M)),
  665    functor(Goal, F, A),
  666    ( interface:'$interface'(M, DIL),
  667      memberchk(F/A, DIL)
  668    ->interface:'$implementation'(I, M)
  669    ).
 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.
  677match_noloops(MGoal, Body) -->
  678    {predicate_property(MGoal, interpreted)},
  679    !,
  680    {strip_module(MGoal, M, Goal)},
  681    get_state(state(Loc1, EvalL, OnErr, CallL, S, Cont, Result1)),
  682    { functor(Goal, F, A),
  683      term_size(Goal, Size),
  684      \+ ( memberchk(M:F/A-Size1, S),
  685           Size1=<Size
  686         )
  687    ->match_head_body(MGoal, Body, Loc),
  688      Result = Result1
  689    ; Loc = Loc1,
  690      Result = bottom
  691    }
  691,
  692    put_state(state(Loc, EvalL, OnErr, CallL, [M:F/A-Size|S], Cont, Result))
  692.
  693match_noloops(MGoal, M:true) -->
  694    {strip_module(MGoal, M, _)},
  695    bottom