In some (simple) cases the time for forward and Qed grows exponentially with the number of locals

[MSoegtropIMC]

For example for the following program:

int my_add(int a, int b)
{
    return a + b;
}

int many_locals_10(int val)
{
    int x00,x01,x02,x03,x04,x05,x06,x07,x08,x09;

    x00 = my_add(1, val);
    x01 = my_add(1, x00);
    x02 = my_add(1, x01);
    x03 = my_add(1, x02);
    x04 = my_add(1, x03);
    x05 = my_add(1, x04);
    x06 = my_add(1, x05);
    x07 = my_add(1, x06);
    x08 = my_add(1, x07);
    x09 = my_add(1, x08);
    return x09;
}

with straight forward verification, both the time to run the forward tactic and the time for Qed grow exponentially with the number of locals. E.g. if the above program is extended to 28 locals, the Qed time is 450s. The Qed time grows fairly precisely by a factor of 2 per local. A fixed version (PR follows soon after some cleanup) does the Qed for the same case in 5.6s.

Attached please find C code with various number of locals + VST verification.

Source.zip

[lennartberinger]

Locals that are dead can often be eliminate from LOCALS using the deadvars! tactic. It seems replacing eg
Time do 28 forward_call.
by
Time do 28 (forward_call; deadvars!).
not only substantially speeds up the forward calls but also the Qed:
For your last example, I get
Time do 28 (forward_call; deadvars!). (Lennart: 5.8secs)
...
and a Qed time of 1.2sec instead of 450secs

[MSoegtropIMC]

In my real use case I actually have a bit more than 30 non dead locals. This is not that rare in numerical C code. And for that use case - even with a regular call to deadvars !, Qed did not finish within 11 hours.

The above use case was made to be simple and scalable so that I can analyze the root cause.

Btw.: I didn't do reliable speed tests as yet, but it might be that there is an average speed improvement of about 20% for the verif files in progs64 with the changes I am going to PR. (was a CPU clocking artifact)

[andrew-appel]

Fixed by #492