Defensive Programming Dawn Song dawnsong cs berkeley edu 1 Reasoning About Code Functions make certain assumptions about their arguments Caller must make sure assumptions are valid These are often called preconditions Precondition for f is an assertion a logical proposition that must hold at input to f Function f must behave correctly if its preconditions are met If any precondition is not met all bets are off Caller must call f such that preconditions true an obligation on the caller and callee may freely assume obligation has been met 2 Simple Precondition Example int deref int p return p Unsafe to dereference a null pointer Impose precondition that caller of deref must meet p NULL holds at entrance to deref If all callers ensure this precondition it will be safe to call deref Can combine assertions using logical connectives and or implication Also existentially and universally quantified logical formulas 3 Another Example int sum int a size t n int total 0 i for i 0 i n i total a i return total Precondition Forall j 0 j n a j NULL If you re comfortable with formal logic write your assertions this way for precision Not necessary to be so formal Goal is to think explicitly about assumptions and communicate requirements to others 4 Postconditions Postcondition for f is an assertion that holds when f returns f has obligation of ensuring condition is true when it returns Caller may assume postcondition has been established by f Example Ensures retval NULL void mymalloc size t n void p malloc n if p perror Out of memory exit 1 return p 5 Process for Writing Function Code First write down its preconditions and postconditions Specifies what obligations caller has and what caller is entitled to rely upon Verify that no matter how function is called if precondition is met at function s entrance then postcondition is guaranteed to hold upon function s return Must prove that this is true for all inputs Otherwise you ve found a bug in either specification preconditions postconditions or implementation function code 6 Proving Precondition Postcondition Basic idea Write down a precondition and postcondition for every line of code Apply same sort of reasoning as for function Requirement Each statement s postcondition must match imply precondition of any following statement At every point between two statements write down invariant that must be true at that point Invariant is postcondition for preceding statement and precondition for next one 7 Example Easy to tell if an isolated statement fits its pre and post conditions Valid postcondition for v 0 is v 0 no matter what the precondition is Or if precondition for v v 1 is v 5 then a valid postcondition is v 6 If precondition for v v 1 is w 100 then a valid postcondition is w 100 Assuming v and w do not alias 8 Loop Invariant An assertion that is true at entrance to the loop on any path through the code Must be true before every loop iteration Both a pre and post condition for the loop body Example Factorial function code Requires n 1 int fact int n int i t i 1 t 1 while i n t i i return t Prerequisite input must be at least 1 for correctness Prove value of fact is always positive 9 Verifying Invariant Correctness Requires n 1 Ensures retval 0 int fact int n int i t n 1 i 1 n 1 i 1 t 1 n 1 i 1 t 1 while i n 1 i i n t 1 loop invariant t i 1 i i n t 1 i 2 i i n 1 t 1 i n t 1 return t Easy if we examine each step Function s precondition implies invariant at function body start Invariant at end of function body implies function s postcondition If each statement matches invariant immediately before and after it everything s OK That leaves the loop invariant 10 Verifying the Loop Invariant Loop invariant 1 i i n t 1 Prove it is true at start of first loop iteration Follows from n 1 i 1 t 1 1 i n t 1 if i 1 then certainly i 1 Prove that if it holds at start of any loop iteration then it holds at start of next iteration if there s one True since invariant at end of loop body 2 i n 1 t 1 and loop termination condition i n implies invariant at start of loop body 1 i n t 1 Follows by induction on number of iterations that loop invariant is always true on entrance to loop body Thus fact will always make postcondition true as precondition is established by its caller 11 Another Example Recursion Requires n 1 int fact int n int t if n 1 return 1 t fact n 1 t n return t Do you see how to prove that this code always outputs a positive integer 12 Analysis Requires n 1 Ensures retval 0 int fact int n int t if n 1 return 1 n 2 t fact n 1 t 0 t n t 0 return t Before recursive call to fact we know n 1 by precondition n 1 since if stmt didn t follow then branch and n is an integer Follows that n 2 or n 1 1 means precondition is met when making recursive call Can conclude that fact n 1 return value is positive from postcondition for fact 13 Function Post Pre Conditions Any time we see a function call we have to verify that its precondition will be met Then we can conclude its postcondition holds and use this fact in our reasoning Annotating every function with pre and post conditions enables modular reasoning Can verify function f by looking only its code and the annotations on every function f calls Can ignore code of all other functions and functions called transitively Makes reasoning about f an almost purely local activity 14 Documentation Pre post conditions serve as useful documentation To invoke Bob s code Alice only has to look at pre and post conditions she doesn t need to look at or understand his code Useful way to coordinate activity between multiple programmers Each module assigned to one programmer and pre post conditions are a contract between caller and callee Alice and Bob can negotiate the interface and responsibilities between their code at design time 15 Avoiding Security Holes To avoid security holes or program crashes Some implicit requirements code must meet Must not divide by zero make out of bounds memory accesses or deference null ptrs We can try to prove that code meets these requirements using same style of reasoning Ex when a pointer is dereferenced there is an implicit precondition that pointer is non null and inbounds 16 Proving Array Accesses are in bounds Requires a NULL and a holds n elements int sum int a size t n int total 0 i for i 0 i n i Loop invariant 0 i n total a i return total Loop invariant true at entrance to first …
View Full Document
Unlocking...