Update SeaHorn's tool-info module

[Po-Chun-Chien]

The existing tool-info module for SeaHorn was created for the version submitted to SV-COMP 2016.
This PR updates the module to work with the latest version.

[Po-Chun-Chien]

The updated tool-info module is not backward compatible.

@PhilippWendler Should I create another file instead?
Or what would be your suggestion?

[PhilippWendler]

The best would be to let the tool-info module work automatically with all versions of the tool, if necessary by detecting the tool's version. This is what we do in several similar cases.

[Po-Chun-Chien]

Let me provide more information:

The old tool-info module is written for the SV-COMP wrapper (bin/sea_svcomp) of SeaHorn (at version 0.1.0).
The new tool-info module I wrote works for SeaHorn's wrapper (bin/sea) for general use
and is compatible with the both older (v0.1.0) and newer version (v14).

(the SV-COMP wrapper does not exist for newer version anymore.)

In this case, should I

• detect the given command-line arguments: if there are SV-COMP specific ones, then bin/sea_svcomp is called (and determine_result is switched as well)
• create a separate file sea.py for the new module

[PhilippWendler]

Having a separate tool-info module is technically always possible, but I would consider it the least desirable solution if there are no strong arguments against a unified tool-info module, in particular because the nice name seahorn.py would really belong to the new tool-info module, but is already used by the old one.

Detecting which tool to call wouldn't really work based on the command-line arguments, because one basically needs to decide already in the executable method, such that version gets the correct executable. Otherwise this probably gets really messy. So how about just looking for bin/sea_svcomp first, then bin/sea in executable()? I guess SeaHorn doesn't ship their wrapper script outside their SV-COMP submissions, or do they have it in their repo and releases?

[Po-Chun-Chien]

So how about just looking for bin/sea_svcomp first, then bin/sea in executable()?

Sure! I could also add some logging if needed.

I guess SeaHorn doesn't ship their wrapper script outside their SV-COMP submissions, or do they have it in their repo and releases?

This I am not sure, but I think it is likely the case.
There are not many releases on their GitHub Releases page.
In v0.1.0 Release (SV-COMP'16), bin/sea_svcomp is included.

The later releases are only available as Docker images.
I manually checked v10 and v14,
and bin/sea_svcomp is not included there.

[PhilippWendler]

So how about just looking for bin/sea_svcomp first, then bin/sea in executable()?

Sure! I could also add some logging if needed.

With level debug, sure.

I guess SeaHorn doesn't ship their wrapper script outside their SV-COMP submissions, or do they have it in their repo and releases?

This I am not sure, but I think it is likely the case. There are not many releases on their GitHub Releases page. In v0.1.0 Release (SV-COMP'16), bin/sea_svcomp is included.

The later releases are only available as Docker images. I manually checked v10 and v14, and bin/sea_svcomp is not included there.

If you think this is a good detection strategy, I would go with it.

[Po-Chun-Chien]

bin/sea_svcomp and bin/sea also write outputs in different style,
thus requires different handling in determine_result().

Is it possible to still retrieve the information of executable() in determine_result()?
Or only the information of run is available?

[PhilippWendler]

You can store the outcome of the check which executable is there in an attribute of your Tool instance. It is a documented guarantee by BenchExec that this works (cf. class doc of BaseTool2).

[Po-Chun-Chien]

@PhilippWendler I have updated the tool-info modulo to be compatible with SeaHorn's SV-COMP wrapper in fa218eb, and also tested it using SeaHorn 0.1.0 and 14.

The old tool-info was written with BaseTool, and I adapted it to BaseTool2.
It would be nice if you could double-check if the mapping between BaseTool and BaseTool2 is correct.