Local variable display breaks when expressions are large

[jpdoyle]

Given this file:

/*@ #include <nat.gh> @*/

/*@

lemma void pow_square(int b, int e);
    requires b >= 1 &*& e >= 0;
    ensures  pow_nat(b,nat_of_int(e))*pow_nat(b,nat_of_int(e))
        ==   pow_nat(b,nat_of_int(2*e));

lemma int test()
    requires true;
    ensures  result == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(18))));
{
    int x = 2;
    pow_square(2,pow_nat(2,nat_of_int(0)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(1))));
    pow_square(2,pow_nat(2,nat_of_int(1)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(2))));
    pow_square(2,pow_nat(2,nat_of_int(2)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(3))));
    pow_square(2,pow_nat(2,nat_of_int(3)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(4))));
    pow_square(2,pow_nat(2,nat_of_int(4)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(5))));
    pow_square(2,pow_nat(2,nat_of_int(5)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(6))));
    pow_square(2,pow_nat(2,nat_of_int(6)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(7))));
    pow_square(2,pow_nat(2,nat_of_int(7)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(8))));
    pow_square(2,pow_nat(2,nat_of_int(8)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(9))));
    pow_square(2,pow_nat(2,nat_of_int(9)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(10))));
    pow_square(2,pow_nat(2,nat_of_int(10)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(11))));
    pow_square(2,pow_nat(2,nat_of_int(11)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(12))));
    pow_square(2,pow_nat(2,nat_of_int(12)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(13))));
    pow_square(2,pow_nat(2,nat_of_int(13)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(14))));
    pow_square(2,pow_nat(2,nat_of_int(14)));
    x *= x;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(15))));
    pow_square(2,pow_nat(2,nat_of_int(15)));
    x *= x;
    int_of_nat_of_int(16);
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(16))));
    pow_square(2,pow_nat(2,nat_of_int(16)));
    x *= x;
    int_of_nat_of_int(17);
    assert int_of_nat(succ(nat_of_int(16))) == 17;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(17))));
    pow_square(2,pow_nat(2,nat_of_int(17)));
    x *= x;
    int_of_nat_of_int(18);
    assert int_of_nat(succ(nat_of_int(17))) == 18;
    assert x == pow_nat(2,nat_of_int(pow_nat(2,nat_of_int(18))));
    return x;
}

  @*/

When I run to cursor on return x; in vfide I see a garbled value in the locals pane:

This doesn't happen when x is 2^(2^16):

Currently this is on a slightly modified version of vfide and I haven't tested it on master yet, but I'd suspect it happens on other versions as well.

[btj]

Seems like it's probably a Gtk fluke.

Note that I started working on VeriFast integration into VSCode recently, partly as a backup plan in case the Gtk-based approach ever becomes too cumbersome. Basic use cases mostly work, but many of the features present in vfide are still missing.

[jpdoyle]

I did some digging, and I'm pretty sure that what's happening is that the text rendering is actually looping around! GTK uses Pango, and most of the coordinate calculations in pango are using int (which I believe is 32-bit on my system). However, by default coordinates are scaled up by 1024 (I think for smoothing/subpixel purposes?). There seem to be bounds checks that prevent it from rendering at negative coordinates, but there aren't checks to prevent things from overflowing.

Going from x to (x * x) increases the string length from n to 2n + 5, and running that 17 times yields a string length of 786427. Guessing ~10px-wide characters, 10*786427*1024 == 8053012480, which is big enough to overflow a signed 32-bit number and wrap back into the positive a few times. And at 16, we have 393211 characters, and 10*393211*1024 is only large enough to overflow into the negative range, rather than looping back around.

What a nifty quirk.