diff options
| -rw-r--r-- | mppa_k1c/Asm.v | 336 | ||||
| -rw-r--r-- | mppa_k1c/Asmblock.v | 1350 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 14 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 28 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 116 | ||||
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 1363 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 6 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 16 | ||||
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 6 |
11 files changed, 1634 insertions, 1611 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 115c8d6d..893552c4 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -220,195 +220,195 @@ Inductive instruction : Type := Definition control_to_instruction (c: control) :=
match c with
- | PExpand (Asmblock.Pbuiltin ef args res) => Pbuiltin ef args res
- | PCtlFlow Asmblock.Pret => Pret
- | PCtlFlow (Asmblock.Pcall l) => Pcall l
- | PCtlFlow (Asmblock.Picall r) => Picall r
- | PCtlFlow (Asmblock.Pgoto l) => Pgoto l
- | PCtlFlow (Asmblock.Pigoto l) => Pigoto l
- | 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
+ | PExpand (Asmvliw.Pbuiltin ef args res) => Pbuiltin ef args res
+ | PCtlFlow Asmvliw.Pret => Pret
+ | PCtlFlow (Asmvliw.Pcall l) => Pcall l
+ | PCtlFlow (Asmvliw.Picall r) => Picall r
+ | PCtlFlow (Asmvliw.Pgoto l) => Pgoto l
+ | PCtlFlow (Asmvliw.Pigoto l) => Pigoto l
+ | PCtlFlow (Asmvliw.Pj_l l) => Pj_l l
+ | PCtlFlow (Asmvliw.Pcb bt r l) => Pcb bt r l
+ | PCtlFlow (Asmvliw.Pcbu bt r l) => Pcbu bt r l
+ | PCtlFlow (Asmvliw.Pjumptable r label) => Pjumptable r label
end.
Definition basic_to_instruction (b: basic) :=
match b with
(** Special basics *)
- | Asmblock.Pget rd rs => Pget rd rs
- | Asmblock.Pset rd rs => Pset rd rs
- | Asmblock.Pnop => Pnop
- | Asmblock.Pallocframe sz pos => Pallocframe sz pos
- | Asmblock.Pfreeframe sz pos => Pfreeframe sz pos
+ | Asmvliw.Pget rd rs => Pget rd rs
+ | Asmvliw.Pset rd rs => Pset rd rs
+ | Asmvliw.Pnop => Pnop
+ | Asmvliw.Pallocframe sz pos => Pallocframe sz pos
+ | Asmvliw.Pfreeframe sz pos => Pfreeframe sz pos
(** PArith basics *)
(* R *)
- | PArithR (Asmblock.Ploadsymbol id ofs) r => Ploadsymbol r id ofs
+ | PArithR (Asmvliw.Ploadsymbol id ofs) r => Ploadsymbol r id ofs
(* RR *)
- | PArithRR Asmblock.Pmv rd rs => Pmv rd rs
- | PArithRR Asmblock.Pnegw rd rs => Pnegw rd rs
- | PArithRR Asmblock.Pnegl rd rs => Pnegl rd rs
- | PArithRR Asmblock.Pcvtl2w rd rs => Pcvtl2w rd rs
- | PArithRR Asmblock.Psxwd rd rs => Psxwd rd rs
- | PArithRR Asmblock.Pzxwd rd rs => Pzxwd rd rs
- | PArithRR Asmblock.Pfabsd rd rs => Pfabsd rd rs
- | PArithRR Asmblock.Pfabsw rd rs => Pfabsw rd rs
- | PArithRR Asmblock.Pfnegd rd rs => Pfnegd rd rs
- | PArithRR Asmblock.Pfnegw rd rs => Pfnegw rd rs
- | PArithRR Asmblock.Pfnarrowdw rd rs => Pfnarrowdw rd rs
- | PArithRR Asmblock.Pfwidenlwd rd rs => Pfwidenlwd rd rs
- | PArithRR Asmblock.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs
- | PArithRR Asmblock.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
- | PArithRR Asmblock.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs
- | PArithRR Asmblock.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs
- | PArithRR Asmblock.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs
- | PArithRR Asmblock.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs
- | PArithRR Asmblock.Pfixedwrzz rd rs => Pfixedwrzz rd rs
- | PArithRR Asmblock.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs
- | PArithRR Asmblock.Pfixeddrzz rd rs => Pfixeddrzz rd rs
- | PArithRR Asmblock.Pfixedudrzz rd rs => Pfixedudrzz rd rs
- | PArithRR Asmblock.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs
- | PArithRR Asmblock.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs
+ | PArithRR Asmvliw.Pmv rd rs => Pmv rd rs
+ | PArithRR Asmvliw.Pnegw rd rs => Pnegw rd rs
+ | PArithRR Asmvliw.Pnegl rd rs => Pnegl rd rs
+ | PArithRR Asmvliw.Pcvtl2w rd rs => Pcvtl2w rd rs
+ | PArithRR Asmvliw.Psxwd rd rs => Psxwd rd rs
+ | PArithRR Asmvliw.Pzxwd rd rs => Pzxwd rd rs
+ | PArithRR Asmvliw.Pfabsd rd rs => Pfabsd rd rs
+ | PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs
+ | PArithRR Asmvliw.Pfnegd rd rs => Pfnegd rd rs
+ | PArithRR Asmvliw.Pfnegw rd rs => Pfnegw rd rs
+ | PArithRR Asmvliw.Pfnarrowdw rd rs => Pfnarrowdw rd rs
+ | PArithRR Asmvliw.Pfwidenlwd rd rs => Pfwidenlwd rd rs
+ | PArithRR Asmvliw.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs
+ | PArithRR Asmvliw.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
+ | PArithRR Asmvliw.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs
+ | PArithRR Asmvliw.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs
+ | PArithRR Asmvliw.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs
+ | PArithRR Asmvliw.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs
+ | PArithRR Asmvliw.Pfixedwrzz rd rs => Pfixedwrzz rd rs
+ | PArithRR Asmvliw.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs
+ | PArithRR Asmvliw.Pfixeddrzz rd rs => Pfixeddrzz rd rs
+ | PArithRR Asmvliw.Pfixedudrzz rd rs => Pfixedudrzz rd rs
+ | PArithRR Asmvliw.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs
+ | PArithRR Asmvliw.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs
(* RI32 *)
- | PArithRI32 Asmblock.Pmake rd imm => Pmake rd imm
+ | PArithRI32 Asmvliw.Pmake rd imm => Pmake rd imm
(* RI64 *)
- | PArithRI64 Asmblock.Pmakel rd imm => Pmakel rd imm
+ | PArithRI64 Asmvliw.Pmakel rd imm => Pmakel rd imm
(* RF32 *)
- | PArithRF32 Asmblock.Pmakefs rd imm => Pmakefs rd imm
+ | PArithRF32 Asmvliw.Pmakefs rd imm => Pmakefs rd imm
(* RF64 *)
- | PArithRF64 Asmblock.Pmakef rd imm => Pmakef rd imm
+ | PArithRF64 Asmvliw.Pmakef rd imm => Pmakef rd imm
(* RRR *)
- | PArithRRR (Asmblock.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2
- | PArithRRR (Asmblock.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2
- | PArithRRR (Asmblock.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2
- | PArithRRR (Asmblock.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2
- | PArithRRR Asmblock.Paddw rd rs1 rs2 => Paddw rd rs1 rs2
- | PArithRRR Asmblock.Psubw rd rs1 rs2 => Psubw rd rs1 rs2
- | PArithRRR Asmblock.Pmulw rd rs1 rs2 => Pmulw rd rs1 rs2
- | PArithRRR Asmblock.Pandw rd rs1 rs2 => Pandw rd rs1 rs2
- | PArithRRR Asmblock.Pnandw rd rs1 rs2 => Pnandw rd rs1 rs2
- | PArithRRR Asmblock.Porw rd rs1 rs2 => Porw rd rs1 rs2
- | PArithRRR Asmblock.Pnorw rd rs1 rs2 => Pnorw rd rs1 rs2
- | PArithRRR Asmblock.Pxorw rd rs1 rs2 => Pxorw rd rs1 rs2
- | PArithRRR Asmblock.Pnxorw rd rs1 rs2 => Pnxorw rd rs1 rs2
- | PArithRRR Asmblock.Pandnw rd rs1 rs2 => Pandnw rd rs1 rs2
- | PArithRRR Asmblock.Pornw rd rs1 rs2 => Pornw rd rs1 rs2
- | PArithRRR Asmblock.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
- | PArithRRR Asmblock.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
- | PArithRRR Asmblock.Psllw rd rs1 rs2 => Psllw rd rs1 rs2
-
- | PArithRRR Asmblock.Paddl rd rs1 rs2 => Paddl rd rs1 rs2
- | PArithRRR Asmblock.Psubl rd rs1 rs2 => Psubl rd rs1 rs2
- | PArithRRR Asmblock.Pandl rd rs1 rs2 => Pandl rd rs1 rs2
- | PArithRRR Asmblock.Pnandl rd rs1 rs2 => Pnandl rd rs1 rs2
- | PArithRRR Asmblock.Porl rd rs1 rs2 => Porl rd rs1 rs2
- | PArithRRR Asmblock.Pnorl rd rs1 rs2 => Pnorl rd rs1 rs2
- | PArithRRR Asmblock.Pxorl rd rs1 rs2 => Pxorl rd rs1 rs2
- | PArithRRR Asmblock.Pnxorl rd rs1 rs2 => Pnxorl rd rs1 rs2
- | PArithRRR Asmblock.Pandnl rd rs1 rs2 => Pandnl rd rs1 rs2
- | PArithRRR Asmblock.Pornl rd rs1 rs2 => Pornl rd rs1 rs2
- | PArithRRR Asmblock.Pmull rd rs1 rs2 => Pmull rd rs1 rs2
- | PArithRRR Asmblock.Pslll rd rs1 rs2 => Pslll rd rs1 rs2
- | PArithRRR Asmblock.Psrll rd rs1 rs2 => Psrll rd rs1 rs2
- | PArithRRR Asmblock.Psral rd rs1 rs2 => Psral rd rs1 rs2
-
- | PArithRRR Asmblock.Pfaddd rd rs1 rs2 => Pfaddd rd rs1 rs2
- | PArithRRR Asmblock.Pfaddw rd rs1 rs2 => Pfaddw rd rs1 rs2
- | PArithRRR Asmblock.Pfsbfd rd rs1 rs2 => Pfsbfd rd rs1 rs2
- | PArithRRR Asmblock.Pfsbfw rd rs1 rs2 => Pfsbfw rd rs1 rs2
- | PArithRRR Asmblock.Pfmuld rd rs1 rs2 => Pfmuld rd rs1 rs2
- | PArithRRR Asmblock.Pfmulw rd rs1 rs2 => Pfmulw rd rs1 rs2
+ | PArithRRR (Asmvliw.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2
+ | PArithRRR (Asmvliw.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2
+ | PArithRRR (Asmvliw.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2
+ | PArithRRR (Asmvliw.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2
+ | PArithRRR Asmvliw.Paddw rd rs1 rs2 => Paddw rd rs1 rs2
+ | PArithRRR Asmvliw.Psubw rd rs1 rs2 => Psubw rd rs1 rs2
+ | PArithRRR Asmvliw.Pmulw rd rs1 rs2 => Pmulw rd rs1 rs2
+ | PArithRRR Asmvliw.Pandw rd rs1 rs2 => Pandw rd rs1 rs2
+ | PArithRRR Asmvliw.Pnandw rd rs1 rs2 => Pnandw rd rs1 rs2
+ | PArithRRR Asmvliw.Porw rd rs1 rs2 => Porw rd rs1 rs2
+ | PArithRRR Asmvliw.Pnorw rd rs1 rs2 => Pnorw rd rs1 rs2
+ | PArithRRR Asmvliw.Pxorw rd rs1 rs2 => Pxorw rd rs1 rs2
+ | PArithRRR Asmvliw.Pnxorw rd rs1 rs2 => Pnxorw rd rs1 rs2
+ | PArithRRR Asmvliw.Pandnw rd rs1 rs2 => Pandnw rd rs1 rs2
+ | PArithRRR Asmvliw.Pornw rd rs1 rs2 => Pornw rd rs1 rs2
+ | PArithRRR Asmvliw.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
+ | PArithRRR Asmvliw.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
+ | PArithRRR Asmvliw.Psllw rd rs1 rs2 => Psllw rd rs1 rs2
+
+ | PArithRRR Asmvliw.Paddl rd rs1 rs2 => Paddl rd rs1 rs2
+ | PArithRRR Asmvliw.Psubl rd rs1 rs2 => Psubl rd rs1 rs2
+ | PArithRRR Asmvliw.Pandl rd rs1 rs2 => Pandl rd rs1 rs2
+ | PArithRRR Asmvliw.Pnandl rd rs1 rs2 => Pnandl rd rs1 rs2
+ | PArithRRR Asmvliw.Porl rd rs1 rs2 => Porl rd rs1 rs2
+ | PArithRRR Asmvliw.Pnorl rd rs1 rs2 => Pnorl rd rs1 rs2
+ | PArithRRR Asmvliw.Pxorl rd rs1 rs2 => Pxorl rd rs1 rs2
+ | PArithRRR Asmvliw.Pnxorl rd rs1 rs2 => Pnxorl rd rs1 rs2
+ | PArithRRR Asmvliw.Pandnl rd rs1 rs2 => Pandnl rd rs1 rs2
+ | PArithRRR Asmvliw.Pornl rd rs1 rs2 => Pornl rd rs1 rs2
+ | PArithRRR Asmvliw.Pmull rd rs1 rs2 => Pmull rd rs1 rs2
+ | PArithRRR Asmvliw.Pslll rd rs1 rs2 => Pslll rd rs1 rs2
+ | PArithRRR Asmvliw.Psrll rd rs1 rs2 => Psrll rd rs1 rs2
+ | PArithRRR Asmvliw.Psral rd rs1 rs2 => Psral rd rs1 rs2
+
+ | PArithRRR Asmvliw.Pfaddd rd rs1 rs2 => Pfaddd rd rs1 rs2
+ | PArithRRR Asmvliw.Pfaddw rd rs1 rs2 => Pfaddw rd rs1 rs2
+ | PArithRRR Asmvliw.Pfsbfd rd rs1 rs2 => Pfsbfd rd rs1 rs2
+ | PArithRRR Asmvliw.Pfsbfw rd rs1 rs2 => Pfsbfw rd rs1 rs2
+ | PArithRRR Asmvliw.Pfmuld rd rs1 rs2 => Pfmuld rd rs1 rs2
+ | PArithRRR Asmvliw.Pfmulw rd rs1 rs2 => Pfmulw rd rs1 rs2
(* RRI32 *)
- | PArithRRI32 (Asmblock.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
- | PArithRRI32 Asmblock.Paddiw rd rs imm => Paddiw rd rs imm
- | PArithRRI32 Asmblock.Pmuliw rd rs imm => Pmuliw rd rs imm
- | PArithRRI32 Asmblock.Pandiw rd rs imm => Pandiw rd rs imm
- | PArithRRI32 Asmblock.Pnandiw rd rs imm => Pnandiw rd rs imm
- | PArithRRI32 Asmblock.Poriw rd rs imm => Poriw rd rs imm
- | PArithRRI32 Asmblock.Pnoriw rd rs imm => Pnoriw rd rs imm
- | PArithRRI32 Asmblock.Pxoriw rd rs imm => Pxoriw rd rs imm
- | PArithRRI32 Asmblock.Pnxoriw rd rs imm => Pnxoriw rd rs imm
- | PArithRRI32 Asmblock.Pandniw rd rs imm => Pandniw rd rs imm
- | PArithRRI32 Asmblock.Porniw rd rs imm => Porniw rd rs imm
- | PArithRRI32 Asmblock.Psraiw rd rs imm => Psraiw rd rs imm
- | PArithRRI32 Asmblock.Psrliw rd rs imm => Psrliw rd rs imm
- | PArithRRI32 Asmblock.Pslliw rd rs imm => Pslliw rd rs imm
- | PArithRRI32 Asmblock.Proriw rd rs imm => Proriw rd rs imm
- | PArithRRI32 Asmblock.Psllil rd rs imm => Psllil rd rs imm
- | PArithRRI32 Asmblock.Psrlil rd rs imm => Psrlil rd rs imm
- | PArithRRI32 Asmblock.Psrail rd rs imm => Psrail rd rs imm
+ | PArithRRI32 (Asmvliw.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
+ | PArithRRI32 Asmvliw.Paddiw rd rs imm => Paddiw rd rs imm
+ | PArithRRI32 Asmvliw.Pmuliw rd rs imm => Pmuliw rd rs imm
+ | PArithRRI32 Asmvliw.Pandiw rd rs imm => Pandiw rd rs imm
+ | PArithRRI32 Asmvliw.Pnandiw rd rs imm => Pnandiw rd rs imm
+ | PArithRRI32 Asmvliw.Poriw rd rs imm => Poriw rd rs imm
+ | PArithRRI32 Asmvliw.Pnoriw rd rs imm => Pnoriw rd rs imm
+ | PArithRRI32 Asmvliw.Pxoriw rd rs imm => Pxoriw rd rs imm
+ | PArithRRI32 Asmvliw.Pnxoriw rd rs imm => Pnxoriw rd rs imm
+ | PArithRRI32 Asmvliw.Pandniw rd rs imm => Pandniw rd rs imm
+ | PArithRRI32 Asmvliw.Porniw rd rs imm => Porniw rd rs imm
+ | PArithRRI32 Asmvliw.Psraiw rd rs imm => Psraiw rd rs imm
+ | PArithRRI32 Asmvliw.Psrliw rd rs imm => Psrliw rd rs imm
+ | PArithRRI32 Asmvliw.Pslliw rd rs imm => Pslliw rd rs imm
+ | PArithRRI32 Asmvliw.Proriw rd rs imm => Proriw rd rs imm
+ | PArithRRI32 Asmvliw.Psllil rd rs imm => Psllil rd rs imm
+ | PArithRRI32 Asmvliw.Psrlil rd rs imm => Psrlil rd rs imm
+ | PArithRRI32 Asmvliw.Psrail rd rs imm => Psrail rd rs imm
(* RRI64 *)
- | PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm
- | PArithRRI64 Asmblock.Paddil rd rs imm => Paddil rd rs imm
- | PArithRRI64 Asmblock.Pmulil rd rs imm => Pmulil rd rs imm
- | PArithRRI64 Asmblock.Pandil rd rs imm => Pandil rd rs imm
- | PArithRRI64 Asmblock.Pnandil rd rs imm => Pnandil rd rs imm
- | PArithRRI64 Asmblock.Poril rd rs imm => Poril rd rs imm
- | PArithRRI64 Asmblock.Pnoril rd rs imm => Pnoril rd rs imm
- | PArithRRI64 Asmblock.Pxoril rd rs imm => Pxoril rd rs imm
- | PArithRRI64 Asmblock.Pnxoril rd rs imm => Pnxoril rd rs imm
- | PArithRRI64 Asmblock.Pandnil rd rs imm => Pandnil rd rs imm
- | PArithRRI64 Asmblock.Pornil rd rs imm => Pornil rd rs imm
+ | PArithRRI64 (Asmvliw.Pcompil it) rd rs imm => Pcompil it rd rs imm
+ | PArithRRI64 Asmvliw.Paddil rd rs imm => Paddil rd rs imm
+ | PArithRRI64 Asmvliw.Pmulil rd rs imm => Pmulil rd rs imm
+ | PArithRRI64 Asmvliw.Pandil rd rs imm => Pandil rd rs imm
+ | PArithRRI64 Asmvliw.Pnandil rd rs imm => Pnandil rd rs imm
+ | PArithRRI64 Asmvliw.Poril rd rs imm => Poril rd rs imm
+ | PArithRRI64 Asmvliw.Pnoril rd rs imm => Pnoril rd rs imm
+ | PArithRRI64 Asmvliw.Pxoril rd rs imm => Pxoril rd rs imm
+ | PArithRRI64 Asmvliw.Pnxoril rd rs imm => Pnxoril rd rs imm
+ | PArithRRI64 Asmvliw.Pandnil rd rs imm => Pandnil rd rs imm
+ | PArithRRI64 Asmvliw.Pornil rd rs imm => Pornil rd rs imm
(** ARRR *)
- | PArithARRR Asmblock.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
- | PArithARRR Asmblock.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
+ | PArithARRR Asmvliw.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
+ | PArithARRR Asmvliw.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
(** ARRI32 *)
- | PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
+ | PArithARRI32 Asmvliw.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
(** ARRI64 *)
- | PArithARRI64 Asmblock.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm
+ | PArithARRI64 Asmvliw.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm
(** Load *)
- | 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)
+ | PLoadRRO Asmvliw.Plb rd ra ofs => Plb rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Plbu rd ra ofs => Plbu rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Plh rd ra ofs => Plh rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Plhu rd ra ofs => Plhu rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Plw rd ra ofs => Plw rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Plw_a rd ra ofs => Plw_a rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Pld rd ra ofs => Pld rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Pld_a rd ra ofs => Pld_a rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Pfls rd ra ofs => Pfls rd ra (AOff ofs)
+ | PLoadRRO Asmvliw.Pfld rd ra ofs => Pfld rd ra (AOff ofs)
+
+ | PLoadRRR Asmvliw.Plb rd ra ro => Plb rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Plbu rd ra ro => Plbu rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Plh rd ra ro => Plh rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Plhu rd ra ro => Plhu rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Plw rd ra ro => Plw rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Plw_a rd ra ro => Plw_a rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Pld rd ra ro => Pld rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Pld_a rd ra ro => Pld_a rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Pfls rd ra ro => Pfls rd ra (AReg ro)
+ | PLoadRRR Asmvliw.Pfld rd ra ro => Pfld rd ra (AReg ro)
(** Store *)
- | 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)
+ | PStoreRRO Asmvliw.Psb rd ra ofs => Psb rd ra (AOff ofs)
+ | PStoreRRO Asmvliw.Psh rd ra ofs => Psh rd ra (AOff ofs)
+ | PStoreRRO Asmvliw.Psw rd ra ofs => Psw rd ra (AOff ofs)
+ | PStoreRRO Asmvliw.Psw_a rd ra ofs => Psw_a rd ra (AOff ofs)
+ | PStoreRRO Asmvliw.Psd rd ra ofs => Psd rd ra (AOff ofs)
+ | PStoreRRO Asmvliw.Psd_a rd ra ofs => Psd_a rd ra (AOff ofs)
+ | PStoreRRO Asmvliw.Pfss rd ra ofs => Pfss rd ra (AOff ofs)
+ | PStoreRRO Asmvliw.Pfsd rd ra ofs => Pfsd rd ra (AOff ofs)
+
+ | PStoreRRR Asmvliw.Psb rd ra ro => Psb rd ra (AReg ro)
+ | PStoreRRR Asmvliw.Psh rd ra ro => Psh rd ra (AReg ro)
+ | PStoreRRR Asmvliw.Psw rd ra ro => Psw rd ra (AReg ro)
+ | PStoreRRR Asmvliw.Psw_a rd ra ro => Psw_a rd ra (AReg ro)
+ | PStoreRRR Asmvliw.Psd rd ra ro => Psd rd ra (AReg ro)
+ | PStoreRRR Asmvliw.Psd_a rd ra ro => Psd_a rd ra (AReg ro)
+ | PStoreRRR Asmvliw.Pfss rd ra ro => Pfss rd ra (AReg ro)
+ | PStoreRRR Asmvliw.Pfsd rd ra ro => Pfsd rd ra (AReg ro)
end.
@@ -449,7 +449,7 @@ Definition fundef := AST.fundef function. Definition program := AST.program fundef unit.
Definition genv := Genv.t fundef unit.
-Definition function_proj (f: function) := Asmblock.mkfunction (fn_sig f) (fn_blocks f).
+Definition function_proj (f: function) := Asmvliw.mkfunction (fn_sig f) (fn_blocks f).
(*
Definition fundef_proj (fu: fundef) : Asmblock.fundef := transf_fundef function_proj fu.
@@ -457,19 +457,19 @@ Definition fundef_proj (fu: fundef) : Asmblock.fundef := transf_fundef function_ Definition program_proj (p: program) : Asmblock.program := transform_program fundef_proj p.
*)
-Definition fundef_proj (fu: fundef) : Asmblock.fundef :=
+Definition fundef_proj (fu: fundef) : Asmvliw.fundef :=
match fu with
| Internal f => Internal (function_proj f)
| External ef => External ef
end.
-Definition globdef_proj (gd: globdef fundef unit) : globdef Asmblock.fundef unit :=
+Definition globdef_proj (gd: globdef fundef unit) : globdef Asmvliw.fundef unit :=
match gd with
| Gfun f => Gfun (fundef_proj f)
| Gvar gu => Gvar gu
end.
-Program Definition genv_trans (ge: genv) : Asmblock.genv :=
+Program Definition genv_trans (ge: genv) : Asmvliw.genv :=
{| Genv.genv_public := Genv.genv_public ge;
Genv.genv_symb := Genv.genv_symb ge;
Genv.genv_defs := PTree.map1 globdef_proj (Genv.genv_defs ge);
@@ -488,13 +488,13 @@ Qed. Next Obligation. Qed.
Fixpoint prog_defs_proj (l: list (ident * globdef fundef unit))
- : list (ident * globdef Asmblock.fundef unit) :=
+ : list (ident * globdef Asmvliw.fundef unit) :=
match l with
| nil => nil
| (i, gd) :: l => (i, globdef_proj gd) :: prog_defs_proj l
end.
-Definition program_proj (p: program) : Asmblock.program :=
+Definition program_proj (p: program) : Asmvliw.program :=
{| prog_defs := prog_defs_proj (prog_defs p);
prog_public := prog_public p;
prog_main := prog_main p
@@ -513,16 +513,16 @@ Qed. (** transf_program *)
-Program Definition transf_function (f: Asmblock.function) : function :=
- {| fn_sig := Asmblock.fn_sig f; fn_blocks := Asmblock.fn_blocks f;
- fn_code := unfold (Asmblock.fn_blocks f) |}.
+Program Definition transf_function (f: Asmvliw.function) : function :=
+ {| fn_sig := Asmvliw.fn_sig f; fn_blocks := Asmvliw.fn_blocks f;
+ fn_code := unfold (Asmvliw.fn_blocks f) |}.
Lemma transf_function_proj: forall f, function_proj (transf_function f) = f.
Proof.
intros f. destruct f as [sig blks]. unfold function_proj. simpl. auto.
Qed.
-Definition transf_fundef : Asmblock.fundef -> fundef := AST.transf_fundef transf_function.
+Definition transf_fundef : Asmvliw.fundef -> fundef := AST.transf_fundef transf_function.
Lemma transf_fundef_proj: forall f, fundef_proj (transf_fundef f) = f.
Proof.
@@ -559,7 +559,7 @@ Proof. Qed.
*)
-Definition transf_program : Asmblock.program -> program := transform_program transf_fundef.
+Definition transf_program : Asmvliw.program -> program := transform_program transf_fundef.
Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),
prog_defs p1 = prog_defs p2 ->
@@ -582,7 +582,7 @@ Proof. rewrite transf_fundef_proj. auto.
Qed.
-Definition match_prog (p: Asmblock.program) (tp: program) :=
+Definition match_prog (p: Asmvliw.program) (tp: program) :=
match_program (fun _ f tf => tf = transf_fundef f) eq p tp.
Lemma transf_program_match:
@@ -615,7 +615,7 @@ Qed. Section PRESERVATION.
-Variable prog: Asmblock.program.
+Variable prog: Asmvliw.program.
Variable tprog: program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index e612576f..3bcb321d 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -31,1202 +31,18 @@ Require Import Locations. Require Stacklayout. Require Import Conventions. Require Import Errors. - -(** * Abstract syntax *) - -(** General Purpose registers. -*) - -Inductive gpreg: Type := - | GPR0: gpreg | GPR1: gpreg | GPR2: gpreg | GPR3: gpreg | GPR4: gpreg - | GPR5: gpreg | GPR6: gpreg | GPR7: gpreg | GPR8: gpreg | GPR9: gpreg - | GPR10: gpreg | GPR11: gpreg | GPR12: gpreg | GPR13: gpreg | GPR14: gpreg - | GPR15: gpreg | GPR16: gpreg | GPR17: gpreg | GPR18: gpreg | GPR19: gpreg - | GPR20: gpreg | GPR21: gpreg | GPR22: gpreg | GPR23: gpreg | GPR24: gpreg - | GPR25: gpreg | GPR26: gpreg | GPR27: gpreg | GPR28: gpreg | GPR29: gpreg - | GPR30: gpreg | GPR31: gpreg | GPR32: gpreg | GPR33: gpreg | GPR34: gpreg - | GPR35: gpreg | GPR36: gpreg | GPR37: gpreg | GPR38: gpreg | GPR39: gpreg - | GPR40: gpreg | GPR41: gpreg | GPR42: gpreg | GPR43: gpreg | GPR44: gpreg - | GPR45: gpreg | GPR46: gpreg | GPR47: gpreg | GPR48: gpreg | GPR49: gpreg - | GPR50: gpreg | GPR51: gpreg | GPR52: gpreg | GPR53: gpreg | GPR54: gpreg - | GPR55: gpreg | GPR56: gpreg | GPR57: gpreg | GPR58: gpreg | GPR59: gpreg - | GPR60: gpreg | GPR61: gpreg | GPR62: gpreg | GPR63: gpreg. - -Definition ireg := gpreg. -Definition freg := gpreg. - -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. - -(** We model the following registers of the RISC-V architecture. *) - -(** basic register *) -Inductive preg: Type := - | IR: gpreg -> preg (**r integer general purpose registers *) - | RA: preg - | PC: preg - . - -Coercion IR: gpreg >-> preg. - -Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. Defined. - -Module PregEq. - Definition t := preg. - Definition eq := preg_eq. -End PregEq. - -Module Pregmap := EMap(PregEq). - -(** Conventional names for stack pointer ([SP]) and return address ([RA]). *) - -Notation "'SP'" := GPR12 (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. - -Inductive btest: Type := - | BTdnez (**r Double Not Equal to Zero *) - | BTdeqz (**r Double Equal to Zero *) - | BTdltz (**r Double Less Than Zero *) - | BTdgez (**r Double Greater Than or Equal to Zero *) - | BTdlez (**r Double Less Than or Equal to Zero *) - | BTdgtz (**r Double Greater Than Zero *) -(*| BTodd (**r Odd (LSB Set) *) - | BTeven (**r Even (LSB Clear) *) -*)| BTwnez (**r Word Not Equal to Zero *) - | BTweqz (**r Word Equal to Zero *) - | BTwltz (**r Word Less Than Zero *) - | BTwgez (**r Word Greater Than or Equal to Zero *) - | BTwlez (**r Word Less Than or Equal to Zero *) - | BTwgtz (**r Word Greater Than Zero *) - . - -Inductive itest: Type := - | ITne (**r Not Equal *) - | ITeq (**r Equal *) - | ITlt (**r Less Than *) - | ITge (**r Greater Than or Equal *) - | ITle (**r Less Than or Equal *) - | ITgt (**r Greater Than *) - | ITneu (**r Unsigned Not Equal *) - | ITequ (**r Unsigned Equal *) - | ITltu (**r Less Than Unsigned *) - | ITgeu (**r Greater Than or Equal Unsigned *) - | ITleu (**r Less Than or Equal Unsigned *) - | ITgtu (**r Greater Than Unsigned *) - (* Not used yet *) - | ITall (**r All Bits Set in Mask *) - | ITnall (**r Not All Bits Set in Mask *) - | ITany (**r Any Bits Set in Mask *) - | ITnone (**r Not Any Bits Set in Mask *) - . - -Inductive ftest: Type := - | FTone (**r Ordered and Not Equal *) - | FTueq (**r Unordered or Equal *) - | FToeq (**r Ordered and Equal *) - | FTune (**r Unordered or Not Equal *) - | FTolt (**r Ordered and Less Than *) - | FTuge (**r Unordered or Greater Than or Equal *) - | FToge (**r Ordered and Greater Than or Equal *) - | FTult (**r Unordered or Less Than *) - . - -(** Offsets for load and store instructions. An offset is either an - immediate integer or the low part of a symbol. *) - -Inductive offset : Type := - | Ofsimm (ofs: ptrofs) - | Ofslow (id: ident) (ofs: ptrofs). - -(** We model a subset of the K1c instruction set. In particular, we do not - support floats yet. - - Although it is possible to use the 32-bits mode, for now we don't support it. - - We follow a design close to the one used for the Risc-V port: one set of - pseudo-instructions for 32-bit integer arithmetic, with suffix W, another - set for 64-bit integer arithmetic, with suffix L. - - When mapping to actual instructions, the OCaml code in TargetPrinter.ml - throws an error if we are not in 64-bits mode. -*) - -(** * Instructions *) - -Definition label := positive. - -(* FIXME - rewrite the comment *) -(** A note on immediates: there are various constraints on immediate - operands to K1c instructions. We do not attempt to capture these - restrictions in the abstract syntax nor in the semantics. The - assembler will emit an error if immediate operands exceed the - representable range. Of course, our K1c generator (file - [Asmgen]) is careful to respect this range. *) - -(** Instructions to be expanded in control-flow -*) -Inductive ex_instruction : Type := - (* Pseudo-instructions *) -(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *) - | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) - - | Pbuiltin: external_function -> list (builtin_arg preg) - -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) -. - -(** FIXME: comment not up to date ! - - - The pseudo-instructions are the following: - -- [Ploadsymbol]: load the address of a symbol in an integer register. - Expands to the [la] assembler pseudo-instruction, which does the right - thing even if we are in PIC mode. - -- [Pallocframe sz pos]: in the formal semantics, this - pseudo-instruction allocates a memory block with bounds [0] and - [sz], stores the value of the stack pointer at offset [pos] in this - block, and sets the stack pointer to the address of the bottom of - this block. - In the printed ASM assembly code, this allocation is: -<< - mv x30, sp - sub sp, sp, #sz - sw x30, #pos(sp) ->> - This cannot be expressed in our memory model, which does not reflect - the fact that stack frames are adjacent and allocated/freed - following a stack discipline. - -- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction - reads the word at [pos] of the block pointed by the stack pointer, - frees this block, and sets the stack pointer to the value read. - In the printed ASM assembly code, this freeing is just an increment of [sp]: -<< - add sp, sp, #sz ->> - Again, our memory model cannot comprehend that this operation - frees (logically) the current stack frame. - -- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table - as follows: -<< - la x31, table - add x31, x31, reg - jr x31 -table: .long table[0], table[1], ... ->> - Note that [reg] contains 4 times the index of the desired table entry. -*) - -(** Control Flow instructions *) -Inductive cf_instruction : Type := - | Pret (**r return *) - | Pcall (l: label) (**r function call *) - | Picall (r: ireg) (**r function call on register value *) - | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *) - - (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *) - | Pgoto (l: label) (**r goto *) - | Pigoto (r: ireg) (**r goto from register *) - | Pj_l (l: label) (**r jump to label *) - - (* Conditional branches *) - | 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 *) -. - -(** Loads **) -Inductive load_name : Type := - | Plb (**r load byte *) - | Plbu (**r load byte unsigned *) - | Plh (**r load half word *) - | Plhu (**r load half word unsigned *) - | Plw (**r load int32 *) - | Plw_a (**r load any32 *) - | Pld (**r load int64 *) - | Pld_a (**r load any64 *) - | Pfls (**r load float *) - | Pfld (**r load 64-bit float *) -. - -Inductive ld_instruction : Type := - | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) - | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) -. - -Coercion PLoadRRO: load_name >-> Funclass. -Coercion PLoadRRR: load_name >-> Funclass. - -(** Stores **) -Inductive store_name : Type := - | Psb (**r store byte *) - | Psh (**r store half byte *) - | Psw (**r store int32 *) - | Psw_a (**r store any32 *) - | Psd (**r store int64 *) - | Psd_a (**r store any64 *) - | Pfss (**r store float *) - | Pfsd (**r store 64-bit float *) -. - -Inductive st_instruction : Type := - | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset) - | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) -. - -Coercion PStoreRRO: store_name >-> Funclass. -Coercion PStoreRRR: store_name >-> Funclass. - -(** Arithmetic instructions **) -Inductive arith_name_r : Type := - | Ploadsymbol (id: ident) (ofs: ptrofs) (**r load the address of a symbol *) -. - -Inductive arith_name_rr : Type := - | Pmv (**r register move *) - | Pnegw (**r negate word *) - | Pnegl (**r negate long *) - | Pcvtl2w (**r Convert Long to Word *) - | Psxwd (**r Sign Extend Word to Double Word *) - | Pzxwd (**r Zero Extend Word to Double Word *) - - | Pfabsd (**r float absolute double *) - | Pfabsw (**r float absolute word *) - | Pfnegd (**r float negate double *) - | Pfnegw (**r float negate word *) - | Pfnarrowdw (**r float narrow 64 -> 32 bits *) - | Pfwidenlwd (**r Floating Point widen from 32 bits to 64 bits *) - | Pfloatwrnsz (**r Floating Point conversion from integer (int -> SINGLE) *) - | Pfloatuwrnsz (**r Floating Point conversion from integer (unsigned int -> SINGLE) *) - | Pfloatudrnsz (**r Floating Point Conversion from integer (unsigned long -> float) *) - | Pfloatudrnsz_i32 (**r Floating Point Conversion from integer (unsigned int -> float) *) - | Pfloatdrnsz (**r Floating Point Conversion from integer (long -> float) *) - | Pfloatdrnsz_i32 (**r Floating Point Conversion from integer (int -> float) *) - | Pfixedwrzz (**r Integer conversion from floating point (single -> int) *) - | Pfixeduwrzz (**r Integer conversion from floating point (single -> unsigned int) *) - | Pfixeddrzz (**r Integer conversion from floating point (float -> long) *) - | Pfixedudrzz (**r Integer conversion from floating point (float -> unsigned long) *) - | Pfixeddrzz_i32 (**r Integer conversion from floating point (float -> int) *) - | Pfixedudrzz_i32 (**r Integer conversion from floating point (float -> unsigned int) *) -. - -Inductive arith_name_ri32 : Type := - | Pmake (**r load immediate *) -. - -Inductive arith_name_ri64 : Type := - | Pmakel (**r load immediate long *) -. - -Inductive arith_name_rf32 : Type := - | Pmakefs (**r load immediate single *) -. - -Inductive arith_name_rf64 : Type := - | Pmakef (**r load immediate float *) -. - -Inductive arith_name_rrr : Type := - | Pcompw (it: itest) (**r comparison word *) - | Pcompl (it: itest) (**r comparison long *) - | Pfcompw (ft: ftest) (**r comparison float32 *) - | Pfcompl (ft: ftest) (**r comparison float64 *) - - | Paddw (**r add word *) - | 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 *) - - | 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 *) - | Psral (**r shift right arithmetic long *) - - | Pfaddd (**r float add double *) - | Pfaddw (**r float add word *) - | Pfsbfd (**r float sub double *) - | Pfsbfw (**r float sub word *) - | Pfmuld (**r float multiply double *) - | Pfmulw (**r float multiply word *) -. - -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 *) -. - -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 := - | PArithR (i: arith_name_r) (rd: ireg) - | PArithRR (i: arith_name_rr) (rd rs: ireg) - | PArithRI32 (i: arith_name_ri32) (rd: ireg) (imm: int) - | PArithRI64 (i: arith_name_ri64) (rd: ireg) (imm: int64) - | PArithRF32 (i: arith_name_rf32) (rd: ireg) (imm: float32) - | PArithRF64 (i: arith_name_rf64) (rd: ireg) (imm: float) - | 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. -Coercion PArithRR: arith_name_rr >-> Funclass. -Coercion PArithRI32: arith_name_ri32 >-> Funclass. -Coercion PArithRI64: arith_name_ri64 >-> Funclass. -Coercion PArithRF32: arith_name_rf32 >-> Funclass. -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) - | PLoad (i: ld_instruction) - | PStore (i: st_instruction) - | Pallocframe (sz: Z) (pos: ptrofs) (**r allocate new stack frame *) - | Pfreeframe (sz: Z) (pos: ptrofs) (**r deallocate stack frame and restore previous frame *) - | Pget (rd: ireg) (rs: preg) (**r get system register *) - | Pset (rd: preg) (rs: ireg) (**r set system register *) - | Pnop (**r virtual instruction that does nothing *) -. - -Coercion PLoad: ld_instruction >-> basic. -Coercion PStore: st_instruction >-> basic. -Coercion PArith: ar_instruction >-> basic. - - -Inductive control : Type := - | PExpand (i: ex_instruction) - | PCtlFlow (i: cf_instruction) -. - -Coercion PExpand: ex_instruction >-> control. -Coercion PCtlFlow: cf_instruction >-> control. - - -(** * Definition of a bblock *) - -Ltac exploreInst := - repeat match goal with - | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var - | [ H : OK _ = OK _ |- _ ] => monadInv H - | [ |- context[if ?b then _ else _] ] => destruct b - | [ |- context[match ?m with | _ => _ end] ] => destruct m - | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m - | [ H : bind _ _ = OK _ |- _ ] => monadInv H - | [ H : Error _ = OK _ |- _ ] => inversion H - end. - -Definition non_empty_bblock (body: list basic) (exit: option control): Prop - := body <> nil \/ exit <> None. - -Definition non_empty_body (body: list basic): bool := - match body with - | nil => false - | _ => true - end. - -Definition non_empty_exit (exit: option control): bool := - match exit with - | None => false - | _ => true - end. - -Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit. - -Lemma non_empty_bblock_refl: - forall body exit, - non_empty_bblock body exit <-> - Is_true (non_empty_bblockb body exit). -Proof. - intros. split. - - destruct body; destruct exit. - all: simpl; auto. intros. inversion H; contradiction. - - destruct body; destruct exit. - all: simpl; auto. - all: intros; try (right; discriminate); try (left; discriminate). - contradiction. -Qed. - -Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res, - exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil. - -Definition builtin_aloneb (body: list basic) (exit: option control) := - match exit with - | Some (PExpand (Pbuiltin _ _ _)) => - match body with - | nil => true - | _ => false - end - | _ => true - end. - -Lemma builtin_alone_refl: - forall body exit, - builtin_alone body exit <-> Is_true (builtin_aloneb body exit). -Proof. - intros. split. - - destruct body; destruct exit. - all: simpl; auto. - all: exploreInst; simpl; auto. - unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto. - assert (b :: body = nil). eapply H; eauto. discriminate. - - destruct body; destruct exit. - all: simpl; auto; try constructor. - + exploreInst; try discriminate. - simpl. contradiction. - + intros. discriminate. -Qed. - -Definition wf_bblockb (body: list basic) (exit: option control) := - (non_empty_bblockb body exit) && (builtin_aloneb body exit). - -Definition wf_bblock (body: list basic) (exit: option control) := - non_empty_bblock body exit /\ builtin_alone body exit. - -Lemma wf_bblock_refl: - forall body exit, - wf_bblock body exit <-> Is_true (wf_bblockb body exit). -Proof. - intros. split. - - intros. inv H. apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1. - apply andb_prop_intro. auto. - - intros. apply andb_prop_elim in H. inv H. - apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1. - unfold wf_bblock. split; auto. -Qed. - -(** A bblock is well-formed if he contains at least one instruction, - and if there is a builtin then it must be alone in this bblock. *) - -Record bblock := mk_bblock { - header: list label; - body: list basic; - exit: option control; - correct: Is_true (wf_bblockb body exit) -}. - -Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)). -(* Local Obligation Tactic := bblock_auto_correct. *) - -Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2. -Proof. - destruct b; simpl; auto. - - destruct p1, p2; auto. - - destruct p1. -Qed. - -Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2. -Proof. - destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl. - intros; subst. - rewrite (Istrue_proof_irrelevant _ c1 c2). - auto. -Qed. - - -(* FIXME: redundant with definition in Machblock *) -Definition length_opt {A} (o: option A) : nat := - match o with - | Some o => 1 - | None => 0 - end. - -(* WARNING: the notion of size is not the same than in Machblock ! - We ignore labels here... - The result is in Z to be compatible with operations on PC -*) -Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)). -(* match (body b, exit b) with - | (nil, None) => 1 - | _ => - end. - *) - -Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat. -Proof. - intros. destruct l; try (contradict H; auto; fail). - simpl. omega. -Qed. - -Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0. -Proof. - intros. destruct z; auto. - - contradict H. simpl. apply gt_irrefl. - - apply Zgt_pos_0. - - contradict H. simpl. apply gt_irrefl. -Qed. - -Lemma size_positive (b:bblock): size b > 0. -Proof. - unfold size. destruct b as [hd bdy ex cor]. simpl. - destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega). - inversion cor; contradict H; simpl; auto. -(* rewrite eq. (* inversion COR. *) (* inversion H. *) - - assert ((length b > 0)%nat). apply length_nonil. auto. - omega. - - destruct e; simpl; try omega. contradict H; simpl; auto. - *)Qed. - - -Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. -Next Obligation. - destruct bb; simpl. assumption. -Defined. - -Lemma no_header_size: - forall bb, size (no_header bb) = size bb. -Proof. - intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity. -Qed. - -Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. -Next Obligation. - destruct bb; simpl. assumption. -Defined. - -Lemma stick_header_size: - forall h bb, size (stick_header h bb) = size bb. -Proof. - intros. destruct bb. unfold stick_header. simpl. reflexivity. -Qed. - -Lemma stick_header_no_header: - forall bb, stick_header (header bb) (no_header bb) = bb. -Proof. - intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. -Qed. - - -Definition bblocks := list bblock. - -Fixpoint size_blocks (l: bblocks): Z := - match l with - | nil => 0 - | b :: l => - (size b) + (size_blocks l) - end - . - -Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }. -Definition fundef := AST.fundef function. -Definition program := AST.program fundef unit. - -Inductive instruction : Type := - | PBasic (i: basic) - | PControl (i: control) -. - -Coercion PBasic: basic >-> instruction. -Coercion PControl: control >-> instruction. - -Definition code := list instruction. -Definition bcode := list basic. - -Fixpoint basics_to_code (l: list basic) := - match l with - | nil => nil - | bi::l => (PBasic bi)::(basics_to_code l) - end. - -Fixpoint code_to_basics (c: code) := - match c with - | (PBasic i)::c => - match code_to_basics c with - | None => None - | Some l => Some (i::l) - end - | _::c => None - | nil => Some nil - end. - -Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c. -Proof. - intros. induction c as [|i c]; simpl; auto. - rewrite IHc. auto. -Qed. - -Lemma code_to_basics_dist: - forall c c' l l', - code_to_basics c = Some l -> - code_to_basics c' = Some l' -> - code_to_basics (c ++ c') = Some (l ++ l'). -Proof. - induction c as [|i c]; simpl; auto. - - intros. inv H. simpl. auto. - - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate. - inv H. erewrite IHc; eauto. auto. -Qed. - -(** - Asmblockgen will have to translate a Mach control into a list of instructions of the form - i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction - These functions provide way to extract the basic / control instructions -*) - -Fixpoint extract_basic (c: code) := - match c with - | nil => nil - | PBasic i :: c => i :: (extract_basic c) - | PControl i :: c => nil - end. - -Fixpoint extract_ctl (c: code) := - match c with - | nil => None - | PBasic i :: c => extract_ctl c - | PControl i :: nil => Some i - | PControl i :: _ => None (* if the first found control instruction isn't the last *) - end. - -(** * Utility for Asmblockgen *) - -Program Definition bblock_single_inst (i: instruction) := - match i with - | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |} - | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |} - end. -Next Obligation. - apply wf_bblock_refl. constructor. - right. discriminate. - constructor. -Qed. - -(** This definition is not used anymore *) -(* Program Definition bblock_basic_ctl (c: list basic) (i: option control) := - match i with - | Some i => {| header:=nil; body:=c; exit:=Some i |} - | None => - match c with - | _::_ => {| header:=nil; body:=c; exit:=None |} - | nil => {| header:=nil; body:=Pnop::nil; exit:=None |} - end - end. -Next Obligation. - bblock_auto_correct. -Qed. Next Obligation. - bblock_auto_correct. -Qed. *) - - -(** * Operational semantics *) - -(** The semantics operates over a single mapping from registers - (type [preg]) to values. We maintain - the convention that integer registers are mapped to values of - type [Tint] or [Tlong] (in 64 bit mode), - and float registers to values of type [Tsingle] or [Tfloat]. *) - -Definition regset := Pregmap.t val. - -Definition genv := Genv.t fundef unit. - -Notation "a # b" := (a b) (at level 1, only parsing) : asm. -Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. - -Open Scope asm. - -(** Undefining some registers *) - -Fixpoint undef_regs (l: list preg) (rs: regset) : regset := - match l with - | nil => rs - | r :: l' => undef_regs l' (rs#r <- Vundef) - end. - - -(** Assigning a register pair *) -Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := - match p with - | One r => rs#r <- v - | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v) - end. - -(* TODO: Is it still useful ?? *) - - -(** Assigning multiple registers *) - -(* Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset := - match rl, vl with - | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1) - | _, _ => rs - end. - *) -(** Assigning the result of a builtin *) - -Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := - match res with - | BR r => rs#r <- v - | BR_none => rs - | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) - end. +Require Export Asmvliw. Section RELSEM. - -(** The semantics is purely small-step and defined as a function - from the current state (a register set + a memory state) - to either [Next rs' m'] where [rs'] and [m'] are the updated register - set and memory state after execution of the instruction at [rs#PC], - or [Stuck] if the processor is stuck. *) - -Inductive outcome: Type := - | Next (rs:regset) (m:mem) - | Stuck. -(* Arguments outcome: clear implicits. *) - - -(** ** Arithmetic Expressions (including comparisons) *) - -Inductive signedness: Type := Signed | Unsigned. - -Inductive intsize: Type := Int | Long. - -Definition itest_for_cmp (c: comparison) (s: signedness) := - match c, s with - | Cne, Signed => ITne - | Ceq, Signed => ITeq - | Clt, Signed => ITlt - | Cge, Signed => ITge - | Cle, Signed => ITle - | Cgt, Signed => ITgt - | Cne, Unsigned => ITneu - | Ceq, Unsigned => ITequ - | Clt, Unsigned => ITltu - | Cge, Unsigned => ITgeu - | Cle, Unsigned => ITleu - | Cgt, Unsigned => ITgtu - end. - -Inductive oporder_ftest := - | Normal (ft: ftest) - | Reversed (ft: ftest) -. - -Definition ftest_for_cmp (c: comparison) := - match c with - | Ceq => Normal FToeq - | Cne => Normal FTune - | Clt => Normal FTolt - | Cle => Reversed FToge - | Cgt => Reversed FTolt - | Cge => Normal FToge - end. - -Definition notftest_for_cmp (c: comparison) := - match c with - | Ceq => Normal FTune - | Cne => Normal FToeq - | Clt => Normal FTuge - | Cle => Reversed FTult - | Cgt => Reversed FTuge - | Cge => Normal FTult - end. - -(* CoMPare Signed Words to Zero *) -Definition btest_for_cmpswz (c: comparison) := - match c with - | Cne => BTwnez - | Ceq => BTweqz - | Clt => BTwltz - | Cge => BTwgez - | Cle => BTwlez - | Cgt => BTwgtz - end. - -(* CoMPare Signed Doubles to Zero *) -Definition btest_for_cmpsdz (c: comparison) := - match c with - | Cne => BTdnez - | Ceq => BTdeqz - | Clt => BTdltz - | Cge => BTdgez - | Cle => BTdlez - | Cgt => BTdgtz - end. - -Definition cmp_for_btest (bt: btest) := - match bt with - | BTwnez => (Some Cne, Int) - | BTweqz => (Some Ceq, Int) - | BTwltz => (Some Clt, Int) - | BTwgez => (Some Cge, Int) - | BTwlez => (Some Cle, Int) - | BTwgtz => (Some Cgt, Int) - - | BTdnez => (Some Cne, Long) - | BTdeqz => (Some Ceq, Long) - | BTdltz => (Some Clt, Long) - | BTdgez => (Some Cge, Long) - | BTdlez => (Some Cle, Long) - | BTdgtz => (Some Cgt, Long) - end. - -Definition cmpu_for_btest (bt: btest) := - match bt with - | BTwnez => (Some Cne, Int) - | BTweqz => (Some Ceq, Int) - | BTdnez => (Some Cne, Long) - | BTdeqz => (Some Ceq, Long) - | _ => (None, Int) - end. - - -(* a few lemma on comparisons of unsigned (e.g. pointers) *) - -Definition Val_cmpu_bool cmp v1 v2: option bool := - Val.cmpu_bool (fun _ _ => true) cmp v1 v2. - -Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: - (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b - -> (Val_cmpu_bool cmp v1 v2) = Some b. -Proof. - intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto). -Qed. - -Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2). - -Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val): - Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2) - (Val_cmpu cmp v1 v2). -Proof. - unfold Val.cmpu, Val_cmpu. - remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob; simpl. - - erewrite Val_cmpu_bool_correct; eauto. - econstructor. - - econstructor. -Qed. - -Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val) - := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2). - -Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: - (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b - -> (Val_cmplu_bool cmp v1 v2) = Some b. -Proof. - intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto). -Qed. - -Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2). - -Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val): - Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2)) - (Val_cmplu cmp v1 v2). -Proof. - unfold Val.cmplu, Val_cmplu. - remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob as [b|]; simpl. - - erewrite Val_cmplu_bool_correct; eauto. - simpl. econstructor. - - econstructor. -Qed. - - -(** Comparing integers *) -Definition compare_int (t: itest) (v1 v2: val): val := - match t with - | ITne => Val.cmp Cne v1 v2 - | ITeq => Val.cmp Ceq v1 v2 - | ITlt => Val.cmp Clt v1 v2 - | ITge => Val.cmp Cge v1 v2 - | ITle => Val.cmp Cle v1 v2 - | ITgt => Val.cmp Cgt v1 v2 - | ITneu => Val_cmpu Cne v1 v2 - | ITequ => Val_cmpu Ceq v1 v2 - | ITltu => Val_cmpu Clt v1 v2 - | ITgeu => Val_cmpu Cge v1 v2 - | ITleu => Val_cmpu Cle v1 v2 - | ITgtu => Val_cmpu Cgt v1 v2 - | ITall - | ITnall - | ITany - | ITnone => Vundef - end. - -Definition compare_long (t: itest) (v1 v2: val): val := - let res := match t with - | ITne => Val.cmpl Cne v1 v2 - | ITeq => Val.cmpl Ceq v1 v2 - | ITlt => Val.cmpl Clt v1 v2 - | ITge => Val.cmpl Cge v1 v2 - | ITle => Val.cmpl Cle v1 v2 - | ITgt => Val.cmpl Cgt v1 v2 - | ITneu => Some (Val_cmplu Cne v1 v2) - | ITequ => Some (Val_cmplu Ceq v1 v2) - | ITltu => Some (Val_cmplu Clt v1 v2) - | ITgeu => Some (Val_cmplu Cge v1 v2) - | ITleu => Some (Val_cmplu Cle v1 v2) - | ITgtu => Some (Val_cmplu Cgt v1 v2) - | ITall - | ITnall - | ITany - | ITnone => Some Vundef - end in - match res with - | Some v => v - | None => Vundef - end - . - -Definition compare_single (t: ftest) (v1 v2: val): val := - match t with - | FTone | FTueq => Vundef (* unused *) - | FToeq => Val.cmpfs Ceq v1 v2 - | FTune => Val.cmpfs Cne v1 v2 - | FTolt => Val.cmpfs Clt v1 v2 - | FTuge => Val.notbool (Val.cmpfs Clt v1 v2) - | FToge => Val.cmpfs Cge v1 v2 - | FTult => Val.notbool (Val.cmpfs Cge v1 v2) - end. - -Definition compare_float (t: ftest) (v1 v2: val): val := - match t with - | FTone | FTueq => Vundef (* unused *) - | FToeq => Val.cmpf Ceq v1 v2 - | FTune => Val.cmpf Cne v1 v2 - | FTolt => Val.cmpf Clt v1 v2 - | FTuge => Val.notbool (Val.cmpf Clt v1 v2) - | FToge => Val.cmpf Cge v1 v2 - | FTult => Val.notbool (Val.cmpf Cge v1 v2) - end. - (** Execution of arith instructions *) Variable ge: genv. -Definition arith_eval_r n := - match n with - | Ploadsymbol s ofs => Genv.symbol_address ge s ofs - end -. - -Definition arith_eval_rr n v := - match n with - | Pmv => v - | Pnegw => Val.neg v - | Pnegl => Val.negl v - | Pcvtl2w => Val.loword v - | Psxwd => Val.longofint v - | Pzxwd => Val.longofintu v - | Pfnegd => Val.negf v - | Pfnegw => Val.negfs v - | Pfabsd => Val.absf v - | Pfabsw => Val.absfs v - | Pfnarrowdw => Val.singleoffloat v - | Pfwidenlwd => Val.floatofsingle v - | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end - | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end - | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end - | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end - | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end - | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end - | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end - | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end - | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end - | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end - | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end - | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end - end. - -Definition arith_eval_ri32 n i := - match n with - | Pmake => Vint i - end. - -Definition arith_eval_ri64 n i := - match n with - | Pmakel => Vlong i - end. - -Definition arith_eval_rf32 n i := - match n with - | Pmakefs => Vsingle i - end. - -Definition arith_eval_rf64 n i := - match n with - | Pmakef => Vfloat i - end. - -Definition arith_eval_rrr n v1 v2 := - match n with - | Pcompw c => compare_int c v1 v2 - | Pcompl c => compare_long c v1 v2 - | Pfcompw c => compare_single c v1 v2 - | Pfcompl c => compare_float c v1 v2 - - | Paddw => Val.add 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 - - | 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 - | Psral => Val.shrl v1 v2 - - | Pfaddd => Val.addf v1 v2 - | Pfaddw => Val.addfs v1 v2 - | Pfsbfd => Val.subf v1 v2 - | Pfsbfw => Val.subfs v1 v2 - | Pfmuld => Val.mulf v1 v2 - | Pfmulw => Val.mulfs v1 v2 - end. - -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) - end. - -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) + | PArithR n d => rs#d <- (arith_eval_r ge n) | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s) @@ -1252,18 +68,9 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := (** Auxiliaries for memory accesses *) -Definition eval_offset (ofs: offset) : res ptrofs := - match ofs with - | Ofsimm n => OK n - | Ofslow id delta => - match (Genv.symbol_address ge id delta) with - | Vptr b ofs => OK ofs - | _ => Error (msg "Asmblock.eval_offset") - end - end. Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := - match (eval_offset ofs) with + match (eval_offset ge ofs) with | OK ptr => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with | None => Stuck | Some v => Next (rs#d <- v) m @@ -1278,7 +85,7 @@ Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ir end. Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := - match (eval_offset ofs) with + match (eval_offset ge ofs) with | OK ptr => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with | None => Stuck | Some m' => Next rs m' @@ -1292,31 +99,7 @@ Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: i | Some m' => Next rs m' end. -Definition load_chunk n := - match n with - | Plb => Mint8signed - | Plbu => Mint8unsigned - | Plh => Mint16signed - | Plhu => Mint16unsigned - | Plw => Mint32 - | Plw_a => Many32 - | Pld => Mint64 - | Pld_a => Many64 - | Pfls => Mfloat32 - | Pfld => Mfloat64 - end. -Definition store_chunk n := - match n with - | Psb => Mint8unsigned - | Psh => Mint16unsigned - | Psw => Mint32 - | Psw_a => Many32 - | Psd => Mint64 - | Psd_a => Many64 - | Pfss => Mfloat32 - | Pfsd => Mfloat64 - end. (** * basic instructions *) @@ -1374,55 +157,11 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := end end. -(** Manipulations over the [PC] register: continuing with the next - instruction ([nextblock]) or branching to a label ([goto_label]). *) - -Definition nextblock (b:bblock) (rs: regset) := - rs#PC <- (Val.offset_ptr rs#PC (Ptrofs.repr (size b))). - -(** Looking up bblocks in a code sequence by position. *) -Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock := - match lb with - | nil => None - | b :: il => - if zlt pos 0 then None (* NOTE: It is impossible to branch inside a block *) - else if zeq pos 0 then Some b - else find_bblock (pos - (size b)) il - end. (** Position corresponding to a label *) -(** TODO: redundant w.r.t Machblock *) -Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. -Proof. - apply List.in_dec. - apply Pos.eq_dec. -Qed. - - -(** Note: copy-paste from Machblock *) -Definition is_label (lbl: label) (bb: bblock) : bool := - if in_dec lbl (header bb) then true else false. - -Lemma is_label_correct_true lbl bb: - List.In lbl (header bb) <-> is_label lbl bb = true. -Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. -Qed. -Lemma is_label_correct_false lbl bb: - ~(List.In lbl (header bb)) <-> is_label lbl bb = false. -Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. -Qed. - -(** convert a label into a position in the code *) -Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z := - match lb with - | nil => None - | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb' - end. Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := match label_pos lbl 0 (fn_blocks f) with @@ -1525,67 +264,13 @@ Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcom register is reserved as temporary, to be used by the generated RV32G 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 := - fun r => - if preg_eq r SP - || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) - then rs r - else Vundef. - - -(** Extract the values of the arguments of an external call. - We exploit the calling conventions from module [Conventions], except that - we use RISC-V registers instead of locations. *) - -Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := - | extcall_arg_reg: forall r, - extcall_arg rs m (R r) (rs (preg_of r)) - | extcall_arg_stack: forall ofs ty bofs v, - bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> - Mem.loadv (chunk_of_type ty) m - (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v -> - extcall_arg rs m (S Outgoing ofs ty) v. - -Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := - | extcall_arg_one: forall l v, - extcall_arg rs m l v -> - extcall_arg_pair rs m (One l) v - | extcall_arg_twolong: forall hi lo vhi vlo, - extcall_arg rs m hi vhi -> - extcall_arg rs m lo vlo -> - extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo). - -Definition extcall_arguments - (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args. - -Definition loc_external_result (sg: signature) : rpair preg := - map_rpair preg_of (loc_result sg). -(** Execution of the instruction at [rs PC]. *) -Inductive state: Type := - | State: regset -> mem -> state. + + + +(** Execution of the instruction at [rs PC]. *) (** TODO @@ -1628,24 +313,7 @@ Inductive step: state -> trace -> state -> Prop := End RELSEM. -(** Execution of whole programs. *) - -Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall m0, - let ge := Genv.globalenv p in - let rs0 := - (Pregmap.init Vundef) - # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero) - # SP <- Vnullptr - # RA <- Vnullptr in - Genv.init_mem p = Some m0 -> - initial_state p (State rs0 m0). - -Inductive final_state: state -> int -> Prop := - | final_state_intro: forall rs m r, - rs PC = Vnullptr -> - rs GPR0 = Vint r -> - final_state (State rs m) r. + Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 92630772..32e5e5bb 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -633,7 +633,7 @@ Fixpoint trans_body (b: list basic) : list L.inst := Definition trans_pcincr (sz: Z) (k: L.inst) := (#PC, Op (Control (OIncremPC sz)) (PReg(#PC) @ Enil)) :: k. -Definition trans_block (b: Asmblock.bblock) : L.bblock := +Definition trans_block (b: Asmvliw.bblock) : L.bblock := trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil). Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb. @@ -649,7 +649,7 @@ Qed. Definition state := L.mem. Definition exec := L.run. -Definition match_states (s: Asmblock.state) (s': state) := +Definition match_states (s: Asmvliw.state) (s': state) := let (rs, m) := s in s' pmem = Memstate m /\ forall r, s' (#r) = Val (rs r). @@ -662,7 +662,7 @@ Definition match_outcome (o:outcome) (s: option state) := Notation "a <[ b <- c ]>" := (assign a b c) (at level 102, right associativity). -Definition trans_state (s: Asmblock.state) : state := +Definition trans_state (s: Asmvliw.state) : state := let (rs, m) := s in fun x => if (Pos.eq_dec x pmem) then Memstate m else match (inv_ppos x) with @@ -1537,7 +1537,7 @@ Definition string_of_op (op: P.op): ?? pstring := | Fail => RET (Str "Fail") end. -Definition bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool := +Definition bblock_eq_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := if verb then IDT.verb_bblock_eq_test string_of_name string_of_op (trans_block p1) (trans_block p2) else @@ -1556,7 +1556,7 @@ Hint Resolve bblock_eq_test_correct: wlp. Import UnsafeImpure. -Definition pure_bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock): bool := unsafe_coerce (bblock_eq_test verb p1 p2). +Definition pure_bblock_eq_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_eq_test verb p1 p2). Theorem pure_bblock_eq_test_correct verb p1 p2: forall ge fn, Ge = Genv ge fn -> @@ -1566,7 +1566,7 @@ Proof. apply unsafe_coerce_not_really_correct; eauto. Qed. -Definition bblock_equivb: Asmblock.bblock -> Asmblock.bblock -> bool := pure_bblock_eq_test true. +Definition bblock_equivb: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_eq_test true. Definition bblock_equiv_eq := pure_bblock_eq_test_correct true. @@ -1576,7 +1576,7 @@ End SECT. Module PChk := ParallelChecks L PosPseudoRegSet. -Definition bblock_para_check (p: Asmblock.bblock) : bool := +Definition bblock_para_check (p: Asmvliw.bblock) : bool := PChk.is_parallelizable (trans_block p). Require Import Asmvliw Permutation. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 3260312d..7cd02540 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -1024,14 +1024,14 @@ Definition transl_function (f: Machblock.function) := Pget GPRA RA ::b storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::b lb)). -Definition transf_function (f: Machblock.function) : res Asmblock.function := +Definition transf_function (f: Machblock.function) : res Asmvliw.function := do tf <- transl_function f; if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks)) then Error (msg "code size exceeded") else OK tf. -Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := +Definition transf_fundef (f: Machblock.fundef) : res Asmvliw.fundef := transf_partial_fundef transf_function f. -Definition transf_program (p: Machblock.program) : res Asmblock.program := +Definition transf_program (p: Machblock.program) : res Asmvliw.program := transform_partial_program transf_fundef p. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 70f188ec..a071a9f8 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -19,9 +19,9 @@ Require Import Op Locations Machblock Conventions Asmblock. Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1.
Module MB := Machblock.
-Module AB := Asmblock.
+Module AB := Asmvliw.
-Definition match_prog (p: Machblock.program) (tp: Asmblock.program) :=
+Definition match_prog (p: Machblock.program) (tp: Asmvliw.program) :=
match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
Lemma transf_program_match:
@@ -33,7 +33,7 @@ Qed. Section PRESERVATION.
Variable prog: Machblock.program.
-Variable tprog: Asmblock.program.
+Variable tprog: Asmvliw.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
@@ -318,7 +318,7 @@ Proof. exploit preg_of_injective; eauto. intros; subst r; discriminate.
Qed.
-Inductive match_states: Machblock.state -> Asmblock.state -> Prop :=
+Inductive match_states: Machblock.state -> Asmvliw.state -> Prop :=
| match_states_intro:
forall s fb sp c ep ms m m' rs f tf tc
(STACKS: match_stack ge s)
@@ -328,7 +328,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop := (AG: agree ms sp rs)
(DXP: ep = true -> rs#FP = parent_sp s),
match_states (Machblock.State s fb sp c ms m)
- (Asmblock.State rs m')
+ (Asmvliw.State rs m')
| match_states_call:
forall s fb ms m m' rs
(STACKS: match_stack ge s)
@@ -337,7 +337,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop := (ATPC: rs PC = Vptr fb Ptrofs.zero)
(ATLR: rs RA = parent_ra s),
match_states (Machblock.Callstate s fb ms m)
- (Asmblock.State rs m')
+ (Asmvliw.State rs m')
| match_states_return:
forall s ms m m' rs
(STACKS: match_stack ge s)
@@ -345,7 +345,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop := (AG: agree ms (parent_sp s) rs)
(ATPC: rs PC = parent_ra s),
match_states (Machblock.Returnstate s ms m)
- (Asmblock.State rs m').
+ (Asmvliw.State rs m').
Record codestate :=
Codestate { pstate: state;
@@ -373,7 +373,7 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop := (DXP: (if MB.header bb then ep else false) = true -> rs0#FP = parent_sp s)
,
match_codestate fb (Machblock.State s fb sp (bb::c) ms m)
- {| pstate := (Asmblock.State rs0 m0);
+ {| pstate := (Asmvliw.State rs0 m0);
pheader := (MB.header bb);
pbody1 := tbc;
pbody2 := (extract_basic tbi);
@@ -384,7 +384,7 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop := |}
.
-Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop :=
+Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop :=
| match_asmstate_some:
forall rs f tf tc m tbb ofs ep tbdy tex lhd
(FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
@@ -394,7 +394,7 @@ Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop := (* (HDROK: header tbb = lhd) *)
,
match_asmstate fb
- {| pstate := (Asmblock.State rs m);
+ {| pstate := (Asmvliw.State rs m);
pheader := lhd;
pbody1 := tbdy;
pbody2 := extract_basic tex;
@@ -402,7 +402,7 @@ Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop := fpok := ep;
rem := tc;
cur := Some tbb |}
- (Asmblock.State rs m)
+ (Asmvliw.State rs m)
.
Ltac exploreInst :=
@@ -716,11 +716,11 @@ Theorem step_simu_control: MB.body bb' = nil ->
(forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) ->
Genv.find_funct_ptr tge fb = Some (Internal fn) ->
- pstate cs2 = (Asmblock.State rs2 m2) ->
+ pstate cs2 = (Asmvliw.State rs2 m2) ->
pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex ->
cur cs2 = Some tbb ->
match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 ->
- match_asmstate fb cs2 (Asmblock.State rs1 m1) ->
+ match_asmstate fb cs2 (Asmvliw.State rs1 m1) ->
exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') E0 S'' ->
(exists rs3 m3 rs4 m4,
exec_body tge tbdy2 rs2 m2 = Next rs3 m3
@@ -1775,7 +1775,7 @@ Definition return_address_offset : Machblock.function -> Machblock.code -> ptrof Asmblockgenproof0.return_address_offset.
Theorem transf_program_correct:
- forward_simulation (MB.semantics return_address_offset prog) (AB.semantics tprog).
+ forward_simulation (MB.semantics return_address_offset prog) (Asmblock.semantics tprog).
Proof.
eapply forward_simulation_star with (measure := measure).
- apply senv_preserved.
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index a9f17f33..6310b8ae 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -41,7 +41,7 @@ let wordsize = if Archi.ptr64 then 8 else 4 let align n a = (n + a - 1) land (-a) -let stack_pointer = Asmblock.GPR12 +let stack_pointer = Asmvliw.GPR12 (* Emit instruction sequences that set or offset a register by a constant. *) (* @@ -49,7 +49,7 @@ let stack_pointer = Asmblock.GPR12 List.iter emit (Asmgen.loadimm32 dst n []) *) let expand_addptrofs dst src n = - List.iter emit (basic_to_instruction (Asmblock.PArith (Asmblockgen.addptrofs dst src n)) :: []) + List.iter emit (basic_to_instruction (Asmvliw.PArith (Asmblockgen.addptrofs dst src n)) :: []) let expand_storeind_ptr src base ofs = List.iter emit (basic_to_instruction (Asmblockgen.storeind_ptr src base ofs) :: []) let expand_loadind_ptr dst base ofs = @@ -65,7 +65,7 @@ let expand_loadind_ptr dst base ofs = (* Fix-up code around calls to variadic functions. Floating-point arguments residing in FP registers need to be moved to integer registers. *) -let int_param_regs = let open Asmblock in [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7; GPR8; GPR9; GPR10; GPR11 |] +let int_param_regs = let open Asmvliw in [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7; GPR8; GPR9; GPR10; GPR11 |] (* let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |] *) let float_param_regs = [| |] @@ -131,7 +131,7 @@ let emit_move dst r = (* FIXME DMonniaux this is probably not complete *) let get_builtin_arg dst arg = match arg with - | BA (Asmblock.IR reg) -> emit_move dst reg + | BA (Asmvliw.IR reg) -> emit_move dst reg | BA (ireg) -> failwith "get_builtin_arg: BA_int(not ireg)" | BA_int _ -> failwith "get_builtin_arg: BA_int" | BA_long _ -> failwith "get_builtin_arg: BA_long" @@ -147,9 +147,9 @@ let get_builtin_arg dst arg = (* FIXME DMonniaux this is really suboptimal (byte per byte) *) let expand_builtin_memcpy_big sz al src dst = assert (sz > Z.zero); - let dstptr = Asmblock.GPR62 - and srcptr = Asmblock.GPR63 - and tmpbuf = Asmblock.GPR61 in + let dstptr = Asmvliw.GPR62 + and srcptr = Asmvliw.GPR63 + and tmpbuf = Asmvliw.GPR61 in get_builtin_arg dstptr dst; get_builtin_arg srcptr src; emit (Pmake (tmpbuf, sz)); @@ -157,10 +157,10 @@ let expand_builtin_memcpy_big sz al src dst = let lbl = new_label() in emit (Ploopdo (tmpbuf, lbl)); emit Psemi; - emit (Plb (tmpbuf, srcptr, AOff (Asmblock.Ofsimm Z.zero))); + emit (Plb (tmpbuf, srcptr, AOff (Asmvliw.Ofsimm Z.zero))); emit (Paddil (srcptr, srcptr, Z.one)); emit Psemi; - emit (Psb (tmpbuf, dstptr, AOff (Asmblock.Ofsimm Z.zero))); + emit (Psb (tmpbuf, dstptr, AOff (Asmvliw.Ofsimm Z.zero))); emit (Paddil (dstptr, dstptr, Z.one)); emit Psemi; emit (Plabel lbl);; @@ -175,41 +175,41 @@ let expand_builtin_memcpy sz al args = (* FIXME probably need to check for size of displacement *) let expand_builtin_vload_common chunk base ofs res = match chunk, res with - | Mint8unsigned, BR(Asmblock.IR res) -> - emit (Plbu (res, base, AOff (Asmblock.Ofsimm ofs))) - | Mint8signed, BR(Asmblock.IR res) -> - emit (Plb (res, base, AOff (Asmblock.Ofsimm ofs))) - | Mint16unsigned, BR(Asmblock.IR res) -> - emit (Plhu (res, base, AOff (Asmblock.Ofsimm ofs))) - | Mint16signed, BR(Asmblock.IR res) -> - emit (Plh (res, base, AOff (Asmblock.Ofsimm ofs))) - | Mint32, BR(Asmblock.IR res) -> - emit (Plw (res, base, AOff (Asmblock.Ofsimm ofs))) - | Mint64, BR(Asmblock.IR res) -> - emit (Pld (res, base, AOff (Asmblock.Ofsimm ofs))) - | Mint64, BR_splitlong(BR(Asmblock.IR res1), BR(Asmblock.IR res2)) -> + | Mint8unsigned, BR(Asmvliw.IR res) -> + emit (Plbu (res, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint8signed, BR(Asmvliw.IR res) -> + emit (Plb (res, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint16unsigned, BR(Asmvliw.IR res) -> + emit (Plhu (res, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint16signed, BR(Asmvliw.IR res) -> + emit (Plh (res, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint32, BR(Asmvliw.IR res) -> + emit (Plw (res, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint64, BR(Asmvliw.IR res) -> + emit (Pld (res, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint64, BR_splitlong(BR(Asmvliw.IR res1), BR(Asmvliw.IR res2)) -> let ofs' = Ptrofs.add ofs _4 in if base <> res2 then begin - emit (Plw (res2, base, AOff (Asmblock.Ofsimm ofs))); - emit (Plw (res1, base, AOff (Asmblock.Ofsimm ofs'))) + emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs))); + emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs'))) end else begin - emit (Plw (res1, base, AOff (Asmblock.Ofsimm ofs'))); - emit (Plw (res2, base, AOff (Asmblock.Ofsimm ofs))) + emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs'))); + emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs))) end - | Mfloat32, BR(Asmblock.IR res) -> - emit (Pfls (res, base, AOff (Asmblock.Ofsimm ofs))) - | Mfloat64, BR(Asmblock.IR res) -> - emit (Pfld (res, base, AOff (Asmblock.Ofsimm ofs))) + | Mfloat32, BR(Asmvliw.IR res) -> + emit (Pfls (res, base, AOff (Asmvliw.Ofsimm ofs))) + | Mfloat64, BR(Asmvliw.IR res) -> + emit (Pfld (res, base, AOff (Asmvliw.Ofsimm ofs))) | _ -> assert false let expand_builtin_vload chunk args res = match args with - | [BA(Asmblock.IR addr)] -> + | [BA(Asmvliw.IR addr)] -> expand_builtin_vload_common chunk addr _0 res | [BA_addrstack ofs] -> expand_builtin_vload_common chunk stack_pointer ofs res - | [BA_addptr(BA(Asmblock.IR addr), (BA_int ofs | BA_long ofs))] -> + | [BA_addptr(BA(Asmvliw.IR addr), (BA_int ofs | BA_long ofs))] -> expand_builtin_vload_common chunk addr ofs res | _ -> assert false @@ -217,32 +217,32 @@ let expand_builtin_vload chunk args res = let expand_builtin_vstore_common chunk base ofs src = match chunk, src with - | (Mint8signed | Mint8unsigned), BA(Asmblock.IR src) -> - emit (Psb (src, base, AOff (Asmblock.Ofsimm ofs))) - | (Mint16signed | Mint16unsigned), BA(Asmblock.IR src) -> - emit (Psh (src, base, AOff (Asmblock.Ofsimm ofs))) - | Mint32, BA(Asmblock.IR src) -> - emit (Psw (src, base, AOff (Asmblock.Ofsimm ofs))) - | Mint64, BA(Asmblock.IR src) -> - emit (Psd (src, base, AOff (Asmblock.Ofsimm ofs))) - | Mint64, BA_splitlong(BA(Asmblock.IR src1), BA(Asmblock.IR src2)) -> + | (Mint8signed | Mint8unsigned), BA(Asmvliw.IR src) -> + emit (Psb (src, base, AOff (Asmvliw.Ofsimm ofs))) + | (Mint16signed | Mint16unsigned), BA(Asmvliw.IR src) -> + emit (Psh (src, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint32, BA(Asmvliw.IR src) -> + emit (Psw (src, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint64, BA(Asmvliw.IR src) -> + emit (Psd (src, base, AOff (Asmvliw.Ofsimm ofs))) + | Mint64, BA_splitlong(BA(Asmvliw.IR src1), BA(Asmvliw.IR src2)) -> let ofs' = Ptrofs.add ofs _4 in - emit (Psw (src2, base, AOff (Asmblock.Ofsimm ofs))); - emit (Psw (src1, base, AOff (Asmblock.Ofsimm ofs'))) - | Mfloat32, BA(Asmblock.IR src) -> - emit (Pfss (src, base, AOff (Asmblock.Ofsimm ofs))) - | Mfloat64, BA(Asmblock.IR src) -> - emit (Pfsd (src, base, AOff (Asmblock.Ofsimm ofs))) + emit (Psw (src2, base, AOff (Asmvliw.Ofsimm ofs))); + emit (Psw (src1, base, AOff (Asmvliw.Ofsimm ofs'))) + | Mfloat32, BA(Asmvliw.IR src) -> + emit (Pfss (src, base, AOff (Asmvliw.Ofsimm ofs))) + | Mfloat64, BA(Asmvliw.IR src) -> + emit (Pfsd (src, base, AOff (Asmvliw.Ofsimm ofs))) | _ -> assert false let expand_builtin_vstore chunk args = match args with - | [BA(Asmblock.IR addr); src] -> + | [BA(Asmvliw.IR addr); src] -> expand_builtin_vstore_common chunk addr _0 src | [BA_addrstack ofs; src] -> expand_builtin_vstore_common chunk stack_pointer ofs src - | [BA_addptr(BA(Asmblock.IR addr), (BA_int ofs | BA_long ofs)); src] -> + | [BA_addptr(BA(Asmvliw.IR addr), (BA_int ofs | BA_long ofs)); src] -> expand_builtin_vstore_common chunk addr ofs src | _ -> assert false @@ -265,7 +265,7 @@ let arguments_size sg = let _nbregargs_ = 12 let _alignment_ = 8 -let save_arguments first_reg base_ofs = let open Asmblock in +let save_arguments first_reg base_ofs = let open Asmvliw in for i = first_reg to (_nbregargs_ - 1) do begin expand_storeind_ptr int_param_regs.(i) @@ -281,9 +281,9 @@ match !vararg_start_ofs with | None -> invalid_arg "Fatal error: va_start used in non-vararg function" | Some ofs -> - expand_addptrofs Asmblock.GPR32 stack_pointer (Ptrofs.repr ofs); + expand_addptrofs Asmvliw.GPR32 stack_pointer (Ptrofs.repr ofs); emit Psemi; - expand_storeind_ptr Asmblock.GPR32 r Ptrofs.zero + expand_storeind_ptr Asmvliw.GPR32 r Ptrofs.zero (* Auxiliary for 64-bit integer arithmetic built-ins. They expand to two instructions, one computing the low 32 bits of the result, @@ -348,7 +348,7 @@ let expand_bswap64 d s = assert false (* Handling of compiler-inlined builtins *) -let expand_builtin_inline name args res = let open Asmblock in +let expand_builtin_inline name args res = let open Asmvliw in match name, args, res with (* Synchronization *) | "__builtin_membar", [], _ -> @@ -376,14 +376,14 @@ let expand_instruction instr = match instr with | Pallocframe (sz, ofs) -> let sg = get_current_function_sig() in - emit (Pmv (Asmblock.GPR17, stack_pointer)); + emit (Pmv (Asmvliw.GPR17, stack_pointer)); if sg.sig_cc.cc_vararg then begin let n = arguments_size sg in let extra_sz = if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in let full_sz = Z.add sz (Z.of_uint extra_sz) in expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg full_sz)); emit Psemi; - expand_storeind_ptr Asmblock.GPR17 stack_pointer ofs; + expand_storeind_ptr Asmvliw.GPR17 stack_pointer ofs; emit Psemi; let va_ofs = sz in @@ -393,7 +393,7 @@ let expand_instruction instr = end else begin expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg sz)); emit Psemi; - expand_storeind_ptr Asmblock.GPR17 stack_pointer ofs; + expand_storeind_ptr Asmvliw.GPR17 stack_pointer ofs; emit Psemi; vararg_start_ofs := None end @@ -476,7 +476,7 @@ let expand_instruction instr = (* NOTE: Dwarf register maps for RV32G are not yet specified officially. This is just a placeholder. *) -let int_reg_to_dwarf = let open Asmblock in function +let int_reg_to_dwarf = let open Asmvliw in function | GPR0 -> 1 | GPR1 -> 2 | GPR2 -> 3 | GPR3 -> 4 | GPR4 -> 5 | GPR5 -> 6 | GPR6 -> 7 | GPR7 -> 8 | GPR8 -> 9 | GPR9 -> 10 | GPR10 -> 11 | GPR11 -> 12 | GPR12 -> 13 | GPR13 -> 14 | GPR14 -> 15 @@ -491,7 +491,7 @@ let int_reg_to_dwarf = let open Asmblock in function | GPR55 -> 56 | GPR56 -> 57 | GPR57 -> 58 | GPR58 -> 59 | GPR59 -> 60 | GPR60 -> 61 | GPR61 -> 62 | GPR62 -> 63 | GPR63 -> 64 -let preg_to_dwarf = let open Asmblock in function +let preg_to_dwarf = let open Asmvliw in function | IR r -> int_reg_to_dwarf r | RA -> 65 (* FIXME - No idea what is $ra DWARF number in k1-gdb *) | _ -> assert false diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index c15a33af..d56a7a84 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -31,9 +31,814 @@ Require Import Locations. Require Stacklayout. Require Import Conventions. Require Import Errors. -Require Export Asmblock. Require Import Sorting.Permutation. +(** * Abstract syntax *) + +(** General Purpose registers. +*) + +Inductive gpreg: Type := + | GPR0: gpreg | GPR1: gpreg | GPR2: gpreg | GPR3: gpreg | GPR4: gpreg + | GPR5: gpreg | GPR6: gpreg | GPR7: gpreg | GPR8: gpreg | GPR9: gpreg + | GPR10: gpreg | GPR11: gpreg | GPR12: gpreg | GPR13: gpreg | GPR14: gpreg + | GPR15: gpreg | GPR16: gpreg | GPR17: gpreg | GPR18: gpreg | GPR19: gpreg + | GPR20: gpreg | GPR21: gpreg | GPR22: gpreg | GPR23: gpreg | GPR24: gpreg + | GPR25: gpreg | GPR26: gpreg | GPR27: gpreg | GPR28: gpreg | GPR29: gpreg + | GPR30: gpreg | GPR31: gpreg | GPR32: gpreg | GPR33: gpreg | GPR34: gpreg + | GPR35: gpreg | GPR36: gpreg | GPR37: gpreg | GPR38: gpreg | GPR39: gpreg + | GPR40: gpreg | GPR41: gpreg | GPR42: gpreg | GPR43: gpreg | GPR44: gpreg + | GPR45: gpreg | GPR46: gpreg | GPR47: gpreg | GPR48: gpreg | GPR49: gpreg + | GPR50: gpreg | GPR51: gpreg | GPR52: gpreg | GPR53: gpreg | GPR54: gpreg + | GPR55: gpreg | GPR56: gpreg | GPR57: gpreg | GPR58: gpreg | GPR59: gpreg + | GPR60: gpreg | GPR61: gpreg | GPR62: gpreg | GPR63: gpreg. + +Definition ireg := gpreg. +Definition freg := gpreg. + +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. + +(** We model the following registers of the RISC-V architecture. *) + +(** basic register *) +Inductive preg: Type := + | IR: gpreg -> preg (**r integer general purpose registers *) + | RA: preg + | PC: preg + . + +Coercion IR: gpreg >-> preg. + +Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. +Proof. decide equality. apply ireg_eq. Defined. + +Module PregEq. + Definition t := preg. + Definition eq := preg_eq. +End PregEq. + +Module Pregmap := EMap(PregEq). + +(** Conventional names for stack pointer ([SP]) and return address ([RA]). *) + +Notation "'SP'" := GPR12 (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. + +Inductive btest: Type := + | BTdnez (**r Double Not Equal to Zero *) + | BTdeqz (**r Double Equal to Zero *) + | BTdltz (**r Double Less Than Zero *) + | BTdgez (**r Double Greater Than or Equal to Zero *) + | BTdlez (**r Double Less Than or Equal to Zero *) + | BTdgtz (**r Double Greater Than Zero *) +(*| BTodd (**r Odd (LSB Set) *) + | BTeven (**r Even (LSB Clear) *) +*)| BTwnez (**r Word Not Equal to Zero *) + | BTweqz (**r Word Equal to Zero *) + | BTwltz (**r Word Less Than Zero *) + | BTwgez (**r Word Greater Than or Equal to Zero *) + | BTwlez (**r Word Less Than or Equal to Zero *) + | BTwgtz (**r Word Greater Than Zero *) + . + +Inductive itest: Type := + | ITne (**r Not Equal *) + | ITeq (**r Equal *) + | ITlt (**r Less Than *) + | ITge (**r Greater Than or Equal *) + | ITle (**r Less Than or Equal *) + | ITgt (**r Greater Than *) + | ITneu (**r Unsigned Not Equal *) + | ITequ (**r Unsigned Equal *) + | ITltu (**r Less Than Unsigned *) + | ITgeu (**r Greater Than or Equal Unsigned *) + | ITleu (**r Less Than or Equal Unsigned *) + | ITgtu (**r Greater Than Unsigned *) + (* Not used yet *) + | ITall (**r All Bits Set in Mask *) + | ITnall (**r Not All Bits Set in Mask *) + | ITany (**r Any Bits Set in Mask *) + | ITnone (**r Not Any Bits Set in Mask *) + . + +Inductive ftest: Type := + | FTone (**r Ordered and Not Equal *) + | FTueq (**r Unordered or Equal *) + | FToeq (**r Ordered and Equal *) + | FTune (**r Unordered or Not Equal *) + | FTolt (**r Ordered and Less Than *) + | FTuge (**r Unordered or Greater Than or Equal *) + | FToge (**r Ordered and Greater Than or Equal *) + | FTult (**r Unordered or Less Than *) + . + +(** Offsets for load and store instructions. An offset is either an + immediate integer or the low part of a symbol. *) + +Inductive offset : Type := + | Ofsimm (ofs: ptrofs) + | Ofslow (id: ident) (ofs: ptrofs). + +(** We model a subset of the K1c instruction set. In particular, we do not + support floats yet. + + Although it is possible to use the 32-bits mode, for now we don't support it. + + We follow a design close to the one used for the Risc-V port: one set of + pseudo-instructions for 32-bit integer arithmetic, with suffix W, another + set for 64-bit integer arithmetic, with suffix L. + + When mapping to actual instructions, the OCaml code in TargetPrinter.ml + throws an error if we are not in 64-bits mode. +*) + +(** * Instructions *) + +Definition label := positive. + +(* FIXME - rewrite the comment *) +(** A note on immediates: there are various constraints on immediate + operands to K1c instructions. We do not attempt to capture these + restrictions in the abstract syntax nor in the semantics. The + assembler will emit an error if immediate operands exceed the + representable range. Of course, our K1c generator (file + [Asmgen]) is careful to respect this range. *) + +(** Instructions to be expanded in control-flow +*) +Inductive ex_instruction : Type := + (* Pseudo-instructions *) +(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *) + | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) + + | Pbuiltin: external_function -> list (builtin_arg preg) + -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) +. + +(** FIXME: comment not up to date ! + + + The pseudo-instructions are the following: + +- [Ploadsymbol]: load the address of a symbol in an integer register. + Expands to the [la] assembler pseudo-instruction, which does the right + thing even if we are in PIC mode. + +- [Pallocframe sz pos]: in the formal semantics, this + pseudo-instruction allocates a memory block with bounds [0] and + [sz], stores the value of the stack pointer at offset [pos] in this + block, and sets the stack pointer to the address of the bottom of + this block. + In the printed ASM assembly code, this allocation is: +<< + mv x30, sp + sub sp, sp, #sz + sw x30, #pos(sp) +>> + This cannot be expressed in our memory model, which does not reflect + the fact that stack frames are adjacent and allocated/freed + following a stack discipline. + +- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction + reads the word at [pos] of the block pointed by the stack pointer, + frees this block, and sets the stack pointer to the value read. + In the printed ASM assembly code, this freeing is just an increment of [sp]: +<< + add sp, sp, #sz +>> + Again, our memory model cannot comprehend that this operation + frees (logically) the current stack frame. + +- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table + as follows: +<< + la x31, table + add x31, x31, reg + jr x31 +table: .long table[0], table[1], ... +>> + Note that [reg] contains 4 times the index of the desired table entry. +*) + +(** Control Flow instructions *) +Inductive cf_instruction : Type := + | Pret (**r return *) + | Pcall (l: label) (**r function call *) + | Picall (r: ireg) (**r function call on register value *) + | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *) + + (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *) + | Pgoto (l: label) (**r goto *) + | Pigoto (r: ireg) (**r goto from register *) + | Pj_l (l: label) (**r jump to label *) + + (* Conditional branches *) + | 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 *) +. + +(** Loads **) +Inductive load_name : Type := + | Plb (**r load byte *) + | Plbu (**r load byte unsigned *) + | Plh (**r load half word *) + | Plhu (**r load half word unsigned *) + | Plw (**r load int32 *) + | Plw_a (**r load any32 *) + | Pld (**r load int64 *) + | Pld_a (**r load any64 *) + | Pfls (**r load float *) + | Pfld (**r load 64-bit float *) +. + +Inductive ld_instruction : Type := + | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset) + | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) +. + +Coercion PLoadRRO: load_name >-> Funclass. +Coercion PLoadRRR: load_name >-> Funclass. + +(** Stores **) +Inductive store_name : Type := + | Psb (**r store byte *) + | Psh (**r store half byte *) + | Psw (**r store int32 *) + | Psw_a (**r store any32 *) + | Psd (**r store int64 *) + | Psd_a (**r store any64 *) + | Pfss (**r store float *) + | Pfsd (**r store 64-bit float *) +. + +Inductive st_instruction : Type := + | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset) + | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) +. + +Coercion PStoreRRO: store_name >-> Funclass. +Coercion PStoreRRR: store_name >-> Funclass. + +(** Arithmetic instructions **) +Inductive arith_name_r : Type := + | Ploadsymbol (id: ident) (ofs: ptrofs) (**r load the address of a symbol *) +. + +Inductive arith_name_rr : Type := + | Pmv (**r register move *) + | Pnegw (**r negate word *) + | Pnegl (**r negate long *) + | Pcvtl2w (**r Convert Long to Word *) + | Psxwd (**r Sign Extend Word to Double Word *) + | Pzxwd (**r Zero Extend Word to Double Word *) + + | Pfabsd (**r float absolute double *) + | Pfabsw (**r float absolute word *) + | Pfnegd (**r float negate double *) + | Pfnegw (**r float negate word *) + | Pfnarrowdw (**r float narrow 64 -> 32 bits *) + | Pfwidenlwd (**r Floating Point widen from 32 bits to 64 bits *) + | Pfloatwrnsz (**r Floating Point conversion from integer (int -> SINGLE) *) + | Pfloatuwrnsz (**r Floating Point conversion from integer (unsigned int -> SINGLE) *) + | Pfloatudrnsz (**r Floating Point Conversion from integer (unsigned long -> float) *) + | Pfloatudrnsz_i32 (**r Floating Point Conversion from integer (unsigned int -> float) *) + | Pfloatdrnsz (**r Floating Point Conversion from integer (long -> float) *) + | Pfloatdrnsz_i32 (**r Floating Point Conversion from integer (int -> float) *) + | Pfixedwrzz (**r Integer conversion from floating point (single -> int) *) + | Pfixeduwrzz (**r Integer conversion from floating point (single -> unsigned int) *) + | Pfixeddrzz (**r Integer conversion from floating point (float -> long) *) + | Pfixedudrzz (**r Integer conversion from floating point (float -> unsigned long) *) + | Pfixeddrzz_i32 (**r Integer conversion from floating point (float -> int) *) + | Pfixedudrzz_i32 (**r Integer conversion from floating point (float -> unsigned int) *) +. + +Inductive arith_name_ri32 : Type := + | Pmake (**r load immediate *) +. + +Inductive arith_name_ri64 : Type := + | Pmakel (**r load immediate long *) +. + +Inductive arith_name_rf32 : Type := + | Pmakefs (**r load immediate single *) +. + +Inductive arith_name_rf64 : Type := + | Pmakef (**r load immediate float *) +. + +Inductive arith_name_rrr : Type := + | Pcompw (it: itest) (**r comparison word *) + | Pcompl (it: itest) (**r comparison long *) + | Pfcompw (ft: ftest) (**r comparison float32 *) + | Pfcompl (ft: ftest) (**r comparison float64 *) + + | Paddw (**r add word *) + | 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 *) + + | 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 *) + | Psral (**r shift right arithmetic long *) + + | Pfaddd (**r float add double *) + | Pfaddw (**r float add word *) + | Pfsbfd (**r float sub double *) + | Pfsbfw (**r float sub word *) + | Pfmuld (**r float multiply double *) + | Pfmulw (**r float multiply word *) +. + +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 *) +. + +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 := + | PArithR (i: arith_name_r) (rd: ireg) + | PArithRR (i: arith_name_rr) (rd rs: ireg) + | PArithRI32 (i: arith_name_ri32) (rd: ireg) (imm: int) + | PArithRI64 (i: arith_name_ri64) (rd: ireg) (imm: int64) + | PArithRF32 (i: arith_name_rf32) (rd: ireg) (imm: float32) + | PArithRF64 (i: arith_name_rf64) (rd: ireg) (imm: float) + | 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. +Coercion PArithRR: arith_name_rr >-> Funclass. +Coercion PArithRI32: arith_name_ri32 >-> Funclass. +Coercion PArithRI64: arith_name_ri64 >-> Funclass. +Coercion PArithRF32: arith_name_rf32 >-> Funclass. +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) + | PLoad (i: ld_instruction) + | PStore (i: st_instruction) + | Pallocframe (sz: Z) (pos: ptrofs) (**r allocate new stack frame *) + | Pfreeframe (sz: Z) (pos: ptrofs) (**r deallocate stack frame and restore previous frame *) + | Pget (rd: ireg) (rs: preg) (**r get system register *) + | Pset (rd: preg) (rs: ireg) (**r set system register *) + | Pnop (**r virtual instruction that does nothing *) +. + +Coercion PLoad: ld_instruction >-> basic. +Coercion PStore: st_instruction >-> basic. +Coercion PArith: ar_instruction >-> basic. + + +Inductive control : Type := + | PExpand (i: ex_instruction) + | PCtlFlow (i: cf_instruction) +. + +Coercion PExpand: ex_instruction >-> control. +Coercion PCtlFlow: cf_instruction >-> control. + + +(** * Definition of a bblock *) + +Ltac exploreInst := + repeat match goal with + | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var + | [ H : OK _ = OK _ |- _ ] => monadInv H + | [ |- context[if ?b then _ else _] ] => destruct b + | [ |- context[match ?m with | _ => _ end] ] => destruct m + | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m + | [ H : bind _ _ = OK _ |- _ ] => monadInv H + | [ H : Error _ = OK _ |- _ ] => inversion H + end. + +Definition non_empty_bblock (body: list basic) (exit: option control): Prop + := body <> nil \/ exit <> None. + +Definition non_empty_body (body: list basic): bool := + match body with + | nil => false + | _ => true + end. + +Definition non_empty_exit (exit: option control): bool := + match exit with + | None => false + | _ => true + end. + +Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit. + +Lemma non_empty_bblock_refl: + forall body exit, + non_empty_bblock body exit <-> + Is_true (non_empty_bblockb body exit). +Proof. + intros. split. + - destruct body; destruct exit. + all: simpl; auto. intros. inversion H; contradiction. + - destruct body; destruct exit. + all: simpl; auto. + all: intros; try (right; discriminate); try (left; discriminate). + contradiction. +Qed. + +Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res, + exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil. + +Definition builtin_aloneb (body: list basic) (exit: option control) := + match exit with + | Some (PExpand (Pbuiltin _ _ _)) => + match body with + | nil => true + | _ => false + end + | _ => true + end. + +Lemma builtin_alone_refl: + forall body exit, + builtin_alone body exit <-> Is_true (builtin_aloneb body exit). +Proof. + intros. split. + - destruct body; destruct exit. + all: simpl; auto. + all: exploreInst; simpl; auto. + unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto. + assert (b :: body = nil). eapply H; eauto. discriminate. + - destruct body; destruct exit. + all: simpl; auto; try constructor. + + exploreInst; try discriminate. + simpl. contradiction. + + intros. discriminate. +Qed. + +Definition wf_bblockb (body: list basic) (exit: option control) := + (non_empty_bblockb body exit) && (builtin_aloneb body exit). + +Definition wf_bblock (body: list basic) (exit: option control) := + non_empty_bblock body exit /\ builtin_alone body exit. + +Lemma wf_bblock_refl: + forall body exit, + wf_bblock body exit <-> Is_true (wf_bblockb body exit). +Proof. + intros. split. + - intros. inv H. apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1. + apply andb_prop_intro. auto. + - intros. apply andb_prop_elim in H. inv H. + apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1. + unfold wf_bblock. split; auto. +Qed. + +(** A bblock is well-formed if he contains at least one instruction, + and if there is a builtin then it must be alone in this bblock. *) + +Record bblock := mk_bblock { + header: list label; + body: list basic; + exit: option control; + correct: Is_true (wf_bblockb body exit) +}. + +Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)). +(* Local Obligation Tactic := bblock_auto_correct. *) + +Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2. +Proof. + destruct b; simpl; auto. + - destruct p1, p2; auto. + - destruct p1. +Qed. + +Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2. +Proof. + destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl. + intros; subst. + rewrite (Istrue_proof_irrelevant _ c1 c2). + auto. +Qed. + + +(* FIXME: redundant with definition in Machblock *) +Definition length_opt {A} (o: option A) : nat := + match o with + | Some o => 1 + | None => 0 + end. + +(* WARNING: the notion of size is not the same than in Machblock ! + We ignore labels here... + The result is in Z to be compatible with operations on PC +*) +Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)). +(* match (body b, exit b) with + | (nil, None) => 1 + | _ => + end. + *) + +Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat. +Proof. + intros. destruct l; try (contradict H; auto; fail). + simpl. omega. +Qed. + +Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0. +Proof. + intros. destruct z; auto. + - contradict H. simpl. apply gt_irrefl. + - apply Zgt_pos_0. + - contradict H. simpl. apply gt_irrefl. +Qed. + +Lemma size_positive (b:bblock): size b > 0. +Proof. + unfold size. destruct b as [hd bdy ex cor]. simpl. + destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega). + inversion cor; contradict H; simpl; auto. +(* rewrite eq. (* inversion COR. *) (* inversion H. *) + - assert ((length b > 0)%nat). apply length_nonil. auto. + omega. + - destruct e; simpl; try omega. contradict H; simpl; auto. + *)Qed. + + +Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; simpl. assumption. +Defined. + +Lemma no_header_size: + forall bb, size (no_header bb) = size bb. +Proof. + intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity. +Qed. + +Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; simpl. assumption. +Defined. + +Lemma stick_header_size: + forall h bb, size (stick_header h bb) = size bb. +Proof. + intros. destruct bb. unfold stick_header. simpl. reflexivity. +Qed. + +Lemma stick_header_no_header: + forall bb, stick_header (header bb) (no_header bb) = bb. +Proof. + intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. +Qed. + + +Definition bblocks := list bblock. + +Fixpoint size_blocks (l: bblocks): Z := + match l with + | nil => 0 + | b :: l => + (size b) + (size_blocks l) + end + . + +Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }. +Definition fundef := AST.fundef function. +Definition program := AST.program fundef unit. + +Inductive instruction : Type := + | PBasic (i: basic) + | PControl (i: control) +. + +Coercion PBasic: basic >-> instruction. +Coercion PControl: control >-> instruction. + +Definition code := list instruction. +Definition bcode := list basic. + +Fixpoint basics_to_code (l: list basic) := + match l with + | nil => nil + | bi::l => (PBasic bi)::(basics_to_code l) + end. + +Fixpoint code_to_basics (c: code) := + match c with + | (PBasic i)::c => + match code_to_basics c with + | None => None + | Some l => Some (i::l) + end + | _::c => None + | nil => Some nil + end. + +Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c. +Proof. + intros. induction c as [|i c]; simpl; auto. + rewrite IHc. auto. +Qed. + +Lemma code_to_basics_dist: + forall c c' l l', + code_to_basics c = Some l -> + code_to_basics c' = Some l' -> + code_to_basics (c ++ c') = Some (l ++ l'). +Proof. + induction c as [|i c]; simpl; auto. + - intros. inv H. simpl. auto. + - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate. + inv H. erewrite IHc; eauto. auto. +Qed. + +(** + Asmblockgen will have to translate a Mach control into a list of instructions of the form + i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction + These functions provide way to extract the basic / control instructions +*) + +Fixpoint extract_basic (c: code) := + match c with + | nil => nil + | PBasic i :: c => i :: (extract_basic c) + | PControl i :: c => nil + end. + +Fixpoint extract_ctl (c: code) := + match c with + | nil => None + | PBasic i :: c => extract_ctl c + | PControl i :: nil => Some i + | PControl i :: _ => None (* if the first found control instruction isn't the last *) + end. + +(** * Utility for Asmblockgen *) + +Program Definition bblock_single_inst (i: instruction) := + match i with + | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |} + | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |} + end. +Next Obligation. + apply wf_bblock_refl. constructor. + right. discriminate. + constructor. +Qed. + +(** This definition is not used anymore *) +(* Program Definition bblock_basic_ctl (c: list basic) (i: option control) := + match i with + | Some i => {| header:=nil; body:=c; exit:=Some i |} + | None => + match c with + | _::_ => {| header:=nil; body:=c; exit:=None |} + | nil => {| header:=nil; body:=Pnop::nil; exit:=None |} + end + end. +Next Obligation. + bblock_auto_correct. +Qed. Next Obligation. + bblock_auto_correct. +Qed. *) + + +(** * Operational semantics *) + +(** The semantics operates over a single mapping from registers + (type [preg]) to values. We maintain + the convention that integer registers are mapped to values of + type [Tint] or [Tlong] (in 64 bit mode), + and float registers to values of type [Tsingle] or [Tfloat]. *) + +Definition regset := Pregmap.t val. + +Definition genv := Genv.t fundef unit. + +Notation "a # b" := (a b) (at level 1, only parsing) : asm. +Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. + +Open Scope asm. + +(** Undefining some registers *) + +Fixpoint undef_regs (l: list preg) (rs: regset) : regset := + match l with + | nil => rs + | r :: l' => undef_regs l' (rs#r <- Vundef) + end. + + +(** Assigning a register pair *) +Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := + match p with + | One r => rs#r <- v + | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v) + end. + +(* TODO: Is it still useful ?? *) + + +(** Assigning multiple registers *) + +(* Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset := + match rl, vl with + | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1) + | _, _ => rs + end. + *) +(** Assigning the result of a builtin *) + +Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := + match res with + | BR r => rs#r <- v + | BR_none => rs + | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + end. + Local Open Scope asm. Section RELSEM. @@ -42,13 +847,394 @@ Section RELSEM. Variable ge: genv. +(** The semantics is purely small-step and defined as a function + from the current state (a register set + a memory state) + to either [Next rs' m'] where [rs'] and [m'] are the updated register + set and memory state after execution of the instruction at [rs#PC], + or [Stuck] if the processor is stuck. *) + +Inductive outcome: Type := + | Next (rs:regset) (m:mem) + | Stuck. +(* Arguments outcome: clear implicits. *) + + + +(** ** Arithmetic Expressions (including comparisons) *) + +Inductive signedness: Type := Signed | Unsigned. + +Inductive intsize: Type := Int | Long. + +Definition itest_for_cmp (c: comparison) (s: signedness) := + match c, s with + | Cne, Signed => ITne + | Ceq, Signed => ITeq + | Clt, Signed => ITlt + | Cge, Signed => ITge + | Cle, Signed => ITle + | Cgt, Signed => ITgt + | Cne, Unsigned => ITneu + | Ceq, Unsigned => ITequ + | Clt, Unsigned => ITltu + | Cge, Unsigned => ITgeu + | Cle, Unsigned => ITleu + | Cgt, Unsigned => ITgtu + end. + +Inductive oporder_ftest := + | Normal (ft: ftest) + | Reversed (ft: ftest) +. + +Definition ftest_for_cmp (c: comparison) := + match c with + | Ceq => Normal FToeq + | Cne => Normal FTune + | Clt => Normal FTolt + | Cle => Reversed FToge + | Cgt => Reversed FTolt + | Cge => Normal FToge + end. + +Definition notftest_for_cmp (c: comparison) := + match c with + | Ceq => Normal FTune + | Cne => Normal FToeq + | Clt => Normal FTuge + | Cle => Reversed FTult + | Cgt => Reversed FTuge + | Cge => Normal FTult + end. + +(* CoMPare Signed Words to Zero *) +Definition btest_for_cmpswz (c: comparison) := + match c with + | Cne => BTwnez + | Ceq => BTweqz + | Clt => BTwltz + | Cge => BTwgez + | Cle => BTwlez + | Cgt => BTwgtz + end. + +(* CoMPare Signed Doubles to Zero *) +Definition btest_for_cmpsdz (c: comparison) := + match c with + | Cne => BTdnez + | Ceq => BTdeqz + | Clt => BTdltz + | Cge => BTdgez + | Cle => BTdlez + | Cgt => BTdgtz + end. + +Definition cmp_for_btest (bt: btest) := + match bt with + | BTwnez => (Some Cne, Int) + | BTweqz => (Some Ceq, Int) + | BTwltz => (Some Clt, Int) + | BTwgez => (Some Cge, Int) + | BTwlez => (Some Cle, Int) + | BTwgtz => (Some Cgt, Int) + + | BTdnez => (Some Cne, Long) + | BTdeqz => (Some Ceq, Long) + | BTdltz => (Some Clt, Long) + | BTdgez => (Some Cge, Long) + | BTdlez => (Some Cle, Long) + | BTdgtz => (Some Cgt, Long) + end. + +Definition cmpu_for_btest (bt: btest) := + match bt with + | BTwnez => (Some Cne, Int) + | BTweqz => (Some Ceq, Int) + | BTdnez => (Some Cne, Long) + | BTdeqz => (Some Ceq, Long) + | _ => (None, Int) + end. + + +(* a few lemma on comparisons of unsigned (e.g. pointers) *) + +Definition Val_cmpu_bool cmp v1 v2: option bool := + Val.cmpu_bool (fun _ _ => true) cmp v1 v2. + +Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: + (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b + -> (Val_cmpu_bool cmp v1 v2) = Some b. +Proof. + intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2). + +Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val): + Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2) + (Val_cmpu cmp v1 v2). +Proof. + unfold Val.cmpu, Val_cmpu. + remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. + destruct ob; simpl. + - erewrite Val_cmpu_bool_correct; eauto. + econstructor. + - econstructor. +Qed. + +Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val) + := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2). + +Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: + (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b + -> (Val_cmplu_bool cmp v1 v2) = Some b. +Proof. + intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2). + +Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val): + Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2)) + (Val_cmplu cmp v1 v2). +Proof. + unfold Val.cmplu, Val_cmplu. + remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. + destruct ob as [b|]; simpl. + - erewrite Val_cmplu_bool_correct; eauto. + simpl. econstructor. + - econstructor. +Qed. + + + +(** Comparing integers *) +Definition compare_int (t: itest) (v1 v2: val): val := + match t with + | ITne => Val.cmp Cne v1 v2 + | ITeq => Val.cmp Ceq v1 v2 + | ITlt => Val.cmp Clt v1 v2 + | ITge => Val.cmp Cge v1 v2 + | ITle => Val.cmp Cle v1 v2 + | ITgt => Val.cmp Cgt v1 v2 + | ITneu => Val_cmpu Cne v1 v2 + | ITequ => Val_cmpu Ceq v1 v2 + | ITltu => Val_cmpu Clt v1 v2 + | ITgeu => Val_cmpu Cge v1 v2 + | ITleu => Val_cmpu Cle v1 v2 + | ITgtu => Val_cmpu Cgt v1 v2 + | ITall + | ITnall + | ITany + | ITnone => Vundef + end. + +Definition compare_long (t: itest) (v1 v2: val): val := + let res := match t with + | ITne => Val.cmpl Cne v1 v2 + | ITeq => Val.cmpl Ceq v1 v2 + | ITlt => Val.cmpl Clt v1 v2 + | ITge => Val.cmpl Cge v1 v2 + | ITle => Val.cmpl Cle v1 v2 + | ITgt => Val.cmpl Cgt v1 v2 + | ITneu => Some (Val_cmplu Cne v1 v2) + | ITequ => Some (Val_cmplu Ceq v1 v2) + | ITltu => Some (Val_cmplu Clt v1 v2) + | ITgeu => Some (Val_cmplu Cge v1 v2) + | ITleu => Some (Val_cmplu Cle v1 v2) + | ITgtu => Some (Val_cmplu Cgt v1 v2) + | ITall + | ITnall + | ITany + | ITnone => Some Vundef + end in + match res with + | Some v => v + | None => Vundef + end + . + +Definition compare_single (t: ftest) (v1 v2: val): val := + match t with + | FTone | FTueq => Vundef (* unused *) + | FToeq => Val.cmpfs Ceq v1 v2 + | FTune => Val.cmpfs Cne v1 v2 + | FTolt => Val.cmpfs Clt v1 v2 + | FTuge => Val.notbool (Val.cmpfs Clt v1 v2) + | FToge => Val.cmpfs Cge v1 v2 + | FTult => Val.notbool (Val.cmpfs Cge v1 v2) + end. + +Definition compare_float (t: ftest) (v1 v2: val): val := + match t with + | FTone | FTueq => Vundef (* unused *) + | FToeq => Val.cmpf Ceq v1 v2 + | FTune => Val.cmpf Cne v1 v2 + | FTolt => Val.cmpf Clt v1 v2 + | FTuge => Val.notbool (Val.cmpf Clt v1 v2) + | FToge => Val.cmpf Cge v1 v2 + | FTult => Val.notbool (Val.cmpf Cge v1 v2) + end. + +Definition arith_eval_r n := + match n with + | Ploadsymbol s ofs => Genv.symbol_address ge s ofs + end +. + +Definition arith_eval_rr n v := + match n with + | Pmv => v + | Pnegw => Val.neg v + | Pnegl => Val.negl v + | Pcvtl2w => Val.loword v + | Psxwd => Val.longofint v + | Pzxwd => Val.longofintu v + | Pfnegd => Val.negf v + | Pfnegw => Val.negfs v + | Pfabsd => Val.absf v + | Pfabsw => Val.absfs v + | Pfnarrowdw => Val.singleoffloat v + | Pfwidenlwd => Val.floatofsingle v + | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end + | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end + | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end + | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end + | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end + | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end + | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end + | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end + | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end + | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end + | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end + | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end + end. + +Definition arith_eval_ri32 n i := + match n with + | Pmake => Vint i + end. + +Definition arith_eval_ri64 n i := + match n with + | Pmakel => Vlong i + end. + +Definition arith_eval_rf32 n i := + match n with + | Pmakefs => Vsingle i + end. + +Definition arith_eval_rf64 n i := + match n with + | Pmakef => Vfloat i + end. + +Definition arith_eval_rrr n v1 v2 := + match n with + | Pcompw c => compare_int c v1 v2 + | Pcompl c => compare_long c v1 v2 + | Pfcompw c => compare_single c v1 v2 + | Pfcompl c => compare_float c v1 v2 + + | Paddw => Val.add 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 + + | 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 + | Psral => Val.shrl v1 v2 + + | Pfaddd => Val.addf v1 v2 + | Pfaddw => Val.addfs v1 v2 + | Pfsbfd => Val.subf v1 v2 + | Pfsbfw => Val.subfs v1 v2 + | Pfmuld => Val.mulf v1 v2 + | Pfmulw => Val.mulfs v1 v2 + end. + +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) + end. + +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. + (* TODO: on pourrait mettre ça dans Asmblock pour factoriser le code en définissant exec_arith_instr ai rs := parexec_arith_instr ai rs rs *) Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := match ai with - | PArithR n d => rsw#d <- (arith_eval_r ge n) + | PArithR n d => rsw#d <- (arith_eval_r n) | PArithRR n d s => rsw#d <- (arith_eval_rr n rsr#s) @@ -66,11 +1252,21 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := | PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i) end. +Definition eval_offset (ofs: offset) : res ptrofs := + match ofs with + | Ofsimm n => OK n + | Ofslow id delta => + match (Genv.symbol_address ge id delta) with + | Vptr b ofs => OK ofs + | _ => Error (msg "Asmblock.eval_offset") + end + end. + (** * load/store *) (* TODO: factoriser ? *) Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) := - match (eval_offset ge ofs) with + match (eval_offset ofs) with | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with | None => Stuck | Some v => Next (rsw#d <- v) mw @@ -85,7 +1281,7 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) end. Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) := - match (eval_offset ge ofs) with + match (eval_offset ofs) with | OK ptr => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with | None => Stuck | Some m' => Next rsw m' @@ -99,6 +1295,32 @@ Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem | Some m' => Next rsw m' end. +Definition load_chunk n := + match n with + | Plb => Mint8signed + | Plbu => Mint8unsigned + | Plh => Mint16signed + | Plhu => Mint16unsigned + | Plw => Mint32 + | Plw_a => Many32 + | Pld => Mint64 + | Pld_a => Many64 + | Pfls => Mfloat32 + | Pfld => Mfloat64 + end. + +Definition store_chunk n := + match n with + | Psb => Mint8unsigned + | Psh => Mint16unsigned + | Psw => Mint32 + | Psw_a => Many32 + | Psd => Mint64 + | Psd_a => Many64 + | Pfss => Mfloat32 + | Pfsd => Mfloat64 + end. + (* rem: parexec_store = exec_store *) (** * basic instructions *) @@ -166,6 +1388,41 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) := Definition par_nextblock size_b (rs: regset) := rs#PC <- (Val.offset_ptr rs#PC size_b). + +(** TODO: redundant w.r.t Machblock *) +Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. +Proof. + apply List.in_dec. + apply Pos.eq_dec. +Qed. + + + +(** Note: copy-paste from Machblock *) +Definition is_label (lbl: label) (bb: bblock) : bool := + if in_dec lbl (header bb) then true else false. + +Lemma is_label_correct_true lbl bb: + List.In lbl (header bb) <-> is_label lbl bb = true. +Proof. + unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. +Qed. + +Lemma is_label_correct_false lbl bb: + ~(List.In lbl (header bb)) <-> is_label lbl bb = false. +Proof. + unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. +Qed. + + + +(** convert a label into a position in the code *) +Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z := + match lb with + | nil => None + | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb' + end. + (* TODO: factoriser ? *) Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) := match label_pos lbl 0 (fn_blocks f) with @@ -300,6 +1557,85 @@ Proof. unfold det_parexec; auto. Qed. + (* 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 := + fun r => + if preg_eq r SP + || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) + then rs r + else Vundef. + + +(** Extract the values of the arguments of an external call. + We exploit the calling conventions from module [Conventions], except that + we use RISC-V registers instead of locations. *) + +Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := + | extcall_arg_reg: forall r, + extcall_arg rs m (R r) (rs (preg_of r)) + | extcall_arg_stack: forall ofs ty bofs v, + bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> + Mem.loadv (chunk_of_type ty) m + (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v -> + extcall_arg rs m (S Outgoing ofs ty) v. + +Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := + | extcall_arg_one: forall l v, + extcall_arg rs m l v -> + extcall_arg_pair rs m (One l) v + | extcall_arg_twolong: forall hi lo vhi vlo, + extcall_arg rs m hi vhi -> + extcall_arg rs m lo vlo -> + extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo). + +Definition extcall_arguments + (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := + list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args. + + +Definition loc_external_result (sg: signature) : rpair preg := + map_rpair preg_of (loc_result sg). + +(** Manipulations over the [PC] register: continuing with the next + instruction ([nextblock]) or branching to a label ([goto_label]). *) + +Definition nextblock (b:bblock) (rs: regset) := + rs#PC <- (Val.offset_ptr rs#PC (Ptrofs.repr (size b))). + +(** Looking up bblocks in a code sequence by position. *) +Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock := + match lb with + | nil => None + | b :: il => + if zlt pos 0 then None (* NOTE: It is impossible to branch inside a block *) + else if zeq pos 0 then Some b + else find_bblock (pos - (size b)) il + end. + + +Inductive state: Type := + | State: regset -> mem -> state. + + Inductive step: state -> trace -> state -> Prop := | exec_step_internal: forall b ofs f bundle rs m rs' m', @@ -335,6 +1671,25 @@ End RELSEM. (** Execution of whole programs. *) +(** Execution of whole programs. *) + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall m0, + let ge := Genv.globalenv p in + let rs0 := + (Pregmap.init Vundef) + # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero) + # SP <- Vnullptr + # RA <- Vnullptr in + Genv.init_mem p = Some m0 -> + initial_state p (State rs0 m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall rs m r, + rs PC = Vnullptr -> + rs GPR0 = Vint r -> + final_state (State rs m) r. + Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index f7a35443..6e2539e3 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -1,4 +1,4 @@ -open Asmblock +open Asmvliw open Printf open Camlcoq open InstructionScheduler @@ -7,7 +7,7 @@ open TargetPrinter.Target let debug = false (** - * Extracting infos from Asmblock instructions + * Extracting infos from Asmvliw instructions *) type immediate = I32 of Integers.Int.int | I64 of Integers.Int64.int | Off of offset @@ -22,7 +22,7 @@ type ab_inst_rec = { is_control : bool; } -(** Asmblock constructor to string functions *) +(** Asmvliw constructor to string functions *) exception OpaqueInstruction diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index e0890a09..599a4024 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -21,7 +21,7 @@ Require Import Axioms. Local Open Scope error_monad_scope. -Definition match_prog (p tp: Asmblock.program) := +Definition match_prog (p tp: Asmvliw.program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. Lemma transf_program_match: @@ -826,7 +826,7 @@ Qed. Theorem transf_program_correct_Asmvliw: forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog). Proof. - eapply forward_simulation_step with (match_states:=fun (s1:Asmblock.state) s2 => s1=s2); eauto. + eapply forward_simulation_step with (match_states:=fun (s1:Asmvliw.state) s2 => s1=s2); eauto. - intros; subst; auto. - intros s1 t s1' H s2 H0; subst; inversion H; clear H; subst; eexists; split; eauto. + eapply exec_step_internal; eauto. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index ef02c25a..90ef6a4d 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -40,7 +40,7 @@ module Target (*: TARGET*) = let print_label oc lbl = label oc (transl_label lbl) - let int_reg_name = let open Asmblock in function + let int_reg_name = let open Asmvliw in function | GPR0 -> "$r0" | GPR1 -> "$r1" | GPR2 -> "$r2" | GPR3 -> "$r3" | GPR4 -> "$r4" | GPR5 -> "$r5" | GPR6 -> "$r6" | GPR7 -> "$r7" | GPR8 -> "$r8" | GPR9 -> "$r9" | GPR10 -> "$r10" | GPR11 -> "$r11" @@ -62,12 +62,12 @@ module Target (*: TARGET*) = let ireg = ireg - let preg oc = let open Asmblock in function + let preg oc = let open Asmvliw in function | IR r -> ireg oc r | RA -> output_string oc "$ra" | _ -> assert false - let preg_annot = let open Asmblock in function + let preg_annot = let open Asmvliw in function | IR r -> int_reg_name r | RA -> "$ra" | _ -> assert false @@ -160,7 +160,7 @@ module Target (*: TARGET*) = *) (* Offset part of a load or store *) - let offset oc = let open Asmblock in function + let offset oc = let open Asmvliw in function | Ofsimm n -> ptrofs oc n | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs) @@ -168,7 +168,7 @@ module Target (*: TARGET*) = | AOff ofs -> offset oc ofs | AReg ro -> ireg oc ro - let icond_name = let open Asmblock in function + let icond_name = let open Asmvliw in function | ITne | ITneu -> "ne" | ITeq | ITequ -> "eq" | ITlt -> "lt" @@ -186,7 +186,7 @@ module Target (*: TARGET*) = let icond oc c = fprintf oc "%s" (icond_name c) - let fcond_name = let open Asmblock in function + let fcond_name = let open Asmvliw in function | FTone -> "one" | FTueq -> "ueq" | FToeq -> "oeq" @@ -198,7 +198,7 @@ module Target (*: TARGET*) = let fcond oc c = fprintf oc "%s" (fcond_name c) - let bcond_name = let open Asmblock in function + let bcond_name = let open Asmvliw in function | BTwnez -> "wnez" | BTweqz -> "weqz" | BTwltz -> "wltz" @@ -279,7 +279,7 @@ module Target (*: TARGET*) = | Pjumptable (idx_reg, tbl) -> let lbl = new_label() in (* jumptables := (lbl, tbl) :: !jumptables; *) - let base_reg = if idx_reg=Asmblock.GPR63 then Asmblock.GPR62 else Asmblock.GPR63 in + let base_reg = if idx_reg=Asmvliw.GPR63 then Asmvliw.GPR62 else Asmvliw.GPR63 in fprintf oc "%s jumptable [ " comment; List.iter (fun l -> fprintf oc "%a " print_label l) tbl; fprintf oc "]\n"; diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index d0e05389..8a83521c 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -16,7 +16,7 @@ Require Import Asmblockgen. Require Import Conventions1. Module MB:=Machblock. -Module AB:=Asmblock. +Module AB:=Asmvliw. Hint Extern 2 (_ <> _) => congruence: asmgen. @@ -311,9 +311,9 @@ Qed. Lemma agree_undef_caller_save_regs: forall ms sp rs, agree ms sp rs -> - agree (Mach.undef_caller_save_regs ms) sp (Asmblock.undef_caller_save_regs rs). + agree (Mach.undef_caller_save_regs ms) sp (Asmvliw.undef_caller_save_regs rs). Proof. - intros. destruct H. unfold Mach.undef_caller_save_regs, Asmblock.undef_caller_save_regs; split. + intros. destruct H. unfold Mach.undef_caller_save_regs, Asmvliw.undef_caller_save_regs; split. - unfold proj_sumbool; rewrite dec_eq_true. auto. - auto. - intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). |