charon

Patinir, E., 1515-1524, paisagem com charon cruzando o styx [óleo sobre madeira]. Museo del Prado, Madri. Fonte

Charon

Charon atua como uma interface entre o compilador RustC e os projetos de verificação de programas. Seu objetivo é processar caixas de ferrugem e convertê -las em arquivos fáceis de manusear por verificadores de programas. Ele é implementado como um driver personalizado para o compilador RustC.

Charon está, na mitologia grega, um velho que carrega as almas do falecido acumula o Styx, um rio que separa o mundo dos vivos do mundo dos mortos. No presente contexto, Charon nos permite ir do mundo dos programas de ferrugem ao mundo da verificação formal.

Estamos abertos a contribuições ! Entre em contato conosco para que possamos nos coordenar, se você estiver disposto a contribuir. Para esse fim, você pode ingressar no Zulip.

Llbc

Charon converte o código MIR em ULLBC (cálculo de empréstimo de nível de baixo nível não estruturado) e depois em LLBC. Ambos os ASTs podem ser emitidos por Charon.

O ULLBC é um mir ligeiramente simplificado, onde tentamos remover o máximo de redundâncias possível. Por exemplo, simplificamos drasticamente a representação de constantes provenientes do compilador de ferrugem.

O LLBC é Ullbc, onde reestruturamos o fluxo de controle com loops, if ... then ... else ... etc. em vez de gotase. Consequentemente, mesclamos declarações e terminadores MIR em um único tipo de instrução LLBC. Também realizamos algumas modificações adicionais, algumas das quais estão listadas abaixo:

Observação : A maioria das transformações que transformam o MIR em UllBC e o LLBC é implementado por meio de micro-passagens. Dependendo da necessidade, poderíamos torná -los opcionais e controlá -los com sinalizadores. Se você quiser saber mais sobre os detalhes, consulte translate no src/driver.rs , que aplica as micro-passagens uma após a outra.

Observação : se você quiser saber os detalhes completos de (u) llbc, dê uma olhada: types.rs , values.rs , expressions.rs , ullbc_ast.rs e llbc_ast.rs .

O AST extraído é serializado nos arquivos .ullbc e .llbc (usando o formato JSON). Extraímos uma caixa inteira em um arquivo.

Estrutura do projeto

• charon : A implementação da ferrugem.
• charon-ml : A biblioteca ML. Fornece utilitários para recuperar e manipular o AST no OCAML (deserialização, impressão etc.).
• tests e tests-polonius : Test Arquivos Diretórios. tests-polonius contém código que requer o verificador de empréstimo de Polonius.

Instalação e construção

Você primeiro precisa instalar rustup .

Como Charon é configurado com carga, o Rustup baixará e instalará automaticamente os pacotes adequados ao criar o projeto. Se você deseja construir apenas o projeto de ferrugem (em ./charon ), basta executar make build-charon-rust no diretório superior.

Se você também deseja criar a biblioteca ML (em ./charon-ml ), precisará instalar o OCAML e as dependências adequadas.

Sugerimos que você siga essas instruções e instale Opam a caminho (mesmas instruções).

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

As dependências podem ser instaladas com o seguinte comando:

 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind

Em seguida, você pode executar make build-charon-ml para construir a biblioteca ML, ou mesmo simplesmente make para construir todo o projeto (Rust e OCAML). Finalmente, você pode executar os testes com make test .

Como alternativa, você pode usar o nix e nix develop (ou usar https://direnv.net/ e direnv allow ) e todas as dependências devem ser disponibilizadas.

Documentação

Você pode acessar a documentação da ferrugem online.

Você também pode executar make para gerar a documentação localmente. Ele gerará uma documentação acessível a partir de doc-rust.html (para o projeto de ferrugem) e doc-ml.html (para a biblioteca ML).

Uso

Para administrar Charon, você deve executar o binário charon de dentro da caixa que deseja compilar, como se quisesse construir a caixa com cargo build . O executável Charon está localizado em bin/charon .

Charon construirá a caixa e suas dependências e, em seguida, extrairá o AST. Charon fornece várias opções e sinalizadores para ajustar seu comportamento: você pode exibir uma documentação detalhada com --help . Em particular, você pode imprimir o LLBC gerado por Charon com --print-llbc .

Se houver um arquivo Charon.toml na raiz do seu projeto, Charon também receberá opções dele. O arquivo suporta as mesmas opções na interface da CLI, exceto as opções relacionadas à entrada/saída como --print-llbc . Exemplo Charon.toml :

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

Observação : Como Charon é compilado com a ferrugem por nigthly (este é um requisito para implementar um motorista RustC), ele construirá sua caixa com ferrugem todas as noites. Você pode encontrar a versão noturna presa para Charon em rust-toolchain.template .