diff options
Diffstat (limited to 'src/SoftwarePipelining/SPBase_types.ml')
| -rw-r--r-- | src/SoftwarePipelining/SPBase_types.ml | 63 |
1 files changed, 24 insertions, 39 deletions
diff --git a/src/SoftwarePipelining/SPBase_types.ml b/src/SoftwarePipelining/SPBase_types.ml index 3e339c3..ba92340 100644 --- a/src/SoftwarePipelining/SPBase_types.ml +++ b/src/SoftwarePipelining/SPBase_types.ml @@ -13,6 +13,7 @@ open Camlcoq open Op open Registers +open Memory open Mem open AST @@ -20,14 +21,13 @@ 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 + | 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 @@ -38,8 +38,7 @@ let inst_coq_to_caml = function | 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.Icond (cond, args, succ1, succ2) -> Icond (cond, args) | RTL.Ireturn (res) -> Ireturn (res) let inst_caml_to_coq i (links : RTL.node list) = @@ -50,23 +49,22 @@ let inst_caml_to_coq i (links : RTL.node list) = | 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) + | 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 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 - | CList.Coq_nil -> "" - | CList.Coq_cons (arg,args) -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args + | [] -> "" + | 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_z z = string_of_int (Z.to_int z) let string_of_comparison = function | Integers.Ceq -> "eq" @@ -89,17 +87,12 @@ let string_of_cond = function 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) + | Ofloatconst f -> Printf.sprintf "floatconst %s" (string_of_float (camlfloat_of_coqfloat32 f)) | 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" @@ -110,34 +103,26 @@ let string_of_op = function | 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" + | Ocmp c -> Printf.sprintf "cmpcmpcmp" + | Olea _ -> "lea" -let rec to_coq_list = function - | [] -> CList.Coq_nil - | e :: l -> CList.Coq_cons (e,(to_coq_list l)) +let to_coq_list = function + | [] -> [] + | e :: l -> e :: l -let rec to_caml_list = function - | CList.Coq_nil -> [] - | CList.Coq_cons (e,l) -> e :: to_caml_list l +let to_caml_list = function + | [] -> [] + | e :: l -> e :: l |