[Bug] vector destructors are usually not called

[brson]

Per https://github.com/solana-labs/move/pull/147, the runtime move_rt_vec_destroy function is supposed to be called when vectors are destroyed, but it usually is not. I expect the stackless bytecode to contain an Operation::Destroy for all vectors going out of scope, but that does not seem to be true.

I have only seen the destroy operation emitted for vectors that have been created, but have not been used afterward. Once a vector is used, the destroy operation seems to always be omitted. There is something about how move wants to destroy vectors that I don't understand.

[nvjle]

In the stackless bytecode translation, Destroy is only induced by a Pop (which would match the behavior you observe). I'm not entirely sure, but it appears that livevar_analysis.rs may be the pass responsible for inserting Destroy at the end of each lifetime. As a simple first exercise, perhaps we could try running the standard move-prover pipeline which includes that and other analyses/transformations. I don't think that is happening today.

Another cheap trick would be to just insert Destroy (or IR equivalent) at the end of the function scope containing them (before each return, say)-- certainly the scopes will end there at the very latest.

[ksolana]

Perhaps move is banking on the 'linear type'? And that move-prover has already ensured that the there is no strict need to destroy opportunistically? We should create an issue in https://github.com/move-language/move to clarify this.

[brson]

Ah that is probably the case that the language directly understands push and pop and knows when a vec is empty - the naming of the vector::destroy_empty function does imply that only empty vecs can be destroyed, but I didn't imagine there was any analysis involved.

I hope this is a static analysis and doesn't require any runtime book-keeping. If it is completely static that seems quite sophisticated.

I'll prefer to land the current PR before trying to tackle this.

[nvjle]

Ah that is probably the case that the language directly understands push and pop and knows when a vec is empty - the naming of the vector::destroy_empty function does imply that only empty vecs can be destroyed, but I didn't imagine there was any analysis involved.

I hope this is a static analysis and doesn't require any runtime book-keeping. If it is completely static that seems quite sophisticated.

I'll prefer to land the current PR before trying to tackle this.

Yes, it is a static analysis, but it doesn't appear that we have to write it-- the code already exists (even if cheap trick #2 didn't pan out). In any case, landing the current PR makes sense before worrying about tackling this issue.