Alguns dias atrás, a equipe de engenharia do Facebook se destacou - recebeu o
Prêmio de Papel POPL Mais Influente . Entre os especialistas em aprendizado de máquina, isso é muito honroso. O prêmio foi entregue pelo trabalho de
Análise de forma composicional por meios de bi-abdução , que revela as nuances do Projeto Infer. O projeto em si foi projetado para detectar e eliminar erros no código de um aplicativo móvel antes de sua implantação.
Erros no software para dispositivos móveis são muito caros para desenvolvedores e usuários. Quanto ao primeiro, a detecção de um problema em um aplicativo já existente em diretórios é um pesadelo para qualquer especialista. Obviamente, o software é testado, o trabalho dos programas é verificado de acordo com certos modelos. Porém, mais frequentemente, os desenvolvedores não podem prever tudo, e os erros no aplicativo são detectados após a implantação.
Lembramos que: para todos os leitores de "Habr" - um desconto de 10.000 rublos ao se inscrever em qualquer curso Skillbox usando o código promocional "Habr".
A Skillbox recomenda: O Curso Online do Python Data Analyst .
O Project Infer verifica o código dos aplicativos móveis e permite encontrar todos os tipos de problemas, cujos padrões são armazenados no banco de dados (e são atualizados o tempo todo). O projeto em si foi apresentado há três anos. Quase imediatamente após o anúncio, o Facebook abriu o código, após o qual passou a ser usado em empresas como Amazon Web Services, Spotify e Uber.
Como isso funciona?
O Project Infer usa um conjunto especializado de algoritmos para analisar a operação do código. Pode haver milhões de combinações no código fonte de qualquer aplicativo grande que possa levar a erros. Os procedimentos tradicionais de análise de código não podem ajudar a detectar tudo. O Infer do Facebook, autoaprendizado, está expandindo sua base, de modo que o projeto permite detectar muitos problemas no código.
De um modo geral, o processo do Facebook Infer pode ser dividido em duas etapas: coleta e análise de dados. O ciclo de vida também é dividido em duas partes: global e diferencial.
Na fase de coleta de dados, o Infer traduz o código-fonte em seu próprio idioma. A fase de análise é dedicada ao estudo dos menores detalhes da estrutura do código, o que pode levar ao aparecimento de um erro. Se o Infer encontrar uma combinação já conhecida de fatores identificados como um padrão de erro, a análise será interrompida para um método ou função específico, mas outros métodos e funções continuam sendo analisados. Aqui está um exemplo de Infer.
Do ponto de vista da execução, o Infer pode trabalhar em duas modalidades - Global e Diferencial, conforme mencionado acima. No primeiro caso, o Infer analisa todos os arquivos. Para um projeto que compila usando Gradle, o Infer é iniciado usando o comando
infer run -- gradle build
O processo diferencial é usado em sistemas de construção incrementais específicos para aplicativos móveis. Nesse caso, você deve primeiro iniciar a coleta de dados do Infer para obter todos os comandos de compilação e depois analisar apenas as alterações. Para fazer isso, use o seguinte conjunto de comandos:
gradle clean infer capture -- gradle build edit some/File.java # make some changes to some/File.java infer run --reactive -- gradle build
Os relatórios Infer podem ser visualizados usando o comando InferTraceBugs.
infer run -- gradle build inferTraceBugs
Fundação Project Infer
O Infer do Facebook é baseado em dois novos métodos matemáticos:
lógica de separação e
abdução dupla.
Uma característica fundamental da lógica de separação é a possibilidade de raciocínio local. Apareceu devido à presença nas declarações de conectivos espaciais entre as partes da pilha. Nesse caso, não há necessidade de considerar toda a quantidade de memória em cada estágio.
O elemento principal da lógica de separação é o operador * (e separadamente), que é chamado de conexão de divisão. A fórmula X↦Y ∗ Y↦X pode ser lida como “X aponta para Y e, separadamente, Y aponta para X”, que é muito semelhante à maneira como os ponteiros de memória funcionam.
No contexto do Infer Bi-abduction, ele pode ser visto como um método de inferência lógica que permite à plataforma detectar propriedades relacionadas ao comportamento de partes independentes do código do aplicativo. O sequestro duplo em conjunto exibe antiframes (partes ausentes do estado) e quadros (aquelas partes que não são afetadas pela operação). Matematicamente, o problema de abdução dupla é expresso usando a seguinte sintaxe: A ∗? Antiframe⊢B ∗? Quadro.
No Infer, do Facebook, o método possibilita derivar as especificações pré / pós do código limpo, desde que conheçamos as especificações dos primitivos em um nível básico de código.
A criação do FI foi possível graças à análise do trabalho de especialistas em aprendizado de máquina, realizado por muitos anos. No decorrer do trabalho no Infer, os seguintes artigos principais foram publicados para todo o campo:
Até agora, o Infer pode ser usado apenas para aplicativos móveis. Mas alguns de seus princípios se aplicam a aplicativos de uso geral. Talvez no futuro as possibilidades do Infer se tornem mais amplas e, com sua ajuda, os desenvolvedores possam analisar aplicativos de desktop ou servidor.
A Skillbox recomenda: