1: %\documentclass[twoside,12pt]{article} 

2: 

3: 

4: %\documentclass{sig-alternate}

5: 

6: \documentclass{llncs}

7: %\usepackage{times}

8: \usepackage{eepic,latexsym,amssymb}

9: \usepackage[all]{xy}

10: \usepackage{fancybox,epic}

11: 

12: \usepackage{listings}

13: \lstset{captionpos=b,

14:         %frame=tb,

15:         basicstyle=\scriptsize\ttfamily,

16:         showstringspaces=false,

17:         keepspaces=true}

18: 

19: %% \setlength{\textwidth}{13.5cm}

20: %%  \setlength{\textheight}{21.5cm}

21: %%  \setlength{\topmargin}{-1cm}

22: %%  \setlength{\oddsidemargin}{1.5cm}

23: %%  \setlength{\evensidemargin}{1.5cm}

24: %%  \setlength{\marginparwidth}{0.25cm}

25: %%  \setlength{\marginparsep}{0.25cm

26: 

27: %% \renewcommand{\arraystretch}{0.83}

28: % \renewcommand{\baselinestretch}{0.97}

29: 

30: %% \setlength{\textwidth}{13cm}

31: %% \setlength{\textheight}{21cm}

32: %% %\setlength{\topmargin}{-1cm}

33: %%  \setlength{\oddsidemargin}{1.48cm}

34: %%  \setlength{\evensidemargin}{1.48cm}

35: %% \setlength{\marginparwidth}{0.25cm}

36: %% \setlength{\marginparsep}{0.25cm}

37: %% \newtheorem{theorem}{Theorem}[section]

38: %% \newtheorem{lemma}[theorem]{Lemma}

39: %% \newtheorem{proposition}[theorem]{Proposition}

40: %% \newtheorem{corollary}[theorem]{Corollary}

41: 

42: %% \newtheorem{definition}[theorem]{Definition}

43: %% \newtheorem{example}[theorem]{Example}

44: %% \newtheorem{remark}[theorem]{Remark}

45: 

46: \renewcommand{\topfraction}{0.90}

47: %% \renewcommand{\textfraction}{0.10}

48: %% \renewcommand{\floatpagefraction}{0.90}

49: \renewcommand{\textfraction}{0}

50: \renewcommand{\floatpagefraction}{1}

51: 

52: 

53: \newcommand{\sizeinprogram}[0]{small}

54: 

55: %% from DISCIPL

56: \newcommand{\kbd}[1]{\mbox{\tt #1}}

57: \newcommand{\nt}[1]{\mbox{\it #1}}

58: 

59: %% from LOPSTR99

60: \newcommand{\Q}{\mbox{$\cal Q$}}

61: 

62: \def\dep#1{\langle{#1}\rangle}

63: 

64: %\def\tuple#1{\langle{#1}\rangle}

65: 

66: %% from LOPSTR04

67: \newcommand{\selatpar}[1]{A_{R#1}}

68: \newcommand{\selat}{A_{R}}

69: \newcommand{\select}{\cR}

70: \newcommand{\sidenote}[1]{\marginpar{#1}}

71: \newcommand{\lub}{\sqsubseteq}

72: \newcommand{\cR}{{\cal R}}

73: \newcommand{\cS}{{\cal S}}

74: \newcommand{\cU}{{\cal U}}

75: \newcommand{\tuple}[2]{#1:#2}

76: 

77: %% NEW

78: \newcommand{\calls}{\mathit{calls}}

79: \newcommand{\success}{\mathit{success}}

80: \newcommand{\ciao}{{\tt Ciao}}

81: \newcommand{\ciaopp}{{\tt CiaoPP}}

82: \newcommand{\trismall}{{\tiny \vartriangleright}}

83: \newcommand{\Proof}{\mathit{Proof}}

84: \newcommand{\andT}{{\sc And}}

85: \newcommand{\orN}{{\sc Or}}

86: \newcommand{\embeds}{\trianglelefteq}

87: 

88: % for semantics

89: \newcommand{\lsem}{\mbox{$\lbrack\hspace{-0.3ex}\lbrack$}}

90: \newcommand{\rsem}{\mbox{$\rbrack\hspace{-0.3ex}\rbrack$}}

91: \newcommand{\sem}[1]{\lsem #1 \rsem}

92: 

93: \newcommand{\mycomment}[1]{*** \textbf{#1} ***}

94: 

95: \newcommand{\pr}[1]{\texttt{#1}}

96: 

97: %% Nudge LaTeX into behaving wrt tables

98: \renewcommand{\topfraction}{0.95}

99: \renewcommand{\textfraction}{0.05}

100: \renewcommand{\floatpagefraction}{0.95}

101: %\newcommand{\sizeinfigure}{\small} % 10pt

102: %\newcommand{\sizeinfigure}{\footnotesize} %11pt

103: 

104: 

105: \newcommand{\sizeintable}{\normalsize} % 10pt

106: \long\def\comment#1{}

107: 

108: %% from TOPLAS2000

109: \newcommand{\CP}{\mbox{\it CP}}

110: \newcommand{\defff}{\mathit{Def}}

111: \newcommand{\AP}{\mbox{\it AP}}

112: 

113: %% Elvira's macros

114: \newcommand{\lto}{\leftarrow}

115: \newcommand{\Def}{\mathit{Def}}

116: 

117: \newcommand{\widening}{\nabla}

118: %% From SAS'96

119: \newcommand{\sizeinfigure}{\small} % 10pt

120: %\newcommand{\sizeinfigure}{\footnotesize} %11pt

121: 

122: 

123: % GP added

124: \newcommand{\SD}{\mbox{\it SD}}

125: 

126: \usepackage{algorithm}

127: %\usepackage{algorithmicx}

128: \usepackage[noend]{algpseudocode}

129: 

130: \newcommand{\algorithmicinput}{\textbf{Input:~}}

131: \newcommand{\algorithmicoutput}{\textbf{Output:~}}

132: \newcommand{\algorithmicglobal}{\textbf{Global:~}}

133: 

134: %% \newcommand{\acombine}{\mbox{\sf Acombine}}

135: \newcommand{\arestrict}{\mbox{\sf Arestrict}}

136: \newcommand{\aextend}{\mbox{\sf Aextend}}

137: \newcommand{\aunif}{\mbox{\sf Aunif}}

138: \newcommand{\aconj}{\mbox{\sf Aconj}}

139: \newcommand{\alub}{\mbox{\sf Alub}}

140: \newcommand{\acalltoentry}{\mbox{\sf Atranslate}}

141: %\newcommand{\widensuccess}{\mbox{\sf Widen\_Success}}

142: \newcommand{\removeuselesscalls}{\mbox{\sc remove\_useless\_calls}}

143: %\newcommand{\removeuselessspecs}{\mbox{\sf remove\_useless\_specs}}

144: 

145: \newcommand{\at}{\mbox{{$\cal AT$}}}

146: \newcommand{\dt}{\mbox{{$\cal DT$}}}

147: \newcommand{\gt}{\mbox{{$\cal GT$}}}

148: \newcommand{\st}{\mbox{{$\cal ST$}}}

149: \newcommand{\emptytable}{\mbox{\sf Create\_Table}}

150: \newcommand{\store}{\mbox{\sf Insert}}

151: \newcommand{\isin}{\mbox{\sf IsIn}}

152: \newcommand{\consult}{\mbox{\sf Look\_up}}

153: 

154: \newcommand{\newpred}{\mbox{\sf new\_filter}}

155: \newcommand{\renameheads}{\mbox{\sf rename\_heads}}

156: \newcommand{\ren}{\mbox{\sf ren}}

157: \newcommand{\getbody}{\mbox{\sf get\_body}}

158: \newcommand{\member}{\mbox{\sf Member}}

159: \newcommand{\delete}{\mbox{\sf Delete}}

160: 

161: \usepackage{listings}

162: \lstset{captionpos=b,

163:         %frame=tb,

164: %        basicstyle=\scriptsize\ttfamily,

165:         showstringspaces=false,

166:         keepspaces=true}

167: 

168: \newcommand{\aabstraction}{\mbox{\it AGeneralize}}

169: \newcommand{\aunfold}{\mbox{\it AUnfold}}

170: \newcommand{\abstraction}{\mbox{\it Generalize}}

171: \newcommand{\unfold}{\mbox{\it Unfold}}

172: 

173: \newcommand{\widencall}{\mbox{\it Widen\_Call}}

174: 

175: 

176: %% \newtheorem{theorem}{Theorem}[section]

177: %% \newtheorem{definition}[theorem]{Definition}

178: %% \newtheorem{lemma}[theorem]{Lemma}

179: %% \newtheorem{example}[theorem]{Example}

180: %% \newtheorem{algorithm}[theorem]{Algorithm}

181: %% \newtheorem{prop}[theorem]{Proposition}

182: %%%%%%%%%%%%%%%%

183: \newcommand{\bibpath}{/home/clip/bibtex/clip}

184: \newcommand{\short}[1]{}

185: %

186: %\renewcommand{\arraystretch}{0.83}

187: %\r%enewcommand{\baselinestretch}{0.96}

188: 

189: \newcommand{\secbeg}{\vspace*{0mm}}

190: \newcommand{\secend}{\vspace*{0mm}}

191: 

192: %\date{\today}

193: 

194: %\tableofcontents

195: %\begin{document} 

196: 

197: %% \markboth{WLPE 2005}{Generic Framework for Analysis and Specialization

198: %%   of Logic Programs} 

199: \title{A Generic Framework for the Analysis and Specialization of

200:   Logic Programs}

201: \author{Germ\'{a}n Puebla\inst{1} \and Elvira Albert\inst{2}

202:  \and Manuel Hermenegildo\inst{1,3}

203: }

204: 

205: \institute{

206: School of Computer Science, Technical U.~of Madrid, 

207: \email{\{german,herme\}@fi.upm.es}

208: \and

209: School of Computer Science, Complutense U.~of  Madrid,

210: \email{elvira@sip.ucm.es}

211: \and

212: Depts. of Comp.~Sci.~and El.~and Comp.~Eng., U. of  New Mexico,

213: \email{herme@unm.edu}

214: } 

215: 

216: \begin{document}

217: \maketitle

218: 

219:  \pagestyle{myheadings}  \markboth{WLPE 2005}{Generic Framework for Analysis and Specialization

220:  of Logic Programs} 

221: 

222: %% \footnote{In A. Serebrenik and S. Mu{\~n}oz-Hern{\'a}ndez (editors), 

223: %% Proceedings of the 15th Workshop on Logic-based methods in Programming 

224: %% Environments, October 2005, Spain. COmputer Research Repository 

225: %% (http://www.acm.org/corr/), cs.SE/0508111; whole proceedings: 

226: %% cs.PL/0508078.}} 

227: 

228: \begin{abstract}

229:    

230: %Partial deduction is a program transformation technique for

231: %specializing logic programs w.r.t.\ parts of their input (and is thus

232: %also called program specialization).  Abstract interpretation has long

233: %been used for static analysis and optimization of (logic) programs.

234: 

235: The relationship between abstract interpretation and partial deduction

236: has received considerable attention and (partial) integrations have

237: been proposed starting from both the partial deduction and abstract

238: interpretation perspectives.

239: %

240: In this work we present what we argue is the first fully described

241: generic algorithm for efficient and precise integration of abstract

242: interpretation and partial deduction.

243: % from an abstract interpretation perspective.

244: %

245: Taking as starting point state-of-the-art algorithms for

246: context-sensitive, polyvariant abstract interpretation and (abstract)

247: partial deduction, we present an algorithm which combines the best of

248: both worlds. Key ingredients include the accurate success propagation

249: inherent to 

250: %context-sensitive 

251: abstract interpretation and the powerful

252: program transformations achievable by partial deduction.

253: %% Interestingly, the central idea in this novel framework

254: %% is simple:

255: %% %

256: %% the abstract interpretation algorithm is modified in such a way that

257: In our algorithm, the calls which appear 

258: %dynamically 

259: in the analysis graph are not analyzed w.r.t.~the original definition

260: of the procedure

261: % in the original program 

262: but w.r.t.

263: %~possibly

264: \emph{specialized definitions} of these procedures.  Such specialized

265: definitions are obtained by applying

266: %powerful techniques for on-line program

267: %specialization, including 

268: both unfolding and abstract executability.

269: %

270: Our framework 

271: %and algorithm are 

272: is parametric w.r.t.~different control strategies and abstract

273: domains. Different combinations of such parameters correspond to

274: existing algorithms for program analysis and specialization.

275: Simultaneously, our approach opens the door to the efficient

276: computation of strictly more precise results than those achievable by

277: each of the individual techniques.

278: %

279: %

280: % 

281: \short{On one hand, the algorithm computes a precise

282: description of the behaviour of the (residual) program.

283: %

284: On the other hand, the specialized definitions computed during the

285: execution of the algorithm provide a highly specialized partial

286: evaluation of the program.

287: %The new

288: %features of the framework introduce non-trivial design, control, and

289: %termination issues, which are studied in the paper.

290: %

291: } 

292: %

293: The algorithm is now one of the key components of the \ciaopp\ 

294: analysis and specialization system.

295: 

296: %% \vspace*{2mm}

297: %% \noindent

298: %% \textbf{Keywords:}  Abstract Interpretation, Partial Deduction,

299: %% Program Analysis and Optimization. 

300: \end{abstract}

301: 

302: \vspace{-0.5cm}

303: \section{Introduction and Motivation}

304: \secend

305:  \label{sec:motivation}

306:  

307: \short{

308:  \input motivation

309:  

310: \section{Running Example}

311: \label{sec:running-example}

312: } %% short

313: 

314: %\input simple-intro

315: 

316: 

317: The relationship between abstract interpretation~\cite{Cousot77-short}

318: and partial evaluation~\cite{pevalbook93} has received considerable

319: attention (see for example

320: \short{pe-in-plai-ws-short,}

321: \cite{gallag88,gallagher:wsa92,Consel-Koo:toplas93,LeuschelDeSchreye:PLILP96-short,jones-pe-ai97,leuschel-jicslp98,spec-jlp-short,pe-in-plai-pepm99-short,Gallagher-Peralta-HOSC,leuschel-gruner-loprstr2001-short,Cousot02-short,spec-inv-pepm03-short,leuschel04:Toplas}

322: and their references).

323: %

324: In order to motivate and illustrate our proposal for an integration of

325: abstract interpretation and partial evaluation, we use the running

326: example of Fig.~\ref{lst:running-ex}. It is a simple \ciao \short{

327:   \ciao~\cite{ciao-manual-1.10-short}

328: } %% short

329: program which uses Peano's arithmetic.\footnote{Rules are written with a unique

330: subscript attached to the head atom (the rule number), and a dual

331: subscript (rule number, body position) attached to each body literal.

332: %,

333: %e.g., $ H_k :- B_{k,1}, \ldots, B_{k,n_k} $ 

334: %where $B_{k,i}$

335: %is a subscripted atom.

336: We sometimes use this notation for denoting calls to atoms as well.}

337: We use the \ciao\ assertion

338: language %~\cite{assert-lang-disciplbook-short} 

339: in order to provide

340: precise descriptions on the initial call patterns. In our case, the

341: \texttt{entry} declaration is used to inform that all calls to the

342: only exported predicate (i.e., \texttt{main/2}) will always be of the

343: form $\tt \leftarrow main(s(s(s(L))),R)$ with $\tt L$ ground and $\tt

344: R$ a variable.

345: %

346: The predicate \texttt{main/2} performs two calls to

347: predicate \texttt{formula/2}, which contains mode tests \texttt{ground(X)}

348: and \texttt{var(W)} on its input arguments. A call

349: \texttt{formula(X,W)} returns $W=(X-2)\times 2$. 

350: %

351: Predicate \texttt{two/1} returns the natural number 2 in Peano's

352: arithmetic.

353: %

354: A call \texttt{minus(A,B,C)} returns $C=B-A$. However, if the result

355: becomes a negative number, $C$ is left as a free variable. This

356: indicates that the result is not valid.

357: %

358: In turn, a call \texttt{twice(A,B)} returns $B=A\times 2$. 

359: Prior to computing the result, this predicate checks whether $A$ is

360: valid, i.e., not a variable, and simply returns a variable otherwise.

361: 

362:  \begin{figure}[t]

363: %\begin{lstlisting}[caption={[Running Example] Running example},label={lst:running-ex}] 

364: {\footnotesize

365: %\begin{quote}

366: \tt

367: :- module(\_,[main/1],[assertions]).\\

368: :- entry main(s(s(s(L))),R) : (ground(L),var(R)).\\[0.6ex]

369: main$_{1}$(X,X2):- formula$_{1,1}$(X,X1), formula$_{1,2}$(X1,X2).\\[0.6ex]

370: formula$_{2}$(X,W):- ground$_{2,1}$(X),var$_{2,2}$(W),two$_{2,3}$(T),minus$_{2,4}$(T,X,X2),twice$_{2,5}$(X2,W).\\[0.6ex]

371: two$_{3}$(s(s(0))).\\[0.6ex]

372: minus$_{4}$(0,X,X).\\

373: minus$_{5}$(s(X),s(Y),R):- minus$_{5,1}$(X,Y,R).\\

374: minus$_{6}$(s(\_X),0,\_R).\\[0.6ex]

375: twice$_{7}$(X,\_Y):- var$_{7,1}$(X).\\

376: twice$_{8}$(X,Y):- ground$_{8,1}$(X), tw$_{8,2}$(X,Y).\\[0.6ex]

377: tw$_{9}$(0,0).\\

378: tw$_{10}$(s(X),s(s(NX))):- tw$_{10,1}$(X,NX).

379: %\end{quote}

380: }

381: %\end{lstlisting}

382: %\vspace*{-0.3cm}

383: \caption{Running Example}

384: \label{lst:running-ex}

385: %\vspace*{-0.6cm}

386: \end{figure}

387: 

388: %% This example illustrates several ideas important in the analysis and

389: %% specialization framework we propose in this paper. (1) The need of

390: %% using abstract information in order to abstractly execute certain

391: %% literals. (2) The need of performing unfolding steps in order to prune

392: %% away useless branches, which will result in improved success

393: %% information. (3) The need of propagating (abstract) success

394: %% information, performing fixpoint computations when needed. (4) The

395: %% usefulness of having information on non \emph{downwards-closed}

396: %% properties.

397: 

398: By observing the behaviour of the program it can be seen that for

399: initial queries satisfying the \texttt{entry} declaration, all calls

400: to the tests \texttt{ground$_{2,1}$(X)} and \texttt{var$_{2,2}$(W)}

401: will definitely succeed, even if we do not know the concrete values of

402: variable $\tt L$ at compile time.  Also, the calls to

403: \texttt{ground$_{8,1}$(X)} will succeed, while the calls to

404: \texttt{var$_{7,1}$(X)} will fail. This shows the benefits of (1)

405: \emph{exploiting abstract information in order to abstractly execute

406:   certain atoms, which in turn may allow unfolding of other atoms}.

407: However, the use of an abstract domain which captures groundness and

408: freeness information will in general not be sufficient to determine

409: that in the second execution of \texttt{formula/2} the tests

410: \texttt{ground$_{2,1}$(X)} and \texttt{var$_{2,2}$(W)} will also

411: succeed. The reason is that, on success of

412: \texttt{minus$_{2,4}$(T,X,X2)}, $\tt X2$ cannot be guaranteed to be

413: ground since \texttt{minus$_6$/3} succeeds with a

414: free variable on its third argument position. It can be observed,

415: however, that for all calls to \texttt{minus/3} in executions

416: described by the \texttt{entry} declaration, such third clause for

417: \texttt{minus/3} is useless. It will never contribute to a success of

418: \texttt{minus/3} since such predicate is always called with a value

419: greater than zero on

420: its second argument.

421: %

422: Unfolding can make this explicit by fully unfolding calls to

423: \texttt{minus/3} since they are sufficiently instantiated (and as a

424: result the ``dangerous'' third clause is disregarded).  It allows

425: concluding that in our particular context, all calls to

426: \texttt{minus/3} succeed with a ground third argument.

427: %% This in

428: %% turn will improve analysis the analysis results for \texttt{twice/2},

429: %% which always succeed with both arguments being

430: %% ground.  

431: This shows the importance of (2) \emph{performing unfolding steps in

432:   order to prune away useless branches, which will result in improved

433:   success information}. By the time execution reaches

434: \texttt{twice$_{2,5}$(X2,W)}, we hopefully know that $\tt X2$ is

435: ground.  In order to determine that, upon success of

436: \texttt{twice$_{2,5}$(X2,W)} (and thus on success of

437: \texttt{formula$_{1,1}$(X,W)}), $\tt W$ is ground, we need to perform

438: a fixpoint computation. Since, for example, the success substitution

439: for \texttt{formula$_{1,1}$(X,X1)} is indeed the call substitution for

440: \texttt{formula$_{1,2}$(X1,X2)}, the success of the second test

441: \texttt{ground$_{2,1}$(X)} (i.e., the one reachable from

442: \texttt{formula$_{1,2}$(X1,X2)}) cannot be established unless we

443: propagate success substitutions. This illustrates the importance of

444: (3) \emph{propagating (abstract) success information, performing

445:   fixpoint computations when needed, which simultaneously will result

446:   in an improved unfolding}. Finally, whenever we call

447: \texttt{formula(X,W)}, $\tt W$ is a variable, a property which cannot be

448: captured if we restrict ourselves to downwards-closed domains. This

449: indicates (4) \emph{the usefulness of having information on non

450:   \emph{downwards-closed} properties}.

451: 

452: Throughout the paper we show that the framework we propose is able to

453: eliminate all calls to mode tests \texttt{ground/1} and

454: \texttt{var/1}, and predicates \texttt{two/1} and \texttt{minus/3} are

455: both fully unfolded and no longer appear in the residual code.

456: %

457: We have used \emph{sharing--freeness} as abstract domain instead of

458: one based on, say regular types, for two reasons.\footnote{The values

459:   for the rest of parameters are: \aabstraction\ and \aunfold\ rules

460:   based on \emph{homeomorphic

461:     embedding}~\cite{LeuschelBruynooghe:TPLP02}, and the identity

462:   function as \widencall\ function.}  First, to illustrate how

463: non-downwards closed information, including freeness and definite

464: independence, can be correctly exploited by our algorithm

465: %both at the local and global level 

466: in order to 

467: %analyze and 

468: optimize the

469: program, and second, to show how unfolding can be of great use in

470: order to improve the accuracy of analyses apparently unrelated to

471: partial deduction, such as the classical \emph{sharing--freeness}.

472: %

473: \begin{example}\label{ex:sp}

474:   The results obtained by \ciaopp---which implements abstract

475:   interpretation with specialized definitions---are both the following

476:   specialized code and an accurate analysis for such

477:   program (rules are renamed using the prefix $\tt sp$).

478: %

479: %\vspace{-0.1cm}

480:   {\footnotesize

481: \begin{quote}\tt

482: sp\_main${}_1$(s(s(s(0))),0).\\

483: sp\_main${}_2$(s(s(s(s(B)))),A) :- sp\_tw${}_{2,1}$(B,C),

484: sp\_formula${}_{2,2}$(C,A).\\[0.6ex]

485: sp\_tw${}_2$(0,0).\\

486: sp\_tw${}_3$(s(A),s(s(B))) :-  sp\_tw${}_{3,1}$(A,B).\\[0.6ex]

487: sp\_formula${}_4$(0,s(s(s(s(0))))).\\

488: sp\_formula${}_5$(s(A),s(s(s(s(s(s(B))))))) :-  sp\_tw${}_{5,1}$(A,B).

489: \end{quote}

490: }%\vspace{-0.1cm}

491: \noindent

492: %

493: In this case, the success information for \texttt{sp\_main(X,X2)}

494: guarantees that $\tt X2$ is definitely ground on success. Note that

495: this is equivalent to proving $\forall X\geq 3,~main(X,X2)\rightarrow

496: X2\geq 0$. Furthermore, our system is able to get to that conclusion

497: even if the \texttt{entry} only informs about $\tt X$ being any

498: possible ground term and $\tt X2$ a free variable.

499: %% wich we

500: %% propose in the paper\footnote{The exact parameters uses are is

501: %%   discussed later in the paper.} with the following parameters: the

502: %% \emph{sharing--freeness} abstract domain, 

503: \end{example}

504: The above results cannot be achieved unless all four points mentioned

505: before are available in a program analysis/specialization system.

506: %

507: For example, if we use traditional partial

508: deduction~\cite{Lloyd91,gallagher:pepm93-short} (PD) with the corresponding

509: \abstraction\ and \unfold\ rules followed by abstract interpretation

510: and \emph{abstract specialization} as described

511: in~\cite{spec-jlp-short,spec-inv-pepm03-short} we only obtain a comparable program

512: after four iterations of the: ``PD + abstract

513: interpretation + abstract specialization'' cycle.

514: %%  in any number of iterations of partial deduction

515: %% followed by abstract interpretation and abstract multiple

516: %% specialization. 

517: If we keep on adding more calls to {\tt formula}, every time more

518: iterations are necessary to obtain results comparable to ours. This

519: shows the importance of achieving an algorithm which is able to

520: \emph{interleave} PD, with abstract interpretation, extended with abstract

521: specialization, in order to communicate

522: the accuracy gains achieved from one to the other as soon as possible.

523: In any case, iterating over ``PD + analysis'' is not a

524: good idea from the efficiency point of view. Also, sometimes partially

525: evaluating a partially evaluated program can degrade the quality of

526: the residual program.

527: 

528: 

529: The remaining of the paper is organized as follows.

530: Section~\ref{sec:prel-notat} recalls some preliminary concepts. In

531: Sect.~\ref{sec:unfold-with-abstr}, we present abstract unfolding which

532: already integrates abstract executability.

533: Section~\ref{sec:spec-defin} introduces our notion of specialized

534: definition and embeds it within an abstract partial deducer. In

535: Sect.~\ref{sec:effic-prop-abstr}, we propose our scheme for abstract

536: interpretation with specialized definitions.

537: %Section~\ref{sec:code-generation} discusses how use interpret the

538: %results or our algorithm. 

539: Finally, Sect.~\ref{sec:disc-relat-work}

540: compares to related work and Sect.~\ref{sec:benefits-or-our}

541: concludes.

542: 

543: \secbeg

544: \section{Preliminaries} %Logic Programs and Partial Deduction}

545: \secend

546: \label{sec:prel-notat}

547: 

548: %% We assume some basic knowledge on the terminology of logic

549: %% programming. 

550: Very briefly (see for example~\cite{Lloyd87} for details), an

551: \emph{atom} $A$ is a syntactic construction of the form

552: $p(t_1,\ldots,t_n)$, where $p/n$, with $n\geq 0$, is a predicate

553: symbol and $t_1,\ldots,t_n$ are terms. %The function $pred$ applied to

554: %atom $A$, i.e., $pred(A)$, returns the predicate symbol $p/n$ for $A$.

555: A \emph{clause} is of the form $H\leftarrow B$ where its head $H$ is

556: an atom and its body $B$ is a conjunction of atoms. A \emph{definite

557:   program} is a finite set of clauses. A \emph{goal} (or query) is a

558: conjunction of atoms.

559: 

560: Let $G$ be a goal of the form

561:   $\leftarrow A_1,\ldots,\selat,\ldots,A_k$, $k\geq 1$. 

562: The concept of

563:   \emph{computation rule}, denoted by $\select$,  is used

564: to select an atom within a goal for its evaluation.

565:  % If $\select(G)=$$\selat$ we say that $\selat$ is the \emph{selected} atom

566:  % in $G$.

567: %  

568: %% \begin{definition}[computation rule] A \emph{computation rule} is a

569: %%   function

570: %% %$R:{\cal G} \mapsto {\cal A}$. 

571: %%   $\select$ from goals to atoms.  Let $G$ be a goal of the form

572: %%   $\leftarrow A_1,\ldots,\selat,\ldots,A_k$, $k\geq 1$.

573: %% %

574: %%   %% This first A_n gave me a weird output, at least on my LaTeX: was

575: %%   %% printed as ``A\''. I really do not understand why. --MH

576: %%   If $\select(G)=$$\selat$ we say that $\selat$ is the \emph{selected} atom

577: %%   in $G$.

578:  % 

579: %% \end{definition}

580: %

581: %

582: The operational semantics of definite programs is based on

583: derivations~\cite{Lloyd87}.

584: %\begin{definition}[derivation step]

585: %\label{def:der-step}

586: %Let $G$ be $\leftarrow A_1,\ldots,\selat,\ldots,A_k$. Let $\select$ be a

587: %computation rule and let $\select(G)=$$\selat$. 

588: %

589: Let $C=H \leftarrow B_1,\ldots,B_m$ be a renamed apart clause in $P$

590: such that $\exists \theta=mgu(\selat,H)$. Then $\leftarrow

591: \theta(A_1,\ldots,\selatpar{-1},B_1,\ldots,B_m,\selatpar{+1},\ldots,A_k)$

592: is \emph{derived} from $G$ and $C$ via $\select$.

593: %% \vspace*{-0.65cm}

594: %%   \begin{eqnarray*}

595: %% \theta=mgu(\selat,H) \\

596: %% G' \mbox{ is the goal } \leftarrow

597: %%   \theta(A_1,\ldots,\selatpar{-1},B_1,\ldots,B_m,\selatpar{+1},\ldots,A_k)

598: %%   \end{eqnarray*}

599: %\end{definition}

600: %

601: As customary, given a program $P$ and a goal $G$, an \emph{SLD

602:   derivation} for $P\cup\{G\}$ consists of a possibly infinite

603: sequence $G=G_0, G_1, G_2,\ldots$ of goals, a sequence $C_1,C_2,\ldots$

604: of properly renamed apart clauses of $P$, and a sequence

605: $\theta_1,\theta_2,\ldots$ of mgus such that each $G_{i+1}$ is derived

606: from $G_i$ and $C_{i+1}$ using $\theta_{i+1}$.

607: %

608: A derivation step can be non-deterministic when $\selat$ unifies with

609: several clauses in $P$, giving rise to

610: several possible SLD derivations for a given goal.  Such SLD

611: derivations can be organized in \emph{SLD trees}.

612: %

613: A finite derivation $G=G_0, G_1, G_2,\ldots, G_n$ is called

614: \emph{successful} if $G_n$ is empty.  In that case

615: $\theta=\theta_1\theta_2\ldots\theta_n$ is called the computed answer

616: for goal $G$.  Such a derivation is called \emph{failed} if it is not

617: possible to perform a derivation step with $G_n$.

618: %

619: %% In PD \cite{Lloyd91,gallagher:pepm93},

620: %% %%

621: %% \short{given a program and

622: %% a set of atoms,}

623: %% %%

624: %% specialized programs are constructed from SLD derivations using the

625: %% notion of % first level, called \emph{local control}, consists in applying an

626: %% \emph{unfolding rule}. %, denoted by $\unfold$, 

627: %% %Essentially an unfolding rule computes finite (possibly incomplete)

628: %% %SLD trees for these atoms.  

629: Given an atom $A$, an \emph{unfolding

630:   rule}~\cite{Lloyd91,gallagher:pepm93-short} computes a set of finite SLD

631: derivations $D_1,\ldots,D_n$ (i.e., a possibly incomplete SLD tree) of

632: the form $D_i=A,\ldots,G_i$ with computed answer substitution

633: $\theta_i$ for $i=1,\ldots,n$ whose associated \emph{resultants} (or

634: residual rules) are $\theta_i(A) \leftarrow G_i$. 

635: %By $\unfold (A,P)$

636: %we denote the set of resultants associated to the root-to-leaf non

637: %failed derivations of the tree from $A$.

638: % By

639: % $\unfold(S,\cR)$ we denote the union of $\unfold(A,\cR)$ for all $A

640: % \in S$.  

641: 

642: The following standard operations are used in the paper to handle

643: keyed-tables: \emptytable$(T)$ initializes a table $T$.

644: \store$(T,\mathit{Key},\mathit{Info})$ adds $\mathit{Info}$ associated

645: to $\mathit{Key}$ to $T$ and deletes previous information associated

646: to $\mathit{Key}$, if any.  \isin$(T,\mathit{Key})$ returns true iff

647: $\mathit{Key}$ is currently stored in the table. Finally,

648: \consult$(T,\mathit{Key})$ returns the information associated to

649: $\mathit{Key}$ in $T$.  For simplicity, we sometimes consider tables

650: as sets and we use the notation $(\mathit{Key}\leadsto

651: \mathit{Info})\in T$ to denote that there is an entry in the table T

652: with the corresponding $\mathit{Key}$ and associated $\mathit{Info}$.

653: 

654: \secbeg

655: \subsection{Abstract Interpretation}

656: \secend

657: 

658: Abstract interpretation \cite{Cousot77-short} provides a general

659: formal framework for computing safe approximations of programs

660: behaviour.

661: %for performing sound program analysis and has been

662: %successfully applied to the analysis of logic programs (see for

663: %example

664: %\cite{mcctr-fixpt,ai-jlp,LeCharlier94:toplas,inc-fixp-sas-short} and

665: %their references).  

666: %

667: Programs are interpreted using values in an \emph{abstract domain}

668: ($D_\alpha$) instead of the \emph{concrete domain} ($D$).

669: %

670: %The latter contains finite, approximate

671: % representations of (sets of) concrete properties.  Then, 

672: %An abstract

673: %value is a finite representation of a, possibly infinite, set of

674: %actual values in the concrete domain.  Our approach relies on the

675: %abstract interpretation theory \cite{Cousot77-short}, where 

676: The set of all possible abstract  values which represents

677: $D_\alpha$ is usually a complete lattice or cpo which is ascending

678: chain finite.

679: %% However, for this

680: %% study, abstract interpretation is restricted to complete lattices over

681: %% sets, 

682: %

683: Values in the abstract domain $\langle D_\alpha, \sqsubseteq \rangle$

684: and sets of values in the concrete domain $\langle 2^D, \subseteq

685: \rangle$ are related via a pair of monotonic mappings $\langle \alpha,

686: \gamma \rangle$: the {\em abstraction} function $\alpha:

687: 2^D\rightarrow D_\alpha$ which assigns to each (possibly infinite) set

688: of concrete values an abstract value, and the {\em concretization}

689: function $\gamma:D_\alpha\rightarrow 2^D$ which assigns to each

690: abstract value the (possibly infinite) set of concrete values it

691: represents.

692: \short{such that

693: %\[

694: $\begin{array}{c}%% \label{over-app}

695:  \forall x\in 2^D:~ \gamma(\alpha(x)) \supseteq x \mbox{~~~and~~~}

696:  \forall y\in D_\alpha:~ \alpha(\gamma(y)) = y .

697: \end{array}$

698: %\]

699: %

700: In general $\sqsubseteq$ is induced by $\subseteq$ and $\alpha$.

701: } %% short

702: %% The following abstract operations on the abstract domain $D_{\alpha}$, that we

703: %% will use in our algorithms, mimic those of $2^D$ in a

704: %% precise sense:

705: The operations on the abstract domain $D_{\alpha}$ that we will use in

706: our algorithms are:

707: %\vspace{-0.1cm}

708: \begin{itemize}

709: \item \arestrict$(\lambda,E)$ performs the abstract restriction (or

710:   projection) of a substitution $\lambda$ to the set of variables in

711:   the expression $E$, denoted $vars(E)$;

712: \item \aextend$(\lambda,E)$ extends the substitution $\lambda$ to the

713:   variables in the set $vars(E)$;

714: \item \aunif$(t_1,t_2,\lambda)$ obtains the description which results

715:   from adding the abstraction of the unification $t_1 = t_2$ to the

716:   substitution $\lambda$;

717: \item \aconj$(\lambda_1,\lambda_2)$ performs the abstract conjunction

718:   ($\sqcap$) of two substitutions;

719: \item \alub$(\lambda_1,\lambda_2)$ performs the abstract

720:   disjunction ($\sqcup$) of two substitutions.

721: \end{itemize}%of {\em least upper bound\/} ($\sqcup$) and

722: %{\em greatest lower bound\/} ($\sqcap$) 

723: %

724: %\vspace{-0.1cm}

725: In our algorithms we also use \acalltoentry$(A:CP,H\leftarrow B)$

726: which adapts and projects the information in an abstract atom $A:CP$

727: to the variables in the clause $C=H\leftarrow B$.  An \emph{abstract atom} of the form

728: $G:CP$ is a concrete atom $G$ which comes equipped with an

729: \emph{abstract substitution} $CP$ which is defined over $vars(G)$ and

730: provides additional information on the context in which the atom will

731: be executed at run-time.  \acalltoentry\ can

732: be defined in terms of the operations above as:

733: \acalltoentry$(A:CP,H\leftarrow B)$ =

734: $\arestrict$(\aunif$(A,H,\aextend(CP, C)),C)$.

735: %

736: Finally, the most general substitution is represented as $\top$,

737: and the least general (empty) substitution as $\bot$.

738: %%  assigns the empty set of values to

739: %% each variable.

740: %of five abstract operations \cite{incanal-toplas} on the description domain

741: 

742: 

743: \secbeg

744: \section{Unfolding with Abstract Substitutions}\label{sec:unfold-with-abstr}

745: \secend

746: 

747: %\subsection{SLD Resolution with Abstract Substitutions}

748: We now present an extension of SLD semantics which exploits abstract

749: information. This will provide the means to overcome difficulties (1)

750: and (2) introduced in Section~\ref{sec:motivation}.

751: %%

752: \short{The objective is to improve the quality of specialized rules

753:   (or resultants) by both unfolding and exploiting abstract call

754:   information.

755: %% \mycomment{Some comment which compares to Michael

756: %%   AUnfolding} 

757: We start by recalling some preliminary notions on partial evaluation.

758: %and fixing our notation.

759: } %% short

760: %

761:  The extended semantics handles abstract goals of the form

762: $G:CP$, i.e., a concrete goal $G$ comes equipped with an

763: abstract substitution $CP$ defined over $vars(G)$.

764: % and

765: %% provides additional information on the context in which the goal will

766: %% be executed at run-time.

767: %

768: The first rule 

769: %of SLD resolution with abstract substitution

770: corresponds to a derivation step.

771: %%  from a call to a user-defined

772: %% predicate. It makes use of the abstract (call) substitutions to remove

773: %% useless clauses.

774: %\vspace*{-0.15cm}

775: \begin{definition}[derivation step]

776:  \label{def:der-step-abs}

777:  Let $G:CP$ be an abstract goal where $G=\leftarrow

778:  A_1,\ldots,\selat,\ldots,A_k$. Let $\select$

779: be a computation rule and let $\select(G)=$$\selat$. 

780: %

781: Let $C=H \leftarrow B_1,\ldots,B_m$ be a renamed apart clause in $P$.

782: Then the abstract goal $G':CP'$ is \emph{derived} from $G:CP$ and $C$

783: via $\select$ if $\exists \theta=mgu(\selat,H)~\wedge$ $CP_u \neq

784: \bot$, where:

785: %\vspace*{-0.25cm}

786: \begin{eqnarray*}

787: CP_u =\aunif(\selat,H\theta,\aextend(CP,C\theta))\\

788: G'=\theta(A_1,\ldots,\selatpar{-1},B_1,\ldots,B_m,\selatpar{+1},\ldots,A_k)\\

789: CP'=\arestrict(CP_u,vars(G'))

790: \end{eqnarray*}

791: \end{definition}

792: %\vspace*{-0.25cm}

793: %

794: %% $\mathit{Derive}$ & $G$ & $\lambda$ & $\Rightarrow$  & $\leftarrow

795: %%   \theta(A_1,\ldots,\selatpar{-1},B_1,\ldots,B_m,\selatpar{+1},\ldots,A_k)$& $\arestrict(\lambda_u,vars(G'))$ 

796: %%   \\[1.5ex]

797: %% & \multicolumn{5}{l}{\begin{minipage}[t]{11cm}

798: %% if $C=H \leftarrow B_1,\ldots,B_m$ is a renamed apart clause in $P$ 

799: %% $\theta=mgu(\selat,H)$,\\

800: %%  ~~~~ $W=vars(C\theta), \lambda_e = \aextend(\lambda,W), 

801: %% \lambda_u =\aunif(\selat,H\theta,\lambda_e), \lambda_u \neq \bot$

802: %% \end{minipage}}\\[1ex]\hline \\

803: %

804: An important difference between the above definition and the standard

805: derivation step

806: % in Sect.~\ref{sec:prel-notat}.  The use

807: is that the use of abstract (call) substitutions allows imposing further

808: conditions for performing derivation steps, in particular, $CP_u$

809: cannot be $\bot$.

810: %% Obviously, if the set of calls possible is empty this derivation is

811: %% useless and can be considered \emph{failed} much in the same way as

812: %% when no clause can be used to further resolve the selected atom.

813: This is because if $CP\neq\bot$ and $CP_u=\bot$ then the head of the

814: clause $C$ is incompatible with $CP$ and the unification $\selat=H$ will

815: definitely fail at run-time.  \short{Thus, a derivation step is not

816:   allowed if $CP_u=\bot$ which may result in a failed derivation if

817:   there are not other clauses to resolve the selected atom $\selat$.}

818: Thus, abstract information allows us to remove useless clauses from

819: the residual program.

820: %% Consequently, the quality of the incomplete SLD trees

821: %% computed will be improved when compared to those achievable when

822: %% traditional SLD resolution is used. 

823: This produces more efficient resultants and increases the accuracy of

824: analysis for the residual code.

825: %\vspace*{-0.15cm}

826: \begin{example}\label{ex:derive}

827:   Consider the abstract atom $\tt

828:   \tuple{formula(s^4(X),X2)}{\{X/G,X2/V\}}$, which appears in the

829:   analysis of our running example (c.f. Fig.~\ref{fig:aog}).  We

830:   abbreviate as $\tt s^n(X)$ the successive application of $\tt n$

831:   functors $\tt s$ to variable $\tt X$. The notation $\tt X/G$ (resp.

832:   $\tt X/V$) indicates that variable $\tt X$ is ground (resp. a free

833:   variable).  After applying a derivation step, we obtain the derived

834:   abstract goal:\\[0.6ex]

835:   {\small $\tt

836:     \tuple{ground(s^4(X)),var(X2),two(T),minus(T,s^4(X),X2'),twice(X2',X2)}{\{X/G,X2/V,T/V,X2'/V\}}

837:     $}\\[0.6ex]

838:   where the abstract description has been extended with updated

839:   information about the freeness of the newly introduced variables. In

840:   particular, both {\tt T} and {\tt X2'} are {\tt V}.

841: \end{example}

842: 

843: 

844: %% The \emph{SLD semantics with abstract substitutions} is formed by the

845: %% above three derivation rules, i.e., those in

846: %% definitions~\ref{def:der-step-abs}, \ref{def:abs-ex-true}, and

847: %% \ref{def:abs-ex-fail}.  

848: 

849: \comment{

850: Regarding rule $\mathit{Aexec}$, though it may seem of narrow

851: applicability, in fact for many builtin procedures such as those that

852: check basic types or which inspect the structure of data, even these

853: simple optimizations are indeed very relevant.  Two non-trivial

854: examples of this are their application to simplifying independence

855: tests in program parallelization~\cite{spec-jlp-short} and the optimization

856: of delay conditions in logic programs with dynamic procedure call

857: scheduling order~\cite{spec-dyn-sch-iclp97}. 

858: 

859: % This, together with the

860: % detection of useless (failed) derivations, will improve the quality of

861: the incomplete SLD trees computed when compared to those achievable

862: when traditional SLD resolution is used. This consequently improves

863: the quality of the unfolding process and thus we generate

864: better resultants. 

865: }

866: 

867: %\vspace*{-0.25cm}

868: 

869: The second rule we present makes use of the availability of abstract

870: substitutions to perform \emph{abstract

871:   executability}~\cite{spec-jlp-short} during resolution.  This allows

872: replacing some atoms with simpler ones, and, in particular, with the

873: predefined atoms {\em true} and {\em false}, provided certain

874: conditions hold.

875: %% , or \emph{error}, or

876: %% to a simpler program fragment, by application of the information

877: %% obtained via abstract interpretation.  

878: We assume the existence of a predefined \emph{abstract executability

879:   table} which contains entries of the form $T:CP \leadsto T'$ which

880: specify the behaviour of external procedures: builtins, libraries, and

881: other user modules.  For instance, for predicate $\tt ground$ contains

882: the information $\tt ground(X):\{X/G\} \leadsto true$. For $\tt var$,

883: it contains $\tt var(X):\{X/V\} \leadsto true$.\footnote{In \ciaopp\ we

884:   use assertions to express such

885:   information in a domain-independent manner.}

886: %

887: \short{

888: The idea is that atoms of the form $A:CP$ which are produced during

889: unfolding and which are described by $T:CP_T$ such that $A=\theta(T)$

890: and $A:CP$ is described by $T:CP_T$ can be safely replaced by

891: $\theta(T')$. 

892: } %% short

893: %% These optimizations can in

894: %% fact be very relevant for many builtin procedures such as those that

895: %% check basic types or which inspect the structure of data.

896: 

897: % %%%%%%%%%%%%%%%%%%%%%%%% MERGED IN TABLE

898: %\vspace*{-0.15cm}

899: \begin{definition}[abstract execution]

900:  \label{def:abs-ex-true}

901:  Let $G:CP$ be an abstract goal where $G=\leftarrow

902:  A_1,\ldots,\selat,\ldots,A_k$. Let $\select$ be a computation rule

903:  and let $\select(G)=$$\selat$.

904: % In the same conditions of Def. \ref{def:der-step-abs}:

905:  Let $(T:CP_T \leadsto T')$ be a renamed apart entry in the abstract

906:  executability table.  Then, the goal $G':CP'$ is \emph{abstractly

907:    executed} from $G:CP$ and $(T:CP_T \leadsto T')$ via $\select$ if

908:  $\selat=\theta(T)$ and $CP_A\sqsubseteq CP_T$, where

909:  %\vspace*{-0.25cm} \vspace*{-0.25cm}

910: \begin{eqnarray*}

911: G' =A_1,\ldots,\selatpar{-1},\theta(T'),\selatpar{+1},\ldots,A_k\\

912: CP'= \arestrict(CP,G')\\ 

913: CP_A = \acalltoentry(A_R:CP,T\leftarrow true)

914:  \end{eqnarray*}

915: %\vspace*{-0.25cm}\vspace*{-0.25cm}

916: \end{definition}

917: %

918: \begin{example}\label{ex:aexec}

919: %\vspace*{-0.25cm}

920:   From the derived goal in Ex.~\ref{ex:derive}, we can apply twice the

921:   above rule to abstractly execute the calls to {\tt ground} and {\tt

922:     var} and obtain:

923: %\vspace*{-0.15cm}

924: \begin{center} $\tt

925:   \tuple{two(T),minus(T,s^4(X),X2'),twice(X2',X2)}{\{X/G,X2/V,T/V,X2'/V\}}

926: $

927: \end{center}%\vspace*{-0.15cm}

928: since both calls succeed by using the abstract executability table

929: described above and the information in the abstract substitution.

930: \end{example}

931: %\vspace*{-0.25cm}

932: %\vspace*{-0.15cm}

933: \begin{definition}[\aunfold]\label{def:aunfold}

934:   Let $\tuple{A}{CP}$ be an abstract atom and $P$ a program. We define

935:   $\aunfold(P,\tuple{A}{CP})$ as the set of \emph{resultants}

936:   associated to a finite (possibly incomplete) SLD tree computed by

937:   applying the rules of Definitions \ref{def:der-step-abs} and

938:   \ref{def:abs-ex-true} to $\tuple{A}{CP}$.

939: \end{definition}

940: %\vspace*{-0.25cm}

941: %%

942: %\subsection{Unfolding based on SLD Resolution with Abstract Substitutions}\label{sec:unfolding-based-sld}

943: %

944: %% \begin{definition}[\unfold]

945: %% %% Consider a program $P$. Let $A$ be an atom and $\lambda$ be an

946: %% %% abstract substitution. We define function $\unfold$ which takes $P$,

947: %% %% $A$ and $\lambda$, denoted by $\unfold(P,\tuple{A}{\lambda})$, and

948: %% %% computes a finite (possibly incomplete) SLD tree by applying the three

949: %% %% rules of the above SLD semantics with abstract substitutions. 

950: %% %

951: %%   Consider a program $P$. Let $A$ be an atom and $\lambda$ be an

952: %%   substitution. The \emph{unfolding rule} computes for

953: %%   $\tuple{A}{\lambda}$ a set of finite SLD derivations

954: %%   $D_1,\ldots,D_n$ of the form $D_i=A,\ldots,G_i$ with computer answer

955: %%   substitution $\theta_i$ for $i=1,\ldots,n$ by applying the three the

956: %%   SLD semantics of Def.~\ref{def:sld}.  We denote by

957: %%   $\unfold(P,\tuple{A}{\lambda})$ the set of \emph{resultants} (or

958: %%   specialized definitions) $\theta_i(A) \leftarrow G_i$ associated to

959: %%   each derivation $D_i$.

960: %% \end{definition}

961: %

962: The so-called \emph{local control} of PD ensures the termination of

963: the above process. For this purpose, the unfolding rule must

964: incorporate some mechanism to stop the construction of SLD derivations

965: (we refer to \cite{LeuschelBruynooghe:TPLP02} for details).

966: \begin{example}\label{ex:aunfold}

967:   Consider an unfolding rule $\aunfold$ based on homeomorphic

968:   embedding \cite{LeuschelBruynooghe:TPLP02} to ensure termination and

969:   the initial goal in Ex.~\ref{ex:derive}. The derivation continuing

970:   from Ex.~\ref{ex:aexec}  performs several additional derivation steps

971:   and abstract executions and branches (we do not include them due to space

972:   limitations and also because it is well understood).  The following

973:   resultants are obtained from the resulting tree:

974: %\vspace*{-0.15cm}

975: \begin{verbatim}

976:       formula(s(s(s(s(0),s(s(s(s(0))))).

977:       formula(s(s(s(s(s(A))))),s(s(s(s(s(s(B))))))) :- tw(A,B)

978: \end{verbatim}

979: %\vspace*{-0.15cm} 

980: %

981: which will later be filtered and renamed resulting

982: in rules 4 and 5 of Ex.~\ref{ex:sp}.

983: \end{example}

984: %

985: %

986: %For this purpose, there exist

987: %several well-known techniques in the literature, e.g., depth-bounds,

988: %loop-checks \cite{Bol93}, well-founded orderings \cite{BdSM92},

989: %well-quasi orderings \cite{SG95}, etc.

990: % Our implementation uses some of

991: %them (we refer to \cite{LeuschelBruynooghe:TPLP02} for details on

992: % local control).

993: %

994: %

995: %\vspace*{-0.05cm} 

996: It is important to note that SLD resolution with

997: abstract substitutions is not restricted to the left-to-right

998: computation rule.  However, it is well-known that non-leftmost

999: derivation steps can produce incorrect results if the goal contains

1000: \emph{impure} atoms to the left of $\selat$.  More details can be

1001: found, e.g., in~\cite{LeuschelEtAl:TPLP03}.

1002: %

1003: Also, abstract execution of non-leftmost atoms can be incorrect if the

1004: abstract domain used captures properties which are not downwards

1005: closed. A simple solution is to only allow leftmost abstract execution

1006: for non-downwards closed domains (and non-leftmost for derivation

1007: steps).

1008: 

1009: 

1010: \secbeg

1011: \section{Specialized Definitions}

1012: \secend

1013: \label{sec:spec-defin}

1014: 

1015: %% \comment{

1016: %% \subsection{Basics of Partial Deduction}

1017: 

1018: %% %A basic partial deduction algorithm appears in

1019: %% %Figure~\ref{basic-algo}.  

1020: 

1021: %% Given an input program and a set of atoms, the following algorithm

1022: %% illustrates the process of computing a partial deduction

1023: %% \cite{Lloyd91,gallagher:pepm93}.

1024: %% %

1025: 

1026: %% \begin{algorithm}[h] \label{basic-algo} ${}$\\

1027: %% {\small\bf Input}: a program $P$ and a set of atoms $T$\\

1028: %% {\small\bf Output}: a set of atoms $S$\\

1029: %% {\small\bf Initialization}: $i := 0;~ T_{0} := T$ \\

1030: %% {\small\bf Repeat} \\

1031: %% \mbox{} ~~~~  \begin{tabular}{ll}

1032: %% 1. & $P' := \unfold(T_{i},P)$; \\

1033: %% 2. & $T_{i+1} := \abstraction(T_{i},P_{calls})$; \\

1034: %% 3. & $i := i+1$; 

1035: %% \end{tabular}\\

1036: %% {\small\bf Until} $T_{i} = T_{i-1}$ (modulo renaming)\\

1037: %% {\small\bf Return} $S := T_{i}$

1038: %% \end{algorithm}

1039: %% %

1040: %% The first level, called \emph{local control}, consists in applying an

1041: %% \emph{unfolding rule} %, denoted by $\unfold$, 

1042: %% to compute finite (possibly incomplete) SLD trees for these atoms.

1043: %% Given an atom $A$, an unfolding rule computes a set of finite SLD

1044: %% derivations $D_1,\ldots,D_n$ (i.e., a possibly incomplete SLD tree) of

1045: %% the form $D_i=A,\ldots,G_i$ with computer answer substitution

1046: %% $\theta_i$ for $i=1,\ldots,n$ whose associated \emph{resultants} (or

1047: %% residual rules) are $\theta_i(A) \leftarrow G_i$. By $\unfold (A,P)$

1048: %% we denote this set of resultants associated to the root-to-leaf non

1049: %% failed derivations of the tree. By $\unfold(S,\cR)$ we denote the union of

1050: %% $\unfold(A,\cR)$ for all $A \in S$.  

1051: 

1052: %% Then, the so-called \emph{global} control defines a $\abstraction$

1053: %% operator which guarantees that the number of SLD trees computed is

1054: %% kept finite (by ensuring the finiteness of the set of terms for which

1055: %% partial evaluations are produced).  The \abstraction\ operator is

1056: %% applied to properly add the atoms in the bodies of the resultants

1057: %% (denoted by $P_{calls}$) to the set of atoms already partially

1058: %% evaluated ($T_i$); the abstraction phase yields a new set of atoms

1059: %% which may need further evaluation and, thus, the process is

1060: %% iteratively repeated while new atoms are introduced.

1061: %% %

1062: 

1063: 

1064: %% The final set of resultants for the computed SLD trees is called a

1065: %% \emph{partial deduction} (PD) for the initial set of atoms.  We refer

1066: %% to \cite{LeuschelBruynooghe:TPLP02,Lloyd91} for details.  Note that

1067: %% the way in which partial evaluations are thus constructed is given by

1068: %% the {\em unfolding rule}, which determines the atoms to be unfolded

1069: %% and which decides how to stop the construction SLD trees.

1070: 

1071: %% }

1072: 

1073: 

1074: %\subsection{Partial Deduction with Specialized Definitions}

1075: 

1076: 

1077: \begin{algorithm}[t]

1078: \caption{Abstract Partial Deduction with Specialized Definitions}

1079: \label{algo:pd-with-spec-defs}

1080: \begin{algorithmic} [1]

1081: \renewcommand{\baselinestretch}{0.5} \sizeinfigure

1082: \Procedure{partial\_evaluation\_with\_spec\_defs}{$P,\{A_1:CP_1,\ldots,A_n:CP_n\}$}

1083: \State \emptytable$(\gt)$; \emptytable$(\st)$

1084: \For{$j = 1..n$}

1085: \State  {\sc process\_call\_pattern}($A_j:CP_j$) 

1086: \EndFor

1087: \EndProcedure

1088: \Statex

1089: \Procedure{process\_call\_pattern}{$A:CP$}

1090: \If {{\bf not }\isin$(\gt,A:CP)$}

1091: \State $(A_1,A_1')\gets$ {\sc specialized\_definition}$(P,A:CP)$

1092: \State $A_1:CP_1\gets$ \consult$(\gt,A:CP)$

1093: \ForAll  {ren. apart clause $C_k=H_k \leftarrow B_{k}\in P$

1094:   s.t. $H_k$ unifies with $A_1'$}

1095: \State $CP_k$ $\gets$ \acalltoentry$(A_1':CP_1,C_k)$

1096: \State {\sc process\_clause}$(CP_k,~B_{k})$

1097: \EndFor

1098: \EndIf

1099: \EndProcedure

1100: \Statex

1101: \Procedure{process\_clause}{$CP,~B$}

1102: %\If {$CP \neq \bot$}

1103: \If {$B=(L,R)$}

1104: \State $CP_L \gets \arestrict(CP,L)$

1105: \State {\sc process\_call\_pattern}($L:CP_L$)  %reversed

1106: \State {\sc process\_clause}$(CP,~R)$  

1107: \Else 

1108: \State $CP_B \gets \arestrict(CP,B)$

1109: \State {\sc process\_call\_pattern}($B:CP_B$)

1110: \EndIf

1111: %\EndIf

1112: \EndProcedure

1113: \Statex

1114: \Function {specialized\_definition}{$P,A:CP$}

1115: \State $A':CP'\gets \aabstraction(\st,A:CP)$

1116: \State $\store(\gt,\tuple{A}{CP},\tuple{A'}{CP'})$

1117: \If {\isin$(\st,A':CP')$}

1118: \State $A''\gets $\consult$(\st,A':CP')$

1119: \Else

1120: \State $\mathit{Def}\gets \aunfold(P,\tuple{A'}{CP'})$

1121: \State $A''\gets \newpred(A')$ 

1122: \State $\store(\st,\tuple{A'}{CP'},A'')$

1123: \State $\mathit{Def}'\gets \{(H' \leftarrow B) ~|~ (H\leftarrow B)\in \mathit{Def}\wedge

1124: H'=\ren(H,\{A'/A''\})\}$

1125: \State $P\gets P\bigcup \mathit{Def}'$

1126: \EndIf

1127: \State \Return $(A',A'')$

1128: \EndFunction

1129: \renewcommand{\baselinestretch}{1.0}\normalsize

1130: \end{algorithmic}

1131: \end{algorithm}

1132: 

1133: We now define an Abstract Partial Deduction (APD) algorithm whose

1134: execution can later be \emph{interleaved} in a seamless way with a

1135: state-of-the-art abstract interpreter.  For this it is essential that

1136: the APD process can generate residual code \emph{online}.  Thus,

1137: we need to produce a residual, specialized definition for a call

1138: pattern as soon as we finish processing it. This will make it possible

1139: for the analysis algorithm to have access to the improved definition.

1140: This may increase the accuracy of the analyzer and addresses the

1141: difficulty (2) described in Sect.~\ref{sec:motivation}.

1142: 

1143: %% It is important to note that traditional PD systems produce the

1144: %% residual program in a final, post-process of their execution.

1145: Typically, PD is presented as an iterative process in which partial

1146: evaluations are computed for the new generated atoms until they

1147: \emph{cover} all calls which can appear in the execution of the

1148: residual program. This is formally known as the \emph{closedness}

1149: condition of PD \cite{Lloyd91}. In order to ensure termination of this

1150: global process, the so-called \emph{global} control defines a

1151: $\aabstraction$ operator (see \cite{LeuschelBruynooghe:TPLP02}) which

1152: guarantees that the number of SLD trees computed is kept finite, i.e.,

1153: it ensures the finiteness of the set of atoms for which partial

1154: evaluation is produced.

1155: %

1156: %% Once this iterative process finishes, the set

1157: %% of resultants is obtained in a straightforward way.

1158: However, the residual program is not generated until such iterative

1159: process terminates.

1160: %

1161: 

1162: Algorithm~\ref{algo:pd-with-spec-defs} presents an APD algorithm.

1163: %

1164: %% In order to produce specialized definitions \emph{during} the

1165: %% execution of the iterative PD process, two main modifications have to

1166: %% be performed on the traditional scheme.  First, there is a need to

1167: %% maintain the specialized definitions and to keep track of the

1168: %% generalized atoms to which they correspond. This is done,

1169: %% respectively, in:

1170: %% \begin{itemize}

1171: %\item 

1172: The main difference with standard algorithms is that the resultants

1173: computed by \aunfold\ (L26) are added to the program during execution

1174: of the algorithm (L30) rather than in a later code generation phase.

1175: %

1176: In order to avoid conflicts among the new clauses and the original

1177: ones, clauses for specialized definitions are renamed with a fresh

1178: predicate name (L29) prior to adding them to the program (L30).

1179: %

1180: The algorithm uses two global data structures. The

1181: \emph{specialization table} contains entries of the form $A:\CP{}

1182: \leadsto A'$.  The atom $A'$ provides the link with the clauses of the

1183: specialized definition for $A:CP$.

1184: %  since a clause

1185: %  $H\leftarrow B$ in $P$ is in the specialized definition for $A:CP$

1186: %  iff $H$ unifies with $A'$.

1187: %\item 

1188: The \emph{generalization table} stores the results of the

1189: \aabstraction\ function and contains entries

1190: %of the  form 

1191:   $A:CP\leadsto A':CP$ where $A':CP'$ is a generalization of $A:CP$.

1192: %%  obtained by applying an $\aabstraction$ operator.

1193: %% operation

1194: %%   corresponds to the so-called global control carried out in partial

1195: %%   deduction (see Sect.~\ref{sec:preliminaries}). Given an abstract

1196: %%   pattern $A:\CP{}$, it returns a possibly more general atom

1197: %%   $A':\CP'{}$ which, at the cost of possibly losing information,

1198: %%   allows us to ensure termination. The correspondence between the

1199: %%   original call and the generalized one is stored in $\gt$ and will be

1200: %%   useful for the generation of the specialized code.

1201: %\end{itemize}

1202: \short{We refer by LX to line number X in the algorithm}

1203: %

1204: 

1205: Computation is initiated by procedure {\sc

1206:   partial\_evaluation\_with\_spec\_defs} (L1-4) which initializes the

1207: tables and calls {\sc process\_call\_pattern} for each abstract atom

1208: $A_i:CP_i$ in the initial set

1209: %of atoms 

1210: to be partially evaluated.  

1211: %

1212: %% , the procedure {\sc process\_call\_pattern} performs the typical

1213: %% global PD processing explained above, which specializes new atoms

1214: %% until closedness is achieved (i.e., no more new atoms appear and thus

1215: %% condition L6 is never again satisfied).

1216: %% 

1217: %% 

1218: %% Second, the obtained specialized definitions have to be

1219: %% independently \emph{renamed} just before inserting them in the

1220: %% specialization table. This is needed for a correct code generation as

1221: %% we discuss in Sect~\ref{sec:code-generation}.

1222: The task of {\sc process\_call\_pattern} is, if the atom has not been

1223: processed yet (L6), to compute a specialized definition for it (L7)

1224: and then process all clauses in its specialized definition by means of

1225: calls to {\sc process\_clause} (L9-11).

1226: %

1227: %% Upon return of {\sc specialized\_definition}, calls in the bodies of

1228: %% the produced resultants have to be inspected and (if required)

1229: %% appropriately specialized. 

1230: Procedure {\sc process\_clause} 

1231: %% is encharged of this task.  The only

1232: %% difference with a traditional PD system is that 

1233: traverses clause bodies, processing their corresponding atoms by means

1234: of calls to {\sc process\_call\_pattern}, in a depth-first,

1235: left-to-right fashion. The order in which pending call patterns

1236: (atoms) are handled by the algorithm is usually not fixed in PD

1237: algorithms. They are often all put together in a set.  The reason

1238: for this presentation is to be as close as possible to our analysis

1239: algorithm which enforces a depth-first, left-to-right traversal of

1240: program clauses.

1241: %

1242: In this regard, the relevant point to note is that this algorithm does

1243: not perform success propagation yet (difficulty 3).  

1244: %

1245: In L16, it becomes apparent that the atom(s) in $R$ will be analyzed

1246: with the same call pattern $CP$ as $L$, which is to their left in

1247: the clause.

1248: %% the its leftmost brother (rather

1249: %% than using its answer pattern). 

1250: This, on one hand, may clearly lead to substantial precision loss.

1251: For instance, the abstract pattern $\tt formula(C,A):\{C/G,C/V\}$ which is

1252: necessary to obtain the last two resultants of Ex.~\ref{ex:sp} cannot

1253: be obtained with this algorithm.  In particular, we cannot infer the

1254: groundness of $\tt C$ which, in turn, prevents us from abstractly

1255: executing the next call to $\tt ground$ and, thus, from obtaining this

1256: optimal specialization.

1257: %

1258: On the other hand, this lack of success propagation makes it difficult

1259: or even impossible to work with non downwards closed domains, since

1260: $CP$ may contain information which holds before execution of the

1261: leftmost atom $L$ but which can be uncertain or even false after that.

1262: In fact, in our example $CP$ contains the info $\tt C/V$, which

1263: becomes false after execution of $\tt tw(B,C)$, since now $\tt C$ is

1264: ground.

1265: %

1266: This problem is solved in the algorithm we present in the next

1267: section, where analysis information flows from left to right, adding

1268: more precise information and eliminating information which is no

1269: longer safe or even definitely wrong. 

1270: %Such left-to-right propagation

1271: %is represented in Fig.~\ref{fig:aog} with a dashed horizontal arrow.

1272: 

1273: For the integration we propose, the most relevant part of the

1274: algorithm comprises L20-31, as it is the code fragment which is

1275: \emph{directly} executed from our abstract interpreter. The remaining

1276: procedures (L1-L19)

1277: %% behave as a traditional partial deducer

1278: %% and 

1279: will be overridden by more accurate ones later.  

1280: %

1281: The procedure of  interest

1282: %corresponds to the process of specializing atoms and it is carried out

1283: is {\sc specialized\_definition}. As it is customary, it performs

1284: (L21) a generalization of the call $A:CP$ using the abstract

1285: counterpart of the $\abstraction$ operator, denoted by

1286: $\aabstraction$, and which is in charge of ensuring termination at the

1287: global level.

1288: %\footnote{These operators have been

1289: %intensively investigated in the PE literature and their definition is

1290: %outside the scope of this paper.}  

1291: The result of the generalization, $A':CP'$, is inserted in the

1292: generalization table $\gt$ (L22). Correctness of the algorithm

1293: requires that $A:CP\sqsubseteq A':CP'$. If $A':CP'$ has been

1294: previously treated (L23), then its specialized definition $A''$ is

1295: looked up in $\st$ (L24) and returned.  Otherwise, a specialized

1296: definition $\mathit{Def}$ is computed for it by using the $\aunfold$

1297: operator of Def.~\ref{def:aunfold} (L26).

1298: %

1299: As already mentioned, the specialized definition $\mathit{Def}$ for

1300: the abstract atom $A:\CP{}$ is used to extend the original program

1301: $P$.  First, the atom $A'$ is renamed by using $\newpred$ which

1302: returns an atom with a fresh predicate name, $A''$, and optionally

1303: filters constants out (L27).  Then, function $\ren$ is applied to

1304: rename the clause heads using atom $A'$ (L29).

1305: % obtained by $\newpred$. 

1306:  $\ren(A,\{B/B'\})$ returns $\theta(B')$ where

1307: $\theta=mgu(A,B)$.  Finally, the program $P$ is extended with the new,

1308: \emph{renamed} specialized definition, $\mathit{Def}'$.

1309: %, and no rule is

1310: %extracted from it (L30).

1311: %\vspace{-0.1cm}

1312: 

1313: \begin{example}

1314:   

1315: Three calls to {\sc specialized\_definition} appear

1316: (within an oval box) during the analysis of our running example in

1317: Fig.~\ref{fig:aog} from the following abstract atoms, first $\tt

1318: main(s^3(X),X2):\{X/G,X2/V\}$, then $\tt tw(B,C):\{B/G,C/V\}$ and

1319: finally $\tt f(C,A):\{C/G,C/V\}$. The output of such executions is

1320: used later (with the proper renaming) to produce the resultants in

1321: Ex.~\ref{ex:sp}. 

1322: %

1323: For instance, the second clause obtained from the first call to {\sc

1324:   specialized\_definition} is

1325: \begin{quote}\tt

1326: %\vspace*{-0.25cm}

1327: sp\_main${}_2$(s(s(s(s(B)))),A) :- tw${}_{2,1}$(B,C),formula${}_{2,2}$(C,A).

1328: %\vspace*{-0.25cm}

1329: \end{quote}

1330: 

1331: \noindent

1332: where only the head is renamed.  The renaming of the body literals is

1333: done in a later code generation phase

1334: % (see

1335: %Section~\ref{sec:fram-as-spec}). 

1336: %% as it is done

1337: %% in Algorithm~\ref{algo:codegen}.

1338: %

1339: As already mentioned, Alg.~\ref{algo:pd-with-spec-defs} is not able

1340: to obtain such abstract atoms due to the absence of success

1341: propagation.

1342: %

1343: \short{

1344: The following section introduces the key concept of how these abstract

1345: atoms are obtained by the abstract interpreter.  Also, we will discuss

1346: later the process of obtaining the partially evaluated program from

1347: the entries in the specialization, in the generalization tables and

1348: the extended program $P'$.

1349: %

1350: In particular, it is crucial the definition of $\aabstraction$

1351: operators which allow obtaining \emph{feasible} partial evaluations.

1352: }

1353: \end{example}

1354: 

1355: 

1356: %

1357: \short{

1358: to ensure independence. This will also make it possible to generate a

1359: partially evaluated program, as we discuss in the remaining of the

1360: section.

1361: } %% short

1362: 

1363: %%   The main differences with the analysis

1364: %% algorithm~\ref{algo:eff-analysis} are (1) the introduction of two more

1365: %% global data structures: the specialization table $\st$ and the

1366: %% generalization table $\gt$ which will make it possible to construct

1367: %% the associated partially evaluated program and (2) the introduction of

1368: %% function {\sc specialized\_definition} to generate new, specialized

1369: %% definitions for the atoms which dynamically appear in the analysis

1370: %% graph.

1371: 

1372: %% The specialization table contains entries of the form $A:\CP{} \mapsto

1373: %% P$.  This corresponds to a new, specialized definition $P$ for the

1374: %% abstract atom $A:\CP{}$. The main novelty is that the standard

1375: %% analysis algorithm (presented in the previous section) will not

1376: %% analyze $A:\CP{}$ w.r.t.~the definition of the procedure in the

1377: %% original program but with $P$. It should be noted that an independent

1378: %% renaming, $\ren$ is applied to the left-hand side of the new

1379: %% definition $P$ in order to facilitate the code generation phase. This

1380: %% issue is discussed in detail in the next section.

1381: 

1382: %% The generalization table contains entries of the form $A:\CP{} \mapsto

1383: %% A':\CP'{}$. The $\abstraction$ operation corresponds to the so-called

1384: %% global control carried out in partial deduction (see

1385: %% Sect.~\ref{sec:preliminaries}). Given an abstract pattern $A:\CP{}$,

1386: %% it returns a possibly more general atom $A':\CP'{}$ which, at the cost

1387: %% of possibly losing information, allows us to ensure termination. The

1388: %% correspondence between the original call and the generalized one is

1389: %% stored in $\gt$ and will be useful for the generation of the

1390: %% specialized code.

1391: 

1392: %% As for the {\sc specialized\_definitions} function, it initially

1393: %% computes a specialized definition, $\mathit{Def}$, for the generalized atom

1394: %% $A':\CP'{}$ by using $\unfold$ (as explained in

1395: %% Sect.~\ref{sec:unfolding-based-sld}). The head of the new definition

1396: %% is renamed. By using $\newpred$, a fresh predicate name is produced

1397: %% for the predicate. Then, function $\ren$ applies the renaming to the

1398: %% clause head.  An important point to note is that the original program

1399: %% is extended with the new, \emph{renamed} specialized definition and no

1400: %% rule is extracted from it. There is no conflict since the new

1401: %% definition has been appropriately renamed.

1402: 

1403: 

1404: 

1405: 

1406: %% \mycomment{Justify equivalence to APD}

1407:  

1408: \short{

1409: \begin{theorem}[closedness]

1410:   All calls which might occur  during the execution of the specialized

1411:   program are covered by some program rule.

1412: \end{theorem}

1413: }%% short

1414: 

1415: 

1416: \secbeg\secbeg

1417: \section{Abstract Interpretation with Specialized Definitions}

1418: \secend

1419:  \label{sec:effic-prop-abstr}

1420: 

1421: 

1422: 

1423: %% 

1424: %% 

1425: %% In order to discuss the propagation of abstract success description we

1426: %% present an extended and adapted version of an existing algorithm for

1427: %% context-sensitive, polyvariant abstract

1428: %% interpretation~\cite{inc-fixp-sas-short}.  

1429: We now present our final algorithm for abstract interpretation with

1430: specialized definitions. This algorithm extends both the APD

1431: Algorithm~\ref{algo:pd-with-spec-defs} and the abstract interpretation

1432: algorithms in \cite{inc-fixp-sas-short,incanal-toplas}.

1433: %

1434: W.r.t.\ Algorithm~\ref{algo:pd-with-spec-defs}, the main improvement

1435: is the addition of success propagation.

1436: %

1437: Unfortunately, this requires computing a global fixpoint. It is an

1438: important objective for us to be able to compute an accurate fixpoint

1439: in an efficient way.

1440: %

1441: W.r.t the algorithms in \cite{inc-fixp-sas-short,incanal-toplas}, the

1442: main improvements are the following. (1) It deals directly with

1443: non-normalized programs. This point, which does not seem very relevant

1444: in a pure analysis system, becomes crucial when combined with a

1445: specialization system in order to profit from constants propagated by

1446: unfolding. (2) It incorporates a hardwired efficient graph traversal

1447: strategy which eliminates the need for maintaining priority queues

1448: explicitly~\cite{incanal-toplas}.

1449: %% This algorithm

1450: %% will form the basis for introducing abstract interpretation with

1451: %% specialized definitions.

1452: (3) The algorithm includes a widening operation for calls,

1453: \widencall, which limits the amount of multivariance in order to keep

1454: finite the number of call patterns analyzed. This is required in order

1455: to be able to use abstract domains which are infinite, such as regular

1456: types.

1457: %

1458: (4) It also includes a number of simplifications to facilitate

1459: understanding, such as the use of the keyed-table ADT, which we assume

1460: encapsulates proper renaming apart of variables and the application

1461: of renaming transformations when needed.

1462: 

1463: In order to compute and propagate success substitutions,

1464: Algorithm~\ref{algo:ai-with-spec-defs} computes a {\em program

1465:   analysis graph} in a similar fashion as state of the art analyzers

1466: such as the \ciaopp\ analyzer~\cite{inc-fixp-sas-short,incanal-toplas}.

1467: %% , GAIA

1468: %% \cite{LeCharlier94:toplas}, and the CLP($\cal R$)

1469: %% analyzer~\cite{softpe}.  

1470: %

1471: \short{Such graph can be viewed as a finite representation of the (possibly

1472: infinite) set of (possibly infinite) AND-OR trees explored by the

1473: concrete execution \cite{bruy91}.

1474: } %% short

1475: For instance, the analysis graph

1476: computed by Algorithm~\ref{algo:ai-with-spec-defs} for our running

1477: example is depicted in Fig.~\ref{fig:aog}.

1478:   %

1479: The graph has two sorts of nodes. Those which correspond to atoms are

1480: called ``OR-nodes''.  For instance, the node $ {\tt

1481:   ^{\{X/G,X2/V\}}main(s^3(X),X2)^{\{X/G,X2/G\}}}$ indicates that when

1482: the atom $\tt main(s^3(X),X2)$ is called with description ${\tt

1483:   \{X/G,X2/V\}}$ the answer (or success) substitution computed is $\tt

1484: \{X/G,X2/G\}$.  Those nodes which correspond to rules are called

1485: ``AND-nodes''. In Fig.~\ref{fig:aog}, they appear within a dashed box

1486: and contain the head of the corresponding clause. Each AND-node has as

1487: children as many OR-nodes as literals there are in the body.  If a

1488: child OR-node is already in the tree, it is no further expanded and

1489: the currently available answer is used.

1490: %

1491: For instance, the analysis graph in Figure~\ref{fig:aog} contains

1492: three occurrences of the abstract atom $\tt tw(B,C):\{B/G,C/V\}$

1493: (modulo renaming), but only one of them has been expanded. This is

1494: depicted by arrows from the two non-expanded occurrences of $\tt

1495: tw(B,C):\{B/G,C/V\}$ to the expanded one.  More information on the

1496: efficient construction of the analysis graph can be found

1497: in~\cite{inc-fixp-sas-short,incanal-toplas,bruy91}.

1498: 

1499: 

1500:  \begin{figure}[t]

1501: \footnotesize \fbox{

1502: \begin{minipage}{12.6cm}\centering

1503:   $\xymatrix@!R=0.5pt{

1504:     &   {\tt ^{\{X/G,X2/V\}}main(s^3(X),X2)^{\{X/G,X2/G\}}} \ar@{..}[d]  \\

1505:     & \ovalbox{\txt{\tt \scriptsize SPEC\_DEF($\tt main(s^3(X),X2):\{X/G,X2/V\}$) }}\ar@{..{*}}[dl]\ar@{..{*}}[dr]\\

1506:    *[F.]{{\tt main(s^3(0),0)}}

1507:     \ar@{-}[d]& & *[F.]{\tt  main(s^4(B),A) } \ar@{-}[dl] \ar@{-}[dr]\\

1508:     \Box & \tt ^{\{B/G,C/V\}}tw(B,C)^{\{B/G,C/G\}}\ar@{..}[d] \ar@{-->}[rr] & &

1509:     \tt ^{\{C/G,A/V\}} f(C,A)^{\{C/G,A/G\}} \ar@{..}[d] \\

1510: & \ovalbox{\txt{\tt  \scriptsize  SPEC\_DEF($\tt tw(B,C):\{B/G,C/V\}$) }}\ar@{..{*}}[dl]\ar@{..{*}}[d] &  &

1511:     \ovalbox{\txt{\tt  \scriptsize SPEC\_DEF($\tt  f(C,A):\{C/G,A/V\}$) }}\ar@{..{*}}[dl]\ar@{..{*}}[d]\\

1512: *[F.]{\tt  tw(0,0)} \ar@{-}[d]  & 

1513: *[F.]{\tt tw(s(B),s^2(C)} \ar@{-}[d]  &  

1514: *[F.]{\tt f(0,s^4(0)))))}  \ar@{-}[d]  &

1515: *[F.]{\tt  f(s(A),s^6(B)} \ar@{-}[d]  \\

1516:  \Box     & \tt ^{\{B/G,C/V\}}tw(B,C)^{\{B/G,C/G\}} \ar@(r,r)[uuu] 

1517: & \Box &  \tt ^{\{A/G,B/V\}}tw(A,B)^{\{A/G,B/G\}}\ar@(r,r)[lluuu]  \\ 

1518: %& *[F.]{\tt f(0,s^4(0))} \ar@{-}[d] & &

1519: %  *[F.]{\tt  f(s(A),s^6(B))} \ar@{-}[d] \\

1520: % &  \Box  & &  \tt tw(A,B)^{\{A/G,B/G\}}\ar@(r,r)[lluuuuu] 

1521:   }$

1522: \end{minipage}

1523: }\caption{Analysis Graph computed by {\scriptsize\sc ABS\_INT\_WITH\_SPEC\_DEF}}

1524: \label{fig:aog}

1525: %\vspace*{-0.5cm}

1526: \end{figure}

1527: 

1528: \short{

1529: \begin{example}

1530: As a result of analyzing our running program, we obtain the following

1531: tables:

1532: \begin{center}

1533:     \begin{tabular}{|c|c|}\hline\hline

1534:      \multicolumn{2}{|c|}{\bf Answer Table} \\ \hline %  \multicolumn{2}{|c|}{\bf Dependency Table} \\ \hline

1535:      Abstract atom & Answer pattern               \\ \hline\hline

1536:     $\tt \tuple{main(s^3(X),X2)}{\{X/G,X2/V\}}$ & $\tt \{X/G,X2/G\}$  \\ \hline

1537:     $\tt \tuple{tw(B,C)}{\{B/G,C/V\}}$ & $\tt \{B/G,C/G\} $ \\ \hline

1538: $\tt \tuple{f(C,A)}{\{C/G,A/V\}}$ & $\tt \{C/G,A/G\}$ \\\hline

1539:     \end{tabular}

1540:   \end{center}

1541: 

1542: \begin{center}

1543: \small

1544:     \begin{tabular}{|l|c|}\hline\hline

1545:     \multicolumn{2}{|c|}{\bf Dependency Table} \\ \hline

1546: \textbf{Or-Node} & \textbf{Set of Dependencies}\\ \hline

1547:  $\tt tw(B,C):\{B/G,C/V\}$ & $\tt \{ main(s^3(X),X2):\{X/G,X2/V\} \Rightarrow [main(s^4(B),A):\{B/G,A/V,C/V\}]  2,1 \}$  \\ \hline

1548: $\tt f(C,A):\{A/V,C/G\}$ & $\tt  \{ main(s^3(X),X2):\{X/G,X2/V\}  \Rightarrow

1549:              [main(s^4(B),A):\{B/G,A/V,C/G\}] 2,2\} $ \\ \hline

1550: $\tt tw(D,E):\{D/G,E/V\}$& $\tt \{\{tw(B,C):\{B/G,C/V\} \Rightarrow [tw(s(B),s^2(C):\{B/G,C/V\}]  3,1\},$  \\

1551:        \hline

1552: & \{$\tt \tt  f(D,E):\{D/G,E/V\} \Rightarrow [f(s(B),s^6(C)):\{B/G,C/V\}]  5,1\}\}$  \\\hline

1553: 

1554:     \end{tabular}

1555:   \end{center}

1556: 

1557: Note that there is an entry in the answer table for each abstract atom which

1558: appear in the graph. The dependencies correspond to

1559: \mycomment{complete}. The specialization table contains

1560: \mycomment{complete}. Finally, the generalization table is empty

1561: because \mycomment{complete}. 

1562: 

1563: \end{example}

1564:  

1565: } %% short

1566: 

1567: 

1568: 

1569: \short{

1570: Finiteness of the program analysis

1571: graph (and thus termination of the algorithm) is achieved by

1572: considering description domains with certain characteristics (such as

1573: being finite, or of finite height, or without infinite ascending

1574: chains) or by the use of a {\em widening} operator \cite{Cousot77-short}.

1575: The graph has two sorts of nodes: those belonging to clauses (also

1576: called ``AND-nodes'') and those belonging to atoms (also called

1577: ``OR-nodes'').  

1578: %% These clauses are annotated by descriptions at each

1579: %% program point of the constraint store when the clause is executed from

1580: %% the calling pattern of the node connected to the clauses. The program

1581: %% points are at the entry to the clause, the point between each two

1582: %% literals, and at the return from the call.  

1583: Atoms in the clause body have arcs to OR-nodes with the corresponding

1584: calling pattern. If such a node is already in the graph it becomes a

1585: recursive call.

1586: } %%

1587: 

1588: 

1589: \begin{algorithm}[t]

1590: \caption{Abstract Interpretation with Specialized Definitions}

1591: \label{algo:ai-with-spec-defs}

1592: %% \algorithmicinput Program $P$\\

1593: %% \algorithmicinput A global control rule \abstraction\\

1594: %% \algorithmicinput A local control rule \emph{Unfold}\\

1595: %% \algorithmicinput Set of abstract atoms of interest $S$\\

1596: %% \algorithmicoutput A partial deduction for $P$ and $S$, encoded by $H$\\

1597: 

1598: 

1599: \begin{algorithmic} [1]

1600: \renewcommand{\baselinestretch}{0.5} \sizeinfigure

1601: \Procedure{abs\_int\_with\_spec\_defs}{$P,\{A_1:CP_1,\ldots,A_n:CP_n\}$}

1602: \State \emptytable$(\at)$; \emptytable$(\dt)$

1603: \State \emptytable$(\gt)$; \emptytable$(\st)$

1604: \For{$j = 1..n$}

1605: \State  {\sc process\_call\_pattern}($A_j:CP_j,\dep{A_j:CP_j\Rightarrow{}[A_j:CP_j],j,entry}$) 

1606: \EndFor

1607: \EndProcedure

1608: \Statex

1609: \Function{process\_call\_pattern}{$A:CP,Parent$}

1610: \State $CP_1 \gets \widencall(\at,A:CP)$

1611: \If {{\bf not }\isin$(\at,A:CP_1)$}

1612: \State \store$(\at,A:CP_1,\bot)$

1613: \State \store$(\dt,A:CP_1,\emptyset)$

1614: \State $(A',A_1')\gets$ {\sc specialized\_definition}$(P,A:CP_1)$

1615: \State $A''\gets \ren(A,\{A'/A_1'\})$

1616: \ForAll  {ren. apart clause $C_k=H_k \leftarrow B_{k}\in P$

1617:   s.t. $H_k$ unifies with $A''$}

1618: \State $CP_k$ $\gets$ \acalltoentry$(A'':CP_1,C_k)$

1619: \State {\sc process\_clause}$(A:CP_1 \Rightarrow{} [H_k:CP_k]~B_{k},k,1)$

1620: \EndFor

1621: %\State $Arcs$ $\gets$ {\sc newcall\_strategy}($A_0$)

1622: \EndIf

1623: \State $Deps\gets \consult(\dt,A:CP_1)\bigcup \{Parent\}$ 

1624: \State \store$(\dt,A:CP_1,Deps$)

1625: \State \Return $\consult(\at,A:CP_1)$

1626: \EndFunction

1627: \Statex

1628: \Procedure{process\_clause}{$H:\!CP \Rightarrow  [H_k:CP_1]~B,k,i$}

1629: \If {$CP_1 \neq \bot$}

1630: \If {$B=(L,R)$}

1631: \State $CP_2 \gets \arestrict(CP_1,L)$

1632: \State $AP_0$ $\gets$ {\sc process\_call\_pattern}($L:CP_2,\dep{H:\!CP \Rightarrow  [H_k:CP_1],k,i}$)  %reversed

1633: %% \Else

1634: %% \State $AP_0$ $\gets$ {\sf Aadd}$(B_{k,i},CP_2)$

1635: %% \EndIf

1636: \State $CP_3$ $\gets$ \aconj$(CP_1,\aextend(AP_0,CP_1))$ 

1637: \State {\sc process\_clause}$(H:CP \Rightarrow [H_k:CP_3]~R,k,i+1)$  

1638: \Else 

1639: \State $CP_2 \gets \arestrict(CP_1,B)$

1640: \State $AP_0\gets$ {\sc process\_call\_pattern}($B:CP_2,\dep{H:CP \Rightarrow [H_k:CP_1],k,i}$)  %reversed

1641: %% \Else

1642: %% \State $AP_0$ $\gets$ {\sf Aadd}$(B_{k,i},CP_2)$

1643: %% \EndIf

1644: \State $CP_3$ $\gets$ \aconj$(CP_1,\aextend(AP_0,CP_1))$ 

1645: \State $AP_1$ $\gets$ \acalltoentry$(H_k:CP_3, H\leftarrow true)$ 

1646: \State $AP_2 \gets$ \consult$(\at,H:CP)$

1647: \State $AP_3 \gets$ \alub$(AP_1,AP_2)$ 

1648: \If {$AP_2 \neq AP_3$} 

1649: \State \store$(\at,H:CP,AP_3)$ 

1650: \State $Deps\gets$ \consult$(\dt,H:CP)$ 

1651: \State {\sc process\_update}($Deps$)

1652: \EndIf

1653: \EndIf

1654: \EndIf

1655: \EndProcedure

1656: \Statex

1657: \Procedure{process\_update}{$Updates$}

1658: \If {$Updates = \{A_1,\ldots,A_n\}$ with $n\geq 0$}

1659: \State $A_1=\dep{H:\!CP \Rightarrow  [H_k:CP_1],k,i}$

1660: \If {$i\neq entry$}

1661: \State $B\gets \getbody(P,k,i)$

1662: \State {\sc remove\_previous\_deps}($H:\!CP \Rightarrow  [H_k:CP_1]~B,k,i$)

1663: \State {\sc process\_clause}$(H:\!CP \Rightarrow  [H_k:CP_1]~B,k,i)$

1664: \State {\sc process\_update}($Updates - \{A_1\}$)

1665: \EndIf

1666: \EndIf

1667: \EndProcedure

1668: %% \Function {specialized\_definition}{$P,A:CP$}

1669: %% \State $A'\gets \abstraction(\st,A)$

1670: %% \State $CP'\gets {\sf update\_call}(A:CP,A')$

1671: %% \State $\store(\gt,\tuple{A}{CP},\tuple{A'}{CP'})$

1672: %% \If {\isin$(\st,A':CP')$}

1673: %% \State $p'\gets $\consult$(\st,A':CP')$

1674: %% \Else

1675: %% \State $Def\gets \aunfold(P,\tuple{A'}{CP'})$

1676: %% \State $p'\gets \newpred(pred(A'))$ 

1677: %% \State $Def'\gets \{(H' \leftarrow B) ~|~ (H\leftarrow B)\in Def\wedge

1678: %% H'=\ren(H,\{p/p'\})\}$

1679: %% \State $P\gets P\bigcup Def'$

1680: %% \State $\store(\st,\tuple{A'}{CP'},p')$

1681: %% \EndIf

1682: %% \State \Return $p'$

1683: %% \EndFunction

1684: \renewcommand{\baselinestretch}{1.0}\normalsize

1685: \end{algorithmic}

1686: \end{algorithm}

1687: 

1688: 

1689: The program analysis graph is implicitly represented in the algorithm

1690: by means of two data structures, the {\em answer table} (\at) and the

1691: {\em dependency table} (\dt).

1692: %% Given the information in these it is

1693: %% straightforward to construct the graph and the associated program

1694: %% point annotations.  

1695: The answer table contains entries of the form $A:\CP{} \leadsto

1696: \AP{}$ which  

1697: %This corresponds to an OR-node in the

1698: %analysis graph and it %of the form $\langle A:\CP{} \mapsto \AP{}\rangle$. 

1699: are interpreted as the answer (success) pattern for $A:\CP{}$ is

1700: $\AP{}$.  For instance, there exists an entry of the form $\tt

1701: main(s^3(X),X2):\{X/G,X2/V\} \leadsto \{X/G,X2/G\}$ associated to the

1702: atom discussed above.  Dependencies indicate direct relations among

1703: OR-nodes. An OR-node $A_F:CP_F$ \emph{depends on} another OR-node

1704: $A_T:CP_T$ iff in the body of some clause for $A_F:CP_F$ there appears

1705: the OR-node $A_T:CP_T$. The intuition is that in computing the answer

1706: for $A_F:CP_F$ we have used the answer pattern for $A_T:CP_T$. In our

1707: algorithm we store \emph{backwards} dependencies,\footnote{In the

1708:   implementation, for efficiency, both forward and backward

1709:   dependencies are stored. We do not include them in the algorithm for

1710:   simplicity of the presentation.} i.e., for each OR-node $A_T:CP_T$

1711: we keep track of the set of OR-nodes which depend on it. That is to

1712: say, the keys in the dependency table are OR-nodes and the information

1713: associated to each node is the set of other nodes which depend on it,

1714: together with some additional information required to iterate when an

1715: answer is modified (updated).  Each element of a \emph{dependency set}

1716: for an atom $B:CP_2$ is of the form $\dep{H:\CP{} \Rightarrow

1717:   [H_k:\CP{}_1] ~k,i}$.

1718: %% We assume that clauses in the program are written with a unique

1719: %% subscript attached to the head atom (the clause number), and dual

1720: %% subscript (clause number, body position) attached to each body

1721: %% literal, e.g., $ H_k ~\verb+:-+~ B_{k,1}, \ldots, B_{k,n_k} $ where

1722: %% $B_{k,i}$ is a subscripted atom uniquely identified as $k,i$.  The

1723: %% clause may also be referred to as clause $k$. \mycomment{explain

1724: %%   get-body}.  

1725: It should be interpreted as follows: the OR-node $H:\CP{}$ through the

1726: literal at position $k,i$ depends on the OR-node $B:CP_2$. Also, the

1727: remaining information $[H_k:\CP{}_1]$ informs that the head of this

1728: clause is $H_k$ and the substitution (in terms of all variables of

1729: clause $k$) just before the call to $B:CP_2$ is $CP_1$.  Such

1730: information avoids reprocessing atoms in the clause $k$ to the left of

1731: position $i$. For instance, the dependency set for $\tt

1732: f(C,A):\{A/V,C/G\}$ is $\tt \{ \dep{main(s^3(X),X2):\{X/G,X2/V\}

1733: \Rightarrow [main(s^4(B),A):\{B/G,A/V,C/G\}] 2,2}\}$. It indicates that

1734: the OR-node $\tt f(C,A):\{A/V,C/G\}$ is only used, via literal (2,2), in the OR-node $\tt

1735: main(s^3(X),X2):\{X/G,X2/V\}$  (see

1736: Example~\ref{ex:sp}). Thus, if the answer pattern for $\tt

1737: f(C,A):\{A/V,C/G\}$ is ever updated, then we must reprocess the

1738: OR-node $\tt \{ main(s^3(X),X2):\{X/G,X2/V\}$ from position 2,2.

1739: 

1740: \short{

1741: Intuitively, the analysis algorithm is just a graph traversal

1742: algorithm which places entries in the answer table and dependency

1743: table as new nodes and arcs in the program analysis graph are

1744: encountered.

1745: } %% short

1746: 

1747: Algorithm~\ref{algo:ai-with-spec-defs} proceeds as follows. The

1748: procedure {\sc abs\_int\_with\_spec\_defs} initializes the four tables

1749: used by the algorithm and calls {\sc process\_call\_pattern} for each

1750: abstract atom in the initial set.

1751: %

1752: The function {\sc process\_call\_pattern} applies, first of all (L7),

1753: the \widencall\ function to $A:CP$ taking into account the set of

1754: entries already in \at. This returns a substitution $CP_1$ s.t. $CP

1755: \sqsubseteq CP_1$. The most precise \widencall\ function possible is

1756: the identity function, but it can only be used with abstract domains

1757: with a finite number of abstract values. This is the case with

1758: \emph{sharing--freeness} and thus we will use the identity function in

1759: our example.

1760: %% here is no need of

1761: %% widening any call pattern in our example. 

1762: If the call pattern $A:CP_1$ has not been processed before, it places

1763: (L9) $\bot$ as initial answer in \at\/ for $A:CP$ and sets to empty

1764: (L10) the set of OR-nodes in the graph which depend on $A:CP_1$. It

1765: then computes (L11) a specialized definition for $A:CP_1$.

1766: %

1767: We do not show in Algorithm~\ref{algo:ai-with-spec-defs} the

1768: definition of {\sc specialized\_definition}, since it is identical to

1769: that in Algorithm~\ref{algo:pd-with-spec-defs}. In the graph, we show

1770: within an oval box the calls to {\sc specialized\_definition} which

1771: appear during the execution of the running example (see the details in

1772: Sect.~\ref{sec:spec-defin}). The clauses in the specialized definition

1773: are linked to the box with a dotted arc.  Then it launches (L13-15)

1774: calls to {\sc process\_clause} for the clauses in the specialized

1775: definition w.r.t. which $A:CP_1$ is to be analyzed. Only after this,

1776: the \emph{Parent} OR-node is added (L16-17) to the dependency set for

1777: $A:CP_1$.

1778: 

1779: 

1780: The function {\sc process\_clause} performs the success propagation

1781: and constitutes the core of the analysis.  

1782: %% In each recursive call, it

1783: %% performs a single step of the left-to-right traversal of a clause

1784: %% body.  

1785: First, the current answer ($\AP{}_0$) for the call to the literal at

1786: position $k,i$ of the form $B:\CP{}_2$ is (L24 and L29) conjoined

1787: (\aconj), after being extended (\aextend) to all variables in the

1788: clause, with the description $\CP{}_1$ from the program point

1789: immediately before $B$ in order to obtain the description $\CP{}_3$

1790: for the program point after $B$. If $B$ is not the last literal,

1791: $CP_3$ is taken as the (improved) calling pattern to process the next

1792: literal in the clause in the recursive call (L25). This corresponds to

1793: left-to-right success propagation and is marked in Fig.~\ref{fig:aog}

1794: with a dashed horizontal arrow.  If we are actually processing the

1795: last literal, $\CP{}_3$ is (L30) adapted (\acalltoentry) to the

1796: initial call pattern $H:CP$ which started {\sc process\_clause},

1797: obtaining $\AP{}_1$.  This value is (L32) disjoined (\alub) with the

1798: current answer, $\AP{}_2$, for $H:CP$ as given by {\consult}.  If the

1799: answer changes, then its dependencies, which are readily available in

1800: \dt, need to be recomputed (L36) using {\sc process\_update}. This

1801: procedure restarts the processing of all body postfixes which depend

1802: on the calling pattern for which the answer has been updated by

1803: launching new calls to {\sc process\_clause}.  There is no need of

1804: recomputing answers in our example.  The procedure {\sc

1805:   remove\_previous\_deps} eliminates (L42) entries in \dt\/ for the clause

1806: postfix which is about to be re-computed. We do not present its

1807: definition here due to lack of space. Note that the new calls to {\sc

1808:   process\_clause} may in turn launch calls to {\sc process\_update}.

1809: On termination of the algorithm a global fixpoint is guaranteed to

1810: have been reached. Note that our algorithm also stores in the

1811: dependency sets calls from the initial entry points (marked with the

1812: value $\mathit{entry}$ in L5). These do not need to be reprocessed

1813: (L40) but are useful for determining the specialized version to use

1814: for the initial queries after code generation.

1815: 

1816: \secbeg%\vspace{-0.1cm}

1817: \subsection{Termination of Abstract Interpretation with Specialized Definitions}

1818: \secend

1819: 

1820: Termination of Algorithm~\ref{algo:ai-with-spec-defs} comprises

1821: several levels. First, termination of the algorithm requires the local

1822: termination of the process of obtaining a specialized definition. This

1823: corresponds to ensuring termination of function {\sc

1824:   specialized\_definition} in Algorithm~\ref{algo:pd-with-spec-defs}.

1825: Second, we need to guarantee that the number of call patterns for

1826: which a specialized definition is computed is finite. This corresponds

1827: to global termination of specialization algorithms.  In terms of our

1828: algorithm, this is equivalent to having a finite number of entries in

1829: \st. The \aabstraction\ function should be able to guarantee it.

1830: Third, it is required that the set of call patterns for which an

1831: answer pattern is to be computed be finite. This corresponds to

1832: control of multivariance in context-sensitive analysis. In terms of

1833: our algorithm, this is equivalent to having a finite number of entries

1834: in \at. The \widencall\ function should be able to guarantee it.

1835: Fourth and final, it is required that the computation of the answer

1836: pattern for each entry in \at\/ needs a finite number of iterations.

1837: This is guaranteed since we consider domains which are ascending chain

1838: finite.

1839: %

1840: %% termination problems which have been studied in the contexts of

1841: %% PD and abstract interpretation. 

1842: %

1843: %% \vspace{-0.1cm}

1844: %% 

1845: %% \begin{theorem}[termination]

1846: %%   Let $\aunfold$, $\aabstraction$ and $\widencall$ be terminating

1847: %%   operators. Then, Algorithm~\ref{algo:ai-with-spec-defs} terminates.

1848: %% \end{theorem}\vspace{-0.1cm}

1849: Another way of looking at this problem is that, intuitively, the

1850: combined effect of terminating \aunfold\ and \aabstraction\ operators

1851: guarantee that the set of specialized definitions which

1852: Algorithm~\ref{algo:ai-with-spec-defs} will compute for an initial set

1853: of atoms is finite. These two problems have received considerable

1854: attention by the PD community (see, e.g.,

1855: \cite{LeuschelBruynooghe:TPLP02}).

1856: %

1857: Since

1858: Algorithm~\ref{algo:ai-with-spec-defs} performs analysis of the program

1859: composed of the set of specialized definitions, once we have

1860: guaranteed the finiteness of the program to be analyzed, a terminating

1861: \widencall\ together with an abstract domain which is ascending chain

1862: finite guarantee termination of the whole process.

1863: %

1864: \comment{GP: maybe there is no room for this other explanation

1865: Another way of looking at this problem is that if we have a

1866: terminating \aunfold\ rule and the abstract domain is ascending chain

1867: finite, non-termination can only occur if the set of call patterns

1868: handled by the algorithm is infinite. 

1869: %

1870: Since the \widencall\ function guarantees that a given concrete atom

1871: $A$ can only be analyzed w.r.t. a finite number of abstract

1872: substitutions $CP$, non-termination can only occur if the set the set

1873: of atoms has infinite elements with different concrete parts. 

1874: %

1875: If the \aabstraction\ function guarantees that an infinite number of

1876: different concrete atoms cannot occur, then non-termination cannot

1877: occur.

1878: }

1879:  

1880: %% \secbeg

1881: %% \section{Interpreting the Results of the Algorithm}

1882: %% \secend

1883: %%  \label{sec:code-generation}

1884:  

1885: %%  \input codegen

1886:  

1887:  

1888:  

1889: \secbeg

1890: \section{Discussion and Related Work}

1891: \secend

1892:  \label{sec:disc-relat-work}

1893: 

1894: 

1895: We have presented a generic framework for the analysis and

1896: specialization of logic programs which is currently the basis of the

1897: analysis/specialization system implemented in the \ciaopp\ 

1898: preprocessor. We argue that, in contrast to other approaches, the fact

1899: that our method can be used both as a specializer and analyzer gives

1900: us more accuracy and efficiency than the individual techniques.

1901: Indeed, the versatility of our framework (and of our implementation)

1902: can be seen by recasting well-known specialization and analysis

1903: frameworks as instances in which the different parameters:

1904: %\begin{itemize}

1905: %\item 

1906: unfolding rule, 

1907: %\item 

1908: widen call rule,

1909: %\item

1910: abstraction operator,

1911: %\item 

1912: %abstract executability,

1913:  and

1914: %\item 

1915: analysis domain, take the following values.

1916: %\end{itemize}

1917: %\begin{description}

1918: 

1919: \secbeg

1920: \paragraph{Polyvariant Abstract Interpretation:} Our algorithm can behave

1921: as the analysis algorithm described in

1922: \cite{incanal-toplas,inc-fixp-sas-short} for polyvariant static

1923: analysis by defining a $\aabstraction$ operator which returns always

1924: the base form of an expression (i.e., it loses all constants) and an

1925: $\aunfold$ operator which performs a single derivation step (i.e., it

1926: returns the original definition). Thus, the resulting framework would

1927: always produce a residual program which coincides with the original

1928: one and can be analyzed with any abstract domain of interest.

1929: %. The analysis

1930: %  results for the original program can nevertheless be still accurate

1931: %  (as \cite{incanal-toplas} has been demonstrated to be an accurate

1932: %  analyzer).

1933:   

1934: \secbeg

1935: \paragraph{Multivariant Abstract Specialization:} The specialization power

1936: of the framework described in \cite{spec-inv-pepm03-short,spec-jlp-short} can be

1937: obtained by using the same $\aabstraction$ described in the above point

1938: plus an $\aunfold$ operator which always performs a derive step

1939: followed by zero or more abstract execution steps.

1940: %

1941: It is interesting to note that in the original framework abstract

1942: executability is performed as an offline optimization phase while it

1943: is performed online in our framework.

1944:   

1945: \secbeg

1946: \paragraph{Classical Partial Deduction:} Our method can be used to perform

1947: classical PD in the style of

1948: \cite{Lloyd91,gallagher:pepm93-short} by using an abstract domain with the

1949: single abstract value $\top$ and the identity function as \widencall\ 

1950: rule. This corresponds to the ${\cal PD}$ domain

1951: of~\cite{leuschel04:Toplas} in which an atom with variables represents

1952: all its instances.  Let us note that, in spite of the fact that the

1953: algorithm follows a left-to-right computation flow, the process of

1954: generating specialized definitions (as discussed in

1955: Section~\ref{sec:unfold-with-abstr}) can perform \emph{non-leftmost}

1956: unfolding steps and achieve optimizations as powerful as in PD.

1957:   

1958: \secbeg

1959: \paragraph{Abstract Partial Deduction:}  Several approaches  have been

1960: proposed which extend PD by using abstract

1961: substitutions~\cite{leuschel-jicslp98,Gallagher-Peralta-HOSC,leuschel-gruner-loprstr2001-short,leuschel04:Toplas}.

1962: In essence, such approaches are very similar to the abstract partial

1963: deduction with call propagation shown in

1964: Algorithm~\ref{algo:pd-with-spec-defs}. Though all those proposals

1965: identify the need of propagating success substitutions, they either

1966: fail to do so or propose means for propagating success information

1967: which are not fully integrated with the APD algorithm and, in our

1968: opinion, do not fit in as nicely as the use of and--or trees. Also,

1969: these proposals are either strongly coupled to a particular (downward

1970: closed) abstract domain, i.e., regular types, as in

1971: \cite{Gallagher-Peralta-HOSC,leuschel-gruner-loprstr2001-short} or do

1972: not provide the exact description of operations on the abstract domain

1973: which are needed by the framework, other than general correctness

1974: criteria~\cite{leuschel-jicslp98,leuschel04:Toplas}. However, the

1975: latter allow conjunctive PD, which is not available in our framework.

1976: 

1977:   

1978: \secbeg

1979: \paragraph{The approach in~\cite{pe-in-plai-pepm99-short}:} was a starting step

1980:   towards our current framework.

1981: %% noticed the

1982: %%   difficulties of the use of SLD semantics for performing

1983: %%   specialization while capturing abstract information and proposed a

1984: %%   completely different approach based on and--or tree semantics,

1985: %% , which

1986: %%   is the semantics used in the majority of practical top-down

1987: %%   approaches to abstract interpretation of logic programs. 

1988:   There, the introduction of unfolding steps directly 

1989:   in the and--or graph was proposed in order to achieve

1990:   transformations as powerful 

1991:   as those of PD while at the same time propagating abstract

1992:   information.

1993: %%   Unfortunately, such approach, though

1994: %%   appealing was not successful in practice since a good number of

1995: %%   questions still remain open, such as the order in which to perform

1996: %%   unfolding steps and success propagation. 

1997:   In contrast, we now resort to augmented SLD semantics for the

1998:   specialization side of the framework while using AND-OR semantics

1999:   for the analysis side of the framework.  This has both conceptual,

2000:   the hybrid approach we propose provides satisfactory answers to the

2001:   four issues raised in Section~\ref{sec:motivation}, and practical

2002:   advantages, since the important body of work in control of PD is

2003:   directly applicable to the specialization side of our framework.

2004: %%  by

2005: %%   resorting to augmented SLD semantics for the specialization side of

2006: %%   the framework while using AND-OR semantics for the analysis side of

2007: %%   the framework.  

2008: %% %

2009: %  This has both conceptual and practical advantages.

2010: %\end{description}

2011: 

2012:  

2013: 

2014: \secbeg

2015: \section{Conclusions}

2016: \secend

2017:  \label{sec:benefits-or-our}

2018: 

2019: 

2020: We have proposed a novel scheme for a seamless integration of the

2021: techniques of abstract interpretation and partial deduction.  Our

2022: scheme is parametric w.r.t.\ the abstract domain and the control

2023: issues which guide the partial deduction process.  Existing proposals

2024: for the integration use abstract interpretation as a \emph{means} for

2025: improving partial evaluation rather than as a \emph{goal}, at the same

2026: level as producing a specialized program.  This implies that, as a

2027: result, their objective is to yield a set of atoms which determines a

2028: partial evaluation rather than to compute a safe approximation of its

2029: success.  Unlike them, a main objective of our work is to improve

2030: success information by analyzing the specialized code, rather than the

2031: original one. We achieve this objective by smoothly

2032: \emph{interleaving} both techniques which improves

2033: success information---even for abstract domains which are not related

2034: directly to partial evaluation. Moreover, with more accurate

2035: success information, we can improve further the quality of partial

2036: evaluation.  The overall method thus yields not only a specialized

2037: program but also a safe approximation of its behaviour.

2038: 

2039: 

2040: \comment{

2041: 

2042: Our new framework conceptually distinguishes two interleaved phases:

2043: one in which specialized definitions are computed and a second one in

2044: which success substitutions are obtained by traversing such

2045: specialized definitions from left to right until a global fixpoint is

2046: reached.

2047: 

2048: In some examples, we observed that by applying \emph{several}

2049: consecutive times a sequence of the above individual techniques we can

2050: achieve the same effect than by applying \emph{once} our algorithm.

2051: %% \begin{example}

2052: %% \mycomment{Write an example..}

2053: %% 

2054: %% \end{example}

2055: The intuition is that after unfolding we can improve the analysis

2056: information which at the same time will improve unfolding in the next

2057: iteration. There are two lines of ongoing research related to this

2058: issue. First, we are currently studying whether the number of

2059: iterations that the individual techniques have to be applied is

2060: actually bounded. Then, we also want to compare the efficiency of our

2061: technique with the application consecutive of the individual

2062: techniques.

2063: 

2064: The benefits of our approach can be seen from two perspectives, from

2065: the point of view of analysis and from that of program

2066: specialization. 

2067: 

2068: Though our approach can be thought of as a powerful specialization

2069: method, it also brings quite important benefits to program

2070: analysis. The success substitutions computed by our algorithm by using

2071: specialized definitions instead of the original ones, not only is

2072: guaranteed to achieve correct results, but also will in general

2073: achieve more accurate results. The alternative to computing

2074: specialized definitions in order to achieve success substitutions of

2075: comparable accuracy is to use abstract domains which capture precise

2076: values of variables, terms, etc. A possible choice is the use of

2077: abstract domain based on regular types. Since our algorithm is

2078: context-sensitive and polyvariant, such domains require the use of a

2079: non-trivial polyvariance control, in our algorithm represented by the

2080: \widencall\ function, in order to guarantee termination since the

2081: number of different call patterns for a same predicate is potentially

2082: infinite. 

2083: 

2084: When the program or the initial descriptions contain relatively large

2085: amounts of \emph{concrete} data, analysis using regular types either

2086: loses precision very quickly in order to guarantee efficiency (for

2087: example, by being monovariant on calls) or become impractical. Another

2088: difficulty related to the use of abstract interpretation only is that

2089: there is very quickly no way to distinguish whether abstract

2090: substitution originate from concrete data in the program and/or

2091: initial descriptions or from previous computation of success

2092: substitutions. In our experience this distinction is important since

2093: concrete data should be consumed during computation of specialized

2094: definitions, whereas abstract information can be treated more

2095: conservatively in order to keep the cost of analysis within reasonable

2096: bounds. 

2097: 

2098: From the point of view of specialization, the possibility of having

2099: context-sensitive success information is very important.  It fits very

2100: nicely in the framework of call propagation. Moreover, it may be the

2101: case that context-sensitive analysis may provide a higher degree of

2102: accuracy which may be crucial in order to enable certain

2103: specializations.

2104: 

2105: }

2106: 

2107: \vspace{-0.5cm} 

2108: \secbeg

2109: \subsection*{Acknowledgments}

2110: \secend

2111: 

2112: \begin{small}

2113: %% \noindent

2114: %%   \textbf{Acknowledgments:} 

2115: The authors would like to thank John Gallagher and Michael Leuschel

2116: for useful discussions on the integration of abstract interpretation

2117: and partial deduction.

2118: %\short{

2119:  This work was

2120:   funded in part by the Information Society Technologies programme of

2121:   the European Commission, Future and Emerging Technologies under the

2122:   IST-2001-38059 {\em ASAP} project and by the Spanish Ministry of

2123:   Science and Education under the MCYT TIC 2002-0055 {\em CUBICO}

2124:   project.

2125: %

2126:   Manuel Hermenegildo is also supported by the Prince of Asturias

2127:   Chair in Information Science and Technology at UNM.2

2128: %}

2129: \end{small}

2130: \vspace{-0.5cm} 

2131: \secbeg

2132: \secbeg

2133: %\bibliographystyle{plain}

2134: %\bibliography{/home/clip/bibtex/clip/clip,/home/clip/bibtex/clip/general,/home/clip/bibtex/soton/michael}

2135: \begin{thebibliography}{10}

2136: 

2137: \bibitem{bruy91}

2138: M.~Bruynooghe.

2139: \newblock {A} {P}ractical {F}ramework for the {A}bstract {I}nterpretation of

2140:   {L}ogic {P}rograms.

2141: \newblock {\em Journal of Logic Programming}, 10:91--124, 1991.

2142: 

2143: \bibitem{Consel-Koo:toplas93}

2144: C.~Consel and S.C. Koo.

2145: \newblock Parameterized partial deduction.

2146: \newblock {\em ACM Transactions on Programming Languages and Systems},

2147:   15(3):463--493, July 1993.

2148: 

2149: \bibitem{Cousot77-short}

2150: P.~Cousot and R.~Cousot.

2151: \newblock {A}bstract {I}nterpretation: a {U}nified {L}attice {M}odel for

2152:   {S}tatic {A}nalysis of {P}rograms by {C}onstruction or {A}pproximation of

2153:   {F}ixpoints.

2154: \newblock In {\em Proc. of POPL'77}, pages 238--252, 1977.

2155: 

2156: \bibitem{Cousot02-short}

2157: P.~Cousot and R.~Cousot.

2158: \newblock {S}ystematic {D}esign of {P}rogram {T}ransformation {F}rameworks by

2159:   {A}bstract {I}nterpretation.

2160: \newblock In {\em Proc. of POPL'02}, pages 178--190. ACM, 2002.

2161: 

2162: \bibitem{gallag88}

2163: J.~Gallagher, M.~Codish, and E.~Shapiro.

2164: \newblock {S}pecialisation of {P}rolog and {FCP} {P}rograms {U}sing {A}bstract

2165:   {I}nterpretation.

2166: \newblock {\em New Generation Computing}, 6(2--3):159--186, 1988.

2167: 

2168: \bibitem{Gallagher-Peralta-HOSC}

2169: J.~P. Gallagher and J.~C. Peralta.

2170: \newblock Regular tree languages as an abstract domain in program

2171:   specialisation.

2172: \newblock {\em Higher Order and Symbolic Computation}, 14(2,3):143--172, 2001.

2173: 

2174: \bibitem{gallagher:wsa92}

2175: J.P. Gallagher.

2176: \newblock {S}tatic {A}nalysis for {L}ogic {P}rogram {S}pecialization.

2177: \newblock In {\em Workshop on Static Analysis WSA'92}, pages 285--294, 1992.

2178: 

2179: \bibitem{gallagher:pepm93-short}

2180: J.P. Gallagher.

2181: \newblock Tutorial on specialisation of logic programs.

2182: \newblock In {\em Proc. of PEPM'93}, pages 88--98. ACM Press, 1993.

2183: 

2184: \bibitem{incanal-toplas}

2185: M.~Hermenegildo, G.~Puebla, K.~Marriott, and P.~Stuckey.

2186: \newblock {I}ncremental {A}nalysis of {C}onstraint {L}ogic {P}rograms.

2187: \newblock {\em ACM Transactions on Programming Languages and Systems},

2188:   22(2):187--223, March 2000.

2189: 

2190: \bibitem{jones-pe-ai97}

2191: N.~D. Jones.

2192: \newblock {C}ombining {A}bstract {I}nterpretation and {P}artial {E}valuation.

2193: \newblock In {\em Static Analysis Symposium}, number 1140 in LNCS, pages

2194:   396--405. Springer-Verlag, 1997.

2195: 

2196: \bibitem{pevalbook93}

2197: N.D. Jones, C.K. Gomard, and P.~Sestoft.

2198: \newblock {\em {P}artial {E}valuation and {A}utomatic {P}rogram {G}eneration}.

2199: \newblock Prentice Hall, New York, 1993.

2200: 

2201: \bibitem{leuschel-jicslp98}

2202: M.~Leuschel.

2203: \newblock {P}rogram {S}pecialisation and {A}bstract {I}nterpretation

2204:   {R}econciled.

2205: \newblock In {\em Joint International Conference and Symposium on Logic

2206:   Programming}, June 1998.

2207: 

2208: \bibitem{leuschel04:Toplas}

2209: M.~Leuschel.

2210: \newblock A framework for the integration of partial evaluation and abstract

2211:   interpretation of logic programs.

2212: \newblock {\em ACM Transactions on Programming Languages and Systems},

2213:   26(3):413 -- 463, May 2004.

2214: 

2215: \bibitem{LeuschelBruynooghe:TPLP02}

2216: M.~Leuschel and M.~Bruynooghe.

2217: \newblock Logic program specialisation through partial deduction: Control

2218:   issues.

2219: \newblock {\em Theory and Practice of Logic Programming}, 2(4 \& 5):461--515,

2220:   July \& September 2002.

2221: 

2222: \bibitem{leuschel-gruner-loprstr2001-short}

2223: M.~Leuschel and S.~Gruner.

2224: \newblock Abstract conjunctive partial deduction using regular types and its

2225:   application to model checking.

2226: \newblock In {\em Proc. of LOPSTR}, number 2372 in LNCS. Springer, 2001.

2227: 

2228: \bibitem{LeuschelEtAl:TPLP03}

2229: M.~Leuschel, J.~J{\o}rgensen, W.~Vanhoof, and M.~Bruynooghe.

2230: \newblock Offline specialisation in {P}rolog using a hand-written compiler

2231:   generator.

2232: \newblock {\em Theory and Practice of Logic Programming}, 4(1):139--191, 2004.

2233: 

2234: \bibitem{LeuschelDeSchreye:PLILP96-short}

2235: Michael Leuschel and De~Schreye.

2236: \newblock Logic program specialisation: How to be more specific.

2237: \newblock In {\em Proc. of PLILP'96}, LNCS 1140, pages 137--151, 1996.

2238: 

2239: \bibitem{Lloyd87}

2240: J.W. Lloyd.

2241: \newblock {\em Foundations of Logic Programming}.

2242: \newblock Springer, second, extended edition, 1987.

2243: 

2244: \bibitem{Lloyd91}

2245: J.W. Lloyd and J.C. Shepherdson.

2246: \newblock {P}artial {E}valuation in {L}ogic {P}rogramming.

2247: \newblock {\em Journal of Logic Programming}, 11(3--4):217--242, 1991.

2248: 

2249: \bibitem{inc-fixp-sas-short}

2250: G.~Puebla and M.~Hermenegildo.

2251: \newblock {O}ptimized {A}lgorithms for the {I}ncremental {A}nalysis of {L}ogic

2252:   {P}rograms.

2253: \newblock In {\em Proc. of SAS'96}, pages 270--284. Springer LNCS 1145, 1996.

2254: 

2255: \bibitem{spec-jlp-short}

2256: G.~Puebla and M.~Hermenegildo.

2257: \newblock {A}bstract {M}ultiple {S}pecialization and its {A}pplication to

2258:   {P}rogram {P}arallelization.

2259: \newblock {\em J.~of Logic Programming.}, 41(2\&3):279--316, November 1999.

2260: 

2261: \bibitem{spec-inv-pepm03-short}

2262: G.~Puebla and M.~Hermenegildo.

2263: \newblock {A}bstract {S}pecialization and its {A}pplications.

2264: \newblock In {\em Proc. of PEPM'03}, pages 29--43. {ACM} {P}ress, 2003.

2265: \newblock Invited talk.

2266: 

2267: \bibitem{pe-in-plai-pepm99-short}

2268: G.~Puebla, M.~Hermenegildo, and J.~Gallagher.

2269: \newblock {A}n {I}ntegration of {P}artial {E}valuation in a {G}eneric

2270:   {A}bstract {I}nterpretation {F}ramework.

2271: \newblock In {\em Proc. of PEPM'99}, number NS-99-1 in BRISC Series, pages

2272:   75--85. University of Aarhus, Denmark, 1999.

2273: 

2274: \end{thebibliography}

2275: 

2276: 

2277: 

2278: %%  \section{Termination Issues}

2279: %%  \label{sec:termination}

2280: %%  \input term-final

2281: 

2282: 

2283: %\appendix

2284: 

2285: %\section{Algorithm for Code Generation}

2286: 

2287: %\input alg-codegen

2288: 

2289: \end{document}

2290: 

2291: