Aviso: para depositar documentos, por favor, inicia sesión e identifícate con tu cuenta de correo institucional de la UCM con el botón MI CUENTA UCM. No emplees la opción AUTENTICACIÓN CON CONTRASEÑA
 

Improving Circom compiler diagnostic messages through static analysis

Loading...
Thumbnail Image

Official URL

Full text at PDC

Publication date

2024

Editors

Journal Title

Journal ISSN

Volume Title

Publisher

Citations
Google Scholar

Citation

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.

Research Projects

Organizational Units

Journal Issue

Description

Trabajo de Fin de Master en Métodos Formales en Ingeniería Informática, Facultad de Informática UCM, Departamento de Sistemas Informáticos y Computación, Curso 2023/2024

Keywords