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.
77:- meta_predicate 78 abstract_interpreter(,,), 79 abstract_interpreter(,,,), 80 abstract_interpreter_body(,,,,), 81 extra_clauses(,,,), 82 match_head(,,,), 83 match_head_body(,,), 84 match_noloops(,,,), 85 call_ai(), 86 eval_ai(), 87 skip_ai(). 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).
226call_ai(G) :- call(G).
232eval_ai(_).
238skip_ai(G) :- call(G).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 ).
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
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, _)320abstract_interpreter(MGoal, Abstraction, Options) :- 321 abstract_interpreter(MGoal, Abstraction, Options, _). 322 323:- meta_predicate catch(, , , , ). 324catch(DCG, Ex, H, S1, S) :- 325 catch(call(DCG, S1, S), Ex, ((S1 = S), H)). 326 327:- meta_predicate cut_to(, , ).
333cut_to(Goal) --> catch(Goal, cut_from, true).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*/
368bottom(state(Loc, EvalL, OnErr, CallL, D, Cont, _),
369 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.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 ->{} 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 ).
679get_state(State, State, 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 ).
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.
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).
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 ).
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
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.