Résumé technique : Raisonnement automatisé avec des types de données imbriqués

1. Énoncé du problème

La théorie des types de données de SMT-LIB fournit un encodage pratique pour les structures de données comme les listes et les arbres, essentiels pour la vérification de logiciels. Cependant, son expressivité est limitée par l'absence d'opérateurs de mise à jour et de capacités d'accès aléatoire. Pour remédier à cela, une combinaison naïve de types de données avec la théorie des tableaux est souvent tentée.

Le problème central identifié dans ce travail est qu'une telle combinaison naïve introduit des modèles non standard. Plus précisément, le principe d'acyclicité — qui dicte qu'une valeur de type de données ne peut pas se contenir elle-même — est contourné lorsque des tableaux sont impliqués. Une valeur de type de données peut apparaître comme un élément d'un tableau où ce même tableau est, à son tour, un champ de cette même valeur de type de données. Cela crée un cycle que la combinaison standard de théories (via Nelson-Oppen) ne parvient pas à détecter car le cycle est « scindé » entre les composantes de types de données et de tableaux. Ces modèles non standard sont indésirables car ils ne s'alignent pas sur les sémantiques intuitives des structures de données imbriquées destinées à la vérification.

2. Méthodologie

Les auteurs proposent une théorie des types de données imbriqués qui exclut explicitement ces modèles non standard. La méthodologie comprend deux composantes principales : une définition formelle de la théorie et une procédure de décision basée sur la réduction.

2.1. Définition formelle

La théorie est définie en restreignant la combinaison standard des types de données et des tableaux.

• Bien-fondé : Les auteurs introduisent une nouvelle définition des sorts bien fondés (Définition 10) qui tient compte de la présence de sorts de tableaux. Cela garantit que la structure récursive des types de données reste bien fondée, même lorsque des éléments de tableaux sont impliqués.
• Relation NDT : Pour exclure les modèles non standard, les auteurs définissent une relation $\mathcal{R}_{\mathcal{A}}$ sur les structures (Définition 16). Cette relation connecte les termes à leurs sous-termes, et les tableaux à leurs éléments. Une structure n'est considérée comme une structure NDT valide que si cette relation est bien fondée. Cela élimine efficacement les cycles où une valeur de type de données fait indirectement référence à elle-même par l'intermédiaire d'un tableau.

2.2. Procédure de décision

Le papier présente une procédure de décision qui réduit le problème de satisfaisabilité des types de données imbriqués à la combinaison (naïve) des types de données, des tableaux et des fonctions non interprétées (EUF). La procédure opère comme suit :

1. Traduction de la signature : Une nouvelle signature $\Sigma_{\varphi}$ est construite.

   • Les sorts de tableaux sont divisés en deux composantes : un sort de type de données ($\sigma^*$) utilisé pour la vérification des cycles et un sort de tableau ($\sigma'$) utilisé pour le raisonnement standard sur les tableaux.
   • Les constructeurs de types de données sont copiés pour opérer sur les nouveaux sorts.
   • Des constructeurs spéciaux sont introduits pour représenter les tableaux comme des tuples finis, capturant les éléments accédés par les indices présents dans la formule d'entrée.
   • Des fonctions non interprétées ($f_A, g_A$) sont ajoutées pour lier les représentations de sort de tableau ($\sigma'$) avec les représentations de sort de type de données ($\sigma^*$).

2. Traduction de la formule : La formule d'entrée $\varphi$ est traduite en $\text{trFormula}(\varphi)$.

   • Les littéraux standards (par exemple, $x = \text{select}(a, i)$) sont mappés vers leurs équivalents dans la nouvelle signature.
   • Lemmes : Crucialement, la traduction est augmentée d'un ensemble de lemmes ($L(\varphi)$) qui imposent la correspondance entre les opérations de tableau dans la formule originale et la représentation par tuple dans la nouvelle signature. Ces lemmes garantissent que les « cycles cachés » sont exposés dans la formule traduite.

3. Résolution : La formule résultante $\text{trFormula}(\varphi)$ est vérifiée pour sa satisfaisabilité en utilisant des solveurs SMT existants capables de gérer la combinaison des types de données, des tableaux et de l'EUF (par exemple, via la méthode de Nelson-Oppen).

2.3. Correctitude et décidabilité

Le papier prouve que la traduction préserve la satisfaisabilité (Théorème 31) sous l'hypothèse que la théorie des types de données est stablement infinie par rapport aux sorts partagés. Par conséquent, la théorie des types de données imbriqués est décidable (Théorème 32).

3. Contributions clés

Le papier apporte trois contributions principales :

1. Définition de la théorie : L'introduction d'une théorie précise des types de données imbriqués qui empêche les modèles cycliques non standard découlant de l'interaction entre les types de données et les tableaux.
2. Procédure de décision : Une procédure de décision basée sur la réduction qui transforme les problèmes de types de données imbriqués en combinaisons de théories standard augmentées de fonctions non interprétées.
3. Implémentation et évaluation : Une implémentation prototype au sein du solveur SMT cvc5 et une évaluation empirique démontrant l'efficacité de l'approche.

4. Résultats expérimentaux

Les auteurs ont évalué leur implémentation sur deux suites de benchmarks :

• Benchmarks synthétiques : Formules systématiquement conçues pour créer des cycles de tailles variables entre les types de données et les tableaux.
  • Sur les instances insatisfaisables (cycles présents), cvc5 a résolu l'ensemble des 500 benchmarks, surpassant Z3 (qui a résolu 299,8 en moyenne, bien que le tableau indique que Z3 a résolu moins d'instances au total).
  • Sur les instances satisfaisables (cycles brisés), cvc5 a résolu 25 sur 50, tandis que Z3 n'en a résolu qu'une seule.
• Benchmarks du monde réel : Formules dérivées de l'outil de vérification Move Prover, qui utilise des types de données imbriqués pour modéliser des structures de données persistantes dans les contrats intelligents.
  • Les deux solveurs ont résolu tous les benchmarks de Move Prover rapidement.
  • cvc5 était comparable ou légèrement plus rapide que Z3 sur les instances satisfaisables.

5. Signification et affirmations

Le papier affirme que la théorie et la procédure de décision proposées traitent avec succès le problème des modèles non standard dans la combinaison des types de données et des tableaux, un problème que les solveurs existants (comme Z3) peuvent traiter implicitement mais sans une définition théorique précise ou une garantie de correctitude concernant l'acyclicité.

Les auteurs déclarent que leur approche est « prometteuse », montrant qu'elle est compétitive avec les solutions existantes sur les benchmarks du monde réel et supérieure sur les benchmarks synthétiques conçus pour tester la détection de cycles. Ils soulignent que ce travail a été motivé par les besoins de Move Prover, où de telles structures imbriquées sont courantes.

Le papier conclut modestement, notant que bien que le présent travail résolve le cas spécifique des tableaux, le problème plus large des cycles non détectés existe pour d'autres structures de données (séquences, ensembles, etc.). Les auteurs suggèrent que leur solution pour les tableaux puisse servir de base à une solution plus générale aux problèmes de combinaison naïve de théories. Les travaux futurs identifient l'extension du support à la résolution incrémentale et aux quantificateurs.