Static Contract Checking for Haskell: Dynamic Contract Checking and Bug Analysis

Static Contract Checking Static Contract Checking for Haskell for Haskell Dana N. Dana N. Xu Xu University of Cambridge Ph.D. Supervisor: Simon Peyton Jones Simon Peyton Jones Microsoft Research Cambridge

From Types to Contracts head [] = BAD head (x:xs) = x BAD means should not happen: crash head :: [a] -> a Type null :: [a] -> Bool null [] = True null (x:xs) = False (head 1) Bug! head {xs | not (null xs)} -> {r | True} Contract Bug! (arbitrary Haskell boolean expression) (head [])

What we want Adapt Findler-Felleisen s ideas for dynamic (high-order) contract checking. Do static contract checking for a lazy language. Haskell function Contract Glasgow Haskell Compiler (GHC) Where the bug is Why it is a bug

Three Outcomes (1) Definitely Safe (no crash, but may loop) (2) Definite Bug (definitely crashes) (3) Possible Bug

Sorting (==>) True x = x (==>) False x = True sorted [] = True sorted (x:[]) = True sorted (x:y:xs) = x <= y && sorted (y : xs) insert :: Int -> [Int] -> [Int] insert {i | True} -> {xs | sorted xs} -> {r | sorted r} merge :: [Int] -> [Int] -> [Int] merge {xs | sorted xs}->{ys | sorted ys}->{r | sorted r} bubbleHelper :: [Int] -> ([Int], Bool) bubbleHelper {xs | True} -> {r | not (snd r) ==> sorted (fst r)} insertsort, mergesort, bubblesort {xs | True} -> {r | sorted r} 5

AVL Tree (&&) True x = x (&&) False x = False balanced :: AVL -> Bool balanced L = True balanced (N t u) = balanced t && balanced u && abs (depth t - depth u) <= 1 data AVL = L | N Int AVL AVL insert, delete :: AVL -> Int -> AVL insert {x | balanced x} -> {y | True} -> {r | notLeaf r && balanced r && 0 <= depth r - depth x && depth r - depth x <= 1 } delete {x | balanced x} -> {y | True} -> {r | balanced r && 0 <= depth x - depth r && depth x - depth r <= 1}

The Contract Idea for Higher-Order Function [Findler/Felleisen] f1 :: (Int -> Int) -> Int f1 ({x | x > 0} -> {y | y >= 0}) -> {r | r >= 0} f1 g = (g 0) - 1 Blame f1: f1 calls g with wrong argument f1 does not satisfy its post-condition f2 :: {r | True} f2 = f1 (\x -> x 5) f3 :: {r | True} f3 = f1 (\x -> x 1) Blame f2: f2 calls f1 with wrong argument f3 is Ok. Can t tell at run-time

What is a Contract? arbitrary Haskell boolean expression Ok = {x | True} Contract t ::= {x | p} Predicate Contract | x:t1 -> t2Dependent Function Contract | (t1, t2) Tuple Contract | Any Polymorphic Any Contract 3 { x | x > 0 } 3 { x | True } (3, []) (Ok, {ys | null ys}) inc x:{x | x>0} -> {y | y == x + 1} (3, []) Any arbitrary constructor Postcondition can mention argument Precondition Postcondition

What we want? Check f <contract_of_f> If main Ok , then the whole program cannot crash. If not, show which function to blame and why. Beauty of Contract Checking

[POPL10] Define e t Main Theorem e t iff e t is crash-free (related to Blume&McAllester:JFP 06) Construct e t (e ensures t) ESC/Haskell [Haskell 06] Symbolically simplify (e t) some e See if BADis syntactically in e . If yes, DONE; else give BLAME

Wrappers and ( pronounced ensures pronounced requires) e {x | p} = case p[e/x] of True -> e False -> BAD e x:t1 -> t2 = v. (e (v t1)) t2[(v t1)/x] e (t1, t2) = case e of (e1, e2) -> (e1 t1, e2 t2) e Any = UNR related to [Findler-Felleisen:ICFP02]

Wrappers and ( pronounced ensures pronounced requires) e {x | p} = case p[e/x] of True -> e False -> UNR e x:t1 -> t2 = v. (e (v t1)) t2[v t1/x] e (t1, t2) = case e of (e1, e2) -> (e1 t1, e2 t2) e Any = BAD related to [Findler-Felleisen:ICFP02]

Some Interesting Details Theory Practice Contracts that loop Contracts that crash Lovely Lemmas Adding tags, e.g. BAD f Achieves precise blaming More tags to trace functions to blame Achieves the same goal of [Meunier:POPL06] Using a theorem prover Counter-example guided unrolling

Lovely Lemmas

Summary Static contract checking is a fertile and under-researched area Distinctive features of our approach Full Haskell in contracts; absolutely crucial Declarative specification of satisfies Nice theory (with some very tricky corners) Static proofs Modular Checking Compiler as theorem prover

After Ph.D. Postdoc project in 2009: probabilistic contract for component base design [ATVA 2010] Current project at Xavier Leroy s team (INRIA) - a verifying compiler: 1. Apply the idea to OCaml compiler by allowing both static and dynamic contract checking 2. Connect with Coq to verify more programs statically. 3. Use Coq to prove the correctness of the framework. 4. Apply new ideas back to Haskell (e.g. GHC).

Static and Dynamic Program with Specifications Static checking Dynamic checking Compile time error attributes blame to the right place Run time error attributes blame to the right place Or, more plausibly: If you guarantee that f t, then the program cannot crash No blaming means Program cannot crashs

What exactly does it mean to say that e satisfies contract t? e t

When does e satisfy a contract? Brief, declarative inc x:{x | x > 0} -> {y | y == x + 1} Postcondition can mention argument Precondition Postcondition

When does e satisfy a contract? The delicate one is the predicate contract. Our decision: e {x | p} iff iff e is crash-free Question: What expression is crash-free ? e is crash-free iff no blameless context can make e crash e is crash-free iff * BAD C. BAD s C. C[e]

Crash-free Examples Crash-free? \x -> x YES (1, True) (1, BAD) \x -> if x > 0 then x else (BAD, x) \x -> if x*x >= 0 then x + 1 else BAD YES NO NO Hmm.. YES Lemma: e is syntactically safe => =>e is crash-free.

When does e satisfy a contract? See the paper for Why e must be crash-free to satisfy predicate contract? Why divergent expression satisfies all contract? What if contract diverges (i.e. p diverges)? What if contract crashes (i.e. p crashes)?

How can we mechanically check that e satisfies contract t? e t ???

Example head:: [a] -> a head [] = BAD head (x:xs) = x head { xs | not (null xs) } -> Ok head {xs | not (null xs)} -> Ok = \v. head (v {xs | not (null xs)}) Ok e Ok = e = \v. head (v {xs | not (null xs)}) = \v. head (case not (null v) of True -> v False -> UNR)

null :: [a] -> Bool null [] = True null (x:xs) = False \v. head (case not (null v) of True -> v False -> UNR) not :: Bool -> Bool not True = False not False = True Now inline not and null = \v. head (case v of [] -> UNR (p:ps) -> p) Now inline head = \v. case v of [] -> UNR (p:ps) -> p head:: [a] -> a head [] = BAD head (x:xs) = x So head [] fails with UNR, not BAD, blaming the caller

Static and Dynamic [Findler, Felleisen, Blume, Hinze, Loh, Runciman, Chitil] [Flanaghan, Mitchell, Pottier] Program with Specifications Static checking Dynamic checking Compile time error attributes blame to the right place Run time error attributes blame to the right place