search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link

Bug: Procedure inliner fails on post-conditions with in-parameters nested in `old` expressions #640

Closed martin-neuhaeusser closed 1 year ago

martin-neuhaeusser commented 1 year ago

(A zip file with all files to reproduce is attached: inliner_bug.zip)

Description

The procedure inliner throws an exception on examples that involve postconditions in ensures clauses containing subexpressions of the form old(expr), where expr contains input-parameters. An example is the following:

var glob : int;

procedure foo(x : int) returns ( result : int)
ensures result == old(glob + x);
modifies glob;
{
  result := glob + x;
  glob := glob + 1;
  return;
}

procedure ULTIMATE.start() returns ()
modifies glob;
{
  var res : int;
  call res := foo(7);
}

Running the procedure inliner on it gives the following exception:

java.lang.AssertionError: Ambiguous translation mapping. DeclarationInformations cannot be merged: <PROC_FUNC_INPARAM,foo>, <PROC_FUNC_INPARAM,foo>
    at de.uni_freiburg.informatik.ultimate.boogie.procedureinliner.backtranslation.ExpressionBacktranslation.combineDeclInfo(ExpressionBacktranslation.java:101)
    at de.uni_freiburg.informatik.ultimate.boogie.procedureinliner.backtranslation.ExpressionBacktranslation.reverseAndAddMapping(ExpressionBacktranslation.java:77)
    at de.uni_freiburg.informatik.ultimate.boogie.procedureinliner.backtranslation.InlinerBacktranslator.addBacktranslation(InlinerBacktranslator.java:98)
    at de.uni_freiburg.informatik.ultimate.boogie.procedureinliner.Inliner.inline(Inliner.java:135)
    at de.uni_freiburg.informatik.ultimate.boogie.procedureinliner.Inliner.process(Inliner.java:114)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.DFSTreeWalker.runObserver(DFSTreeWalker.java:65)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.runObserver(BaseWalker.java:93)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.run(BaseWalker.java:86)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:166)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:155)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:127)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:233)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:227)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:144)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:106)
    at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:319)
    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)