Alexandre D. Salcianu and Martin C. Rinard
PURITY ANS SIDE EFFECT ANALYSIS
FOR JAVA PROGRAMS
Definiciones
 Un método es puro si no “muta” ninguna
locación existente en el estado correcto
anterior a la invocación del método.
Para qué?
 Cómo input para algunos análisis de
programas
 Para entender y documentar el programa
 Para reducir el trabajo de los model checkers
Idea
 Método para analizar la pureza de programas
Java (no anotados).
 Construido sobre una mejora de “combined
pointer and escape analysis method” (RinardWhaley)
 Chequea si un método es puro, en el sentido
de que no cambia ningún objeto existente en
el pre-estado.
Mejoras
 Se distingue entre objetos existentes en el
pre-estado y objetos nuevos (creado por el
método)
 La información adicional generada por el
método sirve para identificar información útil
sobre efectos colaterales.
 El método fue probado (correctitud),
implementado y utilizado en variedad de
tareas.
Generalizaciones de Pureza
 Parámetros Read-Only : el método no cambia
ningún objeto alcanzable desde el parámetro.
 Parámetros Seguros (safe):
 parámetros read-only
 el método no crea ningún camino externo visible
en el heap hacia objetos alcanzables desde el
parámetro.
Resumen hasta acá
 Análisis para detectar métodos puros en
programas Java no anotados
 Presenta mejoras con respecto a análisis
anteriores
 Permite la alocación de objetos nuevos en el heap
 Detecta parámetros read-only y safe.
Revisión del análisis
 Para cada método m y cada punto del
programa dentro de m el análisis computa un
points-to graph que modela la parte del heap
que el método m accede antes de ese punto.
Revisión del análisis
 Un objeto “escapa” si es alcanzable desde
afuera del método analizable (ej: desde uno
de los parámetros)
 En otro caso, el objeto está “capturado”
 Un eje externo siempre termina en un load
node
Revisión del Análisis
 Para cada método m el análisis computa un
conjunto Wm que contiene los campos
abstractos modificados que son visibles
externamente.
 Un campo abstracto es un campo para un nodo
específico.
Revisión del Análisis
 El análisis examina métodos empezando





desde las hojas.
Se realiza sin conocer el contexto en que se
llamó el método.
Obtiene un único resultado parametrizable
El resultado es luego instanciado en cada
lugar que se invoque el método m.
Normalmente, el análisis procesa cada
método una única vez.
Métodos recursivos requieren varias pasadas
hasta llegar a un punto fijo.
Ejemplo: Cell Constructor
Ejemplo: List.add
Descanso??????
Continuando el Análisis
 Cada points-to graph registra los nodos que
“escapan globalmente” , es decir, aquellos
nodos que son potencialmente accesibles por
código que desconocemos.
 Cualquier nodo alcanzable desde estos nodos
también escapa globalmente
 El análisis debe ser muy conservativo con
respecto a estos nodos, en particular, porque
pueden ser mutados por código no conocido.
 Se utiliza un nodo especial para otros nodos
desconocidos que escapan globalmente
Análisis Intraprocedural
Análisis Interprocedural
 Por cada llamada (call) del tipo
vR = v0.s(v1, … , vj)
el análisis usa el points-to graph G anterior a
la llamada y el points-to graph Gcalle (gráfico
final del método invocado) para computar un
points-to graph posterior a la invocación del
método.
 Si hay múltiples posibles invocaciones, el
análisis las considera a todas y mergea el
conjunto de resultados de los points to graph
Paso 1
 El análisis computa un mapeo, que relaciona
los parámetros y los nodos cargados del
método invocado, con los nodos que
representan
Incluir gráfico
Paso 2
Análisis de Efectos
 Este análisis se realiza sobre el análisis
descripto anteriormente.
 El análisis propaga efectos interprocedurales
de las siguiente forma: cuando el análisis del
método m encuentra una invocación, se
utiliza el mapeo de nodos intraprocedural
para proyectar los efectos del método
invocado e incluir esos efectos en el conjunto
Wm.
Diego Garbervetsky, Mike Barnett, Manuel Fähndrich, Francesco
Logozzo
ANNOTATIONS FOR (MORE)
PRECISE POINTS-TO ANALYSIS
Objetivos
 Extender el análisis de grafos Points-to para
.NET (parámetros por referencia y
estructuras).
 Incrementar la precisión en el análisis de
efectos de métodos no analizables.
Definiciones
 Un método es no analizable si su código no
está disponible.
 Un método es débilmente puro si no “muta”
ninguna locación existente en el estado
correcto anterior a la invocación del método.
El problema
List<int> Copy(IEnumerable<int> src)
{
List<int> l = new List<int>();
IEnumerator<int> iter =
src.GetEnumerator();
while (iter.MoveNext()){
int x = iter.get_Current();
l.Add(x);
}
return l;
}
Salcianu
 No puede analizar llamadas a métodos de
interfaces:
 src podría escapar a cualquier posición en
memoria
 El método tiene una (potencial) escritura a
cualquier posición accesible, como las variables
estáticas.
Extensiones para .NET
 Address nodes: representan objetos y
estructuras.
 Un address node que representa un objeto
tiene ejes salientes con etiqueta *.
 Un address node para valores de estructuras
tiene un eje saliente por campo (la etiqueta es
el nombre del campo).
Ejemplo: v1 = v2
Ejemplo: v1 = v2
Ejemplo: v1 = v2
Métodos no analizables
 Métodos analizables: se matchea las
escrituras y lecturas en los load nodes con los
nodos del llamador.
 A diferencia de los métodos analizables, los
efectos en estos pueden no mapear
directamente con el grafo del método
llamador.
Extensiones para métodos no
analizables (nodos)
 Omega nodes (ω): modelan el conjunto de
nodos alcanzables desde ese nodo.
 Omega Confined nodes (ωC): subcojunto de
ω. Son nodos ω que representan solo
aquellos alcanzables por los campos propios
del llamador.
 Un campo f es propio de la clase T si el objeto
O de tipo T posee el objeto apuntado por su
campo f.
Extensiones para métodos no
analizables (ejes)
 Ejes “?”: eje desconocido. Representan
cualquier campo.
 Ejes “$”: campos no propios. Permite
distinguir entre referencias a objetos que
pueden ser escritos por el método y los que
únicamente pueden ser leídos.
Matcheo interprocedural
 Matcheo con ω: calculamos el conjunto de
nodos (del llamador) alcanzables desde este,
y finalmente todos los load nodes se
convierten en ω.
 Matcheo con ωC: consideramos solo caminos
que pasan por los ejes “?” y los ejes propios.
Rechazamos los que contienen ejes “$”.
Ejemplo: omega nodes
Ejemplo: omega nodes
Ejemplo: omega nodes
Anotaciones
Descargar

presentacionPapers