Symetra: Visual Analytics for the Parameter Tuning Process of Symbolic Execution Engines

Título: Symetra: Análise Visual para o Processo de Ajuste de Parâmetros de Motores de Execução Simbólica

1. Problema e Motivação

Os motores de execução simbólica (como o KLEE) são ferramentas poderosas para a geração automática de casos de teste, visando maximizar a cobertura de ramos (branch coverage) em programas de software. No entanto, o uso eficaz desses motores enfrenta desafios críticos:

• Complexidade de Parâmetros: Motores modernos possuem dezenas de parâmetros ajustáveis (binários, contínuos e nominais) que interagem de forma não linear, criando um espaço de busca de alta dimensão.
• Dependência de Configurações Padrão: Devido à dificuldade de ajuste, os usuários frequentemente dependem de configurações padrão subótimas, que podem não ser ideais para programas específicos.
• Limitações dos Ajustadores Automáticos: Embora existam "tuners" automáticos (como o SymTuner), eles operam como "caixas pretas". Eles podem melhorar a cobertura, mas não fornecem insights sobre por que certas configurações funcionam, nem ajudam a identificar configurações complementares (que cobrem diferentes partes do código) ou a diagnosticar falhas que resultam em cobertura zero.
• Ineficiência na Análise Manual: Analisar milhares de configurações geradas manualmente (via planilhas ou logs) é impraticável e não escala para o volume de dados gerado por experimentos modernos.

O objetivo do trabalho é preencher essa lacuna através de uma abordagem Human-in-the-Loop (Humano no Loop), onde a análise visual auxilia os especialistas a entender, refinar e melhorar o processo de ajuste de parâmetros.

2. Metodologia: O Sistema Symetra

O Symetra é um sistema de análise visual projetado para apoiar a análise e o refinamento iterativo do espaço de parâmetros de motores de execução simbólica. O sistema não se limita a um algoritmo de ajuste específico, sendo agnóstico ao tuner utilizado.

Arquitetura e Visualização

O sistema consiste em seis visualizações coordenadas que permitem uma análise do geral para o detalhe:

1. Visão de Parâmetros (Parameter View):

   • Utiliza um modelo de substituição (XGBoost) para aproximar a relação entre parâmetros e cobertura.
   • Aplica valores SHAP (Shapley Additive exPlanations) para quantificar a contribuição de cada parâmetro e de seus valores específicos na cobertura de ramos.
   • Permite identificar quais parâmetros têm maior impacto e quais valores superam o padrão (default).

2. Visão de Cobertura (Coverage View):

   • Projeta os vetores de cobertura de ramos (vetores binários indicando quais ramos foram cobertos) em um espaço 2D usando UMAP com similaridade de Jaccard.
   • Permite identificar clusters de configurações que cobrem partes similares ou distintas do código, mesmo que tenham valores de cobertura totais semelhantes.
   • Suporta coloração baseada em parâmetros para analisar correlações.

3. Visão de Tentativas (Trial View):

   • Tabela detalhada de cada execução (trial), mostrando ID, cobertura e configuração de parâmetros.
   • Permite a seleção e agrupamento de tentativas.

4. Visão de Grupos de Tentativas (Trial Group View):

   • Resume grupos criados pelo usuário (ex: Top 10%, Falhas, Clusters).
   • Utiliza um heatmap para mostrar a complementaridade (ganho de cobertura ao unir grupos) e as diferenças estatísticas entre grupos.

5. Visão de Comparação (Comparison View):

   • Facilita a comparação lado a lado de dois grupos de tentativas.
   • Mostra estatísticas de cobertura, padrões de cobertura por ramo e distribuições de parâmetros, destacando diferenças estatisticamente significativas.

6. Visão de Código (Code View):

   • Mapeia as diferenças de cobertura diretamente no código-fonte.
   • Visualiza quais arquivos e linhas de código são cobertos preferencialmente por um grupo em relação a outro, permitindo a verificação de padrões de cobertura em nível de linha.

Fluxo de Trabalho (Human-in-the-Loop)

O processo iterativo envolve:

1. Execução automática de um tuner para gerar tentativas.
2. Análise visual dos resultados no Symetra para identificar parâmetros críticos, falhas e configurações complementares.
3. Refinamento do espaço de parâmetros (ex: remover valores que causam falhas, ajustar defaults, focar em parâmetros relevantes).
4. Reexecução do tuner com o novo espaço de parâmetros.

3. Contribuições Principais

1. Symetra: O primeiro sistema de análise visual projetado especificamente para o ajuste de parâmetros de motores de execução simbólica.
2. Abstração do Domínio: Caracterização detalhada do cenário de teste de software baseado em execução simbólica, destacando a necessidade de analisar vetores de cobertura e configurações complementares, diferentemente da otimização de hiperparâmetros em Machine Learning.
3. Avaliação Qualitativa e Quantitativa:
   • Estudos de caso com especialistas demonstrando a capacidade do sistema em revelar estratégias de busca complementares e diagnosticar falhas.
   • Uma demonstração quantitativa mostrando que o ajuste guiado por humanos supera abordagens totalmente automatizadas em eficiência e cobertura.

4. Resultados e Avaliação

Os autores realizaram estudos de caso com dois especialistas (P1 e P2) e entrevistas com dois outros, além de um experimento de otimização.

• Descoberta de Estratégias Complementares: No estudo de caso com o programa gcal, o sistema permitiu identificar que diferentes heurísticas de busca (ex: nurs:icnt vs. random-path) cobriam ramos distintos. A fusão dos casos de teste dessas configurações aumentou a cobertura acumulada significativamente (de ~3.350 para ~3.919 ramos).
• Diagnóstico de Falhas: Com o programa grep, o sistema ajudou a identificar que valores específicos de arquivos de semente (SF) e tipos de switch (ST) causavam falhas (cobertura zero). A exclusão desses valores eliminou 100% das falhas em iterações subsequentes.
• Otimização Quantitativa (Human-in-the-Loop):
  • Cenário: Ajuste do motor KLEE no programa gawk.
  • Linha de Base Automática: O tuner automático rodou por 27 horas, alcançando uma cobertura acumulada de 3.832 ramos, com 128 tentativas falhas.
  • Abordagem Symetra: Após três iterações de refinamento guiado pela análise visual (filtrando parâmetros ineficazes, removendo valores causadores de falhas e ajustando defaults), o sistema alcançou uma cobertura de 3.813 ramos em apenas 1 hora de execução, sem nenhuma falha.
  • Conclusão: A abordagem guiada por humanos alcançou resultados comparáveis à automação total em uma fração do tempo, permitindo que o tempo restante fosse usado para explorar mais ramos.

5. Significado e Impacto

O trabalho destaca que a automação pura em engenharia de software muitas vezes falha em fornecer transparência e adaptabilidade. O Symetra demonstra que:

• Transparência: A visualização permite que os engenheiros entendam o "porquê" das configurações, facilitando a transferência de conhecimento para novos programas ou versões.
• Eficiência: A capacidade de identificar rapidamente configurações complementares e eliminar parâmetros problemáticos acelera drasticamente o ciclo de teste.
• Mudança de Paradigma: O sistema desafia a confiança cega em configurações padrão, mostrando que ajustes específicos para cada programa podem melhorar significativamente a qualidade do teste.

O estudo também aponta limitações, como a complexidade inicial de aprendizado de múltiplas visualizações e a necessidade de integração mais profunda com o motor de execução para permitir a execução interativa em tempo real, sugerindo direções para trabalhos futuros.