Abstract syntax for KVX textual assembly language.
Each emittable instruction is defined here. ';;' is also defined as an instruction.
The goal of this representation is to stay compatible with the rest of the generic backend of CompCert
We define unfold : listbblock -> listinstruction
An Asm function is then defined as : fn_sig, fn_blocks, fn_code, and a proof of unfoldfn_blocks = fn_codefn_code has no semantic. Instead, the semantic of Asm is given by using the AsmVLIW semantic on fn_blocks
| Pmv (rdrs: ireg) (* register move *)
| Pnegw (rdrs: ireg) (* negate word *)
| Pnegl (rdrs: ireg) (* negate long *)
| Pcvtl2w (rdrs: ireg) (* Convert Long to Word *)
| Psxwd (rdrs: ireg) (* Sign Extend Word to Double Word *)
| Pzxwd (rdrs: ireg) (* Zero Extend Word to Double Word *)