path sas04

Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions: 

Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions SAS 2004 Sumit Gulwani George Necula EECS Department University of California, Berkeley

Slide2: 

y := 2; z := a; y := a; z := 2; u := 1; v := 1+a; t1 := y-u; t2 := v-z; True True False False Example u := a-1; v := 3; Assert(t1=t2 Æ t1=1 Æ z=2); a=2? All 3 asserts are true a=2?

Slide3: 

y := 2; z := a; y := a; z := 2; u := 1; v := 1+a; t1 := y-u; t2 := v-z; True True False False Path-Insensitive Analysis u := a-1; v := 3; Assert(t1=t2 Æ t1=1 Æ z=2); * Most PTIME analyses treat conditionals as non-deterministic. They will verify only t1=t2 *

Slide4: 

y := 2; z := a; y := a; z := 2; u := 1; v := 1+a; t1 := y-u; t2 := v-z; True True False False Path-Sensitive Analysis u := a-1; v := 3; Assert(t1=t2 Æ t1=1 Æ z=2); c1 We can do better by doing a boolean abstraction of conditionals. Each atomic predicate is abstracted to a boolean variable This will also verify t1=1 This is still abstract though! z=2 not verified undecidable to reason completely c1

Outline: 

Outline Existing approach (MVR) vs. our approach (FCED) FCEDs for linear arithmetic FCEDs for uninterpreted function terms

Slide6: 

y := 2; z := a; y := a; z := 2; u := 1; v := 1+a; t1 := y-u; t2 := v-z; True True False False Multi-Valued ROBDDs (MVRs) u := a-1; v := 3; Assert(t1=t2); Assert(t1=1); c1 c2 |MVR(t1)| = |MVR(y)| £ |MVR(u)| MVR(t1) does not share nodes with MVR(y) and MVR(u) Need a normal form for leaves

Slide7: 

y := 2; z := a; y := a; z := 2; u := 1; v := 1+a; t1 := y-u; t2 := v-z; True True False False Free Conditional Expression Diagrams (FCEDs) c1 2 a y = c2 1 a-1 u = - t1 = u := a-1; v := 3; Assert(t1=t2); Assert(t1=1); c1 c2 |FCED(t1)| = |FCED(y)| + |FCED(u)| FCED(t1) shares nodes with FCED(y) and FCED(u) No need for normal form

Outline: 

Outline Existing approach (MVR) vs. our approach (FCEDs) FCEDs for linear arithmetic FCEDs for uninterpreted function terms

Problem Definition: 

Problem Definition e = q | y | e1 § e2 | q £ e | if b then e1 else e2 b = c | b1 Æ b2 | b1 Ç b2 e: conditional linear arithmetic expression b: boolean formula y: rational variable c: boolean variable q: rational constant Construct FCED for an expression e, given FCEDs for its subexpressions. Check 2 FCEDs for equivalence

FCED: 

FCED An FCED f is a DAG with the following kind of nodes. f := y | q | Plus(f1,f2) | Minus(f1,f2) | Times(q,f) | Choose(f1,f2) | Guard(g,f) Choose(f1,f2) means f1 or f2 Guard(g,f) means if g then f Boolean expressions g are represented using ROBDDs g := true | false | c | If(c,g1,g2)

Example: 

Example Formalization

Example: 

Example Formalization

FCED Construction: 

FCED Construction FCED(y) = Leaf(y) FCED(q) = Leaf(q) FCED(e1+e2) = Plus (FCED(e1), FCED(e2)) FCED(q £ e) = Times(q,FCED(e)) FCED(if b then e1 else e2) = Choose(Guard(R(b),e1), Guard(R(NOT(b)),e2)

FCED Construction: 

FCED Construction FCED(y) = Leaf(y) FCED(q) = Leaf(q) FCED(e1+e2) = Plus (FCED(e1), FCED(e2)) FCED(q £ e) = Times(q,FCED(e)) FCED(if b then e1 else e2) = Choose(||R(b),FCED(e1)||, ||NOT R(b), FCED(e2)||)

Normalize Guard Operator: 

Normalize Guard Operator Inputs: guard g, FCED f Output: FCED f’ s.t. f ´ f’ 8 guard nodes Guard(g,f’’) in f’, BV(g) < BV(f’’) ||g,f|| = Guard(g,f), if BV(g) < BV(f) ||g, Plus(f1,f2) = Plus(||g,f1||, ||g, f2||) ||g, Choose(f1,f2) = Choose(||g,f1||, ||g, f2||) ||g1, Guard(g2,f )|| = Guard(|| INTERSECT(g1,g2),f ||) …

Example: Normalize Guard Operator: 

Example: Normalize Guard Operator plus Given f, construct ||R(c1),f|| choose

Randomized Equivalence Testing for FCEDs: 

Randomized Equivalence Testing for FCEDs Assign hash values to nodes of FCEDs in bottom-up manner V: FCED Node ! Integer V(Leaf(q)) = q V(Leaf(y)) = ry V(Plus(f1,f2)) = V(f1) + V(f2) V(Choose(f1,f2)) = V(f1) + V(f2) V(Guard(g,f)) = H(g) £ V(f) H: Guard ! Integer H(true) = 1, H(false) = 0 H(c) = rc H(If(c,g1,g2)) = rc £ H(g1) + (1-rc) £ H(g2)

Randomized Equivalence Testing for FCEDs : 

Randomized Equivalence Testing for FCEDs Completeness f1 ´ f2 ) V(f1) = V(f2) Soundness f1 ´ f2 ) Pr[V(f1) = V(f2)] · s/t s: maximum # of nodes in a FCED t: size of set from which random values are chosen Proof: 9 1-1 Poly: FCED ! Polynomials such that V(f) is the value of Poly(f)

Outline: 

Outline Existing approach (MVR) vs. our approach (FCEDs) FCEDs for linear arithmetic FCEDs for uninterpreted function terms

Problem Definition: 

Problem Definition e = y | F(e1,e2) | if b then e1 else e2 b = c | b1 Æ b2 | b1 Ç b2 e: conditional uninterpreted function term b: boolean formula y: variable c: boolean variable Construct FCED for an expression e, given FCEDs for its subexpressions. Check 2 FCEDs for equivalence

FCED: 

FCED An FCED f is a DAG with the following kind of nodes. f := y | F(f1,f2) | Choose(f1,f2) | Guard(g,f) Choose(f1,f2) means f1 or f2 Guard(g,f) means if g then f Boolean expressions g are represented using ROBDDs g := true | false | c | If(c,g1,g2)

FCED Construction: 

FCED Construction FCED(y) = Leaf(y) FCED(F(e1,e2)) = F(FCED(e1), FCED(e2)) FCED(if b then e1 else e2) = Choose(||R(b),FCED(e1)||, ||NOT R(b), FCED(e2)||)

Randomized Equivalence Testing of FCEDs: 

Randomized Equivalence Testing of FCEDs Assign hash values to nodes of FCEDs in bottom-up manner V: FCED Node ! Tuple of k integers K ¸ depth of any FCED V(y) = [ry,…ry] V(Choose(f1,f2)) = V(f1) + V(f2) V(Guard(g,f)) = H(g) £ V(f) V(F(f1,f2)) = V(f1) £ M + V(f2) £ N M, N: random k £ k matrices

Randomized Equivalence Testing for FCEDs : 

Randomized Equivalence Testing for FCEDs Completeness f1 ´ f2 ) V(f1) = V(f2) Soundness f1 ´ f2 ) Pr[V(f1) = V(f2)] · s: maximum # of nodes in a FCED t: size of set from which random values are chosen Proof: more involved

Conclusion and Future Work: 

Conclusion and Future Work Randomization can help achieve simplicity and efficiency at the expense of making soundness probabilistic. Integrate randomized techniques with symbolic algorithms Few interesting possible extensions: Combination of uninterpreted functions with arithmetic Partially interpreted functions like commutative and/or associative functions Model memory