Preprocesor Java bytecode pro verifikační nástroje
| Thesis title in Czech: | Preprocesor Java bytecode pro verifikační nástroje |
|---|---|
| Thesis title in English: | Java Bytecode Preprocessor for Program Verification Tools |
| Key words: | Java, JVM, bytecode, transformace kódu, verifikace programů |
| English key words: | Java, JVM, bytecode, code transformation, program verification |
| Academic year of topic announcement: | 2014/2015 |
| Thesis type: | diploma thesis |
| Thesis language: | čeština |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Pavel Parízek, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 08.06.2015 |
| Date of assignment: | 11.06.2015 |
| Confirmed by Study dept. on: | 19.06.2015 |
| Date and time of defence: | 16.06.2016 09:00 |
| Date of electronic submission: | 13.05.2016 |
| Date of submission of printed version: | 13.05.2016 |
| Date of proceeded defence: | 16.06.2016 |
| Opponents: | doc. RNDr. Petr Hnětynka, Ph.D. |
| Guidelines |
| Mnoho verifikačních nástrojů pro jazyk Java klade určitá omezení na vstupní program. Kód programu například nemůže obsahovat určité posloupnosti instrukcí.
Pokud vstupní program tyto podmínky nesplňuje, tak může verifikace skončit chybou nebo spočítá nepravdivý výsledek. Autoři verifikačních nástrojů se zaměřují spíše na vlastní algoritmy, a technické a implementační detaily odsouvají na pozdější dobu. Tato práce se zabývá nástroji J2BP a PANDA, které analyzují zkompilované Java programy na základě technik predikátové abstrakce. Práce má následující hlavní cíle: (1) Rozpoznat posloupnosti instrukcí Java bytecode, které nejsou korektně zpracovány nástroji J2BP a PANDA; (2) Navrhnout a implementovat transformace Java bytecode, které nahradí všechny problematické posloupnosti instrukcí tak, že nástroje J2BP a PANDA dokáží výsledný program korektně zpracovat. Dalším cílem práce je implementovat transformace, které budou nahrazovat volání některých agregovaných metod na třídách kolekcí jazyka Java (jedná se například o metody putAll a containsAll) za ekvivalentní bytecode, který bude obsahovat pouze volání odpovídajících primitivních metod (například put nebo contains) a bežné řídící struktury jazyka Java. Výsledkem práce bude samostatná aplikace, která se použije jako preprocesor pro nástroje J2BP a PANDA. |
| References |
| 1. J2BP: Predicate Abstraction for Java Programs. https://github.com/d3sformal/j2bp
2. PANDA: Predicate Abstraction in Dynamic Analysis. https://github.com/d3sformal/panda 3. ASM: Java Bytecode Manipulation Framework. http://asm.ow2.org/ 4. Polyglot extensible compiler framework. http://www.cs.cornell.edu/projects/polyglot/ 5. JAstAddJ: The JastAdd Extensible Java Compiler. http://jastadd.org/web/jastaddj/ |