Slides preparados por Bruno Monteiro e Marcelo
d’Amorim
Execução simbólica - 24/09/2009

Gerar dados de testes de forma automática
◦ Explora todos os possíveis caminhos (módulo
limitações)

Concreto
◦ Exemplo: “Fui à escola hoje”, 3, new Integer(3)

Simbólico
◦ Exemplo: $a + 3, $s.indexOf(‘a’) != -1

Valor Simbólico representa um conjunto de
valores concretos
f(int x, int y)
Execução Simbólica
REQ1(x,y)
REQ2(x,y)
REQn(x,y)
f(int x, int y)
Execução Simbólica
REQ1(x,y)
REQ2(x,y)
REQn(x,y)
REQi denota um requisito de
entrada sobre x e y na forma
de uma expressão simbólica
f(2,3)
f(-1,-1)
REQ1(x,y)
f(int x,
int y)
REQ2(x,y)
Exec. Simb.
Constraint
Solver
REQn(x,y)
f(0,0)
Gera restrições
simbólicas
Resolve restrições.
Isto é, instancia
variáveis
simbólicas


Representa condições suficientes para
execução alcançar um ponto do programa
Forma:


Conjunção de restrições b1 Λ b2 Λ ... bn
Faz parte do estado de uma execução
simbólica
f(int x, int y){
if(x = y){
 Fork na execução
...
 PC1: $a = $b
}else{
... }
 PC2: $a != $b
}
f($a,$b) produz
PC1 = ($a = $b)
PC2 = $a != $b
f(int x, int y){
Nota:
Exemplo
ilustrativo.
if(x = y){
 Fork na execução
Considere
chamada de funções,
...
}else{ encadeamento
loops,
de
 PC1: $a = $b
... }
condicionais, e outros
}
 PC2: $a != $b
operadores relacionais e
booleanos.
f(int x, int y){
x = x + y
if(x = y){
 Fork na execução
...
 PC1: $a + $b = $b
}else{
...
 PC2: $a + $b != $b
}
}

Suporte para
◦
◦
◦
◦
◦
Métodos Nativos
Loop e recursão
Indexação de Arrays
Strings
Referências
fuzzing
Interpretação especial
de operadores

Referência
◦ S. Khurshid, C. Pasareanu and W. Visser.
Generalized Symbolic Execution for Model Checking
and Testing. TACAS 2003

Strings
◦ D. Shannon, S. Hajra, A. Lee, D. Zhan, and S.
Khurshid. Abstracting Symbolic Execution with
String Analysis. TAIC-PART 2007.
f(T t){
if(t == null){ Fork na execução
...
 PC1: $t == null
}
...
 PC2: $t != null
}



Só inicializa os objetos no momento em que
são usados
Derreferência (ou seja, “r.”) requer lazy
initialization
Três possibilidade para o valor de uma
referência: null, objeto novo, objeto existente
(alias)
foo(String s, String t){
s.equals(t)
}


Operadores da linguagem geram restrições.
 Por exemplo, equals, indexOf, substring, etc.
Duas opções de tratamento:
 s e t têm tamanho fixo n. Equivalente a:
 foo(int s1, ..., sn, t1, ..., tn)
 Não assumir tamanho das entradas

Valor simbólico de uma string $a é
caracterizado pelo autômato que reconhece a
linguagem com todas possíveis strings
concretas associadas a $a
Σ*
f(String s){
s.startWith(“ola ”)
}
o

Σ*
l

a


Soluções para strings
podem ser obtidas
com uma visita no
autômato
f(String s){
s.startWith(“ola ”)
if (s.endsWith(“ turma”) &&
s.length() > 9) {
}
...
}
Σ+
o

l

a



u

r

m

a

t
