Bug / Question: Inconsistent verification results depending on blockencoding settings

[martin-neuhaeusser]

Basic Info

The following example requires the boogie-steps Branch. That branch combines the open PRs and enables handling of LTL attributes in Boogie (as used by the example).

I hope (!) the bug is not related to our changes or our handling of LTL steps. It is triggered by changing a single setting of the large block encoding which - to my understanding - operates only on the product automaton and should therefore be independent of any LTL step annotations.

An archive with the Boogie file, the tool chain, the two settings files, and the resulting log-files is attached: rewrite_not_equals.tar.gz

Description

The example Boogie file example_lbe_rewrite_not_equals.bpl contains an LTL formula that is expected to be true.
Running Ultimate Automizer with the LTLAutomizer.xml tool chain and the settings from LTLAutomizer.epf

Ultimate -tc LTLAutomizer.xml -s LTLAutomizer.epf -i example_lbe_rewrite_not_equals.bpl

succeeds and proves the property.
However, setting the option /instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Rewrite\ not-equals=true (as done in LTLAutomizer_fails.epf and running

Ultimate -tc LTLAutomizer.xml -s LTLAutomizer_fails.epf -i example_lbe_rewrite_not_equals.bpl

produces a counterexample which I think is wrong.
Ultimate Automizer seems to fail tracking a chain of assignments of the msgsender_MSG variable which is initially assumed to be non-null and then takes a wrong branch checking for "nullness" of a variable that got populated indirectly by msgsender_MSG. To see that, start from the branch taking at the end of the counter-example (line 433) and go backwards. If I am not mistaken, spender_s637 cannot be null (null = 0) here due to the assumption in line 730.

Question

The role of rewrite_not_equals is unclear to me - but I suppose it is expected to be equivalence preserving?

[danieldietsch]

Quick answer: yes, it should be equivalence preserving.

[martin-neuhaeusser]

Again, I can't say for sure that the bug is not related to our extensions. So please don't spend too much time on it!
I reported it only because from my understanding, it occurs relatively far away (after the product automaton construction is completed) from the LTL extensions that we introduced.

[Heizmann]

I could reproduce this problem.
However, I find it very difficult to track the value of individual variables since there are a bunch of procedure calls.

Maybe the verification of such examples is speed up by utilizing our procedure inlining plugin. I am however not sure whether this inlining plugin will pass the LTL step attributes.
My plan is to implement that we can see values of variables in the counterexample. I might need some time for this, but I think this feature is desired anyway and this feature would help me to track the values of the variables in this example.

[martin-neuhaeusser]

Obtaining counterexample that contain variable values (also in the presence of procedure calls) is actually more important to us than the potential bug in the block encoding. I just came across it and thought that I'd better report it so that it is not forgotten.

Could you clarify if variable values are generally not reported in counterexamples for programs with nested procedures?
Do we need to use inlining for that to work?

[danieldietsch]

@martin-neuhaeusser this reminds me: you wanted to open an issue / send us an example where we do not produce values in counterexamples.

[martin-neuhaeusser]

@danieldietsch I just opened another issue #597 for the counter-example values. An example is attached there.

[Heizmann]

After 2b22b30 the counterexample looks as follows.
Counterexample.txt
We can see the values of some variables, however for reasons that I don't understand we cannot see the value of spender_s637. I will have a look at that problem.

[Heizmann]

Obtaining counterexample that contain variable values (also in the presence of procedure calls) is actually more important to us than the potential bug in the block encoding. I just came across it and thought that I'd better report it so that it is not forgotten.

Could you clarify if variable values are generally not reported in counterexamples for programs with nested procedures?

• Reporting values is independent of procedures.
• It is just more difficult for me as a human to track values over several procedures. Therefore, I would like to see values in the output.
• In the past we could report values for finite counterexamples but not for infinite counterexamples. My commit allows us to see the values for a finite prefix of the infinite counterexample.

Do we need to use inlining for that to work?

No. But the inlining might improve the performance of the verification. (Might improve, maybe it slows the performance down, it depends on the verification task.)

[Heizmann]

We can see the values of some variables, however for reasons that I don't understand we cannot see the value of spender_s637. I will have a look at that problem.

It seems to me like the value of this variable is lost in the backtranslation of some of the toolchain's plugins.

[martin-neuhaeusser]

As far as I can see, the reason for the incorrect violation is in line 433 of the counterexample:

[L433]  COND TRUE   !(spender_s637 != null)

The corresponding branch is (erroneously) taken, which leads to an exception being raised (in the Boogie model) in line L434-L435):

[L434]              VS_errorMsg := -1425438237;
[L435]              revert := 2;

That directly leads to a violation of the LTL property, which asserts (among other details) that no exception is raised (i.e. that revert ==0 holds).

So (with my limited understanding of the internals of Ultimate) I tend to believe that something goes wrong before the counter-example is mapped back. The very reason that a (this!) counter-example is found relates to the value of the spender_s637 variable.

[Heizmann]

Ok, I spotted another problem:
If the following setting is set to true, the old code of the block encoding plugin does not only replace x!=y by x<y || x>y, the code also replaces all constant symbols by global variables. This replacement can however be unsound in the presence of axioms.
/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Rewrite\ not-equals=true

Note 1: Although the Boogie file does not contain any axioms, the BoogiePreprocessor (our first preprocessing step) will introduce axiom to account for the const unique declarations. E.g., in the program above, we add the following axioms.

axiom null != IERC20;
axiom null != IERC20Metadata;
axiom null != Context;
axiom null != ERC20;
axiom IERC20 != IERC20Metadata;
axiom IERC20 != Context;
axiom IERC20 != ERC20;
axiom IERC20Metadata != Context;
axiom IERC20Metadata != ERC20;
axiom Context != ERC20;

Note 2: The plugin rewrites all not equals relations. An optimization could be to rewrite only the relations that finally cause that an edge is split into two parallel edges.

Note 3: While translating C to Boogie we do not (yet) introduce any axioms. Hence, programs with axioms are not tested very well. There are two known minor problems. These do however not affect the soundness but only the perfomance.

[danieldietsch]

For 2: If I remember correctly, some (non)termination proofs profit from a rewrite even if we do not split the edge. If you want to add a check that prevents rewrites if no split is possible, I would make it an option.

[Heizmann]

For 2: If I remember correctly, some (non)termination proofs profit from a rewrite even if we do not split the edge. If you want to add a check that prevents rewrites if no split is possible, I would make it an option.

Interesting. I do not have an explanation for such a behavior. If a (non)termination proof benefits from a rewrite without a split this must be due to a bug in the block encoding or the termination analysis.

[Heizmann]

@martin-neuhaeusser I was still trying to find out why we cannot see the values for spender_s637 in the counterexample. It seems to me that we have a major bug in the backtranslation of the BuchiProgramProduct. Due to this bug the position of many program states (the values) in the output is wrong. Some program states occur too late and others are missing because their position is erroneously beyond the last statement and dropped during the backtranslation.
I think I can fix the problem this weekend, maybe also tomorrow.

[martin-neuhaeusser]

@Heizmann Did you use our boogie-steps branch of Ultimate? The Boogie files in my examples will most likely only make sense with the extensions for handling LTL steps.
Not that one of my PRs is actually causing the problems. So please don't spend too much time on the issue!

[Heizmann]

@martin-neuhaeusser Yes, I did use the boogie-steps branch of Ultimate. Thanks for the hint.

[Heizmann]

@martin-neuhaeusser There was definitely a bug that did not only exist in your branch. The bug caused the wrongly positioned program states and is now fixed on the dev branch.

[Heizmann]

Ok, I think I fixed the underlying problem in abfc54d. The commit message explains the problem.
Now, a run with the option /instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Rewrite\ not-equals=true also says that the LTL formula holds for the program.
The problem was that the constant null was sometimes replaced by an auxiliary variable. In the counterexample run, this variable had the value 1.
After the bugfix it should be sound to use the Rewrite\ not-equals=true option.

A minor problem that remains is the our counterexample run does not show values for constants. However, showing the values of constants requires some refactoring and I don't know if if values of constants are important for you @martin-neuhaeusser. (Furthermore, I this raises the question if values for constants should be shown after every step or only once. If we show values of constants only once, this raises the question whether variables of all variables in scope really be shown after each step or if we only want to see that variables that were recently re-assigned.)