Comment implémenteriez-vous le déréférencement des pointeurs dans z3?

Question

Essayer d'analyser certains programmes C avec z3 en python, et avoir des problèmes avec les pointeurs. Je travaille avec des termes tels que:

float * buffer = (float*)malloc(5*sizeof(float)) 

J'interprète tampon comme valeur BitVec(32) donc *buffer devrait être Real(). Cela devrait être ok, mais ce que les affirmations dois-je écrire pour les termes tels que

*(buffer+3) or *(buffer+i) 

Comment devraient être les affirmations écrites si je suis indexation sur comme

*(buffer-1) or *(buffer+10) 

Answer 1

Une solution consiste à encoder le tas de programme comme une carte H des emplacements aux valeurs. En Z3, la théorie des matrices peut être utilisée pour encoder des cartes. Les points/adresses sont des emplacements entiers, l'arithmétique entière code l'arithmétique du pointeur; cela permettrait des contraintes telles que H(buffer + i) > 0 dans votre encodage. Si vous deviez encoder une langue OO, vous pouvez utiliser la paire (récepteur, nom de champ) pour coder les adresses. Par exemple. H(r, f) > 0 correspondrait à r.f > 0. Notez que ce codage de carte prend naturellement en compte l'aliasing, par ex. si buffer1 == buffer2 et i == 3 puis H(buffer1 + i) == H(buffer + 3).

Voir l'étude Heaps and Data Structures: A Challenge for Automated Provers pour une comparaison intéressante des codages de tas basés sur la carte.

Les codages basés sur une carte sont généralement utilisés par des outils basés sur des conditions de vérification, tels que Frama-C, Dafny et Boogie. Les outils basés sur l'exécution symbolique, tels que Silicon (qui fait partie des Viper verification infrastructure) et VeriFast utilisent généralement un codage différent; voir, par exemple. Heap-Dependent expressions in separation logic.