crab
1.0.0
O caranguejo é uma biblioteca C ++ para a construção de análises estáticas do programa com base na interpretação abstrata. O caranguejo fornece um rico conjunto de domínios abstratos, solucionadores de ponto de fixação baseados em Kleene, bem como análises diferentes, como fluxo de dados, interprocedural e atrasado. O design do caranguejo é bastante modular, de modo que é fácil plugar novos domínios e solucionadores abstratos ou criar novas análises.
Os domínios abstratos de caranguejo podem raciocinar sobre o conteúdo da memória, matrizes do tipo C e propriedades numéricas. O caranguejo usa implementações eficientes de domínios numéricos populares, como zonas e octagons e novos domínios, para raciocinar, por exemplo, sobre termos simbólicos (também conhecidos como funções não interpretadas). O caranguejo também implementa domínios não relacionais populares, como intervalo ou congruências usando mapas de ambiente eficientes, e permite a combinação de domínios arbitrários por meio de construções padrão de produtos reduzidos. O caranguejo também fornece domínios não convexos, como intervalos disjuntivos especializados chamados caixas com base em diagramas de decisão lineares e uma estratégia de particionamento de valor mais geral que eleva um domínio arbitrário para uma excesso de aproximações de sua conclusão de disjunção. Além desses domínios, todos desenvolvidos por autores de caranguejo, a biblioteca de caranguejos integra bibliotecas de domínio abstrato populares como avental, Elina e pplite.
O caranguejo fornece o solucionador de ponto de fixação intercalado de última geração que usa a fraca ordem topológica de Bourdoncle para selecionar o conjunto de pontos de ampliação. Para mitigar as perdas de precisão durante o alargamento, o caranguejo implementa algumas técnicas populares, como ampliação com limiares e ampliação de lookahead.
O caranguejo fornece duas implementações diferentes de análises interprocedurais: um de cima para baixo com análise interprocedural de memórias com suporte para chamadas recursivas e um híbrido de análise de baixo para cima + de cima para baixo. Por último, mas não menos importante, o caranguejo também implementa uma análise mais experimental que pode ser usada para calcular as pré -condições necessárias e/ou reduzir o número de alarmes falsos.
O caranguejo não analisa diretamente uma linguagem de programação convencional, mas, em vez disso, analisa sua própria representação intermediária baseada em CFG chamada Crabir. O Crabir é um código de três endereço e é fortemente digitado. Em Crabir, o fluxo de controle é definido por meio de instruções não determinísticas. Além das operações booleanas e aritméticas padrão, Crabir fornece declarações especiais e afirmam. O primeiro pode ser usado para refinar o fluxo de controle e o último fornece um mecanishm simples para verificar se há propriedades definidas pelo usuário. Apesar de seu design simples, Crabir é rico o suficiente para representar idiomas como o LLVM.
O caranguejo está ativamente em desenvolvimento. Se você encontrar um bug, abra um problema do GitHub. Pull Pedidos com novos recursos são muito bem -vindos. A documentação disponível pode ser encontrada em nosso wiki. Se você usar esta biblioteca, cite este artigo.
| Windows | Ubuntu | OS X. | Cobertura |
|---|---|---|---|
| TBD |  | TBD |
Uma versão (noturna) pré-construída de caranguejo que executa todos os testes pode ser obtida usando o Docker:
docker pull seahorn/crab:bionic
docker run -v ` pwd ` :/host -it seahorn/crab:bionicO caranguejo é escrito em C ++ e depende da biblioteca do Boost. Os principais requisitos são:
-DCRAB_USE_APRON=ON ou -DCRAB_USE_ELINA=ON )-DCRAB_USE_PPLITE=ON )No Linux, você pode instalar requisitos digitando os comandos:
sudo apt-get install libboost-all-dev libboost-program-options-dev
sudo apt-get install libgmp-dev
sudo apt-get install libmpfr-dev
sudo apt-get install libflint-dev
Para instalar caranguejo, digite:
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR ../
3. cmake --build . --target install
O diretório tests contém muitos exemplos de como criar programas escritos em Crabir e calcular invariantes usando diferentes análises e domínios abstratos. Para compilar esses testes, adicione a opção -DCRAB_ENABLE_TESTS=ON na linha 2.
E então, por exemplo, para executar test1 :
build/test-bin/test1
Os domínios de caixas/avental/elina/pplite requerem bibliotecas de terceiros. Para evitar o ônus dos usuários que não estão interessados nesses domínios, a instalação das bibliotecas é opcional.
Se você deseja usar o domínio das caixas, adicione -DCRAB_USE_LDD=ON opção.
Se você deseja usar os domínios da biblioteca de avental, adicione -DCRAB_USE_APRON=ON opção.
Se você deseja usar os domínios da biblioteca Elina, adicione -DCRAB_USE_ELINA=ON opção.
Se você deseja usar os domínios da biblioteca Pplite, adicione -DCRAB_USE_PPLITE=ON opção.
IMPORTANTE: Apron e Elina atualmente não são compatíveis, portanto você não pode ativar -DCRAB_USE_APRON=ON e -DCRAB_USE_ELINA=ON ao mesmo tempo.
Por exemplo, para instalar caranguejo com caixas e avental, digite:
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target ldd && cmake ..
4. cmake --build . --target apron && cmake ..
5. cmake --build . --target install
As linhas 3 e 4 baixam, compilam e instalam os domínios de caixas e aventais, respectivamente. Substitua apron na linha 4 por elina ou pplite , se você quiser usar Elina ou Pplite. Se você já compilou e instalou essas bibliotecas em sua máquina, pule os comandos na linha 3 e 4 e adicione as seguintes opções na linha 2.
-DAPRON_ROOT=$APRON_INSTALL_DIR-DELINA_ROOT=$ELINA_INSTALL_DIR-DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR-DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIRPara incluir caranguejo no seu aplicativo C ++, você precisa:
Inclua os arquivos de cabeçalho C ++ localizados no $INSTALL_DIR/crab/include
Ligue seu aplicativo às bibliotecas de caranguejo instaladas em $INSTALL_DIR/crab/lib .
Se você compilar com caixas/avental/elina/pplite, também precisará incluir $INSTALL_DIR/EXT/include e link com $INSTALL_DIR/EXT/lib onde EXT=apron|elina|ldd|pplite .
Se o seu projeto usar cmake , você só precisará adicionar CMakeLists.txt do seu projeto:
add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})
E então vincule seu executável com ${CRAB_LIBS}
Se o seu projeto make , leia esta amostra Makefile.
