Research On Symbolic Analysis Based Static Defect Detection Technique

As a result of the scale up on software size, complexity and application field, the software trustworthiness problem has become the common concern of software users, programmers and researchers recently. A common view in software engineering area is that, discovering and removing software defects during the early period of software product line is an efficient approach to produce the trustworthy software. The static analysis technique is becoming a typical method to improve the trustworthiness of software, which could efficiently analyze part of a program for detecting the small probability potential defects, without executing the program. However, static analysis could not be both sound and complete, which might casue precision loss and lead to false positives and false negatives. So the false positive ratio and false negative ratio have become a key factor for measuring the performance of static defect detection tools, and how to improve the static analysis precision in order to lower the false positive ratio and false negative ratio has become the critical factor affecting the capability of static analysis techniques, which is also the hot research topic both in domestic and overseas.Funded by the National High-Tech Research and Development Plan of China under Grant "2009AA012404,2012AA010101", and the National Science Foundation of China under Grant "91018002,2010", aiming at improving the precision and efficiency of static defect detection tools, four aspects of work are included:(1)STVL:Improve the precision of static defect detection with symbolic three-valued logicAmong various abstract domains, the interval domain is simple but also less precise. To improve the precision of static defect detection based on the interval domain, we propose a symbolic three-valued logic (STVL) based dataflow analysis. Our STVL differs from other symbolic techniques in that it is capable of handling the logical relationship between variables, which could help eliminating false positives. In addition, for the pointer related defect detection, we introduce a STVL-based pointer model, which naturally supports the pointer arithmetic operation, alias analysis and point-to memory abstraction. Experimental results indicate that the technique is able to achieve sizable precision improvements at reasonable costs, compared with the none-symbolic method.(2) Context-sensitive interprocedural defect detection based on a unified symbolic procedure summary modelPrecise interprocedural analysis is crucial for defect detection faced with the problem of procedure call. Procedure summary is an effective and classical technique to handle this problem. However, there is no general recipe to construct and instantiate procedure summaries with context-sensitivity. This paper addresses the above challenge by introducing a unified symbolic procedure summary model (SPSM), which consists of three aspects:1) the post-condition briefly records the invocation side effects to calling context,2) the feature means some inner attributes that might cause both the dataflow and control-flow transformation and3) the pre-condition implies some potential dataflow safety properties that should not be violated at the call site, or there would exist defects. We represent each aspect of SPSM in the STVL manner:<Conditional Constraints, Symbolic Expression, Abstract Value>. Moreover, by comparing the concrete call site context (CSC) with the conditional constraints (CC), we achieve context-sensitivity while instantiating the summary. Furthermore, we propose a summary transfer function for capturing the nesting call effect of a procedure, which transfers the procedure summary in a bottom-up manner.(3) Improving the efficiency and accuracy of path-sensitive defect detecting based on program slicing techniqueWhile detecting defects with path-sensitivity, the defect state contains all data flow information of the current control flow vex, which might lower the efficiency by the defect irrespective data flow information. Further, in order to avoid the path explosion problem during full-path-sensitive analysis, the defect states encountering the control flow confluent nodes might be simply merged. The preliminary state-merging strategy might lead to an accuracy loss which could induce false positives. To address the above issues, we propose a path-sensitive defect detection method based on program slicing technique. The slice criteria include defect feature and path condition, and the source program is sliced by the inclusion relation between the dataflow information and the slice criteria. The sliced program not only slices the defect irrespective codes, but also is totally equivalent to the original program, which improves the efficiency. In order to further reduce the false positives of path-sensitive defect detection, we present a refined state-merging strategy to diminish the accuracy loss, which selectively merges the defect states by adding path condition as state attribute. Experimental results suggest that applying our technique to path-sensitive defect detecting analysis improves the efficiency, at the same time reduce potential false positives.(4) False positive elimination in static defect detection by the forward dataflow analysis and backward constraint query combined techniqueThe false positive ratio is a key factor for measuring the performance of static defect detection tools. Based on the analysis of a series of false positive elimination techniques, we put forward a defect detection method which combines the strength of forward dataflow analysis and backward constraint query techniques. The forward dataflow analysis generates a conservative dataflow solution, which could help reporting an initial defect detection result. According to the dataflow feature of the initial defect location, by querying the potential constraints that might cause defects, the satisfiability of the initial defects could be determined by the collection of queried constraints, with the help of a general purpose constraint solver. So the initial "coarse granularity" defect detection result is refined. In addition, by introducing the symbolic analysis technique during dataflow analysis, not only the precision of dataflow analysis is improved, but also facilitates the constraint representation and improves the constraint querying efficiency.