tlaplus
IOSerialize and IODeserialize testing wrt. unseen string problem
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.
