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 BTL
open Op
open! Integers
open Camlcoq
open DebugPrint
open RTLcommonaux
open BTLcommonaux
open AST
open Datatypes
open Maps

(** Tools *)

(** TODO gourdinl move to BTLcommonaux *)
let rec iblock_to_list ib =
  match ib with
  | Bseq (ib1, ib2) -> iblock_to_list ib1 @ iblock_to_list ib2
  | _ -> [ ib ]

let rec list_to_iblock lib =
  match lib with
  | i1 :: k ->
      if List.length lib > 1 then
        Bseq (i1, list_to_iblock k)
      else i1
  | [] -> failwith "list_to_iblock: called on empty list"

(** Mini CSE (a dynamic numbering is applied during expansion. 
    The CSE algorithm is inspired by the "static" one used in backend/CSE.v *)

(** Managing virtual registers and node index *)

let reg = ref 1

let r2p () = P.of_int !reg

let r2pi () =
  reg := !reg + 1;
  r2p ()

(** Below are the types for rhs and equations *)

type rhs = Sop of operation * int list | Smove

type seq = Seq of int * rhs

(** This is a mini abstraction to have a simpler representation during expansion
    - (Sr r) is inserted if the value was found in register r
    - (Sexp dest rhs args iinfo) represent an instruction
    - (Scond cond args ib1 ib2 iinfo) represents a condition
*)

type expl =
  | Sr of P.t
  | Sexp of P.t * rhs * P.t list * inst_info
  | Scond of condition * P.t list * iblock * iblock * inst_info

(** Record used during the "dynamic" value numbering *)

type numb = {
  mutable nnext : int;  (** Next unusued value number *)
  mutable seqs : seq list;  (** equations *)
  mutable nreg : (P.t, int) Hashtbl.t;  (** mapping registers to values *)
  mutable nval : (int, P.t list) Hashtbl.t;
      (** reverse mapping values to registers containing it *)
}

let print_list_pos l =
  debug "[";
  List.iter (fun i -> debug "%d;" (p2i i)) l;
  debug "]\n"

let empty_numbering () =
  { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 }

let rec get_nvalues vn = function
  | [] -> []
  | r :: rs ->
      let v =
        match Hashtbl.find_opt !vn.nreg r with
        | Some v ->
            debug "getnval r=%d |-> v=%d\n" (p2i r) v;
            v
        | None ->
            let n = !vn.nnext in
            debug "getnval r=%d |-> v=%d\n" (p2i r) n;
            !vn.nnext <- !vn.nnext + 1;
            Hashtbl.replace !vn.nreg r n;
            Hashtbl.replace !vn.nval n [ r ];
            n
      in
      let vs = get_nvalues vn rs in
      v :: vs

let get_nval_ornil vn v =
  match Hashtbl.find_opt !vn.nval v with None -> [] | Some l -> l

let forget_reg vn rd =
  match Hashtbl.find_opt !vn.nreg rd with
  | Some v ->
      debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v;
      let old_regs = get_nval_ornil vn v in
      debug "forget_reg: old_regs are:\n";
      print_list_pos old_regs;
      Hashtbl.replace !vn.nval v
        (List.filter (fun n -> not (P.eq n rd)) old_regs)
  | None -> debug "forget_reg: no mapping for r=%d\n" (p2i rd)

let update_reg vn rd v =
  debug "update_reg: update v=%d with r=%d\n" v (p2i rd);
  forget_reg vn rd;
  let old_regs = get_nval_ornil vn v in
  Hashtbl.replace !vn.nval v (rd :: old_regs)

let rec find_valnum_rhs rh = function
  | [] -> None
  | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl

let set_unknown vn rd =
  debug "set_unknown: rd=%d\n" (p2i rd);
  forget_reg vn rd;
  Hashtbl.remove !vn.nreg rd

let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> ()

let addrhs vn rd rh =
  match find_valnum_rhs rh !vn.seqs with
  | Some vres ->
      debug "addrhs: Some v=%d\n" vres;
      Hashtbl.replace !vn.nreg rd vres;
      update_reg vn rd vres
  | None ->
      let n = !vn.nnext in
      debug "addrhs: None v=%d\n" n;
      !vn.nnext <- !vn.nnext + 1;
      !vn.seqs <- Seq (n, rh) :: !vn.seqs;
      update_reg vn rd n;
      Hashtbl.replace !vn.nreg rd n

let addsop vn v op rd =
  debug "addsop\n";
  if op = Omove then (
    update_reg vn rd (List.hd v);
    Hashtbl.replace !vn.nreg rd (List.hd v))
  else addrhs vn rd (Sop (op, v))

let rec kill_mem_operations = function
  | (Seq (v, Sop (op, vl)) as eq) :: tl ->
      if op_depends_on_memory op then kill_mem_operations tl
      else eq :: kill_mem_operations tl
  | [] -> []
  | eq :: tl -> eq :: kill_mem_operations tl

let reg_valnum vn v =
  debug "reg_valnum: trying to find a mapping for v=%d\n" v;
  match Hashtbl.find !vn.nval v with
  | [] -> None
  | r :: rs ->
      debug "reg_valnum: found a mapping r=%d\n" (p2i r);
      Some r

let rec reg_valnums vn = function
  | [] -> Some []
  | v :: vs -> (
      match (reg_valnum vn v, reg_valnums vn vs) with
      | Some r, Some rs -> Some (r :: rs)
      | _, _ -> None)

let find_rhs vn rh =
  match find_valnum_rhs rh !vn.seqs with
  | None -> None
  | Some vres -> reg_valnum vn vres

(** Functions to perform the dynamic reduction during CSE *)

let extract_arg l =
  if List.length l > 0 then
    match List.hd l with
    | Sr r -> (r, List.tl l)
    | Sexp (rd, _, _, _) -> (rd, l)
    | _ -> failwith "extract_arg: final instruction arg can not be extracted"
  else failwith "extract_arg: trying to extract on an empty list"

let extract_final vn fl fdest =
  if List.length fl > 0 then
    match List.hd fl with
    | Sr r ->
        if not (P.eq r fdest) then (
          let v = get_nvalues vn [ r ] in
          addsop vn v Omove fdest;
          Sexp (fdest, Smove, [ r ], def_iinfo ()) :: List.tl fl)
        else List.tl fl
    | _ -> fl
  else failwith "extract_final: trying to extract on an empty list"

let addinst vn op args rd iinfo =
  let v = get_nvalues vn args in
  let rh = Sop (op, v) in
  match find_rhs vn rh with
  | Some r ->
      debug "addinst: rhs found with r=%d\n" (p2i r);
      Sr r
  | None ->
      addsop vn v op rd;
      Sexp (rd, rh, args, iinfo)

(** Expansion functions *)

let is_inv_cmp = function Cle | Cgt -> true | _ -> false

let make_optR is_x0 is_inv =
  if is_x0 then if is_inv then Some X0_L else Some X0_R else None

let cond_int32s vn is_x0 cmp a1 a2 dest iinfo =
  let optR = make_optR is_x0 (is_inv_cmp cmp) in
  match cmp with
  | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest iinfo ]
  | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest iinfo ]
  | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest iinfo ]
  | Cle ->
      let r = r2pi () in
      let op = OEsltw optR in
      let i1 = addinst vn op [ a2; a1 ] r iinfo in
      let r', l = extract_arg [ i1 ] in
      addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l
  | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest iinfo ]
  | Cge ->
      let r = r2pi () in
      let op = OEsltw optR in
      let i1 = addinst vn op [ a1; a2 ] r iinfo in
      let r', l = extract_arg [ i1 ] in
      addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l

(** Return olds args if the CSE numbering is empty *)

let get_arguments vn vals args =
  match reg_valnums vn vals with Some args' -> args' | None -> args

let rec gen_btl_list vn exp =
  match exp with
  | Sr r :: _ ->
      failwith "write_tree: there are still some symbolic values in the list"
  | Sexp (rd, Sop (op, vals), args, iinfo) :: k ->
      let args = get_arguments vn vals args in
      let inst = Bop (op, args, rd, iinfo) in
      inst :: gen_btl_list vn k
  | [ Sexp (rd, Smove, args, iinfo) ] ->
      [ Bop (Omove, args, rd, iinfo) ]
  | [ Scond (cond, args, succ1, succ2, iinfo) ] ->
      [ Bcond (cond, args, succ1, succ2, iinfo) ]
  | [] -> []
  | _ -> failwith "write_tree: invalid list"

let expanse_list li =
  debug "#### New block for expansion oracle\n";
  let exp = ref [] in
  let was_exp = ref false in
  let vn = ref (empty_numbering ()) in
  let rec expanse_list_rec li =
    match li with
    | [] -> li
    | i :: li' ->
        was_exp := false;
        (if !Clflags.option_fexpanse_rtlcond then
         match i with
         | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) ->
             debug "Bop/Ccomp\n";
             exp := cond_int32s vn false c a1 a2 dest iinfo;
             exp := extract_final vn !exp dest;
             was_exp := true
         | _ -> ());
        if not !was_exp then (
          (match i with
          | Bop (op, args, dest, iinfo) ->
              let v = get_nvalues vn args in
              addsop vn v op dest
          | Bload (_, _, _, _, dst, _) -> set_unknown vn dst
          | Bstore (_, _, _, _, _) ->
              !vn.seqs <- kill_mem_operations !vn.seqs
              (* TODO gourdinl empty numb BF? vn := empty_numbering ()*)
          | _ -> ());
          i :: expanse_list_rec li')
        else
          gen_btl_list vn !exp @ expanse_list_rec li'
  in
  expanse_list_rec li

let expanse n ibf btl =
  debug_flag := true;
  let lib = iblock_to_list ibf.entry in
  let new_lib = expanse_list lib in
  let ibf' = { entry = list_to_iblock new_lib;
               input_regs = ibf.input_regs;
               binfo = ibf.binfo } in
  debug_flag := false;
  PTree.set n ibf' btl

(** Form a list containing both sources and destination regs of a block *)
let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]

let rec get_regs_ib = function
  | Bnop _ -> []
  | Bop (_, args, dest, _) -> dest :: args
  | Bload (_, _, _, args, dest, _) -> dest :: args
  | Bstore (_, _, args, src, _) -> src :: args
  | Bcond (_, args, ib1, ib2, _) -> 
      get_regs_ib ib1 @ get_regs_ib ib2 @ args
  | Bseq (ib1, ib2) ->
      get_regs_ib ib1 @ get_regs_ib ib2
  | BF (Breturn (Some r), _) -> [r]
  | BF (Bcall (_, t, args, dest, _), _) -> dest :: (get_regindent t @ args)
  | BF (Btailcall (_, t, args), _) -> (get_regindent t @ args)
  | BF (Bbuiltin (_, args, dest, _), _) -> 
      AST.params_of_builtin_res dest @ AST.params_of_builtin_args args
  | BF (Bjumptable (arg, _), _) -> [arg]
  | _ -> []

let rec find_last_reg = function
  | [] -> ()
  | (pc, ibf) :: k ->
      let rec traverse_list var = function
        | [] -> ()
        | e :: t ->
            let e' = p2i e in
            if e' > !var then var := e';
            traverse_list var t
      in
      traverse_list reg (get_regs_ib ibf.entry);
      find_last_reg k