Interpretação abstrata - Abstract interpretation

Na ciência da computação , a interpretação abstrata é uma teoria de aproximação sonora da semântica de programas de computador , baseada em funções monotônicas sobre conjuntos ordenados , especialmente reticulados . Pode ser visto como uma parcial a execução de um programa de computador que recebe informações sobre a sua semântica (por exemplo, controlo de fluxo , fluxo de dados ) sem a realização de todos os cálculos .

Sua principal aplicação concreta é a análise estática formal , a extração automática de informações sobre as possíveis execuções de programas de computador; tais análises têm dois usos principais:

A interpretação abstrata foi formalizada pelo casal de cientistas da computação francês Patrick Cousot e Radhia Cousot no final dos anos 1970.

Intuição

Esta seção ilustra a interpretação abstrata por meio de exemplos do mundo real, não computacionais.

Considere as pessoas em uma sala de conferências. Suponha um identificador exclusivo para cada pessoa na sala, como um número de previdência social nos Estados Unidos. Para provar que alguém não está presente, basta verificar se o número do seguro social não consta da lista. Como duas pessoas diferentes não podem ter o mesmo número, é possível provar ou contestar a presença de um participante simplesmente procurando seu número.

No entanto, é possível que apenas os nomes dos participantes tenham sido registrados. Se o nome de uma pessoa não for encontrado na lista, podemos concluir com segurança que essa pessoa não estava presente; mas se for, não podemos concluir definitivamente sem mais investigações, devido à possibilidade de homônimos (por exemplo, duas pessoas chamadas John Smith). Observe que essa informação imprecisa ainda será adequada para a maioria dos propósitos, porque homônimos são raros na prática. Porém, com todo o rigor, não podemos afirmar com certeza que alguém esteve presente na sala; tudo o que podemos dizer é que ele ou ela possivelmente esteve aqui. Se a pessoa que procuramos for um criminoso, emitiremos um alarme ; mas é claro que existe a possibilidade de emitir um alarme falso . Fenômenos semelhantes ocorrerão na análise de programas.

Se estivermos interessados ​​apenas em alguma informação específica, digamos, "havia uma pessoa de idade n na sala?", Manter uma lista de todos os nomes e datas de nascimento é desnecessário. Podemos, com segurança e sem perda de precisão, restringir-nos a manter uma lista das idades dos participantes. Se isso já é demais para suportar, podemos manter apenas a idade do mais novo, m e pessoa mais velha, M . Se a pergunta for sobre uma idade estritamente inferior a m ou estritamente superior a M , então podemos responder com segurança que nenhum participante estava presente. Do contrário, podemos apenas dizer que não sabemos.

No caso da computação, informações concretas e precisas em geral não são computáveis ​​em tempo e memória finitos (veja o teorema de Rice e o problema da parada ). A abstração é usada para permitir respostas generalizadas a perguntas (por exemplo, responder "talvez" a uma pergunta sim / não, significando "sim ou não", quando nós (um algoritmo de interpretação abstrata) não podemos computar a resposta precisa com certeza); isso simplifica os problemas, tornando-os passíveis de soluções automáticas. Um requisito crucial é adicionar imprecisão suficiente para tornar os problemas gerenciáveis, mantendo a precisão suficiente para responder às perguntas importantes (como "o programa pode travar?").

Interpretação abstrata de programas de computador

Dada uma linguagem de programação ou especificação, a interpretação abstrata consiste em dar várias semânticas ligadas por relações de abstração. Uma semântica é uma caracterização matemática de um possível comportamento do programa. A semântica mais precisa, que descreve muito de perto a execução real do programa, é chamada de semântica concreta . Por exemplo, a semântica concreta de uma linguagem de programação imperativa pode associar a cada programa o conjunto de traços de execução que ele pode produzir - um traço de execução sendo uma sequência de possíveis estados consecutivos da execução do programa; um estado normalmente consiste no valor do contador do programa e nos locais da memória (globais, pilha e heap). Mais semânticas abstratas são então derivadas; por exemplo, pode-se considerar apenas o conjunto de estados alcançáveis ​​nas execuções (o que equivale a considerar os últimos estados em traços finitos).

O objetivo da análise estática é derivar uma interpretação semântica computável em algum ponto. Por exemplo, pode-se escolher representar o estado de um programa manipulando variáveis ​​inteiras, esquecendo os valores reais das variáveis ​​e mantendo apenas seus sinais (+, - ou 0). Para algumas operações elementares, como a multiplicação , tal abstração não perde precisão: para obter o sinal de um produto, basta conhecer o sinal dos operandos. Para algumas outras operações, a abstração pode perder a precisão: por exemplo, é impossível saber o sinal de uma soma cujos operandos são respectivamente positivos e negativos.

Às vezes, uma perda de precisão é necessária para tornar a semântica decidível (consulte o teorema de Rice e o problema da parada ). Em geral, existe um compromisso a ser feito entre a precisão da análise e sua decidibilidade ( computabilidade ), ou tratabilidade ( custo computacional ).

Na prática, as abstrações definidas são adaptadas às propriedades do programa que se deseja analisar e ao conjunto de programas alvo. A primeira análise automatizada em grande escala de programas de computador com interpretação abstrata foi motivada pelo acidente que resultou na destruição do primeiro vôo do foguete Ariane 5 em 1996.

Formalização

Exemplo: abstração de conjuntos inteiros (vermelho) para conjuntos de sinais (verde)

Seja L um conjunto ordenado, denominado conjunto concreto e seja L ′ outro conjunto ordenado, denominado conjunto abstrato . Esses dois conjuntos estão relacionados entre si definindo funções totais que mapeiam elementos de um para o outro.

Uma função α é chamada de função de abstração se ela mapeia um elemento x no conjunto concreto L para um elemento α ( x ) no conjunto abstrato L ′. Isto é, elemento α ( x ) em G ', é a abstracção de X em L .

A γ função é chamada de função de concretização se ele mapeia um elemento x "no conjunto abstrato L 'a um elemento γ ( x ') no conjunto concreto L . Ou seja, o elemento γ ( x ′) em L é uma concretização de x ′ em L ′.

Sejam L 1 , L 2 , L1 e L2 conjuntos ordenados. A semântica concreta f é uma função monotônica de L 1 a L 2 . Uma função f ′ de L1 a L2 é considerada uma abstração válida de f se para todo x ′ em L1 , ( f ∘ γ) ( x ′) ≤ (γ ∘ f ′) ( x ′ )

A semântica do programa é geralmente descrita usando pontos fixos na presença de loops ou procedimentos recursivos. Vamos supor que G é uma estrutura completa e deixe f ser uma função monotônica de L em L . Então, qualquer x ′ tal que f ( x ′) ≤ x ′ é uma abstração do menor ponto fixo de f , que existe, de acordo com o teorema de Knaster-Tarski .

A dificuldade agora é obter esse x ′. Se L ′ é de altura finita, ou pelo menos verifica a condição da cadeia ascendente (todas as sequências ascendentes são finalmente estacionárias), então tal x ′ pode ser obtido como o limite estacionário da sequência ascendente xn definida pela indução da seguinte forma: x0 = ⊥ (o menor elemento de L ′) e xn +1 = f ′ ( xn ).

Em outros casos, ainda é possível obter um tal x 'através de um operador de alargamento ∇: para todos os x e y , xy deve ser maior ou igual do que ambos X e Y , e para qualquer sequência y ' n , a sequência definido por x0 = ⊥ e xn +1 = xnyn é basicamente estacionário. Podemos então tomar yn = f ′ ( xn ).

Em alguns casos, é possível definir captações utilizando ligações de Galois (a, y) onde α é de G para G 'e γ é de G ' a G . Isso supõe a existência das melhores abstrações, o que não é necessariamente o caso. Por exemplo, se abstrairmos conjuntos de pares ( x , y ) de números reais envolvendo poliedros convexos , não haverá abstração ótima para o disco definido por x 2 + y 2 ≤ 1.

Exemplos de domínios abstratos

Pode-se atribuir a cada variável x disponível em um determinado ponto do programa um intervalo [ L x , H x ]. Um estado atribuindo o valor v ( x ) à variável x será uma concretização desses intervalos se para todo x , v ( x ) estiver em [ L x , H x ]. A partir dos intervalos [ L x , H x ] e [ L y , H y ] para as variáveis x e y , pode-se facilmente obter intervalos para x + y ([ L x + L y , H x + H y ]) e para x - y ([ L x - H y , H x - L y ]); observe que essas são abstrações exatas , uma vez que o conjunto de resultados possíveis para, digamos, x + y , é precisamente o intervalo ([ L x + L y , H x + H y ]). Fórmulas mais complexas podem ser derivadas para multiplicação, divisão, etc., resultando na chamada aritmética de intervalo .

Vamos agora considerar o seguinte programa muito simples:

y = x;
z = x - y;
Combinação de aritmética de intervalo ( verde ) e congruência mod 2 em inteiros ( ciano ) como domínios abstratos para analisar um pedaço simples de código C ( vermelho : conjuntos concretos de valores possíveis em tempo de execução). Usando as informações de congruência ( 0 = par, 1 = ímpar), uma divisão zero pode ser excluída. (Uma vez que apenas uma variável está envolvida, os domínios relacionais vs. não relacionais não são um problema aqui.)
Um exemplo de poliedro convexo tridimensional que descreve os valores possíveis de 3 variáveis ​​em algum ponto do programa. Cada uma das variáveis ​​pode ser zero, mas todas as três não podem ser zero simultaneamente. A última propriedade não pode ser descrita no domínio da aritmética de intervalo.

Com tipos aritméticos razoáveis, o resultado para zdeve ser zero. Mas se fizermos aritmética de intervalo a partir dex em [0, 1], obtém-se zem [-1, +1]. Embora cada uma das operações tomadas individualmente tenha sido abstraída exatamente, sua composição não é.

O problema é evidente: não acompanhamos a relação de igualdade entre x e y; na verdade, esse domínio de intervalos não leva em consideração nenhum relacionamento entre as variáveis ​​e, portanto, é um domínio não relacional . Domínios não relacionais tendem a ser rápidos e simples de implementar, mas imprecisos.

Alguns exemplos de domínios abstratos numéricos relacionais são:

  • relações de congruência em inteiros
  • poliedros convexos (cf. imagem à esquerda) - com alguns altos custos computacionais
  • matrizes ligadas à diferença
  • "octógonos"
  • igualdades lineares

e combinações dos mesmos (como o produto reduzido, cf. imagem à direita).

Quando se escolhe um domínio abstrato, normalmente é necessário encontrar um equilíbrio entre manter relacionamentos de baixa granularidade e altos custos computacionais.

Veja também

Referências

links externos

Notas de aula