(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Léo Gourdin        UGA, VERIMAG                   *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

open Asmblock

(*type called_function = (Registers.reg, AST.ident) Datatypes.sum*)

type instruction = PBasic of Asmblock.basic | PControl of Asmblock.control

type opweights = {
  pipelined_resource_bounds : int array;
  nr_non_pipelined_units : int;
  latency_of_op : instruction -> int -> int;
  resources_of_op : instruction -> int -> int array;
      (*non_pipelined_resources_of_op : Op.operation -> int -> int array;*)
      (*latency_of_load : AST.trapping_mode -> AST.memory_chunk -> Op.addressing -> int -> int;*)
      (*resources_of_load : AST.trapping_mode -> AST.memory_chunk -> Op.addressing -> int -> int array;*)
      (*resources_of_store : AST.memory_chunk -> Op.addressing -> int -> int array;*)
      (*resources_of_cond : Op.condition -> int -> int array;*)
      (*latency_of_call : AST.signature -> called_function -> int;*)
      (*resources_of_call : AST.signature -> called_function -> int array;*)
      (*resources_of_builtin : AST.external_function -> int array*)
}

module Cortex_A53 = struct
  let resource_bounds = [| 2; 2; 1; 1 |]

  (* instr ; ALU ; MAC; LSU *)
  let nr_non_pipelined_units = 1

  let latency_of_op (i : instruction) (nargs : int) =
    match i with
    | PBasic (PArith (PArithP (_, _))) -> 1
    | PBasic (PArith (PArithPP (i', _, _))) -> (
        match i' with
        | Psbfiz (_, _, _) | Psbfx (_, _, _) | Pubfiz (_, _, _) | Pubfx (_, _, _)
          ->
            2
        | Pfcvtds | Pfcvtsd
        | Pfcvtzs (_, _)
        | Pfcvtzu (_, _)
        | Pfabs _ | Pfneg _
        | Pscvtf (_, _)
        | Pucvtf (_, _) ->
            6
        | _ -> 1)
    | PBasic (PArith (PArithPPP (i', _, _, _))) -> (
        match i' with
        | Pasrv _ | Plslv _ | Plsrv _ | Prorv _ | Paddext _ | Psubext _ -> 2
        | Psmulh | Pumulh -> 4
        | Pfdiv _ | Psdiv _ | Pudiv _ -> 50
        | _ -> 6)
    | PBasic (PArith (PArithRR0R (_, _, _, _))) -> 2
    | PBasic (PArith (PArithRR0 (_, _, _))) -> 1
    | PBasic (PArith (PArithARRRR0 (_, _, _, _, _))) -> 4
    | PBasic (PArith (PArithComparisonPP (_, _, _))) -> 6
    | PBasic (PArith (PArithComparisonR0R (_, _, _))) -> 1
    | PBasic (PArith (PArithComparisonP (i', _))) -> (
        match i' with Pfcmp0 _ -> 6 | _ -> 1)
    | PBasic (PArith (Pcset (_, _))) | PBasic (PArith (Pcsel (_, _, _, _))) -> 6
    | PBasic (PArith _) -> 1
    | PBasic (PLoad _) -> 3
    | PBasic (PStore _) -> 3
    | PBasic (Pallocframe (_, _)) -> 3
    | PBasic (Pfreeframe (_, _)) -> 1
    | PBasic (Ploadsymbol (_, _)) -> 1
    | PBasic (Pcvtsw2x (_, _)) -> 2
    | PBasic (Pcvtuw2x (_, _)) -> 2
    | PBasic (Pcvtx2w _) -> 1
    | PBasic (Pnop) -> 0
    | PControl _ -> 6

  let resources_of_op (i : instruction) (nargs : int) =
    match i with
    | PBasic (PArith (PArithP (i', _))) -> (
        match i' with
        | Pfmovimmd _ | Pfmovimms _ -> [| 1; 1; 0; 1 |]
        | _ -> [| 1; 1; 0; 0 |])
    | PBasic (PArith (PArithPP (i', _, _))) -> (
        match i' with
        | Pfcvtds | Pfcvtsd
        | Pfcvtzs (_, _)
        | Pfcvtzu (_, _)
        | Pfabs _ | Pfneg _
        | Pscvtf (_, _)
        | Pucvtf (_, _) ->
            [| 1 ; 1; 1; 0 |]
        | _ -> [| 1; 1; 0; 0 |])
    | PBasic (PArith (PArithPPP (i', _, _, _))) -> (
        match i' with
        | Pasrv _ | Plslv _ | Plsrv _ | Prorv _ | Paddext _ | Psubext _ -> [| 1; 1; 0; 0 |]
        | Pfdiv _ | Psdiv _ | Pudiv _ -> [| 1; 0; 0; 0 |]
        | _ -> [| 1; 1; 1; 0 |])
    | PBasic (PArith (PArithRR0R (_, _, _, _))) -> [| 1; 1; 0; 0 |]
    | PBasic (PArith (PArithRR0 (_, _, _))) -> [| 1; 1; 0; 0 |]
    | PBasic (PArith (PArithARRRR0 (_, _, _, _, _))) -> [| 1; 1; 1; 0 |]
    | PBasic (PArith (PArithComparisonPP (_, _, _))) -> [| 1; 1; 1; 0 |]
    | PBasic (PArith (PArithComparisonR0R (_, _, _))) -> [| 1; 1; 0; 0 |]
    | PBasic (PArith (PArithComparisonP (i', _))) -> (
      match i' with Pfcmp0 _ -> [| 1; 1; 1; 0 |] | _ -> [| 1; 1; 0; 0 |])
    | PBasic (PArith (Pcset (_, _))) | PBasic (PArith (Pcsel (_, _, _, _))) -> [| 1; 1; 1; 0 |]
    | PBasic (PArith _) -> [| 1; 1; 0; 0 |]
    | PBasic (PLoad _) -> [| 1; 0; 0; 1 |]
    | PBasic (PStore _) -> [| 1; 0; 0; 1 |]
    | PBasic (Pallocframe (_, _)) -> [| 1; 0; 0; 1 |]
    | PBasic (Pfreeframe (_, _)) -> [| 1; 1; 0; 0 |]
    | PBasic (Ploadsymbol (_, _)) -> [| 1; 1; 0; 0 |]
    | PBasic (Pcvtsw2x (_, _)) -> [| 1; 1; 0; 0 |]
    | PBasic (Pcvtuw2x (_, _)) -> [| 1; 1; 0; 0 |]
    | PBasic (Pcvtx2w _) -> [| 1; 1; 0; 0 |]
    | PBasic (Pnop) -> [| 0; 0; 0; 0 |]
    | PControl _ -> resource_bounds

  (*let non_pipelined_resources_of_op (op : operation) (nargs : int) =
      match op with
      | Odiv | Odivu -> [| 29 |]
      | Odivfs -> [| 20 |]
      | Odivl | Odivlu | Odivf -> [| 50 |]
      | _ -> [| -1 |];;

    let resources_of_cond (cmp : condition) (nargs : int) =
      (match cmp with
       | Ccompf _                              (* r FP comparison *)
         | Cnotcompf _                           (* r negation of an FP comparison *)
         | Ccompfzero _                          (* r comparison with 0.0 *)
         | Cnotcompfzero _                       (* r negation of comparison with 0.0 *)
         | Ccompfs _                             (* r FP comparison *)
         | Cnotcompfs _                          (* r negation of an FP comparison *)
         | Ccompfszero _                         (* r equal to 0.0 *)
         | Cnotcompfszero _                     (* r not equal to 0.0 *) ->
          [| 1; 1; 1; 0 |]
       | _ -> [| 1; 1; 0; 0 |] )*)

end

let get_opweights () : opweights =
  (*match !Clflags.option_mtune with*)
  (*| "cortex-a53" | "cortex-a35" | "" ->*)
  {
    pipelined_resource_bounds = Cortex_A53.resource_bounds;
    nr_non_pipelined_units = Cortex_A53.nr_non_pipelined_units;
    latency_of_op = Cortex_A53.latency_of_op;
    resources_of_op =
      Cortex_A53.resources_of_op
      (*non_pipelined_resources_of_op = Cortex_A53.non_pipelined_resources_of_op;*)
      (*latency_of_load = Cortex_A53.latency_of_load;*)
      (*resources_of_load = Cortex_A53.resources_of_load;*)
      (*resources_of_store = Cortex_A53.resources_of_store;*)
      (*resources_of_cond = Cortex_A53.resources_of_cond;*)
      (*latency_of_call = Cortex_A53.latency_of_call;*)
      (*resources_of_call = Cortex_A53.resources_of_call;*)
      (*resources_of_builtin = Cortex_A53.resources_of_builtin*);
  }

(*| xxx -> failwith (Printf.sprintf "unknown -mtune: %s" xxx);;*)