diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:10:55 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:10:55 +0000 |
commit | 82d69d247c7de8387b92936086abdc3d441c8628 (patch) | |
tree | 227f7db7e785f1c3affa2028bc2484e0771d54f4 /src/pipelining/SPBase_types.ml | |
parent | fea7ee4d30aa7597ff5b8e2a2954ed452a1a7a57 (diff) | |
download | vericert-82d69d247c7de8387b92936086abdc3d441c8628.tar.gz vericert-82d69d247c7de8387b92936086abdc3d441c8628.zip |
Rename pipelining
Diffstat (limited to 'src/pipelining/SPBase_types.ml')
-rw-r--r-- | src/pipelining/SPBase_types.ml | 128 |
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 |