hernanponcedeleon/Dat3M

LoopFormVerification and gotos

Closed this issue · 8 comments

hernanponcedeleon commented

The LoopFormVerification pass throws an exception on the code below (coming from a real benchmark)

int main()
{
    if (__VERIFIER_nondet_int()) goto forward;

backward:
    if (__VERIFIER_nondet_int()) {
        goto forward;
    }
    if (__VERIFIER_nondet_int()) {
        if (__VERIFIER_nondet_int()) {
            goto forward;
        } else if (__VERIFIER_nondet_int()) {
            if (__VERIFIER_nondet_int()) {
                goto forward;
            }
            else {
                goto backward;
            }
        } else {
            return 0;
        }
    } else {
        return 1;
    }

forward:
    if (__VERIFIER_nondet_int()) goto backward;
    if (__VERIFIER_nondet_int()) return 0;
    goto backward;
}
ThomasHaas commented

Have you tried adding -loop-simplify to the LLVM passes as mentioned in #465 ?

hernanponcedeleon commented

Yes ... I tried inserting it in different places (in case of passes order has an influence) and even tried a few other options related to loops, but nothing helped.

ThomasHaas commented

I haven't checked the loop in detail, but maybe it is not a natural one (though I don't see why).

hernanponcedeleon commented

The main problem seems to be the first goto ... If I remove this one, there are no problems. However, if I remove any of the other ones, the problem remains.

ThomasHaas commented

Maybe it is because the first goto jumps from outside the loop directly into the middle.
The loop doesn't seem to have a unique entry point.

ThomasHaas commented

Have you tried adding fix-irreducible on top of loop-simplify?

hernanponcedeleon commented

This order seems to work ATOMIC_REPLACE_OPTS="-mem2reg -sroa -early-cse -indvars -loop-unroll -fix-irreducible -loop-simplify -simplifycfg -gvn".

I will do some testing to see changing these flags do not affect our usual benchmarks and if so, update the README