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 | |
parent | 48dc03004ba4078670b583561b108043085334b8 (diff) | |
download | compcert-kvx-2d41078f6864c8138321e0c27440a8f93d815ea5.tar.gz compcert-kvx-2d41078f6864c8138321e0c27440a8f93d815ea5.zip |
still issues with FR in kvx
Diffstat (limited to 'kvx')
-rw-r--r-- | kvx/Asm.v | 3 | ||||
-rw-r--r-- | kvx/Asmblockgen.v | 8 | ||||
-rw-r--r-- | kvx/Asmvliw.v | 42 |
3 files changed, 26 insertions, 27 deletions
@@ -35,13 +35,12 @@ Require Import Smallstep. Require Import Locations. Require Stacklayout. Require Import Conventions. -Require Import Asmvliw. +Require Export Asmvliw. Require Import Linking. Require Import Errors. (** Definitions for OCaml code *) Definition label := positive. -Definition preg := preg. Inductive addressing : Type := | AOff (ofs: offset) diff --git a/kvx/Asmblockgen.v b/kvx/Asmblockgen.v index 7167cebe..e218f4ef 100644 --- a/kvx/Asmblockgen.v +++ b/kvx/Asmblockgen.v @@ -19,7 +19,7 @@ Require Archi. Require Import Coqlib Errors. Require Import AST Integers Floats Memdata. -Require Import Op Locations Machblock Asmblock. +Require Import Op Locations Machblock Asmvliw Asmblock. Require ExtValues. Require Import Chunks. @@ -36,12 +36,6 @@ Import PArithCoercions. (** Extracting integer or float registers. *) -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. - Inductive immed32 : Type := | Imm32_single (imm: int). 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 := |