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