Optimize dt without or patterns #267
Conversation
|
I'm working on a change to the frontend that will desugar |
|
@bbyalcinkaya we should also test this with mx-backend to see if it works there before merging. No point merging something that won't work there. @Baltoli same goes for whatever frontend fix we get. |
|
I tested this with mx-backend and it passes all the existing tests. I think we can merge this to avoid blocking mx-backend from receiving further updates. Also, there is a possibility that the desugaring may not work well with cut point rules in mx-backend. (runtimeverification/k#4363) cc: @Baltoli |
|
Yep, seems sensible to me! |
virgil-serbanuta
left a comment
virgil-serbanuta
left a comment
There was a problem hiding this comment.
I had some minor comments. I'll approve, but please read them before merging.
| syntax ThrowException ::= #throwException( ExceptionCode , String ) | ||
| syntax ThrowException ::= #throwException( ExceptionCode , String ) [macro] | ||
| | #throwExceptionBs( ExceptionCode , Bytes ) |
There was a problem hiding this comment.
I see that you removed these constructors from many places. Are they still used?
There was a problem hiding this comment.
#throwException was used both as an instruction and a command. I replaced #throwExceptions in the <commands> cell with #exception. Now #throwException is only used in <instrs> and #exception is used in <commands>.
| <vmOutput> _ => .VMOutput </vmOutput> | ||
| <logging> S => S +String " -- callContract " +String #parseWasmString(FUNCNAME) </logging> | ||
| <instrs> (#waitCommands ~> _) #Or .K </instrs> | ||
| <instrs> .K </instrs> |
There was a problem hiding this comment.
Just making sure: when calling callContractAux, the instrs cell is always empty, right?
There was a problem hiding this comment.
Yes, <instrs> is emptied in callContract => resetCallState.
| => transferESDTsAux(FROM, TO, L) | ||
| ~> appendToOutAccount(TO, OutputTransfer(FROM, L)) | ||
| rule transferESDTsAux(FROM, TO, ListItem(T) Ts) |
There was a problem hiding this comment.
I'm always a bit nervous about having owise rules when extra conditions may be added implicitly by k to the non-owise rules. This does not happen here, but, e.g., if transferESDT would take a subsort of Bytes as the first argument (this does not exist, but let's assume it does for this example), then the owise rule would not handle only the empty list case, as intended, but also the case when FROM is bytes, but not that subsort.
In this case, it is feasible to check that the owise case does, indeed, behave as expected, but I think that the code would be easier to follow if you either add sorts to the FROM and TO variables, or you write the rule below with an actual empty list instead of an owise attribute.
| // <instrs> (#waitCommands ~> _) #Or .K </instrs> | ||
| [priority(61)] | ||
| rule [addToESDTBalance-new-err]: |
There was a problem hiding this comment.
If any of these rule names that you change are on one of these lists, please update them in a follow-up PR:
https://github.com/runtimeverification/mx-backend/blob/master/kmxwasm/src/kmxwasm/property_testing/running.py#L35-L71
bbyalcinkaya
force-pushed
the
optimize-without-or
branch
from
74011b7 to
2fbc1fa
Compare
Booster backend does not support or patterns. This PR aims to remove the occurrences of or patterns introduced in PR #265 while keeping the decision tree reasonably small.
In general, the semantics were refactored by:
*-instrs-empty / *-instrs-wait)