viper: associate the first exhale with the async expression
#3524
Conversation
src/viper/trans.ml
Outdated
| !!(SeqnS ( | ||
| let (!!) p = !!! at p in | ||
| !!([], | ||
| !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)), |
There was a problem hiding this comment.
This is the relevant change, sorry for the other noise...
| (self ctxt Source.no_region, !!id), | ||
| (!!(AddE(!!(FldAcc (self ctxt (s.at), !!id)), | ||
| intLitE Source.no_region 1))))); | ||
| !@(ExhaleS (!@(AndE(!@(MacroCall("$Perm", self ctxt at)), |
There was a problem hiding this comment.
This is the relevant change, sorry for the other noise...
There was a problem hiding this comment.
!! still marks up the await, but !@ points at the async.
There was a problem hiding this comment.
Right but doesn't the exhale belong to the await, not the async? This is when you need to establish the invariant before suspending. That was my thinking at least. But I don't know why it doesn't highlight the await rather than default to the unknow region.
There was a problem hiding this comment.
I think the exhale is due to the async being filed into the continuation table. But you are right, that only the await opens up the context switch so that a havoc can occur. I.e. a totally unrelated async could be it too.
| (self ctxt at, !@id), | ||
| (!@(SubE(!@(FldAcc (self ctxt at, !@id)), | ||
| intLitE at 1))))); | ||
| !!! (e.at) (SeqnS stmts); |
There was a problem hiding this comment.
Is this maybe confusing things and should really be !@
Not needed for the demo and I won't merge right now. This can wait. |
ggreif
added
automerge-squash
This changes the srcloc of certain Viper subexpression to better track the original Motoko.