UNIVERSITY OF CALIFORNIA, SAN DIEGO Computer Science


Download UNIVERSITY OF CALIFORNIA, SAN DIEGO Computer Science


Preview text

UNIVERSITY OF CALIFORNIA, SAN DIEGO
Liquid Types
A dissertation submitted in partial satisfaction of the requirements for the degree Doctor of Philosophy
in Computer Science
by
Patrick Rondon
Committee in charge: Professor Ranjit Jhala, Chair Professor Samuel R. Buss Professor Sorin Lerner Professor Jens Palsberg Professor Geoffrey Voelker
2012

Copyright Patrick Rondon, 2012
All rights reserved.

The dissertation of Patrick Rondon is approved, and it is acceptable in quality and form for publication on microfilm and electronically:
Chair
University of California, San Diego 2012
iii

DEDICATION
For Mom, Dad, and Claudia.
iv

EPIGRAPH Given the pace of technology, I propose we leave math to the machines and go play outside.
— Calvin
v

TABLE OF CONTENTS

Signature Page . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii

Dedication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iv

Epigraph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . v

Table of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vi

List of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . viii

List of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ix

Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . x

Vita . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xii

Abstract of the Dissertation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xiii

Chapter 1

Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1 Toward Automated Program Verification . . . . . . . . . . . . . . . . . 2 1.2 Quantified Reasoning with Refinement Types . . . . . . . . . . . . . . 5 1.3 Liquid Types: A Method for Refinement Type Inference . . . . . . . . . 7 1.4 Other Approaches to Refinement Type Inference . . . . . . . . . . . . . 8 1.5 Low-Level Liquid Types . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.6 Related Approaches to Verifying Low-Level Programs . . . . . . . . . 11 1.7 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

Chapter 2

Liquid Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.1.1 Refinement Types and Qualifiers . . . . . . . . . . . . . . . . . . 15 2.1.2 Liquid Type Inference by Example . . . . . . . . . . . . . . . . . 16 2.2 The λL Language and Type System . . . . . . . . . . . . . . . . . . . . . 22 2.2.1 Elements of λL . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.2.2 Liquid Type Checking Rules . . . . . . . . . . . . . . . . . . . . 25 2.2.3 Features of the Liquid Type System . . . . . . . . . . . . . . . . 27 2.3 Liquid Type Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.3.1 ML Types and Templates . . . . . . . . . . . . . . . . . . . . . . 30 2.3.2 Constraint Generation . . . . . . . . . . . . . . . . . . . . . . . . 31 2.3.3 Constraint Solving . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2.3.4 Features of Liquid Type Inference . . . . . . . . . . . . . . . . . 37 2.4 Implementation and Evaluation . . . . . . . . . . . . . . . . . . . . . . 38 2.4.1 DSOLVE: Liquid Types for OCaml . . . . . . . . . . . . . . . . . 38 2.4.2 Benchmark Results . . . . . . . . . . . . . . . . . . . . . . . . . . 39

Chapter 3

Low-Level Liquid Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.1.1 Physical and Refinement Types and Heaps . . . . . . . . . . . . 45 3.1.2 Low-Level Liquid Types By Example . . . . . . . . . . . . . . . 46 3.2 The NANOC Language and Type System . . . . . . . . . . . . . . . . . 53 3.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 3.2.2 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

vi

3.2.3 Typing Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 3.3 Data Structure Verification with Final Fields . . . . . . . . . . . . . . . 69
3.3.1 Final Fields Example: Memory Allocation . . . . . . . . . . . . 70 3.3.2 Linked Structure Invariants . . . . . . . . . . . . . . . . . . . . . 72 3.3.3 Formal Changes to the NANOC Type System . . . . . . . . . . . 75 3.4 Type Inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 3.4.1 Physical Type Inference . . . . . . . . . . . . . . . . . . . . . . . 80 3.4.2 Fold and Unfold Inference . . . . . . . . . . . . . . . . . . . . . 80 3.4.3 Final Field Inference . . . . . . . . . . . . . . . . . . . . . . . . . 81 3.4.4 Refinement Inference . . . . . . . . . . . . . . . . . . . . . . . . 81 3.5 Implementation and Evaluation . . . . . . . . . . . . . . . . . . . . . . 82 3.5.1 CSOLVE: Liquid Types for C . . . . . . . . . . . . . . . . . . . . 82 3.5.2 Memory Safety Benchmarks . . . . . . . . . . . . . . . . . . . . 83 3.5.3 Data Structure Benchmarks . . . . . . . . . . . . . . . . . . . . . 87

Chapter 4

Conclusions and Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 4.1 Polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 4.2 Flow-Sensitive Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . 90 4.3 Liquid Types for Dynamic Languages . . . . . . . . . . . . . . . . . . . 91

Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92

Appendix A Correctness of Liquid Type Inference . . . . . . . . . . . . . . . . . . . . . . . 99

Appendix B Dynamic Semantics of NANOC . . . . . . . . . . . . . . . . . . . . . . . . . . 118

Appendix C Soundness of NANOC Type Checking . . . . . . . . . . . . . . . . . . . . . . 123

vii

LIST OF FIGURES
Figure 2.1: Example OCaml Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Figure 2.2: Syntax of λL expressions and types . . . . . . . . . . . . . . . . . . . . . . . . 23 Figure 2.3: Rules for Liquid Type Well-Formedness . . . . . . . . . . . . . . . . . . . . . . 25 Figure 2.4: Rules for Liquid Type Checking . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Figure 2.5: Constraint Generation from λL Programs . . . . . . . . . . . . . . . . . . . . . 31 Figure 2.6: Liquid Type Inference Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Figure 3.1: Example: make string . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Figure 3.2: Example: new string . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 Figure 3.3: Example: new strings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 Figure 3.4: Syntax of NANOC programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 Figure 3.5: Syntax of NANOC types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 Figure 3.6: Well-formedness rules for NANOC . . . . . . . . . . . . . . . . . . . . . . . . . 59 Figure 3.7: Subtyping rules for NANOC . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 Figure 3.8: Subindex relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 Figure 3.9: Typing rules for pure NANOC expressions . . . . . . . . . . . . . . . . . . . . 63 Figure 3.10: Index arithmetic operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 Figure 3.11: Typing rules for standard NANOC expressions . . . . . . . . . . . . . . . . . . 65 Figure 3.12: Typing rules for NANOC heap reads and writes . . . . . . . . . . . . . . . . . 66 Figure 3.13: Non-standard typing rules for NANOC expressions . . . . . . . . . . . . . . . 67 Figure 3.14: Program Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 Figure 3.15: Final fields example: memory management . . . . . . . . . . . . . . . . . . . 71 Figure 3.16: Additions to NANOC types to support final fields . . . . . . . . . . . . . . . . 76 Figure 3.17: Determining well-formedness of refinement predicates . . . . . . . . . . . . . 76 Figure 3.18: Rules for well-formedness of NANOC types with final fields . . . . . . . . . . 77 Figure 3.19: Rules for type checking NANOC expressions with final fields . . . . . . . . . 78 Figure B.1: Small-step semantics of pure NANOC expressions . . . . . . . . . . . . . . . . 119 Figure B.2: Small-step semantics of effectful NANOC expressions . . . . . . . . . . . . . . 121 Figure B.3: Small-step semantics of NANOC programs . . . . . . . . . . . . . . . . . . . . 122 Figure C.1: Updated reference values and semantics for NANOC . . . . . . . . . . . . . . 128 Figure C.2: Updated typing rules for NANOC expressions . . . . . . . . . . . . . . . . . . 133
viii

LIST OF TABLES Table 2.1: Liquid Types Benchmark Results . . . . . . . . . . . . . . . . . . . . . . . . . . 40 Table 3.1: Low-Level Liquid Types Benchmark Results . . . . . . . . . . . . . . . . . . . 85
ix

ACKNOWLEDGEMENTS
I owe a huge thanks to my advisor, Ranjit Jhala, for all the generous and patient guidance and support as well as the insight, inspiration, good humor, and, of course, food and coffee he’s provided over the years.
Thanks to my committee members Sorin Lerner, Sam Buss, Geoff Voelker and Jens Palsberg for showing a keen interest in the work and firming up my efforts with their questions and insights.
I feel very fortunate to have spent the last few years with the incredibly talented and driven UCSD programming languages group. Thanks to all of you for hearing out my half-baked ideas, reading my half-written drafts, and sitting through my half-cocked talks; the other halves were always so much better for your input. Particular thanks are due to Sorin Lerner, who was always ready to dole out advice or lend an ear as needed.
I’ve been especially lucky to have Ming Kawaguchi, Ravi Chugh, and Alexander Bakst as collaborators and friends. Trying to keep up with them has always pushed me to go further and faster. Among non-collaborators, I owe particular thanks to Ross Tate and Zach Tatlock, who have been great friends and good or bad influences as appropriate (or inappropriate).
I’m lucky to have made a large number of friends at UCSD who have changed my life for the better in countless ways. I won’t attempt an exhaustive list, for fear of missing someone or running out of pages; you know who you are. Thanks for everything!
I’m grateful for the lifelong support and encouragement of my “generalized parents”: thanks, Mom, Dad, Uncle Ronnie, Tom, and Norah, for keeping me going. Thanks to Joseph, Vanessa, Aprille, Frank, Ryan, and Evan; if I turned out OK, it’s largely because I grew up in such good company.
Finally, much of the credit for the actual completion of this work belongs to my wife and constant coffee shop companion, Claudia, who made the bad days bearable and the good days outstanding.
Published Works Adapted in This Dissertation
Chapter 2 contains material adapted from the following publications:
Patrick Rondon, Ming Kawaguchi, Ranjit Jhala. “Liquid Types”, Proceedings of the 2008 ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), pages 159–169, 2008.
Ming Kawaguchi, Patrick Rondon, Ranjit Jhala. “DSolve: Safety Verification via Liquid Types”, Proceedings of Computer Aided Verification 2010 (CAV), pages 123–126, 2010.
The dissertation author was principal investigator on both publications. Chapter 3 contains material adapted from the following publications:
x

Preparing to load PDF file. please wait...

0 of 0
100%
UNIVERSITY OF CALIFORNIA, SAN DIEGO Computer Science