popl05

Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules: 

Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules Sorin Lerner* Todd Millstein** Erika Rice* Craig Chambers* * University of Washington ** UCLA [graduating this year!]

A traditional compiler: 

A traditional compiler Parser Code Gen Compiler Opt Opt Opt

Using a domain specific language: 

Using a domain specific language Parser Code Gen Compiler DSL Opt DSL Opt DSL Opt

Using a domain specific language: 

Using a domain specific language Parser Code Gen Compiler DSL Execution engine DSL Opt DSL Opt DSL Opt

Checking correctness automatically: 

Checking correctness automatically Parser Code Gen Compiler DSL Execution engine DSL Opt DSL Opt DSL Opt

Checking correctness automatically: 

Checking correctness automatically Parser Code Gen Compiler DSL Execution engine

Checking correctness automatically: 

Checking correctness automatically Checker

Checking correctness automatically: 

DSL Opt Checking correctness automatically Checker

Checking correctness automatically: 

DSL Opt Checking correctness automatically

Checking correctness automatically: 

Checking correctness automatically VCGen Verification Condition (VC) Checker DSL Opt

Checking correctness automatically: 

Checking correctness automatically VCGen DSL Opt Checker Verification Condition (VC)

Checking correctness automatically: 

Checking correctness automatically Checker Lemma: VC implies correctness VC

Cobalt: 

Cobalt The Cobalt DSL is an instantiation of this architecture An opt written in Cobalt is a rewrite rule triggered by a declarative global condition over the CFG Expressed and automatically proved the correctness of a variety of intraprocedural optimizations, including: const prop and folding, branch folding, CSE, PRE, DAE, partial DAE [PLDI 03]

In this talk: the Rhodium DSL: 

In this talk: the Rhodium DSL Increased expressiveness New model for expressing opts: local propagation rules with explicit dataflow facts Heap summaries Infinite analysis domains Flow-sensitive and -insensitive Intraprocedural and interprocedural Some Rhodium opts not expressible in Cobalt: Arithmetic invariant detection, integer range analysis, loop-induction-variable strength reduction, Andersen's may-point-to analysis with allocation-site summaries

Outline: 

Outline Overview Rhodium by example Checking correctness automatically Future work, related work and conclusion

MustPointTo analysis: 

MustPointTo analysis c := a a := andamp;b *c := d

MustPointTo info in Rhodium: 

MustPointTo info in Rhodium c := a a := andamp;b *c := d

MustPointTo info in Rhodium: 

MustPointTo info in Rhodium c := a a := andamp;b *c := d c := a a := andamp;b *c := d

MustPointTo info in Rhodium: 

MustPointTo info in Rhodium define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d

Propagating facts: 

Propagating facts c := a a := andamp;b *c := d define fact mustPointTo(X:Var,Y:Var)

Propagating facts: 

if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d mustPointTo (a, b) mustPointTo (c, d) if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out a := andamp;b mustPointTo (a, b)

Propagating facts: 

if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d

Propagating facts: 

if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d mustPointTo (a, b) mustPointTo (c, d) mustPointTo (c, d) if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out a := andamp;b mustPointTo (c, d) mustPointTo (c, d)

Propagating facts: 

if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d mustPointTo (a, b) mustPointTo (c, d) mustPointTo (a, b) mustPointTo (c, b) if mustPointTo(X,Y)@in Æ currStmt = [Z := X] then mustPointTo(Z,Y)@out c := a mustPointTo (a, b) mustPointTo (c, b)

Propagating facts: 

if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Propagating facts if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d if mustPointTo(X,Y)@in Æ currStmt = [Z := X] then mustPointTo(Z,Y)@out

Transformations: 

if currStmt = [X := andamp;Y] then mustPointTo(X,Y)@out Transformations if mustPointTo(X,Y)@in Æ currStmt = [Z := andamp;W] Æ X  Z then mustPointTo(X,Y)@out define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d

Transformations: 

*c := d Transformations define fact mustPointTo(X:Var,Y:Var) c := a a := andamp;b *c := d mustPointTo (a, b) mustPointTo (c, b) if mustPointTo(X,Y)@in Æ currStmt = [*X := Z] then transform to [Y := Z] mustPointTo (c, b) b := d

Semantics of a Rhodium opt: 

Semantics of a Rhodium opt Run all the propagations rules using optimistic iterative analysis starting with complete set of facts until the best fixed point is reached Then run all transformation rules For better precision, combine analyses and transformations using our previous composition framework [POPL 02]

More in Rhodium (see paper for details): 

More in Rhodium (see paper for details) Mixing facts Heap summaries MayPointTo analysis via MustNotPointTo Infinite domains Flow-sensitive and -insensitive Intraprocedural and interprocedural

Outline: 

Outline Overview Rhodium by example Checking correctness automatically Future work, related work and conclusion

Rhodium correctness checker: 

Rhodium correctness checker Automatic theorem prover Checker opt- independent VCGen VC Lemma: VC ) correctness Rhodium optimization

Rhodium correctness checker: 

Rhodium correctness checker Automatic theorem prover Checker opt- independent VCGen Rhodium optimization define fact … if … then transform … if … then … VC Lemma: VC ) correctness

Rhodium correctness checker: 

Rhodium correctness checker Automatic theorem prover Rhodium optimization Checker opt- independent Lemma: VC ) correctness define fact … if … then transform … if … then … VCGen Local VC Local VC Lemma: Local VCs ) correctness

Local correctness of prop. rules: 

Local correctness of prop. rules define fact mustPointTo(X:Var,Y:Var) Z := X currStmt = [Z := X] then mustPointTo(Z,Y)@out if mustPointTo(X,Y)@in Æ

Local correctness of prop. rules: 

define fact mustPointTo(X:Var,Y:Var) Local correctness of prop. rules currStmt = [Z := X] then mustPointTo(Z,Y)@out Z := X Z := X in out Local VC sent to ATP: if mustPointTo(X,Y)@in Æ

Local correctness of trans. rules: 

Local correctness of trans. rules define fact mustPointTo(X:Var,Y:Var) if mustPointTo(X,Y)@in Æ currStmt = [*X := Z] then transform to [Y := Z] with meaning « X == andamp;Y ¬ then if « X == andamp;Y ¬ (in) Æ *X := Z in out Y := Z in out *X := Z *X := Z out ? Y := Z out Y := Z Local VC sent to ATP:

More on correctness (see paper for details): 

More on correctness (see paper for details) Heap summaries Separating profitability from correctness Theorem stating soundness of the framework for creating interprocedural and flow-insensitive analyses

Outline: 

Outline Overview Rhodium by example Checking correctness automatically Future work, related work and conclusion

Current and future work: 

Current and future work Backward optimizations Infer rules from just the dataflow fact declarations and their meanings Debugging Efficient execution engine

Some related work: 

Some related work Proving correctness by hand Abstract interpretation [Cousot and Cousot 77, 79] Partial equivalence relations [Benton 04] Temporal logic [Lacey et al. 02] Proving correctness with interactive theorem prover Using Coq proof assistant [Cachera et al. 04] Testing correctness one compilation at a time Translation validation [Pnueli et al. 98, Necula 00] Credible compilation [Rinard 99] Execution engines Incremental execution of transformations [Sittampalam et al. 04] Running opts specified with temporal logic [Steffen 91]

Conclusion: 

Conclusion Local rules in Rhodium are more expressive than Cobalt’s global condition The correctness checker found subtle bugs in our Rhodium opts Good step towards pushing more of the burden of writing compilers on to the computer