Bug: Incorrect result when using LTLAutomizer with Boogie inlining

[martin-neuhaeusser]

Basic Info

• Version: This is Ultimate 0.2.2-dev-2b22b30-m
  The example files are attached.

Description

I was experimenting with inlining of our Boogie models, as Matthias hinted at a possible performance improvement. In my experiments LTLAutomizer incorrectly reports that the Boogie program models the LTL formula although it correctly finds the counterexample when run without inlining.
To make sure that this is not due to my changes of the LTLStepAnnotations and the Boogie attributes, I hand-crafted another example in C which uses __VERIFIER_ltl_step to add LTL steps into the resulting Boogie models. Running with the current dev HEAD (2b22b30), I can reproduce the same behavior.

It seems as if LTLAutomizer is able to pick up the LTL specification which is contained in the *.c file in all configurations. However, it only finds the counter-example if run on the LTLAutomizerC_Without_Inlining.xml toolchain.

My command lines were:

Ultimate -tc LTLAutomizerC_With_Inlining_Before_Boogie_Preprocessor.xml -s LTLAutomizer.epf -i c_example_sequential_steps_incorrect.c
Ultimate -tc LTLAutomizerC_With_Inlining_After_Boogie_Preprocessor.xml -s LTLAutomizer.epf -i c_example_sequential_steps_incorrect.c
Ultimate -tc LTLAutomizerC_Without_Inlining.xml -s LTLAutomizer.epf -i c_example_sequential_steps_incorrect.c

In all three cases, the result summary on the console indicates that the LTL formula has been found and parsed:

• For the third invocation:

Found an infinite, lasso-shaped execution that violates the LTL property G(((1 == ~a~0) ==> X((4 == ~b~0))))

• For the first two invocations:

Buchi Automizer proved that the LTL property G(((1 == ~a~0) ==> X((4 == ~b~0)))) holds

[maul-esel]

LTLAutomizer has troubles with inlining, because it ignores all steps within the procedures ULTIMATE.init and ULTIMATE.start. Inlining results in a program where all code is inlined into one of these procedures (see here and here).

We'd probably need to support some limited inlining that ignores these procedures. IIRC the inliner already has a blacklist such that calls to procedures on the blacklist are not inlined; here we would need to make sure that calls from ULTIMATE.start/.init are not inlined.

If your models have some uniquely named starting procedure that is not called from anywhere else, putting that procedure (or in case of C programs, main) on the existing blacklist might also work.

[martin-neuhaeusser]

@maul-esel Thanks for the explanation! I changed our model construction to always call an entry procedure from within ULTIMATE.start and add that procedure to the exceptions for the Boogie inliner.

On most of the examples I experimented with today, inlining brings a significant performance improvement. An interesting observation is that on the inlined Boogie models, most (if not all) kinds of block encoding are degrading performance. Without having conducted a thorough benchmark (yet), the most promising combination for our standard examples seems to be inlining, followed by the LTLAutomizer toolchain without any block encoding after the product construction.

If I recall correctly, I came across examples where Büchi Automizer spends 3s without block encoding and block encoding itself require >40s.

Are you interested in such benchmarks? If so, I can try to provide some - but that will take some days, at least. I have some other deadlines approaching and need to work for that a bit.

[Heizmann]

@martin-neuhaeusser
Yes, these benchmarks would be interesting. However, this is absolutely not urgent.