Minimal set of effective settings

[ivanperez-keera]

IKOS' analysis can be configured via command-line flags.

Is there a set of flags that will 1) be relatively fast to run and 2) have a very low rate of false positives (meaning code that IKOS marks as potentially or definitely unsafe, but isn't)?

I'm happy if the checks are limited in scope, but I'm interested in identifying settings that will fulfill the conditions above.

Thanks!

[arthaud]

For a very fast run you can use --proc=intra, it will do an intraprocedural analysis which does not propagate invariants between functions (except for pointers, since that's handled as a separate step).
Then if you only want very high signal messages, you can use --status-filter=error. Note that this is an ikos-report option, so you have to run the initial ikos command with ikos -f=no and then run ikos-report.
I'm not sure this will yield anything useful though, it will only flag very obvious errors.

[ivanperez-keera]

Thanks!

Well, it's a start. We've added support for ikos to https://github.com/space-ros/space-ros, but it's currently disabled and some potential users won't enable it because it produces too many false positives. My hope is that we can work our way up, starting with the most obvious errors.

We are also expecting that some users will run IKOS in their CI. For that use case specifically, it can't produce many false positives.

[ivanperez-keera]

Being included in Debian & Ubuntu would go a long way towards helping us pack IKOS with Space ROS. It's work in progress.

Right now, if we want to do it, we have to compile it "by hand".

[ivanperez-keera]

I have an update: IKOS will be included with the next release of Space ROS, which will be released very soon. It'll still be disabled in its battery of tests by default, but users can enable it by hand and will have it immediately available.

For the next release of Space ROS after that (April 30), finding this minimal set would be very helpful, since it would justify turning IKOS on by default. Helping Space ROS and ROS 2 users detect bugs could in turn help IKOS gain adoption, creating a positive feedback loop between IKOS and the Space ROS and ROS communities.

I'll try with the settings you propose and take it from there. If anyone wants to try it on their end, I'd be very happy to provide instructions.

[ivanperez-keera]

Tagging @xfiderek for awareness. This discussion is related to the plans for Space ROS and the need for configuration settings that make IKOS run 1) faster and 2) producing fewer false positives. The settings we find may end up being documented also part of IKOS' guide or something like that.