Fundamentos de
Análise Estática
O que é?
• Análise automática feita em código sem
execução
Objetivo (Para que serve?)
• Verificação de propriedades
• Entendimento de código
Foco desta aula
Objetivo (Para que serve?)
• Verificação de propriedades
• Entendimento de código
Foco desta aula
Entendimento de código
pode facilitar verificação!
Várias formas (Como?)
• Sistemas de tipos
• Verificação de restrições
• Análise de dataflow
Foco desta aula
Conceitos Básicos
Aproximação de soluções
• Propriedades complexas
– Análise é indecidível ou alto custo
Aproximação de soluções
• Propriedades complexas
– Análise é indecidível ou alto custo
Maioria das propriedades
interessantes são complexas!
Aproximação de soluções
• Propriedades complexas
– Análise é indecidível ou alto custo
• Abordagem: aproximar espaço de solução
– super-aproximação: falso positivos
– sub-aproximação: falso negativos
comum
Aproximação de soluções
• Propriedades complexas
– Análise é indecidível ou alto custo
• Abordagem: aproximar espaço de solução
comum
– super-aproximação: falso positivos
sub-aproximação:
falsoquando
negativos
Uma–análise
é conservadora
resultado inclui
necessariamente
todas as soluções. Por exemplo,
• Prática:
uma–análise
para
encontrar
erros dee tipo
é
Balanço
entre
falso positivos
negativos
e
conservadora
quandopotencializa
não permite
escapar
escalabilidade
utilidade
danenhum
análise
erro. Por outro lado, geralmente, reporta erros
espúrios (i.e., alarmes falso).
Frequentemente balanço entre falso
positivos, negativos, e escalabilidade é
mais importante (i.e., útil) que garantias
fortes de correção (0% falso negativos) e
completude (0% falso positivos).
Um pouco de teoria...
Teoria dos Reticulados (Lattice)
• O que estes grafos tem em comum?
– Obs. vértice denota relação de ordem
Ordem Parcial
• Ordem parcial é uma relação binária:
– reflexiva, transitiva e anti-simétrica
• Conceitos associados
– Upper Bound
– Least Upper Bound (LUB)
– Lower Bound
– Greatest Lower Bound (GLB)
LUB
LUB para este
subconjunto?
LUB
LUB para este
subconjunto?
GLB
GLB para este
subconjunto?
GLB
GLB para este
subconjunto?
Top e Bottom
Top
Bottom
Lattice
• Reticulado
– Ordem parcial onde qualquer subconjunto de
elementos da relação possui LUB e GLB
associado
• Esta ordem parcial é um lattice?
Exemplos: Lattices
Exemplo: relação de inclusão
de inteiros {0,1,2,3}
Função monotônica e Ponto Fixo
• Função f: L → L
– Monotônica
• Não decresce. Conceitualmente, acumula
informação
Função monotônica e Ponto Fixo
• Função f: L → L
– Monotônica
• Não decresce. Conceitualmente, acumula
informação
• Ponto fixo fix(f), f(fix(f)) = fix(f)
• Teorema do ponto fixo (Tarski):
– Toda função monotônica f admite ponto fixo
em um reticulado L de altura finita.
Ilustração
• Iterações sucessivas de
uma função
– Acumula informação
(f é monotônica)
– Para em ponto fixo quando
“não há mais informação
para se descobrir”
Relação com nosso problema
O domínio e contra-domínio de f representam
alguma informação de nosso interesse no
programa. Por exemplo, definições alcançáveis
em um ponto do programa. Tipicamente, f opera
em uma representação abstrata do programa.
Por exemplo, o control-flow graph (CFG) ou o
inter. flow graph (IFG). Uma iteração de f
propaga informação nesta estrututura. Por
exemplo, propaga informação armazenada nos
nós pelos vértices de um CFG.
Um pouco de prática...
Perspectiva
• Análise estática propaga informação
usando estrutura do programa
– Intra-procedural: fluxo de controle de um
método/função (CFG)
– Inter-procedural: fluxo de chamadas entre
métodos/funções (IFG)
Perspectiva
• Análise estática propaga informação
usando estrutura do programa
– Intra-procedural: fluxo de controle de um
método/função (CFG)
– Inter-procedural: fluxo de chamadas entre
métodos/funções (IFG)
CFG
Quiz
• Quais as definições de f
alcançáveis no nó return
f? (assuma que uma def.
consiste de um nome de
variável + id. do bloco
básico)
Como mecanizar análise
mental?
• Associado a cada nó i:
– Informação acumulada: xi
• No exemplo anterior xi armazena conjunto de
definições
– Função (monotônica) de transferência: Fi
Chaotic Iteration
Simplificação: na prática,
Fi lê apenas conteúdo em
nós vizinhos a i!
Framework
• Em geral, 4 funções descrevem uma
análise intra-procedural: in, out, kill e gen
• Ilustração
in
out
gen
kill
Exemplo: Reachable Definitions
•
•
•
•
in[b] = U OUT[k], for all k ∈ pred[b]
out[b] = (IN[b] – kill[b]) + gen[b]
kill[b] = “definições mortas em b”
gen[b] = “novas definições (não mortas) em b”
Existem vários frameworks de análise que
permitem escrever basicamente estas 4
funções e obter sua análise intra-proc. E.g.,
SOOT (http://www.sable.mcgill.ca/soot)
Outros Detalhes
• Generalização
– May/Must
– Forward/Backward
• Reachable Defintions é uma análise
– May e Forward
Perspectiva
• Análise estática propaga informação
usando estrutura do programa
– Intra-procedural: fluxo de controle de um
método/função (CFG)
– Inter-procedural: fluxo de chamadas entre
métodos/funções (IFG)
Similaridades entre Inter e Intra
• Informação se propaga em um grafo
– Informação e função de transferência
associada a cada nó
Grafo inclui informação de
chamador e chamado
Diferenças
• Representação do grafo é diferente
• Context insensitivity: alguns caminhos
(de chamadas) são explorados, mas não
são possíveis!
f() calls g()
Caixinha é
um CFG
returns from g() back to f()
h() calls g()
g()
returns from g() back to h()
Diferenças
• Representação do grafo é diferente
• Context insensitivity: alguns caminhos
(de chamadas) são explorados, mas não
propagada
informação
são possíveis!
acumulada no contexto
f() calls g()
de chamada de h() para
o retorno da chamada
de g() em f()!
h() calls g()
g()
returns from g() back to f()
returns from g() back to h()
Inlining
• Uma tentativa é representar um CFG do
programa fazendo inlining de função
• Problemas
– Como tratar recursão?
– Não escala (vários contextos de chamada)
Existe uma variedade de representações de
interprocedural flow graphs (IFGs). Por
exemplo, IFG proposto por Harrold e Soffa
em “Efficient Computation of Interprocedural
Definition-Use Chains”, TOPLAS 1994.
Considerações Finais
• Representação do programa pode facilitar
muito a análise do programa
– 3-address
– SSA
O framework SOOT oferece 4
representações (formatos) do
programa de entrada.
Leitura adicional
• Michael Shwartzbach’s Lecture Notes on
Static Analysis:
http://www.brics.dk/~mis/static.pdf