Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update Deagle's tool module info for SV-COMP 2024 #950

Merged
merged 8 commits into from
Nov 8, 2023

Conversation

Misasasa
Copy link
Contributor

@Misasasa Misasasa commented Nov 2, 2023

In the SV-COMP 2024 version, Deagle just receives a property file and the input file. So we update Deagle.py accordingly.

@PhilippWendler
Copy link
Member

Please keep this tool-info module backwards compatible with old versions of Deagle. Other users might want to use it to benchmark older versions.

What is the reason for removing this parameter handling? Does Deagle not accept these parameters anymore?

@Misasasa
Copy link
Contributor Author

Misasasa commented Nov 3, 2023

In fact, this tool-info module is used to benchmark a "Deagle-script", which chooses parameters for the Deagle executable based on properties.
For instance, using this tool-info module, benchexec invokes

./deagle.sh no-overflow.prp input.i

, this shell script runs

./deagle.exe input.i --signed-overflow-check --unsigned-overflow-check

The parameters accepted in deagle.exe remain unchanged. Therefore, as long as we provide deagle.sh for users, there is no problem benchmarking old versions of deagle.exe.

@PhilippWendler
Copy link
Member

First, note that this tool-info module executes something named deagle, not deagle.sh or deagle.exe. But this doesn't matter.

The problem with benchmarking old versions of Deagle with a new BenchExec is that the set of parameters passed to Deagle would change (the data model would be missing). So old benchmark executions could not be replicated anymore and (in this case) people could even get wrong results.

@Misasasa
Copy link
Contributor Author

Misasasa commented Nov 3, 2023

Thanks for your notice, when we finally submit our archive, we will rename "deagle.sh" and "deagle.exe" so that Benchexec can easily identify.

In fact, we have conducted experiments to confirm that: an old version of deagle.exe can still be benchmarked by a new Benchexec via the shell script deagle.sh.
When the new Benchexec invokes

./deagle.sh [property_file] [input_file]

This shell script runs

./deagle.exe [options_based_on_property] [input_file]

This command works regardless of deagle.exe's version.

We would explain this carefully when publishing Deagle.

@PhilippWendler
Copy link
Member

Yes, it can be executed, but it will behave differently then previous versions without any warning, and might even produce wrong results. This is a problem for reproducibility and not backwards compatible.

@Misasasa
Copy link
Contributor Author

Misasasa commented Nov 3, 2023

In fact, the previous tool-module info was a mistake: we overlooked the problem of scalability. When Deagle participated in SV-COMP for the first time, it only dealt with PropertyUnreachCall.prp, so that we need not specify the property file in its tool-info module. Recently, it has been extended to four properties (perhaps more in the future!), so I feel an urgent need to fix this mistake as soon as possible.

For users who need to benchmark old versions of Deagle, we will soon give a detailed notice on our Deagle page (e.g., specify the version of Benchexec to use)

@PhilippWendler
Copy link
Member

Ah, I had not noticed the change in the property file, only in the now missing data model. (Btw., don't you need in the future?)

The typical solution for this in tool-info modules is to detect the version and then create the command-line appropriately. So you could do this here as well.

@Misasasa
Copy link
Contributor Author

Misasasa commented Nov 7, 2023

Thanks for your suggestion! Sorry for being a little late but this new version should work!

@PhilippWendler
Copy link
Member

Thanks! I am still surprised that you don't need the data model anymore, but as long as your tool works and the tool-info module is backwards compatible, it is up to you, of course. I have just one last comment, then I can merge.

@Misasasa
Copy link
Contributor Author

Misasasa commented Nov 8, 2023

Thanks for your advice! This new tool-info module caches the current Deagle version. Also, we decide to retain data_model_param in case of future uses.

@PhilippWendler PhilippWendler merged commit d5a4ecb into sosy-lab:main Nov 8, 2023
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

Successfully merging this pull request may close these issues.

2 participants