Verifying Programs with BDDs Sept. 22, 2006Verification ExampleMore ExamplesHow Can We Verify Programs?Bit-Level Program VerificationExtracting Boolean RepresentationTabular Function RepresentationAlgebraic Function RepresentationTree RepresentationOrdered Binary Decision DiagramsExample FunctionsMore Complex FunctionsSymbolic ExecutionSymbolic Execution (cont.)Counterexample GenerationSlide 16Performance: GoodPerformance: BadWhy Is Multiplication Slow?What if Multiplication were Easy?Dealing with ConditionalsDealing with LoopsEvaluationSome HistoryVerifying Programs with BDDsSept. 22, 2006Verifying Programs with BDDsSept. 22, 2006TopicsTopicsRepresenting Boolean functions with Binary Decision DiagramsApplication to program verificationclass08-bdd.ppt15-213“The course that gives CMU its Zip!”15-213, F’06– 2 –Verification ExampleVerification ExampleDo these functions produce Do these functions produce identical results?identical results?How could you find out?How could you find out?How about exhaustive testing?How about exhaustive testing?int abs(int x) { int mask = x>>31; return (x ^ mask) + ~mask + 1;}int test_abs(int x) { return (x < 0) ? -x : x; }– 3 –More ExamplesMore Examplesint addXY(int x, int y){ return x+y;}int addYX(int x, int y){ return y+x;}?=int mulXY(int x, int y){ return x*y;}int mulYX(int x, int y){ return y*x;}?=– 4 –How Can We Verify Programs?How Can We Verify Programs?TestingTestingExhaustive testing not generally feasibleCurrently, programs only tested over small fraction of possible casesFormal VerificationFormal VerificationMathematical “proof” that code is correctDid Pythagoras show that a2 + b2 = c2 by testing?abc– 5 –Bit-Level Program VerificationBit-Level Program VerificationView computer word as 32 separate bit valuesEach output becomes Boolean function of inputsabsx0x1x2•••x31y0y1y2•••y31••••••x0x1x2•••x31•••yiabsiint abs(int x) { int mask = x>>31; return (x ^ mask) + ~mask + 1;}– 6 –Extracting Boolean RepresentationExtracting Boolean RepresentationDo these functions produce Do these functions produce identical results?identical results?int bitOr(int x, int y){ return ~(~x & ~y);}int test_bitOr(int x, int y){ return x | y;}yxv1 = ~xv2 = ~yv3 = v1 & v2v4 = ~v3v5 = x | yt = v4 == v5Straight-Line Evaluation– 7 –Tabular Function RepresentationTabular Function RepresentationList every possible function valueComplexityComplexityFunction with n variables00001111001100110101010100010101x1x2x3f– 8 –Algebraic Function RepresentationAlgebraic Function Representationf(x1, x2, x3) = (x1 + x2) · x3Boolean AlgebraComplexityComplexityRepresentationDetermining properties of functionE.g., deciding whether two expressions are equivalent00001111001100110101010100010101x1x2x3fx1 · x3x2 · x3– 9 –Tree RepresentationTree RepresentationTruth Table Decision TreeVertex represents decisionFollow green (dashed) line for value 0Follow red (solid) line for value 1Function value determined by leaf valueComplexityComplexity0 0x30 1x3x20 1x30 1x3x2x100001111001100110101010100010101x1x2x3f– 10 –Ordered Binary Decision DiagramsOrdered Binary Decision DiagramsInitial Tree Reduced GraphCanonical representation of Boolean functionCanonical representation of Boolean functionTwo functions equivalent if and only if graphs isomorphicCan be tested in linear timeDesirable property: simplest form is canonical.x20 1x3x10 0x30 1x3x20 1x30 1x3x2x1(x1 + x2) · x3– 11 –Example FunctionsExample FunctionsConstantsUnique unsatisfiable functionUnique tautology10VariableTreat variableas function0 1xOdd ParityLinearrepresentationx2x3x410x4x3x2x1Typical Functionx20 1x4x1 (x1 + x2 ) · x4 No vertex labeled x3 independent of x3 Many subgraphs shared– 12 –More Complex FunctionsMore Complex Functionsb3b3a3Coutb3b2b2a2b2b2a2b3a3S3b2b1b1a1b1b1a1b2a2S2b1a0a0b1a1S1b010b0a0S0FunctionsFunctionsAdd 4-bit words a and bGet 4-bit sum SCarry output bit CoutShared RepresentationShared RepresentationGraph with multiple roots31 nodes for 4-bit adder571 nodes for 64-bit adderLinear growth!– 13 –Symbolic ExecutionSymbolic Execution(3-bit word size)xx210x110x010yy210y110y010v1 = ~xx201x101x001v2 = ~yy201y101y001– 14 –Symbolic Execution (cont.)Symbolic Execution (cont.)v3 = v1 & v2x2y201x1y101x0y001v4 = ~v3x2y210x1y110x0y010v5 = x | yx2y210x1y110x0y010t = v4 == v51– 15 –Counterexample GenerationCounterexample GenerationFind values of Find values of xx & & yy for which these for which these programs produce different resultsprograms produce different resultsint bitOr(int x, int y){ return ~(~x & ~y);}int bitXor(int x, int y){ return x ^ y;}yxv1 = ~xv2 = ~yv3 = v1 & v2v4 = ~v3v5 = x ^ yt = v4 == v5Straight-Line Evaluation– 16 –Symbolic ExecutionSymbolic Executionv4 = ~v3x2y210x1y110x0y010v5 = x ^ yx2y210y2x1y110y1x0y010y0t = v4 == v5x2y2x1y1x0y001x = 111y = 001– 17 –Performance: GoodPerformance: Goodint addXY(int x, int y){ return x+y;}int addYX(int x, int y){ return y+x;}010020030040050060070080090010000 8 16 24 32Word SizeSecondsEnumerateBDD– 18 –Performance: BadPerformance: Badint mulXY(int x, int y){ return x*y;}int mulYX(int x, int y){ return y*x;}010020030040050060070080090010000 8 16 24 32Word SizeSecondsEnumerateBDD– 19 –Why Is Multiplication Slow?Why Is Multiplication Slow?Multiplication function intractable for BDDsExponential growth, regardless of variable orderingBitsBitsAddAddMultMult44 21 15588 41 14560Multiplication-4Add-4Node Counts– 20 –What if Multiplication were Easy?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);}int one(int x, int y){ return 1;}– 21 –Dealing with ConditionalsDealing with ConditionalsDuring Evaluation, Keep Track of:During Evaluation, Keep Track of:Current Context: Under what condition would code be evaluatedDefinedness (for each variable)Has it been assigned a valueint abs(int x){ int r; if (x < 0) r = -x; else r = x; return r;}t1 = x<0xv1 = -xr = v1v2 = rr = x11t1t11!t1000t111000t1?v1:0t1?v1:xt1?v1:xContextrdefinedrvalue– 22 –Dealing with LoopsDealing with LoopsUnrollUnrollTurn into bounded sequence of conditionalsDefault limit = 33Signal runtime error if don’t complete within
View Full Document