Hotfix pass singleton tuples as single elements to closures

[jberthold]

No description provided.

[Stevengre]

What about removing this expected file, since it's already reached the #EndProgram.

[jberthold]

I think it does not hurt to keep it.

[Stevengre]

I'd like to use prove-rs folder even for concrete testing. Because it only has one file to be added and one test to be ran. exec-smir eliminates the smir.json generation process, but have to execute both llvm and haskell backend.

[jberthold]

All exec_smir tests EDIT: The exec_smir tests that run without step limit
are also run as proofs to prove termination. I thought it is an advantage to run the test in more than one way.

[Stevengre]

Agreed, just think it's a little bit annoying of these file changes (smir.json, .state, test_integration). Additionally, to my experience, the .state only different when there are some issues in the semantics.

[dkcumming]

I agree with you @Stevengre and I raised it before and @ehildenb and @jberthold convinced my it was safer to have a dump some intermediate state to compare against. It isn't much more overhead to update with the make commands, and it could potentially uncover a bug in our process if we have unexpected diffs in that intermediate state but the proof itself still passes.

[jberthold]

When testing this with p-token, I found that the recognition of closures is still not complete.
Will try to make another test program that has the same characteristics as the load_mut function closure.

[dkcumming]

I looked at this with close account, and I do see more branching so I believe this is working. Is this meant to remove thunks that we were seeing in p-token, if so which ones? Maybe it would be good to add a description (even if brief) before merging so if we look back we can see what this is in relation to before needing to read the code changes.

[jberthold]

I looked at this with close account, and I do see more branching so I believe this is working. Is this meant to remove thunks that we were seeing in p-token, if so which ones? Maybe it would be good to add a description (even if brief) before merging so if we look back we can see what this is in relation to before needing to read the code changes.

Definitely working because the test programs will execute wrongly without the new K code.
What I don't understand is how the information about the calling convention does not get into Stable MIR JSON for the programs. The spread_arg flag should just be set for all closures. I'll check stable-mir-json about this.

Will extend the documenting text and mention that flag before I merge.