Efficient sequential tight field bounds computation, and their impact on the performance of SAT based program analysis

Dada una descripción formal de los estados válidos del heap -por ejemplo, un invariante de una estructuras de datos- las cotas ajustadas para los campos del heap son el conjunto de los valores que pueden tomar los campos en alguna instancia válida. Así, los valores de campos que no pertenecen a las cotas ajustadas pueden ser ignorados por los análisis automáticos (acotados) de código, reduciendo así el espacio de estados a explorar, y mejorando la performance del análisis. Sin embargo, el cómputo de cotas ajustadas es costoso. El único enfoque conocido que computa estas cotas en un tiempo aceptable, TACO+, es intrínsecamente paralelo, y requiere de un cluster con varias computadoras para su ejecución eficiente. En este trabajo se aborda el problema de computar eficientemente cotas ajustadas en entornos de ejecución secuenciales. Así, se presentan dos nuevos enfoques para resolver este problema. El primero, denominado bottom-up, utiliza un procedimiento de decisión basado en SAT para visitar instancias válidas del heap, y computa cotas ajustadas usando los valores de los campos de estas instancias. bottom-up, al igual que TACO+, requiere de una especificación en algún lenguaje declarativo de alto nivel -como JML para JAVA- de los estados válidos del heap. De esta manera, bottom-up y TACO+ generan cotas ajustadas equivalentes. El segundo, SLBD, se basa en una especificación del heap en términos de un predicado inductivo de la lógica de separación. Este enfoque computa cotas ajustadas mientras realiza (un número finito de) desplegados del predicado inductivo de entrada. En algunos casos SLBD puede producir cotas ajustadas diferentes a las de TACO+ (y bottom-up). Se evaluaron experimentalmente los enfoques bottom-up, SLBD y la técnica relacionada TACO+, en la generación de cotas ajustadas para varias clases contenedoras JAVA. Los resultados muestran que, en un ambiente de ejecución secuencial, bottom-up es un orden de magnitud más rápido que TACO+ (secuencializado), y que SLBD es dos órdenes de magnitud más rápido que bottom-up. Además, se evaluó el impacto de las cotas ajustadas generadas por nuestros enfoques en la veri ficación de código y en la generación exhaustiva de estructuras (que satisfacen un predicado) basados en SAT. Los resultados indican que los enfoques que computan cotas ajustadas secuencialmente (vía bottom-up o SLBD), y luego las aprovechan durante el análisis, son significativamente más eficientes que los análisis convencionales, que no explotan la idea de cotas ajustadas. Además, para los análisis basados en SAT mencionados, los resultados muestran que las cotas ajustadas computadas por SLBD tienen un impacto similar a las computadas por TACO+ y bottom-up.Given a formal description of the feasible heap states -for example, an invariant for a data structure-, tight field bounds for heap fields are the set of values that the fields can take in any valid instance. Thus, field values that do not belong to the tight field bounds can be safely ignored by automated (bounded) program analyses, reducing the state space to be explored, and improving the performance of the analysis. However, computing tight field bounds is an expensive process. The only known approach to compute these bounds that performs reasonably, TACO+, is intrinsically parallel, and it requires a cluster of several computers to run efficiently. In this work we address the problem of computing tight field bounds efficiently under a secuential execution environment. Thus, we introduce two novel approaches to solve this problem. The first, called bottom-up, uses a SAT based decision procedure to traverse valid heap instances, and computes tight field bounds using the field values of the visited instances. bottom-up, like TACO+, requires a description of the feasible heap states in a high level declarative language -like JML for JAVA-. In this way, bottom-up and TACO+ yield equivalent tight field bounds. The second, SLBD, is based on a specification of the valid heap states in terms of a separation logic's inductive predicate. This approach computes tight field bounds during the process of unfolding its input's inductive predicate (a finite number of times). In some cases, the tight field bounds computed by SLBD and TACO+ (and bottom-up) might differ. We assessed bottom-up, SLBD and the related technique TACO+ experimentally, in generating tight field bounds for several JAVA container classes. The results show that, under a secuential execution environment, bottom-up is an order of magnitude faster than TACO+ (secuentialized), and that SLBD is two orders of magnitude faster than bottom-up. Moreover, we assesed the impact of the tight field bounds produced by our approaches in SAT based code analysis and in exhaustive bounded generation of structures (satisfying a predicate). The results show that the approaches that compute tight field bounds secuentially (via bottom-up or SLBD), and subsecuently exploit them during analysis, are significatively faster than the more conventional analyses that do not take advantage of tight field bounds. Furthermore, for the aformentioned SAT based analyses, the experiments show that the tight field bounds computed by SLBD have a similar impact to those computed by TACO+ and bottom-up.Fil:Ponzio, Pablo Daniel. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina