IOSerialize and IODeserialize testing wrt. unseen string problem

[fhackett]

This PR aims to address a problem with how TLC deserializes string values that did not come from the same run of TLC.
For now, it consists of a failing test that shows the issue.

IODeserialize allows TLC to ingest arbitrary (supported) TLA+ values using the same mechanism that TLC uses for state checkpoints. This almost always works, except for an interaction with string interning.

All strings TLC "sees" are interned in a table, indices into which are used for efficient string comparisons. On state checkpoint, TLC stores both the table and the string objects. The string objects contain indices into that particular TLC process's string table. That's fine, as long as the values are only loaded by either the same TLC instance, or one that restored the same string table from a checkpoint.

The current version of IODeserialize addresses the problem partially, in that it looks up strings in its string table by value regardless of the serialized table index. This means that two TLCs with the same table entries in a different order are compatible. The problem is that IODeserialize can be used outside of this safe condition as well. We can load value dumps from completely unrelated TLC processes (which could be processing specs containing strings we haven't seen), and we can also generate binary files outside of TLC entirely (my use case, incidentally).

Strings that exist as literals in the TLA+, or were previously generated at any point of the same TLC process's runtime, are safe to load. Loading a previously non-interned string, however, creates a StringValue object with a null val pointer, which will crash TLC whenever the value is next accessed. For example, printing it is what I use in the included test.

[lemmy]

@fhackett, should this PR remain open?

[fhackett]

@lemmy thanks for the ping. The plan originally was to merge this once #1102 above was reliably available, but unfortunately I forgot.

I assume the precondition is actually true by now, so maybe we can review and merge the test? It is an obscure issue that might be important to test regressions in.

[lemmy]

@fhackett Can you rebase this PR on top of the master branch? This should trigger the new PR workflow that runs the tests.

[fhackett]

(oops, I hit "sync fork" when looking at my branch not master, and it merged rather than rebased... result is achieved I suppose)

[lemmy]

Thanks Finn