Planning: Upcoming changes in IKOS 3.3

[ivanperez-keera]

IKOS 3.3 is planned to be released on March 28, 2024.

--

This is just an open discussion to propose issues to address in IKOS 3.3. If there's a bug that is affecting you, one that you know the solution for, or a feature you'd like to contribute, feel free to comment below.

EDIT: Roughly, the plan is as follows:

• Dec 28 - Jan 10: Planning and selecting issues.

• Jan 11 - Mar 7: Development

  -- Mar 8: Request to release

• Mar 8 - Mar 14: First release candidate, testing

• Mar 15 - Mar 21: Second release candidate / draft of final release, testing

• Mar 25 - Mar 28: Draft release announcement

  -- Mar 28: Final release

[ivanperez-keera]

• Issue IKOS should tolerate snprintf(NULL, 0, ...) #221 looks like low-hanging fruit.
• Issue error: unsupported llvm instruction fneg #197 has a proposed solution already.

[ivanperez-keera]

More things I'd like to address at some point:

• IKOS produces a lot of false positives. The default settings should produce fewer false positives, otherwise people don't use the tools because of the signal to noise ratio.

• IKOS is advertised as a C/C++ static analyzer, but C++ support is preliminary and most of the times, when someone has an issue, we just say "sorry, not supported". I think it'd be better to be straightforward and say it's a C static analyzer, and then somewhere else say that we have preliminary support for C++.

• I'd like to collect a list of orgs using IKOS, and evaluate the user experience more deeply.

• IKOS is advertised as "Static analyzer for C/C++ based on the theory of Abstract Interpretation." I think we lose half the crowd there because they don't know what the "theory of Abstract Interpretation" is. Let's just advertise it as a "Static analyzer for C" with some additional qualifiers that convey to the person not versed in abstract interpretation what the distinguishing characteristics are.

[ivanperez-keera]

And to help drive this discussion, here are some goals for IKOS in the longer term future:

• Increase stability.

• Increase accuracy.

• Increase adoption.

• Increase active participation from the open source community.

[ivanperez-keera]

I don't know exactly what it would entail, but we soon may have to start considering supporting LLVM > 14.

[ivanperez-keera]

I'd like to see this issue investigated and hopefully solved: NASA-SW-VnV/homebrew-core#11

[ivanperez-keera]

Similarly to 197, for #205 we have a candidate solution, making it a perfect candidate to be included in the next milestone. I'm not yet equipped to evaluate it in depth; all I can do at this point is check whether the bug does not manifest after applying the proposed solution.

[ivanperez-keera]

@asensi has indicated that we may not have to bump the copyright years like we did for IKOS 3.2. The following comments offer more details:

• Announcement: IKOS 3.2 #257 (comment)
• Announcement: IKOS 3.2 #257 (comment)

[ivanperez-keera]

An upcoming change that we may consider for 3.3 is the change of license, which has been requested. This will allow IKOS to also be included in Debian's main repositories (right now we can only be included in non-free, which a lot of people do not enable).

We cannot really plan it for 3.3 as such, since it doesn't really depend on us and it can take an arbitrary amount of time. But we'll add it to the release if possible.

[asensi]

It seems the best that can be done at this time. Thanks!

[ivanperez-keera]

I started on a new project in Jan and could not finish as much as I had originally hoped to do. However, we still have a release and we can move some of these low-hanging issues to the next release.