diff options
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 97 |
1 files changed, 91 insertions, 6 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index b656789b..b341388c 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -85,7 +85,8 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]). *) Notation "'SP'" := GPR12 (only parsing) : asm. -Notation "'FP'" := GPR14 (only parsing) : asm. +Notation "'FP'" := GPR17 (only parsing) : asm. +Notation "'MFP'" := R17 (only parsing) : asm. Notation "'GPRA'" := GPR16 (only parsing) : asm. Notation "'RTMP'" := GPR32 (only parsing) : asm. @@ -338,8 +339,13 @@ Inductive arith_name_rrr : Type := | Psubw (**r sub word *) | Pmulw (**r mul word *) | Pandw (**r and word *) + | Pnandw (**r nand word *) | Porw (**r or word *) + | Pnorw (**r nor word *) | Pxorw (**r xor word *) + | Pnxorw (**r nxor word *) + | Pandnw (**r andn word *) + | Pornw (**r orn word *) | Psraw (**r shift right arithmetic word *) | Psrlw (**r shift right logical word *) | Psllw (**r shift left logical word *) @@ -347,8 +353,13 @@ Inductive arith_name_rrr : Type := | Paddl (**r add long *) | Psubl (**r sub long *) | Pandl (**r and long *) + | Pnandl (**r nand long *) | Porl (**r or long *) + | Pnorl (**r nor long *) | Pxorl (**r xor long *) + | Pnxorl (**r nxor long *) + | Pandnl (**r andn long *) + | Pornl (**r orn long *) | Pmull (**r mul long (low part) *) | Pslll (**r shift left logical long *) | Psrll (**r shift right logical long *) @@ -366,13 +377,19 @@ Inductive arith_name_rri32 : Type := | Pcompiw (it: itest) (**r comparison imm word *) | Paddiw (**r add imm word *) + | Pmuliw (**r add imm word *) | Pandiw (**r and imm word *) + | Pnandiw (**r nand imm word *) | Poriw (**r or imm word *) + | Pnoriw (**r nor imm word *) | Pxoriw (**r xor imm word *) + | Pnxoriw (**r nxor imm word *) + | Pandniw (**r andn word *) + | Porniw (**r orn word *) | Psraiw (**r shift right arithmetic imm word *) | Psrliw (**r shift right logical imm word *) | Pslliw (**r shift left logical imm word *) - + | Proriw (**r rotate right imm word *) | Psllil (**r shift left logical immediate long *) | Psrlil (**r shift right logical immediate long *) | Psrail (**r shift right arithmetic immediate long *) @@ -381,9 +398,28 @@ Inductive arith_name_rri32 : Type := Inductive arith_name_rri64 : Type := | Pcompil (it: itest) (**r comparison imm long *) | Paddil (**r add immediate long *) + | Pmulil (**r mul immediate long *) | Pandil (**r and immediate long *) + | Pnandil (**r nand immediate long *) | Poril (**r or immediate long *) + | Pnoril (**r nor immediate long *) | Pxoril (**r xor immediate long *) + | Pnxoril (**r nxor immediate long *) + | Pandnil (**r andn immediate long *) + | Pornil (**r orn immediate long *) +. + +Inductive arith_name_arrr : Type := + | Pmaddw (**r multiply add word *) + | Pmaddl (**r multiply add long *) +. + +Inductive arith_name_arri32 : Type := + | Pmaddiw (**r multiply add word *) +. + +Inductive arith_name_arri64 : Type := + | Pmaddil (**r multiply add long *) . Inductive ar_instruction : Type := @@ -396,6 +432,9 @@ Inductive ar_instruction : Type := | PArithRRR (i: arith_name_rrr) (rd rs1 rs2: ireg) | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int) | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64) + | PArithARRR (i: arith_name_arrr) (rd rs1 rs2: ireg) + | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int) + | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64) . Coercion PArithR: arith_name_r >-> Funclass. @@ -407,6 +446,9 @@ Coercion PArithRF64: arith_name_rf64 >-> Funclass. Coercion PArithRRR: arith_name_rrr >-> Funclass. Coercion PArithRRI32: arith_name_rri32 >-> Funclass. Coercion PArithRRI64: arith_name_rri64 >-> Funclass. +Coercion PArithARRR: arith_name_arrr >-> Funclass. +Coercion PArithARRI32: arith_name_arri32 >-> Funclass. +Coercion PArithARRI64: arith_name_arri64 >-> Funclass. Inductive basic : Type := | PArith (i: ar_instruction) @@ -502,9 +544,8 @@ Proof. assert (b :: body = nil). eapply H; eauto. discriminate. - destruct body; destruct exit. all: simpl; auto; try constructor. - + exploreInst. + + exploreInst; try discriminate. simpl. contradiction. - discriminate. + intros. discriminate. Qed. @@ -1091,8 +1132,13 @@ Definition arith_eval_rrr n v1 v2 := | Psubw => Val.sub v1 v2 | Pmulw => Val.mul v1 v2 | Pandw => Val.and v1 v2 + | Pnandw => Val.notint (Val.and v1 v2) | Porw => Val.or v1 v2 + | Pnorw => Val.notint (Val.or v1 v2) | Pxorw => Val.xor v1 v2 + | Pnxorw => Val.notint (Val.xor v1 v2) + | Pandnw => Val.and (Val.notint v1) v2 + | Pornw => Val.or (Val.notint v1) v2 | Psrlw => Val.shru v1 v2 | Psraw => Val.shr v1 v2 | Psllw => Val.shl v1 v2 @@ -1100,8 +1146,13 @@ Definition arith_eval_rrr n v1 v2 := | Paddl => Val.addl v1 v2 | Psubl => Val.subl v1 v2 | Pandl => Val.andl v1 v2 + | Pnandl => Val.notl (Val.andl v1 v2) | Porl => Val.orl v1 v2 + | Pnorl => Val.notl (Val.orl v1 v2) | Pxorl => Val.xorl v1 v2 + | Pnxorl => Val.notl (Val.xorl v1 v2) + | Pandnl => Val.andl (Val.notl v1) v2 + | Pornl => Val.orl (Val.notl v1) v2 | Pmull => Val.mull v1 v2 | Pslll => Val.shll v1 v2 | Psrll => Val.shrlu v1 v2 @@ -1119,12 +1170,19 @@ Definition arith_eval_rri32 n v i := match n with | Pcompiw c => compare_int c v (Vint i) | Paddiw => Val.add v (Vint i) + | Pmuliw => Val.mul v (Vint i) | Pandiw => Val.and v (Vint i) + | Pnandiw => Val.notint (Val.and v (Vint i)) | Poriw => Val.or v (Vint i) + | Pnoriw => Val.notint (Val.or v (Vint i)) | Pxoriw => Val.xor v (Vint i) + | Pnxoriw => Val.notint (Val.xor v (Vint i)) + | Pandniw => Val.and (Val.notint v) (Vint i) + | Porniw => Val.or (Val.notint v) (Vint i) | Psraiw => Val.shr v (Vint i) | Psrliw => Val.shru v (Vint i) | Pslliw => Val.shl v (Vint i) + | Proriw => Val.ror v (Vint i) | Psllil => Val.shll v (Vint i) | Psrlil => Val.shrlu v (Vint i) | Psrail => Val.shrl v (Vint i) @@ -1134,11 +1192,33 @@ Definition arith_eval_rri64 n v i := match n with | Pcompil c => compare_long c v (Vlong i) | Paddil => Val.addl v (Vlong i) + | Pmulil => Val.mull v (Vlong i) | Pandil => Val.andl v (Vlong i) + | Pnandil => Val.notl (Val.andl v (Vlong i)) | Poril => Val.orl v (Vlong i) + | Pnoril => Val.notl (Val.orl v (Vlong i)) | Pxoril => Val.xorl v (Vlong i) + | Pnxoril => Val.notl (Val.xorl v (Vlong i)) + | Pandnil => Val.andl (Val.notl v) (Vlong i) + | Pornil => Val.orl (Val.notl v) (Vlong i) end. +Definition arith_eval_arrr n v1 v2 v3 := + match n with + | Pmaddw => Val.add v1 (Val.mul v2 v3) + | Pmaddl => Val.addl v1 (Val.mull v2 v3) + end. + +Definition arith_eval_arri32 n v1 v2 v3 := + match n with + | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3)) + end. + +Definition arith_eval_arri64 n v1 v2 v3 := + match n with + | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3)) + end. + Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | PArithR n d => rs#d <- (arith_eval_r n) @@ -1155,6 +1235,12 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i) | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i) + + | PArithARRR n d s1 s2 => rs#d <- (arith_eval_arrr n rs#d rs#s1 rs#s2) + + | PArithARRI32 n d s i => rs#d <- (arith_eval_arri32 n rs#d rs#s i) + + | PArithARRI64 n d s i => rs#d <- (arith_eval_arri64 n rs#d rs#s i) end. (** * load/store *) @@ -1395,7 +1481,6 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) | (None, _) => Stuck end - (** Pseudo-instructions *) | Pbuiltin ef args res => Stuck (**r treated specially below *) @@ -1420,7 +1505,7 @@ 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 + | 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 |