search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
964 stars 84 forks source link

Relax instruction conventions in word_alloc #1036

Open tanyongkiam opened 3 months ago

tanyongkiam commented 3 months ago

The SSA pass currently forces the allocator to use fixed registers for instructions like LongMul following the requirements of x64.

It should be relaxed.

tanyongkiam commented 1 week ago

After some initial experimentation, I decided not to implement this for now.

It is not too difficult to add this in wordLang (every relevant pass gains a flag to control its behavior on LongMul).

However, word-to-stack for LongMul appears significantly more complicated because one needs to respect the register conventions even when some of the arguments are spilled.

tanyongkiam commented 1 week ago

In https://github.com/CakeML/cakeml/blob/master/compiler/backend/semantics/wordPropsScript.sml#L3309

Some of the restrictions for inst_ok_less can be simplified (if we assume that inst_arg_convention gets forced by SSA)