diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-11-16 10:06:56 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-11-16 10:06:56 +0100 |
commit | 17f236ede68a56f7a007d61d569f841f4cf0fd8b (patch) | |
tree | 9956654dd9f7690b28e6ba275f7d3470d529d894 /arm/Asm.v | |
parent | 09ee4a28f7c87b0f1e9ade86ac4c6bfa860af12d (diff) | |
download | compcert-17f236ede68a56f7a007d61d569f841f4cf0fd8b.tar.gz compcert-17f236ede68a56f7a007d61d569f841f4cf0fd8b.zip |
Moved arm eabi fixup to Asmexpand.
Instead of expanding the fixup code for incoming and outgoing
registers in the TargetPrinter we expand them in Asmexpand. This
simplifies the estimate size function and is a prerequisite for
the json export.
Bug 22472
Diffstat (limited to 'arm/Asm.v')
-rw-r--r-- | arm/Asm.v | 27 |
1 files changed, 25 insertions, 2 deletions
@@ -43,6 +43,16 @@ Inductive freg: Type := | FR8: freg | FR9: freg | FR10: freg | FR11: freg | FR12: freg | FR13: freg | FR14: freg | FR15: freg. +Inductive sreg: Type := + | SR0: sreg | SR1: sreg | SR2: sreg | SR3: sreg + | SR4: sreg | SR5: sreg | SR6: sreg | SR7: sreg + | SR8: sreg | SR9: sreg | SR10: sreg | SR11: sreg + | SR12: sreg | SR13: sreg | SR14: sreg | SR15: sreg + | SR16: sreg | SR17: sreg | SR18: sreg | SR19: sreg + | SR20: sreg | SR21: sreg | SR22: sreg | SR23: sreg + | SR24: sreg | SR25: sreg | SR26: sreg | SR27: sreg + | SR28: sreg | SR29: sreg | SR30: sreg | SR31: sreg. + Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. @@ -228,8 +238,15 @@ Inductive instruction : Type := | Pldrh_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int16 load with post increment *) | Pstr_p: ireg -> ireg -> shift_op -> instruction (**r int32 store with post increment *) | Pstrb_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int8 store with post increment *) - | Pstrh_p: ireg -> ireg -> shift_op -> instruction. (**r unsigned int16 store with post increment *) + | Pstrh_p: ireg -> ireg -> shift_op -> instruction (**r unsigned int16 store with post increment *) + (* Instructions for fixup of calling conventions *) + | Pfcpy_fs: freg -> sreg -> instruction (**r single precision float move for incoming arguments *) + | Pfcpy_sf: sreg -> freg -> instruction (**r single precision float move for outgoing arguments *) + | Pfcpy_fii: freg -> ireg -> ireg -> instruction (**r copy integer register pair to double fp-register *) + | Pfcpy_fi: freg -> ireg -> instruction (**r copy integer register to single fp-register *) + | Pfcpy_iif: ireg -> ireg -> freg -> instruction (**r copy double fp-register to integer register pair *) + | Pfcpy_if: ireg -> freg -> instruction. (**r copy single fp-register to integer register *) (** The pseudo-instructions are the following: @@ -784,7 +801,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pldrh_p _ _ _ | Pstr_p _ _ _ | Pstrb_p _ _ _ - | Pstrh_p _ _ _ => + | Pstrh_p _ _ _ + | Pfcpy_fs _ _ + | Pfcpy_sf _ _ + | Pfcpy_fii _ _ _ + | Pfcpy_fi _ _ + | Pfcpy_iif _ _ _ + | Pfcpy_if _ _ => Stuck end. |