cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Make cutsets smaller in DataLang

Open myreen opened this issue 6 months ago • 0 comments

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

myreen avatar Aug 09 '24 18:08 myreen