Give VerCors the capability to report under which branch conditions an error occurs

[pieter-bos]

Silicon can simply output this information with --enableBranchconditionReporting:

If you have suggestions on how to render this, that would be appreciated! I think you can fairly easily get to a somewhat large number of branch conditions, so that's a concern.

[bobismijnnaam]

Do you have some idea of translating this information back through the passes as well? That sounds particularly difficult. As a compromise, maybe we can label each branch condition with the type of origin. That could give some indication of its meaning (given that we've been diligent with origins... Hmmm.)

For unprocessed presentation, I think presenting them as a list together with the failed assertion would be nice, though only when activated by a flag. One thing we can maybe improve is split individual path conditions over &&/** as well. So if you have a path condition a && b, this would become a \n b, or something. Maybe we want to indent theses "sub-pathconditions"?

If you want a very pretty way of presenting it to the user, or give the user the option to compress some part of the branch condition but not others, perhaps you can generate HTML and use the trick for collapsible CSS trees in this article: https://iamkate.com/code/tree-views/

EDIT: This information would also be helpful on assertions where we time out! To be clear, I would already be happy with a plaintext dump split on top-level conjuction-like operators :) (Or you could use unicode characters for fancy printing :))

[pieter-bos]

Do you have some idea of translating this information back through the passes as well? That sounds particularly difficult. As a compromise, maybe we can label each branch condition with the type of origin. That could give some indication of its meaning (given that we've been diligent with origins... Hmmm.)

I guess on an abstraction level branch conditions should really be part of the blame somehow? But then again branch conditions have almost nothing to do with concrete errors. I think origins are at least a fair approximation of how the branch condition came to be (though maybe I would prefer it if it pointed to the statement / other node that actually caused the branch as well).

For unprocessed presentation, I think presenting them as a list together with the failed assertion would be nice, though only when activated by a flag. One thing we can maybe improve is split individual path conditions over &&/** as well. So if you have a path condition a && b, this would become a \n b, or something. Maybe we want to indent theses "sub-pathconditions"?

Probably we should only output this information with a flag regardless, since it's in some sense a poor approximation of a counterexample. Splitting out is indeed probably a good idea when outputting silicon-level

If you want a very pretty way of presenting it to the user, or give the user the option to compress some part of the branch condition but not others, perhaps you can generate HTML and use the trick for collapsible CSS trees in this article: https://iamkate.com/code/tree-views/

I don't really get that? The list of branch conditions is fairly flat...

EDIT: This information would also be helpful on assertions where we time out! To be clear, I would already be happy with a plaintext dump split on top-level conjuction-like operators :) (Or you could use unicode characters for fancy printing :))

If you don't get the silicon-level branch conditions for time-outing assertions, please let me know! That should already work via the symbexlogger.

[pieter-bos]

I think the optimal solution is to have an indication in the gutter, where e.g. active branches are green, and ignored paths are grayed out (something to that effect). We can figure out some type of highlighting thing for inline branches (ternaries and whatnot). Obviously we would first need some kind of IDE...

[pieter-bos]

From the meeting:

• We could do external output, but that's probably a bit too interrupting
• Colors / inline icons could be a nice way to indicate whether a branch is active/inactive
• We could try to make it so messages in origin contexts are mergeable when the lines overlap (though they might become unordered)