Rename pipelining

1 files changed, 128 insertions, 0 deletions

diff --git a/src/pipelining/SPBase_types.ml b/src/pipelining/SPBase_types.ml
new file mode 100644
index 0000000..ba92340
--- /dev/null
+++ b/src/pipelining/SPBase_types.ml
@@ -0,0 +1,128 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                        Compcert Extensions                          *)
+(*                                                                     *)
+(*                       Jean-Baptiste Tristan                         *)
+(*                                                                     *)
+(*  All rights reserved.  This file is distributed under the terms     *)
+(*  described in file ../../LICENSE.                                   *)
+(*                                                                     *)
+(***********************************************************************)
+
+
+open Camlcoq
+open Op
+open Registers
+open Memory
+open Mem
+open AST
+
+type ('a,'b) sum = ('a,'b) Datatypes.sum
+
+type instruction =
+  | Inop 
+  | Iop of operation * reg list * reg
+  | Iload of memory_chunk * addressing * reg list * reg
+  | Istore of memory_chunk * addressing * reg list * reg
+  | Icall of signature * (reg, ident) sum * reg list * reg
+  | Itailcall of signature * (reg, ident) sum * reg list
+  | Icond of condition * reg list
+  | Ireturn of reg option
+
+type resource = Reg of reg | Mem
+
+let inst_coq_to_caml = function 
+  | RTL.Inop succ -> Inop
+  | RTL.Iop (op, args, dst, succ) -> Iop (op, args, dst)
+  | RTL.Iload (chunk, mode, args, dst, succ) -> Iload (chunk, mode, args, dst)
+  | RTL.Istore (chunk, mode, args, src, succ) -> Istore (chunk, mode, args, src)
+  | RTL.Icall (sign, id, args, dst, succ) -> Icall (sign, id, args, dst)
+  | RTL.Itailcall (sign, id, args) -> Itailcall (sign, id, args)
+  | RTL.Icond (cond, args, succ1, succ2) -> Icond (cond, args)
+  | RTL.Ireturn (res) -> Ireturn (res)
+ 
+let inst_caml_to_coq i (links : RTL.node list) =
+  match i,links with 
+  | Inop,[p] -> RTL.Inop p
+  | Iop (op, args, dst),[p] -> RTL.Iop (op, args, dst,p)  
+  | Iload (chunk, mode, args, dst),[p] -> RTL.Iload (chunk, mode, args,dst,p) 
+  | Istore (chunk, mode, args, src),[p] -> RTL.Istore (chunk, mode, args, src,p)  
+  | Icall (sign, id, args, dst),[p] -> RTL.Icall (sign, id, args, dst,p) 
+  | Itailcall (sign, id, args),[] -> RTL.Itailcall (sign, id, args) 
+  | Icond (cond, args),[p1;p2] -> RTL.Icond (cond,args,p1,p2)
+  | Ireturn (res),[] -> RTL.Ireturn res 
+  | _,_ -> failwith "Echec lors de la conversion des instrucitons internes vers compcert"
+
+
+let print_inst node = string_of_int (snd node)
+
+let to_int = fun n -> P.to_int n
+let to_binpos = fun n -> P.of_int n
+
+let rec string_of_args args =
+  match args with
+    | [] -> ""
+    | arg :: args -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args
+
+let string_of_z z = string_of_int (Z.to_int z)
+
+let string_of_comparison = function
+  | Integers.Ceq -> "eq"
+  | Integers.Cne -> "ne"
+  | Integers.Clt -> "lt"
+  | Integers.Cle -> "le"
+  | Integers.Cgt -> "gt"
+  | Integers.Cge -> "ge"
+ 
+let string_of_cond = function
+  | Ccomp c -> Printf.sprintf "comp %s" (string_of_comparison c)
+  | Ccompu c -> Printf.sprintf "compu %s" (string_of_comparison c)
+  | Ccompimm (c,i) -> Printf.sprintf "compimm %s %s" (string_of_comparison c) (string_of_z i)
+  | Ccompuimm (c,i) -> Printf.sprintf "compuimm %s %s" (string_of_comparison c) (string_of_z i)
+  | Ccompf c -> Printf.sprintf "compf %s" (string_of_comparison c)
+  | Cnotcompf c -> Printf.sprintf "notcompf %s" (string_of_comparison c)
+  | Cmaskzero i -> Printf.sprintf "maskzero %s" (string_of_z i)
+  | Cmasknotzero i -> Printf.sprintf "masknotzero %s" (string_of_z i)
+
+let string_of_op = function
+  | Omove -> "move"
+  | Ointconst i -> Printf.sprintf "intconst %s" (string_of_z i)
+  | Ofloatconst f -> Printf.sprintf "floatconst %s" (string_of_float (camlfloat_of_coqfloat32 f))
+  | Ocast8signed -> "cast8signed"
+  | Ocast8unsigned -> "cast8unsigned"
+  | Ocast16signed -> "cast16signed"
+  | Ocast16unsigned -> "cast16unsigned"
+  | Osub -> "sub"
+  | Omul -> "mul"
+  | Omulimm i -> Printf.sprintf "mulimm %s" (string_of_z i)
+  | Odiv -> "div"
+  | Odivu -> "divu"
+  | Oand -> "and"
+  | Oandimm i -> Printf.sprintf "andimm %s" (string_of_z i)
+  | Oor -> "or"
+  | Oorimm i -> Printf.sprintf "orimm %s" (string_of_z i)
+  | Oxor -> "xor"
+  | Oxorimm i -> Printf.sprintf "xorimm %s" (string_of_z i)
+  | Oshl -> "shl"
+  | Oshr -> "shr"
+  | Oshrimm i -> Printf.sprintf "shrimm %s" (string_of_z i)
+  | Oshrximm i -> Printf.sprintf "shrximm %s" (string_of_z i)
+  | Oshru -> "shru"
+  | Onegf -> "negf"
+  | Oabsf -> "absf"
+  | Oaddf -> "addf"
+  | Osubf -> "subf"
+  | Omulf -> "mulf"
+  | Odivf -> "divf"
+  | Osingleoffloat -> "singleoffloat"
+  | Ofloatofint -> "floatofint"
+  | Ocmp c -> Printf.sprintf "cmpcmpcmp"
+  | Olea _ -> "lea"
+  
+let to_coq_list = function
+  | [] -> []
+  | e :: l -> e :: l
+
+let to_caml_list = function
+  | [] -> []
+  | e :: l -> e :: l