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/SelectLong.vp | 463 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 463 insertions(+) create mode 100644 kvx/SelectLong.vp (limited to 'kvx/SelectLong.vp') diff --git a/kvx/SelectLong.vp b/kvx/SelectLong.vp new file mode 100644 index 00000000..b3638eca --- /dev/null +++ b/kvx/SelectLong.vp @@ -0,0 +1,463 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* 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. *) +(* *) +(* *************************************************************) + +(** Instruction selection for 64-bit integer operations *) + +Require Import Coqlib. +Require Import Compopts. +Require Import AST Integers Floats. +Require Import Op CminorSel. +Require Import OpHelpers. +Require Import SelectOp SplitLong. +Require Import ExtValues. +Require Import DecBoolOps. + +Local Open Scope cminorsel_scope. +Local Open Scope string_scope. + +Section SELECT. + +Context {hf: helper_functions}. + +Definition longconst (n: int64) : expr := + if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil. + +Definition is_longconst (e: expr) := + if Archi.splitlong then SplitLong.is_longconst e else + match e with + | Eop (Olongconst n) Enil => Some n + | _ => None + end. + +Definition intoflong (e: expr) := + if Archi.splitlong then SplitLong.intoflong e else + match is_longconst e with + | Some n => Eop (Ointconst (Int.repr (Int64.unsigned n))) Enil + | None => Eop Olowlong (e ::: Enil) + end. + +Definition longofint (e: expr) := + if Archi.splitlong then SplitLong.longofint e else + match is_intconst e with + | Some n => longconst (Int64.repr (Int.signed n)) + | None => Eop Ocast32signed (e ::: Enil) + end. + +Definition longofintu (e: expr) := + if Archi.splitlong then SplitLong.longofintu e else + match is_intconst e with + | Some n => longconst (Int64.repr (Int.unsigned n)) + | None => Eop Ocast32unsigned (e ::: Enil) + end. + +(** ** Integer addition and pointer addition *) + +Definition addlimm_shllimm sh k2 e1 := + if Compopts.optim_addx tt + then + match shift1_4_of_z (Int.unsigned sh) with + | Some s14 => Eop (Oaddxlimm s14 k2) (e1:::Enil) + | None => Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil) + end + else Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil). + +Nondetfunction addlimm (n: int64) (e: expr) := + if Int64.eq n Int64.zero then e else + match e with + | Eop (Olongconst m) Enil => longconst (Int64.add n m) + | Eop (Oaddrsymbol s m) Enil => + (if Compopts.optim_globaladdroffset tt + then Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil + else Eop (Oaddlimm n) (e ::: Enil)) + | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil + | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add n m)) (t ::: Enil) + | Eop (Oaddxlimm sh m) (t ::: Enil) => Eop (Oaddxlimm sh (Int64.add n m)) (t ::: Enil) + | Eop (Oshllimm sh) (t1:::Enil) => addlimm_shllimm sh n t1 + | _ => Eop (Oaddlimm n) (e ::: Enil) + end. + +Definition addl_shllimm n e1 e2 := + if Compopts.optim_addx tt + then + match shift1_4_of_z (Int.unsigned n) with + | Some s14 => Eop (Oaddxl s14) (e1:::e2:::Enil) + | None => Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil) + end + else Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil). + +Nondetfunction addl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.addl e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => addlimm n1 t2 + | t1, Eop (Olongconst n2) Enil => addlimm n2 t1 + | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) => + addlimm (Int64.add n1 n2) (Eop Oaddl (t1:::t2:::Enil)) + | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil => + Eop Oaddl (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n1) n2)) Enil ::: t1 ::: Enil) + | Eop (Oaddrstack n1) Enil, Eop (Oaddlimm n2) (t2:::Enil) => + Eop Oaddl (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int64 n2))) Enil ::: t2 ::: Enil) + | Eop (Oaddlimm n1) (t1:::Enil), t2 => + addlimm n1 (Eop Oaddl (t1:::t2:::Enil)) + | t1, Eop (Oaddlimm n2) (t2:::Enil) => + addlimm n2 (Eop Oaddl (t1:::t2:::Enil)) + | t1, (Eop Omull (t2:::t3:::Enil)) => + Eop Omaddl (t1:::t2:::t3:::Enil) + | (Eop Omull (t2:::t3:::Enil)), t1 => + Eop Omaddl (t1:::t2:::t3:::Enil) + | t1, (Eop (Omullimm n) (t2:::Enil)) => + Eop (Omaddlimm n) (t1:::t2:::Enil) + | (Eop (Omullimm n) (t2:::Enil)), t1 => + Eop (Omaddlimm n) (t1:::t2:::Enil) + | (Eop (Oshllimm n) (t1:::Enil)), t2 => + addl_shllimm n t1 t2 + | t2, (Eop (Oshllimm n) (t1:::Enil)) => + addl_shllimm n t1 t2 + | _, _ => Eop Oaddl (e1:::e2:::Enil) + end. + +(** ** Integer and pointer subtraction *) + +Nondetfunction subl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.subl e1 e2 else + match e1, e2 with + | t1, Eop (Olongconst n2) Enil => + addlimm (Int64.neg n2) t1 + | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) => + addlimm (Int64.sub n1 n2) (Eop Osubl (t1:::t2:::Enil)) + | Eop (Oaddlimm n1) (t1:::Enil), t2 => + addlimm n1 (Eop Osubl (t1:::t2:::Enil)) + | t1, Eop (Oaddlimm n2) (t2:::Enil) => + addlimm (Int64.neg n2) (Eop Osubl (t1:::t2:::Enil)) + | t1, (Eop Omull (t2:::t3:::Enil)) => + Eop Omsubl (t1:::t2:::t3:::Enil) + | t1, (Eop (Omullimm n) (t2:::Enil)) => + Eop (Omaddlimm (Int64.neg n)) (t1:::t2:::Enil) + | _, _ => Eop Osubl (e1:::e2:::Enil) + end. + +Definition negl (e: expr) := + if Archi.splitlong then SplitLong.negl e else + match is_longconst e with + | Some n => longconst (Int64.neg n) + | None => Eop Onegl (e ::: Enil) + end. + +(** ** Immediate shifts *) + +Nondetfunction shllimm (e1: expr) (n: int) := + if Archi.splitlong then SplitLong.shllimm e1 n else + if Int.eq n Int.zero then + e1 + else if negb (Int.ltu n Int64.iwordsize') then + Eop Oshll (e1 ::: Eop (Ointconst n) Enil ::: Enil) + else match e1 with + | Eop (Olongconst n1) Enil => + longconst (Int64.shl' n1 n) + | Eop (Oshllimm n1) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int64.iwordsize' + then Eop (Oshllimm (Int.add n n1)) (t1:::Enil) + else Eop (Oshllimm n) (e1:::Enil) + | _ => + Eop (Oshllimm n) (e1:::Enil) + end. + +Nondetfunction shrluimm (e1: expr) (n: int) := + if Archi.splitlong then SplitLong.shrluimm e1 n else + if Int.eq n Int.zero then e1 else + if negb (Int.ltu n Int64.iwordsize') then + Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil) + else + match e1 with + | Eop (Olongconst n1) Enil => + longconst (Int64.shru' n1 n) + | Eop (Oshrluimm n1) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int64.iwordsize' + then Eop (Oshrluimm (Int.add n n1)) (t1:::Enil) + else Eop (Oshrluimm n) (e1:::Enil) + | Eop (Oshllimm n1) (t1:::Enil) => + let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in + let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in + if is_bitfieldl stop start + then Eop (Oextfzl stop start) (t1:::Enil) + else Eop (Oshrluimm n) (e1:::Enil) + | _ => + Eop (Oshrluimm n) (e1:::Enil) + end. + +Nondetfunction shrlimm (e1: expr) (n: int) := + if Archi.splitlong then SplitLong.shrlimm e1 n else + if Int.eq n Int.zero then e1 else + if negb (Int.ltu n Int64.iwordsize') then + Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil) + else + match e1 with + | Eop (Olongconst n1) Enil => + longconst (Int64.shr' n1 n) + | Eop (Oshrlimm n1) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int64.iwordsize' + then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil) + else Eop (Oshrlimm n) (e1:::Enil) + | Eop (Oshllimm n1) (t1:::Enil) => + let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in + let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in + if is_bitfieldl stop start + then Eop (Oextfsl stop start) (t1:::Enil) + else Eop (Oshrlimm n) (e1:::Enil) + | _ => + Eop (Oshrlimm n) (e1:::Enil) + end. + +(** ** General shifts *) + +Definition shll (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.shll e1 e2 else + match is_intconst e2 with + | Some n2 => shllimm e1 n2 + | None => Eop Oshll (e1:::e2:::Enil) + end. + +Definition shrl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.shrl e1 e2 else + match is_intconst e2 with + | Some n2 => shrlimm e1 n2 + | None => Eop Oshrl (e1:::e2:::Enil) + end. + +Definition shrlu (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.shrlu e1 e2 else + match is_intconst e2 with + | Some n2 => shrluimm e1 n2 + | _ => Eop Oshrlu (e1:::e2:::Enil) + end. + +(** ** Integer multiply *) + +Definition mullimm_base (n1: int64) (e2: expr) := + match Int64.one_bits' n1 with + | i :: nil => + shllimm e2 i + | i :: j :: nil => + Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j)) + | _ => + Eop (Omullimm n1) (e2 ::: Enil) + end. + +Nondetfunction mullimm (n1: int64) (e2: expr) := + if Archi.splitlong then SplitLong.mullimm n1 e2 + else if Int64.eq n1 Int64.zero then longconst Int64.zero + else if Int64.eq n1 Int64.one then e2 + else match e2 with + | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2) + | Eop (Oaddlimm n2) (t2:::Enil) => addlimm (Int64.mul n1 n2) (mullimm_base n1 t2) + | _ => mullimm_base n1 e2 + end. + +Nondetfunction mull (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.mull e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => mullimm n1 t2 + | t1, Eop (Olongconst n2) Enil => mullimm n2 t1 + | _, _ => Eop Omull (e1:::e2:::Enil) + end. + +Definition mullhu (e1: expr) (n2: int64) := + if Archi.splitlong then SplitLong.mullhu e1 n2 else + Eop Omullhu (e1 ::: longconst n2 ::: Enil). + +Definition mullhs (e1: expr) (n2: int64) := + if Archi.splitlong then SplitLong.mullhs e1 n2 else + Eop Omullhs (e1 ::: longconst n2 ::: Enil). + +(** ** Bitwise and, or, xor *) + +Nondetfunction andlimm (n1: int64) (e2: expr) := + if Int64.eq n1 Int64.zero then longconst Int64.zero else + if Int64.eq n1 Int64.mone then e2 else + match e2 with + | Eop (Olongconst n2) Enil => + longconst (Int64.and n1 n2) + | Eop (Oandlimm n2) (t2:::Enil) => + Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil) + | Eop Onotl (t2:::Enil) => Eop (Oandnlimm n1) (t2:::Enil) + | _ => + Eop (Oandlimm n1) (e2:::Enil) + end. + +Nondetfunction andl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.andl e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2 + | t1, Eop (Olongconst n2) Enil => andlimm n2 t1 + | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) + | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) + | _, _ => Eop Oandl (e1:::e2:::Enil) + end. + +Nondetfunction orlimm (n1: int64) (e2: expr) := + if Int64.eq n1 Int64.zero then e2 else + if Int64.eq n1 Int64.mone then longconst Int64.mone else + match e2 with + | Eop (Olongconst n2) Enil => longconst (Int64.or n1 n2) + | Eop (Oorlimm n2) (t2:::Enil) => Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil) + | Eop Onotl (t2:::Enil) => Eop (Oornlimm n1) (t2:::Enil) + | _ => Eop (Oorlimm n1) (e2:::Enil) + end. + +Nondetfunction orl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.orl e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2 + | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 + | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) + | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) + | (Eop (Oandlimm nmask) (prev:::Enil)), + (Eop (Oandlimm mask) + ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) => + let zstart := Int.unsigned start in + let zstop := int64_highest_bit mask in + if is_bitfieldl zstop zstart + then + let mask' := Int64.repr (zbitfield_mask zstop zstart) in + if and_dec (Int64.eq_dec mask mask') + (Int64.eq_dec nmask (Int64.not mask')) + then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil) + else Eop Oorl (e1:::e2:::Enil) + else Eop Oorl (e1:::e2:::Enil) + | (Eop (Oandlimm nmask) (prev:::Enil)), + (Eop (Oandlimm mask) (fld:::Enil)) => + let zstart := 0 in + let zstop := int64_highest_bit mask in + if is_bitfieldl zstop zstart + then + let mask' := Int64.repr (zbitfield_mask zstop zstart) in + if and_dec (Int64.eq_dec mask mask') + (Int64.eq_dec nmask (Int64.not mask')) + then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil) + else Eop Oorl (e1:::e2:::Enil) + else Eop Oorl (e1:::e2:::Enil) + | _, _ => Eop Oorl (e1:::e2:::Enil) + end. + +Nondetfunction xorlimm (n1: int64) (e2: expr) := + if Int64.eq n1 Int64.zero then e2 else + if Int64.eq n1 Int64.mone + then Eop Onotl (e2:::Enil) + else + match e2 with + | Eop (Olongconst n2) Enil => longconst (Int64.xor n1 n2) + | Eop (Oxorlimm n2) (t2:::Enil) => + let n := Int64.xor n1 n2 in + if Int64.eq n Int64.zero then t2 else Eop (Oxorlimm n) (t2:::Enil) + | _ => Eop (Oxorlimm n1) (e2:::Enil) + end. + +Nondetfunction xorl (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.xorl e1 e2 else + match e1, e2 with + | Eop (Olongconst n1) Enil, t2 => xorlimm n1 t2 + | t1, Eop (Olongconst n2) Enil => xorlimm n2 t1 + | _, _ => Eop Oxorl (e1:::e2:::Enil) + end. + +(** ** Integer logical negation *) + +Nondetfunction notl (e: expr) := + match e with + | Eop Oandl (e1:::e2:::Enil) => Eop Onandl (e1:::e2:::Enil) + | Eop (Oandlimm n) (e1:::Enil) => Eop (Onandlimm n) (e1:::Enil) + | Eop Oorl (e1:::e2:::Enil) => Eop Onorl (e1:::e2:::Enil) + | Eop (Oorlimm n) (e1:::Enil) => Eop (Onorlimm n) (e1:::Enil) + | Eop Oxorl (e1:::e2:::Enil) => Eop Onxorl (e1:::e2:::Enil) + | Eop (Oxorlimm n) (e1:::Enil) => Eop (Onxorlimm n) (e1:::Enil) + | Eop Onandl (e1:::e2:::Enil) => Eop Oandl (e1:::e2:::Enil) + | Eop (Onandlimm n) (e1:::Enil) => Eop (Oandlimm n) (e1:::Enil) + | Eop Onorl (e1:::e2:::Enil) => Eop Oorl (e1:::e2:::Enil) + | Eop (Onorlimm n) (e1:::Enil) => Eop (Oorlimm n) (e1:::Enil) + | Eop Onxorl (e1:::e2:::Enil) => Eop Oxorl (e1:::e2:::Enil) + | Eop (Onxorlimm n) (e1:::Enil) => Eop (Oxorlimm n) (e1:::Enil) + | Eop Oandnl (e1:::e2:::Enil) => Eop Oornl (e2:::e1:::Enil) + | Eop (Oandnlimm n) (e1:::Enil) => Eop (Oorlimm (Int64.not n)) (e1:::Enil) + | Eop Oornl (e1:::e2:::Enil) => Eop Oandnl (e2:::e1:::Enil) + | Eop (Oornlimm n) (e1:::Enil) => Eop (Oandlimm (Int64.not n)) (e1:::Enil) + | Eop Onotl (e1:::Enil) => e1 + | Eop (Olongconst k) Enil => Eop (Olongconst (Int64.not k)) Enil + | _ => Eop Onotl (e:::Enil) + end. +(* old: if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e. *) + +(** ** Integer division and modulus *) + +Definition divlu_base (e1: expr) (e2: expr) := SplitLong.divlu_base e1 e2. +Definition modlu_base (e1: expr) (e2: expr) := SplitLong.modlu_base e1 e2. +Definition divls_base (e1: expr) (e2: expr) := SplitLong.divls_base e1 e2. +Definition modls_base (e1: expr) (e2: expr) := SplitLong.modls_base e1 e2. + +Definition shrxlimm (e: expr) (n: int) := + if Archi.splitlong then SplitLong.shrxlimm e n else + if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil). + +(** ** Comparisons *) + +Definition cmplu (c: comparison) (e1 e2: expr) := + if Archi.splitlong then SplitLong.cmplu c e1 e2 else + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => + Eop (Ointconst (if Int64.cmpu c n1 n2 then Int.one else Int.zero)) Enil + | Some n1, None => Eop (Ocmp (Ccompluimm (swap_comparison c) n1)) (e2:::Enil) + | None, Some n2 => Eop (Ocmp (Ccompluimm c n2)) (e1:::Enil) + | None, None => Eop (Ocmp (Ccomplu c)) (e1:::e2:::Enil) + end. + +Definition cmpl (c: comparison) (e1 e2: expr) := + if Archi.splitlong then SplitLong.cmpl c e1 e2 else + match is_longconst e1, is_longconst e2 with + | Some n1, Some n2 => + Eop (Ointconst (if Int64.cmp c n1 n2 then Int.one else Int.zero)) Enil + | Some n1, None => Eop (Ocmp (Ccomplimm (swap_comparison c) n1)) (e2:::Enil) + | None, Some n2 => Eop (Ocmp (Ccomplimm c n2)) (e1:::Enil) + | None, None => Eop (Ocmp (Ccompl c)) (e1:::e2:::Enil) + end. + +(** ** Floating-point conversions *) + +Definition longoffloat (e: expr) := + if Archi.splitlong then SplitLong.longoffloat e else + Eop Olongoffloat (e:::Enil). + +Definition longuoffloat (e: expr) := + if Archi.splitlong then SplitLong.longuoffloat e else + Eop Olonguoffloat (e:::Enil). + +Definition floatoflong (e: expr) := + if Archi.splitlong then SplitLong.floatoflong e else + Eop Ofloatoflong (e:::Enil). + +Definition floatoflongu (e: expr) := + if Archi.splitlong then SplitLong.floatoflongu e else + Eop Ofloatoflongu (e:::Enil). + +Definition longofsingle (e: expr) := longoffloat (floatofsingle e). + +Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e). + +Definition singleoflong (e: expr) := SplitLong.singleoflong e. + +Definition singleoflongu (e: expr) := SplitLong.singleoflongu e. + +End SELECT. + +(* Local Variables: *) +(* mode: coq *) +(* End: *) -- cgit