Value Set Analysis#6
Conversation
… of memory variable addresses from one store to the other
…d to appear in the store: it's implied
…g + a good clean up
…l affects the memory being read
| match bf with | ||
| | Top -> false | ||
| | Bottom -> true | ||
| | Bit {ones = o; zeros = z} -> Int32.(not ((z lor o) = 0b11111111111111111111111111111111l)) |
There was a problem hiding this comment.
est-ce correct ? Si z = 0b11..11, o = 0b11..11, alors z lor o = 0b11..11, donc (not ((z lor o) = 0b11..11) est faux, et ce n'est pas considéré comme bottom.
There was a problem hiding this comment.
Oui c'est correct. En fait, dans ton exemple, si z=0b11111... et o=0b11111..., alors tous les bits sont indéterminés (peuvent être 0 ou 1), donc ça représente toutes les valeurs possibles. C'est donc Top, et non Bottom. C'est donc normal que is_bottom retourne faux. En fait, le calcul (not ((z lor o) = 0b11111111111111111111111111111111l)) retourne vrai ssi il y a un bit qui n'est ni 0 ni 1. Dans ce cas, le bitfield ne représente aucun entier valide et doit être considéré comme bottom.
| let one = Bit {zeros = (-2l); ones = 1l} | ||
|
|
||
| let zero = Bit {zeros = (-1l); ones = 0l} | ||
|
|
There was a problem hiding this comment.
c'est étrange de définir ça avec (-2l) ou (-1l), utiliser des 0b... serait plus lisible
There was a problem hiding this comment.
Je suis d'accord, je vais changer ça pour une notation hexadécimale
| [NegInfinity + Infinity]). *) | ||
| let plus (x : t) (y : t) : t = | ||
| match x, y with | ||
| | Infinity, NegInfinity | NegInfinity, Infinity -> failwith "Invalid_argument \"ExtendedInt.plus: Infinity + NegInfinity is undefined\"" |
There was a problem hiding this comment.
plutôt que failwith, tu veux probablement utiliser la fonction invalid_arg : string -> 'a ici qui fait exactement ça
There was a problem hiding this comment.
Merci pour la suggestion, je viens de changer ça
| | ValueSet x, Boolean {numeric_value = y; _} | Boolean {numeric_value = x; _}, ValueSet y -> ValueSet (RIC.join x y) | ||
| | ValueSet x, Bitfield y | Bitfield y, ValueSet x -> ValueSet (RIC.join x (RIC.of_bitfield y)) | ||
| | Boolean {numeric_value = x; _}, Bitfield y | ||
| | Bitfield y, Boolean {numeric_value = x; _} -> ValueSet (RIC.join x (RIC.of_bitfield y)) |
There was a problem hiding this comment.
c'est voulu que meet soit implémenté en terme de join ?
There was a problem hiding this comment.
Absolument pas. J'ai probablement fait un copier/coller le la fonction join pour garder la structure, et j'ai oublié de changer quelques join en meet. Je viens de corriger.
mais de toute façon, c'était dans les cas qui n'arrivent jamais en pratique.
| | Top, _ | _, Top -> Top | ||
| | Bottom, Bottom -> Bottom | ||
| | Bottom, _ -> ric2 | ||
| | _, Bottom -> ric1 |
There was a problem hiding this comment.
généralement bottom et absorbant. Il me semble que c'est nécessaire pour la soundness. Ici, bottom + x retourne x plutôt que bottom.
There was a problem hiding this comment.
En effet. Je viens de corriger. Je ne me souviens plus s'il y avait une raison pour que j'aie fait ça comme ça, mais en réalité, dans le reste de l'analyse, je considère que si je tombe sur un Bottom, alors je dois forcément être dans une branche qui est soit le retour d'une boucle pas encore initialisée, ou dans une branche inaccessible. Dans les deux cas, je n'ai certainement pas besoin que Bottom + x soit égal à x, donc je n'avais sans doute pas une raison valable pour implémenter ça ainsi.
| let i32_sub (x : t) (y : t) : t = | ||
| i32_add (negative x) y |
There was a problem hiding this comment.
i32_sub x y calcule ((- x) + y), ce qui n'est pas (x - y), c'est voulu ?
There was a problem hiding this comment.
c'est louche, en effet, je vais aller voir si j'avais un bon motif pour les inverser
There was a problem hiding this comment.
Je viens de vérifier, et il n'y avait pas d'erreur. Je crois que je l'avais mis dans cet ordre à cause de l'ordre des arguments sur la pile. Si la pile est x::y::_, alors on doit soustraire x à y (x étant au sommet de la pile), raison pour laquelle j'ai mis ça dans cet ordre. Je crois que ça semblait plus naturel comme ça à partir du site d'appel de la fonction. Mais j'avoue que lorsqu'on sort la fonction de son contexte, ça a l'air bizarre de mettre les paramètres dans cet ordre. Crois-tu qu'il serait préférable que j'inverse ça?
| [Top] is neutral; [Bottom] is absorbing. *) | ||
| let and_ (bf1 : t) (bf2 : t) : t = | ||
| match bf1, bf2 with | ||
| | Top, x | x, Top -> x |
There was a problem hiding this comment.
Il me semble que Top and_ x devrait être Top.
Par exemple, avec un bitfield de taille 1: Top signifie 0b0 ou 0b1. Top and_ 0b1 devrait retourner le join de 0b0 and_ 0b1 (= 0b0) et 0b1 and_ 0b1 (= 0b1), donc ça devrait retourner Top et pas le second argument tel quel,
There was a problem hiding this comment.
faisons un exemple sur 4 bits, avec des X pour signifier 0 ou 1.
par exemple, faisons le and de Top avec une autre valeur x
Top = XXXX
x = 1X01
----------
XX0X
Finalement, le résultat recherché est ni Top, ni x. Je vais aller corriger ça maintenant.
There was a problem hiding this comment.
Il en va de même pour le or :
Top = XXXX
x = 01X0
----------
X1XX
j'ai donc modifié les deux fonctions:
let and_ (bf1 : t) (bf2 : t) : t =
match bf1, bf2 with
| Bottom, _ | _, Bottom -> Bottom
| Top, Top -> Top
| Top, Bit {ones; _} | Bit {ones; _}, Top -> Bit {ones; zeros=0xFFFFFFFFl}
| Bit bf1, Bit bf2 ->
Bit {zeros = Int32.(bf1.zeros lor bf2.zeros); ones = Int32.(bf1.ones land bf2.ones)}
let or_ (bf1 : t) (bf2 : t) : t =
match bf1, bf2 with
|Bottom, _ | _, Bottom -> Bottom
| Top, Top -> Top
| Top, Bit {zeros; _} | Bit {zeros; _}, Top -> Bit {ones=0xFFFFFFFFl; zeros}
| Bit bf1, Bit bf2 ->
Bit {zeros = Int32.(bf1.zeros land bf2.zeros);
ones = Int32.(bf1.ones lor bf2.ones)}
2 participants
No description provided.