Identifying and triaging software bugs through backward propagation of under-approximated values and empiric techniques

Abstract

A software testing tool may use static verification analysis techniques to locate points (lines/events) in computer code at which an error may be present and points (lines/events) in the computer code that may be the underlying cause of the located error points. In one implementation, a device may perform a static verification analysis of computer code to locate a point in the code that causes an error in the execution of the computer code. The static analysis may be performed by analyzing a first set of possible execution paths of the computer code based on an over-approximation of states. The device may back-propagate, from the located point, through a second set of possible execution paths, where the second set of possible execution paths is obtained based on an under-approximation of the states that were over-approximated. Based on the back-propagation, the device may determine potential causes of the error. Additionally, in some implementations, empiric analysis techniques, based on semantic information for the computer code, may also be performed. The empiric analysis techniques may be used to assist in classifying the potential causes of the error.

1 . A device-implemented method, comprising:
 receiving computer code, at the device;   performing a static verification analysis of the computer code to locate a point in the code that, under at least one set of states of variables in the computer code, causes an error in the execution of the computer code, where the static analysis is performed by analyzing a first plurality of possible execution paths of the computer code based on an over-approximation of states, where the performing is performed by the device;   back-propagating, by the device and from the located point, through a second plurality of possible execution paths, where the second plurality of possible execution paths is obtained based on an under-approximation of the states that were over-approximated, where the back-propagating is performed by the device;   determining, based on the back-propagation, a second point in the computer code as a potential cause of the error, the determining being performed by the device; and   storing output information to describe the second point in the computer code, the storing being performed by the device.   
     
     
         2 . The method of  claim 1 , where the static verification is performed through an abstract interpretation of variable states in the computer code. 
     
     
         3 . The method of  claim 1 , where determining the second point in the computer code further includes:
 determining the second point as a point in the computer code that includes an input, variable assignment, variable declaration, or function return value.   
     
     
         4 . The method of  claim 1 , where the over-approximation of the states includes approximating possible variable states such that at least some of the approximated variable states include states that can not be reached during dynamic execution of the computer code. 
     
     
         5 . The method of  claim 1 , where the under-approximation of the states includes approximating possible variable states, during back-propagation, such that all of the determined second points are co-accessible from the located point. 
     
     
         6 . The method of  claim 1 , where the static verification analysis detects one or more of:
 errors relating to overflows and underflows; division by zero; out-of-bounds array access; illegally dereferenced pointers; read access to non-initialized data; dangerous type conversions; exceptions; dead code; access to null pointers; or impossible entry point synchronization errors.   
     
     
         7 . The method of  claim 1 , where the under-approximated states includes states that are co-accessible from a set of states corresponding to the error. 
     
     
         8 . The method of  claim 1 , where the computer code represents code generated based on a model created in a technical computing environment. 
     
     
         9 . The method of  claim 1 , further comprising:
 determining a category for the potential cause of the error as a category selected from a first category in which the cause of the error is determined to be within the computer code or a second category in which the cause of the error is determined to be due to an input to the computer code.   
     
     
         10 . The method of  claim 9 , where determining the category additionally includes:
 analyzing the computer code using empiric techniques, based on semantic information for the computer code, to determine the category.   
     
     
         11 . The method of  claim 10 , further comprising:
 outputting information describing a likeliness of the located point causing an error based at least on outputs of the back-propagation and the empiric techniques.   
     
     
         12 . Computer-readable media, containing programming instructions, that when executed by one or more devices, causes the devices to:
 receive computer code;   perform a static verification analysis to classify the computer code into classes that include computer code that has a possible error condition;   store possible execution paths of the computer code, corresponding to points in the computer code that were determined to have the possible error conditions, where the execution paths are obtained as execution paths corresponding to an over-approximation of possible states of variables in the computer code;   traverse a subset of the stored execution paths in a backward direction, where the subset is chosen based on an under-approximation of possible states, to obtain points in the computer code that are determined to be a cause of the possible error conditions; and   output an indication of the points that are determined to be a cause of the possible error conditions.   
     
     
         13 . The computer-readable medium of  claim 12 , where the execution paths include a plurality of ordered states, where each state is defined by a particular point in the computer code and representations of variable values corresponding to the particular point in the computer code. 
     
     
         14 . The computer-readable medium of  claim 12 , where the points in the computer code that are determined to be a cause of the possible error conditions include points in the computer code associated with an input, variable assignment, variable declaration, or function return value. 
     
     
         15 . The computer-readable medium of  claim 12 , where the over-approximation of the possible states includes approximating possible variable states such that at least some of the approximated variable states include states that can not be reached during dynamic execution of the computer code. 
     
     
         16 . The computer-readable medium of  claim 12 , where the under-approximation of the possible states includes approximating possible states such that all of the obtained points are co-accessible from the possible error condition. 
     
     
         17 . The computer-readable medium of  claim 12 , where the static verification analysis detects one or more of:
 errors relating to overflows and underflows; division by zero; out-of-bounds array access; illegally dereferenced pointers; read access to non-initialized data; dangerous type conversions; exceptions; dead code; access to null pointers; or impossible entry point synchronization errors.   
     
     
         18 . The computer-readable medium of  claim 12 , where the computer code represents code generated based on a model created in a technical computing environment. 
     
     
         19 . The computer-readable medium of  claim 12 , further comprising instructions to:
 determine categories for the causes of the potential error conditions as categories selected from a first category in which the cause of the potential errors are determined to be within the computer code or a second category in which the causes of the potential errors are determined to be due to an input to the computer code.   
     
     
         20 . The computer-readable medium of  claim 19 , where the instructions to determine the categories additionally includes instructions to:
 analyze the computer code using empiric techniques, based on semantic information for the computer code, to determine the category.   
     
     
         21 - 26 . (canceled)