Tesis digital

En mi sitio personal pueden encontrar mi tesis, ¡con esto doy por finalizado este blog!

¡Me recibí!

Me recibí y por ende este blog cumplió ya su cometido. Todo salió muy lindo y no hay mucho más para decir salvo agradecer a Diego y a Dani por toda su paciencia y dedicación. El laburo que resultó me gusta mucho. Quizás más tarde ponga aquí un link cuando el mismo esté subido en algún sitio.

Defensa de tesis de licenciatura de Guido de Caso

Qué: Defensa de tesis de licenciatura
Quién: Guido de Caso
Cuándo: Martes 4 de diciembre a las 19hs.
Dónde: Aula a confirmar.

Título: "Construcciones de alto nivel como anotaciones para la verificación automática de software"

Directores: Diego Garbervetsky, Daniel Gorín
Jurado: Eduardo Bonelli, Juan Pablo Galeotti

Breve resumen:
"La verificación automática de software es una disciplina que ha crecido mucho en los últimos años, aportando herramientas que con bajo costo permiten aumentar la confianza que se tiene sobre un sistema. En particular la verificación automática de código ha comenzado a ser una alternativa viable, pero gran parte de las herramientas actuales se han montado sobre lenguajes preexistentes. Este enfoque ha brindado soluciones que pueden lidiar sólo con una parte del poder expresivo de los mismos y suelen ser introducidas mediante modificaciones ad-hoc a la sintaxis. Esta metodología no integral desfavorece la adopción de estas técnicas a gran escala.

Se presenta en este trabajo un lenguaje imperativo multiprocedural muy básico cuyo diseño está orientado a la verificabilidad. Se dota a este lenguaje de mecanismos de inferencia de precondiciones y postcondiciones que permiten asistir la tarea de anotar ciertos fragmentos del código. Haciendo uso de estas técnicas se extiende el lenguaje con construcciones de iteración de alto nivel para las cuales no es necesario proveer ningún tipo de anotación para su verificación. Se espera que estas característiscas alivien la carga de trabajo que requiere especificar un programa, logrando de esta forma una adopción mayor de las técnicas de verificación automática. Se presenta un prototipo de herramienta que pone a prueba esta hipótesis, trabajando con un conjunto diverso de demostradores de teoremas en paralelo de forma tal de maximizar la cantidad de programas que pueden ser verificados sin intervención del programador."

Como parte de la defensa se hará una breve demostración del prototipo de herramienta implementado.

¡Quedan todos cordialmente invitados!

¡Diego es doctor!

¡Hoy (o mejor dicho ayer) diego se doctoró! Ahora tiene mucho tiempo libre para ayudarme a terminar de revisar mi tesis ;).

Hablando de lo cual, en estos días estuve terminando de escribir los capítulos 5 y 6. Si todo marcha bien se los mandamos al jurado la semana que viene.

Estuvimos hablando con Diego sobre fechas para presentar la tesis. Una posibilidad sería martes 11 de diciembre... veremos si el jurado llega a revisar toda la tesis para ese entonces. ¡Ojalá así sea!

Jurado con capítulos

El jurado, compuesto por Juan Pablo Galeotti y Eduardo Bonelli, recibió el viernes una copia de los primeros cuatro capítulos de mi tesis.

Mientras ellos avanzan en su lectura, yo continúo escribiendo lo que falta.

Cuatro adentro

Hace instantes les mandé a Diego y a Dani los primeros 4 capítulos de la tesis. En teoría ya tienen todos los cambios que ellos me sugirieron. De esta forma, si todos los planetas se alinean, le estaría mandando mañana (viernes) al jurado estos primeros 4 capítulos.

Faltan todavía terminar algunas partecitas del capítulo 5 y escribir las conclusiones y el future work para el capítulo 6. No falta tanto...

Un informe de nunca acabar

Sigo escribiendo el informe de la tesis. Se podría decir que los capítulos 1, 2 y 3 están bastante bien. El capítulo 4 está terminado pero tiene que atravezar varios procesos de revisión. El capítulo 5 está a medio escribir y el capítulo 6 (las conclusiones) todavía no lo empecé.

No falta tanto, pero no veo la hora de terminar, siempre aparece alguna cosa para corregir... ¡¡ánimo!!

Elecciones, Bariloche, introducción

La semana del 24/9 al 29/9 fue caótica. Elecciones, o sea pasarse las 25 horas del día en la facu, comiendo mal, durmiendo peor y mordiéndose las uñas...

Para descansar y aprovechando la oportunidad me escapé un par de días a Bariloche, lo cual me sirvió mucho para descansar.

Hoy, recién vuelto y con pilas renovadas, escribí el capítulo de introducción. También charle con Dani, que dentro de poco se va para Francia por unos meses.

Un paso atras, ¿dos adelante?

Dicen que a veces para dar avanzar hay que retroceder un poco. Puede que haya sido el caso esta semana.

El miércoles casi desespero cuando encontré un error que hizo tambalear varias partes relativamente importantes del formalismo que estamos usando.

Me pasé el jueves y el viernes sufriendo para ver como se emparchaba. Charlando con Diego y Dani para solucionarlo.

Finalmente la solución que encontramos no es la que más nos satisface, pero es la más cercana a lo que hay hecho. Cualquier otra versión que se nos ocurrió tenía problemas iguales o peores y nada parecía indicar que valía la pena el esfuerzo y el riesgo.

Así que casi como al comienzo, pero con muchas más justificaciones de por qué hicimos lo que hicimos cómo lo hicimos.

Avanzo un poco más

Creo que es normal que ya no escriba tanto acá. Estoy escribiendo mucho en la tesis y creo que antes cuando programaba extrañaba el castellano y usaba este medio para reencontrarme un poquito. Ahora no lo necesito tanto...

Bueno, avancé un poco más, tengo la formalización para la parte básica del lenguaje terminada y algunas demostraciones. Esta semana se viene complicada, pero si tengo tiempo voy a ver de empezar a formalizar las construcciones de alto nivel.

Avanzo con la formalización

Entregué una primera versión a Diego y Dani, me hicieron algunas correcciones y volví a entregarles otra versión.

Ya tengo la sintáxis y la semántica operacional que me convencen bastante. Avancé un poco con la semántica abstracta, que sería lo que permite "tipar" programas con sus pre y post condiciones.

Definiciones básicas

Estuve escribiendo definiciones básicas a partir de las cuales formalizar algunas de las cosas que estuvimos haciendo.

Por ahora tengo:

• Sintaxis básica del lenguaje Pest:
• Expresiones.
• Términos.
• Predicados.
• Parámetros.
• Sentencias (sin incluir map, find, for).
  
• Procedimientos.
• Programas.
  

• Concepto de expresión válida, término válido, ..., programa válido.

• Semántica operacional para un programa. Esto requiere definir semántica para los predicados, los términos, las expresiones.

Con todo ya suman más o menos 11 páginas de definiciones.

Faltan explicaciones que complementen las definiciones formales. Pero hasta que no esté seguro de qué cosas quedan y qué cosas cambian no tiene sentido invertir tiempo en eso.

Escribiendo

Después de varios meses programando estuve por fin escribiendo un poco el documento final. Formalizando, decidiendo algunas cosas de formato, etc.

Además estuve muy colgado porque el jueves amanecí con fiebre. Por suerte ahora ya estoy mejor y con pilas.

Con respecto a la imple simplemente corregí algún que otro bug.

Buenas y malas

(Copiado de un mail a mis directores)

Las buenas:
- Ahora PEST tiene "For" (for var from low to high do {...}) que no necesitan de proveer invariante y tampoco variante.

- Me maté programando y cambie casi toda la estructura que usaba para almacenar las VC's. ahora se hace en dos pasadas:

1) se recorre el programa PEST de arriba hacia abajo haciendo dynamic single assignment. Se obtiene algo que llamo "lenguaje intermedio" que sería similar a boogie: tiene assume, assert, if, lemma (para simular el assume false de boogie).

El lenguaje intermedio también tiene una construccion especial llamada "For" que, como su nombre lo indica, representa de forma temporaria los For's no resueltos del lenguaje Pest. o sea, durante la primera pasada no se generan VC's para la correctitud del For, solamente se generan para la correctitud de su cuerpo (recursivamente).

2) Se recorre el lenguaje intermedio de ABAJO hacia arriba para remover los For's no resueltos. Esto permite que en cada paso ya tener la cola resuelta, es decir con todos sus For's reemplazados por lemmas que deberían probar que son correctos.

En cada paso que se encuentra un For se calcula la wp de la cola (que como no tiene for's, se puede obtener tranquilamente). Se la debilita y se usa eso como invariante. Es decir: se pregunta si vale antes de entrar, si se preserva y se asume al final, una vez terminado el for.

Una vez eliminado el For, se reemplaza por un lema muy similar a lo que hubiera quedado si en vez de un For era un While común (con invariante, etc.). La diferencia es que no es necesario ver la terminación, está garantizada por la estructura misma.

- Esto lo probé únicamente en el caso para calcular el máximo de un arreglo y parece funcionar. Pero quiero probarlo en casos donde haya código entre el fin del for y el fin del procedimiento, de manera tal de tener que calcular una wp más compleja que simplemente la postcondicion del procedimiento.

- Otros cambios pequeños: ahora PEST tiene como nativos comandos assume y assert. yo no los dejaría en el lenguaje final, pero para testear cosas son útiles. esta caracteristica, junto con los procedimientos hizo que los bloques con pre y post sean obsoletos, así que los saqué.

Las malas:

Al cambiar la estructura necesité retocar bastante fuertemente la forma en la que trabajo con predicados internamente. Para calcular wp's necesito a veces cuantificar arreglos y ahora los arreglos son ciudadanos de primer nivel en los predicados. Es decir un store sobre un arreglo es un término. Y todo eso los provers de primer orden no lo soportan así que temporariamente los desconecté.

Se me ocurre que con algún tipo de preproceso a los predicados se pueden eliminar las cuantificaciones de arreglos (esto no se puede hacer en el caso general, pero la pinta de las cuantificaciones que aparecen parecería ser simple). Y cambiar los update terms por renombres y axiomas que digan como se relacionan.

Pero considerando que los provers de primer orden no habían aportado nada (o sea, no encontré ningún caso donde puedan probar algo que los SMT solvers no pudieran, sino más bien todo lo contrario) por ahora no quiero invertir tiempo en hacer toda esta traducción que parece ser nada trivial.

Pero por ahora me parece más interesante ver qué potencia y limitaciones tiene nuestro brand-new For y el cálculo de wp's.

Varias cosas nuevas

Entre ayer y hoy implementé varias cosas interesantes:

• Los dos patrones de iteración que tengo por ahora son map y find. Ambos ahora aceptan cotas opciones sobre el ranto de operación. Por ejemplo:
• map e in a[..k..10] { ... }
  
• find first x in a[j..k..i+1] { ... }

• Ahora find también soporta búsqueda desde atrás.
  
• find first ...
  
• find last ...
  

• Se pueden crear arreglos en cualquier punto, así como antes se podían crear variables.
• local b[|a| - 10] <- .. a[0] ..
  
• inicializa un arreglo de tamaño |a|-10 con todos elementos iguales a a[0]

• Diseñé una clase genérica ProverOrchestrator que permite implementar distintas estrategias para combinar provers. Por ahora hay dos estrategias:
  
• Simple: usar un prover en particular, si anda anda, si no no.
• Lista: usar una serie de provers en un orden prefijado. Mientras la respuesta sea unknown se va pasando al siguiente.
  

Con esta segunda estrategia pude demostrar que bubbleSort es correcto y preserva los elementos en el caso de arreglos sin repetidos.

Map y Find

Hice algunos cambios:

• Ahora multiassign se llama map, es un poco más marketinero.
• Modularice un poquito la semántica de (ahora llamado) map.
• No se generan nombres nuevos para las variables al entrar a un if. En cambio se espera a que sean modificadas por primera vez para hacerlo.
  
• Rompí un poco la estructura lineal de los Proofplans, de esta manera se pueden ir olvidando las cosas que se probaron dentro de un lema, dejando sólamente la conclusión de ese lema, para evitar enviarle al prover axiomas que no usará.
• Ahora los procedimientos deben indicar explícitamente que parámetros tocan. Esto genera chequeos sintácticos que prohiben la asignación sobre los mismos. Esto permite usar procedimientos dentro de los bloques que de map (y otras construcciones de alto nivel) que restringen qué cosas se pueden tocar.

También implementé una nueva construcción, llamada find first. Más tarde los detalles.

Procedimientos

Hoy implementé los detalles que faltaban para el soporte de procedimientos. Ahora se puede utilizar la sentencia:

nombre(p1,...,pn)

La semántica de pasaje de parámetros es la siguiente:

• Si un parámetro es de tipo arreglo, entonces se espera un arreglo, denotado nombre_arreglo[]

• Si un parámetro es de tipo entero, se espera una variable entera.

• Adicionalmente, cuando un parámetro es de tipo entero, se puede esperar una expresión como por ejemplo un número entero. La misma es evaluada y pasada como parámetro. La salida de ese parámetro no es observable.

Dado que todos los parámetros se manejan como inout, o referencias, y no queremos generar aliasing, se espera que todos los parámetros sean distintos entre si.

Un día de estos tengo que implementar un chequeo que restrinja todo tipo de recursividad. Para eso hay que construir un grafo de llamados y ver que no tenga ciclos.

Multiassign, (casi) procedimientos

Entre ayer y hoy implementé la primer estructura de iteración de alto nivel. Es algo así:

for e in a[..k..] {
e <- e + k - |a|
}

La semántica es ejecutar el bloque de código reemplazando a "e" por cada uno de los elementos en el arreglo "a". Este bloque no puede leer directamente elementos de "a" (sólo puede hacerlo mediante la variable "e"). Tampoco puede modificar variables (a excepción de "e" y cualquier otra variable local que se cree dentro del mismo bloque).

Esta estructura permite simplificar muchísimo la escritura y verificación de programas como: resetear un arreglo a 0, poner números de 1...N en un arreglo, poner números de N...1 en un arreglo, etc.

Por otra parte estuve empezando a implementar procedimientos. Esto está incompleto, cuando lo tenga andando comento los detalles.

Inferencia de postcondiciones

Hoy implementé una versión básica de inferencia de postcondiciones. Esto es necesario para poder contar con estructuras de iteración relativamente piolas como por ejemplo la asignación simultánea. Todavía hay varias cosas que pulir.

También estoy cada vez más seguro de que necesito una capa extra de abstracción entre los predicados que utilizo y los provers. Esto puede ser un poco denso de implementar pero hay varios indicios que marcan que sería el camino correcto a seguir, aunque por ahora (mientras no me trabe) es algo que voy a patear...

Plan

Nos juntamos con Diego y Dani. Charlamos de que venimos avanzando bastante bien y que podemos llegar a que me reciba en noviembre. Por supuesto que para eso hay que meterle porque faltan cerrar algunas cosas y además escribir todo.

De lo que falta hacer (en orden de prioridad) están las siguientes cosas:

• Implementar la idea de patrones de iteración que tienen un invariante conocido. De la mano de esto hay que buscar ejemplos donde estos patrones tienen sentido y evitan la escritura de un invariante potencialmente engorroso.

• Estrategias para elegir qué prover usar. Esto involucra probar varios demostradores distintos sobre cada fórmula, hasta que alguno pueda verificar la propiedad.

• Procedimientos.

• Syntax sugar para cuatificación más cómoda sobre elementos de arreglos, etc.

Además está la idea de escribir la tesis en inglés así ya se puede reutilizar una parte para armar algún artículo y presentarlo.

Esto hace que la idea de armar un plugin de eclipse quede postergada para después de que me reciba.

Avanzo en mi TODO list

De mi lista del post anterior pude implementar hablar con provers de primer orden y verificar accesos a arreglos son en rango.

Mañana tenemos con Diego y Dani una reunión donde definir un poco mejor cómo seguimos, de todas formas algunas cosas que quiero hacer en estos días son:

• cambiar la estructura de iteración
  
• inferir postcondiciones
• procedimientos
• plugin de eclipse, basado en el código fuente del plugin de javaCC

Una buena nueva es que pude demostrar la corrección de bubblesort, antes no podía porque un invariante tenía un error. Y ahora estoy tratando de demostrar el hecho de que el arreglo es permutación del original (asumiendo que no hay repetidos).

BubbleSort, TODO

Hoy programé un BubbleSort y casi casi lo verifico completo. De 38 VC's pude verificar 37.

Tengo que revisar, quizás algún invariante está un poco débil.

También tengo una pequeña lista de cosas interesantes para hacer con respecto a la implementación:

• hablar con first-order provers
  
• verificar que los accesos a arreglos siempre son correctos
• inferir postcondiciones
• inferir precondiciones (wp)
• más benchmarks
• procedimientos
• construcciones de alto nivel (foreach, acum, select, etc.)
• ¿plugin de eclipse?

Arrays

Estuve aumentando el lenguaje PEST para que pueda hablar de arreglos. Además, ya que estaba tocando el parser, mejoré la sintaxis de expresiones para que se puedan escribir cosas complejas en una misma sentencia como:

x <- a[i] + 3*i


Por otra parte reimplementé el output a SMT-lib porque la traducción que ofrecía CVC era muy mala para lidiar con operadores aritméticos no lineales.

Para poder soportar aritmética no lineal en Z3 y Yices lo que hice fue crear operadores no interpretados para la suma y la división. La idea es axiomatizarlos lo más posible (sin que pinche) y demostrar algunas cosas... que siempre es mejor que nada.

Con todo esto pude demostrar la corrección de programas como el máximo de un arreglo, el arreglo 1...N, incrementar en 1 cada posición de un arreglo, ver si un arreglo está ordenado, etc.

SMT-lib

Descubrí que el demostrador CVC viene con una característica que permite traducir a formato SMT-lib. Este es un formato que usan todos los demostradores SMT en una competencia que se hace una vez por año.

O sea, que ahora puedo escribir en SMT-lib gratis, sin esfuerzo porque el output a CVC ya lo tenía hecho.

Un tema es que varios demostradores, al leer archivos en este formato SMT-lib, sólo le dan bola a la primer propiedad que aparece ahí. Por eso ahora lo que hago es:

1. Ir acumulando las cosas que sé que son verdad (precondición y los asserts que surgen del flujo del programa).
2. Cuando encuentro un query lo parto en tantos átomos como elementos de la conjunción que denota.
3. Para cada átomo genero un archivo con todos los asserts acumulados como axiomas y pregunto si es teorema.
   
4. Si es teorema lo agrego al conjunto de axiomas. Sino, no.
5. Sigo hasta agotar todos los átomos de cada uno de los queries.

Al finalizar eventualmente hay algunas subfórmulas que no pudieron ser probadas.

Varios días pasaron

El jueves pasado di la charla sobre lo que estuve haciendo y en términos generales gustó. Hubo muchas preguntas (tal como esperábamos) sobre para qué sirve lo que estamos haciendo y cuál es la innovación, cuestiones que ni nosotros (Dani, Diego y yo) sabemos por ahora.

Estos días estuve yendo y viniendo con refactors al código hasta que me cansé y decidí que así como está es un código suficientemente malo y suficientemente bueno.

También estuve cursando una ECI con Shaz Qadeer, la verdad me está sirviendo muchísimo para aprender cosas nuevas y profundizar y entender otras que más o menos había visto en papers.

Le mostramos a Shaz lo que tenemos hecho y le pareció bien. Le pareció que la idea de Dani de hablar con demostradores de FOL es interesante, y vale la pena probar. Por eso estos días quiero ver de hacer algunos ejemplos, aunque sea a mano.

Para piter que lo mira por tevé

Se que piter cada tanto lee este blog. Piter, comprá la licuadora que debés.

Sin 'at'

A partir de lo que ví del artículo que mencionaba ayer, surgió un detalle que es no tratar más las variables dentro de estados tipo:

at(x,S0) ó at(y,S1)

Sino tratarlas con sufijos por ejemplo

x_S0 ó y_S1

De esta manera el demostrador se ahorra tener que trabajar con la función no interpreteada 'at' y posiblemente eso sea más rápido.

La contra: las aserciones descargadas al verificador son un poquito menos legibles.

Slides listas, PPL promete, un artículo

Por partes:

• Las slides para la charla de este jueves ya están cocinadas. Puede faltar pulir un poco, pero la base está.

• Estuve jugando con la interfaz para Java de la PPL. Probé BDDs y Poliedros (el otro día me di cuenta que en castellano van sin 'h'). Aparentemente la interfaz Java no tiene bindings para trabajar con Octágonos, incluso cuando éstos están implementados en la versión 0.10pre7 (que es la que obtuve del CVS). En estos días voy a ver si hago una interfaz propia para manejar de forma más o menos cómoda la interfaz de Java de la PPL. (Y también ver de que cuando le agreguen el soporte para Octágonos a la API de Java, poder incluirlo rápidamente en mi wrapper.)

• Estuve leyendo un artículo que promete ser interesante. Menciona una combinación entre SMT solvers e interpretación abstracta. La idea es discutir este artículo con Dani y Diego para ver qué se puede aprovechar de ahí.

PPL y preparando una charla

Estuve perdiendo bastante tiempo compilando una biblioteca o librería (como quieran llamarla) para manejar polihedros llamada PPL (Parma Polyhedra Library). Por suerte una vez concluido todo el asunto con éxito, pude engancharla con Java y ejecutar un pequeño test. Ahora debería empezar a montar una interfaz para trabajar contra esta o cualquier otra librería de polihedros.

Además estuve empezando a armar slides para dar una charla interna este jueves a la gente de la oficina. Dani y Diego me estuvieron dando una mano revisando lo que había hecho, que creo que está dentro de todo bien. Falta ampliar un poco algunas secciones y agregar algunas imágenes.

Frío, código y finde largo

¡Nieve en Buenos Aires! Tenía que decirlo, bueno, ahora lo "importante":

Durante el finde largo y las últimas horas de este martes que se va programé la verificación en tiempo de ejecución de los predicados tales como invariantes, precondiciones, etc. Falta verificar que los variantes decrecen.

De todas formas eso no es más que un pasatiempo para demorar las decisiones que tarde o temprano va a haber que tomar.

Por un lado quiero darle una segunda oportunidad a Simplify, un demostrador desarrollado por Compaq (cuando todavía existía) y que a Dani en un primer momento no le cerró, pero vi un par de personas que lo usan para cosas con cuantificadores (¡muchos cuantificadores!) y quiero ver cómo se comporta.

Por otro lado está la idea de usar mútiples demostradores en paralelo y ver cuál demuestra primero, de esta forma se aprovechan los puntos fuertes de cada uno.

Está también la idea, que debería empezar a delinear, de realizar ejecución simbólica de instrucciones sobre un dominio abstracto abstracto (sí, repetí abstracto).

Por último a mi me gustaría decidir cómo incorporar los arreglos. Una forma es dando un soporte genérico (instrucciones de store y load). Otra forma es dar una única operación sobre la cual podamos controlar un poco más, aunque no me queda muy claro cómo.

Ah, además Diego insiste (y con razón) en que lea un poco más, cosa que quiero hacer, pero una vez que haya decidido (más o menos) para donde encarar.

Cerrando la semana

Estuve laburando en integrar un demostrador genérico. Para no complicarse con librerias lo hago a travez de un llamado al programa y me engancho escribiendo en su input, leyendo su output desde java, lo cual permite integracion con cualquier demostrador para el cual contemos con:

• un ejecutable
• un convertidor de mis predicados a predicados en el lenguaje del demostrador
• un intérprete para la salida del demostrador que mapee a VALID, INVALID, UNKNOWN

También estuve generando código java a partir de nuestros programas y lo que quedó funciona muy bien (¡incluso los genera sin warnings!). Lo que por ahora (por falta de tiempo) no hace es generar código (assertions) que verifiquen que las pre y post valen en tiempo de ejecución.

Por último estuve jugando con los dos demostradores (yices y cvc) para ver que tanto se bancan arrays y cuatificadores. En mi experiencia cada vez que digo algo cuantificado universalmente la respuesta es unknown. Realmente estoy empezando a dudar seriamente de que algo con arrays pueda llegar siquiera a hacerse (siempre y cuando nos quedemos en el mundo de los demostradores automáticos). En caso de que esto sea tan malo como parece, creo que vamos a necesitar un "plan b"... porque introducir arrays sería equivalente a demostrar todos los programas EXCEPTO aquellos que tienen arrays... algo bastante ridículo.

Un nuevo demostrador, velitas y desilución

El martes leyendo por ahí alguna web que ya no recuerdo, encontré un demostrador que se llama Yices, que le gana a todo el resto según los resultados de una competencia llamada SMT-COMP.

El miércoles cumplí 24 años. A pesar de que estuve en la facu un rato, mucho no laburé.

El jueves, o sea, hoy, implementé el binding necesario para utilizar este otro demostrador. Y me llevé una triste sorpresa al comprobar que no soporta bajo ningún concepto aritmética no lineal. O sea... que no me sirve para casi nada...

Sin procedimientos

Después de charlar con Diego y Dani llegamos a la conclusión de que por lo pronto iremos para adelante sin procedimientos, volviendo a la vieja idea de los bloques con pre y postcondiciones.

Hoy programé un rato y finalmente lo tengo andando: verifica loops y todo.

Además me contestó la gente de CVC3, diciendo que todavía no tuvieron tiempo de ver un bug report que les envié, pero que cualquier novedad me lo harían saber.

¿Procedimientos?

Después de varios días de reestructurar código llegué a una especie de callejón sin salida al querer implementar bloques con pre y post condiciones.

No queda claro qué cosas modifican y qué cosas no y cómo vincular esto con el resto del código que envuelve ese bloque.

Una forma posible de resolverlo es definir muy claramente cuál es la semántica con la que queremos trabajar con dichos bloques, pero creo que el problema es equivalente al de definir una semántica formal para trabajar con procedimientos.

Por lo tanto se me ocurre que es mejor optar por empezar a manejar procedimientos y matar dos pájaros de un tiro.

Arreglo todo, rompo todo, arreglo todo...

Ayer y hoy me dediqué a cambiar el lenguaje para incorporarle los scopes. Primero que nada tuve que cambiar la symbol table para que pueda trabajarse con distintas encarnaciones de un mismo nombre, y ahora estoy trabajando sobre los nombres de estados y otras yerbas.

Pero no todo es romper, ¡el otro día antes de cambiar el lenguaje pude demostrar la corrección de un programa que calcula la suma de los primeros n naturales! :)

¡Muy, muy contento!

Así es como me siento en este momento de la noche, en un día lleno de PROblemas políticos que se vienen en el horizonte.

Y no me siento culpable por sentirme así, ya que la causa de esta alegría es que encontré programando una forma de no pensar en lo nefasto de la situación que se viene...

En concreto, implementé soporte para loops y de esa manera el lenguaje sobre el que corro las verificaciones se volvió infinitamente más expresivo.

Ya demostré la corrección de un programa que calcula la copia de un número mediante incrementos de a uno y un programa que calcula el cociente y el resto de una división.

En estos días voy a ver de terminar de entender y luego implementar una forma de tratar scoping y generalizar el concepto de pre y post condiciones que se le ocurrió a Dani.

Una tarde charlando...

... en el comedor de la facu.

Repasamos junto con Dani y Diego los avances que hubo en la implementación que estuve haciendo y brevemente cómo seguir.

Por un lado quiero completar la posibilidad de analizar programas con ciclos, con la versión del lenguaje tal como está y a eso me voy a dedicar en el futuro inmediato.

Pero por otra parte el lenguaje está empezando a mostrar las primeras señales de que si no lo definimos formalmente nos va a estallar en la cara en el momento menos deseado.

Así que de acá a un tiempo no muy lejano la idea es definir lo mejor posible tanto el lenguaje intermedio como el de alto nivel (o al menos algunos lineamientos).

Hay que decidir cuestiones como:

• de qué forma se trabajará la semántica de parámetros,
  
• qué cosas se asumen como obvias en las post-condiciones (e invariantes) y no son necesarias decir (a = a@pre, b = b@pre, etc...),
• si el lenguaje de alto nivel se traducirá de forma sencilla o también este pasaje al intermedio requiere de análisis "semánticos" y validación de algunas cuestiones usando el demostrador.
• ¡un nombre por favor para el lenguaje alto y el intermedio así podemos hablar entre nosotros y saber a qué nos referimos!

¡Muy contento!

Después de algunos días construyendo un parser y definiendo una sintáxis abstracta, empecé a definir la semántica a través de traducciones a lógica.

Todavía no soporto ciclos, pero hace apenas 5 minutos pude demostrar la correctitud del siguiente programa, muy básico, pero algo al fin...

f(in a, out b)
:? a != 0
:! b > 10
{
____b <- 0
____c <- not a
____if a then {
________if c then {
________} else {
____________b <- b + 5
________}
________b <- b + 5
____} else {
________b <- b + 1
____}
____b <- b + 1
}

Idea

Tengo la impresión de que el lenguaje de especificación permite expresar formulas demasiado complejas (con varios niveles de anidamiento, etc.). Esto puede que perjudique el funcionamiento del demostrador.

Probar reduciendo la complejidad de las fórmulas al permitir únicamente comparar variables. Cualquier cosa más compleja deberá ser simulada creando variables y hacerlas valer lo que uno quiere comparar a través de instrucciones del lenguaje de programación.

Manos a la obra...

Charlamos con Dani y Diego. El objetivo a corto plazo es tener un lenguaje monoprocedural con enteros y arreglos. Este lenguaje le exige al programador que escriba una pre y una post condición las cuales pueden incluir cuantificadores acotados. Los ciclos deben incluir invariante y función variante.

Una vez definido la idea es basarme en una herramienta proof of concept de Dani para generar aserciones y consultas en un demostrador de teoremas que permitirá (si todo sale bien) demostrar la corrección del programa.

También estuvimos pensando en definir un segundo lenguaje, de nivel más alto que el primero donde ciertas construcciones modelen tipos de iteración comunes, para de esta forma tener ciertos invariantes precalculados. Supongo que esto lo veremos una vez que esté bien definido el lenguaje mencionado más arriba (que por ahora llamaré "lenguaje intermedio").

¿Quizás un rumbo nuevo?

Estuvimos charlando con Diego G. y Daniel G. porque existía la posibilidad de tomar un rumbo relativamente distinto en la tesis.

Dani propone analizar un lenguajecito muy chico, inventado por nosotros para demostrar que el código cumple con la especificación, suponiendo que el usuario provee precondición, postcondición e invariantes para los ciclos.

Si logramos hacer inferencia de invariantes con una herramienta similar a la de Diego P., luego la usabilidad sería relativamente alta y el lenguajecito podría ir creciendo hasta tener algo relativamente serio.

Veremos cómo sigue esto, es una opción más que interesante.

¡Y hoy paso el tiempo...

... resumiendo papers!

http://docs.google.com/Doc?id=dt3n7b3_5gmsg74

Leyendo, leyendo...

Después de un tiempo de peleas con el código de Diego P. estoy empezando a leer distintos artículos sobre temas relacionados con análisis de programas en general. Por ejemplo octágonos como dominio abstracto, modelado del heap, etc.

En algunos días actualizaré con una breve reseña de las cosas que estuve leyendo.

Como diría Mostaza...

Ardua tarea la de enfrentarse (sí, enfrentarse es el verbo adecuado) a un código escrito por otra persona hace bastante tiempo y que no tiene ningún tipo de documentación. Uno vuelca en el código que hace parte de su forma de ser, de pensar. Por lo tanto lidiar con código de otra persona siempre es distinto que hacerlo con código propio.

El proceso de estas primeras semanas fue apropiarme, en el mejor sentido de la palabra, del código de Diego P. Y se podría decir que ya casi lo he logrado.

Si bien no comprendo del todo el 100% de los detalles, he llegado a tener una idea general de que hace cada una de las clases importantes. Algunas ideas que me ayudaron a hacer que el código me resulte más familiar:

• Cambiar el estilo de indentación y formato por el que yo uso. Esto lo hizo el Eclipse de forma automática.
• Documentar en el código los descubrimientos que voy haciendo, ningún lugar es más accesible que el propio código, especialmente cuando la IDE maneja esa documentación de forma automática.
• Renombrar las variables, métodos y clases para que tengan nombres que me resulten adecuados a mi entendimiento del código.
• Estructurar los paquetes o módulos o incluso jerarquía de clases a medidad que comprendo su funcionalidad y detecto cosas que hubiera hecho distinto.

Cabe aclarar que todos estos cambios no quieren decir que el código original sea malo, simplemente fue hecho por otra persona. Otra persona que ya no lo usará más y ahora quien debe hacer un fuerte uso y reingeniería soy sólo yo. Si tuviera que compartir ese código con la persona que lo hizo u otros desarrolladores no lo tocaría o consultaría primero.

Dejado esto en claro ahora tengo dos objetivos sobre el código:

1. Entender un poco más las clases de los paquetes analysis y variable. El resto de los paquetes ya están bastante digeridos.
   
2. Leer un poco sobre la fase callgraph de soot y ver cómo se relaciona con el análisis que hace Diego P. en su tesis.

Con respecto a lo teórico me gustaría releer Fundamentals of Program Analysis, un libro que me prestó Diego G. y que explica la teoría más básica detrás de los análisis de programas (reticulados, dataflow, may, etc.).

Javadoc, javadoc, ...

Sigo día a día leyendo distintas clases y tratando de dilucidar su función, su rol. Me siento como enfrente a un gran rompecabezas, examino cada pieza y me fijo como se lleva con las demás.

Es una tarea repetitiva y cansadora, por eso la llevo de a poco, pero de forma relativamente constante. Estimo de acá a una semana o como mucho dos tener ya todo el código revisado y con una primera idea de qué hace cada parte.

A partir de ahí la idea es dejar por un tiempo el código y pasar a pensar en papel cómo implementar analisis interprocedural simbólico con el heap ahí haciendo lío en el medio.

Un domingo productivo

Hoy trabajé todo el día en la tesis. Sin proponérmelo surgió una nueva estrategia. El código de Diego P. no tiene javadoc, con lo cual es difícil de seguir. Mi idea fue empezar a documentar para familiarizarme, y de paso hacerlo vía javadoc para que me sirva más adelante y también a otras personas que quieran seguir usando ese código (allá ellos...).

Además estuve cambiando la estructura de paquetes, que no se si fue muy buena idea, pero estos días voy a seguir con esa línea.

Un avance

¡Funcionó! Hoy hice andar la tesis de Diego P. en la compu de mi casa, luego de varios intentos y peleas está funcionando perfectamente.

El objetivo para estos próximos días es principalmente lograr entender el código (e ir comentando y cambiando el estilo para hacerlo más familiar). De forma adicional, voy a ver si cambio la librería de poliedros, pero no parece ser tarea sencilla...

Algunos avances

Me siento en mi nueva compu en la oficina de la facultad (la anterior está actualmente ocupada, así que mi nuevo "hogar" es terminus). El primer panorama es desolador, todo el software desactualizado y sin acceso a internet.

Me paso el primer día viendo por qué no hay acceso a internet hasta que en mi desesperación intento cambiar el cable ethernet y lo logro. Luego me dedico durante una noche a actualizar sus paquetes (la velocidad durante el día haría de esta una tarea tortuosa). Paso a paso me voy sintiendo nuevamente en una compu "mía".

Otro tema técnico es que el servidor de dependex está roto, su disco se quemó y por lo tanto instalé un precario servidor de cvs en casa.

(CVSROOT :pserver:gdecaso@tetrix.hopto.org:2401/tesis).

Un buen paso fue lograr hacer andar la tesis de Diego P. en la computadora que él usaba y luego casi lograrlo en mi nueva compu, sólo con un error (espero menor) de javax.crypto.cipher.

Charla con Diego G.

Hoy me reuní con mi director para discutir aspectos de la tesis. Los dos coincidimos en que el punto central de la misma es realizar una buena técnica de análisis interprocedural que primordialmente esté formalizada.

La escalabilidad es un tema a tener en cuenta, pero no es el objetivo número uno, especialmente teniendo en cuenta que se trata del primer acercamiento al tema.

También discutimos brevemente sobre la representación del heap y otras cuestiones como aplicaciones posibles del trabajo o de que manera trabajar con contratos hechos por otras personas, etc.

Mañana trabajaremos juntos intentando hacer andar la tesis de Diego P., tarea que me está resultando un tanto más compleja de lo que esperaba. Diego G. dice que en "negritus" (una de las máquinas de la oficina) hay una versión funcionando, veremos...

Primeros pasos

El día de ayer me dediqué a instalar Eclipse en su versión 3.2.2 y la JDK 6 de Java en mi Kubuntu Dapper Drake. Debido a problemas de velocidad en mi conexión a internet, fue recién a las 20 horas que pude tener todo andando.

Entonces creé un nuevo proyecto pero, contrario a lo que dije ayer, me dediqué a importar todas las cosas de Diego P. en el mismo. Sin embargo tuve problemas para hacer andar JNI contra las librerías de PolyLib, por lo tanto mi objetivo para hoy es o bien arreglar tal vínculo, o ceder y empezar a probar con JNA.

Algunos puntos de comienzo

La tesis consta de extender un trabajo hecho por Diego P. hace aproximadamente un año. Cuento aquí con los fuentes de su trabajo y el primer objetivo es tener un conocimiento relativamente completo sobre ellos.

Para esto se me ocurren 2 opciones:

1. Importarlos de forma completa como un proyecto en Eclipse e intentar lograr que compile, recorrer el código de arriba a abajo y abajo a arriba para entender de a poco.
   
   
2. Crear un proyecto nuevo e importar archivos, clases o funcionalidades a medida que los voy necesitando.

Me convence más la segunda, ya que si bien tardaré un poco más, cada línea de código, cada clase al menos habrá sido tenida en cuenta y habrá muy poco código ajeno a mi entender.

A esto se le suma que el proyecto de Diego P. utiliza una librería para tratar poliedros, la PolyLib, según Diego G., mi director, esta librería tiene muchos problemas de memoria y performance.

Dado que comenzaré el proyecto "de cero" pienso usar en cambio la PPL, una librería hecha en Italia, que aparentemente funciona mucho mejor.

Hay un problema, tanto PolyLib como PPL están desarrolladas en C++, y la tesis será desarrollada en Java. Para hacer llamados a librerías nativas desde Java hay que usar JNI, lo cual es muy difícil según me han dicho.

Existe una interface más sencilla, llamada JNA, que aparentemente facilita la integración, evitando tener que lidiar con JNI directamente.

Por lo tanto, los objetivos para estos primeros días:

• Crear un nuevo proyecto Java
• Importar de a poco los contenidos de la tesis de Diego P. hasta tener un conocimiento amplio de ellos
• Instalar PPL
• Conectar el proyecto Java con PPL usando JNA

Esta primera fase culminaría cuando mi nuevo proyecto logre reproducir la funcionalidad de la tesis de Diego P. pero con la nueva librería, supuestamente mejor que la anterior.

Objetivo secundario: para poder realizar comparaciones sería interesante que la librería de poliedros se pueda seleccionar entre estas dos opciones (y posiblemente otras en el futuro).

Empecemos

Hace pocas semanas que regreso de un viaje que me ha hecho recorrer gran parte de Argentina y Bolivia por lapso de varios meses. Energía, ganas, la mente bien fresca es lo que caracteriza mi estado de ánimo al tocar nuevamente el viejo terruño porteño.

Pero esta historia comienza un tiempo atrás, un tiempo pretérito en el cual el año actual era el 2003 y la gente era más buena que ahora, todo más barato y la pizza más rica, como en todo tiempo pasado.

¿Por qué el 2003? ¿Por qué no comenzar en 1983? ¿Por qué no en 1916 y por qué no en 1492? En algún punto hay que poner el cero, es una cuestión de referencias. Dado que este blog intenta acompañar el fin de mis estudios universitarios, nada mejor que remontar su inicio a los comienzos de estos.

Allá por 2003, me anoto en mi carrera y comienzo el sinuoso, tortuoso, trabajoso, penoso andar por cursadas, trabajos prácticos y finales. Rudimentos básicos de álgebra y análisis matemático, nociones de probabilidad y estadística, incursiones en algoritmos y estructuras de datos... una a una las asignaturas van quedando atrás.

Toda vivencia guardada en nuestra memoria está condicionada no sólo por la forma en la que uno la sintió, sino por todo lo que transcurrió hasta el momento en que uno elige recordar. El caso de mis cursadas no es la excepción.

En su momento eran dolores de cabeza, nervios antes de los exámenes, sufrimiento por sentir que uno no llegaba con las cosas en tiempo y/o forma... hoy miro atrás con cierta melancolía y pienso "no era tan grave".

Luego de 4 años de cursada libré una a una las batallas que cada materia planteaba, y victorioso, en diciembre decidí tomarme unas largas vacaciones. Volvemos entonces al punto de partida, vuelvo del viaje con ganas renovadas, con nuevo objetivo también.