Verification Example 15 213 The course that gives CMU its Zip int abs int x int mask x 31 return x mask mask 1 Verifying Programs with BDDs Sept 22 2006 int test abs int x return x 0 x x Topics Representing Boolean functions with Binary Decision Diagrams Do these functions produce identical results Application to program verification How could you find out How about exhaustive testing 15 213 F 06 class08 bdd ppt More Examples int addXY int x int y return x y 2 How Can We Verify Programs int addYX int x int y return y x Testing Exhaustive testing not generally feasible Currently programs only tested over small fraction of possible cases Formal Verification int mulXY int x int y return x y int mulYX int x int y return y x Mathematical proof that code is correct c a b 3 4 Did Pythagoras show that a2 b2 c2 by testing Bit Level Program Verification Extracting Boolean Representation int abs int x int mask x 31 return x mask mask 1 x0 x1 x2 y0 y1 y2 x31 5 x0 x1 x2 abs Straight Line Evaluation int bitOr int x int y return x y absi y31 x31 View computer word as 32 separate bit values Each output becomes Boolean function of inputs Tabular Function Representation x1 x2 x3 0 0 0 0 1 1 1 1 0 0 1 1 0 0 1 1 0 1 0 1 0 1 0 1 yi Do these functions produce identical results v1 x v2 y v3 v1 v2 v4 v3 v5 x y t v4 v5 6 Algebraic Function Representation x1 x2 x3 f 0 0 0 1 0 1 0 1 0 0 0 0 1 1 1 1 List every possible function value Function with n variables y int test bitOr int x int y return x y Complexity x 0 0 1 1 0 0 1 1 0 1 0 1 0 1 0 1 f 0 0 0 1 0 1 0 1 f x1 x2 x3 x1 x2 x3 Boolean Algebra x 2 x3 x 1 x3 Complexity Representation Determining properties of function z E g deciding whether two expressions are equivalent 7 8 Tree Representation Truth Table x1 x2 x3 0 0 0 0 1 1 1 1 0 0 1 1 0 0 1 1 Ordered Binary Decision Diagrams Decision Tree Initial Tree 0 1 0 1 0 1 0 1 x1 0 0 0 1 0 1 0 1 x2 x2 x3 x3 0 0 x3 x3 1 x3 0 1 0 0 Follow green dashed line for value 0 Follow red solid line for value 1 Function value determined by leaf value Unique tautology Typical Function x2 x1 x2 x4 No vertex labeled x3 x4 0 11 1 1 0 0 1 1 Two functions equivalent if and only if graphs isomorphic Desirable property simplest form is canonical More Complex Functions x Functions 0 Treat variable as function 1 Odd Parity x2 x2 x3 Linear representation x3 x4 x4 0 1 Add 4 bit words a and b Get 4 bit sum S Carry output bit Cout Shared Representation x1 independent of x3 Many subgraphs shared 0 10 Variable 1 1 x3 x3 z Can be tested in linear time Example Functions Unique unsatisfiable function 0 x3 1 Complexity 0 x3 0 x2 x2 Canonical representation of Boolean function Vertex represents decision Constants x1 x2 x3 x2 x1 x1 x1 f 0 9 Reduced Graph Graph with multiple roots 31 nodes for 4 bit adder 571 nodes for 64 bit adder Linear growth S3 Cout a3 a3 b3 b3 b3 b3 a2 a2 a2 b2 b2 b2 b2 b2 b2 a1 a1 a1 b1 b1 b1 b1 b1 b1 a0 a0 a0 S2 S1 S0 b0 0 12 b0 1 Symbolic Execution x2 x 3 bit word size x1 0 1 0 Symbolic Execution cont x0 1 0 v3 x2 v1 v2 1 y2 y1 0 1 0 0 x2 x 1 0 x1 1 v4 1 v2 0 1 y2 y 1 1 1 0 x1 x0 y1 y0 x0 0 1 y1 0 0 x2 v3 0 1 y0 y0 y2 v1 x0 y1 1 y2 y x1 v5 y0 0 1 1 0 1 0 1 0 x2 x y x1 y2 0 0 t 13 x0 y1 1 0 v4 v5 y0 1 0 1 1 14 Counterexample Generation Symbolic Execution Straight Line Evaluation int bitOr int x int y return x y v4 x Find values of x y for which these programs produce different results 15 x1 y2 y 0 v1 int bitXor int x int y return x y x2 v3 1 0 y0 1 0 t v4 v5 1 x2 x2 x y x1 x0 y2 y v3 v1 v2 v4 v3 v5 x y t v4 v5 y1 x v5 v2 x0 y2 y2 y1 y1 y0 y0 0 1 0 1 0 1 x 111 y 001 x1 y1 x0 y0 1 16 0 Performance Good Performance Bad int addXY int x int y return x y int mulXY int x int y return x y int addYX int x int y return y x 1000 1000 900 900 800 800 700 700 600 Seconds Seconds int mulYX int x int y return y x Enumerate BDD 500 400 300 600 Enumerate BDD 500 400 200 300 100 200 100 0 0 8 16 24 32 0 0 Word Size 8 16 24 32 Word Size 17 18 Why Is Multiplication Slow What if Multiplication were Easy Multiplication function intractable for BDDs z Exponential growth regardless of variable ordering Node Counts Bits Add 4 19 Multiplication 4 Add Mult 4 21 155 8 41 14560 int factorK int x int y int K XXXX X int rangeOK 1 x x y int factorOK x y K return rangeOK factorOK 20 int one int x int y return 1 Dealing with Conditionals int abs int x int r if x 0 r x else r x return r r r Context defined value x 1 0 0 t1 x 0 1 0 0 v1 x t1 0 0 r v1 t1 t1 t1 v1 0 r x t1 1 t1 v1 x v2 r 1 1 t1 v1 x Dealing with Loops int ilog2 unsigned x int r 1 while x r x 1 return r Unroll During Evaluation Keep Track of Current Context Under what condition would code be evaluated Definedness for each variable z Has it been assigned a value 21 Turn into bounded sequence of conditionals z Default limit 33 Signal runtime error if don t complete within limit Some History Strengths Origins Provides 100 guarantee of correctness Performance very good for simple arithmetic functions Important integer functions have exponential blowup Not practical for programs that build and operate on large data structures Lee 1959 Akers 1976 Hopcroft Fortune Schmidt 1978 z Idea of representing Boolean function as BDD Weaknesses int ilog2 unsigned x int r 31 if x r x 1 else return r if x r x 1 else return r if …
View Full Document
Unlocking...