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