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            op(201,xfx,+\)
   51          ]).   52
   53:- use_module(library(apply)).   54:- use_module(library(lists)).   55:- use_module(library(option)).   56:- use_module(library(prolog_stack)).   57:- use_module(library(qualify_meta_goal)).   58:- use_module(library(resolve_calln)).   59:- use_module(library(solution_sequences)).   60:- use_module(library(term_size)).   61:- use_module(library(terms_share)).   62:- use_module(library(neck)).   63:- use_module(library(interface), []).   64
   65:- 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 */
   77:- meta_predicate
   78    abstract_interpreter(0,4,?),
   79    abstract_interpreter(0,4,+,-),
   80    abstract_interpreter_body(+,+,4,?,?),
   81    extra_clauses(+,+,-,-),
   82    match_head(0,*,*,*),
   83    match_head_body(0,*,*),
   84    match_noloops(0,*,*,*),
   85    call_ai(0),
   86    eval_ai(0),
   87    skip_ai(0).   88
   89:- multifile
   90    replace_goal_hook/3,
   91    replace_body_hook/3,
   92    evaluable_goal_hook/2,
   93    evaluable_body_hook/3.   94
   95:- dynamic
   96    evaluable_goal_hook/2.   97
   98evaluable_body_hook(absolute_file_name(A, _, O), _, (ground(A), ground(O))).
   99evaluable_body_hook(atom_concat(A, B, C), _,
  100                    ( nonvar(A), nonvar(B)
  101                    ; nonvar(A), nonvar(C)
  102                    ; nonvar(B), nonvar(C)
  103                    )).
  104evaluable_body_hook(atomic_list_concat(A, _), _, ground(A)).
  105evaluable_body_hook(atomic_list_concat(A, B, C), _,
  106                    ( ground(A), ground(B)
  107                    ; ground(B), ground(C)
  108                    )).
  109evaluable_body_hook(thread_self(_), _, true).
  110evaluable_body_hook(atom_length(A, _), _, ground(A)).
  111evaluable_body_hook(length(A, B), _, (is_list(A);ground(B))).
  112evaluable_body_hook(upcase_atom(A, _), _, ground(A)).
  113evaluable_body_hook(downcase_atom(A, _), _, ground(A)).
  114evaluable_body_hook(string_lower(A, _), _, ground(A)).
  115evaluable_body_hook(string_upper(A, _), _, ground(A)).
  116evaluable_body_hook(nb_current(A, _), _, ground(A)).
  117evaluable_body_hook(subtract(A, B, _), _, (is_list(A),is_list(B))).
  118evaluable_body_hook(intersection(A, B, _), _, (is_list(A),is_list(B))).
  119evaluable_body_hook(_ is A, _, ground(A)).
  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(A =:= B, _, (ground(A),ground(B))).
  125evaluable_body_hook(atom_codes(A, B), _, (ground(A);ground(B))).
  126evaluable_body_hook(atom_chars(A, B), _, (ground(A);ground(B))).
  127evaluable_body_hook(member(_, L), _, is_list(L)).
  128evaluable_body_hook(current_predicate(P), _, ground(P)).
  129evaluable_body_hook(current_module(M), _, ground(M)).
  130evaluable_body_hook(select(_, L, _), _, is_list(L)).
  131evaluable_body_hook(option(O, L), _, (once((is_dict(L);is_list(L))), nonvar(O))).
  132evaluable_body_hook(option(O, L, _), _, (once((is_dict(L);is_list(L))), nonvar(O))).
  133evaluable_body_hook(select_option(O, L, _), _, (once((is_dict(L);is_list(L))), nonvar(O))).
  134evaluable_body_hook(select_option(O, L, _, _), _, (once((is_dict(L);is_list(L))), nonvar(O))).
  135evaluable_body_hook(merge_options(N, O, _), _, (once((is_dict(N);is_list(N))),once((is_dict(O);is_list(O))))).
  136evaluable_body_hook(nth0(I, L, _), _, (is_list(L);nonvar(I))).
  137evaluable_body_hook(nth1(I, L, _), _, (is_list(L);nonvar(I))).
  138evaluable_body_hook(arg(_, C, _), _, nonvar(C)).
  139evaluable_body_hook(var(V),     _, nonvar(V)).
  140evaluable_body_hook(nonvar(V),  _, nonvar(V)).
  141evaluable_body_hook(atomic(A),  _, nonvar(A)).
  142evaluable_body_hook(atom(A),    _, nonvar(A)).
  143evaluable_body_hook(is_list(A), _, (ground(A);is_list(A))).
  144evaluable_body_hook(number(A),  _, nonvar(A)).
  145evaluable_body_hook(float(A),   _, nonvar(A)).
  146evaluable_body_hook(integer(A), _, nonvar(A)).
  147evaluable_body_hook(succ(A, B), _, (ground(A);ground(B))).
  148evaluable_body_hook(strip_module(A, _, _), _, nonvar(A)).
  149evaluable_body_hook(clause(A, _),    _, (strip_module(A, M, B), atom(M), callable(B))).
  150evaluable_body_hook(clause(A, _, _), _, (strip_module(A, M, B), atom(M), callable(B))).
  151evaluable_body_hook(nth_clause(H, _, R), _, (ground(R);strip_module(H, _, P), nonvar(P))).
  152evaluable_body_hook(format(Out, Format, Args), _,
  153                    (compound(Out), nonvar(Format), ground(Args))).
  154evaluable_body_hook(sort(A, _), _, (is_list(A), maplist(nonvar, A))).
  155evaluable_body_hook(A==B, _, (A==B;A\=B)).
  156evaluable_body_hook(is_dict(D), _, (ground(D))).
  157evaluable_body_hook(dict_pairs(D, T, P), _, (ground(D);ground(T),is_list(P))).
  158evaluable_body_hook(A=..B, _, (is_list(B),B=[E|_],atomic(E);atomic(A);compound(A))).
  159evaluable_body_hook(atom_number(A, N), _, (ground(A);ground(N))).
  160evaluable_body_hook(functor(H, F, A), _, (nonvar(H);ground(F),ground(A))).
  161evaluable_body_hook(predsort(G, L, _), _, (nonvar(G),is_list(L))).
  162evaluable_body_hook(predicate_property(A,B), _, (nonvar(A),nonvar(B))).
  163evaluable_body_hook(term_to_atom(A,B), _, (ground(A);ground(B))).
  164evaluable_body_hook(list(A, B), _, (is_list(A);ground(B))).
  165evaluable_body_hook(list_to_set(A, _), _, is_list(A)).
  166evaluable_body_hook(re_replace(A, B, V, _), _, (ground(A),ground(B),ground(V))).
  167evaluable_body_hook(context_module(_), _, fail).
  168evaluable_body_hook(file_name_extension(B, E, N), _, (ground(B);ground(E),ground(N))).
  169evaluable_body_hook(exists_file(F), _, ground(F)).
  170evaluable_body_hook(open(_, _, _, _), _, fail).
  171evaluable_body_hook(close(_), _, fail).
  172evaluable_body_hook(odbc_query(_, _, _, _), _, fail).
  173evaluable_body_hook(read_string(_, _, _), _, fail).
  174evaluable_body_hook(read_file_to_string(_, _, _), _, fail).
  175evaluable_body_hook(split_string(S, E, A,_), _, (ground(S),ground(E),ground(A))).
  176evaluable_body_hook(atomics_to_string(L, S, A), _, (ground(S),(is_list(L);ground(A)))).
  177evaluable_body_hook(between(L, U, _), _, (ground(L),ground(U))).
  178evaluable_body_hook(sub_string(S, _, _, _, _), _, ground(S)).
  179evaluable_body_hook(prolog_current_choice(_), _, fail).
  180evaluable_body_hook(prolog_current_frame(_), _, fail).
  181evaluable_body_hook(prolog_frame_attribute(_, _, _), _, fail).
  182evaluable_body_hook(copy_term(_, _), _, true).
  183evaluable_body_hook(left_trim(Type, Atomic, _), trim_utils, (ground(Type),ground(Atomic))).
  184evaluable_body_hook(right_trim(Type, Atomic, _), trim_utils, (ground(Type),ground(Atomic))).
  185
  186replace_goal_hook(retractall(_), _, true).
  187replace_goal_hook(retract(_),    _, true).
  188replace_goal_hook(assertz(_),    _, true).
  189replace_goal_hook(asserta(_),    _, true).
  190replace_goal_hook(assert( _),    _, true).
  191replace_goal_hook(erase(  _),    _, true).
  192replace_goal_hook(gtrace, _, true).
  193replace_goal_hook(repeat, _, (true;true)).
  194replace_goal_hook(write(_, _), _, true).
  195replace_goal_hook(writeq(_, _), _, true).
  196replace_goal_hook(writeln(_, _), _, true).
  197replace_goal_hook(write(_), _, true).
  198replace_goal_hook(writeq(_), _, true).
  199replace_goal_hook(writeln(_), _, true).
  200replace_goal_hook(write_term(_, _), _, true).
  201replace_goal_hook(write_term(_, _, _), _, true).
  202replace_goal_hook(nl, _, true).
  203replace_goal_hook(nl(_), _, true).
  204replace_goal_hook(call_ai(G), abstract_interpreter, G).
  205replace_goal_hook(eval_ai(G), abstract_interpreter, G).
  206replace_goal_hook(skip_ai(_), abstract_interpreter, true).
  207replace_goal_hook(V is A, _, (ground(A)->catch(V is A,_,fail); var(V))).
  208replace_goal_hook(nb_getval(A, V), _, ignore((nonvar(A), nb_current(A, V)))).
  209replace_goal_hook(nb_setarg(_, _, _), _, true).
  210
  211replace_body_hook(with_value(G, _, _), context_values, G).
  212replace_body_hook(with_value(G, _, _, _), context_values, G).
  213replace_body_hook(with_context_value(G, _, _), context_values, G).
  214replace_body_hook(with_context_value(G, _, _, _), context_values, G).
  215replace_body_hook(with_context_values(G, _, _), context_values, G).
  216replace_body_hook(with_context_values(G, _, _, _), context_values, G).
  217replace_body_hook('$with_asr'( G, _), ctrtchecks, G).
  218replace_body_hook('$with_gloc'(G, _), ctrtchecks, G).
  219replace_body_hook('$with_ploc'(G, _), ctrtchecks, G).
  220replace_body_hook(intr_ai(G), _, G).
 call_ai(:Goal)
Calls Goal during abstract interpretation and execution
  226call_ai(G) :- call(G).
 eval_ai(Goal)
Calls Goal during abstract interpretation but ignore during execution
  232eval_ai(_).
 skip_ai(Goal)
Calls Goal during execution bug ignore during abstract interpretation
  238skip_ai(G) :- call(G).
 intr_ai(Goal)
Abstract interpret Goal but ignore during execution
  244intr_ai(_).
  245
  246norm_eval(M, G as R, [] +\ (I:H as B:C)) :-
  247    !,
  248    strip_module(M:G, N, H),
  249    predicate_property(N:H, implementation_module(I)),
  250    strip_module(M:R, A, C),
  251    predicate_property(A:C, implementation_module(B)).
  252norm_eval(M, V +\ (G as R), V +\ (I:H as B:C)) :-
  253    !,
  254    strip_module(M:G, N, H),
  255    predicate_property(N:H, implementation_module(I)),
  256    strip_module(M:R, A, C),
  257    predicate_property(A:C, implementation_module(B)).
  258norm_eval(M, G :- B, [] +\ (I:H :- B)) :-
  259    strip_module(M:G, N, H),
  260    predicate_property(N:H, implementation_module(I)).
  261norm_eval(M, A +\ (G :- B), A +\ (I:H :- B)) :-
  262    strip_module(M:G, N, H),
  263    predicate_property(N:H, implementation_module(I)).
  264norm_eval(M, G, I:F/A) :-
  265    strip_module(M:G, N, F/A),
  266    functor(H, F, A),
  267    predicate_property(N:H, implementation_module(I)).
  268
  269:- public
  270    default_on_error/1.  271
  272default_on_error(Error) :-
  273    print_message(error, Error),
  274    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
  306abstract_interpreter(M:Goal, Abstraction, Options, State) :-
  307    option(location(Loc),   Options, context(toplevel, Goal)),
  308    option(evaluable(Eval), Options, []),
  309    option(on_error(OnErr), Options, abstract_interpreter:default_on_error),
  310    flatten(Eval, EvalL), % make it easy
  311    maplist(norm_eval(M), EvalL, MEvalL),
  312    abstract_interpreter_body(Goal, M, Abstraction,
  313                              state(Loc, MEvalL, M:OnErr, [], [], [], []),
  314                              State).
 abstract_interpreter(:Goal, :Abstraction, +Options) is multi
Same as abstract_interpreter(Goal, Abstraction, Options, _)
  320abstract_interpreter(MGoal, Abstraction, Options) :-
  321    abstract_interpreter(MGoal, Abstraction, Options, _).
  322
  323:- meta_predicate catch(2, ?, ?, ?, ?).  324catch(DCG, Ex, H, S1, S) :-
  325    catch(call(DCG, S1, S), Ex, ((S1 = S), H)).
  326
  327:- meta_predicate cut_to(2, ?, ?).
 cut_to(:Goal, ?State0, ?State)
Mark a place to where cut_from will come back.
  333cut_to(Goal) --> catch(Goal, cut_from, true).
 cut_from
Jump to where the cut_to was called
  339cut_from.
  340cut_from :- throw(cut_from).
  341
  342/*
  343% alternative (and more efficient) implementation follows:
  344% Note: this does not work since the choice points could be removed
  345% by a further cut operation, causing odd behavior
  346%
  347:- use_module(library(intercept)).
  348:- use_module(library(safe_prolog_cut_to)).
  349
  350:- meta_predicate intercept(2, ?, ?, ?, ?).
  351intercept(DCG, Ex, H, S1, S) :-
  352    intercept(call(DCG, S1, S), Ex, H).
  353
  354cut_to(Goal) -->
  355    {prolog_current_choice(CP)},
  356    intercept(Goal, cut_from, catch(safe_prolog_cut_to(CP), _, true)).
  357
  358cut_from :- send_signal(cut_from).
  359*/
 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.
  368bottom(state(Loc, EvalL, OnErr, CallL, D, Cont, _),
  369       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.
  377abstract_interpreter_body(Goal, M, _) -->
  378    {var(Goal) ; var(M)}, bottom, !.
  379abstract_interpreter_body(M:Goal, _, Abs) -->
  380    !,
  381    abstract_interpreter_body(Goal, M, Abs).
  382abstract_interpreter_body(@(M:Goal, CM), _, Abs) -->
  383    !,
  384    cut_to(abstract_interpreter_lit(Goal, M, CM, Abs)).
  385
  386abstract_interpreter_body(call(Goal), M, Abs) --> !,
  387    cut_to(abstract_interpreter_body(Goal, M, Abs)).
  388abstract_interpreter_body(\+ A, M, Abs) --> !,
  389    abstract_interpret_body_not(A, M, Abs).
  390abstract_interpreter_body(catch(Goal, Ex, Handler), M, Abs, S1, S) :-
  391    !,
  392    catch(abstract_interpreter_body(Goal, M, Abs, S1, S), Ex,
  393          ( Handler,
  394            S = S1
  395          )).
  396abstract_interpreter_body(once(Goal), M, Abs, S1, S) :- !,
  397    once(abstract_interpreter_body(Goal, M, Abs, S1, S)).
  398abstract_interpreter_body(distinct(Goal), M, Abs, S1, S) :-
  399    predicate_property(M:distinct(_), implementation_module(solution_sequences)),
  400    !,
  401    distinct(Goal, abstract_interpreter_body(Goal, M, Abs, S1, S)).
  402abstract_interpreter_body(distinct(Witness, Goal), M, Abs, S1, S) :-
  403    predicate_property(M:distinct(_, _), implementation_module(solution_sequences)),
  404    !,
  405    distinct(Witness, abstract_interpreter_body(Goal, M, Abs, S1, S)).
  406abstract_interpreter_body(order_by(Spec, Goal), M, Abs, S1, S) :-
  407    !,
  408    ( is_list(Spec),
  409      Spec \= [],
  410      maplist(nonvar, Spec),
  411      maplist(ord_spec, Spec)
  412    ->order_by(Spec, abstract_interpreter_body(Goal, M, Abs, S1, S))
  413    ; abstract_interpreter_body(Goal, M, Abs, S1, S)
  414    ).
  415abstract_interpreter_body(setup_call_cleanup(S, C, E), M, Abs, State1, State) :-
  416    !,
  417    setup_call_cleanup(abstract_interpreter_body(S, M, Abs, State1, State2),
  418                       abstract_interpreter_body(C, M, Abs, State2, State3),
  419                       ( ( var(State3)
  420                         ->( var(State2)
  421                           ->State3 = State1
  422                           ; State3 = State2
  423                           )
  424                         ; true
  425                         ),
  426                         abstract_interpreter_body(E, M, Abs, State3, State)
  427                       )),
  428    ( var(State)
  429    ->( var(State3)
  430      ->( var(State2)
  431        ->State = State1
  432        ; State = State2
  433        )
  434      ; State = State3
  435      )
  436    ; true
  437    ).
  438
  439abstract_interpreter_body(call_cleanup(C, E), M, Abs, State1, State) :-
  440    !,
  441    call_cleanup(abstract_interpreter_body(C, M, Abs, State1, State2),
  442                 ( ( var(State2)
  443                   ->State2 = State1
  444                   ; true
  445                   ),
  446                   abstract_interpreter_body(E, M, Abs, State2, State)
  447                 )),
  448    ( var(State)
  449    ->State = State2
  450    ; true
  451    ).
  452abstract_interpreter_body(findall(Pattern, Goal, List), M, Abs, State, State) :-
  453    !,
  454    findall(Pattern,
  455            ( call_nth(abstract_interpreter_body(Goal, M, Abs, State, _), N),
  456              ( N = 2 % this prevents infinite loops
  457              ->!
  458              ; true
  459              )
  460            ), List, _).
  461abstract_interpreter_body((A, B), M, Abs) -->
  462    !,
  463    { \+ terms_share(A, B)
  464    ->CutOnFail = true
  465    ; CutOnFail = fail
  466    },
  467    get_conts(ContL),
  468    put_conts([B|ContL]),
  469    abstract_interpreter_body(A, M, Abs),
  470    put_conts(ContL),
  471    ( abstract_interpreter_body(B, M, Abs)
  472    *->[]
  473    ; { CutOnFail = true
  474      ->!, fail                 % The whole body will fail
  475      }
  476    ).
  477abstract_interpreter_body((A*->B;C), M, Abs) -->
  478    !,
  479    { \+ terms_share(A, B)
  480    ->CutOnFail = true
  481    ; CutOnFail = fail
  482    },
  483    ( get_conts(ContL),
  484      put_conts([B|ContL]),
  485      abstract_interpreter_body(A, M, Abs),
  486    % *->
  487      put_conts(ContL),
  488      ( abstract_interpreter_body(B, M, Abs)
  489      *->[]
  490      ; { CutOnFail = true
  491        ->!, fail                 % The whole body will fail
  492        }
  493      )
  494    ; abstract_interpreter_body(C, M, Abs)
  495    ).
  496abstract_interpreter_body((A->B;C), M, Abs) --> !,
  497    {SCE = s(no)},
  498    ( interpret_local_cut(A, B, M, Abs, CutElse),
  499      {nb_setarg(1, SCE, CutElse)}
  500    ; ( {SCE = s(no)}
  501      ->abstract_interpreter_body(C, M, Abs)
  502      )
  503    ).
  504abstract_interpreter_body((A;B), M, Abs) --> !,
  505    ( abstract_interpreter_body(A, M, Abs)
  506    ; abstract_interpreter_body(B, M, Abs)
  507    ).
  508abstract_interpreter_body(A->B, M, Abs) --> !,
  509    interpret_local_cut(A, B, M, Abs, _).
  510abstract_interpreter_body(CallN, M, Abs) -->
  511    {do_resolve_calln(CallN, Goal)}, !,
  512    cut_to(abstract_interpreter_body(Goal, M, Abs)).
  513abstract_interpreter_body(!,    _, _) --> !, cut_if_no_bottom.
  514abstract_interpreter_body(A=B,  _, _) --> !, {A=B}.
  515abstract_interpreter_body(A\=B, _, _) -->
  516    !,
  517    ( {A\=B}
  518    ->[]
  519    ; {A==B}
  520    ->{fail}
  521    ; bottom
  522    ).
  523abstract_interpreter_body(A\==B, _, _) -->
  524    !,
  525    ( {A==B}
  526    ->{fail}
  527    ; {A\=B}
  528    ->{true}
  529    ; bottom
  530    ).
  531abstract_interpreter_body(BinExpr, _, _) -->
  532    { member(BinExpr, [A=\=B,
  533                       A=:=B,
  534                       A>B,
  535                       A<B,
  536                       A>=B,
  537                       A=<B])
  538    },
  539    necki,
  540    !,
  541    ( { ground(A),
  542        ground(B)
  543      }
  544    ->{BinExpr}
  545    ; bottom
  546    ).
  547abstract_interpreter_body(memberchk(A, B), _, _) -->
  548    !,
  549    ( {is_list(B)}
  550    ->( {nonvar(A)}
  551      ->{memberchk(A, B)}
  552      ; {member(A, B)},
  553        bottom
  554      )
  555    ; { append(_, [A|T], B),
  556        ( var(T)
  557        ->!
  558        ; true
  559        )
  560      },
  561      bottom
  562    ).
  563abstract_interpreter_body(true, _, _) --> !.
  564abstract_interpreter_body(fail, _, _) --> !, {fail}.
  565abstract_interpreter_body(A, M, _) -->
  566    get_state(state(Loc, _, OnError, CallL, _, _, _)),
  567    {evaluable_body_hook(A, M, Condition)},
  568    !,
  569    ( {call(Condition)}
  570    ->{catch(M:A,
  571             Error,
  572             ( call(OnError, at_location(Loc, Error)),
  573               call(OnError, call_stack(CallL)),
  574               fail
  575             ))
  576      }
  577    ; bottom
  578    ).
  579
  580abstract_interpreter_body(G, M, _) -->
  581    get_state(state(_, EvalL, _, _, _, _, _)),
  582    {get_body_replacement(G, M, EvalL, MR)},
  583    !,
  584    {call(MR)}.
  585abstract_interpreter_body(H, M, Abs) -->
  586    cut_to(abstract_interpreter_lit(H, M, M, Abs)).
  587
  588% Auxiliary predicates for abstract_interpreter_body//3.  Placed here since I
  589% can not use discontiguous otherwise it will be impossible to debug it:
  590abstract_interpret_body_not(A, M, Abs) -->
  591    ( cut_to(abstract_interpreter_body(A, M, Abs))
  592    ->( \+ is_bottom
  593      ->!,
  594        {fail}
  595      ; {fail}
  596      )
  597    ; !
  598    ).
  599abstract_interpret_body_not(_, _, _) --> bottom.
  600
  601get_conts(Conts, State, State) :-
  602    State = state(_, _, _, _, _, Conts, _).
  603
  604put_conts(Conts,
  605          state(Loc, EvalL, OnErr, CallL, Data, _, Result),
  606          state(Loc, EvalL, OnErr, CallL, Data, Conts, Result)).
  607
  608ord_spec(asc(_)).
  609ord_spec(desc(_)).
  610
  611push_top(Prev,
  612         state(Loc, EvalL, OnErr, CallL, Data, Cont, Prev),
  613         state(Loc, EvalL, OnErr, CallL, Data, Cont, [])).
  614
  615pop_top(bottom,
  616        state(Loc, EvalL, OnErr, CallL, Data, Cont, _),
  617        state(Loc, EvalL, OnErr, CallL, Data, Cont, bottom)).
  618pop_top([]) --> [].
  619
  620% CutElse make the failure explicit wrt. B
  621interpret_local_cut(A, B, M, Abs, CutElse) -->
  622    { \+ terms_share(A, B)
  623    ->CutOnFail = true
  624    ; CutOnFail = fail
  625    },
  626    push_top(Prev),
  627    get_conts(ContL),
  628    put_conts([B|ContL]),
  629    cut_to(abstract_interpreter_body(A, M, Abs)), % loose of precision
  630    put_conts(ContL),
  631    ( \+ is_bottom
  632    ->!,
  633      { CutElse = yes }
  634    ; { CutElse = no  }
  635    ),
  636    pop_top(Prev),
  637    ( abstract_interpreter_body(B, M, Abs)
  638    *->
  639      []
  640    ; ( {CutOnFail = true}
  641      ->cut_if_no_bottom
  642      ; []
  643      )
  644    ).
  645
  646get_body_replacement(G, M, EvalL, MR) :-
  647    predicate_property(M:G, implementation_module(IM)),
  648    ( functor(G, F, A),
  649      functor(P, F, A),
  650      memberchk(LArgs +\ (IM:P as I:T), EvalL)
  651    ->copy_term(LArgs +\ (IM:P as I:T), (LArgs +\ (IM:G as I:R))),
  652      % This weird code is used because we can not use @/2 here
  653      qualify_meta_goal(M:R, MQ),
  654      strip_module(MQ, _, Q),
  655      MR = I:Q
  656    ; replace_goal_hook(G, IM, R)
  657    ->MR = M:R
  658    ; ( evaluable_goal_hook(G, IM)
  659      ; functor(G, F, A),
  660        memberchk(IM:F/A, EvalL)
  661      )
  662    ->MR = M:G
  663    ).
  664
  665is_bottom(State, State) :-
  666    State = state(_, _, _, _, _, _, bottom),
  667    neck.
  668
  669cut_if_no_bottom -->
  670    ( \+ is_bottom
  671    ->{cut_from}
  672    ; []
  673    ).
 get_state(State, State, State)
Used in DCG's to get the current State
  679get_state(State, State, State).
 put_state(State, _, State)
Used in DCG's to set the current State
  685put_state(State, _, State).
  686
  687abstract_interpreter_lit(H, M, CM, Abs) -->
  688    { predicate_property(M:H, meta_predicate(Meta))
  689    ->qualify_meta_goal(CM:H, Meta, Goal)
  690    ; Goal = H
  691    },
  692    {predicate_property(M:Goal, implementation_module(IM))},
  693    get_state(state(Loc, EvalL, OnError, CallL, Data, Cont, Result)),
  694    ( {member(MCall-_, CallL),
  695       MCall =@= IM:Goal
  696      }
  697    ->bottom
  698    ; {copy_term(IM:Goal, MCall)},
  699      put_state(state(Loc, EvalL, OnError, [MCall-Loc|CallL], Data, Cont, Result)),
  700      ( { functor(Goal, F, A),
  701          functor(Pred, F, A),
  702          memberchk((LArgs +\ (IM:Pred :- Patt)), EvalL),
  703          % Using copy_term to avoid undesirable unifications:
  704          copy_term((LArgs +\ (IM:Pred :- Patt)), (LArgs +\ (IM:Goal :- Body)))
  705        ; replace_body_hook(Goal, IM, Body)
  706        }
  707      ->cut_to(abstract_interpreter_body(Body, M, Abs))
  708      ; { \+ predicate_property(M:Goal, defined) }
  709      ->{ call(OnError, error(existence_error(procedure, M:Goal), Loc)),
  710          call(OnError, call_stack(CallL)),
  711          % TBD: information to error
  712          fail
  713        }
  714      ; call(Abs, M:Goal, BM:Body),
  715        cut_to(abstract_interpreter_body(Body, BM, Abs))
  716      )
  717    ).
 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.
  724match_head(MGoal, M:true) -->
  725    {predicate_property(MGoal, interpreted)},
  726    !,
  727    {strip_module(MGoal, M, _)},
  728    get_state(state(_,   EvalL, OnErr, CallL, D, Cont, Result)),
  729    put_state(state(Loc, EvalL, OnErr, CallL, D, Cont, Result)),
  730    {match_head_body(MGoal, Body, Loc)},
  731    ( {Body = _:true}
  732    ->[]
  733    ; bottom
  734    )
  734.
  735match_head(MGoal, M:true) -->
  736    {strip_module(MGoal, M, _)},
  737    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.
  745match_head_body(MGoal, CMBody, From) :-
  746    ( extra_clauses(MGoal, CMBody, From)
  747    ; From = clause(Ref),
  748      clause(MGoal, Body, Ref),
  749      clause_property(Ref, module(CM)),
  750      CMBody = CM:Body
  751    ).
  752
  753extra_clauses(M:Goal, Body, From) :-
  754    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.
  762:- multifile extra_clauses/4.  763
  764extra_clauses(Goal, CM, I:Goal, _From) :-
  765    predicate_property(CM:Goal, implementation_module(M)),
  766    functor(Goal, F, A),
  767    ( interface:'$interface'(M, DIL),
  768      memberchk(F/A, DIL)
  769    ->interface:'$implementation'(I, M)
  770    ).
 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.
  778match_noloops(MGoal, Body) -->
  779    {predicate_property(MGoal, interpreted)},
  780    !,
  781    {strip_module(MGoal, M, Goal)},
  782    get_state(state(Loc1, EvalL, OnErr, CallL, S, Cont, Result1)),
  783    { functor(Goal, F, A),
  784      term_size(Goal, Size),
  785      \+ ( memberchk(M:F/A-Size1, S),
  786           Size1=<Size
  787         )
  788    ->match_head_body(MGoal, Body, Loc),
  789      Result = Result1
  790    ; Loc = Loc1,
  791      Result = bottom
  792    }
  792,
  793    put_state(state(Loc, EvalL, OnErr, CallL, [M:F/A-Size|S], Cont, Result))
  793.
  794match_noloops(MGoal, M:true) -->
  795    {strip_module(MGoal, M, _)},
  796    bottom