Arm instructions for long multiplication

[Slukoo]

Added UMLAL, SMULL, SMLAL, SMMUL & SMMULR instructions.

[bgregoir]

I thank a lot for this PR.
I have a small general remark:
it seems that you frequently use the same sequence of code:
let lo := zero_extend U32 res in
let hi := zero_extend U32 (wshr res 32) in
Can you introduce some intermediate function to do that (in word.v)
Maybe it can be implemented using other pattern (split_word? I do not remember the name).

A more problematic remark:

I think that the semantic of the instructions are wrong.
Most of then should compute (x * y + (u : v))
The general pattern you use in
(l,h) = x * y
(u+l, h + v)
I think this is incorrect because the carry that can occurs in u + l is not propagated to the high part.

[Slukoo]

Thank you for your help, I tried addressing the issues you were pointing out. Please tell me if there are still some things to improve/correct

[bgregoir]

thank for all the changes. I think it is ok now.