Entorn per a l'anàlisi de terminació de programes

Entorn per a l’an`alisi de terminaci´o de programes Pau Castells Diumenj´o Treball Final de Grau Director: Albert Rubio Gimeno Departament: Llenguatges i Sistemes Inform`atics Data de la defensa: 30 de juny del 2014 Grau en Enginyeria Inform`atica (Computaci´o) Facultat d’Inform`atica de Barcelona (FIB) Universitat Polit`ecnica de Catalunya (UPC) BarcelonaTech Agra¨ıments A l’Albert Rubio, el director del projecte, per tota la paci`encia que ha tingut i per haver-me confiat aquest projecte. Als meus pares i la meva fam´ılia, si no fos per ells hagu´es abandonat fa molt de temps. Als meus amics, especialment al Manel, que m’han animat i ajudat en els moments m´es dif´ıcils. 3 4 ´ Index 1 Resum del projecte 7 1.1 Catal`a............................... 7 1.2 Castell`a .............................. 8 1.3 Angl`es............................... 9 2 Introducci´o 11 2.1 Motivacions............................ 11 2.2 Objectius del treball . . . . . . . . . . . . . . . . . . . . . . . 11 2.3 Context .............................. 12 2.4 Utilitats.............................. 12 2.5 Productes similars . . . . . . . . . . . . . . . . . . . . . . . . 12 2.6 Impacte Mediambiental . . . . . . . . . . . . . . . . . . . . . 14 2.7 Estructura de la mem`oria . . . . . . . . . . . . . . . . . . . . 14 3 Planificaci´o 15 3.1 Descripci´o de tasques . . . . . . . . . . . . . . . . . . . . . . . 15 3.2 Retards i solucions . . . . . . . . . . . . . . . . . . . . . . . . 16 3.3 Diagrama de Gantt . . . . . . . . . . . . . . . . . . . . . . . . 16 3.4 Planificaci´o inicial i variacions . . . . . . . . . . . . . . . . . . 16 4 Planificaci´o econ`omica del projecte 19 4.1 Identificaci´o de recursos . . . . . . . . . . . . . . . . . . . . . 19 4.2 Estimaci´o de costos . . . . . . . . . . . . . . . . . . . . . . . . 19 4.3 Viabilitat del projecte . . . . . . . . . . . . . . . . . . . . . . 20 4.4 Variacions respecte la planificaci´o original . . . . . . . . . . . 20 5 Conceptes te`orics 21 5.1 Components fortament connexes . . . . . . . . . . . . . . . . 21 5.2 Invariants ............................. 22 5.3 Termination Implication . . . . . . . . . . . . . . . . . . . . . 22 5.4 FuncionsdeRanking....................... 23 5 6´ INDEX 6 Implementaci´o del projecte 25 6.1 Parser ............................... 25 6.1.1 Gram`atica......................... 25 6.2 Comprovador de terminaci´o . . . . . . . . . . . . . . . . . . . 26 6.2.1 Estructures de dades . . . . . . . . . . . . . . . . . . . 26 6.2.2 Algorismes utilitzats . . . . . . . . . . . . . . . . . . . 26 6.2.3 Eliminar locations i transicions . . . . . . . . . . . . . 28 6.2.4 Comprovaci´o dels invariants . . . . . . . . . . . . . . . 28 6.2.5 Comprovaci´o de les termination implications . . . . . 29 6.2.6 Comprovaci´o de les funcions de ranking . . . . . . . . 30 6.2.7 Test de feasibility . . . . . . . . . . . . . . . . . . . . . 31 6.3 Desenvolupament de la web . . . . . . . . . . . . . . . . . . . 31 6.3.1 Interf´ıcie.......................... 32 6.3.2 Servidor.......................... 32 6.4 Testing .............................. 33 7 Conclusions 35 7.1 Valoraci´o personal . . . . . . . . . . . . . . . . . . . . . . . . 35 7.2 TreballFutur ........................... 35 Bibliografia 37 Cap´ıtol 1 Resum del projecte 1.1 Catal`a El problema de la terminaci´o ha tingut un augment en l’inter`es, encara que es tracta d’un problema indecidible. Aix`o es deu al fet que l’an`alisi de terminaci´o est`a en un punt on crear eines per provar terminaci´o autom`aticament ´es factible. Per`o el resultat d’aquestes eines normalment est`a basat en codi complex que pot donar resultats erronis. Per aix`o cal verificar que els resultats que s’obtenen amb aquestes eines s´on correctes. Aquest projecte presenta una eina que comprova si els resultats d’an`alisi de terminaci´o generats pel programa CppInv s´on correctes o no. Per a realitzar aquestes comprovacions, l’eina verifica que els invariants generats s´on correctes, i aplicant les funcions de ranking i les implicacions de terminaci´o verifica que la demostraci´o de terminaci´o del programa ´es correcte. Finalment, aquest projecte tamb´e presenta una web que permet als usuaris realitzar un an`alisi de terminaci´o del seu codi. 7 8CAP´ ITOL 1. RESUM DEL PROJECTE 1.2 Castell`a El problema de la terminaci´on ha aumentado en inter´es, aunque se trata de un problema indecidible. Esto se debe a que el an´alisis de terminaci´on est´a en un punto en el que crear instrumentos para probar la terminaci´on autom´atica es factible. Pero el resultado de estos instrumentos normalmente est´a basado en c´odigo complejo que puede dar resultados err´oneos. Es por este motivo que es necesario verificar que los resultados que se obtienen con estos instrumentos son correctos. Este proyecto presenta un instrumento que comprueba si los resultados de los an´alisis de terminaci´on generados por el programa CppInv son correctos o no. Para realizar las comprobaciones, el instrumento verifica que los invariantes generados son correctos y aplicando las funciones de ranking y las implicaciones de terminaci´on verifica que la demostraci´on de terminaci´on del programa es correcta. Finalmente, este proyecto tambi´en presenta una web que permite a los usuarios realizar un an´alisis de terminaci´on de su c´odigo. 1.3. ANGL ` ES 9 1.3 Angl`es Over the last years, the interest in the Halting Problem has increased. It is still, however, a undecidable problem. Nowadays, even if it is possible to create algorithms/methods/tools to prove automatic termination, the result of these algorithms/methods/tools is normally based on complex code, which can lead to wrong results. As a consequence, it is essential to make sure that the results obtained from these algorithms/methods/tools are correct. This thesis introduces a algorithm/method/tool to check whether the termination analysis results obtained from the program CppInv are correct or not. To achieve this, the aformentioned algorithm/method/tool checks if the generated invariants are correct, and by applying ranking functions and termination implications verifies if the termination demonstration is correct. Last but not least, this thesis also presents a web that enables regular users to perform a termination analysis of their code. 16 CAP´ ITOL 3. PLANIFICACI ´ O 3.2 Retards i solucions La planificaci´o inicial tenia com a objectiu presentar el projecte el febrer, per`o no ha sigut possible per motius laborals, entre d’altres. Aix`o ha suposat moure el projecte del per´ıode de setembre a febrer, al per´ıode de gener a juny. 3.3 Diagrama de Gantt Les figures 3.1 i 3.2 mostren el diagrama de Gantt al final del projecte. Figura 3.1: Tasques del diagrama de Gantt al final del projecte Figura 3.2: Taula de temps del diagrama de Gantt al final del projecte Podem veure que la tasca de desenvolupar la web s’ha portat a terme durant tot el projecte, per`o nomes perqu`e s’havia d’anar fent petites modificacions. 3.4 Planificaci´o inicial i variacions Com podem veure en les figures 3.3 i 3.4 la planificaci´o final ha sigut bastant diferent a la que es va proposar a la fita inicial. A la tasca inicial es va proposar una tasca de simplificaci´o de resultats, que per manca de temps no s’ha fet. Tamb´e es poden observar variacions en l’ordre de les tasques. 3.4. PLANIFICACI ´ O INICIAL I VARIACIONS 17 Figura 3.3: Tasques del diagrama de Gantt a la planificaci´o inicial Figura 3.4: Taula de temps del diagrama de Gantt a la planificaci´o inicial Finalment s’ha actuat desenvolupant primer la part web, quan a la fita inicial es plantejava com una tasca a fer cap al final. 18 CAP´ ITOL 3. PLANIFICACI ´ O Cap´ıtol 4 Planificaci´o econ`omica del projecte 4.1 Identificaci´o de recursos Els recursos que es necessiten per dur a terme aquest projecte s´on els seg¨uents: •Recursos humans: Calen diferents persones que realitzin una feina determinada. ´ Es necess`aria la presencia d’un programador, una persona que realitzi el testing, un dissenyador web i una persona encarregada de dirigir i documentar el projecte. •Recursos materials: Cal un ordinador per persona i un servidor. 4.2 Estimaci´o de costos Amb la finalitat d’estimar els costos d’aquest projecte, considerem que les hores necess`aries s´on 400. El calcul estimat de hores treballades (Figura 4.1) ser`a de 4 hores al dia. Encara que no es dedicaran 8 dies en fer la documentaci´o, sin`o que se’n dedicaran m´es per`o menys hores diaries, s’ha estimat que seria equivalent a 8 dies a mitja jornada. Tamb´e podem veure els costos en materials (Figura 4.2). Com podem observar les hores estimades al servidor estan en forma de multiplicaci´o, ja que estar`a enc`es les 24 hores del dia, i aix`o significa uns 2,40 ¤/ dia. Per tant s’hauria d’intentar encendre el servidor com m´es tard millor. He estimat que el cost per hora de l’electricitat ´es de 10 c`entims d’euro. 19 20 CAP´ ITOL 4. PLANIFICACI ´ O ECON ` OMICA DEL PROJECTE C`arrec Preu de treball Documentaci´o Estat de l’art Implementar Interf´ıcie Web Testing Total (h) Cost total M`anagers 60 ¤/h 8 0 0 0 0 32 1.920¤ Programador 30 ¤/h 0 5 50 0 0 220 6.600¤ Dissenyador 20 ¤/h 0 0 0 16 0 64 1.280¤ Tester 20 ¤/h 0 0 0 0 10 40 800¤ 10.600¤ Figura 4.1: Costos dels treballadors i dies dedicats en cada feina Estimem que el preu mig que t´e un ordinador ´es de 500¤. Recurs Cost inicial Cost hora Hores estimades Cost total Ordinador 4x500 ¤0.10 ¤/h 400 2.040¤ Servidor 1000 ¤0.10 ¤/h 24x21 1.050,4¤ 3.090,4¤ Figura 4.2: Costos de les eines de treball 4.3 Viabilitat del projecte Aquest projecte forma part d’un projecte major. No es poden estimar beneficis econ`omics vinculats directament a aquesta part del projecte, per`o la viabilitat com a eina de recerca i de doc`encia ´es elevada. 4.4 Variacions respecte la planificaci´o original Hi ha hagut una petita variaci´o. En la planificaci´o inicial nom´es es va contemplar un ordinador. Aix`o ha canviat a un ordinador per persona que treballa en el projecte, augmentant els costos del projecte en 1.500¤. Cap´ıtol 5 Conceptes te`orics Com ja s’ha comentat, aquest projecte verifica el resultat d’un analitzador de terminaci´o de programes, per ser concrets el CppInv. El CppInv transforma el codi del programa que ha d’analitzar en un sistema de transicions. Un sistema de transicions S= (υ, L,Θ,T) consisteix en una tupla de variables υ, un conjunt de locations L, un array associatiu, o map, Θ de locations a f´ormules amb els valors inicials de les variables, i un conjunt de transicions T. Cada transici´o τ∈ T est`a composta per una tripleta (`, `0, ρ), on `,`0∈ L s´on la location d’origen i la location de dest´ı, iρ´es la relaci´o de transici´o: una f´ormula sobre les variables del programa υi les seves versions primades υ0, que representen els valors de les variables al sortir d’una transici´o. A partir d’aqu´ı, assumim que les variables tenen valors enters i els programes lineals, ´es a dir: les condicions inicials Θ i les relacions de transici´o ρ estan descrites com conjuncions de desigualtats lineals. Gr`acies al tipus enter de les variables, es poden traduir les desigualtats estrictes a desigualtats no estrictes, ja que: x>n≡x≥n+ 1, n, x ∈Z. Al finalitzar l’an`alisi de terminaci´o, el CppInv mostra el sistema de transicions que ha generat seguit dels m`etodes utilitzats per demostrar la terminaci´o del codi. A continuaci´o s’expliquen aquests m`etodes. 5.1 Components fortament connexes Es diu que un graf dirigit ´es fortament connex, si per cada parella de v`ertexs uivhi ha un cam´ı que va de uavi un cam´ı que va de vau. Les components fortament connexes o SCC(strongly connected component) d’un graf dirigit s´on els subgrafs de mida m`axima fortament connexos. Cada graf nom´es t´e una ´unica representaci´o de components fortament connexes. Podem veure una representaci´o dels SCC d’un graf a la figura 5.1. 21 22 CAP´ ITOL 5. CONCEPTES TE ` ORICS AB C Figura 5.1: Exemple de SCC 5.2 Invariants Un invariant ´es una condici´o que es compleix sempre que s’arriba a un determinat punt del programa. ´ Es usual buscar invariants que descriguin el comportament dels bucles. En aquest cas es volen generar invariants inductius. Es diu que una propietat µ´es un invariant inductiu si: •Iniciaci´o: per cada location `∈ L : Θ(`)|=µ(`) •Consecuci´o: per cada transici´o τ= (`, `0, ρ)∈ T :µ(`)∧ρ|=µ(`0)0 5.3 Termination Implication Una termination implication ´es una funci´o que es crea per intentar demostrar que les transicions no s’executen de manera infinita. Es diu que una propietat J`´es una termination implication en una location `si: •Condici´o: per cada transici´o τ= (ˆ `, `, ρ)∈ T :Iˆ `∧ρ|=J0 ` 5.4. FUNCIONS DE RANKING 23 Com a conseq¨u`encia, per cada transici´o que surti de `tindrem que: •ˆτ= (`, `0, ρ)∈ T ser`a ˆτ= (`, `0, ρ ∧J`). 5.4 Funcions de Ranking L’idea b`asica que es segueix per demostrar la terminaci´o d’un programa ´es que cap transici´o es pot executar de manera infinita. Per comen¸car cap transici´o eliminada pot executar-se infinitament. Per tant, nom´es cal mirar transicions que ajuntin dues locations del mateix SCC, ja que si una transici´o s’executa una vegada i una altra, aleshores les locations d’origen i desti d’aquesta pertanyen al mateix SCC. Assumim que es troba una ranking function per una transici´o τ, d’acord amb: Sigui τ= (`, `0, ρ) una transici´o, tal que `i`0pertanyen al mateix SCC que anomenem C. Es diu que una funci´o R:υ−→ Z´es una ranking function per τsi: •Acotaci´o: ρ|=R≥0 •Decreixement estricte: ρ|=R > R0 •No creixement: Per cada ˆτ= (ˆ `, ˆ `0,ˆρ)∈ T tal que: ˆ `, ˆ `0∈C: ˆρ|= R≥R0 24 CAP´ ITOL 5. CONCEPTES TE ` ORICS Cap´ıtol 6 Implementaci´o del projecte Aquest cap´ıtol de la mem`oria explica la implementaci´o del projecte. 6.1 Parser Per comen¸car, es necessitava llegir i interpretar l’entrada del programa i poder-la guardar en estructures amb les que fos f`acil treballar. Per aix`o calia fer un parser. Es va decidir utilitzar ANTLR[7] com a eina per generar el codi de la gram`atica. 6.1.1 Gram`atica Les f´ormules d’entrada del programa tenen un format semblant a aquest: (y=0) /\ (-x<=0) /\ (-x+1<=0) /\ (x-x’-1=0) /\ (y-y’+1=0) Per tant nom´es cal definir una gram`atica simple que transformes aquesta entrada en un arbre f`acil de rec´orrer[8]. ∧ ∧ ∧ ∧ = y 0 <= − x 0 <= + − x 1 0 = − − x x0 1 0 = + − y y0 1 0 25 32 CAP´ ITOL 6. IMPLEMENTACI ´ O DEL PROJECTE 6.3.1 Interf´ıcie La interf´ıcie de la web ´es bastant senzilla. Com la majoria de p`agines web amb finalitats similars, per exemple compiladors o int`erprets online, s’ha prioritzat la funcionalitat a l’est`etica. Es pot veure una imatge de la p`agina d’inici a la figura 6.2. Figura 6.2: P`agina inicial La p`agina d’inici permet introduir el codi que es vol analitzar mitjan¸cant un camp de text o carregant un fitxer de codi. Si es vol fer mitjan¸cant la primera opci´o cal indicar si el codi est`a escrit en C++ o en T2. En canvi, si es decideix afegir el codi mitjan¸cant un arxiu, ´es necessari que aquest arxiu tingui l’extensi´o correcta. Per acabar, la p`agina web permet crear comptes d’usuari (Figura 6.3). Els usuaris registrats poden consultar els enviaments que havien realitzat (Figura 6.4) i descarregar-ne els arxius enviats i les seves demostracions. 6.3.2 Servidor El servidor, que est`a allotjat en una m`aquina Linux de la UPC, crea de manera din`amica la p`agina web que est`a escrita en PHP i HTML. Mitjan¸cant 6.4. TESTING 33 Figura 6.3: Formulari de registre de l’usuari Figura 6.4: Llista de consultes realitzades per l’Usuari1 crides per terminal, el servidor executa els programes necessaris per realitzar la demostraci´o de terminaci´o. En un altre servidor MySQL, hi ha emmagatzemades les bases de dades que guarden les dades dels usuaris registrats i de les consultes que realitzen. 6.4 Testing Per a verificar que els resultats que mostra el programa s´on correctes, s’ha utilitzat, com a joc de proves, un subconjunt d’enviaments fets a l’eina educativa Jutge.org[12] i una llista amb m´es de 250 exemples en el llenguatge, que descriu sistemes de transicions, T2. 34 CAP´ ITOL 6. IMPLEMENTACI ´ O DEL PROJECTE Cap´ıtol 7 Conclusions Gr`acies als resultats obtinguts durant la fase de testing i altres proves fetes, es pot dir que el programa CppInv ´es una eina molt eficient i que les demostracions de terminaci´o que genera s´on correctes. 7.1 Valoraci´o personal Considero que aquest projecte ha estat bastant complet, ja que he utilitzat coneixements que he adquirit en moltes assignatures diferents de la carrera. I no nom´es aix`o, sin´o que m’ha donat l’oportunitat d’aprendre m´es coses sobre les bases de dades i de treballar amb llenguatges que gaireb´e no coneixia com PHP o HTML. 7.2 Treball Futur Com s’explica a la introducci´o, aquest projecte comprova que les demostracions de terminaci´o del CppInv siguin correctes. Com que el CppInv no nom´es genera demostracions de terminaci´o, encara queda feina a fer: •Comprovar solucions de no terminaci´o S’hauria d’implementar i afegir un comprovador de demostracions de no terminaci´o al comprovador de terminaci´o. •Simplificar les demostracions que genera A vegades, les demostracions que genera el CppInv poden resultar dif´ıcils d’entendre i les funcions de ranking poden tenir valors massa alts, caldria simplificar les demostracions que genera i fer-les m´es f`acils d’entendre pels usuaris. •Millorar els algorismes sobre grafs Es podria millorar l’algorisme de reachability (Secci´o 6.2.2) per no 35 36 CAP´ ITOL 7. CONCLUSIONS haver de mirar, cada vegada que s’elimina una transici´o, si alguna location deixa de ser accessible. Bibliografia [1] Alan Turing, ”On computable numbers, with an application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society, Series 2, 42 (1936), pp. 230-265. [2] D. Larraz, A. Oliveras, E. Rodr´ıguez-Carbonell i A. Rubio, ”Proving Termination of Imperative Programs Using Max-SMT”. In: Proc. FMCAD ’13, 2013. [3] B. Cook, A. Podelski i A. Rybalchenko, ”T2 termination prover”, http://research.microsoft.com/en-us/projects/t2/ [4] M. Bofill, R. Nieuwenhuis, A. Oliveras, E. Rodr´ıguez-Carbonell i A. Rubio, ”The Barcelogic SMT Solver”, in CAV, ser. LNCS, vol. 5123. Springer, 2008, pp. 294-298. [5] C. Otto, M. Brockschmidt, C. Von Essen i J. Giesl, ”Automated Termination Analysis of Java Bytecode by Term Rewriting”, http://aprove.informatik.rwth-aachen.de, 2010. [6] A. Rybalchenko, ”ARMC: Abstraction Refinement Model Checker”, https://www7.in.tum.de/˜rybal/armc/, Agost 2011. [7] Terence J. Parr, ”Language Translation Using PCCTS and C++, A reference guide”, Automata Publishing Company, 1993. [8] G. Godoy i R. Ferrer i Cancho, ”Parsing and AST construction with PCCTS”, Universitat Polit`ecnica de Catalunya, 2011. [9] Tarjan, R. E. (1972), ”Depth-first search and linear graph algorithms”, SIAM Journal on Computing 1 (2): pp. 146-160, doi:10.1137/0201010. [10] David R. Cok, ”The SMT-LIBv2 Language and Tools: A Tutorial”. http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf Mar¸c 2013. [11] ”The PHP micro-frameworkbased on the Symfony2 Components.” http://silex.sensiolabs.org/. 37 38 BIBLIOGRAFIA [12] J. Petit, O. Gim´enez i S. Roura, ”Jutge.org: an educational programming judge”, in SIGCSE, AMC, 2012, pp. 445-450.