fix issue #645

[hra687261]

No description provided.

[bclement-ocp]

Given my current understanding of the bitv module, I am not sure that the fix is correct. I will post my reasoning below, can you share insight/explanations?

• uniforme_slice is given a list of bv expressions, each of which being a list representing a concatenation of "simple" bitvector expressions (of type simple_term). This function calls slicing_pattern with the sizes of the concatenated bvs; and slicing_pattern returns a list of sizes that "slices" each of the bv expressions in the original list, which seems to mean that the returned sizes are a subpartition of all the concatenations. For instance, if we have [ x[2] ; y[3] ] as one concatenation and [ a[1]; b[2]; c[2] ] as another, we match the bitvectors (I write left-to-right, it may have to be interpreted right-to-left, but that is not relevant here):

xxyyy
abbcc

and insert separators on each concatenation when we change bitvectors:

xx|yyy
a|bb|cc

and finally take the union of all positions that have a separator anywhere in the concatenation:

x|x|y|yy
a|b|b|cc

Up to this point I am fairly certain of my understanding. Now for the shaky part. uniform_slice then iterates over the bitvector concatenation and extracts "equations" and "substitutions" using the slice_composition that is given the original bitvector concatenation and the slicing pattern extracted above.

I am not what happens with the equations afterwards, but this leads me to the first question: the name uniform_slice and the way it is implemented seems to imply that we expect all the resulting concatenations to have the same sizes. I do not see where this is actually used in the code (uniform_slice is called by equations_slice which is still a mystery to me), but your fix breaks that invariant (it changes the shape of the pattern). Do you have any insight as to why that is correct?

Another think I do not understand about these functions is that they seem to be able to construct unrelated sub-components of the same vector, when dealing with A and C vectors (do you have any insight on this A/B/C classification by the way?). Let's say we have [ a[3]; a[3] ] as a vector, and the pattern is [1; 2; 2; 1 ]. Then we will split the first a[3] as [ a_1[1] ; a_2[2] ] and then just… forget about that substitution? Which means that we will later split a[3] as a_3[2]; a_4[1] (in fact we could split it as 1; 2 again) we forget the equalities involving a_1 @ a_2 and a_3 @ a_4. I think the same sort of thing occurs with C bitvectors (where we will only remember the last substitution and forget the others — I believe).

Looking at the functions that create variables, we never duplicate A bitvectors, and we only duplicate C bitvectors across different equalities, so maybe that is an invariant that was intended when the code was written; however, I am not sure what (if any) prevents A and C duplicates from appearing due to substitutions (e.g. if a B bitvector is substituted into a A or C bitvector — presumably at least one of them is possible with AC(X) since B is sorted between A and C — but maybe that is not actually possible?).

[bclement-ocp]

OK, I dug a little deeper in the code, and I can confirm that this fix is not correct, for a reason related to what I said above but I can't quite articulate yet.

With the fix, I get Fatal error: exception Invalid_argument("List.map2") for the following input:

logic x: bitv[10]

goal g: x^{8,8} @ x^{7,8} @ x^{1,4} = x^{7,7} @ x^{5,6} @ x^{5,8}

I have some heavily commented version of the code that explains how I got to that example and I will share, although I have some more digging to do. At least I can answer my own question regarding A/B/C variable classification above: the code generates a system of equations where the left-hand-side is pre-existing variables and the right-hand-side is a concatenation of fresh A/B/C variables. The A/B/C classification works as follow: on the right-hand-side, A variables appear at most once in the whole system. B variables appear in at most one equation, but can appear multiple times in that same equation. C variables appear at most once in each equation, but can appear in multiple equations.

And this also gives a hint as to the proper fix for the issue: we must take into consideration the "link" between multiple occurences of the B variables (and only the B variables) when computing the pattern.

[hra687261]

After reading your review and the documentation you wrote in #683, I agree that the suggested fix is totally incorrect.

From what I understand, a correct fix would be to rewrite slicing_pattern so that it produces correct patterns, and correct patterns would be ones in which (duplicated) B variables that are split, also split their duplicates.
So when there are two B variables b of the same size, and one of them is split into two smaller b variables b1 and b2, then if the duplicate of that variable "fits" into a pattern (if it is of size 2 and falls under a pattern of the same size), then that pattern should be split.

The idea would be then, when creating the pattern, instead of taking lists of lists of sizes of variables, we would have more info, for example if the variable is a B variable or not and maybe its Id for substitution (?). Then when we encounter a B variable that was substituted and that fits into a pattern, we split that pattern.

The annoying thing is that with this one, we will need to also be able identify the two new variables that are produced when splitting the original B variable, in case they get split in another iteration, and we end up having to substitute them too. So in a certain sens, it's as if we actually do the splittings here that we expect to have to do in the future, which seems like doing them twice but not necessarily.

Anyway, I'm not sure, I'll write this one, the code will probably be clearer than the explication, then we'll see if there's a smarter way to do it.

(funny how it seems that there is an implicit similarity or link to what was discussed in #680)

[bclement-ocp]

I have a different implementation for this, I will send it out shortly (it was one of the fixes mentioned in #683 )

[hra687261]

Alright, closing this one then.

[bclement-ocp]

What it does is to re-slice everything if the pattern changed, similar to what is done for the c-substitutions (see equations_slice). I don't know if that is the best way; I tried to do something similar to what you described above but it feels like we are doing the slicing twice, once when creating the pattern and then again to actually slice

[hra687261]

So in a certain sens, it's as if we actually do the splittings here that we expect to have to do in the future, which seems like doing them twice but not necessarily.

Yes that was my issue with it as well.

[bclement-ocp]

#686