Improving Circom compiler diagnostic messages through static analysis

Abstract

A static program analyzer reasons about the behavior of a program and analyzes its source code to find potential issues such as bugs, antipatterns, and other issues that can be diagnosed without executing the program. In the present work, we apply techniques from static program analysis to Circom, a programming language and a compiler for designing arithmetic circuits expressed as polynomial constraints and encoded as a set of equations called to rank-1 constraint system (R1CS). The analyzer we implement identifies patterns in the source code to recommend code snippets to the programmer to make their code more idiomatic. Moreover, it applies Path Analysis techniques to verify semantic rules that are enforced by the Circom compiler, and helps in detecting non-terminating loops in order to avoid wasting resources on a nonterminating program.

Las herramientas de análisis de código estático examinan el código fuente de un programa con el fin de detectar posibles problemas como errores de funcionamiento (bug), antipatrones, y demás inconvenientes que puedan diagnosticarse sin tener que ejecutar dicho programa. En el presente trabajo aplicaremos técnicas de análisis estático de programas a Circom, un lenguaje de programación y compilador para diseñar circuitos aritméticos que se expresan y codifican como un sistema de ecuaciones que se denomina "rank-1 constraint system (R1CS)". El analizador que desarrollaremos es capaz de encontrar patrones en el código fuente y sugerir fragmentos de código al programador con el fin de mejorar su código y hacerlo más idiomático. Asimismo, se aplican técnicas de grafo de control de flujo (CFG) para llevar a cabo un Path Analysis que verifica que se cumplan las reglas semánticas que impone el compilador de Circom, así como detectar bucles que no terminan con el propósito de aprovechar mejor los recursos de computación.