Different widening results across instantiations

[culechetoo]

I am working with a fairly large codebase and for some reason need to compare the outputs across the two different versions.

This code at some point computes the widening of 2 values in the Octagon domain. The input to the widening function is “sort of” the same in both versions of the code. However, I am getting a different output across the versions. Here are the values, and the outputs across the 2 versions:

v1: [|cur_v>=0; -cur_v>=0; -cur_v-n>=0; cur_v-n>=0; -n>=0; -n+prefn>=0; -cur_v-prefn>=0; cur_v-prefn>=0; -n-prefn>=0; n-prefn>=0; -prefn>=0|]
v2: [|cur_v>=0; -cur_v+1.>=0; -cur_v-n+2.>=0; cur_v-n>=0; -n+1.>=0; -n+prefn>=0; -cur_v-prefn+2.>=0; cur_v-prefn>=0; -n-prefn+2.>=0; n-prefn>=0; -prefn+1.>=0|]

The new version returns [|cur_v>=0; cur_v-n>=0; -n+prefn>=0; cur_v-prefn>=0; n-prefn>=0|] The old version returns [|cur_v>=0; -n+prefn>=0; n-prefn>=0|]

I think the old version’s output is correct. However, I am not sure why the new version produces that. I tried to look at the fdump output of v1 across the 2 files and there is a difference which I do not know how to interpret.

This is the (verbatim) output of the old version: abstract value of level 1:

environment: dim = (3,0), count = 21
 0: cur_v
 1: n
 2: prefn
octagon of dim (3,0)
matrix:
0 0
0 0
+oo +oo 0 +oo
+oo +oo 0 0
+oo +oo 0 +oo 0 +oo
+oo +oo 0 0 0 0
closed matrix:
0 0
0 0
+oo +oo 0 +oo
0 0 0 0
+oo +oo 0 +oo 0 +oo
0 0 0 0 0 0

This is the output of the new version: abstract value of level 1:

environment: dim = (3,0), count = 1
 0: cur_v
 1: n
 2: prefn
octagon of dim (3,0)
matrix: NULL
closed matrix:
0 0
0 0
+oo +oo 0 +oo
0 0 0 0
+oo +oo 0 +oo 0 +oo
0 0 0 0 0 0

[antoinemine]

Hi, Could you please clarify what are both widening arguments in both case? I'd expect to see four octagons, o1, o2, o3, o4, such that o1 ▽ o2 and o3 ▽ o4 are different. What do you mean by "sort of" the same?

There are several possible widenings for octagons. Apron employs a syntactic widening that is sensitive to the representation (set of constraints) of its inputs, as it can be more precise than more semantic widening. In all cases, the widening is quite sensitive to its inputs.

[culechetoo]

I'm computing v1 ▽ v2. In both cases, the widening arguments have the above stated "Abstract1.print" output.

However, the "Abstract1.fdump" output for v1 is different in the two cases. This leads to different outputs.

I would expect that given the "Abstract1.print" representation is the same, I should observe the same output.

[antoinemine]

OK. What happens is that octagon matrices are put in closed form for most operations, including printing, as this is a normal form which ensures the best precision. Widening is an exception. Forcing a closed form between iterates can jeopardize convergence. Hence, although both versions of v1 (and v2) may print equal and have an equal normal form, they may have a different non-closed representation, which is the one used by widening. This explains the difference in output. However, both results should be correct over-approximations.

An alternate widening for octagons, which is semantic and not syntactic, has been proposed in later works. However, it is not implemented in Apron.