cakeml
cakeml copied to clipboard
Make cutsets smaller in DataLang
@tanyongkiam noticed that cutsets are sometimes too large.
For example, the explorer output reveals:
(seq
...
(6 := Mult (5 4) (some {4,5}))
(return 6))
Here 4 and 5 are in the cutset ({4,5}
) only because they are used as arguments to Mult
. Ideally, the cutset should be empty because 4 and 5 are not used afterMult
.
The reason they are in the cutset can be seen in the semantics of DataLang, here:
https://github.com/CakeML/cakeml/blob/48a421d7a393f35b150221d8dec6d3caca9befe6/compiler/backend/semantics/dataSemScript.sml#L1146-L1153
This needs to be corrected so that the arguments are read (get_vars
) before the cutset is applied (cut_state_opt
). With this change data_live
can make the cutsets smaller. The data_to_word
proofs need updating.