Quelqu'un peut-il expliquer ce qu'est une mise à jour forte et donner un exemple qui l'illustre ?

Question

Je lis le Forte mise à jour section d'un document sur Analyse efficace des pointeurs sensibles au contexte pour les programmes C et je ne parviens pas à en saisir le sens exact. Quelqu'un peut-il fournir un exemple, en particulier pour cette ligne dans le lien :

Cela améliore considérablement notre capacité à effectuer des mises à jour solides. Étant donné qu'un bloc de tas représente tout le stockage alloué dans un contexte particulier, nous supposons que les blocs de tas alloués localement ne sont jamais uniques.

Answer 1

Une mise à jour forte, une mise à jour faible

Dans le contexte de l'analyse statique, où l'on essaie de déduire tous les comportements possibles du programme en une seule fois, une forte mise à jour est une opération de mise à jour (affectation) dans laquelle l'adresse mise à jour est connue avec précision. En revanche, une affectation dans laquelle l'adresse écrite n'est pas connue avec précision est appelée un faible mise à jour .

Lors du traitement d'une mise à jour faible, non seulement la nouvelle valeur peut être écrite à plusieurs endroits sans que l'on sache lesquels, mais en outre, il faut envisager la possibilité que chaque endroit conserve son ancienne valeur (puisque la mise à jour peut avoir lieu ailleurs).

Exemple

Considérer Analyse de la valeur de Frama-C L'analyse de pointeurs contextuelle efficace pour les programmes C est disponible sous forme de paquetage dans la plupart des distributions Linux. Disons que nous analysons le programme suivant :

int a, b, c, d, *p, t[5];

int main(int argc, char **argv){
  a = 1; // strong
  p = &b;
  *p = 2; // strong
  if (c & 1) 
    p = &c;
  else
    p = &d;
  *p = 3; // weak

  t[2] = 4; // strong
  t[c & 2] = 5; // weak
}

En analysant cet exemple avec l'analyse de la valeur de Frama-C, on obtient :

$ frama-c -val t.c
[value] Values at end of function main:
  a ∈ {1}
  b ∈ {2}
  c ∈ {0; 3}
  d ∈ {0; 3}
  p ∈ {{ &c ; &d }}
  t[0] ∈ {0; 5}
   [1] ∈ {0}
   [2] ∈ {4; 5}
   [3..4] ∈ {0}
  __retres ∈ {0}

Les lieux c , d , t[0] y t[2] ont fait l'objet d'une mise à jour insuffisante. Chacun d'entre eux peut contenir soit une nouvelle valeur (qui aurait pu être écrite à cet endroit), soit une ancienne valeur (qui existait à ce moment-là et qui aurait pu rester).

Par opposition, a y b ont fait l'objet d'une forte mise à jour. On savait que l'affectation écrivait exactement dans chacune de ces variables, il n'est donc pas nécessaire d'envisager la possibilité qu'elles aient conservé leurs anciennes valeurs.

Dans le contexte de l'article

En ce qui concerne le paragraphe précis que vous citez :

L'essentiel est de reconnaître qu'un paramètre étendu représentant le valeur initiale d'un pointeur unique peut être un bloc unique même si ce a de nombreuses valeurs possibles dans le contexte de l'appel. Puisque le ne peut contenir qu'une seule de ces possibilités à tout moment, le paramètre étendu est un bloc unique dans le cadre de la procédure. procédure. Ce n'est que lorsque plus d'un emplacement pointe vers un paramètre étendu et que les valeurs réelles de ce paramètre ne constituent pas un seul et unique unique, nous devons marquer le paramètre comme n'étant pas unique. Cela a pour effet de Cela améliore grandement notre capacité à effectuer des mises à jour fortes.

Les chercheurs visent à utiliser la mise à jour forte le plus souvent possible, car elle est plus précise. Dans ce paragraphe, ils font remarquer que même si un pointeur p peut indiquer plusieurs emplacements possibles, si vous donnez un nom à "l'emplacement". p pointe vers", vous pouvez alors mettre fortement à jour cet emplacement. Je pense que c'est ce qu'ils veulent dire.

Cela permettrait, dans mon exemple de programme, de lire les données de *p à la fin du programme et de constater qu'il contient exactement 3 , bien que p pointe vers c qui peut contenir 0 o 3 ou à d qui peut contenir 0 o 3 . Les anciennes versions de l'analyse de la valeur de Frama-C déduisaient cette information avec une technique similaire à celle décrite (si j'ai bien compris), mais elle était trop coûteuse et a été supprimée.