diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-03 20:12:42 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-03 20:12:42 +0100 |
| commit | 2d41078f6864c8138321e0c27440a8f93d815ea5 (patch) | |
| tree | 6e2420ef06266b05a113a89dfe4d05d3e38d0304 /kvx/Asmvliw.v | |
| parent | 48dc03004ba4078670b583561b108043085334b8 (diff) | |
| download | compcert-kvx-2d41078f6864c8138321e0c27440a8f93d815ea5.tar.gz compcert-kvx-2d41078f6864c8138321e0c27440a8f93d815ea5.zip | |
still issues with FR in kvx
Diffstat (limited to 'kvx/Asmvliw.v')
| -rw-r--r-- | kvx/Asmvliw.v | 42 |
1 files changed, 24 insertions, 18 deletions
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index 66b468d7..91d119bf 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -163,6 +163,30 @@ Module PregEq. Definition eq := preg_eq. End PregEq. +(* FIXME - R16 and R32 are excluded *) +Definition preg_of (r: mreg) : preg := + match r with + | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4 + | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9 + | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *) + | R15 => GPR15 (* | R16 => GPR16 *) | R17 => GPR17 | R18 => GPR18 | R19 => GPR19 + | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24 + | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29 + | R30 => GPR30 | R31 => GPR31 (* | R32 => GPR32 *) | R33 => GPR33 | R34 => GPR34 + | R35 => GPR35 | R36 => GPR36 | R37 => GPR37 | R38 => GPR38 | R39 => GPR39 + | R40 => GPR40 | R41 => GPR41 | R42 => GPR42 | R43 => GPR43 | R44 => GPR44 + | R45 => GPR45 | R46 => GPR46 | R47 => GPR47 | R48 => GPR48 | R49 => GPR49 + | R50 => GPR50 | R51 => GPR51 | R52 => GPR52 | R53 => GPR53 | R54 => GPR54 + | R55 => GPR55 | R56 => GPR56 | R57 => GPR57 | R58 => GPR58 | R59 => GPR59 + | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63 + end. + +Definition ireg_of (r: mreg) : res ireg := + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.ireg_of") end. + +Definition freg_of (r: mreg) : res freg := + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end. + Module Pregmap := EMap(PregEq). (** ** Conventional names for stack pointer ([SP]), return address ([RA]), frame pointer ([FP]) and other temporaries used *) @@ -1548,24 +1572,6 @@ Definition det_parexec (f: function) (bundle: bblock) (rs: regset) (m: mem) rs' code. *) -(* FIXME - R16 and R32 are excluded *) -Definition preg_of (r: mreg) : preg := - match r with - | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4 - | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9 - | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *) - | R15 => GPR15 (* | R16 => GPR16 *) | R17 => GPR17 | R18 => GPR18 | R19 => GPR19 - | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24 - | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29 - | R30 => GPR30 | R31 => GPR31 (* | R32 => GPR32 *) | R33 => GPR33 | R34 => GPR34 - | R35 => GPR35 | R36 => GPR36 | R37 => GPR37 | R38 => GPR38 | R39 => GPR39 - | R40 => GPR40 | R41 => GPR41 | R42 => GPR42 | R43 => GPR43 | R44 => GPR44 - | R45 => GPR45 | R46 => GPR46 | R47 => GPR47 | R48 => GPR48 | R49 => GPR49 - | R50 => GPR50 | R51 => GPR51 | R52 => GPR52 | R53 => GPR53 | R54 => GPR54 - | R55 => GPR55 | R56 => GPR56 | R57 => GPR57 | R58 => GPR58 | R59 => GPR59 - | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63 - end. - (** **** Undefine all registers except SP and callee-save registers *) Definition undef_caller_save_regs (rs: regset) : regset := |