lart

Lart: ferramenta de abstração e refinamento LLVM

Lart = ferramenta de abstração e refinamento LLVM. O objetivo desta ferramenta é fornecer transformações de LLVM para LLVM que implementam várias abstrações do programa. Em termos do conjunto de instruções, os programas resultantes são normais, concreto LLVM que podem ser executados e analisados. Informações extras sobre a (s) abstração (s) em vigor sobre um programa (fragmento) são inseridas usando funções intrínsecas especiais de LLVM e nós de metadados LLVM. O LART fornece uma ferramenta independente que processa arquivos de código de bits no disco, bem como uma estrutura que pode ser integrada às ferramentas complexas baseadas em LLVM. A principal motivação por trás do LART é fornecer um "pré-processador" para verificadores de modelos baseados em LLVM e outras ferramentas de análise, simplificando seu trabalho, reduzindo o tamanho do problema sem comprometer a solidez das análises. As abstrações implementadas pelo LART geralmente podem ser refinadas com base em instruções específicas sobre qual "parte" da abstração é muito difícil (uma abstração muito difícil criará erros espúrios visíveis para análises subsequentes, mas não estão presentes no programa original).

Abstrações para LLVM Bitcode

O objetivo de todo o exercício é abstrair as informações do LLVM Bitcode, tornando as análises subsequentes mais eficientes (às custas de alguma precisão). Para esse fim, precisamos ser capazes de codificar a escolha não determinística em programas LLVM, que podem ser feitos simplesmente por meio de uma função de uso especial (semelhante ao LLVM Intrinsics). A função é nomeada @lart.choice , pega um par de limites como argumentos e retorna não deterministicamente um valor que cai entre esses limites.

Essa extensão para a semântica de LLVM precisa ser reconhecida pela ferramenta a jusante. Este também é o único desvio crucial do Standard LLVM Bitcode. Muitas ferramentas de análise já implementarão um mecanismo semelhante, internamente ou mesmo com uma interface externa. As ferramentas de adaptação sem suporte para @lart.choice trabalharem com o LART geralmente são muito simples.

Existem outras funções de uso especial fornecidas por Lart, a saber, a família @lart.meta.* @llvm.dbg.* Espera -se que as transformações do programa mantenham essas chamadas, caso o Lart seja chamado para refinar uma abstração (cada abstração fornecida pelo LART vem com um procedimento de refinamento correspondente, que geralmente precisará encontrar as chamadas @lart.meta inseridas pela abstração).

Enquanto a maioria dos mecanismos de abstração tradicionais funcionam como intérpretes, as abstrações também podem ser "compiladas" em programas. Em vez de (re) interpretar instruções simbolicamente, as instruções simbólicas podem ser compiladas. Em caso de abstração predicada, o código de bits resultante manipulará e usará avaliações predicadas em vez de variáveis ​​de concreto. Como explicado acima, a diferença importante é que o código de bits precisa fazer escolhas não determinísticas, pois alguns predicados podem ter avaliações indeterminadas (são verdadeiras e falsas). Algumas variáveis ​​podem ser abstraídas completamente, e todos os testes nessas variáveis ​​produzirão respostas sim e não.

Construir

Use ou repita a configuração de ./devcontainer/Dockerfile por enquanto.

Em seguida, use:

 ./scripts/build.sh

Executar compilador

 ./build/bin/lartcc <domain> <compiler arguments> in.c

OPTAR

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

Teste

 lit -v build/test

Nota: build/lartcc/lartcc deve ter permissão exacutabple.