Correctly identify extern statics

[tedinski]

Description of changes:

Fixes Kani's detection of extern static variables. This has no observable effect, because I believe this has no animating semantics on the CBMC side. I suspect this flag on the symbol exists for the CBMC C compiler's benefit only.

Nevertheless, this corrects our behavior. The old linkage check was wrong: that only detects the presence of a #[linkage] attribute, not the externness of the declaration.

Resolved issues:

Resolves #388
Resolves #400

Testing:

• How is this change tested? N/A apparently: a comment describes my experiments. It doesn't matter.

• Is this a refactor change? no

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

CBMC does also use this information when constructing the initialiser code for objects with static lifetime. When is_extern is true and there is no initialisation value provided then a non-deterministic value is constructed. I suspect that either you never have symbols without initialiser, or perhaps those are just never used (which would be the desirable!).

[tedinski]

I'll add that info to the comment, but: we... might not want that behavior for Kani? I would be inclined to see errors if we try to use an uninitialized static variable, just like we do for missing function definitions.

[tedinski]

In CBMC, is !is_extern with a missing initializer an error or zero-initialized?

[tedinski]

Aha, this is the function static_lifetime_init in static_lifetime_init.cpp and I think I see the zero-init. :)

[tautschnig]

Yes re zero-init; for the "error" case: I think that's the "poison value" problem, so we really need/want a solution for that one.

[celinval]

Is it possible to add some tests that declare and use extern statics?

[tedinski]

Is it possible to add some tests that declare and use extern statics?

Given Michael's clarification about the actual semantics difference, I can add a test for that at least.

Interestingly, the previous behavior was extra-broken. It was setting is_extern to rlinkage.is_none() which... was probably the opposite of the intention. Of course, it didn't break anything because no current test tries to exercise a missing/uninitialized extern static.

[celinval]

Thanks