From b4a08d0815342b6238d307864f0823d0f07bb691 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 May 2020 22:04:20 +0200 Subject: k1c -> kvx changes --- kvx/Peephole.v | 158 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 158 insertions(+) create mode 100644 kvx/Peephole.v (limited to 'kvx/Peephole.v') diff --git a/kvx/Peephole.v b/kvx/Peephole.v new file mode 100644 index 00000000..35f4bbd9 --- /dev/null +++ b/kvx/Peephole.v @@ -0,0 +1,158 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Coqlib. +Require Import Asmvliw. +Require Import Values. +Require Import Integers. +Require Import AST. +Require Compopts. + +Definition gpreg_q_list : list gpreg_q := +R0R1 :: R2R3 :: R4R5 :: R6R7 :: R8R9 +:: R10R11 :: R12R13 :: R14R15 :: R16R17 :: R18R19 +:: R20R21 :: R22R23 :: R24R25 :: R26R27 :: R28R29 +:: R30R31 :: R32R33 :: R34R35 :: R36R37 :: R38R39 +:: R40R41 :: R42R43 :: R44R45 :: R46R47 :: R48R49 +:: R50R51 :: R52R53 :: R54R55 :: R56R57 :: R58R59 +:: R60R61 :: R62R63 :: nil. + +Definition gpreg_o_list : list gpreg_o := +R0R1R2R3 :: R4R5R6R7 :: R8R9R10R11 :: R12R13R14R15 +:: R16R17R18R19 :: R20R21R22R23 :: R24R25R26R27 :: R28R29R30R31 +:: R32R33R34R35 :: R36R37R38R39 :: R40R41R42R43 :: R44R45R46R47 +:: R48R49R50R51 :: R52R53R54R55 :: R56R57R58R59 :: R60R61R62R63 :: nil. + +Fixpoint gpreg_q_search_rec r0 r1 l := + match l with + | h :: t => + let (s0, s1) := gpreg_q_expand h in + if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) + then Some h + else gpreg_q_search_rec r0 r1 t + | nil => None + end. + +Fixpoint gpreg_o_search_rec r0 r1 r2 r3 l := + match l with + | h :: t => + match gpreg_o_expand h with + | (((s0, s1), s2), s3) => + if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) && + (gpreg_eq r2 s2) && (gpreg_eq r3 s3) + then Some h + else gpreg_o_search_rec r0 r1 r2 r3 t + end + | nil => None + end. + +Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q := + gpreg_q_search_rec r0 r1 gpreg_q_list. + +Definition gpreg_o_search r0 r1 r2 r3 : option gpreg_o := + gpreg_o_search_rec r0 r1 r2 r3 gpreg_o_list. + +Parameter print_found_store: forall A, Z -> A -> A. + +Definition coalesce_octuples := true. + +Fixpoint coalesce_mem (insns : list basic) : list basic := + match insns with + | nil => nil + | h0 :: t0 => + match t0 with + | h1 :: t1 => + match h0, h1 with + | (PStoreRRO Psd_a rs0 ra0 ofs0), + (PStoreRRO Psd_a rs1 ra1 ofs1) => + match gpreg_q_search rs0 rs1 with + | Some rs0rs1 => + let zofs0 := Ptrofs.signed ofs0 in + let zofs1 := Ptrofs.signed ofs1 in + if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) + then + if coalesce_octuples + then + match t1 with + | (PStoreRRO Psd_a rs2 ra2 ofs2) :: + (PStoreRRO Psd_a rs3 ra3 ofs3) :: t3 => + match gpreg_o_search rs0 rs1 rs2 rs3 with + | Some octuple => + let zofs2 := Ptrofs.signed ofs2 in + let zofs3 := Ptrofs.signed ofs3 in + if (zofs2 =? zofs0 + 16) && (ireg_eq ra0 ra2) && + (zofs3 =? zofs0 + 24) && (ireg_eq ra0 ra3) + then (PStore (PStoreORRO octuple ra0 ofs0)) :: Pnop :: Pnop :: Pnop :: (coalesce_mem t3) + else (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + | None => (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + end + | _ => (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + end + else (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + else h0 :: (coalesce_mem t0) + | None => h0 :: (coalesce_mem t0) + end + + | (PLoad (PLoadRRO TRAP Pld_a rd0 ra0 ofs0)), + (PLoad (PLoadRRO TRAP Pld_a rd1 ra1 ofs1)) => + match gpreg_q_search rd0 rd1 with + | Some rd0rd1 => + let zofs0 := Ptrofs.signed ofs0 in + let zofs1 := Ptrofs.signed ofs1 in + if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) && negb (ireg_eq ra0 rd0) + then + if coalesce_octuples + then + match t1 with + | (PLoad (PLoadRRO TRAP Pld_a rd2 ra2 ofs2)) :: + (PLoad (PLoadRRO TRAP Pld_a rd3 ra3 ofs3)) :: t3 => + match gpreg_o_search rd0 rd1 rd2 rd3 with + | Some octuple => + let zofs2 := Ptrofs.signed ofs2 in + let zofs3 := Ptrofs.signed ofs3 in + if (zofs2 =? zofs0 + 16) && (ireg_eq ra0 ra2) && + (zofs3 =? zofs0 + 24) && (ireg_eq ra0 ra3) && + negb (ireg_eq ra0 rd1) && negb (ireg_eq ra0 rd2) + then (PLoad (PLoadORRO octuple ra0 ofs0)) :: Pnop :: Pnop :: Pnop :: (coalesce_mem t3) + else (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + | None => (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + end + | _ => (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + end + else (PLoad (PLoadQRRO rd0rd1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + else h0 :: (coalesce_mem t0) + | None => h0 :: (coalesce_mem t0) + end + | _, _ => h0 :: (coalesce_mem t0) + end + | nil => h0 :: nil + end + end. + +Definition optimize_body (insns : list basic) := + if Compopts.optim_coalesce_mem tt + then coalesce_mem insns + else insns. + +Program Definition optimize_bblock (bb : bblock) := + let optimized := optimize_body (body bb) in + let wf_ok := wf_bblockb optimized (exit bb) in + {| header := header bb; + body := if wf_ok then optimized else (body bb); + exit := exit bb |}. +Next Obligation. + destruct (wf_bblockb (optimize_body (body bb))) eqn:Rwf. + - rewrite Rwf. simpl. trivial. + - exact (correct bb). +Qed. -- cgit