Büchi product construction complains about duplicate identifiers when using inlining

[martin-neuhaeusser]

Basic Info

• Version: Ultimate 0.2.2-boogie-steps-59e45e1-m

• The example files are attached here: duplicate_location_names.zip

• That issue arises quite often (but only on selected instances, i.e. not always)

Description

The following command aborts with an exception that complains about duplicate identifiers being found during the Büchi product construction.

Ultimate -tc LTLAutomizerWithInlining.xml -s LTLAutomizer.epf -i Obfuscated-erc20-transfer-revert-zero.bpl

The exception is

[2022-09-30 13:33:07,817 INFO  L113        PluginConnector]: ------------------------Büchi Program Product----------------------------
[2022-09-30 13:33:07,817 INFO  L271        PluginConnector]: Initializing Büchi Program Product...
[2022-09-30 13:33:07,818 INFO  L275        PluginConnector]: Büchi Program Product initialized
[2022-09-30 13:33:07,819 INFO  L185        PluginConnector]: Executing the observer BuchiProductObserver from plugin Büchi Program Product for "Obfuscated-erc20-transfer-revert-zero.bpl de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 30.09 01:33:07" (2/3) ...
[2022-09-30 13:33:07,819 INFO  L205        PluginConnector]: Invalid model from Büchi Program Product for observer de.uni_freiburg.informatik.ultimate.buchiprogramproduct.BuchiProductObserver@718a61a2 and model type LTL+Program Product de.uni_freiburg.informatik.ultimate.buchiprogramproduct OTHER 30.09 01:33:07, skipping insertion in model container
[2022-09-30 13:33:07,820 INFO  L185        PluginConnector]: Executing the observer BuchiProductObserver from plugin Büchi Program Product for "Hardcoded de.uni_freiburg.informatik.ultimate.ltl2aut AST 30.09 01:33:07" (3/3) ...
[2022-09-30 13:33:07,822 INFO  L104   BuchiProductObserver]: Initial property automaton 2 locations, 3 edges
[2022-09-30 13:33:07,827 INFO  L110   BuchiProductObserver]: Initial RCFG 2758 locations, 4432 edges
[2022-09-30 13:33:07,828 INFO  L93    BuchiProductObserver]: Beginning generation of product automaton
[2022-09-30 13:33:07,841 FATAL L?                        ?]: The Plugin de.uni_freiburg.informatik.ultimate.buchiprogramproduct has thrown an exception:
java.lang.AssertionError: The original RCFG had two locations with the same location name: L1621-76_T0_init of type class de.uni_freiburg.informatik.ultimate.buchiprogramproduct.productgenerator.ProductLocationNameGenerator$BuchiProgramDebugIdentifier
	at de.uni_freiburg.informatik.ultimate.buchiprogramproduct.productgenerator.ProductGenerator.updateProductStates(ProductGenerator.java:232)
	at de.uni_freiburg.informatik.ultimate.buchiprogramproduct.productgenerator.ProductGenerator.createProductStates(ProductGenerator.java:217)
	at de.uni_freiburg.informatik.ultimate.buchiprogramproduct.productgenerator.ProductGenerator.<init>(ProductGenerator.java:153)
	at de.uni_freiburg.informatik.ultimate.buchiprogramproduct.BuchiProductObserver.finish(BuchiProductObserver.java:96)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:168)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:151)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:128)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:232)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:226)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:142)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:104)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:320)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)

Observations

When verifying the same input file without inlining, it works as expected and proves the LTL property.

Ultimate -tc LTLAutomizerWithoutInlining.xml -s LTLAutomizer.epf -i Obfuscated-erc20-transfer-revert-zero.bpl

When inlining the Boogie file separately (and fixing it slightly to avoid the syntax error reported in #600; also re-adding the LTL formulas), the corresponding file is verified without any duplicate locations appearing:

Ultimate -tc LTLAutomizerWithoutInlining.xml -s LTLAutomizer.epf -i Obfuscated-erc20-transfer-revert-zero_inlined.bpl

Speculation

• Could it be that Ultimate Automizer picks up both the inlined and the non-inlined programs and gets confused?
• Might having the LTL formula in the non-inlined file and analyzing (hopefully?) the inlined one create problems?
• How are the two files differentiated by the toolchain?

[Heizmann]

Ok, the problem is that the BuchiProgramProduct identifies (indirectly via the DebugIndentfier) program points with their line number in the original program. If the procedure inlining was used there are several program points that have the same line number.
If the result was written to a file, the inlined statements get new line numbers.

I can probably fix the bug this evening. I will not be able to test the fix very well since we have only few examples with an LTL specification and several procedures.