New category for undefined behavior?

[dbeyer]

Currently, we have this structure for SV-COMP 2017:
https://sv-comp.sosy-lab.org/2017/categories.svg
The main categories Arrays, BitVectors, and HeapDataStructures
contain each a sub-category for memsafety or overflows,
which in turn represent undefined behavior (invalid free, invalid deref, and invalid overflows).

Would it be better to concentrate undefined behavior in an own property class or category?

I.e., wouldn't it be better to move invalid free, invalid deref, and invalid overflows to a category
for undefined behavior, and leave mem-leak in the Heaps category?

Overflows: Were put to BitVectors because it was assumed that bit-vector theory is good to find those bugs. But other techniques work as well. So the connection to bit-vectors is not obvious anymore.

Arrays-MemSafety: Are those verification tasks really interesting properties for a theory of arrays,
or are we simply looking for undefined stuff?

I am wondering if a property/category for "Defined Behavior" makes more sense in terms of
a more logical or intuitive structure,
and is a good idea to invite definedness checkers to the competition in that category.

[tautschnig]

We could generalise memory leaks to "resource leaks", which is a class of practically relevant problems. (And then, finally, the Infer team might want to join.)

[dbeyer]

+1

…

On 2016-11-27 10:50 PM, Michael Tautschnig wrote: We could generalise memory leaks to "resource leaks", which is a class of practically relevant problems. (And then, finally, the Infer team might want to join.) — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#261 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACzgUL6APQJzUfHJ1AU6uTmLIqJ9inr2ks5rCftBgaJpZM4K9Q4w>.

[zvonimir]

Just to clarify, you are not suggesting that we add additional properties to check (such as undefined behaviors that are currently not specified/caught as SV-COMP properties), but rather only to restructure the benchmarks/categories. Is that right?

[dbeyer]

That is right.
But we should have new properties in mind (for demo category or next year),
such as _no-undef-vars or so, in order to more thoroughly check for undefined behavior.
Even if we do not have a category of this in SV-COMP, it would be good for the
definedness checkers to provide a defined playground to them in the repository.

[zvonimir]

Absolutely! That would be super valuable for a demo category and next year as well!

[tautschnig]

Are we on a path to ending the never-ending category debate?

[Heizmann]

I presume you changed the SVG in the current file, the main categories are Reachability, Memory Safety, Overflows, Concurrency, Termination, and Software Systems.

I think, we should not (neither now nor in the future) have a property "undefined behaviour". There are many kinds of undefined behaviour we might want to have a property for each of them and want to check them individually (wherever possible) because we want to attract also tools that check only some of these properties.

Regarding the other questions I do not have strong preferences. I fine with your current suggestions (SVG above).

[dbeyer]

Conclusion: For SV-COMP 2017, we leave the invalid derefs and invalid frees in MemSafety,
and the invalid overflows in Overflows.
Next time we reconsider adding a property for checking undefined variables and have another
category capturing this.

Compare with issue #270.

[dbeyer]

_false-def-behavior

is the label to mark programs that have undefined behavior different from

• invalid dereference (_false-valid-deref),
• invalid deallocation (_false-valid-free), and
• invalid overflows of signed integer variables (_false-no-overflow).