A flow analysis framework for realistic scheme programs [Elektronische Ressource] / vorgelegt von Eric Jean Knauel

Eric Knauel

Sujets

• Informatik

Informations

• Publié par: eberhard_karls_universitat_tubingen
• Publié le: 01 janvier 2008
• Nombre de lectures: 22
• Poids de l'ouvrage: 1 Mo

Extrait

A flow-analysis framework for
realistic Scheme programs
Dissertation
der Fakultat¨ fur¨ Informations- und Kognitionswissenschaften
der Eberhard-Karls-Universitat¨ Tubing¨ en
zur Erlangung des Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat.)
vorgelegt von
Dipl.-Inform. Eric Jean Knauel
aus Buchholz in der Nordheide
Tubingen¨
2008Tag der mun¨ dlichen Qualifikation: 7. Mai 2008
Dekan: Prof. Dr. Michael Diehl
1. Berichterstatter: Prof. Dr. Herbert Klaeren
2. Berich Prof. Dr. Schroeder-HeisterAbstract
It is possible to scale control-flow analyses for higher-order languages to com-
plete, fully-fledged programming languages and consequently compute the flow
analysis of realistic programs. This dissertation gives a formal specification of
a universal flow-analysis framework for the functional programming languages
Scheme and PreScheme that covers all aspects and features of these languages.
Moreover, the dissertation proposes new implementation strategies and tech-
niques that have been developed and tested in context of an implementation
for Scheme 48. These techniques yield an efficient implementation that enables
analysis of realistic programs.
Zusammenfassung
Es ist moglich, Kontrollflussanalysen fur Sprachen hoherer Ordnung auf reali-¨ ¨ ¨
stische Programme anzuwenden. Diese Dissertation spezifiziert eine universell
verwendbare Flussanalyse fur die funktionalen Programmiersprachen Scheme¨
und PreScheme, die alle Aspekte und Fahigkeiten dieser Sprachen abdeckt. Fur¨ ¨
die praktische Umsetzung dieser Analyse werden neuartige Implementierungs-
strategienund-technikenvorgestellt,dieimRahmeneinerImplementierungfur¨
Scheme 48 entwickelt und erprobt wurden. Diese Techniken fuh¨ ren zu einer effi-
zienten Implementierung, welche die Analyse realistischer Programme erlaubt.4Contents
1 Introduction 9
1.1 Implementation Scalability . . . . . . . . . . . . . . . . . . . . . 9
1.2 Executable semantic model . . . . . . . . . . . . . . . . . . . . . 12
1.3 Setting the scene . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.4 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.5 Structure of this dissertation . . . . . . . . . . . . . . . . . . . . 14
2 Intermediate Language 17
2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 Printing CPS Programs . . . . . . . . . . . . . . . . . . . . . . . 22
2.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.4 Complete programs . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.4.1 Complete PreScheme programs . . . . . . . . . . . . . . . 30
2.4.2 Complete Scheme programs . . . . . . . . . . . . . . . . . 31
2.4.3 Treating complete programs . . . . . . . . . . . . . . . . . 31
2.4.4 Initial state . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3 Flow analysis of Programs 33
3.1 Control flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.2 Using control-flow information for optimization . . . . . . . . . . 35
3.3 Control-flow analysis for higher-order languages . . . . . . . . . . 36
4 Analysis Framework 39
4.1 Semantic domains . . . . . . . . . . . . . . . . . . . . . . . . . . 39
4.2 State transition . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.3 Semantic correctness . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.4 Language-specific abstractions. . . . . . . . . . . . . . . . . . . . 52
4.4.1 Abstracting PreScheme values . . . . . . . . . . . . . . . 53
4.4.2g Scheme values . . . . . . . . . . . . . . . . . 60
d4.5 Precision and Time . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.5.1 k-CFA time abstractions . . . . . . . . . . . . . . . . . . . 74
4.6 Flow analysis examples. . . . . . . . . . . . . . . . . . . . . . . . 75
5 Executable Semantic Model 83
5.1 Example trace . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
5.2 Implementation with PLT Redex . . . . . . . . . . . . . . . . . . 86
5.2.1 Grammar definition . . . . . . . . . . . . . . . . . . . . . 86
5.2.2 Metafunctions . . . . . . . . . . . . . . . . . . . . . . . . 90
56 CONTENTS
5.2.3 Reduction relations . . . . . . . . . . . . . . . . . . . . . . 100
5.2.4 Generating traces . . . . . . . . . . . . . . . . . . . . . . . 102
6 Implementation 105
6.1 Abstract syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
6.2 Semantic domains . . . . . . . . . . . . . . . . . . . . . . . . . . 106
6.2.1 Representing time . . . . . . . . . . . . . . . . . . . . . . 106
6.2.2 Representing the binding environment . . . . . . . . . . . 106
6.2.3 Representing variable environments . . . . . . . . . . . . 107
6.2.4 Representing abstract values . . . . . . . . . . . . . . . . 107
6.2.5 Implementing the visited set . . . . . . . . . . . . . . . . 112
6.3 Description of flow information . . . . . . . . . . . . . . . . . . . 114
6.4 Analysis with Garbage Collection . . . . . . . . . . . . . . . . . . 116
6.4.1 Semantics with global garbage collection . . . . . . . . . . 117
6.4.2 Abstract values with GC marks . . . . . . . . . . . . . . . 122
6.4.3 Garbage Collection and variable environment . . . . . . . 124
6.4.4 Splitting the root set . . . . . . . . . . . . . . . . . . . . . 127
6.5 Experimental results . . . . . . . . . . . . . . . . . . . . . . . . . 127
6.6 Testing and Debugging . . . . . . . . . . . . . . . . . . . . . . . . 131
7 Conclusion 133
7.1 Review . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133
7.2 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134
A Notation 137
B Semantic Correctness 139
C PreScheme Primops 149
C.1 Primops with one return value . . . . . . . . . . . . . . . . . . . 149
C.2 Pr for compound values . . . . . . . . . . . . . . . . . . . . 151
C.3 Primops with multiple return values . . . . . . . . . . . . . . . . 153
D Scheme Primops 155
D.1 Arithmetic Primops . . . . . . . . . . . . . . . . . . . . . . . . . 157
D.2 Primops for compound values . . . . . . . . . . . . . . . . . . . . 158
D.3 Procedures with rest list argument . . . . . . . . . . . . . . . . . 161
D.4 Multiple return values . . . . . . . . . . . . . . . . . . . . . . . . 162Acknowledgments
First,IthankmyadvisorProfessorHerbertKlaeren. ProfessorKlaerenprovided
a pleasant work environment and allowed me great latitude in my choice of
research activities, and agreed with this dissertation project. I thank Professor
Peter Schroeder-Heister who immediately agreed to co-review this dissertation.
I am greatly indebted to Mike Sperber. Mike was the first to direct my
attention to research in compiler construction and especially to flow analyses.
He wakened my curiosity for these subjects. I am deeply thankful that Mike
shared his extensive knowledge with me, and the time and effort he spent read-
ing the various drafts of this dissertation. Mike’s profound remarks, numerous
correctionsandsuggestions—theremainingmistakesaremine—reallyhelped
me improve this work.
My colleague Marcus Crestani deserves special thanks. Marcus not only
carefully proof-read this dissertation and suggested valuable improvements, but
also relieved me of parts of my teaching workload during the last semester.
I am grateful to Matthew Might and Olin Shivers for patiently answering
all my e-mails on flow analyses, garbage collection for flow analyses, and frame
strings. Matthew Might also gave me access to his ΔCFA and ΓCFA implemen-
tations. Matthew and Olin also shared draft versions of their latest research
results with me. For all of this, I am grateful.
I thank Robby Findler for answering my questions on PLT Redex — using
this tool to model the semantics ranks among the most pleasant parts of this
work.
Martin Gasbichler is an expert on Scheme 48 and I thank him for patiently
answering all my questions on the byte code, native code, and PreScheme com-
pilers, the virtual machine, and other aspects of this complex system. Espe-
cially, I thank Martin for helping me develop the id tables for Scheme 48. My
colleague Holger Gast was always available to help me with typesetting prob-
lems — I would probably still be struggling with strange T X problems withoutE
his help.
Frank Suh¨ l and Thomas Rasch, both close friends of mine, provided many
helpful comments and encouragement — for both I am grateful.
I am very grateful for the support from my parents Hermann and Marie-
Louise. Marie-Louise proof-read the whole work and suggested lots of linguistic
improvements. Both supported and encouraged me tireless from day one of my
studies till the end of this dissertation project.
Finally, I thank my wife Gertraud for her love, support, and patience during
the months I suffered from something she identified as the “compiling syn-
drome” — a state of mind, characterized by confusion and mental absence,
caused by long debugging sessions of flow analyses.8 CONTENTSChapter 1
Introduction
It is possible to scale control-flow analyses for higher-order languages to com-
plete, fully-fledged programming languages and consequently compute the flow
analysis of realistic programs.
Only few compilers for functional languages employ a flow analysis to gain
information on the run-time behavior of a program and subsequ