This is not a lasso program

[danieldietsch]

With the new ICFG and the new block encoding, LassoRanker seems to have trouble finding lassos in the CFG.

For example, consider the (formerly working) input:

• examples/termination/svcomp15/termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_true-termination.c
• examples/settings/LassoRankerBEv2.epf
• examples/toolchains/LassoRankerCBEv2.xml

LassoRanker reports "This is not a lasso program".

The NWA constructed from the ICFG looks as follows:

NestedWordAutomaton nwa = (
    callAlphabet = {"call ULTIMATE.init();" "call #t~ret4 := main();" },
    internalAlphabet = {"assume true;" "assume -2147483648 <= #t~nondet0 && #t~nondet0 <= 2147483647;~tx~2 := #t~nondet0;havoc #t~nondet0;assume -2147483648 <= #t~nondet1 && #t~nondet1 <= 2147483647;~x~2 := #t~nondet1;havoc #t~nondet1;assume -2147483648 <= #t~nondet2 && #t~nondet2 <= 2147483647;~y~2 := #t~nondet2;havoc #t~nondet2;assume ~x~2 >= ~y~2 && ~tx~2 >= 0;" "assume (#t~nondet3 <= 2147483647 && -2147483648 <= #t~nondet3) && !(#t~nondet3 != 0);havoc #t~nondet3;~y~2 := ~y~2 + 1 + ~tx~2;assume ~x~2 >= ~y~2 && ~tx~2 >= 0;" "assume (#t~nondet3 <= 2147483647 && -2147483648 <= #t~nondet3) && #t~nondet3 < 0;havoc #t~nondet3;~x~2 := ~x~2 - 1 - ~tx~2;assume ~x~2 >= ~y~2 && ~tx~2 >= 0;" "assume (#t~nondet3 <= 2147483647 && -2147483648 <= #t~nondet3) && #t~nondet3 > 0;havoc #t~nondet3;~x~2 := ~x~2 - 1 - ~tx~2;assume ~x~2 >= ~y~2 && ~tx~2 >= 0;" },
    returnAlphabet = {"return;" },
    states = {"1#ULTIMATE.initEXITtrue" "2#L16true" "3#mainENTRYtrue" "4#L1true" "5#ULTIMATE.startENTRYtrue" "6#ULTIMATE.initFINALtrue" },
    initialStates = {"5#ULTIMATE.startENTRYtrue" },
    finalStates = {"1#ULTIMATE.initEXITtrue" "2#L16true" "3#mainENTRYtrue" "4#L1true" "5#ULTIMATE.startENTRYtrue" "6#ULTIMATE.initFINALtrue" },
    callTransitions = {
        ("4#L1true" "call #t~ret4 := main();" "3#mainENTRYtrue")
        ("5#ULTIMATE.startENTRYtrue" "call ULTIMATE.init();" "6#ULTIMATE.initFINALtrue")
    },
    internalTransitions = {
        ("2#L16true" "assume (#t~nondet3 <= 2147483647 && -2147483648 <= #t~nondet3) && !(#t~nondet3 != 0);havoc #t~nondet3;~y~2 := ~y~2 + 1 + ~tx~2;assume ~x~2 >= ~y~2 && ~tx~2 >= 0;" "2#L16true")
        ("2#L16true" "assume (#t~nondet3 <= 2147483647 && -2147483648 <= #t~nondet3) && #t~nondet3 < 0;havoc #t~nondet3;~x~2 := ~x~2 - 1 - ~tx~2;assume ~x~2 >= ~y~2 && ~tx~2 >= 0;" "2#L16true")
        ("2#L16true" "assume (#t~nondet3 <= 2147483647 && -2147483648 <= #t~nondet3) && #t~nondet3 > 0;havoc #t~nondet3;~x~2 := ~x~2 - 1 - ~tx~2;assume ~x~2 >= ~y~2 && ~tx~2 >= 0;" "2#L16true")
        ("3#mainENTRYtrue" "assume -2147483648 <= #t~nondet0 && #t~nondet0 <= 2147483647;~tx~2 := #t~nondet0;havoc #t~nondet0;assume -2147483648 <= #t~nondet1 && #t~nondet1 <= 2147483647;~x~2 := #t~nondet1;havoc #t~nondet1;assume -2147483648 <= #t~nondet2 && #t~nondet2 <= 2147483647;~y~2 := #t~nondet2;havoc #t~nondet2;assume ~x~2 >= ~y~2 && ~tx~2 >= 0;" "2#L16true")
        ("6#ULTIMATE.initFINALtrue" "assume true;" "1#ULTIMATE.initEXITtrue")
    },
    returnTransitions = {
        ("1#ULTIMATE.initEXITtrue" "5#ULTIMATE.startENTRYtrue" "return;" "4#L1true")
    }
);

L#16true contains cycles, is accepting, and is connected as far as I can tell.

[Heizmann]

This is definitely a lasso program. The problem is that the new block encoding does not seem to compose sequences that contain calls an returns. A workaround could be to use the procedure inlining as well.

[danieldietsch]

I can add this composition. But I have to check Kojaks support for it first.

[Heizmann]

The termination analysis in general would benefit from this composition.