Program Analysis By Combining Abstract Interpretation With Satisfiability Modulo Theories

With the increasing demand and complexity of software system,the dependability of software is playing a more and more important role,especially in safety-critical fields,such as aeronautics,astronautics,healthcare,finance,etc.Design and running of the safety-critical software,especially for embedded software,depend on hardware and physical model of the environment,which involve plenty of numerical computations inevitably.Numerical behaviors of the program are bound with the most dependability properties and faults,such as divided-by-zero,arithmetic overflow,array-out-of-bound,etc.Thus it is vital for the dependability of the safety-critical software to analyze numerical properties of the program and extract numerical constraints on variables automatically.interpretation is a widely used and workable framework in program analysis and verification,which provides a general framework to discover automatically numerical properties in the program.Program analysis based on abstract interpretation obtains low cost and good scalability by leveraging lightweight abstract domain representation and operations,which often leads to the precision loss even false alarms.While Satisfiability Modulo Theories(SMT)that profits from expressive connectors(such as disjunctive predicate,existence quantifier)and abundant theories,could express complicated constrains and depict transfer semantics of basic blocks precisely.Unfortunately it costs high to solve an SMT problem sometimes,and it is challenging for techniques based on SMT to cope with loops.Consequently,this thesis aims at a novel program analysis approach by combining abstract interpretation with SMT so as to achieve the tradeoff between precision and efficiency.The major contributions of this thesis are listed as follows.1)We propose a block-wise abstract interpretation(BWAI)framework,aiming at precision limitation of statement-wise analysis,which combines abstract interpretation with SMT.Under this framework,we first partition the program into several blocks,encodes the transfer semantics through SMT inside the block,abstracts the the SMT formula that encodes the postcondition into an abstract element in a chosen abstract domain,and leverages the widening operator of abstract domains to deal with loops.Besides,we design a lifting functor on top of abstract domains to represent and transmit the useful disjunctive information between blocks.Furthermore,we consider block-wise sparsity in framework of BWAI to improve the analysis efficiency.Experimental results on programs in SV-COMP show that block-wise analysis can check about 1x more properties than statement-wise analysis does.2)We propose the backwards policy iteration(BPI)algorithm to solve the least fixpoint of a loop,to remedy the poor efficiency of policy iteration,which is under the“try+test” framework.The BPI algorithm first solves a fixpoint candidate about some template speedy based on SMT-opt,and then checks its feasibility based on SMT solving and linear programming.If the candidate is feasible,the BPI algorithm achieves the least fixpoint about that template.Otherwise,the BPI algorithm solves a new fixpoint candidate iteratively.We also prove the correctness of the BPI algorithm and analyze its complexity.Furthermore,we apply the BPI algorithm to program verification with respect to the specified property,and propose a property guided backwards policy iteration(PGBPI)algorithm,which considers the template and policy more related to the given property.The PGBPI algorithm would terminate earlier if it finds that the property is already checked by the fixpoint candidate,and thus it often reduces the iteration procedure.3)We design and implement a new numerical domain——interval template constraint matrix(itvTCM)domain,aiming at the lack in expressiveness of convex abstract domain,which extends classical template constraint matrix domain based on linear template constraints and could infer interval linear inequality relations among variables in the program.The itvTCM domain takes “weak solution” as the semantics of the solution of interval linear constraints to character domain elements,and implements most domain operations based on interval linear programming.Each itvTCM element could be considered as a disjunction of multiple TCMs but without using any explicit disjunctive operations.From the geometric point of view,each itvTCM element maps each orthant to a convex polyhedron(maybe an empty polyhedron).Also we discuss how to generate templates for itvTCM.Experimental results show that itvTCM is useful to capture disjunctive behaviors of a program.