[CN-exec] Runtime loop invariants

[rbanerjee20]

Implementation of runtime loop invariant checking within Fulminate

[bcpierce00]

Question about defaults: If I run with instrumentation on a file with no annotations, will I get dinged for missing loop invariants? I know there was some discussion about this a while back, but I'm not sure where we settled. (FWIW, I think it's better for loop invariant checking to be off by default, to provide a smoother onramp for new users, testing tutorial readers, etc.)

[cp526]

Question about defaults: If I run with instrumentation on a file with no annotations, will I get dinged for missing loop invariants? I know there was some discussion about this a while back, but I'm not sure where we settled. (FWIW, I think it's better for loop invariant checking to be off by default, to provide a smoother onramp for new users, testing tutorial readers, etc.)

Agreed. Ideally the specifying of a loop invariant itself is what turns the invariant checking on locally, just for that invariant.

[bcpierce00]

Yes, that’s even better than a global default.

…

On Fri, Feb 21, 2025 at 5:23 PM Christopher Pulte ***@***.***> wrote: Question about defaults: If I run with instrumentation on a file with no annotations, will I get dinged for missing loop invariants? I know there was some discussion about this a while back, but I'm not sure where we settled. (FWIW, I think it's better for loop invariant checking to be off by default, to provide a smoother onramp for new users, testing tutorial readers, etc.) Agreed. Ideally the specifying of a loop invariant itself is what turns the invariant checking on locally, just for that invariant. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/pull/884*issuecomment-2675740373__;Iw!!IBzWLUs!Q1JjlteNFI8d03bwkThB5KJIEM1ehpbEDmO94rrIwerEMj-lSA51fgfZqlaImhYn_QLKFeKJOKQWW-9SSiMdF43Swlb7$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC4LPEBGVA6C2ZZKHWT2Q6ROHAVCNFSM6AAAAABXTOZZAWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMNZVG42DAMZXGM__;!!IBzWLUs!Q1JjlteNFI8d03bwkThB5KJIEM1ehpbEDmO94rrIwerEMj-lSA51fgfZqlaImhYn_QLKFeKJOKQWW-9SSiMdF4BzAzhU$> . You are receiving this because you commented.Message ID: ***@***.***> [image: cp526]*cp526* left a comment (rems-project/cerberus#884) <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/pull/884*issuecomment-2675740373__;Iw!!IBzWLUs!Q1JjlteNFI8d03bwkThB5KJIEM1ehpbEDmO94rrIwerEMj-lSA51fgfZqlaImhYn_QLKFeKJOKQWW-9SSiMdF43Swlb7$> Question about defaults: If I run with instrumentation on a file with no annotations, will I get dinged for missing loop invariants? I know there was some discussion about this a while back, but I'm not sure where we settled. (FWIW, I think it's better for loop invariant checking to be off by default, to provide a smoother onramp for new users, testing tutorial readers, etc.) Agreed. Ideally the specifying of a loop invariant itself is what turns the invariant checking on locally, just for that invariant. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/rems-project/cerberus/pull/884*issuecomment-2675740373__;Iw!!IBzWLUs!Q1JjlteNFI8d03bwkThB5KJIEM1ehpbEDmO94rrIwerEMj-lSA51fgfZqlaImhYn_QLKFeKJOKQWW-9SSiMdF43Swlb7$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC4LPEBGVA6C2ZZKHWT2Q6ROHAVCNFSM6AAAAABXTOZZAWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDMNZVG42DAMZXGM__;!!IBzWLUs!Q1JjlteNFI8d03bwkThB5KJIEM1ehpbEDmO94rrIwerEMj-lSA51fgfZqlaImhYn_QLKFeKJOKQWW-9SSiMdF4BzAzhU$> . You are receiving this because you commented.Message ID: ***@***.***>

[rbanerjee20]

Thanks @bcpierce00 @cp526 for your comments. I've now added some functionality for keeping track of whether the user has provided any CN loop spec. If they have, the loop gets instrumented with runtime checks; otherwise, no checks get inserted. Previously, the statements that CN generates internally whenever it sees a loop were also being translated and inserted by Fulminate. I agree that it doesn't make sense to make the output verbose with these checks if the user has not written any spec for their loop.

@cp526 if you could take a look at this commit this set of commits, that would be good, as I made a small change to Mucore.Label and had to propagate this throughout the CN codebase. If there is some better/easier way of keeping track of whether the user has provided any loop annotations, please let me know.