Avoid base invariant fallback not understood message on reflexive pointer literal equality

[sim642]

Closes #1374.

The fix is uglier than I imagined it to be because address set refinement happens in invariant_fallback, not in the general inv_exp, so it doesn't simply fall into the existing https://github.com/goblint/analyzer/blob/da91765f030b3583606e50ad21b0d0b336c52fc7/src/analyses/baseInvariant.ml#L775

A less ugly fix would be to make inv_exp also do addresses with HC4-revise, but that requires carefully porting all the ancient fallback logic with countless edge cases.

[michael-schwarz]

Maybe the fix should also attempt to forgo emitting these: Tasking the event system with what we know to be a fool's errand, might have a performance impact. While it will most likely be very small, it's probably still worth doing as it'll be very little extra work to add this check.

Also, I am not entirely convinced by the usage of polymorphic variants here yet. I guess the only difference to normal variants here is that NothingToRefine cannot be emitted by helper. Is this really an important invariant that we want to enforce (and are worth paying the penalty for less efficient code for it, provided this is still the case after flambda)?

[sim642]

Also, I am not entirely convinced by the usage of polymorphic variants here yet. I guess the only difference to normal variants here is that NothingToRefine cannot be emitted by helper. Is this really an important invariant that we want to enforce (and are worth paying the penalty for less efficient code for it, provided this is still the case after flambda)?

The use of polymorphic variants doesn't actually change the memory representations here: argument-less polymorphic variants are unboxed integers like normal variants and a polymorphic variant with two arguments is really a block with a reference to a pair block, but that was also the case before with a pair option.

[michael-schwarz]

Besides the point but still interesting:

The use of polymorphic variants doesn't actually change the memory representations here: [...] a polymorphic variant with two arguments is really a block with a reference to a pair block, but that was also the case before with a pair option.

Interesting, do you have a reference for this? RealWorldOCaml seems to disagree:

Polymorphic variants use more memory space than normal variants when parameters are included in the data type constructors. Normal variants use the tag byte to encode the variant value and save the fields for the contents, but this single byte is insufficient to encode the hashed value for polymorphic variants. They must allocate a new block (with tag 0) and store the value in there instead. Polymorphic variants with constructors thus use one word of memory more than normal variant constructors.

https://dev.realworldocaml.org/runtime-memory-layout.html

I would read this as:

• (x * y ) option
  • 1 block for the pointer to the tuple, and Some vs None expressed in the tag
  • 1 block for the tuple itself
  • • memory for x and y

[sim642]

Polymorphic variants with constructors thus use one word of memory more than normal variant constructors.

Normal variants flatten their arguments instead of storing a tuple, so what this is saying is that `Refine of lval * value uses one block more than Refine of lval * value would. But also Refine of (lval * value) would use one block more for the pair which it explicitly contains. And that by abstraction is the same as (lval * value) option.

[michael-schwarz]

The atomic privatizations added in the course of https://github.com/goblint/analyzer/pull/1216 seem to depend on the refine event being emitted for &a == &a. That seems very strange.

[sim642]

The atomic privatizations added in the course of #1216 seem to depend on the refine event being emitted for &a == &a. That seems very strange.

That's odd indeed. Maybe it has something to do with the special atomic lock somehow.

[sim642]

I extracted the optimization to #1407 to get approved thing merged.