From 51e3a17d2e65b095861c243807f4e8d76c60ea0e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 17 Dec 2020 10:02:23 +0000 Subject: Add Software pipelining stage by tristan et al. --- src/SoftwarePipelining/SPBase_types.ml | 143 +++++++++++++++++++++++++++++++++ 1 file changed, 143 insertions(+) create mode 100644 src/SoftwarePipelining/SPBase_types.ml (limited to 'src/SoftwarePipelining/SPBase_types.ml') diff --git a/src/SoftwarePipelining/SPBase_types.ml b/src/SoftwarePipelining/SPBase_types.ml new file mode 100644 index 0000000..3e339c3 --- /dev/null +++ b/src/SoftwarePipelining/SPBase_types.ml @@ -0,0 +1,143 @@ +(***********************************************************************) +(* *) +(* 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 Mem +open AST + +type ('a,'b) sum = ('a,'b) Datatypes.sum + +type instruction = + | Inop + | Iop of operation * reg CList.list * reg + | Iload of memory_chunk * addressing * reg CList.list * reg + | Istore of memory_chunk * addressing * reg CList.list * reg + | Icall of signature * (reg, ident) sum * reg CList.list * reg + | Itailcall of signature * (reg, ident) sum * reg CList.list + | Ialloc of reg * reg + | Icond of condition * reg CList.list + | Ireturn of reg Datatypes.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.Ialloc (dst, size, succ) -> Ialloc (dst, size) + | 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) + | Ialloc (dst, size),[p] -> RTL.Ialloc (dst, size,p) + | 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 -> Int32.to_int (camlint_of_positive n) +let to_binpos = fun n -> positive_of_camlint (Int32.of_int n) + +let rec string_of_args args = + match args with + | CList.Coq_nil -> "" + | CList.Coq_cons (arg,args) -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args + +let string_of_z z = string_of_int (Int32.to_int (Camlcoq.camlint_of_z 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 f) + | Oaddrsymbol (id,i) -> Printf.sprintf "addrsymbol %s %s" (string_of_int (to_int id)) (string_of_z i) + | Oaddrstack i -> Printf.sprintf "addrstack %s" (string_of_z i) + | Ocast8signed -> "cast8signed" + | Ocast8unsigned -> "cast8unsigned" + | Ocast16signed -> "cast16signed" + | Ocast16unsigned -> "cast16unsigned" + | Oadd -> "add" + | Oaddimm i -> Printf.sprintf "addimm %s" (string_of_z i) + | Osub -> "sub" + | Osubimm i -> Printf.sprintf "subimm %s" (string_of_z i) + | 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) + | Onand -> "nand" + | Onor -> "nor" + | Onxor -> "nxor" + | 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" + | Orolm (i,j) -> Printf.sprintf "rolm %s %s" (string_of_z i) (string_of_z j) + | Onegf -> "negf" + | Oabsf -> "absf" + | Oaddf -> "addf" + | Osubf -> "subf" + | Omulf -> "mulf" + | Odivf -> "divf" + | Omuladdf -> "muladdf" + | Omulsubf -> "mulsubf" + | Osingleoffloat -> "singleoffloat" + | Ointoffloat -> "intoffloat" + | Ointuoffloat -> "intuoffloat" + | Ofloatofint -> "floatofint" + | Ofloatofintu -> "floatofintu" + | Ocmp c -> Printf.sprintf "cmpcmpcmp" + +let rec to_coq_list = function + | [] -> CList.Coq_nil + | e :: l -> CList.Coq_cons (e,(to_coq_list l)) + +let rec to_caml_list = function + | CList.Coq_nil -> [] + | CList.Coq_cons (e,l) -> e :: to_caml_list l -- cgit