Extracting information from property names is unreliable

[adpaco-aws]

CBMC version: 5.63.0

In general, property names have the format <function>.<class>.<counter>. Until now, we had assumed in Kani that <function>. was optional, so extracting the property class was still easy enough.

Some time ago, we had a regression in Kani for detecting missing function definitions when we tried to upgrade to CBMC 5.59.0 (more details in model-checking/kani#1271). Now I'm reviewing the code which extracts information from property names (using CBMC JSON output), and I've found that all of these variants are possible:

1. <function>.<class>.<counter>
2. <class>.<counter>
3. <function>.<counter>
4. .recursion (specific case with description "recursion unwinding assertion")

It's very complicated for us to know whether we are in case (2) or (3). And case (4) was totally unexpected. Is there a reason not to add these attributes (function, class and counter) as separate fields in the JSON output?

[tautschnig]

Would you have example code exhibiting these? I would like to believe that only (1) is expected, and all others are some kind of bug that needs fixing.

[markrtuttle]

It would be helpful to have a small example to study that is independent of kani. The json and xml output from cbmc differ dramatically in content. For error traces, the xml output is far easier to deal with, and more complete for the things I care about. I consider the canonical property listings to be from cbmc --show-properties --xml-ui. The output of cbmc --trace --xml-ui does include property listings, but I believe only for the failed properties. The cbmc-viewer put a lot of work into turning text, json, and xml output into a canonical json representation, and this is available with the cbmc-viewer property subcommand.

[thomasspriggs]

Separate fields for the various different components of the property names is a far more robust solution in my opinion than trying to keep a standardised string which is then split. In particular the current style of approach has caused many problems to me in the past dealing with Java type names. For example with a Java name such as foo.bar.baz it isn't clear whether bar is a package or a class, without further context given that java has both nested packages and classes. Therefore I would be in favour of adding separate fields and adding them to both the JSON and XML UI, in order to bring them closer to parity. IMO it would would good for us to aim to have the full information printed in both the XML and JSON UIs so that there is no need to look at both output formats. Which improvements we make to the UI and when is a separate question of prioritisation however.

[adpaco-aws]

Would you have example code exhibiting these? I would like to believe that only (1) is expected, and all others are some kind of bug that needs fixing.

Apologies for the delay, @tautschnig !

We have examples of each instance in our regression suite. They are easier to identify with a few modifications on the deserializing code in model-checking/kani#1514 (which we may to use as a temporary fix in Kani). Below I point you to some of them.

<class>.<counter>

This case is the most common by far, and it looks like a high number of them are related to CBMC built-in functions/checks.

• pointer_dereference.1 (+11 other instances) in tests/kani/Closure/main.rs
• bit_count.1(+3 other instances) in tests/kani/Count/Unstable/Cttz/main.rs are two of them.

<function>.<counter>

This case seems specific to missing functions.

• _ZN60_$LT$alloc..string..String$u20$as$u20$core..clone..Clone$GT$5clone17h4b8dc932343fdba9E.1 in tests/ui/missing-function/replaced-description/main.rs.

.recursion

• .recursion in tests/expected/dynamic-error-trait/main.rs.

[adpaco-aws]

It would be helpful to have a small example to study that is independent of kani. The json and xml output from cbmc differ dramatically in content. For error traces, the xml output is far easier to deal with, and more complete for the things I care about. I consider the canonical property listings to be from cbmc --show-properties --xml-ui. The output of cbmc --trace --xml-ui does include property listings, but I believe only for the failed properties. The cbmc-viewer put a lot of work into turning text, json, and xml output into a canonical json representation, and this is available with the cbmc-viewer property subcommand.

Thanks for the comment, @markrtuttle ! We might consider using cbmc-viewer to this end, but in my opinion it would be better to get this fixed in CBMC. It doesn't make sense that the JSON and XML outputs differ that much!

[adpaco-aws]

Separate fields for the various different components of the property names is a far more robust solution in my opinion than trying to keep a standardised string which is then split. In particular the current style of approach has caused many problems to me in the past dealing with Java type names. For example with a Java name such as foo.bar.baz it isn't clear whether bar is a package or a class, without further context given that java has both nested packages and classes. Therefore I would be in favour of adding separate fields and adding them to both the JSON and XML UI, in order to bring them closer to parity. IMO it would would good for us to aim to have the full information printed in both the XML and JSON UIs so that there is no need to look at both output formats. Which improvements we make to the UI and when is a separate question of prioritisation however.

Thanks for the input, @thomasspriggs ! We also have this issue in Kani since mangled names may contain dots in between, which makes it harder to separate the property attributes.