1% ---------------------------------------------------------------------- 2% BEGIN LICENSE BLOCK 3% Version: CMPL 1.1 4% 5% The contents of this file are subject to the Cisco-style Mozilla Public 6% License Version 1.1 (the "License"); you may not use this file except 7% in compliance with the License. You may obtain a copy of the License 8% at www.eclipse-clp.org/license. 9% 10% Software distributed under the License is distributed on an "AS IS" 11% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See 12% the License for the specific language governing rights and limitations 13% under the License. 14% 15% The Original Code is The ECLiPSe Constraint Logic Programming System. 16% The Initial Developer of the Original Code is Cisco Systems, Inc. 17% Portions created by the Initial Developer are 18% Copyright (C) 1991-2006 Cisco Systems, Inc. All Rights Reserved. 19% 20% Contributor(s): ECRC GmbH 21% Contributor(s): IC-Parc, Imperal College London 22% 23% END LICENSE BLOCK 24% 25% System: ECLiPSe Constraint Logic Programming System 26% Version: $Id: modes.pl,v 1.4 2013/02/09 20:27:57 jschimpf Exp $ 27% ---------------------------------------------------------------------- 28 29% 30% IDENTIFICATION: modes.pl 31% AUTHOR: Joachim Schimpf 32% PROJECT: IDLE 33% 34% An abstract interpreter for mode ananlysis. 35% 36% The abstract interpreter uses dataflow-driven computation with 37% streams to do the fixpoint iteration, which is based on the ideas of 38% 39% "An Implementation Technique for the Abstract Interpretation of Prolog" 40% by Annika Waern (SICS), ICLP 88 41% 42% The abstract terms are represented with ECLiPSe metaterms. 43% For a description of the abstract domain see below. 44% 45 46%-------------------------------------------------------- 47:- module(modes). 48%-------------------------------------------------------- 49 50:- comment(categories, ["Development Tools"]). 51:- comment(summary, "An abstract interpreter for mode ananlysis"). 52:- comment(author, "Joachim Schimpf, ECRC Munich"). 53:- comment(copyright, "Cisco Systems, Inc"). 54:- comment(date, "$Date: 2013/02/09 20:27:57 $"). 55:- comment(desc, html(" 56 This library provides a static mode analysis tool for ECLiPSe 57 programs. It takes as input a Prolog program and a goal pattern, and 58 performs an analysis of the modes that the predicates in the program 59 will be called with, given the specified goal pattern. The mode 60 analyser is loaded with 61 <PRE> 62 :- lib(modes). 63 </PRE> 64 The usage is simple. The predicate read_source/1 is used to read in 65 the source file to be analysed. The predicate analyze/1 starts the 66 analysis with a given call pattern and prints the results in the form 67 of a compilable mode declaration: 68 <PRE> 69 [eclipse 2]: read_source(qsort). 70 reading qsort 71 72 yes. 73 [eclipse 3]: analyze(qsort(++,-)). 74 75 % Analysed 3 call patterns of 3 predicates in 0.05 sec 76 % Number of pending goals: 29 77 % Global Stack used: 12892 78 :- mode partition(++, ++, -, -). 79 :- mode qsort(++, -). 80 :- mode qsort(++, -, ++). 81 82 yes. 83 [eclipse 4]: analyze(qsort(+,-)). 84 85 % Analysed 4 call patterns of 3 predicates in 0.13 sec 86 % Number of pending goals: 54 87 % Global Stack used: 35968 88 :- mode partition(?, ?, -, -). 89 :- mode qsort(+, -). 90 :- mode qsort(+, -, +). 91 92 yes. 93 </PRE> 94 Restrictions: Programs that use coroutining features cannot be analysed. 95 ")). 96 97:- export analyze/1, analyze_exits/1. 98 99 100:- reexport read_source/1 from source_storage. 101:- import get_clauses/2, undefined_predicate/1 from source_storage. 102 103:- pragma(nodebug). 104 105:- use_module(library(apply_macros)). 106:- setval(collect_builtin_modes, off). 107 108:- meta_attribute(modes, [ copy_term:copy_mode_attr/2 ]). 109 110:- import replace_attribute/3 from sepia_kernel. 111 112:- local merge/3. 113 114%-------------------------------------------------------- 115 116analyze(Call) :- 117 analyze(Call, Lookup), 118 lookup_to_list(Lookup, LookupList), 119 keysort(LookupList, SortedLookupList), 120 print_entry_lubs(SortedLookupList). 121 122analyze_exits(Call) :- 123 analyze(Call, Lookup), 124 lookup_to_list(Lookup, LookupList), 125 keysort(LookupList, SortedLookupList), 126 print_entry_exits(SortedLookupList). 127 128analyze(Call, Lookup) :- 129 check_call_arguments(Call), 130 setval(calls,0), 131 setval(predicates,0), 132 cputime(T0), 133 % Use subcall/2 to get rid of the delayed goals 134 block( 135 subcall(prove_goal(Call, Lookup, _Exit), Residue), 136 Tag, 137 printf("*** %w\n", [Tag]) 138 ), 139 T is cputime-T0, 140 statistics(global_stack_used, G), 141 length(Residue, GoalNr), 142 getval(calls, N), 143 getval(predicates, P), 144 printf("\n%% Analysed %d call patterns of %d predicates in %.2f sec\n", 145 [N, P, T]), 146 printf("%% Number of pending goals: %d\n", [GoalNr]), 147 printf("%% Global Stack used: %d\n", [G]). 148 149check_call_arguments(Call) :- 150 Call =.. [_|L], 151 check_argument_list(L). 152 153check_argument_list([]). 154check_argument_list([M|L]) :- 155 (nonvar(M), pattern(M) -> 156 true 157 ; 158 printf(error, "*** Bad call argument: %w\n%b", [M]), 159 abort 160 ), 161 check_argument_list(L). 162 163collect_keys(T, []) :- var(T), !. 164collect_keys([], []). 165collect_keys([K-_|Ps], [K|Ks]) :- 166 collect_keys(Ps, Ks). 167 168add_functor_keys([], []). 169add_functor_keys([H|T], [F-H|FT]) :- 170 functor(H, F, _), 171 add_functor_keys(T, FT). 172 173print_modes(Modes) :- 174 add_functor_keys(Modes, Keyed), 175 keysort(Keyed, KeySorted), 176 print_values(KeySorted). 177 178print_values([]). 179print_values([_-Mode|T]) :- 180 printf(":- mode %QDvOw", Mode), writeln(.), 181 print_values(T). 182 183print_entry_lubs([]). 184print_entry_lubs([_ - info(Entries, _Exits)|T]) :- 185 print_entry_lub(Entries), 186 print_entry_lubs(T). 187 188print_entries(X) :- 189 var(X), !. 190print_entries([H|T]) :- 191 writeln(H), 192 print_entries(T). 193 194print_entry_lub(Entries) :- 195 get_lub(Entries, '$bottom$', Lub), 196 ( 197 compound(Lub), 198 \+ aux_predicate(Lub) 199 -> 200 printf(":- mode %QDvOw", Lub), 201 writeln(.) 202 ; 203 true 204 ). 205 206print_entry_exits([]). 207print_entry_exits([_ - info(Entries, Exits)|T]) :- 208 print_entries(Entries), 209 print_exits(Exits), 210 print_entry_exits(T). 211 212print_exits([]). 213print_exits([H|T]) :- 214 put(output, 0' ), 215 writeln(H), 216 print_exits(T). 217 218aux_predicate(Call) :- 219 functor(Call, Name, _), 220 atom_string(Name, NameS), 221 substring(NameS, "$disj_", 1). 222 223%-------------------------------------------------------- 224% the abstract interpreter 225%-------------------------------------------------------- 226 227prove_goal(Call, Lookup, ExitStream) :- 228 functor(Call, F, A), 229 prove_goal(Call, Lookup, ExitStream, F/A). 230 231prove_goal(Call, Lookup, ExitStream, PredSpec) :- 232 undefined_predicate(PredSpec), 233 builtin(Call, ExitStream), !, 234 ( getval(collect_builtin_modes, on) -> 235 lookup_or_enter(Lookup, PredSpec, Info), 236 ( var(Info) -> 237 RawEntryStream = [Call|_], 238 stream_to_lubstream('$bottom$', RawEntryStream, _EntryStream), 239 Info = info(RawEntryStream, _) 240 ; 241 Info = info(RawEntryStream, not_used), 242 get_tail(RawEntryStream, RawEntryT), 243 RawEntryT = [Call|_] 244 ) 245 ; 246 true 247 ). 248prove_goal(Call, Lookup, ExitStream, PredSpec) :- 249 lookup_or_enter(Lookup, PredSpec, Info), 250 ( var(Info) -> % new predicate 251 RawEntryStream = [Call|_], 252 stream_to_lubstream('$bottom$', RawExitStream, ExitStream), 253 stream_to_lubstream('$bottom$', RawEntryStream, EntryStream), 254 Info = info(RawEntryStream, ExitStream), 255% writeln('New predicate' - PredSpec), 256 incval(predicates), 257 prove_call(EntryStream, Lookup, RawExitStream) 258 ; 259 Info = info(RawEntryStream, WholeExitStream), 260 get_tail(RawEntryStream, RawEntryT), 261 RawEntryT = [Call|_], % order? 262 get_last_sofar(WholeExitStream, ExitStream), % order? 263 true 264 ). 265 266 267delay prove_call(CallStream, _, _) if var(CallStream). 268 269prove_call([], _, []). 270prove_call([Call|Calls], Lookup, RawExitStream) :- 271% writeln(Call), 272 incval(calls), 273 get_clauses(Call, Clauses), 274 merge(ExitStream1, ExitStream2, RawExitStream), 275 prove_clauses(Clauses, Call, ExitStream1, Lookup), % order ? 276 prove_call(Calls, Lookup, ExitStream2). 277 278 279% prove_clauses(Clauses, Call, ExitStream, Lookup) 280% apply the call pattern Call to all Clauses in the list Clauses, 281% constructions a stream of exit patterns ExitStream 282% 283% If Clauses is [], then we have no source information (e.g. dynamic predicate) 284% and we use the worst case exit modes (by unifying every argument with ?). 285 286prove_clauses([], Call, [Exit], _) :- 287 mapargs(=(?), Call, Exit). 288prove_clauses([Clause|Clauses], Call, ExitStream, Lookup) :- 289 (Clauses == [] -> 290 prove_clause(Clause, Call, ExitStream, Lookup) 291 ; 292 merge(ExitStream1, ExitStream2, ExitStream), 293 prove_clause(Clause, Call, ExitStream1, Lookup), 294 prove_clauses(Clauses, Call, ExitStream2, Lookup) 295 ). 296 297prove_clause((Head :- Body), Call, ExitStream, Lookup) :- 298 pattern_to_term(Call, Head), 299 prove_subgoal(Lookup, Body, Head, EnvStream), 300 mapstream(term_to_pattern, EnvStream, ExitStream). 301 302 303% prove_subgoal(Lookup, Goal-Env, EnvStream) 304% prove_subgoal(Lookup, Goal, Env, EnvStream) 305% 306% Interpret the goal Goal in the environment Env, generating a stream 307% EnvStream of possible instances of Env (resulting from the execution 308% of Goal). Goal shares variables with Env, Env is usually the rest 309% of the clause that contains Goal. 310 311prove_subgoal(Lookup, Goal-Env, EnvStream) :- 312 prove_subgoal(Lookup, Goal, Env, EnvStream). 313 314prove_subgoal(_Lookup, Goal, Env, EnvStream) :- var(Goal), !, 315 writeln(error, "*** Problem: Metacalled goal unknown at analysis time"), 316 EnvStream = [Env]. % ignore metacalled abstract terms (wrong!) 317prove_subgoal(_Lookup, true, Env, EnvStream) :- !, 318 EnvStream = [Env]. 319prove_subgoal(Lookup, (Goal1 , Goal2), Env, EnvStream) :- !, 320 prove_subgoal(Lookup, Goal1, Goal2-Env, Env1Stream), 321 merge_stream_of_streams(Env2StreamStream, EnvStream), 322 mapstream(prove_subgoal(Lookup), Env1Stream, Env2StreamStream). 323/****** 324prove_subgoal(_Lookup, Term1=Term2, Env, EnvStream) :- !, 325 (unify(Term1, Term2) -> 326 EnvStream = [Env] 327 ; 328 EnvStream = [] 329 ). 330*******/ 331prove_subgoal(Lookup, Goal, Env, EnvStream) :- 332 term_to_pattern(Goal, Call), 333% writeln(Call), 334 prove_goal(Call, Lookup, GoalExitStream), 335 mapstream(make_alt_envs(Goal, Env), GoalExitStream, EnvStream). 336% mapstream(update_env(Goal, Env), GoalExitStream, EnvStream). 337 338 339% make a copy of Env, instantiated according to GoalExit 340% 341% (To avoid keeping substitutions explicit, we store copies 342% of clause parts with the current instantiations) 343 344make_alt_envs(Goal, Env, GoalExit, NewEnv) :- 345% put(9), writeln(GoalExit), 346 copy_term([Goal|Env], [GoalCopy|NewEnv0]), 347 pattern_to_term(GoalExit, GoalCopy), 348 NewEnv = NewEnv0. % propagate only now 349 350% when the exitstream is lub'd, we can update the old environment 351% NO! because this will cause left-propagation of bindings, i.e. 352% we might evaluate new alternatives to a left hand goal using 353% instantiations from a right hand one. 354% 355% update_env(Goal, Env, GoalExit, NewEnv) :- 356% put(9), writeln(GoalExit), 357% (pattern_to_term(GoalExit, Goal) -> 358% true 359% ; 360% writeln(unexpected_failure(pattern_to_term(GoalExit, Goal))) 361% ), 362% NewEnv = Env. 363 364 365%-------------------------------------------------------- 366% Handling of abstract and mixed terms 367% 368% Abstract terms are represented by metaterms whose attribute is the mode. 369% 370% Aliasing: Variables which have multiple occurrences in the same 371% head/subgoal, are marked with '$alias'/1 by the source preprocessor. 372% To achieve safe handling of aliasing, we turn '$alias'({-}) 373% into ? rather than - . 374%-------------------------------------------------------- 375 376is_moded(_{Attr}) :- -?-> 377 nonvar(Attr), 378 !. 379 380get_mode(_{Attr}, Mode) :- -?-> 381 nonvar(Attr), 382 Mode = Attr. 383 384copy_mode_attr(_{Attr}, Copy) :- -?-> 385 add_attribute(Copy, Attr). 386 387 388% pattern_to_term(Call, Head) or pattern_to_term(Exit, SubGoal) 389% 390% convert a call/exit pattern into a mixed representation goal term 391 392pattern_to_term(Abstr, Term) :- 393 mapargs(abstraction_to_term, Abstr, Term). 394 395 396% convert an abstract descriptor into a mixed representation term 397% 398% the !(P) solutions is unsatisfactory, it works only for builtin returns. 399% Better: don't use unification for exit-patterns, but overwriting. 400% In that case be careful, so that builtin descriptions always transfer 401% the call mode properly to the exit mode in case the arg is not affected. 402 403abstraction_to_term(!(P), X) :- !, 404 ( is_moded(X) -> 405 replace_attribute(X, P, modes) 406 ; 407 unify_pattern_any(P, X) 408 ). 409abstraction_to_term(P, X) :- 410 unify_pattern_any(P, X). 411 412% convert a Goal in mixed representation into its abstract pattern form 413 414term_to_pattern(Call, Pattern) :- 415 mapargs(term_to_abstraction, Call, Pattern). 416 417 418% convert a term in mixed representation into its abstract descriptor 419 420term_to_abstraction(X, P) :- 421 var(X), !, 422 ( get_mode(X, P) -> 423 true 424 ; 425 P = - 426 ). 427term_to_abstraction('$alias'(X), P) :- !, 428 term_to_abstraction(X, P0), 429 aliasing_effect(P0, P). 430term_to_abstraction(X, P) :- 431 sumargs(compose_abstraction, X, ++, P). 432 433compose_abstraction(X, P0, P) :- 434 term_to_abstraction(X, Px), 435 composition(P0, Px, P). 436 437/*********** 438% 439% unify two mixed abstract/concrete terms 440% 441% (this should be done by directly unifying the two terms and defining 442% the proper handlers for the metaterms. The only thing that currently 443% prevents this is the '$alias'/1 wrapper. If aliasing is represented 444% with metaterm information as well, it can be done.) 445 446unify(X, Y) :- 447 var(X), !, 448 ( meta(X) -> 449 unify_abstr_any(X, Y) 450 ; 451 X=Y 452 ). 453unify('$alias'(X), Y) :- !, 454 unify(X, Y). 455unify(X, Y) :- 456 unify_concr_any(X, Y). 457 458unify_concr_any(X, Y) :- 459 var(Y), !, 460 ( meta(Y) -> 461 unify_abstr_concr(Y, X) 462 ; 463 X=Y 464 ). 465unify_concr_any(X, '$alias'(Y)) :- !, 466 unify_concr_any(X, Y). 467unify_concr_any(X, Y) :- 468 unify_concr_concr(X, Y). 469 470unify_concr_concr(X, Y) :- 471 (compound(X) -> 472 functor(X, F, A), 473 functor(Y, F, A), % this can fail ! 474 mapargs(unify, X, Y) 475 ; 476 X=Y % this can fail ! 477 ). 478 479unify_abstr_any(X, Y) :- 480 var(Y), !, 481 ( meta(Y) -> 482 unify_abstr_abstr(X, Y) 483 ; 484 X=Y 485 ). 486unify_abstr_any(X, '$alias'(Y)) :- !, 487 unify_abstr_any(X, Y). 488unify_abstr_any(X, Y) :- 489 unify_abstr_concr(X, Y). 490 491unify_abstr_abstr(X, Y) :- 492 meta_term(X, Xa), 493 meta_term(Y, Ya), 494 =(Xa, Ya, Za), 495 meta_term(Z, Za), 496 meta_bind(X, Z), 497 meta_bind(Y, Z). 498 499unify_abstr_concr(X, Y) :- 500 meta_term(X, Xa), 501 unify_pattern_any(Xa, Y), 502 term_to_abstraction(Y, Ya), % this doesn't look quite right ... 503 =(Xa, Ya, Za), 504 meta_term(Z, Za), 505 meta_bind(X, Z). 506 507**********/ 508 509unify_pattern_any(Xp, Y) :- % can't fail 510 var(Y), !, 511 ( get_mode(Y, Ya) -> 512 =(Xp, Ya, Za), 513 replace_attribute(Y, Za, modes) 514 ; 515 add_attribute(Y, Xp) % only here we _create_ meta terms! 516 ). 517unify_pattern_any(Xp, '$alias'(Y)) :- !, 518 unify_pattern_any(Xp, Y). 519unify_pattern_any(P, Y) :- 520 compound(Y), !, 521 functor(Y, _, N), 522 decomposition(P, Parg), 523 unify_pattern_any(N, Y, Parg). 524unify_pattern_any(_, _). 525 526unify_pattern_any(0, _, _) :- !. 527unify_pattern_any(N, Y, P) :- 528 arg(N, Y, Arg), 529 unify_pattern_any(P, Arg), 530 N1 is N-1, 531 unify_pattern_any(N1, Y, P). 532 533 534%-------------------------------------------------------- 535% 536% The abstract domain 537% 538% Abstract domain partial ordering: 539% 540% ? 541% / \ 542% -+ + 543% / \ / 544% / +- 545% - | 546% \ ++ 547% \ / 548% $bottom$ 549% 550% ++ ground term 551% + non-variable 552% - uninstantiated variable 553% +- non-variable term without internal shared variables 554% -+ - or +- 555% ? + or -, ie any term 556% 557%-------------------------------------------------------- 558 559% pattern(P) 560% 561% the valid abstract term descriptors 562 563pattern(-). 564pattern(++). 565pattern(+-). 566pattern(-+). 567pattern(+). 568pattern(?). 569 570 571% composition(P0, Pn, P) 572% 573% If an argument of type Pn is added as an additional argument to 574% a structure of type P0, then the type of the new structure is P 575 576composition(++, ++, ++) :- !. % groundness preservation 577composition(++, +-, +-) :- !. 578composition(++, -+, +-) :- !. 579composition(++, -, +-) :- !. 580composition(+-, ++, +-) :- !. % non-sharing preservation 581composition(+-, +-, +-) :- !. 582composition(+-, -+, +-) :- !. 583composition(+-, -, +-) :- !. 584composition(_, _, +). % otherwise: worst case for compound terms 585 586 587% decomposition(P, Parg) 588% 589% If a structure has type P, its arguments are of type Parg 590 591decomposition(-, -). 592decomposition(++, ++). 593decomposition(+-, -+). 594decomposition(-+, -+). 595decomposition(+, ?). 596decomposition(?, ?). 597 598 599% aliasing_effect(P0, P) 600 601aliasing_effect(-, ?) :- !. 602aliasing_effect(-+, ?) :- !. 603aliasing_effect(+-, +) :- !. 604aliasing_effect(P, P). 605 606 607% lub(PX, PY, PLub) 608% 609% least upper bound of 2 modes (cf. lattice above) 610 611lub(-, Y, LUB) :- 'lub-'(Y, LUB). 612lub(++, Y, LUB) :- 'lub++'(Y, LUB). 613lub(+-, Y, LUB) :- 'lub+-'(Y, LUB). 614lub(-+, Y, LUB) :- 'lub-+'(Y, LUB). 615lub(+, Y, LUB) :- 'lub+'(Y, LUB). 616lub(?, _, ?). 617 618'lub-'(-, -). 619'lub-'(++, -+). 620'lub-'(+-, -+). 621'lub-'(-+, -+). 622'lub-'(+, ?). 623'lub-'(?, ?). 624 625'lub+'(-, ?). 626'lub+'(++, +). 627'lub+'(+-, +). 628'lub+'(-+, ?). 629'lub+'(+, +). 630'lub+'(?, ?). 631 632'lub++'(-, -+). 633'lub++'(++, ++). 634'lub++'(+-, +-). 635'lub++'(-+, -+). 636'lub++'(+, +). 637'lub++'(?, ?). 638 639'lub+-'(-, -+). 640'lub+-'(++, +-). 641'lub+-'(+-, +-). 642'lub+-'(-+, -+). 643'lub+-'(+, +). 644'lub+-'(?, ?). 645 646'lub-+'(-, -+). 647'lub-+'(++, -+). 648'lub-+'(+-, -+). 649'lub-+'(-+, -+). 650'lub-+'(+, ?). 651'lub-+'(?, ?). 652 653% 654% =(PX, PY, PResult) 655% 656% unification of two abstract terms 657% 658 659=(-, Y, Y). 660=(++, _, ++). 661=(+-, Y, Z) :- '+- ='(Y,Z). 662=(-+, Y, Z) :- '-+ ='(Y,Z). 663=(+, Y, Z) :- '+ ='(Y,Z). 664=(?, Y, Z) :- '? ='(Y,Z). 665 666'+ ='(-, +). 667'+ ='(++, ++). 668'+ ='(+-, +). 669'+ ='(-+, +). 670'+ ='(+, +). 671'+ ='(?, +). 672 673'+- ='(-, +-). 674'+- ='(++, ++). 675'+- ='(+-, +-). 676'+- ='(-+, +-). 677'+- ='(+, +). 678'+- ='(?, +). 679 680'-+ ='(-, -+). 681'-+ ='(++, ++). 682'-+ ='(+-, +-). 683'-+ ='(-+, -+). 684'-+ ='(+, +). 685'-+ ='(?, ?). 686 687'? ='(-, ?). 688'? ='(++, ++). 689'? ='(+-, +). 690'? ='(-+, ?). 691'? ='(+, +). 692'? ='(?, ?). 693 694 695%-------------------------------------------------------- 696% operations on streams 697%-------------------------------------------------------- 698 699delay merge_stream_of_streams(StreamStream, _) if var(StreamStream). 700 701merge_stream_of_streams([], []). 702merge_stream_of_streams([SubStream|SubStreams], Merged) :- 703 merge(SubStream, MergedRest, Merged), 704 merge_stream_of_streams(SubStreams, MergedRest). 705 706 707% merge streams keeping duplicates 708 709delay merge(Stream1, Stream2, _) if var(Stream1), var(Stream2). 710 711merge(Stream1, Stream2, MergedTail) :- 712 var(Stream2) -> 713 merge1(Stream1, Stream2, MergedTail) 714 ; 715 merge1(Stream2, Stream1, MergedTail). 716 717merge1([], Stream2, Stream2). 718merge1([New|Tail], Stream2, [New|MergedTail1]) :- 719 merge(Tail, Stream2, MergedTail1). 720 721 722get_last(Rest, X, Last) :- 723 var(Rest), !, 724 X = Last. 725get_last([], X, X). 726get_last([H|T], _, Last) :- 727 get_last(T, H, Last). 728 729get_last_sofar(List, Last) :- 730 var(List), !, 731 List = Last. 732get_last_sofar(List, Last) :- 733 get_last(List, Last). 734 735get_last(List, Last) :- 736 var(List), !, 737 writeln(problem is get_last(List, Last)), 738 abort. 739get_last(List, Last) :- 740 List = [_|T], 741 (var(T) -> 742 Last = List 743 ; 744 get_last(T, Last) 745 ). 746 747get_tail(List, Tail) :- 748 var(List), !, 749 List = Tail. 750get_tail([_|T], Tail) :- 751 get_tail(T, Tail). 752 753get_lub(List, Lub, Lub) :- 754 var(List), !. 755get_lub([H|T], Lub0, Lub) :- 756 lub_pattern(Lub0, H, Lub1), 757 get_lub(T, Lub1, Lub). 758 759 760 761delay stream_to_lubstream(_OldLub, Stream, _LubStream) if var(Stream). 762 763stream_to_lubstream(_OldLub, [], []). 764stream_to_lubstream(OldLub, [H|T], LubT) :- 765 lub_pattern(OldLub, H, NewLub), 766 ( OldLub == NewLub -> 767 stream_to_lubstream(OldLub, T, LubT) 768 ; 769 LubT = [NewLub|NewLubT], 770 stream_to_lubstream(NewLub, T, NewLubT) 771 ). 772 773 774lub_pattern('$bottom$', T2, Tlub) :- !, 775 T2 = Tlub. 776lub_pattern(T1, T2, Tlub) :- 777 functor(T1, F, N), 778 functor(T2, F, N), 779 functor(Tlub, F, N), 780 lub_pattern(N, T1, T2, Tlub). 781 782lub_pattern(0, _, _, _) :- !. 783lub_pattern(N, T1, T2, Tlub) :- 784 arg(N, T1, A1), 785 arg(N, T2, A2), 786 arg(N, Tlub, Alub), 787 lub(A1, A2, Alub), 788 N1 is N-1, 789 lub_pattern(N1, T1, T2, Tlub). 790 791 792%-------------------------------------------------------- 793% lookup table 794% table(Key, Value, Left, Right) 795% 796% Key = Name/Arity 797% Value = info(EntryStream, ExitStream) 798%-------------------------------------------------------- 799 800 801new_lookup(_). 802 803lookup_or_enter(Table, Key, Value) :- 804 var(Table), !, 805 Table = table(Key, Value, _, _). 806lookup_or_enter(Table, Key, Value) :- 807 Table = table(K, _, _, _), 808 compare(Relation, Key, K), 809 descend(Relation, Key, Value, Table). 810 811descend(=, _, Value, table(_, Value, _, _)). 812descend(<, Key, Value, table(_, _, L, _)) :- 813 lookup_or_enter(L, Key, Value). 814descend(>, Key, Value, table(_, _, _, R)) :- 815 lookup_or_enter(R, Key, Value). 816 817lookup_to_list(Table, List) :- 818 lookup_to_list(Table, List, []). 819 820lookup_to_list(Table, List, Tail) :- 821 var(Table), !, 822 List = Tail. 823lookup_to_list(table(K, V, L, R), List, Tail) :- 824 lookup_to_list(L, List, [K-V|Rlist]), 825 lookup_to_list(R, Rlist, Tail). 826 827 828%-------------------------------------------------------- 829% some builtin descriptions 830% 831% specify the exit modes (success patterns) that will result 832% from the given input mode. [] means it will surely fail. 833% - be careful not to weaken the call modes! Use =/3 to avoid this. 834% - it helps the analysis when the exit patterns are free of 835% instantiation fault patterns 836% - in case one argument is not bound by the builtin, use '-' in the exit mode 837% This means that the caller argument is not affected 838% - The form !(<mode>) can be used to specify that the exit mode of an input 839% argument can be reduced with respect to the call mode, but it is not 840% possible to specify by unification, e.g. var(?) ---> var(!(-)) 841% (exit unification would not be able to change ? to something else) 842% - take care of builtins that can cause aliasing, currently: 843% =/2, =../2, arg/3, sort/2, keysort/2 844% library predicates: 845% member/2, delete/3 846% they must never return -, -+ or +- ! 847% 848% (=/2 should be handled directly by the abstract interpreter above) 849%-------------------------------------------------------- 850 851:- mode builtin(++, ?). 852 853builtin(X = Y, [Z = Z]) :- =(X,Y,Z0), aliasing_effect(Z0,Z). 854builtin(X \= Y, [X \= Y]). 855builtin(X == Y, [X == Y]). % could be handled better 856builtin(X \== Y, [X \== Y]). 857builtin(X @< Y, [X @< Y]). 858builtin(X @> Y, [X @> Y]). 859builtin(X @=< Y, [X @=< Y]). 860builtin(X @>= Y, [X @>= Y]). 861 862builtin(!, [!]). 863builtin(repeat, [repeat]). 864builtin(fail, []). 865builtin(abort, []). 866 867% The metacalling builtins are assumed to be preprocessed to cover 868% the calling aspect. Here we describe only the instantiation effect. 869builtin('$findall'(T,G,L), ['$findall'(T,G1,L1)]) :- 870 =(+, G, G1), =(+, L, L1). 871builtin('$bagof'(T,G,L), ['$bagof'(T,G1,L1)]) :- 872 =(+, G, G1), =(+, L, L1). 873builtin('$setof'(T,G,L), ['$setof'(T,G1,L1)]) :- 874 =(+, G, G1), =(+, L, L1). 875builtin('$coverof'(T,G,L), ['$coverof'(T,G1,L1)]) :- 876 =(+, G, G1), =(+, L, L1). 877builtin('$block'(G,_,R), ['$block'(G,?,R)]). 878 879builtin(var(++), []) :- !. 880builtin(var(+), []) :- !. 881builtin(var(+-), []) :- !. 882builtin(var(_), [var(!(-))]). 883builtin(nonground(++), []) :- !. 884builtin(nonground(_), [nonground(-)]). 885builtin(nonvar(-), []) :- !. 886builtin(nonvar(-+), [nonvar(+-)]) :- !. 887builtin(nonvar(?), [nonvar(+)]) :- !. 888builtin(nonvar(_), [nonvar(-)]). 889builtin(atom(-), []) :- !. 890builtin(atom(_), [atom(++)]). 891builtin(atomic(-), []) :- !. 892builtin(atomic(_), [atomic(++)]). 893builtin(number(-), []) :- !. 894builtin(number(_), [number(++)]). 895builtin(integer(-), []) :- !. 896builtin(integer(_), [integer(++)]). 897builtin(float(-), []) :- !. 898builtin(float(_), [float(++)]). 899builtin(string(-), []) :- !. 900builtin(string(_), [string(++)]). 901builtin(compound(-), []) :- !. 902builtin(compound(-+), [compound(+-)]) :- !. 903builtin(compound(?), [compound(+)]) :- !. 904builtin(compound(_), [compound(-)]). 905builtin(type_of(_,_), [type_of(-,++)]). 906builtin(get_var_info(_,_,_), [get_var_info(-,++,++)]). 907builtin(get_cut(_), [get_cut(++)]). 908builtin(cut_to(_), [cut_to(++)]). 909 910builtin(_ is _, [++ is ++]). 911builtin(_ > _, [++ > ++]). 912builtin(_ >= _, [++ >= ++]). 913builtin(_ < _, [++ < ++]). 914builtin(_ =< _, [++ =< ++]). 915builtin(_ =:= _, [++ =:= ++]). 916builtin(_ =\= _, [++ =\= ++]). 917builtin(>(_,_,_), [>(++,++,++)]). 918builtin(>=(_,_,_), [>=(++,++,++)]). 919builtin(<(_,_,_), [<(++,++,++)]). 920builtin(=<(_,_,_), [=<(++,++,++)]). 921builtin(=:=(_,_,_), [=:=(++,++,++)]). 922builtin(=\=(_,_,_), [=\=(++,++,++)]). 923builtin(max(_,_,_), [max(++,++,++)]). 924builtin(min(_,_,_), [min(++,++,++)]). 925 926% in univ, both arguments must have the same exit modes, but at least + 927builtin(++ =.. _, [++ =.. ++]) :- !. 928builtin(_ =.. ++, [++ =.. ++]) :- !. 929builtin(_ =.. _, [+ =.. +]). 930builtin(arg(_,++,_), [arg(++,++,++)]) :- !. 931builtin(arg(_,_,++), [arg(++,+-,++)]) :- !. 932builtin(arg(_,_,_), [arg(++,+,?)]). 933builtin(atom_string(_,_), [atom_string(++,++)]). 934builtin(char_int(_,_), [char_int(++,++)]). 935builtin(copy_term(X,_), [copy_term(X,X)]). 936builtin(functor(_,_,_), [functor(+-,++,++)]). 937builtin(integer_atom(_,_), [integer_atom(++,++)]). 938builtin(name(_,_), [name(++,++)]). 939builtin(string_list(_,_), [string_list(++,++)]). 940builtin(term_string(_,_), [term_string(-,++)]). 941 942builtin(concat_strings(_,_,_), [concat_strings(++,++,++)]). 943builtin(concat_atoms(_,_,_), [concat_atoms(++,++,++)]). 944 945builtin(read(_), [read(?)]). 946builtin(read(_,_), [read(++,?)]). 947builtin(read_(_,_,_), [read_(++,?,++)]). 948builtin(get(_), [get(++)]). 949builtin(write(_), [write(-)]). 950builtin(write(_,_), [write(++,-)]). 951builtin(writeln(_), [writeln(-)]). 952builtin(writeln(_,_), [writeln(++,-)]). 953builtin(writeq(_), [writeq(-)]). 954builtin(writeq(_,_), [writeq(++,-)]). 955builtin(writeq_(_,_,_), [writeq_(++,-,++)]). 956builtin(display(_), [display(-)]). 957builtin(put(_), [put(++)]). 958builtin(ttynl, [ttynl]). 959builtin(ttyput(_), [ttyput(++)]). 960builtin(get_stream(_,_), [get_stream(++,++)]). 961builtin(set_stream(_,_), [set_stream(++,++)]). 962builtin(get_prompt(_,_,_), [get_prompt(++,++,++)]). 963builtin(set_prompt(_,_,_), [set_prompt(++,++,++)]). 964builtin(flush(_), [flush(++)]). 965builtin(nl, [nl]). 966builtin(nl(_), [nl(++)]). 967builtin(open(_,_,_), [open(++,++,++)]). 968builtin(close(_), [close(++)]). 969 970builtin(asserta(_), [asserta(-)]). 971builtin(assert(_), [assert(-)]). 972builtin(retract(_), [retract(+)]). 973builtin(retract_all(_), [retract_all(-)]). 974builtin(clause(_), [clause(+)]). 975builtin(clause(_,_), [clause(+,+)]). 976builtin(abolish(_), [abolish(++)]). 977 978builtin(recorda(_,_), [recorda(+-,?)]). 979builtin(recorda(_,_,_), [recorda(+-,?,++)]). 980builtin(recordz(_,_), [recordz(+-,?)]). 981builtin(recordz_body(_,_,_), [recordz_body(+-,?,++)]). 982builtin(recorded(_,_), [recorded(+-,?)]). 983builtin(recorded(_,_,_), [recorded(+-,?,++)]). 984builtin(recorded_body(_,_,_), [recorded_body(+-,?,++)]). 985builtin(recorded_body(_,_,_,_), [recorded_body(+-,?,++,++)]). 986builtin(erase(_), [erase(++)]). 987builtin(erase(_,_), [erase(+-,?)]). 988 989builtin(setval(_,_), [setval(++,-)]). 990builtin(getval(_,_), [getval(++,?)]). 991builtin(incval(_), [incval(++)]). 992 993builtin(op(_,_,_), [op(++,++,++)]). 994builtin(local_op(_,_,_), [local_op(++,++,++)]). 995builtin(global_op(_,_,_), [global_op(++,++,++)]). 996builtin(local_record(_), [local_record(++)]). 997builtin(local_record_body(_,_), [local_record_body(++,++)]). 998builtin(cputime(_), [cputime(++)]). 999builtin(current_op(_,_,_), [current_op(++, ++,++)]). 1000builtin(current_module(_), [current_module(++)]). 1001builtin(create_module(_), [create_module(++)]). 1002builtin(get_flag(_,_), [get_flag(++,++)]). % not quite, but ... 1003builtin(set_flag(_,_), [set_flag(++,++)]). % not quite, but ... 1004builtin(get_flag(_,_,_), [get_flag(++,++,++)]). 1005builtin(get_flag_body(_,_,_,_), [get_flag_body(++,++,++,++)]). 1006builtin(set_flag(_,_,_), [set_flag(++,++,++)]). 1007builtin(set_flag_body(_,_,_,_), [set_flag_body(++,++,++,++)]). 1008builtin(is_predicate(_), [is_predicate(++)]). 1009builtin(is_predicate_(_,_), [is_predicate_(++,++)]). 1010builtin(compile_term(_), [compile_term(-)]). 1011builtin(compile_term_(_,_), [compile_term_(-,++)]). 1012builtin(statistics, [statistics]). 1013builtin(statistics(_,_), [statistics(++,++)]). 1014builtin(dynamic_body(_,_), [dynamic_body(++,++)]). 1015builtin(compare(_,_,_), [compare(++,-,-)]). 1016 1017builtin(error(_,_), [error(++,?)]). 1018builtin(substring(_,_,_), [substring(++,++,++)]). 1019builtin(pathname(_,_), [pathname(++,++)]). 1020builtin(pathname(_,_,_), [pathname(++,++,++)]). 1021builtin(suffix(_,_), [suffix(++,++)]). 1022builtin(exists(_), [exists(++)]). 1023 1024builtin(sort(X,Y), [sort(Z,Z)]) :- =(X,Y,Z0), =(+-,Z0,Z). 1025builtin(keysort(X,Y), [keysort(Z,Z)]) :- =(X,Y,Z0), =(+-,Z0,Z). 1026 1027builtin(length(_,_), [length(+-,++)]). 1028builtin(member(_,++), [member(++,++)]) :- !. 1029builtin(member(_,_), [member(?,+)]). 1030builtin(delete(_,++,_), [delete(++,++,++)]) :- !. 1031builtin(delete(_,_,_), [delete(?,+,+)]). 1032 1033% cprolog 1034builtin(prompt(_,_), [prompt(++,++)]). 1035builtin(see(_), [see(++)]). 1036builtin(seen, [seen]). 1037builtin(tell(_), [tell(++)]). 1038builtin(telling(_), [telling(++)]). 1039builtin(told(_), [told(++)]). 1040builtin(seeing(_), [seeing(++)]). 1041builtin(skip(_), [skip(++)]). 1042builtin(skip(_), [skip(++,++)]). 1043builtin(tab(_), [tab(++)]). 1044builtin(tab(_,_), [tab(++,++)]). 1045builtin(get0(_), [get0(++)]). 1046 1047 1048/*** to be reviewed 1049 1050:- import bound_arg_/4 from sepia_kernel. 1051 1052bi_mode(Call, Exit) :- 1053 functor(Call, F, N), 1054 functor(Exit, F, N), 1055 bi_mode(N, F/N, Call, Exit). 1056 1057bi_mode(0, _, _, _) :- !. 1058bi_mode(N, Pred, Call, Exit) :- 1059 N1 is N-1, 1060 arg(N, Call, CallArg), 1061 arg(N, Exit, ExitArg), 1062 ( 1063 is_predicate_body(Pred, source), 1064 bound_arg_(Pred, N, Binding, source) 1065 -> 1066 map_modes(Binding, ExitArg) 1067 ; 1068 ExitArg=CallArg 1069 ), 1070 bi_mode(N1, Pred, Call, Exit). 1071 1072map_modes(constant, ++). 1073map_modes(nonvar, +). 1074map_modes(ground, ++). 1075 1076***/ 1077 1078%----------------------------------------------------------------------- 1079 1080?- nl, 1081writeln("Mode Analysis"), nl, 1082writeln("1. read a source file (e.g. src.pl): read_source(src)."), 1083writeln("2. analyze a call pattern (e.g. p/2): analyze(p(++,-))"), 1084writeln("This will print the resulting mode declarations"), 1085writeln("Valid modes are ++ + - ? +- and -+"), nl, 1086writeln("To collect builtin call modes, use setval(collect_builtin_modes, on)@modes."), nl. 1087 1088 1089 1090