diff options
Diffstat (limited to 'caml')
| -rw-r--r-- | caml/Allocationaux.ml | 39 | ||||
| -rw-r--r-- | caml/Allocationaux.mli | 5 | ||||
| -rw-r--r-- | caml/CMlexer.mll | 2 | ||||
| -rw-r--r-- | caml/CMparser.mly | 22 | ||||
| -rw-r--r-- | caml/CMtypecheck.ml | 22 | ||||
| -rw-r--r-- | caml/Camlcoq.ml | 5 | ||||
| -rw-r--r-- | caml/Coloringaux.ml | 10 | ||||
| -rw-r--r-- | caml/Floataux.ml | 13 | ||||
| -rw-r--r-- | caml/PrintPPC.ml | 67 | ||||
| -rw-r--r-- | caml/RTLtypingaux.ml | 122 |
10 files changed, 237 insertions, 70 deletions
diff --git a/caml/Allocationaux.ml b/caml/Allocationaux.ml deleted file mode 100644 index c682c3c1..00000000 --- a/caml/Allocationaux.ml +++ /dev/null @@ -1,39 +0,0 @@ -open Camlcoq -open Datatypes -open CList -open AST -open Locations - -type status = To_move | Being_moved | Moved - -let parallel_move_order lsrc ldst = - let src = array_of_coqlist lsrc - and dst = array_of_coqlist ldst in - let n = Array.length src in - let status = Array.make n To_move in - let moves = ref Coq_nil in - let rec move_one i = - if src.(i) <> dst.(i) then begin - status.(i) <- Being_moved; - for j = 0 to n - 1 do - if src.(j) = dst.(i) then - match status.(j) with - To_move -> - move_one j - | Being_moved -> - let tmp = - match Loc.coq_type src.(j) with - | Tint -> R IT2 - | Tfloat -> R FT2 in - moves := Coq_cons (Coq_pair(src.(j), tmp), !moves); - src.(j) <- tmp - | Moved -> - () - done; - moves := Coq_cons(Coq_pair(src.(i), dst.(i)), !moves); - status.(i) <- Moved - end in - for i = 0 to n - 1 do - if status.(i) = To_move then move_one i - done; - CList.rev !moves diff --git a/caml/Allocationaux.mli b/caml/Allocationaux.mli deleted file mode 100644 index 0cf3b944..00000000 --- a/caml/Allocationaux.mli +++ /dev/null @@ -1,5 +0,0 @@ -open Datatypes -open List -open Locations - -val parallel_move_order: loc list -> loc list -> (loc, loc) prod list diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll index b8d3ae74..49d0dbdd 100644 --- a/caml/CMlexer.mll +++ b/caml/CMlexer.mll @@ -20,6 +20,7 @@ rule token = parse | blank + { token lexbuf } | "/*" { comment lexbuf; token lexbuf } | "absf" { ABSF } + | "alloc" { ALLOC } | "&" { AMPERSAND } | "&&" { AMPERSANDAMPERSAND } | "!" { BANG } @@ -38,6 +39,7 @@ rule token = parse | "==f" { EQUALEQUALF } | "==u" { EQUALEQUALU } | "exit" { EXIT } + | "extern" { EXTERN } | "float" { FLOAT } | "float32" { FLOAT32 } | "float64" { FLOAT64 } diff --git a/caml/CMparser.mly b/caml/CMparser.mly index d461a157..5595afed 100644 --- a/caml/CMparser.mly +++ b/caml/CMparser.mly @@ -24,6 +24,7 @@ let orbool e1 e2 = %token ABSF %token AMPERSAND %token AMPERSANDAMPERSAND +%token ALLOC %token BANG %token BANGEQUAL %token BANGEQUALF @@ -41,6 +42,7 @@ let orbool e1 e2 = %token EQUALEQUALU %token EOF %token EXIT +%token EXTERN %token FLOAT %token FLOAT32 %token FLOAT64 @@ -120,7 +122,7 @@ let orbool e1 e2 = %left LESSLESS GREATERGREATER GREATERGREATERU %left PLUS PLUSF MINUS MINUSF %left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU -%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 +%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC %left LPAREN /* Entry point */ @@ -145,7 +147,8 @@ global_declarations: ; global_declaration: - VAR STRINGLIT LBRACKET INTLIT RBRACKET { Coq_pair($2, z_of_camlint $4) } + VAR STRINGLIT LBRACKET INTLIT RBRACKET + { Coq_pair($2, Coq_cons(Init_space (z_of_camlint $4), Coq_nil)) } ; proc_list: @@ -163,11 +166,15 @@ proc: stmt_list RBRACE { Coq_pair($1, - { fn_sig = $6; - fn_params = CList.rev $3; - fn_vars = CList.rev $9; - fn_stackspace = $8; - fn_body = $10 }) } + Internal { fn_sig = $6; + fn_params = CList.rev $3; + fn_vars = CList.rev $9; + fn_stackspace = $8; + fn_body = $10 }) } + | EXTERN STRINGLIT COLON signature + { Coq_pair($2, + External { ef_id = $2; + ef_sig = $4 }) } ; signature: @@ -250,6 +257,7 @@ expr: | INT16S expr { Cmconstr.cast16signed $2 } | INT16U expr { Cmconstr.cast16unsigned $2 } | FLOAT32 expr { Cmconstr.singleoffloat $2 } + | ALLOC expr { Ealloc $2 } | expr PLUS expr { Cmconstr.add $1 $3 } | expr MINUS expr { Cmconstr.sub $1 $3 } | expr STAR expr { Cmconstr.mul $1 $3 } diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml index b6f94cb5..4e700d7a 100644 --- a/caml/CMtypecheck.ml +++ b/caml/CMtypecheck.ml @@ -5,6 +5,7 @@ open Datatypes open CList open Camlcoq open AST +open Integers open Op open Cminor @@ -95,6 +96,8 @@ let type_operation = function | Oundef -> [], newvar() | Ocast8signed -> [tint], tint | Ocast16signed -> [tint], tint + | Ocast8unsigned -> [tint], tint + | Ocast16unsigned -> [tint], tint | Oadd -> [tint;tint], tint | Oaddimm _ -> [tint], tint | Osub -> [tint;tint], tint @@ -141,6 +144,8 @@ let name_of_operation = function | Oundef -> "undef" | Ocast8signed -> "cast8signed" | Ocast16signed -> "cast16signed" + | Ocast8unsigned -> "cast8unsigned" + | Ocast16unsigned -> "cast16unsigned" | Oadd -> "add" | Oaddimm n -> sprintf "addimm %ld" (camlint_of_coqint n) | Osub -> "sub" @@ -282,6 +287,14 @@ let rec type_expr env lenv e = te2 | Eletvar n -> type_letvar lenv n + | Ealloc e -> + let te = type_expr env lenv e in + begin try + unify tint te + with Error s -> + raise (Error (sprintf "In alloc:\n%s" s)) + end; + tint and type_exprlist env lenv el = match el with @@ -349,7 +362,7 @@ let rec env_of_vars idl = | Coq_nil -> [] | Coq_cons(id1, idt) -> (id1, newvar()) :: env_of_vars idt -let type_function (Coq_pair (id, f)) = +let type_function id f = try type_stmt (env_of_vars f.fn_vars @ env_of_vars f.fn_params) @@ -357,5 +370,10 @@ let type_function (Coq_pair (id, f)) = with Error s -> raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s)) +let type_fundef (Coq_pair (id, fd)) = + match fd with + | Internal f -> type_function id f + | External ef -> () + let type_program p = - coqlist_iter type_function p.prog_funct; p + coqlist_iter type_fundef p.prog_funct; p diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index b0bb4ff9..fc5d2d87 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -7,6 +7,11 @@ open BinInt (* Integers *) +let rec camlint_of_nat n = + match n with + | O -> 0l + | S n -> Int32.add (camlint_of_nat n) 1l + let rec camlint_of_positive = function | Coq_xI p -> Int32.add (Int32.shift_left (camlint_of_positive p) 1) 1l | Coq_xO p -> Int32.shift_left (camlint_of_positive p) 1 diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml index f4f4bcd3..a7c8db5c 100644 --- a/caml/Coloringaux.ml +++ b/caml/Coloringaux.ml @@ -266,15 +266,13 @@ let class_of_type = function Tint -> 0 | Tfloat -> 1 let num_register_classes = 2 let caller_save_registers = [| - [| R3; R4; R5; R6; R7; R8; R9; R10 |]; - [| F1; F2; F3; F4; F5; F6; F7; F8; F9; F10 |] + array_of_coqlist Conventions.int_caller_save_regs; + array_of_coqlist Conventions.float_caller_save_regs |] let callee_save_registers = [| - [| R13; R14; R15; R16; R17; R18; R19; R20; R21; R22; - R23; R24; R25; R26; R27; R28; R29; R30; R31 |]; - [| F14; F15; F16; F17; F18; F19; F20; F21; F22; - F23; F24; F25; F26; F27; F28; F29; F30; F31 |] + array_of_coqlist Conventions.int_callee_save_regs; + array_of_coqlist Conventions.float_callee_save_regs |] let num_available_registers = diff --git a/caml/Floataux.ml b/caml/Floataux.ml index f43efa27..f61bd5b5 100644 --- a/caml/Floataux.ml +++ b/caml/Floataux.ml @@ -1,4 +1,5 @@ open Camlcoq +open Integers let singleoffloat f = Int32.float_of_bits (Int32.bits_of_float f) @@ -15,9 +16,9 @@ let floatofintu i = let cmp c (x: float) (y: float) = match c with - | AST.Ceq -> x = y - | AST.Cne -> x <> y - | AST.Clt -> x < y - | AST.Cle -> x <= y - | AST.Cgt -> x > y - | AST.Cge -> x >= y + | Ceq -> x = y + | Cne -> x <> y + | Clt -> x < y + | Cle -> x <= y + | Cgt -> x > y + | Cge -> x >= y diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index 830de0d5..eaa383b4 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -26,10 +26,23 @@ let label_for_label lbl = Hashtbl.add current_function_labels lbl lbl'; lbl' +(* Record identifiers of external functions *) + +module IdentSet = Set.Make(struct type t = ident let compare = compare end) + +let extfuns = ref IdentSet.empty + +let record_extfun (Coq_pair(name, defn)) = + match defn with + | Internal _ -> () + | External _ -> extfuns := IdentSet.add name !extfuns + (* Basic printing functions *) let print_symb oc symb = - fprintf oc "_%s" (extern_atom symb) + if IdentSet.mem symb !extfuns + then fprintf oc "L%s$stub" (extern_atom symb) + else fprintf oc "_%s" (extern_atom symb) let print_label oc lbl = fprintf oc "L%d" (label_for_label lbl) @@ -99,6 +112,8 @@ let print_instruction oc labels = function fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 print_constant c | Paddze(r1, r2) -> fprintf oc " addze %a, %a\n" ireg r1 ireg r2 + | Pallocblock -> + fprintf oc " bl _compcert_alloc\n" | Pallocframe(lo, hi) -> let lo = camlint_of_coqint lo and hi = camlint_of_coqint hi in @@ -317,7 +332,7 @@ let rec labels_of_code = function Labelset.add lbl (labels_of_code c) | Coq_cons(_, c) -> labels_of_code c -let print_function oc (Coq_pair(name, code)) = +let print_function oc name code = Hashtbl.clear current_function_labels; fprintf oc " .text\n"; fprintf oc " .align 2\n"; @@ -325,10 +340,52 @@ let print_function oc (Coq_pair(name, code)) = fprintf oc "%a:\n" print_symb name; coqlist_iter (print_instruction oc (labels_of_code code)) code -let print_var oc (Coq_pair(name, size)) = - fprintf oc " .comm %a, %ld\n" print_symb name (camlint_of_z size) +let print_external_function oc name = + let name = extern_atom name in + fprintf oc " .text\n"; + fprintf oc " .align 2\n"; + fprintf oc "L%s$stub:\n" name; + fprintf oc " addis r11, 0, ha16(L%s$ptr)\n" name; + fprintf oc " lwz r11, lo16(L%s$ptr)(r11)\n" name; + fprintf oc " mtctr r11\n"; + fprintf oc " bctr\n"; + fprintf oc " .non_lazy_symbol_pointer\n"; + fprintf oc "L%s$ptr:\n" name; + fprintf oc " .indirect_symbol _%s\n" name; + fprintf oc " .long 0\n" + +let print_fundef oc (Coq_pair(name, defn)) = + match defn with + | Internal code -> print_function oc name code + | External ef -> print_external_function oc name + +let print_init_data oc = function + | Init_int8 n -> + fprintf oc " .byte %ld\n" (camlint_of_coqint n) + | Init_int16 n -> + fprintf oc " .short %ld\n" (camlint_of_coqint n) + | Init_int32 n -> + fprintf oc " .long %ld\n" (camlint_of_coqint n) + | Init_float32 n -> + fprintf oc " .long %ld # %g \n" (Int32.bits_of_float n) n + | Init_float64 n -> + fprintf oc " .quad %Ld # %g \n" (Int64.bits_of_float n) n + | Init_space n -> + let n = camlint_of_z n in + if n > 0l then fprintf oc " .space %ld\n" n + +let print_var oc (Coq_pair(name, init_data)) = + match init_data with + | Coq_nil -> () + | _ -> + fprintf oc " .data\n"; + fprintf oc " .globl %a\n" print_symb name; + fprintf oc "%a:" print_symb name; + coqlist_iter (print_init_data oc) init_data let print_program oc p = + extfuns := IdentSet.empty; + coqlist_iter record_extfun p.prog_funct; coqlist_iter (print_var oc) p.prog_vars; - coqlist_iter (print_function oc) p.prog_funct + coqlist_iter (print_fundef oc) p.prog_funct diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml new file mode 100644 index 00000000..b76a0bb8 --- /dev/null +++ b/caml/RTLtypingaux.ml @@ -0,0 +1,122 @@ +(* Type inference for RTL *) + +open Datatypes +open CList +open Camlcoq +open Maps +open AST +open Op +open Registers +open RTL + +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 raise (Type_error "type mismatch") + +let rec set_types rl tyl = + match rl, tyl with + | Coq_nil, Coq_nil -> () + | Coq_cons(r1, rs), Coq_cons(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 (Coq_pair(pc, i)) = + match i with + | Inop(_) -> + () + | Iop(Omove, _, _, _) -> + () + | Iop(Oundef, Coq_nil, res, _) -> + () + | Iop(Oundef, _, _, _) -> + raise (Type_error "wrong Oundef") + | Iop(op, args, res, _) -> + let (Coq_pair(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 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 None -> Tint | Some ty -> ty) + | 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, None -> () + | Some r, Some ty -> set_type r ty + | _, _ -> raise (Type_error "type mismatch in Ireturn") + end + +let type_pass1 retty instrs = + coqlist_iter (type_instr retty) instrs + +(* Second pass: extract move constraints typeof(r1) = typeof(r2) + and solve them iteratively *) + +let rec extract_moves = function + | Coq_nil -> [] + | Coq_cons(Coq_pair(pc, i), rem) -> + match i with + | Iop(Omove, Coq_cons(r1, Coq_nil), 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 |