Semántica Operacional Estructural para Máquinas de Grafo de Flujo de Control

Los compiladores utilizan representaciones de grafo de flujo de control (CFG) de programas de bajo nivel porque son adecuadas para el análisis y la optimización de programas. Sin embargo, formalizar el comportamiento y la metateoría de los programas CFG no es trivial: los programas CFG no se componen bien, su semántica depende de un estado auxiliar y, como consecuencia, no disfrutan de una teoría ecuacional simple que se pueda utilizar para razonar sobre la corrección de las transformaciones de programas. Las representaciones intermedias basadas en el cálculo lambda, en contraste, tienen semánticas operacionales y metateoría bien entendidas, incluyendo ricas teorías ecuacionales, lo que las hace accesibles a la verificación formal. Este artículo establece una equivalencia ajustada entre (una variante de) el cálculo de valor por empuje de Levy (CBPV) y una máquina de grafo de flujo de control cuyas instrucciones están en forma de asignación única estática (SSA). La correspondencia se hace precisa a través de una serie de máquinas abstractas que alinean las transiciones de la semántica operacional estructural del lenguaje CBPV con los pasos de cálculo de la forma SSA. La máquina objetivo, que se deriva del lenguaje CBPV, captura con precisión el modelo de ejecución de los grafos de flujo de control, incluyendo saltos directos, bloques de código recursivos mutuamente y llamadas a funciones con múltiples argumentos, y el subconjunto sin cierre es similar a las representaciones intermedias SSA que se encuentran en compiladores modernos como LLVM y GCC. Las definiciones de toda la semántica del lenguaje/maquinaria abstracta y los teoremas que las relacionan están completamente verificadas en Coq.