Expansion of Ccompimm in RTL [Admitted checker]

1 files changed, 174 insertions, 0 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
new file mode 100644
index 00000000..15a418fd
--- /dev/null
+++ b/riscV/ExpansionOracle.ml
@@ -0,0 +1,174 @@
+(* *************************************************************)
+(*                                                             *)
+(*             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 = Xori | Slti
+
+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 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 get_opimm imm = function
+  | Xori -> OExoriw imm
+  | Slti -> OEsltiw 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 xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xori
+let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Slti
+
+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 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 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 code' = ref code in
+  Array.iter (fun n ->
+    let inst = get_some @@ PTree.get n code in
+    match inst with
+    | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> (
+      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";
+      let start_node = Camlcoq.P.of_int (!node + 1) in
+      let exp = expanse_condimm_int32s c a1 imm dest succ [] in
+      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;
+      (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
+      (*entry := n2p()*)
+    (*| Icond (cond,args,ifso,ifnot,info) -> (code' :=
+        match cond, args with
+        | Ccompimm (c, imm), a1 :: nil ->
+            expanse_condimm_int32s cond a1 imm info ifso ifnot
+            PTree.set n (Icond (cond,args,ifso,ifnot,info)) !code'
+        | (_, _) -> !code'*)
+        (*PTree.set node*))
+    | _ -> new_order := !new_order @ [n]
+  ) 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