From 47a4ccade6f73e95be34cd2d55be3655302fff97 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 21 Mar 2019 20:29:57 +0100 Subject: begin jumptables (does not work) --- mppa_k1c/Asm.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'mppa_k1c/Asm.v') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 493f4a05..8c918c2d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -69,6 +69,7 @@ Inductive instruction : Type := | Pj_l (l: label) (**r jump to label *) | Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *) | Pcbu (bt: btest) (r: ireg) (l: label) (**r branch based on btest with unsigned semantics *) + | Pjumptable (r: ireg) (labels: list label) | Ploopdo (count: ireg) (loopend: label) (** Loads **) @@ -228,6 +229,7 @@ Definition control_to_instruction (c: control) := | PCtlFlow (Asmblock.Pj_l l) => Pj_l l | PCtlFlow (Asmblock.Pcb bt r l) => Pcb bt r l | PCtlFlow (Asmblock.Pcbu bt r l) => Pcbu bt r l + | PCtlFlow (Asmblock.Pjumptable r label) => Pjumptable r label end. Definition basic_to_instruction (b: basic) := -- cgit From 4adb0af96c3c0523438e86275f9e23ffdc69e4ba Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 2 Apr 2019 17:37:09 +0200 Subject: Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet --- mppa_k1c/Asm.v | 97 ++++++++++++++++++++++++++++++++++++---------------------- 1 file changed, 61 insertions(+), 36 deletions(-) (limited to 'mppa_k1c/Asm.v') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 2d708b79..115c8d6d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -38,6 +38,11 @@ Require Import Errors. Definition label := positive. Definition preg := preg. +Inductive addressing : Type := + | AOff (ofs: offset) + | AReg (ro: ireg) +. + (** Syntax *) Inductive instruction : Type := (** pseudo instructions *) @@ -70,26 +75,26 @@ Inductive instruction : Type := | Ploopdo (count: ireg) (loopend: label) (** Loads **) - | Plb (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte *) - | Plbu (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte unsigned *) - | Plh (rd: ireg) (ra: ireg) (ofs: offset) (**r load half word *) - | Plhu (rd: ireg) (ra: ireg) (ofs: offset) (**r load half word unsigned *) - | Plw (rd: ireg) (ra: ireg) (ofs: offset) (**r load int32 *) - | Plw_a (rd: ireg) (ra: ireg) (ofs: offset) (**r load any32 *) - | Pld (rd: ireg) (ra: ireg) (ofs: offset) (**r load int64 *) - | Pld_a (rd: ireg) (ra: ireg) (ofs: offset) (**r load any64 *) - | Pfls (rd: freg) (ra: ireg) (ofs: offset) (**r load float *) - | Pfld (rd: freg) (ra: ireg) (ofs: offset) (**r load 64-bit float *) + | Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *) + | Plbu (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte unsigned *) + | Plh (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word *) + | Plhu (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word unsigned *) + | Plw (rd: ireg) (ra: ireg) (ofs: addressing) (**r load int32 *) + | Plw_a (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any32 *) + | Pld (rd: ireg) (ra: ireg) (ofs: addressing) (**r load int64 *) + | Pld_a (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any64 *) + | Pfls (rd: freg) (ra: ireg) (ofs: addressing) (**r load float *) + | Pfld (rd: freg) (ra: ireg) (ofs: addressing) (**r load 64-bit float *) (** Stores **) - | Psb (rs: ireg) (ra: ireg) (ofs: offset) (**r store byte *) - | Psh (rs: ireg) (ra: ireg) (ofs: offset) (**r store half byte *) - | Psw (rs: ireg) (ra: ireg) (ofs: offset) (**r store int32 *) - | Psw_a (rs: ireg) (ra: ireg) (ofs: offset) (**r store any32 *) - | Psd (rs: ireg) (ra: ireg) (ofs: offset) (**r store int64 *) - | Psd_a (rs: ireg) (ra: ireg) (ofs: offset) (**r store any64 *) - | Pfss (rs: freg) (ra: ireg) (ofs: offset) (**r store float *) - | Pfsd (rd: freg) (ra: ireg) (ofs: offset) (**r store 64-bit float *) + | Psb (rs: ireg) (ra: ireg) (ofs: addressing) (**r store byte *) + | Psh (rs: ireg) (ra: ireg) (ofs: addressing) (**r store half byte *) + | Psw (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int32 *) + | Psw_a (rs: ireg) (ra: ireg) (ofs: addressing) (**r store any32 *) + | Psd (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int64 *) + | Psd_a (rs: ireg) (ra: ireg) (ofs: addressing) (**r store any64 *) + | Pfss (rs: freg) (ra: ireg) (ofs: addressing) (**r store float *) + | Pfsd (rd: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *) (** Arith RR *) | Pmv (rd rs: ireg) (**r register move *) @@ -364,26 +369,46 @@ Definition basic_to_instruction (b: basic) := | PArithARRI64 Asmblock.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm (** Load *) - | PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra ofs - | PLoadRRO Asmblock.Plbu rd ra ofs => Plbu rd ra ofs - | PLoadRRO Asmblock.Plh rd ra ofs => Plh rd ra ofs - | PLoadRRO Asmblock.Plhu rd ra ofs => Plhu rd ra ofs - | PLoadRRO Asmblock.Plw rd ra ofs => Plw rd ra ofs - | PLoadRRO Asmblock.Plw_a rd ra ofs => Plw_a rd ra ofs - | PLoadRRO Asmblock.Pld rd ra ofs => Pld rd ra ofs - | PLoadRRO Asmblock.Pld_a rd ra ofs => Pld_a rd ra ofs - | PLoadRRO Asmblock.Pfls rd ra ofs => Pfls rd ra ofs - | PLoadRRO Asmblock.Pfld rd ra ofs => Pfld rd ra ofs + | PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra (AOff ofs) + | PLoadRRO Asmblock.Plbu rd ra ofs => Plbu rd ra (AOff ofs) + | PLoadRRO Asmblock.Plh rd ra ofs => Plh rd ra (AOff ofs) + | PLoadRRO Asmblock.Plhu rd ra ofs => Plhu rd ra (AOff ofs) + | PLoadRRO Asmblock.Plw rd ra ofs => Plw rd ra (AOff ofs) + | PLoadRRO Asmblock.Plw_a rd ra ofs => Plw_a rd ra (AOff ofs) + | PLoadRRO Asmblock.Pld rd ra ofs => Pld rd ra (AOff ofs) + | PLoadRRO Asmblock.Pld_a rd ra ofs => Pld_a rd ra (AOff ofs) + | PLoadRRO Asmblock.Pfls rd ra ofs => Pfls rd ra (AOff ofs) + | PLoadRRO Asmblock.Pfld rd ra ofs => Pfld rd ra (AOff ofs) + + | PLoadRRR Asmblock.Plb rd ra ro => Plb rd ra (AReg ro) + | PLoadRRR Asmblock.Plbu rd ra ro => Plbu rd ra (AReg ro) + | PLoadRRR Asmblock.Plh rd ra ro => Plh rd ra (AReg ro) + | PLoadRRR Asmblock.Plhu rd ra ro => Plhu rd ra (AReg ro) + | PLoadRRR Asmblock.Plw rd ra ro => Plw rd ra (AReg ro) + | PLoadRRR Asmblock.Plw_a rd ra ro => Plw_a rd ra (AReg ro) + | PLoadRRR Asmblock.Pld rd ra ro => Pld rd ra (AReg ro) + | PLoadRRR Asmblock.Pld_a rd ra ro => Pld_a rd ra (AReg ro) + | PLoadRRR Asmblock.Pfls rd ra ro => Pfls rd ra (AReg ro) + | PLoadRRR Asmblock.Pfld rd ra ro => Pfld rd ra (AReg ro) (** Store *) - | PStoreRRO Asmblock.Psb rd ra ofs => Psb rd ra ofs - | PStoreRRO Asmblock.Psh rd ra ofs => Psh rd ra ofs - | PStoreRRO Asmblock.Psw rd ra ofs => Psw rd ra ofs - | PStoreRRO Asmblock.Psw_a rd ra ofs => Psw_a rd ra ofs - | PStoreRRO Asmblock.Psd rd ra ofs => Psd rd ra ofs - | PStoreRRO Asmblock.Psd_a rd ra ofs => Psd_a rd ra ofs - | PStoreRRO Asmblock.Pfss rd ra ofs => Pfss rd ra ofs - | PStoreRRO Asmblock.Pfsd rd ra ofs => Pfsd rd ra ofs + | PStoreRRO Asmblock.Psb rd ra ofs => Psb rd ra (AOff ofs) + | PStoreRRO Asmblock.Psh rd ra ofs => Psh rd ra (AOff ofs) + | PStoreRRO Asmblock.Psw rd ra ofs => Psw rd ra (AOff ofs) + | PStoreRRO Asmblock.Psw_a rd ra ofs => Psw_a rd ra (AOff ofs) + | PStoreRRO Asmblock.Psd rd ra ofs => Psd rd ra (AOff ofs) + | PStoreRRO Asmblock.Psd_a rd ra ofs => Psd_a rd ra (AOff ofs) + | PStoreRRO Asmblock.Pfss rd ra ofs => Pfss rd ra (AOff ofs) + | PStoreRRO Asmblock.Pfsd rd ra ofs => Pfsd rd ra (AOff ofs) + + | PStoreRRR Asmblock.Psb rd ra ro => Psb rd ra (AReg ro) + | PStoreRRR Asmblock.Psh rd ra ro => Psh rd ra (AReg ro) + | PStoreRRR Asmblock.Psw rd ra ro => Psw rd ra (AReg ro) + | PStoreRRR Asmblock.Psw_a rd ra ro => Psw_a rd ra (AReg ro) + | PStoreRRR Asmblock.Psd rd ra ro => Psd rd ra (AReg ro) + | PStoreRRR Asmblock.Psd_a rd ra ro => Psd_a rd ra (AReg ro) + | PStoreRRR Asmblock.Pfss rd ra ro => Pfss rd ra (AReg ro) + | PStoreRRR Asmblock.Pfsd rd ra ro => Pfsd rd ra (AReg ro) end. -- cgit