Revolutionizing Program Analysis Through Constraint Solving

Program Analysis as Constraint Solving Sumit Gulwani (MSR Redmond) Ramarathnam Venkatesan (MSR Redmond) Saurabh Srivastava (Univ. of Maryland)

Introduction Last decade has witnessed an engineering revolution in constraint solving. We have developed techniques to reduce classic program analysis problems to constraint solving (in the context of linear arithmetic properties). Program Verification Inter-procedural Program Analysis Weakest Precondition Generation Strongest Postcondition Generation We show applications of these techniques to Proving termination/Bounds Analysis Finding preconditions for non-termination Most-general counterexamples 1

Introduction Last decade has witnessed an engineering revolution in constraint solving. We have developed techniques to reduce classic program analysis problems to constraint solving (in the context of linear arithmetic properties). Program Verification Inter-procedural Program Analysis Weakest Precondition Generation Strongest Postcondition Generation We show applications of these techniques to Proving termination/Bounds Analysis Finding preconditions for non-termination Most-general counterexamples 2

Program Verification Verify a Hoare triple (Pre, Program, Post) Pre while (c) S Post Pre ) I I :c ) Post (I c)[S] ) I I 8X 9 I Second-order satisfiability constraint 3

Solving second-order satisfiability constraints 9I 8X 1(I,X) Second-order to First-order Assume I has some form, e.g., j ajxj 0 9I 8X 1(I,X) translates to 9aj8X 2(aj,X) First-order to only existentially quantified Farkas Lemma helps translate 8 to 9 8X ( k(ek 0) ) e 0) iff 9 k 0 8X (e + k kek) Eliminate X from polynomial equality by equating coefficients. 9aj8X 2(aj,X) translates to 9aj9 k 3(aj, k) only existentially quantified to SAT Bit-vector modeling for integer variables 4

Program Verification: Example [n=1 m=1] x := 0; y := 0; while (x < 100) x := x+n; y := y+m; [y 100] Invariant Template Satisfying Solution Loop Invariant a0 + a1x + a2y + a3n + a4m 0 b0 + b1x + b2y + b3n + b4m 0 c0 + c1x + c2y + c3n + c4m 0 y x m 1 n 1 a2=b0=c4=1, a1=b3=c0=-1 a2=b2=1, a1=b1=-1 y x m n a0 + a1x + a2y + a3n + a4m 0 b0 + b1x + b2y + b3n + b4m 0 UNSAT Invalid triple or Imprecise Template a0 + a1x + a2y + a3n + a4m 0 5

Outline Program Verification Weakest Precondition Generation Termination/Bounds Analysis Most-general Counterexamples 6

Weakest Precondition Find weakest Pre such that the Hoare triple (Pre, Program, Post) is valid. [m n] x := 0; y := 0; while (x < 100) x := x+n; y := y+m; [y 100] 7

Weakest Precondition: Attempt 1 Find weakest Pre such that the Hoare triple (Pre, Program, Post) is valid. VC(Pre) Precondition Encoding Pre while (c) S Post Pre ) I I :c ) Post (I c)[S] ) I I 9 Pre, I 8X Weakest Precondition Encoding VC(Pre) 8R: If R is weaker than Pre, then :VC(R) 9 Pre, I Unfortunately, Farkas lemma is no longer applicable since the formula is non-linear in universally quantified variables. 8

Weakest Precondition: Attempt 2 Find weakest Pre such that the Hoare triple (Pre, Program, Post) is valid. VC(Pre) Precondition Encoding Pre while (c) S Post Pre ) I I :c ) Post (I c)[S] ) I I 9 Pre, I 8X Non-false Precondition Encoding Pre x := 0; y := 0; while (x < 100) x := x+n; y := y+m; [y 100] VC(Pre) Pre is weaker than false 9 Pre, I m n+127 is a satisfying assignment for Pre. However, this is still not Weakest Pre. 9

Weakest Precondition: Attempt 3 Find weakest Pre such that the Hoare triple (Pre, Program, Post) is valid. VC(Pre) Precondition Encoding Pre while (c) S Post Pre ) I I :c ) Post (I c)[S] ) I I 9 Pre, I 8X Weaker then Previous Precondition Encoding Pre x := 0; y := 0; while (x < 100) x := x+n; y := y+m; [y 100] VC(Pre) Pre is weaker than Previous Pre 9 Pre, I Seq. m n+127, m n+126, , m n is admissible. This iterative refinement is too slow. 10

Weakest Precondition: Solution 1 Find weakest Pre such that the Hoare triple (Pre, Program, Post) is valid. VC(Pre) Precondition Encoding Pre while (c) S Post Pre ) I I :c ) Post (I c)[S] ) I I 9 Pre, I 8X Locally-weakest Precondition Encoding Pre x := 0; y := 0; while (x < 100) x := x+n; y := y+m; [y 100] VC(Pre) Pre is weaker then Previous Pre :VC(R1) :VC(R2) where R1, R2, are weaker neighbors of Pre. 9 Pre, I 11

Weaker Neighborhood Structure Weaker neighbors of e1 0 e2 0 are: Geometric Interpretation e1+1 0 e2 0 Shift plane ei parallel to itself. e1 0 e2+1 0 e1+e2 0 e2 0 Rotate plane ei along its intersection with another plane. e1 0 e2+e1 0 12

Weakest Precondition: Solution 1 Find weakest Pre such that the Hoare triple (Pre, Program, Post) is valid. VC(Pre) Precondition Encoding Pre while (c) S Post Pre ) I I :c ) Post (I c)[S] ) I I 9 Pre, I 8X Locally-weakest Precondition Encoding Pre x := 0; y := 0; while (x < 100) x := x+n; y := y+m; [y 100] VC(Pre) :VC(R1) :VC(R2) Pre is weaker than Previous Pre We directly obtain m n. m n+c is no longer locally-weakest for c>0. In fact, we obtain one more solution: n 0. Generally, locally weakest weakest. Iteration may be required. 9 Pre, I

Outline Program Verification Weakest Precondition Generation Termination/Bounds Analysis Most-general Counterexample 14

Termination/Bounds Analysis i := 0; while (c) i := i+1; Assert(i F(inputs)); S while (c) S Transformation introduces a counter to track loop iterations. Then we run Program Verification Algorithm. Besides loop invariant, part F of assertion is also unknown. Existence of a solution yields a termination proof. Solution for F gives upper bound on # of loop iterations. 15

Outline Program Verification Weakest Precondition Generation Termination/Bounds Analysis Most-general Counterexample 16

Most-general Counterexample Pre x := 0; err := 0; i := 0; while (x < n) i := i+1; Assert(i F(n,y)); if (x 200) err := 1; x := x+y; Assert (err=1) x := 0; while (x < n) Assert(x<200); x := x+y; n=356 and y=12 leads to a bug. However, it is more useful to say y>0 n 200+y leads to a bug. We generate this by: 2-step Transformation Introduce error variable err to track assertion violation. Introduce counter i to track loop iterations/termination. Then, we run weakest Precondition algorithm. 17

Experiments: Methodology We ran our tool against academic/small benchmarks used by 10 earlier pieces of work that address a wide variety of program analyses related to linear arithmetic properties. Inter-procedural analysis, Disjunctive invariant inference, termination/bounds analysis, non-termination, strongest Postcondition generation. Parameters: Templates: 2 conjuncts/1 disjunct Bit-vector modeling: 3 bits for unknown coefficients, 6 bits for unknown constants, 1 bit for multipliers in Farkas lemma Iteratively increased these quantities. 18

Experiments: Results Clauses generated: 5K to 560K (Most examples < 200K) Time taken: 0.1 sec to 80 sec (Most examples < 5 sec) comparable; however, demonstrates versatility 80 70 60 50 Time (s) 40 30 20 10 0 0 100 200 300 400 500 600 Clauses (K) 19

Related Work: Constraint based techniques Invariant discovery Linear [Colon, Sankaranarayanan, Sipma, CAV 03] Non-linear [Sankaranarayanan et al, POPL 04]; [Kapur, 05] Linear arithmetic + uninterpreted fns [Beyer et.al., VMCAI 07] This work only addresses linear invariants, but With arbitrary (pre-specified) boolean structure. In an inter-procedural setting. In a weakest precondition generation mode too. Bug Finding SATURN [Xie, Aiken, CAV 05]: works with loop-free programs This work only addresses programs with linear assignments, but Finds most-general bugs in programs with loops 20

Conclusion Constraint-based techniques offer 2 advantages over fixed-point computation based techniques: Goal-directed (may buy efficiency) Do not require widening (may buy precision) This work showed how to reduce a wide variety of program analysis problems to constraint solving over the domain of linear arithmetic. Future work includes extending these ideas to other domains such as pointers, quantifiers. 21