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/Machregs.v | 245 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 245 insertions(+) create mode 100644 kvx/Machregs.v (limited to 'kvx/Machregs.v') diff --git a/kvx/Machregs.v b/kvx/Machregs.v new file mode 100644 index 00000000..02fa4e6b --- /dev/null +++ b/kvx/Machregs.v @@ -0,0 +1,245 @@ +(* *************************************************************) +(* *) +(* 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. *) +(* *) +(* *************************************************************) + +Require Import String. +Require Import Coqlib. +Require Import Decidableplus. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Op. + +(** ** Machine registers *) + +(** The following type defines the machine registers that can be referenced + as locations. These include: +- Integer registers that can be allocated to RTL pseudo-registers ([Rxx]). +- Floating-point registers that can be allocated to RTL pseudo-registers + ([Fxx]). + + The type [mreg] does not include reserved machine registers such as + the zero register (x0), the link register (x1), the stack pointer + (x2), the global pointer (x3), and the thread pointer (x4). + Finally, register x31 is reserved for use as a temporary by the + assembly-code generator [Asmgen]. +*) + +Inductive mreg: Type := + (* Allocatable General Purpose regs. *) + | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 + | R10 | R11 (* | R12 | R13 | R14 *) | R15 (* | R16 *) | R17 | R18 | R19 + | R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 | R28 | R29 + | R30 | R31 (* | R32 *) | R33 | R34 | R35 | R36 | R37 | R38 | R39 + | R40 | R41 | R42 | R43 | R44 | R45 | R46 | R47 | R48 | R49 + | R50 | R51 | R52 | R53 | R54 | R55 | R56 | R57 | R58 | R59 + | R60 | R61 | R62 | R63. + +Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. +Proof. decide equality. Defined. +Global Opaque mreg_eq. + +Definition all_mregs := + R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 + :: R10 :: R11 (* :: R12 :: R13 :: R14 *) :: R15 (* :: R16 *) :: R17 :: R18 :: R19 + :: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 + :: R30 :: R31 (* :: R32 *) :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 + :: R40 :: R41 :: R42 :: R43 :: R44 :: R45 :: R46 :: R47 :: R48 :: R49 + :: R50 :: R51 :: R52 :: R53 :: R54 :: R55 :: R56 :: R57 :: R58 :: R59 + :: R60 :: R61 :: R62 :: R63 :: nil. + +Lemma all_mregs_complete: + forall (r: mreg), In r all_mregs. +Proof. + assert (forall r, proj_sumbool (In_dec mreg_eq r all_mregs) = true) by (destruct r; reflexivity). + intros. specialize (H r). InvBooleans. auto. +Qed. + +Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. + +Instance Finite_mreg : Finite mreg := { + Finite_elements := all_mregs; + Finite_elements_spec := all_mregs_complete +}. + +Definition mreg_type (r: mreg): typ := Tany64. + +Open Scope positive_scope. + +Module IndexedMreg <: INDEXED_TYPE. + Definition t := mreg. + Definition eq := mreg_eq. + Definition index (r: mreg): positive := + match r with + | R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4 | R4 => 5 + | R5 => 6 | R6 => 7 | R7 => 8 | R8 => 9 | R9 => 10 + | R10 => 11 | R11 => 12 (* | R12 => 13 | R13 => 14 | R14 => 15 *) + | R15 => 16 (* | R16 => 17 *) | R17 => 18 | R18 => 19 | R19 => 20 + | R20 => 21 | R21 => 22 | R22 => 23 | R23 => 24 | R24 => 25 + | R25 => 26 | R26 => 27 | R27 => 28 | R28 => 29 | R29 => 30 + | R30 => 31 | R31 => 32 (* | R32 => 33 *) | R33 => 34 | R34 => 35 + | R35 => 36 | R36 => 37 | R37 => 38 | R38 => 39 | R39 => 40 + | R40 => 41 | R41 => 42 | R42 => 43 | R43 => 44 | R44 => 45 + | R45 => 46 | R46 => 47 | R47 => 48 | R48 => 49 | R49 => 50 + | R50 => 51 | R51 => 52 | R52 => 53 | R53 => 54 | R54 => 55 + | R55 => 56 | R56 => 57 | R57 => 58 | R58 => 59 | R59 => 60 + | R60 => 61 | R61 => 62 | R62 => 63 | R63 => 64 + end. + + Lemma index_inj: + forall r1 r2, index r1 = index r2 -> r1 = r2. + Proof. + decide_goal. + Qed. +End IndexedMreg. + +Definition is_stack_reg (r: mreg) : bool := false. + +(** ** Names of registers *) + +Local Open Scope string_scope. + +Definition register_names := + ("R0" , R0) :: ("R1" , R1) :: ("R2" , R2) :: ("R3" , R3) :: ("R4" , R4) + :: ("R5" , R5) :: ("R6" , R6) :: ("R7" , R7) :: ("R8" , R8) :: ("R9" , R9) + :: ("R10", R10) :: ("R11", R11) (* :: ("R12", R12) :: ("R13", R13) :: ("R14", R14) *) + :: ("R15", R15) (* :: ("R16", R16) *) :: ("R17", R17) :: ("R18", R18) :: ("R19", R19) + :: ("R20", R20) :: ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) + :: ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) :: ("R29", R29) + :: ("R30", R30) :: ("R31", R31) (* :: ("R32", R32) *) :: ("R33", R33) :: ("R34", R34) + :: ("R35", R35) :: ("R36", R36) :: ("R37", R37) :: ("R38", R38) :: ("R39", R39) + :: ("R40", R40) :: ("R41", R41) :: ("R42", R42) :: ("R43", R43) :: ("R44", R44) + :: ("R45", R45) :: ("R46", R46) :: ("R47", R47) :: ("R48", R48) :: ("R49", R49) + :: ("R50", R50) :: ("R51", R51) :: ("R52", R52) :: ("R53", R53) :: ("R54", R54) + :: ("R55", R55) :: ("R56", R56) :: ("R57", R57) :: ("R58", R58) :: ("R59", R59) + :: ("R60", R60) :: ("R61", R61) :: ("R62", R62) :: ("R63", R63) :: nil. + +Definition register_by_name (s: string) : option mreg := + let fix assoc (l: list (string * mreg)) : option mreg := + match l with + | nil => None + | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l' + end + in assoc register_names. + +(** ** Destroyed registers, preferred registers *) + +Definition destroyed_by_op (op: operation): list mreg := nil. +(*match op with + | Ointoffloat | Ointuoffloat | Ointofsingle | Ointuofsingle + | Olongoffloat | Olonguoffloat | Olongofsingle | Olonguofsingle + => F6 :: nil + | _ => nil + end. +*) + +Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg := nil. + +Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := nil. + +Definition destroyed_by_cond (cond: condition): list mreg := nil. + +Definition destroyed_by_jumptable: list mreg := R62 :: R63 :: nil. + +Fixpoint destroyed_by_clobber (cl: list string): list mreg := + match cl with + | nil => nil + | c1 :: cl => + match register_by_name c1 with + | Some r => r :: destroyed_by_clobber cl + | None => destroyed_by_clobber cl + end + end. + +Definition destroyed_by_builtin (ef: external_function): list mreg := + match ef with + | EF_inline_asm txt sg clob => destroyed_by_clobber clob + | EF_memcpy sz al => + if Z.leb sz 15 + then R62 :: R63 :: R61 :: nil + else R62 :: R63 :: R61 :: R60 :: nil + | EF_profiling _ _ => R62 :: R63 ::nil + | _ => nil + end. + +Definition destroyed_by_setstack (ty: typ): list mreg := nil. + +Definition destroyed_at_function_entry: list mreg := R17 :: nil. + +Definition temp_for_parent_frame: mreg := R17. (* Temporary used to store the parent frame, where the arguments are *) + +Definition destroyed_at_indirect_call: list mreg := nil. + (* R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: nil. *) + +Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := (nil, None). + +(* FIXME DMonniaux this seems to be the place for preferred registers for arguments *) +Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(option mreg) := (nil, nil). + + (* match ef with + | EF_builtin name sg => + if (negb Archi.ptr64) && string_dec name "__builtin_bswap64" then + (Some R6 :: Some R5 :: nil, Some R5 :: Some R6 :: nil) + else + (nil, nil) + | _ => + (nil, nil) + end. *) + +Global Opaque + destroyed_by_op destroyed_by_load destroyed_by_store + destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin + destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame + mregs_for_operation mregs_for_builtin. + +(** Two-address operations. Return [true] if the first argument and + the result must be in the same location *and* are unconstrained + by [mregs_for_operation]. There are two: the pseudo [Ocast32signed], + because it expands to a no-op owing to the representation of 32-bit + integers as their 64-bit sign extension; and [Ocast32unsigned], + because it builds on the same magic no-op. *) + +Definition two_address_op (op: operation) : bool := + match op with + | Ofmaddf | Ofmaddfs + | Ofmsubf | Ofmsubfs + | Omadd | Omaddimm _ + | Omaddl | Omaddlimm _ + | Omsub | Omsubl + | Osel _ _ | Oselimm _ _ | Osellimm _ _ + | Oinsf _ _ | Oinsfl _ _ => true + | _ => false + end. + +(** Constraints on constant propagation for builtins *) + +Definition builtin_constraints (ef: external_function) : + list builtin_arg_constraint := + match ef with + | EF_builtin id sg => + if string_dec id "__builtin_kvx_get" then OK_const :: nil + else if string_dec id "__builtin_kvx_set" + then OK_const :: OK_default :: nil + else if string_dec id "__builtin_kvx_wfxl" + then OK_const :: OK_default :: nil + else if string_dec id "__builtin_kvx_wfxm" + then OK_const :: OK_default :: nil + else nil + | EF_vload _ => OK_addressing :: nil + | EF_vstore _ => OK_addressing :: OK_default :: nil + | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil + | EF_annot kind txt targs => map (fun _ => OK_all) targs + | EF_debug kind txt targs => map (fun _ => OK_all) targs + | _ => nil + end. -- cgit