1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2% Copyright (C) 1990 Peter Van Roy and Regents of the University of California.
3% All rights reserved.  This program may be freely used and modified for
4% non-commercial purposes provided this copyright notice is kept unchanged.
5% Written by Peter Van Roy as a part of the Aquarius project.
6%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7
8% Benchmark based on the Aquarius compiler flow analyzer version 1.
9% This program does a dataflow analysis of quicksort using abstract
10% interpretation.  The lattice has two useful values: uninit and ground.
11% Analysis takes three passes (it prints three 'x' characters).
12% Builtins used: compare/3, arg/3, functor/3, sort/2, keysort/2, ==/2, \==/2.
13
14top :- main(_).
15% main :- main(Table), write(Table), nl.
16
17main(Table) :-
18	analyze_strees(
19	  [stree(main/0,
20	      (main:-
21	       (qsort([1,2],L,[]),true
22               ;fail
23	       )),
24              (main:-true),[],1),
25	   stree(qsort/3,
26	      (qsort(U,P,Q):-
27	       (U=[N|O],part(O,N,R,S),qsort(S,T,Q),qsort(R,P,[N|T]),true
28	       ;U=[],Q=P,true
29	       ;fail
30	       )),
31	      (qsort(_,_,_):-true),[],1),
32	   stree(part/4,
33	      (part(W,X,Y,Z):-
34	       ('$cut_load'(A1),'$cut_part/4_1'(W,X,Y,Z,A1),true
35	       ;fail
36	       )),
37	      (part(_,_,_,_):-true),
38	   [stree('$cut_part/4_1'/5,
39	      ('$cut_part/4_1'(I1,E1,F1,G1,H1):-
40	       (I1=[C1|D1],'$fac_$cut_part/4_1/5_2'(D1,E1,F1,G1,H1,C1),true
41	       ;I1=[],F1=[],G1=[],true
42	       ;fail
43	       )),
44	      ('$cut_part/4_1'(_,_,_,_,_):-true),
45	    [stree('$fac_$cut_part/4_1/5_2'/6,
46	      ('$fac_$cut_part/4_1/5_2'(K1,L1,Q1,O1,P1,M1):-
47	       (Q1=[M1|N1],M1=<L1,'$cut_shallow'(P1),part(K1,L1,N1,O1),true
48	       ;O1=[M1|R1],part(K1,L1,Q1,R1),true
49	       ;fail
50	       )),
51	      ('$fac_$cut_part/4_1/5_2'(_,_,_,_,_,_):-true),[],1)
52	    ],1)
53	   ],1)
54	  ], Table).
55
56analyze_strees(Strees, OutTable) :-
57	init_strees(Strees, _, Table),
58	seal(Table),
59	analyze_closure(Strees, Table, OutTable).
60
61% Repeat traversal step until there are no more changes:
62analyze_closure(Strees, InTable, OutTable) :-
63	traverse_strees(Strees, InTable, MidTable, 0, Changes),
64	% Mark an analysis pass:
65	% put("x"), nl,
66	analyze_closure(Strees, MidTable, OutTable, Changes).
67
68analyze_closure(Strees, InTable, InTable, N) :- N=<0, !.
69analyze_closure(Strees, InTable, OutTable, N) :- N>0, !,
70	analyze_closure(Strees, InTable, OutTable).
71
72%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73
74% Initialize the table of call lattice values:
75
76init_strees([],_4,_4) :-
77   true.
78init_strees([_12|_13],_4,_5) :-
79   _12=stree(_14,(_15:-_16),_17,_18,_19),
80   bottom_call(_14,_20),
81   table_command(get(_14,_20),_4,_23),
82   init_disj(_16,_23,_24),
83   init_strees(_18,_24,_25),
84   init_strees(_13,_25,_5),
85   true.
86
87init_conj(true,_4,_4) :-
88   true.
89init_conj((_12,_13),_4,_5) :-
90   init_goal(_12,_4,_16),
91   init_conj(_13,_16,_5),
92   true.
93
94init_disj(fail,_4,_4) :-
95   true.
96init_disj((_12;_13),_4,_5) :-
97   init_conj(_12,_4,_16),
98   init_disj(_13,_16,_5),
99   true.
100
101init_goal(_3,_4,_5) :-
102   call_p(_3),
103   !,
104   functor(_3,_12,_13),
105   bottom_call(_12/_13,_14),
106   table_command(get(_12/_13,_14),_4,_5),
107   true.
108init_goal(_3,_4,_4) :-
109   unify_p(_3),
110   !,
111   true.
112
113%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
114
115traverse_strees([],_4,_4,_6,_6) :-
116   true.
117traverse_strees([_14|_15],_4,_5,_6,_7) :-
118   _14=stree(_16,(_17:-_18),_19,_20,_21),
119   traverse_disj(_17,_18,_4,_26,_6,_27),
120   traverse_strees(_20,_26,_28,_27,_29),
121   traverse_strees(_15,_28,_5,_29,_7),
122   true.
123
124traverse_disj(_3,fail,_5,_5,_7,_7) :-
125   true.
126traverse_disj(_3,(_15;_16),_5,_6,_7,_8) :-
127   traverse_conj(_3,_15,_5,_22,_7,_23),
128   traverse_disj(_3,_16,_22,_6,_23,_8),
129   true.
130
131traverse_conj(_3,_4,_5,_6,_7,_8) :-
132   varset(_3,_24),
133   functor(_3,_15,_16),
134   table_command(get(_15/_16,_17),_5,_25),
135   get_entry_modes(uninit,_3,_17,_26),
136   get_entry_modes(ground,_3,_17,_27),
137   traverse_conj(_4,_25,_6,_7,_8,_27,_28,_26,_29,_24,_30),
138   true.
139
140traverse_conj(true,_4,_4,_6,_6,_8,_8,_10,_10,_12,_12) :-
141   true.
142traverse_conj((_20,_21),_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) :-
143   varset(_20,_32),
144   update_goal(_20,_32,_4,_33,_6,_34,_8,_35,_10,_36,_12,_37),
145   unionv(_32,_37,_38),
146   traverse_conj(_21,_33,_5,_34,_7,_35,_9,_36,_11,_38,_13),
147   true.
148
149update_goal(_3,_4,_5,_5,_7,_7,_9,_10,_11,_12,_13,_13) :-
150   split_unify(_3,_21,_27),
151   var(_21),
152   nonvar(_27),
153   varset(_27,_28),
154   subsetv(_28,_9),
155   !,
156   set_command(add(_21),_9,_10),
157   set_command(sub(_21),_11,_12),
158   true.
159update_goal(_3,_4,_5,_5,_7,_7,_9,_9,_11,_12,_13,_13) :-
160   split_unify(_3,_21,_30),
161   var(_21),
162   nonvar(_30),
163   inv(_21,_11),
164   !,
165   diffv(_4,_13,_31),
166   diffv(_31,_9,_22),
167   set_command(add_set(_22),_11,_32),
168   set_command(sub(_21),_32,_33),
169   intersectv(_4,_13,_23),
170   set_command(sub_set(_23),_33,_12),
171   true.
172update_goal(_3,_4,_5,_5,_7,_7,_9,_10,_11,_12,_13,_13) :-
173   split_unify(_3,_27,_28),
174   var(_27),
175   inv(_27,_9),
176   !,
177   set_command(add_set(_4),_9,_10),
178   set_command(sub_set(_4),_11,_12),
179   true.
180update_goal(_3,_4,_5,_5,_7,_7,_9,_9,_11,_12,_13,_13) :-
181   unify_p(_3),
182   !,
183   set_command(sub_set(_4),_11,_12),
184   true.
185update_goal(_3,_4,_5,_6,_7,_8,_9,_9,_11,_12,_13,_13) :-
186   call_p(_3),
187   !,
188   goal_dupset(_3,_33),
189   var_args(_3,_34),
190   functor(_3,_22,_23),
191   functor(_35,_22,_23),
192   create_new_call(1,_23,_9,_34,_33,_11,_13,_3,_35),
193   update_table(_22/_23,_35,_5,_6,_7,_8),
194   set_command(sub_set(_4),_11,_12),
195   true.
196
197update_table(_15/_16,_4,_5,_6,_7,_8) :-
198   table_command(get(_15/_16,_18),_5,_24),
199   lub_call(_18,_4,_19),
200   _18\==_19,
201   !,
202   table_command(set(_15/_16,_19),_24,_6),
203   _8 is _7+1,
204   true.
205update_table(_15/_16,_4,_5,_5,_7,_7).
206
207create_new_call(I, Ar, _, _, _, _, _, _, _) :- I>Ar, !.
208create_new_call(I, Ar, Gnd, VarArgs, DupVars, Uni, SoFar, Goal, Call) :-
209	I=<Ar,
210	!,
211	arg(I, Goal, X),
212	arg(I, Call, Y),
213	ground_flag(X, Gnd, Gf),
214	membership_flag(X, VarArgs, Vf),
215	membership_flag(X, DupVars, Df),
216	membership_flag(X, Uni, Uf),
217	membership_flag(X, SoFar, Sf),
218	create_argument(Gf, Vf, Df, Uf, Sf, Y),
219	I1 is I+1,
220	create_new_call(I1, Ar, Gnd, VarArgs, DupVars, Uni, SoFar, Goal, Call).
221
222%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
223
224% Lattice utilities:
225
226lub(unknown,       X,      X) :- !.
227lub(      X, unknown,      X) :- !.
228lub(    any,       _,    any) :- !.
229lub(      _,     any,    any) :- !.
230lub( uninit,  uninit, uninit) :- !.
231lub( ground,  ground, ground) :- !.
232lub( uninit,  ground,    any) :- !.
233lub( ground,  uninit,    any) :- !.
234
235bottom(unknown).
236
237create_argument(yes,   _,   _,   _,   _, ground) :- !. % Ground argument.
238create_argument( no, yes,  no, yes,   _, uninit) :- !. % Non-duplicated uninit.
239create_argument( no, yes,  no,   _,  no, uninit) :- !. % First occurrence.
240create_argument( no, yes,   _,  no, yes, any) :- !.    % Already initialized.
241create_argument( no, yes, yes,   _,   _, any) :- !.    % Duplicated argument.
242create_argument( no,  no,   _,   _,   _, any) :- !.    % Non-variable argument.
243
244lub_call(Call1, Call2, Lub) :-
245	functor(Call1, Na, Ar),
246	functor(Call2, Na, Ar),
247	functor(Lub, Na, Ar),
248	lub_call(1, Ar, Call1, Call2, Lub).
249
250lub_call(I, Ar, _, _, _) :- I>Ar, !.
251lub_call(I, Ar, Call1, Call2, Lub) :- I=<Ar, !,
252	arg(I, Call1, X1),
253	arg(I, Call2, X2),
254	arg(I, Lub, X),
255	lub(X1, X2, X),
256	I1 is I+1,
257	lub_call(I1, Ar, Call1, Call2, Lub).
258
259bottom_call(Na/Ar, Bottom) :-
260	functor(Bottom, Na, Ar),
261	bottom_call(1, Ar, Bottom).
262
263bottom_call(I, Ar, Bottom) :- I>Ar, !.
264bottom_call(I, Ar, Bottom) :- I=<Ar, !,
265	bottom(B),
266	arg(I, Bottom, B),
267	I1 is I+1,
268	bottom_call(I1, Ar, Bottom).
269
270lattice_modes_call(Na/Ar, Table, (Head:-Formula)) :-
271	functor(Head, Na, Ar),
272	get(Table, Na/Ar, Value),
273	lattice_modes_call(1, Ar, Value, Head, Formula, true).
274
275lattice_modes_call(I, Ar, _, _, Link, Link) :- I>Ar, !.
276lattice_modes_call(I, Ar, Value, Head, Formula, Link) :- I=<Ar, !,
277	arg(I, Value, T),
278	arg(I, Head, X),
279	lattice_modes_arg(T, X, Formula, Mid),
280	I1 is I+1,
281	lattice_modes_call(I1, Ar, Value, Head, Mid, Link).
282
283lattice_modes_arg(uninit, X, (uninit(X),Link), Link) :- !.
284lattice_modes_arg(ground, X, (ground(X),Link), Link) :- !.
285lattice_modes_arg( Other, X, Link, Link).
286
287%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
288
289% Table utilities:
290
291% This code implements a mutable array, represented as a binary tree.
292
293% Access a value in logarithmic time and constant space:
294% This predicate can be used to create the array incrementally.
295get(node(N,W,L,R), I, V) :- get(N, W, L, R, I, V).
296
297get(N, V, _, _, I, V) :- I=N, !.
298get(N, _, L, R, I, V) :-
299	compare(Order, I, N),
300	get(Order, I, V, L, R).
301
302get(<, I, V, L, _) :- get(L, I, V).
303get(>, I, V, _, R) :- get(R, I, V).
304
305set(leaf,          I, V, node(I,V,leaf,leaf)).
306set(node(N,W,L,R), I, V, node(N,NW,NL,NR)) :-
307	compare(Order, I, N),
308	set_2(Order, I, V, W, L, R, NW, NL, NR).
309
310set_2(<, I, V, W, L, R, W, NL, R) :- set(L, I, V, NL).
311set_2(=, I, V, _, L, R, V, L, R).
312set_2(>, I, V, W, L, R, W, L, NR) :- set(R, I, V, NR).
313
314% Prevent any further insertions in the array:
315seal(leaf).
316seal(node(_,_,L,R)) :- seal(L), seal(R).
317
318%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
319
320% General utilities:
321
322membership_flag(X, Set, yes) :- inv(X, Set), !.
323membership_flag(X, Set,  no).
324
325ground_flag(X, Ground, yes) :- varset(X, Set), subsetv(Set, Ground), !.
326ground_flag(X, Ground,  no).
327
328get_entry_modes(Type, Head, Value, TypeSet) :-
329	functor(Head, Na, Ar),
330	get_entry_modes(Type, 1, Ar, Head, Value, Bag),
331	sort(Bag, TypeSet).
332
333get_entry_modes(_, I, Ar, _, _, []) :- I>Ar, !.
334get_entry_modes(T, I, Ar, Head, Value, [X|Bag]) :- I=<Ar, arg(I, Value, T), !,
335	arg(I, Head, X),
336	I1 is I+1,
337	get_entry_modes(T, I1, Ar, Head, Value, Bag).
338get_entry_modes(T, I, Ar, Head, Value, Bag) :- I=<Ar, !,
339	I1 is I+1,
340	get_entry_modes(T, I1, Ar, Head, Value, Bag).
341
342var_args(Goal, Set) :-
343	functor(Goal, _, Ar),
344	filter_vars(Ar, Goal, Bag),
345	sort(Bag, Set).
346
347filter_vars(Ar, Goal, Vs) :- filter_vars(Ar, Goal, Vs, []).
348
349filter_vars(N, Goal) --> {N=<0}, !.
350filter_vars(N, Goal) --> {N>0}, !,
351	{arg(N, Goal, V)},
352	filter_vars_arg(N, Goal, V).
353
354filter_vars_arg(N, Goal, V) --> {var(V)}, !, [V],
355	{N1 is N-1},
356	filter_vars(N1, Goal).
357filter_vars_arg(N, Goal, V) --> {nonvar(V)}, !,
358	{N1 is N-1},
359	filter_vars(N1, Goal).
360
361goal_dupset(Goal, DupSet) :-
362	goal_dupset_varbag(Goal, DupSet, _).
363
364goal_dupset_varset(Goal, DupSet, VarSet) :-
365	goal_dupset_varbag(Goal, DupSet, VarBag),
366	sort(VarBag, VarSet).
367
368goal_dupset_varbag(Goal, DupSet, VarBag) :-
369	varbag(Goal, VarBag),
370	make_key(VarBag, KeyBag),
371	keysort(KeyBag, KeySet),
372	filter_dups(KeySet, DupSet).
373
374make_key([], []).
375make_key([V|Bag], [V-dummy|KeyBag]) :- make_key(Bag, KeyBag).
376
377filter_dups(KeySet, Set) :- filter_dups(KeySet, Set, []).
378
379filter_dups([]) --> !.
380filter_dups([V1-_,V2-_,V3-_|KeySet]) --> {V1==V2,V2==V3}, !,
381	filter_dups([V2-_,V3-_|KeySet]).
382filter_dups([V1-_,V2-_|KeySet]) --> {V1==V2}, !,
383	[V1], filter_dups(KeySet).
384filter_dups([V1-_|KeySet]) --> !,
385	filter_dups(KeySet).
386
387%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
388
389% Low-level utilities:
390
391set_command(sub(X), In, Out) :- diffv(In, [X], Out).
392set_command(add(X), In, Out) :- includev(X, In, Out).
393set_command(sub_set(X), In, Out) :- diffv(In, X, Out).
394set_command(add_set(X), In, Out) :- unionv(X, In, Out).
395
396table_command(get(I,Val), In,  In) :- get(In, I, Val).
397table_command(set(I,Val), In, Out) :- set(In, I, Val, Out).
398
399% Set utilities inspired by R. O'Keefe in Practical Prolog:
400inv(A, [B|S]) :-
401	compare(Order, A, B),
402	inv_2(Order, A, S).
403
404inv_2(=, _, _).
405inv_2(>, A, S) :- inv(A, S).
406
407intersectv([], _, []).
408intersectv([A|S1], S2, S) :- intersectv_2(S2, A, S1, S).
409
410intersectv_2([], A, S1, []).
411intersectv_2([B|S2], A, S1, S) :-
412	compare(Order, A, B),
413	intersectv_3(Order, A, S1, B, S2, S).
414
415intersectv_3(<, A, S1, B, S2,     S) :- intersectv_2(S1, B, S2, S).
416intersectv_3(=, A, S1, _, S2, [A|S]) :- intersectv(S1, S2, S).
417intersectv_3(>, A, S1, B, S2,     S) :- intersectv_2(S2, A, S1, S).
418
419diffv([], _, []).
420diffv([A|S1], S2, S) :- diffv_2(S2, A, S1, S).
421
422diffv_2([], A, S1, [A]).
423diffv_2([B|S2], A, S1, S) :-
424	compare(Order, A, B),
425	diffv_3(Order, A, S1, B, S2, S).
426
427diffv_3(<, A, S1, B, S2, [A|S]) :- diffv(S1, [B|S2], S).
428diffv_3(=, A, S1, _, S2,     S) :- diffv(S1, S2, S).
429diffv_3(>, A, S1, _, S2,     S) :- diffv_2(S2, A, S1, S).
430
431unionv([], S2, S2).
432unionv([A|S1], S2, S) :- unionv_2(S2, A, S1, S).
433
434unionv_2([], A, S1, [A|S1]).
435unionv_2([B|S2], A, S1, S) :-
436	compare(Order, A, B),
437	unionv_3(Order, A, S1, B, S2, S).
438
439unionv_3(<, A, S1, B, S2, [A|S]) :- unionv_2(S1, B, S2, S).
440unionv_3(=, A, S1, _, S2, [A|S]) :- unionv(S1, S2, S).
441unionv_3(>, A, S1, B, S2, [B|S]) :- unionv_2(S2, A, S1, S).
442
443includev(A, S1, S) :- includev_2(S1, A, S).
444
445includev_2([], A, [A]).
446includev_2([B|S1], A, S) :-
447	compare(Order, A, B),
448	includev_3(Order, A, B, S1, S).
449
450includev_3(<, A, B, S1, [A,B|S1]).
451includev_3(=, _, B, S1, [B|S1]).
452includev_3(>, A, B, S1, [B|S]) :- includev_2(S1, A, S).
453
454subsetv([], _).
455subsetv([A|S1], [B|S2]) :-
456	compare(Order, A, B),
457	subsetv_2(Order, A, S1, S2).
458
459subsetv_2(=, A, S1, S2) :- subsetv(S1, S2).
460subsetv_2(>, A, S1, S2) :- subsetv([A|S1], S2).
461
462varset(Term, VarSet) :- varbag(Term, VB), sort(VB, VarSet).
463varbag(Term, VarBag) :- varbag(Term, VarBag, []).
464
465varbag(Var) --> {var(Var)}, !, [Var].
466varbag(Str) --> {nonvar(Str), !, functor(Str,_,Arity)}, varbag(Str, 1, Arity).
467
468varbag(_Str, N, Arity) --> {N>Arity}, !.
469varbag(Str, N, Arity) --> {N=<Arity}, !,
470        {arg(N, Str, Arg)}, varbag(Arg),
471        {N1 is N+1},
472        varbag(Str, N1, Arity).
473
474unify_p(_=_).
475
476call_p(G) :- \+unify_p(G).
477
478split_unify(X=Y, X, Y).
479split_unify(Y=X, X, Y).
480
481%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
482