seahorn
v0.1.0 Release (SV-COMP'16)
O Seahorn é uma estrutura de análise automatizada para idiomas baseados em LLVM. Esta versão compila contra o LLVM 14.
Alguns dos recursos suportados são
O Seahorn é desenvolvido principalmente como uma estrutura para a realização de pesquisas em verificação automatizada. As estruturas fornecem muitos componentes que podem ser montados de várias maneiras. No entanto, não é uma ferramenta de análise estática "pronta para uso".
Muitas ferramentas e exemplos de análise são fornecidos com a estrutura. Estamos constantemente procurando novos aplicativos e fornecemos suporte a novos usuários. Para obter mais informações sobre o que está acontecendo, consulte o nosso blog (com pouca frequência).
Seahorn é distribuído sob uma licença BSD modificada. Consulte License.txt para obter detalhes.
O Seahorn fornece um script python chamado sea para interagir com os usuários. Dado um programa C anotado com afirmações, os usuários precisam digitar: sea pf file.c
O resultado do sea-pf é unsat se todas as afirmações se mantiverem, um sat se alguma das afirmações for violada.
A opção pf diz a Seahorn para traduzir file.c em LLVM Bitcode, gerar um conjunto de condições de verificação (VCS) e, finalmente, resolvê -los. O solucionador principal de back-end é o espaçador.
O comando pf fornece, entre outros, as seguintes opções:
--show-invars : Exiba invariantes calculados se a resposta foi unsat .
--cex=FILE : armazena um contra-exemplo no FILE se a resposta foi sat .
-g : compila com informações de depuração para contra -exemplos mais rastreáveis.
--step=large : codificação de grande etapa. Cada relação de transição corresponde a fragmentos livres de loop.
--step=small : codificação de pequenas etapas. Cada relação de transição corresponde a um bloco básico.
--track=reg : o modelo (número inteiro) somente os registros.
--track=ptr : registros e ponteiros do modelo (mas não conteúdo de memória)
--track=mem : modele ambos escalares, ponteiros e conteúdos de memória
--inline : Inlines o programa antes da verificação
--crab : injetar invariantes no spacer gerado pela ferramenta baseada em interpretação abstrata-interpretação do caranguejo. Leia aqui para obter detalhes sobre todas as opções de caranguejo (prefixo --crab ). Você pode ver quais invariantes são inferidos pelo caranguejo, digitando opção --log=crab .
--bmc : use o mecanismo BMC.
sea pf é um oleoduto que executa vários comandos. As partes individuais do oleoduto também podem ser executadas separadamente:
sea fe file.c -o file.bc : Seahorn Frontend traduz um programa C em um código de bits LLVM otimizado, incluindo a transformação de semantics mistos.
sea horn file.bc -o file.smt2 : Seahorn gera as condições de verificação do file.bc e os produz no formato SMT -LIB V2. Os usuários podem escolher entre diferentes estilos de codificação com vários níveis de precisão adicionando:
--step={small,large,fsmall,flarge} Onde small é a codificação de pequenas etapas, a codificação large é a larga de blocos, fsmall é uma pequena etapa que produz cláusulas de buzina plana (ou seja, gera um sistema de transição com apenas um predicado) e flarge : a alga da produção de lã produzindo a produção de chifres.
--track={reg,ptr,mem} onde apenas reg modela os escalares inteiros, os modelos ptr reg e o ponteiro endereços e os modelos mem ptr e o conteúdo da memória.
sea smt file.c -o file.smt2 : Gera CHC no formato SMT -LIB2. É um pseudônimo para sea fe seguido de sea horn . O comando sea pf é um pseudônimo para sea smt --prove .
sea clp file.c -o file.clp : Gera CHC no formato CLP.
sea lfe file.c -o file.ll : executa o front -end Legacy
Para ver todos os comandos, digite sea --help . Para ver as opções para cada comando individual cmd (por exemplo, horn ), tipo sea CMD --help (por exemplo, sea horn --help ).
Seahorn não usa caranguejo por padrão. Para ativar o caranguejo, adicione a opção --crab ao comando sea .
O intérprete abstrato é por padrão intra-procedimento e usa o domínio das zonas como domínio abstrato numérico. Essas opções padrão devem ser suficientes para usuários normais. Para os desenvolvedores, se você deseja usar outros domínios abstratos necessários:
cmake -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONsea com opção --crab-dom=DOM onde DOM pode estar:int para intervalosterm-int para intervalos com funções não interpretadasboxes : para intervalos disjuntivosoct para octógonospk para poliedros Para usar a análise --crab-inter do sea
Por padrão, o intérprete abstrato apenas argumenta sobre variáveis escalares (ou seja, registros LLVM). Execute sea com as opções --crab-track=mem --crab-singleton-aliases=true à razão sobre o conteúdo da memória.
O caranguejo é principalmente insensível ao caminho enquanto espaçador, nosso solucionador de clima, é sensível ao caminho. Embora as análises insensíveis ao caminho sejam mais eficientes, a sensibilidade ao caminho é normalmente necessária para provar a propriedade de interesse. Isso motiva nossa decisão de executar o primeiro caranguejo (se opção --crab ) e depois passar os invariantes gerados para o espaçador. Atualmente, existem duas maneiras de espaçador usar os invariantes gerados pelo caranguejo. A opção sea --horn-use-invs=VAL diz spacer como usar esses invariantes:
VAL for igual a bg , os invariantes são usados apenas para ajudar spacer a provar que um lema é indutivo.VAL é igual a always , o comportamento é semelhante ao bg , mas, além disso, os invariantes também são usados para ajudar spacer a bloquear um contra -exemplo. O valor padrão é bg . Obviamente, se o caranguejo puder provar que o programa é seguro, o espaçador não incorre em nenhum custo extra.
Presume -se que as propriedades sejam afirmações. Seahorn fornece um comando de asserção estática sassert , conforme ilustrado no exemplo a seguir
/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();
int main ( void ) {
int k = 1 ;
int i = 1 ;
int j = 0 ;
int n = nd ();
while ( i < n ) {
j = 0 ;
while ( j < i ) {
k += ( i - j );
j ++ ;
}
i ++ ;
}
sassert ( k >= n );
} Internamente, o Seahorn segue a Convenção SV-Comp de Codificação de Erros por uma chamada para a função de erro designada __VERIFIER_error() . Seahorn retorna unsat quando __VERIFIER_error() é inacessível e o programa é considerado seguro. Seahorn sat quando __VERIFIER_error() é acessível e o programa é inseguro. O método sassert() é definido em seahorn/seahorn.h .
Além de provar propriedades ou produzir contra -exmostras, às vezes é útil inspecionar o código em análise para ter uma idéia de sua complexidade. Para isso, o Seahorn fornece um comando sea inspect . Por exemplo, dado um programa C ex.c tipo:
sea inspect ex.c --sea-dsa=cs+t --mem-dot
A opção --sea-dsa=cs+t permite a nova análise Sea-DSA sensível ao contexto, descrita no FMCAD19. Este comando gera um arquivo FUN.mem.dot para cada função FUN no programa de entrada. Para visualizar o gráfico da função principal, use a interface Web Graphivz ou os seguintes comandos:
$ dot -Tpdf main.mem.dot -o main.mem.pdfMais detalhes sobre os gráficos de memória estão no Repositório Seadsa: aqui.
Use sea inspect --help para ver todas as opções. Atualmente, as opções disponíveis são:
sea inspect --profiler imprime o número de funções, blocos básicos, loops, etc.sea inspect --mem-callgraph-dot impressa para o formato dot O gráfico de chamadas construído por Seadsa.sea inspect --mem-callgraph-stats impressa para a saída padrão Algumas estatísticas sobre a construção de gráficos de chamada feita por Seadsa.sea inspect --mem-smc-stats imprime o número de acessos de memória que podem ser comprovados seguros pela Seadsa.A maneira mais fácil de começar com Seahorn é através de uma distribuição do Docker.
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly Comece com a exploração do que o comando sea pode fazer:
$ sea --help
$ sea pf --help A tag nightly é automaticamente atualizada diariamente e contém a versão mais recente de desenvolvimento. Mantemos todas as outras tags (que requerem atualização manual) com pouca frequência. Verifique as datas no DockerHub e registre um problema no GitHub se forem muito obsoletos.
Exemplos adicionais e opções de configuração estão no blog. O blog é atualizado com pouca frequência. Em particular, as opções mudam, os recursos são eliminados, coisas novas são adicionadas. Se você encontrar problemas no blog, informe -nos. Pelo menos, atualizaremos a postagem do blog para indicar que não se espera que funcione com a versão mais recente do código.
Você também pode instalar manualmente:
Seguindo as instruções no arquivo do docker Dockerfile: docker/seahorn-builder.Dockerfile .
Se isso não funcionar, execute:
$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *Os três primeiros comandos instalarão LLVM 14, o 4º instalará libpolly, que é indevidamente omitido do LLVM 14 (mas incluído nas versões subsequentes)
Em seguida, siga as instruções no arquivo do docker acima
As informações a partir deste ponto são apenas para desenvolvedores. Se você deseja contribuir com o Seahorn, construa suas próprias ferramentas com base nela ou apenas interessado em como funciona dentro, continue lendo.
Seahorn requer LLVM, Z3 e Boost. As versões exatas das bibliotecas continuam mudando, mas o CMake Craft é usado para verificar se a versão correta está disponível.
Para especificar uma versão específica de qualquer uma das dependências, use o <PackageName>_ROOT e/ou <PackageName>_DIR (consulte Find_package () para obter variáveis cmake.
Seahorn é dividido em vários componentes que vivem em diferentes repositórios (sob a organização Seahorn). O processo de construção verifica automaticamente tudo o que é necessário. Para obter instruções de construção atuais, verifique os scripts do CI.
Estas são as etapas genéricas. Não os use. Leia para uma maneira melhor:
cd seahorn ; mkdir build ; cd build (o diretório de compilação também pode estar fora do diretório de origem.)cmake -DCMAKE_INSTALL_PREFIX=run ../ (instalação é necessária! )cmake --build . --target extra && cmake .. (clones componentes que vivem em outros lugares)cmake --build . --target crab && cmake ..cmake --build . --target install (construa e instale tudo em run )cmake --build . --target test-all (Executar testes)NOTA : O alvo de instalação é necessário para que os testes funcionem!
Para uma experiência aprimorada de desenvolvimento:
clanglld LLDcompile_commands.json No Linux, sugerimos a seguinte configuração cmake :
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run
-DCMAKE_BUILD_TYPE=RelWithDebInfo
-DCMAKE_CXX_COMPILER="clang++-14"
-DCMAKE_C_COMPILER="clang-14"
-DSEA_ENABLE_LLD=ON
-DCMAKE_EXPORT_COMPILE_COMMANDS=1
../
-DZ3_ROOT=<Z3_ROOT>
-DLLVM_DIR=<LLMV_CMAKE_DIR>
-GNinja
$ (cd .. && ln -sf build/compile_commands.json .)
onde <Z3_ROOT é um diretório que contém distribuição binária z3 e LLMV_CMAKE_DIR é um diretório que contém LLVMConfig.cmake .
Outras opções legais para CMAKE_BUILD_TYPE são Debug e Coverage . Observe que o CMAKE_BUILD_TYPE deve ser compatível com o usado para compilar LLVM . Em particular, você precisará de uma construção Debug do LLVM para compilar SeaHorn no modo de depuração **. Certifique -se de ter muita paciência, espaço em disco e tempo se decidir seguir esse caminho.
Como alternativa, o projeto pode ser configurado usando predefinições de cmake. Para fazer isso, basta executar o seguinte comando:
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > Para configurar o cmake, onde <BUILD_TYPE> é um dos: Debug , RelWithDebInfo ou Coverage e <PRESET_NAME> é a predefinição que você gostaria de usar. As predefinições atualmente disponíveis são: jammy . Essas predefinições assumem que você instalou o Z3 em /opt/z3-4.8.9 e yices instalados em /opt/yices-2.6.1 .
Isso também permitirá que o projeto seja configurado e compilado no código VS usando a extensão do CMake Tools.
Se você deseja usar diferentes configurações de compilação ou se tiver Z3 ou YICes instalados em qualquer outro diretório, precisará criar seu próprio arquivo CMakeUserPresets.json com suas próprias predefinições.
Não inclua -DSEA_ENABLE_LLD=ON . O compilador padrão é CLANG, portanto, talvez você não precise defini -lo explicitamente.
O Seahorn fornece vários componentes que são clonados e instalados automaticamente através do alvo extra . Esses componentes podem ser usados por outros projetos fora do Seahorn.
Sea-dsa: git clone https://github.com/seahorn/sea-dsa.git
sea-dsa é uma nova análise de heap baseada em DSA. Ao contrário llvm-dsa , sea-dsa é sensível ao contexto e, portanto, uma partição de grão mais fino da pilha pode ser gerada na presença de chamadas de função.
Clam: git clone https://github.com/seahorn/crab-llvm.git
clam fornece invariantes indutivos usando técnicas abstratas de interpretação para o restante dos back -ends de Seahorn.
llvm-seahorn: git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn fornece versões personalizadas para verificação de passes InstCombine e IndVarSimplify LLVM, bem como um passe de LLVM para converter valores indefinidos em chamadas não determinísticas, entre outras coisas.
Seahorn não vem com sua própria versão de Clang e espera encontrá -la no diretório de compilação ( run/bin ) ou no caminho. Certifique -se de que a versão do Clang corresponda à versão do LLVM usada para compilar Seahorn (atualmente LLVM14). A maneira mais fácil de fornecer a versão correta do CLANG é baixá -la de LLVM.org, Unpatt em algum lugar e criar um link simbólico para clang e clang++ em run/bin .
$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++ onde <CLANG_ROOT> é o local em que Clang foi descompactado.
A infraestrutura de teste depende de vários pacotes Python. Estes têm suas próprias dependências. Se você não conseguir descobrir, use o Docker.
$ pip install lit OutputCheck networkx pygraphviz Podemos usar gcov e lcov para gerar informações de cobertura de teste para Seahorn. Para construir com a cobertura ativada, precisamos executar o Build sob um diretório diferente e definir CMAKE_BUILD_TYPE como Coverage durante a configuração do CMake.
Exemplo de etapas para gerar relatório de cobertura para o test-opsem Target:
mkdir coverage; cd coverage Criar e inserir diretório de construção de coberturacmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem OPSEM, agora os arquivos .gcda e .gcno devem ser criados nos diretórios CMakeFiles correspondenteslcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info coleta dados de cobertura do módulo desejado, se clang for usado como compilador em vez do gcc , crie um script de bash llvm-gcov.sh : #! /bin/bash
exec llvm-cov gcov " $@ " $ chmod +x llvm-gcov.sh Em seguida, anexa --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh ao comando lcov -c ... 6. Extraia dados dos diretórios desejados e geram relatório HTML:
lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report Em seguida, abre coverage_report/index.html no navegador para visualizar o relatório de cobertura
Consulte também scripts/coverage para scripts usados pelo CI. Relatório de cobertura para construções noturnas está disponível no Codecov
O banco de dados de compilação para o projeto Seahorn e todos os seus subprojetos é gerado usando -DCMAKE_EXPORT_COMPILE_COMMANDS=ON opção para cmake .
Uma maneira fácil de fazer com que a indexação de código funcione com o suporte ao banco de dados de compilação é vincular o arquivo compilation_database.json no diretório principal do projeto e seguir as instruções específicas para o seu editor.
lsp-ui com clangd que estão disponíveis no SpaceMacs Develop Branch Para um guia detalhado para um fluxo de trabalho remoto com a configuração de Clion Verifique Clion.
Use nosso garfo de mainframer. Não perca a configuração de exemplo.
