charon

Patinir, E., 1515-1524, paisaje con Charon cruzando el styx [aceite en madera]. Museo del Prado, Madrid. Fuente

Charón

Charon actúa como una interfaz entre el compilador RustC y los proyectos de verificación de programas. Su propósito es procesar las cajas de óxido y convertirlas en archivos fáciles de manejar por los verificadores de programas. Se implementa como un controlador personalizado para el compilador RustC.

Charon es, en la mitología griega, un anciano que lleva las almas del difunto Across the Styx, un río que separa el mundo de los vivos de los mundos de los muertos. En el contexto actual, Charon nos permite pasar del mundo de los programas de óxido al mundo de la verificación formal.

¡Estamos abiertos a contribuciones ! Comuníquese con nosotros para que podamos coordinarnos si está dispuesto a contribuir. Para este propósito, puede unirse al zulip.

LLBC

Charon convierte el código MIR en ULLBC (cálculo de préstamo de bajo nivel no estructurado) y luego a LLBC. Ambos AST pueden ser emitidos por Charon.

ULLBC es un MIR ligeramente simplificado, donde tratamos de eliminar la mayor cantidad de despidos posible. Por ejemplo, simplificamos drásticamente la representación de constantes provenientes del compilador de óxido.

LLBC es ULLBC donde reestructuramos el flujo de control con bucles, if ... then ... else ... , etc. en lugar de gotos. En consecuencia, fusionamos las declaraciones y terminadores de MIR en un solo tipo de instrucción LLBC. También realizamos algunas modificaciones adicionales, algunas de las cuales se enumeran a continuación:

Observación : La mayoría de las transformaciones que transforman el MIR a UllBC y luego LLBC se implementan mediante micro-pases. Dependiendo de la necesidad, podríamos hacerlos opcionales y controlarlos con banderas. Si desea saber más sobre los detalles, consulte translate en src/driver.rs , que aplica los micro-pases uno tras otro.

Observación : Si desea conocer los detalles completos de (U) LLBC, eche un vistazo a: types.rs , values.rs , expressions.rs , ullbc_ast.rs y llbc_ast.rs .

El AST extraído se serializa en archivos .ullbc y .llbc (usando el formato JSON). Extraemos una caja entera en un archivo.

Estructura de proyectos

• charon : La implementación de Rust.
• charon-ml : la biblioteca ML. Proporciona utilidades para recuperar y manipular el AST en OCAML (deserialización, impresión, etc.).
• tests y tests-polonius : prueba directorios de archivos. tests-polonius contiene código que requiere el verificador de préstamo de Polonio.

Instalación y construcción

Primero necesitas instalar rustup .

Como Charon está configurado con carga, Rustup descargará automáticamente e instalará los paquetes adecuados al construir el proyecto. Si solo desea construir el Proyecto Rust (en ./charon ), simplemente ejecute make build-charon-rust en el directorio superior.

Si también desea construir la biblioteca ML (in ./charon-ml ), deberá instalar OCAML y las dependencias adecuadas.

Le sugerimos que siga esas instrucciones e instale OPAM en el camino (mismas instrucciones).

Para Charon-ML, utilizamos OCAML 4.13.1 : opam switch create 4.13.1+options

Las dependencias se pueden instalar con el siguiente comando:

 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind

Luego puede ejecutar make build-charon-ml para construir la biblioteca ML, o incluso simplemente make para construir todo el proyecto (Rust y Ocaml). Finalmente, puede ejecutar las pruebas con make test .

Alternativamente, puede usar NIX y hacer nix develop (o usar https://direnv.net/ y direnv allow ) y todas las dependencias deben estar disponibles.

Documentación

Puede acceder a la documentación de Rust en línea.

También puede ejecutar make para generar la documentación localmente. Generará una documentación accesible desde doc-rust.html (para el Proyecto Rust) y doc-ml.html (para la biblioteca ML).

Uso

Para ejecutar Charon, debe ejecutar el binario de Charon desde la caja que desea compilar, como si quisiera construir la caja con cargo build . El ejecutable de Charon se encuentra en bin/charon .

Charon construirá la caja y sus dependencias, luego extraerá el AST. Charon proporciona varias opciones y banderas para ajustar su comportamiento: puede mostrar una documentación detallada con --help . En particular, puede imprimir el LLBC generado por Charon con --print-llbc .

Si hay un archivo Charon.toml en la raíz de su proyecto, Charon también tomará opciones de él. El archivo admite las mismas opciones en la interfaz CLI, excepto por las opciones que se relacionan con la entrada/salida como --print-llbc . Ejemplo Charon.toml :

[ charon ]
extract_opaque_bodies = true
[ rustc ]
flags = [ " --cfg " , " abc " ]

Observación : Debido a que Charon se compila con Rust Nigthly (este es un requisito para implementar un controlador Rustc), construirá su caja con Rust noches. Puede encontrar la versión nocturna fijada para Charon en rust-toolchain.template .