search

dafny-lang / dafny-reportgenerator

A tool for analyzing and reporting on Dafny, especially the results of verification
MIT License
3 stars 4 forks source link

Support per-assertion batch maximum bounds #18

Open robin-aws opened 1 year ago

robin-aws commented 1 year ago

It's common to have just a few assertion batches in a code base that are far more expensive/highly variable, and it would be much better to only raise the bounds on individual batches when you have to rather than raising them across all batches.

This is getting a bit complicated to specify on the CLI and we may want to find a way of adding it to the project file instead: https://github.com/dafny-lang/dafny/pull/3851

keyboardDrummer commented 1 year ago

Shouldn't it be specified in-code, where the batch is defined?

seebees commented 1 year ago

Just came to request this. Yes, in code would be great too!

robin-aws commented 1 year ago

There's a bit of a UX challenge to think through here: I'm not sure how to identify assertion batches in general, and/or robustly attach an attribute (for example) to an assertion batch. Even something like {:max-resource-count} on a method is ambiguous in the default encoding: does it refer to the well-formedness assertion batch or the implementation batch? And if splitting is used, can we somehow specify the limit on "batch 11/24"?

keyboardDrummer commented 1 year ago

I'm not sure how to identify assertion batches in general

I suggest changing the language so most batches have to be named. I think better than assert {:split_here} true would be [split] label <BatchName>:. For the the WF vs IMPL problem, I suggest adding an optional boolean to the annotation that tweaks the batch. For working with {:split_on_every_assert}, you could allow annotating the assertions.

Btw, when you introduce splits, do you always get an extra WF and IMPL batch per split section, or are you only splitting the IMPL part and does the WF part stay one big batch?

atomb commented 1 year ago

One thing I could imagine, and maybe @keyboardDrummer drummer is also suggesting this above, would be to allow a maximum resource count to be attached to an assertion, and that would then apply to every assertion in the same batch.

keyboardDrummer commented 1 year ago

One thing I could imagine, and maybe @keyboardDrummer drummer is also suggesting this above, would be to allow a maximum resource count to be attached to an assertion, and that would then apply to every assertion in the same batch.

I think if you attach it to an assertion, that assertion should be in its own singleton batch.