Exploring C Program Refinement Types with Liquid Types and Invariant Discovery
Discover the integration of Liquid Types and Refinement Types in C programming through Invariant Discovery, leading to automatically adapting C programs to fit Liquid Types. Explore challenges and solutions in expressing invariants, handling unknown aliasing, and implementing strong updates within the context of C programs.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Patrick M. Rondon, Ming Kawaguchi, RanjitJhala University of California, San Diego http://www.flickr.com/photos/fallsroad/6759129/in/set-125319/
Liquid Types x : positive int x++; Refinement Type Inference (Invariant Discovery) C Program Inferred Refinement Types (Discovered Invariants) How Do We Fit C To Liquid Types?
Challenge Solution struct string { int char *str; } len; Positive 1. Expressing Invariants? Types & Refinement Types Points To Start Of len Bytes + void init (string *s, int n) { s->len = n; s->str = malloc(n); } + strHasn t Been Set Yet 2. Temporary Violations? Strong Updates void reinit (stringlist *sl) { while (sl != NULL) { init (sl->s, random ()); sl = sl->next; } } Adapt C To Liquid Types 3. Unknown Aliasing? Check In, Check Out Discipline sl, sl->next May Alias
Liquid Types x : positive int x++; Refinement Type Inference (Invariant Discovery) Inferred Refinement Types (Discovered Invariants) C Program C Program + Types + Strong Update + Check In, Check Out Automatically Adapt C Programs To Fit Liquid Types
Basic Types Refinement Types Refinement Types And Collections Refinement Type Inference Evaluation
Offset 0 int(4, ) Offset 4 int(4, ) L Pointer To Location L At Byte Offset 0 p : ref(L, 0) struct pair { int fst; int snd; } 4-Byte Integer With Value 0 At Start Of Struct 0 : int(4, 0) At Offset 0 In L p + 0 : ref(L, 0) 4-Byte Integer With Value 4 After 4-byte int fst Pointer To Location L At Byte Offset 0 Type Given Read/Write int(4, ) 4 : int(4, 4) At Offset 4 In L p + 4 : ref(L, 4) p->fst++; p->snd++; *(p + 4)++; *(p + 0)++; Read/Write int(4, ) Pointer To Location L At Byte Offset 4
Basic Types Refinement Types Refinement Types And Collections Refinement Type Inference Evaluation
{: type | p()} type Refinement Predicate { : int(4, ) | > 0} { : ref(L, 0) | 0} Positive Integer Non-NULL Pointer Pair With snd fst Offset 0 Offset 4 L { : int(4, ) | @0} snd Field int(4, ) fst Field Denotes fst Field
Offset 0 L int(4, ) Offset 4 int L { : int(4, ) | @0} { @0} p->fst++; p->snd++; Temporary Invariant Violation Invariant Reestablished Invariant Maintained Requires Flow-Sensitivity And Strong Update
int { @0} L Change @0 to f0 Rename snd To f4 Records Same Invariant With Initial Values Named Rename fst To f0 Env. f0 : int f4 : { f0} L { = f0} { = f4}
p : ref(L, 0) Env. f0 : int f4 : { f0} L { = f0} { = f4} snd Unchanged Type { = f0} Type { = f0 + 1} Is Subsumed By: p->fst = p->fst + 1; p->fst++; L L { = f0 + 1} int { = f4} { @0} p->snd++; L { = f4 + 1} { = f0 + 1} Invariant Reestablished!
Basic Types Refinement Types Refinement Types And Collections Refinement Type Inference Evaluation
L L int int { @0} { @0} ref(L, 0) ref(L, 0) next Field Abstract Location Many Items Represented By L while (p != NULL) { p->fst++; p->snd++; p = p->next; } Their Invariants Are Locked struct pair { int fst; int snd; pair *next; } Strong Updates To Abstract Locations Are Unsound!
p All Satisfy L s Invariant Unfold p Check Out p Checked Out Lp Accessing Other Items Forbidden Only Allow Accesses To One Checked Out Lp Must Check In (Reestablish Invariant)To Check Out Another Item Fold Check In p All Satisfy L s Invariant
int { @0} L p : ref(L, 0) Unfold p while (p != NULL) { p->fst++; p->snd++; p = p->next; } Fold Ensures Validity At Iteration s End Unfold p At Loop Head Fold, Unfold Verify Collection Invariant int { @0} L { = f0} { = f4} Lp p->fst++; p->snd++; int { @0} L Lp { = f0 + 1} { = f4 + 1} Fold int { @0} L Invariant Maintained!
Basic Types Refinement Types Refinement Types And Collections Refinement Type Inference Evaluation
{R} int { f0, = 0, } { @0} {S} L L L { f0, = 0, } Unfold p * = 0 f0 = 0 {R} int { f0, = 0, } { @0} {S} L L L { f0, = 0, } Lp { = f0} { = f4} Hints For Refinement Inference Instantiate With Value Names Assign Conjunction To Variables Keep Only Valid Refinements p->fst++; p->snd++; Liquid Types Overview: 1. Unknown Refinement Variables 2. Subtyping Constraints Over Variables 3. Solve To Infer Refinements {R} int { f0, = 0, } { @0} L L {S} { f0, = 0, } { = f0 + 1} { = f4 + 1} Lp Fold {R} int { f0, = 0, } { @0} {S} L L L { f0, = 0, }
Basic Types Refinement Types Refinement Types And Collections Refinement Type Inference Evaluation
C Source void incpairs(pair *p) { while (p != NULL) { *(p + offsetOf(fst)); *(p + offsetOf(snd)); p = p->next; } } Pointer Safe! Spatial Memory Safety: Array Bounds Pointer Dereferences Field Accesses Pointer Unsafe! CSolve Hints * * = * + 1
Program Lines stringlist strcpy adpcm pmap mst power ft ks Total Hints Dyn. Checks Time (s) 1 3 13 3 1 7 2 9 39 72 77 198 250 309 620 652 742 2,920 0 0 0 0 0 2 6 7 2 4 Arrays Linked Lists Arrays 42 34 16 111 310 721 1,240 Arrays Linked Lists Arrays Arrays Linked Lists Graphs Arrays Linked Lists Graphs Arrays Graphs Arrays Linked Lists 15
Challenge Solution 1. Expressing Invariants? Types & Refinement Types 2. Temporary Violations? Strong Updates 3. Unknown Aliasing? Check In, Check Out Discipline 4. Annotation Burden? Liquid Types
