Context-Sensitive Interprocedural Defect Detection Based on a Unified Symbolic Procedure Summary Model

Precise 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 (PSM), 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 and (3) 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 PSM in a three-valued logic: <;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 proposed a summary transfer function for capturing the nesting call effect of a procedure, which transfers the procedure summary in a bottom-up manner. Algorithms are proposed to construct and instantiate the summary model at concrete call sites with context-sensitivity. Experimental results on 10 open source GCC benchmarks attest to the effectiveness of our technique on detecting null pointer dereference and out of boundary defects.