diff options
Diffstat (limited to 'src/pipelining/SPTyping.ml')
| -rw-r--r-- | src/pipelining/SPTyping.ml | 526 |
1 files changed, 526 insertions, 0 deletions
diff --git a/src/pipelining/SPTyping.ml b/src/pipelining/SPTyping.ml new file mode 100644 index 0000000..9b9c679 --- /dev/null +++ b/src/pipelining/SPTyping.ml @@ -0,0 +1,526 @@ +(***********************************************************************) +(* *) +(* Compcert Extensions *) +(* *) +(* Jean-Baptiste Tristan *) +(* *) +(* All rights reserved. This file is distributed under the terms *) +(* described in file ../../LICENSE. *) +(* *) +(***********************************************************************) + + +(*open Datatypes +open List +open Camlcoq +open Maps +open AST +open Op +open Registers +open RTL + +open Conventions +open Coqlib +open Errors +open Specif + +exception Type_error of string + +let env = ref (PTree.empty : typ PTree.t) + +let set_type r ty = + match PTree.get r !env with + | None -> env := PTree.set r ty !env + | Some ty' -> if ty <> ty' then + begin + Printf.fprintf SPDebug.dc "Failed to type register : %i " (P.to_int r); + raise (Type_error "type mismatch") + end + +let rec set_types rl tyl = + match rl, tyl with + | [], [] -> () + | r1 :: rs, ty1 :: tys -> set_type r1 ty1; set_types rs tys + | _, _ -> raise (Type_error "arity mismatch") + +(* First pass: process constraints of the form typeof(r) = ty *) + +let type_instr retty (pc, i) = + Printf.fprintf SPDebug.dc "typage de l'instruction : %i \n" (P.to_int pc); + match i with + | Inop(_) -> + () + | Iop(Omove, _, _, _) -> + () + | Iop(op, args, res, _) -> + let (targs, tres) = type_of_operation op in + set_types args targs; set_type res tres + | Iload(chunk, addr, args, dst, _) -> + set_types args (type_of_addressing addr); + set_type dst (type_of_chunk chunk) + | Istore(chunk, addr, args, src, _) -> + set_types args (type_of_addressing addr); + set_type src (type_of_chunk chunk) + | Icall(sg, ros, args, res, _) -> + begin try + begin match ros with + | Coq_inl r -> set_type r Tint + | Coq_inr _ -> () + end; + set_types args sg.sig_args; + set_type res (match sg.sig_res with Tret t -> t | _ -> Tint); + with Type_error msg -> + let name = + match ros with + | Coq_inl _ -> "<reg>" + | Coq_inr id -> extern_atom id in + raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s" + name msg)) + end + | Itailcall(sg, ros, args) -> + begin try + begin match ros with + | Coq_inl r -> set_type r Tint + | Coq_inr _ -> () + end; + set_types args sg.sig_args; + if sg.sig_res <> retty then + raise (Type_error "mismatch on return type") + with Type_error msg -> + let name = + match ros with + | Coq_inl _ -> "<reg>" + | Coq_inr id -> extern_atom id in + raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s" + name msg)) + end +(* | Ialloc(arg, res, _) -> + set_type arg Tint; set_type res Tint*) + | Icond(cond, args, _, _) -> + set_types args (type_of_condition cond) + | Ireturn(optres) -> + begin match optres, retty with + | None, Tvoid -> () + | Some r, Tret ty -> set_type r ty + | _, _ -> raise (Type_error "type mismatch in Ireturn") + end + +let type_pass1 retty instrs = + List.iter (type_instr retty) instrs + +(* Second pass: extract move constraints typeof(r1) = typeof(r2) + and solve them iteratively *) + +let rec extract_moves = function + | [] -> [] + | (pc, i) :: rem -> + match i with + | Iop(Omove, [r1], r2, _) -> + (r1, r2) :: extract_moves rem + | Iop(Omove, _, _, _) -> + raise (Type_error "wrong Omove") + | _ -> + extract_moves rem + +let changed = ref false + +let rec solve_moves = function + | [] -> [] + | (r1, r2) :: rem -> + match (PTree.get r1 !env, PTree.get r2 !env) with + | Some ty1, Some ty2 -> + if ty1 = ty2 + then (changed := true; solve_moves rem) + else raise (Type_error "type mismatch in Omove") + | Some ty1, None -> + env := PTree.set r2 ty1 !env; changed := true; solve_moves rem + | None, Some ty2 -> + env := PTree.set r1 ty2 !env; changed := true; solve_moves rem + | None, None -> + (r1, r2) :: solve_moves rem + +let rec iter_solve_moves mvs = + changed := false; + let mvs' = solve_moves mvs in + if !changed then iter_solve_moves mvs' + +let type_pass2 instrs = + iter_solve_moves (extract_moves instrs) + +let typeof e r = + match PTree.get r e with Some ty -> ty | None -> Tint + +let infer_type_environment f instrs = + try + env := PTree.empty; + set_types f.fn_params f.fn_sig.sig_args; + type_pass1 f.fn_sig.sig_res instrs; + type_pass2 instrs; + let e = !env in + env := PTree.empty; + Some(typeof e) + with Type_error msg -> + Printf.eprintf "Error during RTL type inference: %s\n" msg; + None + +(** val typ_eq : typ -> typ -> bool **) + +let typ_eq t1 t2 = + match t1 with + | Tint -> (match t2 with + | Tint -> true + | Tfloat -> false) + | Tfloat -> (match t2 with + | Tint -> false + | Tfloat -> true) + +(** val opt_typ_eq : typ option -> typ option -> bool **) + +let opt_typ_eq t1 t2 = + match t1 with + | Some x -> (match t2 with + | Some t -> typ_eq x t + | None -> false) + | None -> (match t2 with + | Some t -> false + | None -> true) + +(** val check_reg : regenv -> reg -> typ -> bool **) + +let check_reg env r ty = + match typ_eq (env r) ty with + | true -> true + | false -> false + +(** val check_regs : regenv -> reg list -> typ list -> bool **) + +let rec check_regs env rl tyl = + match rl with + | [] -> + (match tyl with + | [] -> true + | (t :: l) -> false) + | r1 :: rs -> + (match tyl with + | [] -> false + | (ty :: tys) -> + (match typ_eq (env r1) ty with + | true -> check_regs env rs tys + | false -> false)) + +(** val check_op : regenv -> operation -> reg list -> reg -> bool **) + +let check_op env op args res0 = + let (targs, tres) = type_of_operation op in + (match check_regs env args targs with + | true -> + (match typ_eq (env res0) tres with + | true -> true + | false -> false) + | false -> false) + +(** val check_successor : coq_function -> node -> bool **) + +let check_successor funct s = + match Maps.PTree.get s funct.fn_code with + | Some i -> true + | None -> false + +(** val check_instr : coq_function -> regenv -> instruction -> bool **) + +let check_instr funct env = function + | Inop s -> check_successor funct s + | Iop (op, args, res0, s) -> + (match op with + | Omove -> + (match args with + | Coq_nil -> false + | Coq_cons (arg, l) -> + (match l with + | Coq_nil -> + (match typ_eq (env arg) (env res0) with + | true -> check_successor funct s + | false -> false) + | Coq_cons (r, l0) -> false)) + | Ointconst i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ofloatconst f -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) +(* | Oaddrsymbol (i0, i1) -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false)*) +(* | Oaddrstack i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false)*) + | Ocast8signed -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocast8unsigned -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocast16signed -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocast16unsigned -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) +(* | Oadd -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oaddimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false)*) + | Osub -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Osubimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omul -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omulimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Odiv -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Odivu -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oand -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oandimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oor -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oorimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oxor -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oxorimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Onand -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Onor -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Onxor -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshl -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshr -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshrimm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshrximm i0 -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oshru -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Orolm (i0, i1) -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Onegf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oabsf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Oaddf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Osubf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omulf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Odivf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omuladdf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Omulsubf -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Osingleoffloat -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ointoffloat -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ointuoffloat -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ofloatofint -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ofloatofintu -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false) + | Ocmp c -> + (match check_op env op args res0 with + | true -> check_successor funct s + | false -> false)) + | Iload (chunk, addr, args, dst, s) -> + (match check_regs env args (type_of_addressing addr) with + | true -> + (match typ_eq (env dst) (type_of_chunk chunk) with + | true -> check_successor funct s + | false -> false) + | false -> false) + | Istore (chunk, addr, args, src, s) -> + (match check_regs env args (type_of_addressing addr) with + | true -> + (match typ_eq (env src) (type_of_chunk chunk) with + | true -> check_successor funct s + | false -> false) + | false -> false) + | Icall (sig0, ros, args, res0, s) -> + (match match ros with + | Coq_inl r -> + (match typ_eq (env r) Tint with + | true -> check_regs env args sig0.sig_args + | false -> false) + | Coq_inr s0 -> check_regs env args sig0.sig_args with + | true -> + (match typ_eq (env res0) (proj_sig_res sig0) with + | true -> check_successor funct s + | false -> false) + | false -> false) + | Itailcall (sig0, ros, args) -> + (match match match ros with + | Coq_inl r -> + (match typ_eq (env r) Tint with + | true -> check_regs env args sig0.sig_args + | false -> false) + | Coq_inr s -> check_regs env args sig0.sig_args with + | true -> + proj_sumbool + (opt_typ_eq sig0.sig_res funct.fn_sig.sig_res) + | false -> false with + | true -> tailcall_is_possible sig0 + | false -> false) +(* | Ialloc (arg, res0, s) -> + (match typ_eq (env arg) Tint with + | true -> + (match typ_eq (env res0) Tint with + | true -> check_successor funct s + | false -> false) + | false -> false)*) + | Icond (cond, args, s1, s2) -> + (match match check_regs env args (type_of_condition cond) with + | true -> check_successor funct s1 + | false -> false with + | true -> check_successor funct s2 + | false -> false) + | Ireturn optres -> + (match optres with + | Some r -> + (match funct.fn_sig.sig_res with + | Some t -> + (match typ_eq (env r) t with + | true -> true + | false -> false) + | None -> false) + | None -> + (match funct.fn_sig.sig_res with + | Some t -> false + | None -> true)) + +(** val check_params_norepet : reg list -> bool **) + +let check_params_norepet params = + match list_norepet_dec Registers.Reg.eq params with + | true -> true + | false -> false + +(** val check_instrs : coq_function -> regenv -> (node, instruction) prod + list -> bool **) + +let rec check_instrs funct env = function + | Coq_nil -> true + | Coq_cons (p, rem) -> + let Coq_pair (pc, i) = p in + (match check_instr funct env i with + | true -> check_instrs funct env rem + | false -> false) + +(** val type_function : coq_function -> unit **) + +let type_function f = + let instrs = Maps.PTree.elements f.fn_code in + match infer_type_environment f instrs with + | Some env -> + (match match match match check_regs env f.fn_params + f.fn_sig.sig_args with + | true -> check_params_norepet f.fn_params + | false -> false with + | true -> check_instrs f env instrs + | false -> false with + | true -> check_successor f f.fn_entrypoint + | false -> false with + | true -> Printf.fprintf SPDebug.dc "The code is well typed\n" + | false -> failwith "Type checking failure\n") + | None -> failwith "Type inference failure\n" +*) |