Síntesis de código de bajo nivel mediante programación con restricciones

Abstract

La super-optimización es una técnica que busca encontrar la secuencia de instrucciones óptima a una dada explorando secuencias equivalentes. Esta técnica es muy efectiva resolviendo optimizaciones complejas, pero implementarla es muy costosa computacionalmente. En este trabajo de fin de grado buscamos explorar técnicas escalables que han sido propuestas en herramientas para super-optimizar lenguajes de máquinas de pila. Estas técnicas pueden manejar diferentes criterios de optimización y pueden ser adaptadas para diferentes tipos de lenguajes basados en pila. Se ha desarrollado un modelo en MiniZinc para super-optimizar a dos lenguajes de estos: la Ethereum Virtual Machine (EVM) y WebAssembly (Wasm). Para ambos lenguajes se examinan diferentes objetivos de optimización que son relevantes en sus respectivos contextos. Además, se proponen diferentes mecanismos para mejorar la escalabilidad de este enfoque y evaluar su impacto en la propuesta inicial. Se ha evaluado nuestro modelo en un conjunto significativo de ejemplos y se ha podido demostrar que este modelo puede manejar, de forma efectiva, bloques de código de tamaño significativo y optimizarlos, hasta bloques de instrucciones que ya han sido optimizados.Super-optimization is a technique that seeks to find the optimal instruction sequence for a given one by exploring equivalent sequences. This technique is very effective in solving complex optimizations but implementing it is very demanding computationally speaking. This project seeks to explore scalable techniques that have been proposed to super-optimize stack-based bytecode languages. These techniques can manage different optimization criteria and can be modified for different types of stack-based bytecode languages. A model in MiniZinc has been developed to super-optimize two different stack-based bytecode languages: the Ethereum Virtual Machine (EVM) and WebAssembly (Wasm). For both languages different optimization criteria that are relevant in their respective contexts are examined. Furthermore, different mechanisms are proposed to improve the scalability of this approach and evaluate their impact on the initial proposal. The model has been evaluated over significant benchmark sets, and it has been possible to demonstrate that this model can effectively handle and optimize blocks of code of a significant size, even those which have been previously optimized.