Skip to content

Enable thunking #applyUnOp #595

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 7 commits into from
May 21, 2025
Merged

Conversation

ehildenb
Copy link
Member

@ehildenb ehildenb commented May 21, 2025

A couple of programs were getting stuck at #applyUnOp for unimplemented operations, this enables thunking unary operations. In particular:

  • #applyUnOp is put in sort Evaluation so that thunking can happen.
  • #compute is renamed to #applyBinOp.
  • The P-token test is limited to 7 iterations of the prover maximum to keep it from running too long (arbitrary limit, still takes about 10 minutes).
  • Test output is updated: there are 2 tests where the rename #compute => #applyBinOp has an effect, and 2 where we get further into execution of programs because we thunk up #applyUnOp (including the P-token test).

@ehildenb ehildenb self-assigned this May 21, 2025
Comment on lines +79 to +89
┃ ├─ 12
┃ │ #selectBlock ( switchTargets ( ... branches: .Branches , otherwise: basicBlockId
┃ │
┃ │ (85 steps)
┃ └─ 17 (vacuous, leaf)
┃ #expect ( typedValue ( BoolVal ( 0 <Int size ( ARG_ARRAY7:List ) ) , ty ( 28 ) ,
┗━━┓
└─ 13 (stuck, leaf)
#selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 7 ) )
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can see we're getting vacuous and stuck nodes (which are nonsensical), and that our #switchBlocks is not carrying through side-conditions correctly. That will have to be investigated in a further PR.

@ehildenb ehildenb marked this pull request as ready for review May 21, 2025 16:42
@ehildenb ehildenb requested review from dkcumming and jberthold May 21, 2025 16:42
@automergerpr-permission-manager automergerpr-permission-manager bot merged commit f69d23a into master May 21, 2025
6 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the thunk-unop branch May 21, 2025 17:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants