diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 21:58:47 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 21:58:47 +0200 |
| commit | 5d09dd8f3194ecc90137178d6b5d18b9ad31aabf (patch) | |
| tree | ff75ed576da62990e3dd3521204d2f45b1fe55b4 /mppa_k1c/Asmvliw.v | |
| parent | 56ab9fea6dc937dac56e883a64f06cae3c931551 (diff) | |
| download | compcert-kvx-5d09dd8f3194ecc90137178d6b5d18b9ad31aabf.tar.gz compcert-kvx-5d09dd8f3194ecc90137178d6b5d18b9ad31aabf.zip | |
find consecutive writes
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index e460727c..0cbe27e1 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -66,12 +66,63 @@ Inductive gpreg: Type := Definition ireg := gpreg. Definition freg := gpreg. +Lemma gpreg_eq: forall (x y: gpreg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. Proof. decide equality. Defined. +Inductive gpreg_q : Type := +| R0R1 | R2R3 | R4R5 | R6R7 | R8R9 +| R10R11 | R12R13 | R14R15 | R16R17 | R18R19 +| R20R21 | R22R23 | R24R25 | R26R27 | R28R29 +| R30R31 | R32R33 | R34R35 | R36R37 | R38R39 +| R40R41 | R42R43 | R44R45 | R46R47 | R48R49 +| R50R51 | R52R53 | R54R55 | R56R57 | R58R59 +| R60R61 | R62R63. + +Lemma gpreg_q_eq : forall (x y : gpreg_q), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Definition gpreg_q_expand (x : gpreg_q) : gpreg * gpreg := + match x with + | R0R1 => (GPR0, GPR1) + | R2R3 => (GPR2, GPR3) + | R4R5 => (GPR4, GPR5) + | R6R7 => (GPR6, GPR7) + | R8R9 => (GPR8, GPR9) + | R10R11 => (GPR10, GPR11) + | R12R13 => (GPR12, GPR13) + | R14R15 => (GPR14, GPR15) + | R16R17 => (GPR16, GPR17) + | R18R19 => (GPR18, GPR19) + | R20R21 => (GPR20, GPR21) + | R22R23 => (GPR22, GPR23) + | R24R25 => (GPR24, GPR25) + | R26R27 => (GPR26, GPR27) + | R28R29 => (GPR28, GPR29) + | R30R31 => (GPR30, GPR31) + | R32R33 => (GPR32, GPR33) + | R34R35 => (GPR34, GPR35) + | R36R37 => (GPR36, GPR37) + | R38R39 => (GPR38, GPR39) + | R40R41 => (GPR40, GPR41) + | R42R43 => (GPR42, GPR43) + | R44R45 => (GPR44, GPR45) + | R46R47 => (GPR46, GPR47) + | R48R49 => (GPR48, GPR49) + | R50R51 => (GPR50, GPR51) + | R52R53 => (GPR52, GPR53) + | R54R55 => (GPR54, GPR55) + | R56R57 => (GPR56, GPR57) + | R58R59 => (GPR58, GPR59) + | R60R61 => (GPR60, GPR61) + | R62R63 => (GPR62, GPR63) + end. + (** We model the following registers of the RISC-V architecture. *) (** basic register *) |