le 19 janvier 2019
Clément Ballabriga, Julien Forget, Giuseppe Lipari reçoivent le Prix du meilleur article à la conférence VMCAI'19 “Analyse statique d’un code binaire avec des indirections de mémoire à l’aide de polyèdres” Dans cet article, nous proposons un nouveau domaine abstrait pour l’analyse statique du code binaire. Note motivation découle de la nécessité d’améliorer la précision de l’estimation du temps d’exécution dans le pire des cas (WCET) d’un code temps réel critique pour la sécurité. L’estimation du WCET nécessite la calcul d’informations telles que les limites supérieures du nombre d’itérations de la boucle, les chemins d’exécutions irréalisables, etc. Ces estimations sont généralement effectuées sur du code binaire, principalement pour éviter de faire des hypothèses sur le fonctionnement du compilateur. Notre domaine abstrait, basé sur les polyèdres aux registres et sur deux fonctions de mapping qui associent les variables des polyèdres aux registres et à la mémoire, vise le calcul précis de telles informations. Nous prouvons la justesse de la méthode et démontrons son efficacité sur des benchmarks et des exemples de codes embarqués typiques.
En savoir plus...
français
English