search

ultimate-pa / ultimate

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

Question: How to use bvbuiltin functions in LTLAutomizer? #659

Open GreenieQwQ opened 10 months ago

GreenieQwQ commented 10 months ago

Basic Info

The following boogie example may require the boogie-steps Branch. The branch enables handling of LTL attributes in Boogie (as used by the example).

An archive with the Boogie file, the tool chain and the setting file is attached: archive.zip.

Description

I'm running Ultimate Debugging Gui to test if LTLAutomizer supports the bitvector version of boogie. Unfortunately, it reported:

java.lang.UnsupportedOperationException: function symbols not yet supported: (add.bv8 (_ BitVec 8) (_ BitVec 8) (_ BitVec 8)) Type: class de.uni_freiburg.informatik.ultimate.lib.smtlibutils.NonTheorySymbol$Function
    at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoPartitioneer.addInOuAuxVar(LassoPartitioneer.java:238)
    at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoPartitioneer.constructTransFormulaLR(LassoPartitioneer.java:210)
    at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoPartitioneer.doPartition(LassoPartitioneer.java:165)
    at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoPartitioneer.<init>(LassoPartitioneer.java:95)
    at de.uni_freiburg.informatik.ultimate.lassoranker.preprocessors.LassoPartitioneerPreprocessor.process(LassoPartitioneerPreprocessor.java:65)
    at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoBuilder.applyPreprocessor(LassoBuilder.java:154)
    at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoBuilder.preprocess(LassoBuilder.java:262)
    at de.uni_freiburg.informatik.ultimate.lassoranker.LassoAnalysis.preprocess(LassoAnalysis.java:280)
    at de.uni_freiburg.informatik.ultimate.lassoranker.LassoAnalysis.<init>(LassoAnalysis.java:229)
    at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.LassoCheck.synthesize(LassoCheck.java:601)
    at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.LassoCheck$LassoCheckResult.checkLassoTermination(LassoCheck.java:916)
    at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.LassoCheck$LassoCheckResult.<init>(LassoCheck.java:823)
    at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.LassoCheck.<init>(LassoCheck.java:247)
    at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.cegar.AbstractBuchiCegarLoop.runCegarLoop(AbstractBuchiCegarLoop.java:310)
    at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.BuchiAutomizerObserver.doTerminationAnalysis(BuchiAutomizerObserver.java:146)
    at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.BuchiAutomizerObserver.finish(BuchiAutomizerObserver.java:363)
    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)

I manually added the detailed information in the first line. I wonder if there is something wrong in my settings, or the current version of LTLAutomizer is not capable of handling bvbuiltin functions (as in the example, add.bv8 is of attribute {:bvbuiltin "bvadd"})?

Any answer would be of great help.

schuessf commented 10 months ago

If I remember correctly, we currently cannot handle bitvectors in the computation of ranking functions, which is however necessary in LTLAutomizer and BuchiAutomizer. The implementation of this feature would require some effort. @Heizmann knows more about this than I do, so correct me if I am wrong.