L’analyse statique de ressource s'intéresse aux méthodes permettant de déterminer la quantité de ressource (temps, mémoire, énergie, ...) nécessaire à exécution d'un programme, et les grandeurs caractéristiques dont cette quantité dépend. Dans ce domaine, le nerf de la guerre consiste à trouver des invariants/variants entre les différents états d'un programme à l'exécution: l'analyseur doit automatiquement comprendre les algorithmes codés dans le programme, sans intervention de son auteur.e.
Nous nous intéressons plus particulièrement aux analyses de ressources par le typage pour les langages fonctionnels. À cet effet, nous présentons AutoBill, une représentation intermédiaire par machine abstraite pour l'analyse de ressources par le typage des langages fonctionnel. Les ressources analysées peuvent être monotones (temps, énergie), ou non monotone (mémoire, argent). Nous compilons vers cette machine, entre autre, un langage fonctionnel à la OCaml, avec structures de données (ADT) et récursion (points fixes), muni de quelques extensions.
La sémantique opérationnelle Call-by-Push-Value d'AutoBill permet de mêler appel par nom et par valeur, pour encoder les sémantiques opérationnelles des langages fonctionnels. L'usage d'une machine abstraite permet, de plus, d'encoder les continuations des programmes comme des piles explicites. Cela permet aux techniques d'analyses des structures de données d'être ré-utilisées pour l'analyse des flots de contrôles.
Sur cette machine, un système de type linéaire dit polarisé permet d'expliciter les flots de ressources qui accompagnent l'entrée/sortie dans les calculs. Les types sont enrichis avec les paramètres entiers naturels, qui sont contrôlés durant le typage via l'introduction d'équations et de contraintes dans les définitions des types. Nous pouvons alors générer une contrainte du premier ordre sur les grandeurs caractéristiques du programmes: tailles, coûts, invariants combinatoires, etc. L'inférence de type engendre alors une contrainte sur ces quantités, qui lie les grandeurs caractéristiques des entrées du programme et l'usage maximal de ressources son exécution, et qui est transmise à un solveur SMT pour validation, ou à un optimisateur de problème linéaire pour instancier des bornes polynomiales.
Nous implémentons dans AutoBill la méthode "Automated Amortized Resource Analysis" (AARA), qui, pour chaque structure de donnée, énumère le nombre de sous-structures d'une certaine forme, permettant ainsi de borner le nombre d'itérations d'un calcul et d'obtenir des complexités au pire cas exprimées par des polynômes. Cette analyse est implémentée via un schéma de compilation spécifique du langage source vers la machine. Le moteur d'analyse est indépendant de ce langage source et de la méthode d'analyse de ressource décrite par le schéma de compilation.