path: root/riscV/ExpansionOracle.ml

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

open RTLpathLivegenaux
open RTLpathCommon
open Datatypes
open Maps
open RTL
open Op
open Asmgen
open DebugPrint
(*open PrintRTL*)
open! Integers

let reg = ref 1
let node = ref 1

let r2p () = Camlcoq.P.of_int !reg
let n2p () = Camlcoq.P.of_int !node
let n2pi () = node := !node + 1; n2p()

type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul

let load_hilo32 dest hi lo succ k =
  if Int.eq lo Int.zero then
    Iop (OEluiw hi, [], dest, succ) :: k
  else (
      Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k)

let load_hilo64 dest hi lo succ k =
  if Int64.eq lo Int64.zero then
    Iop (OEluil hi, [], dest, succ) :: k
  else (
      Iop (OEluil hi, [], dest, n2pi()) :: (Iop (Oaddlimm lo, [dest], dest, succ)) :: k)

let loadimm32 dest n succ k =
  match make_immed32 n with
  | Imm32_single imm ->
      Iop (OEaddiwr0 imm, [], dest, succ) :: k
  | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k

let loadimm64 dest n succ k =
  match make_immed64 n with
  | Imm64_single imm ->
      Iop (OEaddilr0 imm, [], dest, succ) :: k
  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k
  | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k

let get_opimm imm = function
  | Xoriw -> OExoriw imm
  | Sltiw -> OEsltiw imm
  | Sltiuw -> OEsltiuw imm
  | Xoril -> OExoril imm
  | Sltil -> OEsltil imm
  | Sltiul -> OEsltiul imm

let opimm32 a1 dest n succ k op opimm =
  match make_immed32 n with
  | Imm32_single imm ->
      Iop (get_opimm imm opimm, [a1], dest, succ) :: k
  | Imm32_pair (hi, lo) ->
      reg := !reg + 1;
      load_hilo32 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)

let opimm64 a1 dest n succ k op opimm =
  match make_immed64 n with
  | Imm64_single imm ->
      Iop (get_opimm imm opimm, [a1], dest, succ) :: k
  | Imm64_pair (hi, lo) ->
      reg := !reg + 1;
      load_hilo64 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
  | Imm64_large imm  ->
      reg := !reg + 1;
      Iop (OEloadli imm, [], r2p(), n2pi()) :: Iop (op, [a1;r2p()], dest, succ) :: k

let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw
let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw
let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw
let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil
let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul

let cond_int32s_x0 cmp a1 dest succ k =
  match cmp with
  | Ceq -> Iop (OEseqw (Some false), [a1;a1], dest, succ) :: k
  | Cne -> Iop (OEsnew (Some false), [a1;a1], dest, succ) :: k
  | Clt -> Iop (OEsltw (Some false), [a1;a1], dest, succ) :: k
  | Cle -> Iop (OEsltw (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
  | Cgt -> Iop (OEsltw (Some true), [a1;a1], dest, succ) :: k
  | Cge -> Iop (OEsltw (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k

let cond_int32s_reg cmp a1 a2 dest succ k =
  match cmp with
  | Ceq -> Iop (OEseqw None, [a1;a2], dest, succ) :: k
  | Cne -> Iop (OEsnew None, [a1;a2], dest, succ) :: k
  | Clt -> Iop (OEsltw None, [a1;a2], dest, succ) :: k
  | Cle -> Iop (OEsltw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
  | Cgt -> Iop (OEsltw None, [a2;a1], dest, succ) :: k
  | Cge -> Iop (OEsltw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k

let cond_int32u_x0 cmp a1 dest succ k =
  match cmp with
  | Ceq -> Iop (OEseqw (Some false), [a1;a1], dest, succ) :: k
  | Cne -> Iop (OEsnew (Some false), [a1;a1], dest, succ) :: k
  | Clt -> Iop (OEsltuw (Some false), [a1;a1], dest, succ) :: k
  | Cle -> Iop (OEsltuw (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
  | Cgt -> Iop (OEsltuw (Some true), [a1;a1], dest, succ) :: k
  | Cge -> Iop (OEsltuw (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k

let cond_int32u_reg cmp a1 a2 dest succ k =
  match cmp with
  | Ceq -> Iop (OEseqw None, [a1;a2], dest, succ) :: k
  | Cne -> Iop (OEsnew None, [a1;a2], dest, succ) :: k
  | Clt -> Iop (OEsltuw None, [a1;a2], dest, succ) :: k
  | Cle -> Iop (OEsltuw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
  | Cgt -> Iop (OEsltuw None, [a2;a1], dest, succ) :: k
  | Cge -> Iop (OEsltuw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k

let cond_int64s_x0 cmp a1 dest succ k =
  match cmp with
  | Ceq -> Iop (OEseql (Some false), [a1;a1], dest, succ) :: k
  | Cne -> Iop (OEsnel (Some false), [a1;a1], dest, succ) :: k
  | Clt -> Iop (OEsltl (Some false), [a1;a1], dest, succ) :: k
  | Cle -> Iop (OEsltl (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
  | Cgt -> Iop (OEsltl (Some true), [a1;a1], dest, succ) :: k
  | Cge -> Iop (OEsltl (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k

let cond_int64s_reg cmp a1 a2 dest succ k =
  match cmp with
  | Ceq -> Iop (OEseql None, [a1;a2], dest, succ) :: k
  | Cne -> Iop (OEsnel None, [a1;a2], dest, succ) :: k
  | Clt -> Iop (OEsltl None, [a1;a2], dest, succ) :: k
  | Cle -> Iop (OEsltl None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
  | Cgt -> Iop (OEsltl None, [a2;a1], dest, succ) :: k
  | Cge -> Iop (OEsltl None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k

let cond_int64u_x0 cmp a1 dest succ k =
  match cmp with
  | Ceq -> Iop (OEseql (Some false), [a1;a1], dest, succ) :: k
  | Cne -> Iop (OEsnel (Some false), [a1;a1], dest, succ) :: k
  | Clt -> Iop (OEsltul (Some false), [a1;a1], dest, succ) :: k
  | Cle -> Iop (OEsltul (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
  | Cgt -> Iop (OEsltul (Some true), [a1;a1], dest, succ) :: k
  | Cge -> Iop (OEsltul (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k

let cond_int64u_reg cmp a1 a2 dest succ k =
  match cmp with
  | Ceq -> Iop (OEseql None, [a1;a2], dest, succ) :: k
  | Cne -> Iop (OEsnel None, [a1;a2], dest, succ) :: k
  | Clt -> Iop (OEsltul None, [a1;a2], dest, succ) :: k
  | Cle -> Iop (OEsltul None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
  | Cgt -> Iop (OEsltul None, [a2;a1], dest, succ) :: k
  | Cge -> Iop (OEsltul None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k

let expanse_condimm_int32s cmp a1 n dest succ k =
  if Int.eq n Int.zero then cond_int32s_x0 cmp a1 dest succ k else
  match cmp with
  | Ceq | Cne ->
      xorimm32 a1 dest n (n2pi()) (cond_int32s_x0 cmp dest dest succ k)
  | Clt -> sltimm32 a1 dest n succ k
  | Cle -> if Int.eq n (Int.repr Int.max_signed)
           then loadimm32 dest Int.one succ k
            else sltimm32 a1 dest (Int.add n Int.one) succ k
  | _   -> reg := !reg + 1;
           loadimm32 (r2p()) n (n2pi()) (cond_int32s_reg cmp a1 (r2p()) dest succ k)

let expanse_condimm_int32u cmp a1 n dest succ k =
  if Int.eq n Int.zero then cond_int32u_x0 cmp a1 dest succ k else
  match cmp with
  | Clt -> sltuimm32 a1 dest n succ k
  | _   -> reg := !reg + 1;
           loadimm32 (r2p()) n (n2pi()) (cond_int32u_reg cmp a1 (r2p()) dest succ k)

let expanse_condimm_int64s cmp a1 n dest succ k =
  if Int.eq n Int.zero then cond_int64s_x0 cmp a1 dest succ k else
  match cmp with
  | Ceq | Cne ->
      reg := !reg + 1;
      xorimm64 a1 (r2p()) n (n2pi()) (cond_int64s_x0 cmp (r2p()) dest succ k)
  | Clt -> sltimm64 a1 dest n succ k
  | Cle -> if Int64.eq n (Int64.repr Int64.max_signed)
           then loadimm32 dest Int.one succ k
            else sltimm64 a1 dest (Int64.add n Int64.one) succ k
  | _   -> reg := !reg + 1;
           loadimm64 (r2p()) n (n2pi()) (cond_int64s_reg cmp a1 (r2p()) dest succ k)
 
let expanse_condimm_int64u cmp a1 n dest succ k =
  if Int64.eq n Int64.zero then cond_int64u_x0 cmp a1 dest succ k else
  match cmp with
  | Clt -> sltuimm64 a1 dest n succ k
  | _   -> reg := !reg + 1;
           loadimm64 (r2p()) n (n2pi()) (cond_int64u_reg cmp a1 (r2p()) dest succ k)

let rec write_tree exp n code' =
  match exp with
  | (Iop (_,_,_,succ)) as inst :: k ->
      (*print_instruction stderr (0,inst);*)
      (*Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);*)
      code' := PTree.set n inst !code';
      (*Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);*)
      write_tree k (Camlcoq.P.of_int ((Camlcoq.P.to_int n) + 1)) code'
  | _ -> !code'

let get_regindent = function
  | Coq_inr _ -> []
  | Coq_inl r -> [r]
  
let get_regs_inst = function
  | Inop (_) -> []
  | Iop (_,args,dest,_) -> dest :: args
  | Iload (_,_,_,args,dest,_) -> dest :: args
  | Istore (_,_,args,src,_) -> src :: args
  | Icall (_,t,args,dest,_) -> dest :: ((get_regindent t) @ args)
  | Itailcall (_,t,args) -> (get_regindent t) @ args
  | Ibuiltin (_,args,dest,_) ->
      (AST.params_of_builtin_res dest) @
      AST.params_of_builtin_args args
  | Icond (_,args,_,_,_) -> args
  | Ijumptable (arg,_) -> [arg]
  | Ireturn (Some r) -> [r]
  | _ -> []

let generate_head_order n start_node new_order =
  Printf.eprintf "GEN n %d start %d node %d\n" (Camlcoq.P.to_int n) (Camlcoq.P.to_int start_node) !node;
  for i = !node downto (Camlcoq.P.to_int start_node) do
    new_order := !new_order @ [Camlcoq.P.of_int i];
  done;
  new_order := n :: !new_order

let expanse (sb: superblock) code =
  debug_flag := true;
  let new_order = ref [] in
  let exp = ref [] in
  let was_exp = ref false in
  let code' = ref code in
  Array.iter (fun n ->
    was_exp := false;
    let inst = get_some @@ PTree.get n code in
    let start_node = Camlcoq.P.of_int (!node + 1) in (
    match inst with
    | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> (
      Printf.eprintf "Ccomp\n";
      exp := cond_int32s_reg c a1 a2 dest succ [];
      was_exp := true)
    | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> (
      Printf.eprintf "Ccompu\n";
      exp := cond_int32u_reg c a1 a2 dest succ [];
      was_exp := true)
    | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> (
      Printf.eprintf "Ccompimm\n";
      exp := expanse_condimm_int32s c a1 imm dest succ [];
      was_exp := true)
    | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> (
      Printf.eprintf "Ccompuimm\n";
      exp := expanse_condimm_int32u c a1 imm dest succ [];
      was_exp := true)
    | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> (
      Printf.eprintf "Ccompl\n";
      exp := cond_int64s_reg c a1 a2 dest succ [];
      was_exp := true)
    | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> (
      Printf.eprintf "Ccomplu\n";
      exp := cond_int64u_reg c a1 a2 dest succ [];
      was_exp := true)
    | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> (
      (*Printf.eprintf "Ccomplimm\n";*)
      (*Printf.eprintf "[EXPANSION] Last node is: %d\n" !node;*)
      (*Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg;*)
      (*Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n);*)
      (*Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);*)
      (*debug "[EXPANSION] Replace this:\n";*)
      (*print_instruction stderr (0,inst);*)
      (*debug "[EXPANSION] With:\n";*)
      (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
      (*entry := n2p()*)
      exp := expanse_condimm_int64s c a1 imm dest succ [];
      was_exp := true)
    | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> (
      Printf.eprintf "Ccompluimm\n";
      exp := expanse_condimm_int64u c a1 imm dest succ [];
      was_exp := true)
    | _ -> new_order := !new_order @ [n]);
    if !was_exp then (
      code' := write_tree (List.rev !exp) start_node code';
      let first = Inop (n2pi()) in
      code' := PTree.set n first !code';
      generate_head_order n start_node new_order)
  ) sb.instructions;
  sb.instructions <- Array.of_list !new_order;
  (*print_arrayp sb.instructions;*)
  debug_flag := false;
  !code'

let rec find_last_node_reg = function
  | [] -> ()
  | (pc, i) :: k ->
    let rec traverse_list var = function
    | [] -> ()
    | e :: t ->
        (let e' = Camlcoq.P.to_int e in
        if e' > !var then var := e';
        traverse_list var t) in
    traverse_list node [pc];
    traverse_list reg (get_regs_inst i);
    find_last_node_reg k