Optimize dt without or patterns

runtimeverification / mx-semantics

6 stars 1 forks source link

Optimize dt without or patterns #267

Closed bbyalcinkaya closed 1 month ago

bbyalcinkaya commented 1 month ago

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.

Target	Before #265	After #265	After
llvm-mandos	474 MB	195 MB	252 MB
llvm-kasmer	566 MB	231 MB	301 MB

In general, the semantics were refactored by:

duplicating short and simple rules (rules with label *-instrs-empty / *-instrs-wait)
converting rules that operate by converting one command into multiple commands into functions or macros.

Baltoli commented 1 month ago

I'm working on a change to the frontend that will desugar #Or patterns on the LHS of rules, so perhaps let's see if that works before reverting to this PR.

ehildenb commented 1 month ago

@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.

bbyalcinkaya commented 1 month ago

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

Baltoli commented 1 month ago

Yep, seems sensible to me!