From 5b05d3668571bd9b748b781b0cc29ae10f745f61 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 10 Mar 2016 13:35:48 +0100 Subject: Code cleanup. Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394. --- backend/CMlexer.mll | 2 - backend/CMparser.mly | 12 ++-- backend/CMtypecheck.ml | 29 ++------ backend/Fileinfo.ml | 4 +- backend/IRC.ml | 57 ++------------- backend/IRC.mli | 1 - backend/Inliningaux.ml | 4 +- backend/Linearizeaux.ml | 13 ++-- backend/PrintAsm.ml | 7 +- backend/PrintAsm.mli | 2 +- backend/PrintAsmaux.ml | 1 - backend/PrintCminor.ml | 3 +- backend/PrintLTL.ml | 7 +- backend/PrintMach.ml | 8 +-- backend/PrintRTL.ml | 6 +- backend/PrintXTL.ml | 12 ++-- backend/RTLgenaux.ml | 42 ++++++----- backend/Regalloc.ml | 184 ++++++++++++++++++++++++------------------------ backend/Splitting.ml | 4 +- backend/XTL.ml | 24 +++---- 20 files changed, 166 insertions(+), 256 deletions(-) (limited to 'backend') diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index 6695b6b7..82769924 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -14,8 +14,6 @@ (* *********************************************************************) { -open BinNums -open Camlcoq open CMparser exception Error of string } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 5f189e7b..b20dea38 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -17,7 +17,7 @@ including function calls in expressions, matches, while statements, etc. */ %{ -open Datatypes +open !Datatypes open Camlcoq open BinNums open Integers @@ -210,17 +210,17 @@ let mkmatch_aux expr cases = let ncases = List.length cases in let rec mktable n = function | [] -> assert false - | [key, action] -> [] - | (key, action) :: rem -> + | [_, _] -> [] + | (key, _) :: rem -> (coqint_of_camlint key, Nat.of_int n) :: mktable (n + 1) rem in let sw = Sswitch(false, expr, mktable 0 cases, Nat.of_int (ncases - 1)) in let rec mkblocks body n = function | [] -> assert false - | [key, action] -> + | [_, action] -> Sblock(Sseq(body, action)) - | (key, action) :: rem -> + | (_, action) :: rem -> mkblocks (Sblock(Sseq(body, Sseq(action, Sexit (Nat.of_int n))))) (n - 1) @@ -233,7 +233,7 @@ let mkmatch expr cases = let s = match cases with | [] -> Sskip (* ??? *) - | [key, action] -> action + | [_, action] -> action | _ -> mkmatch_aux c cases in prepend_seq !convert_accu s diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 72bf9cb4..399eb9bd 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -18,11 +18,9 @@ (* FIXME: proper support for type Tsingle *) open Printf -open Datatypes open Camlcoq open AST open PrintAST -open Integers open Cminor exception Error of string @@ -74,21 +72,6 @@ let type_var env id = with Not_found -> raise (Error (sprintf "Unbound variable %s\n" (extern_atom id))) -let type_letvar env n = - let n = Nat.to_int n in - try - List.nth env n - with Not_found -> - raise (Error (sprintf "Unbound let variable #%d\n" n)) - -let name_of_comparison = function - | Ceq -> "eq" - | Cne -> "ne" - | Clt -> "lt" - | Cle -> "le" - | Cgt -> "gt" - | Cge -> "ge" - let type_constant = function | Ointconst _ -> tint | Ofloatconst _ -> tfloat @@ -313,12 +296,12 @@ let rec type_stmt env blk ret s = | Sexit n -> if Nat.to_int n >= blk then raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n))) - | Sswitch(islong, e, cases, deflt) -> + | Sswitch(islong, e, _, _) -> unify (type_expr env [] e) (if islong then tlong else tint) | Sreturn None -> begin match ret with | None -> () - | Some tret -> raise (Error ("return without argument")) + | Some _ -> raise (Error ("return without argument")) end | Sreturn (Some e) -> begin match ret with @@ -339,9 +322,9 @@ let rec type_stmt env blk ret s = with Error s -> raise (Error (sprintf "In tail call:\n%s" s)) end - | Slabel(lbl, s1) -> + | Slabel(_, s1) -> type_stmt env blk ret s1 - | Sgoto lbl -> + | Sgoto _ -> () let rec env_of_vars idl = @@ -360,8 +343,8 @@ let type_function id f = let type_globdef (id, gd) = match gd with | Gfun(Internal f) -> type_function id f - | Gfun(External ef) -> () - | Gvar v -> () + | Gfun(External _) -> () + | Gvar _ -> () let type_program p = List.iter type_globdef p.prog_defs; p diff --git a/backend/Fileinfo.ml b/backend/Fileinfo.ml index 0490def0..a78a24db 100644 --- a/backend/Fileinfo.ml +++ b/backend/Fileinfo.ml @@ -25,7 +25,7 @@ let reset_filenames () = let close_filenames () = Hashtbl.iter - (fun file (num, fb) -> + (fun _ (_, fb) -> match fb with Some b -> Printlines.close b | None -> ()) filename_info; reset_filenames() @@ -46,7 +46,7 @@ let print_file oc file = try Hashtbl.find filename_info file with Not_found -> - let (filenum, filebuf as res) = enter_filename file in + let (filenum, _ as res) = enter_filename file in fprintf oc " .file %d %S\n" filenum file; res diff --git a/backend/IRC.ml b/backend/IRC.ml index eb677069..8780bce3 100644 --- a/backend/IRC.ml +++ b/backend/IRC.ml @@ -12,13 +12,11 @@ open Printf open Camlcoq -open Datatypes open AST open Registers open Machregs open Locations open Conventions1 -open Conventions open XTL (* Iterated Register Coalescing: George and Appel's graph coloring algorithm *) @@ -116,7 +114,7 @@ let name_of_loc = function let name_of_node n = match n.var with - | V(r, ty) -> sprintf "x%ld" (P.to_int32 r) + | V(r, _) -> sprintf "x%ld" (P.to_int32 r) | L l -> name_of_loc l (* The algorithm manipulates partitions of the nodes and of the moves @@ -138,7 +136,6 @@ module DLinkNode = struct nstate = state; nprev = empty; nnext = empty } in empty let dummy = make Colored - let clear dl = dl.nnext <- dl; dl.nprev <- dl let notempty dl = dl.nnext != dl let insert n dl = n.nstate <- dl.nstate; @@ -167,7 +164,6 @@ module DLinkMove = struct mstate = state; mprev = empty; mnext = empty } in empty let dummy = make CoalescedMoves - let clear dl = dl.mnext <- dl; dl.mprev <- dl let notempty dl = dl.mnext != dl let insert m dl = m.mstate <- dl.mstate; @@ -180,12 +176,6 @@ module DLinkMove = struct remove m dl1; insert m dl2 let pick dl = let m = dl.mnext in remove m dl; m - let iter f dl = - let rec iter m = if m != dl then (f m; iter m.mnext) - in iter dl.mnext - let fold f dl accu = - let rec fold m accu = if m == dl then accu else fold m.mnext (f m accu) - in fold dl.mnext accu end (* Auxiliary data structures *) @@ -447,7 +437,7 @@ let moveRelated n = (* Initial partition of nodes into spill / freeze / simplify *) let initialNodePartition g = - let part_node v n = + let part_node n = match n.nstate with | Initial -> let k = g.num_available_registers.(n.regclass) in @@ -459,44 +449,7 @@ let initialNodePartition g = DLinkNode.insert n g.simplifyWorklist | Colored -> () | _ -> assert false in - Hashtbl.iter part_node g.varTable - - -(* Check invariants *) - -let degreeInvariant g n = - let c = ref 0 in - iterAdjacent (fun n -> incr c) n; - if !c <> n.degree then - failwith("degree invariant violated by " ^ name_of_node n) - -let simplifyWorklistInvariant g n = - if n.degree < g.num_available_registers.(n.regclass) - && not (moveRelated n) - then () - else failwith("simplify worklist invariant violated by " ^ name_of_node n) - -let freezeWorklistInvariant g n = - if n.degree < g.num_available_registers.(n.regclass) - && moveRelated n - then () - else failwith("freeze worklist invariant violated by " ^ name_of_node n) - -let spillWorklistInvariant g n = - if n.degree >= g.num_available_registers.(n.regclass) - then () - else failwith("spill worklist invariant violated by " ^ name_of_node n) - -let checkInvariants g = - DLinkNode.iter - (fun n -> degreeInvariant g n; simplifyWorklistInvariant g n) - g.simplifyWorklist; - DLinkNode.iter - (fun n -> degreeInvariant g n; freezeWorklistInvariant g n) - g.freezeWorklist; - DLinkNode.iter - (fun n -> degreeInvariant g n; spillWorklistInvariant g n) - g.spillWorklist + Hashtbl.iter (fun _ a -> part_node a) g.varTable (* Enable moves that have become low-degree related *) @@ -737,7 +690,7 @@ let selectSpill g = (* Find a spillable node of minimal cost *) let (n, cost) = DLinkNode.fold - (fun n (best_node, best_cost as best) -> + (fun n (_, best_cost as best) -> (* Manual inlining of [spillCost] above plus algebraic simplif *) let deg = float n.degree in let deg2 = deg *. deg in @@ -894,7 +847,7 @@ let assign_color g n = let location_of_var g v = match v with | L l -> l - | V(r, ty) -> + | V(_, ty) -> try let n = Hashtbl.find g.varTable v in let n' = getAlias n in diff --git a/backend/IRC.mli b/backend/IRC.mli index e81b6dc5..d27dedaa 100644 --- a/backend/IRC.mli +++ b/backend/IRC.mli @@ -12,7 +12,6 @@ (* Iterated Register Coalescing: George and Appel's graph coloring algorithm *) -open AST open Registers open Machregs open Locations diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 42129166..7893da89 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -10,9 +10,7 @@ (* *) (* *********************************************************************) -open Camlcoq - (* To be considered: heuristics based on size of function? *) -let should_inline (id: AST.ident) (f: RTL.coq_function) = +let should_inline (id: AST.ident) (_: RTL.coq_function) = C2C.atom_is_inline id diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 71ee2e56..41a98873 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -10,10 +10,7 @@ (* *) (* *********************************************************************) -open Coqlib -open Datatypes open LTL -open Lattice open Maps open Camlcoq @@ -82,13 +79,13 @@ let basic_blocks f joins = let rec do_instr_list = function | [] -> assert false | Lbranch s :: _ -> next_in_block blk minpc s - | Ltailcall (sig0, ros) :: _ -> end_block blk minpc - | Lcond (cond, args, ifso, ifnot) :: _ -> + | Ltailcall _ :: _ -> end_block blk minpc + | Lcond (_, _, ifso, ifnot) :: _ -> end_block blk minpc; start_block ifso; start_block ifnot - | Ljumptable(arg, tbl) :: _ -> + | Ljumptable(_, tbl) :: _ -> end_block blk minpc; List.iter start_block tbl | Lreturn :: _ -> end_block blk minpc - | instr :: b' -> do_instr_list b' in + | _ :: b' -> do_instr_list b' in do_instr_list b (* next_in_block: check if join point and either extend block or start block *) @@ -113,5 +110,5 @@ let flatten_blocks blks = (* Build the enumeration *) -let enumerate_aux f reach = +let enumerate_aux f _ = flatten_blocks (basic_blocks f (join_points f)) diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 6c1eda57..6eff7c02 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -12,9 +12,8 @@ (* *********************************************************************) open AST -open Asm open Camlcoq -open Datatypes +open !Datatypes open DwarfPrinter open PrintAsmaux open Printf @@ -105,7 +104,7 @@ module Printer(Target:TARGET) = let print_globdef oc (name,gdef) = match gdef with | Gfun (Internal code) -> print_function oc name code - | Gfun (External ef) -> () + | Gfun (External _) -> () | Gvar v -> print_var oc name v module DwarfTarget: DwarfTypes.DWARF_TARGET = @@ -119,7 +118,7 @@ module Printer(Target:TARGET) = module DebugPrinter = DwarfPrinter (DwarfTarget) end -let print_program oc p db = +let print_program oc p = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in Fileinfo.reset_filenames (); diff --git a/backend/PrintAsm.mli b/backend/PrintAsm.mli index 0b2869b0..29e91540 100644 --- a/backend/PrintAsm.mli +++ b/backend/PrintAsm.mli @@ -11,4 +11,4 @@ (* *) (* *********************************************************************) -val print_program: out_channel -> Asm.program -> DwarfTypes.dw_entry option -> unit +val print_program: out_channel -> Asm.program -> unit diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 0ca5b8e0..148c5300 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -14,7 +14,6 @@ open AST open Asm open Camlcoq -open Datatypes open Memdata open Printf open Sections diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 9b6b1488..5e686b55 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -17,7 +17,6 @@ open Format open Camlcoq -open Datatypes open Integers open AST open PrintAST @@ -27,7 +26,7 @@ open Cminor type associativity = LtoR | RtoL | NA -let rec precedence = function +let precedence = function | Evar _ -> (16, NA) | Econst _ -> (16, NA) | Eunop _ -> (15, RtoL) diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 0f78bc58..ba28b30d 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -17,8 +17,7 @@ open Camlcoq open Datatypes open Maps open AST -open Integers -open Locations +open !Locations open LTL open PrintAST open PrintOp @@ -73,9 +72,9 @@ let print_instruction pp succ = function | Lstore(chunk, addr, args, src) -> fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing mreg) (addr, args) mreg src - | Lcall(sg, fn) -> + | Lcall(_, fn) -> fprintf pp "call %a" ros fn - | Ltailcall(sg, fn) -> + | Ltailcall(_, fn) -> fprintf pp "tailcall %a" ros fn | Lbuiltin(ef, args, res) -> fprintf pp "%a = %s(%a)" diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index 0ce2e87b..07ec6a1a 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -15,14 +15,10 @@ open Printf open Camlcoq open Datatypes -open Maps open AST -open Integers -open Locations open Machregsaux open Mach open PrintAST -open PrintOp let reg pp r = match name_of_register r with @@ -61,9 +57,9 @@ let print_instruction pp i = (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src - | Mcall(sg, fn) -> + | Mcall(_, fn) -> fprintf pp "\tcall %a\n" ros fn - | Mtailcall(sg, fn) -> + | Mtailcall(_, fn) -> fprintf pp "\ttailcall %a\n" ros fn | Mbuiltin(ef, args, res) -> fprintf pp "\t%a = %s(%a)\n" diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index f2242c13..a22aa422 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -17,10 +17,8 @@ open Camlcoq open Datatypes open Maps open AST -open Integers open RTL open PrintAST -open PrintOp (* Printing of RTL code *) @@ -63,11 +61,11 @@ let print_instruction pp (pc, i) = (PrintOp.print_addressing reg) (addr, args) reg src; print_succ pp s (pc - 1) - | Icall(sg, fn, args, res, s) -> + | Icall(_, fn, args, res, s) -> fprintf pp "%a = %a(%a)\n" reg res ros fn regs args; print_succ pp s (pc - 1) - | Itailcall(sg, fn, args) -> + | Itailcall(_, fn, args) -> fprintf pp "tailcall %a(%a)\n" ros fn regs args | Ibuiltin(ef, args, res, s) -> diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index dd8434da..1bee1e15 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -17,9 +17,7 @@ open Camlcoq open Datatypes open Maps open AST -open Registers -open Op -open Locations +open !Locations open PrintAST open PrintOp open XTL @@ -69,8 +67,8 @@ let ros pp = function let liveset pp lv = fprintf pp "{"; - VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r) - | L l -> ()) + VSet.iter (function V(r, _) -> fprintf pp " x%d" (P.to_int r) + | L _ -> ()) lv; fprintf pp " }" @@ -95,9 +93,9 @@ let print_instruction pp succ = function | Xstore(chunk, addr, args, src) -> fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing var) (addr, args) var src - | Xcall(sg, fn, args, res) -> + | Xcall(_, fn, args, res) -> fprintf pp "%a = call %a(%a)" vars res ros fn vars args - | Xtailcall(sg, fn, args) -> + | Xtailcall(_, fn, args) -> fprintf pp "tailcall %a(%a)" ros fn vars args | Xbuiltin(ef, args, res) -> fprintf pp "%a = %s(%a)" diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 045299d4..fdf41897 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -11,9 +11,7 @@ (* *********************************************************************) open Datatypes -open Camlcoq open AST -open Switch open CminorSel (* Heuristic to orient if-then-else statements. @@ -28,22 +26,22 @@ open CminorSel putting the bigger of the two branches in fall-through position. *) let rec size_expr = function - | Evar id -> 0 - | Eop(op, args) -> 1 + size_exprs args - | Eload(chunk, addr, args) -> 1 + size_exprs args + | Evar _ -> 0 + | Eop(_, args) -> 1 + size_exprs args + | Eload(_, _, args) -> 1 + size_exprs args | Econdition(ce, e1, e2) -> 1 + size_condexpr ce + max (size_expr e1) (size_expr e2) | Elet(e1, e2) -> size_expr e1 + size_expr e2 - | Eletvar n -> 0 - | Ebuiltin(ef, el) -> 2 + size_exprs el - | Eexternal(id, sg, el) -> 5 + size_exprs el + | Eletvar _ -> 0 + | Ebuiltin(_, el) -> 2 + size_exprs el + | Eexternal(_, _, el) -> 5 + size_exprs el and size_exprs = function | Enil -> 0 | Econs(e1, el) -> size_expr e1 + size_exprs el and size_condexpr = function - | CEcond(c, args) -> size_exprs args + | CEcond(_, args) -> size_exprs args | CEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3 | CElet(a, c) -> @@ -54,8 +52,8 @@ let size_exprlist al = List.fold_right (fun a s -> size_expr a + s) al 0 let size_builtin_args al = size_exprlist (params_of_builtin_args al) let rec size_exitexpr = function - | XEexit n -> 0 - | XEjumptable(arg, tbl) -> 2 + size_expr arg + | XEexit _ -> 0 + | XEjumptable(arg, _) -> 2 + size_expr arg | XEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_exitexpr c2 + size_exitexpr c3 | XElet(a, c) -> @@ -63,34 +61,34 @@ let rec size_exitexpr = function let rec length_exprs = function | Enil -> 0 - | Econs(e1, el) -> 1 + length_exprs el + | Econs(_, el) -> 1 + length_exprs el let size_eos = function | Coq_inl e -> size_expr e - | Coq_inr id -> 0 + | Coq_inr _ -> 0 let rec size_stmt = function | Sskip -> 0 - | Sassign(id, a) -> size_expr a - | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src - | Scall(optid, sg, eos, args) -> + | Sassign(_, a) -> size_expr a + | Sstore(_, _, args, src) -> 1 + size_exprs args + size_expr src + | Scall(_, _, eos, args) -> 3 + size_eos eos + size_exprs args + length_exprs args - | Stailcall(sg, eos, args) -> + | Stailcall(_, eos, args) -> 3 + size_eos eos + size_exprs args + length_exprs args | Sbuiltin(_, (EF_annot _ | EF_debug _), _) -> 0 - | Sbuiltin(optid, ef, args) -> 1 + size_builtin_args args + | Sbuiltin(_, _, args) -> 1 + size_builtin_args args | Sseq(s1, s2) -> size_stmt s1 + size_stmt s2 | Sifthenelse(ce, s1, s2) -> size_condexpr ce + max (size_stmt s1) (size_stmt s2) | Sloop s -> 1 + 4 * size_stmt s | Sblock s -> size_stmt s - | Sexit n -> 1 + | Sexit _ -> 1 | Sswitch xe -> size_exitexpr xe | Sreturn None -> 2 | Sreturn (Some arg) -> 2 + size_expr arg - | Slabel(lbl, s) -> size_stmt s - | Sgoto lbl -> 1 + | Slabel(_, s) -> size_stmt s + | Sgoto _ -> 1 -let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = +let more_likely (_: condexpr) (ifso: stmt) (ifnot: stmt) = size_stmt ifso > size_stmt ifnot diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index a5fa8cd7..ee35d7a0 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -33,9 +33,7 @@ open Datatypes open Coqlib open Maps open AST -open Memdata open Kildall -open Registers open Op open Machregs open Locations @@ -87,16 +85,16 @@ let constrain_reg v c = let rec constrain_regs vl cl = match vl, cl with | [], _ -> [] - | v1 :: vl', [] -> vl - | v1 :: vl', Some mr1 :: cl' -> L(R mr1) :: constrain_regs vl' cl' + | _ :: _, [] -> vl + | _ :: vl', Some mr1 :: cl' -> L(R mr1) :: constrain_regs vl' cl' | v1 :: vl', None :: cl' -> v1 :: constrain_regs vl' cl' let move v1 v2 k = if v1 = v2 then k - else if is_stack_reg v1 then begin + else if XTL.is_stack_reg v1 then begin let t = new_temp (typeof v2) in Xmove(v1, t) :: Xmove(t, v2) :: k - end else if is_stack_reg v2 then begin + end else if XTL.is_stack_reg v2 then begin let t = new_temp (typeof v1) in Xmove(v1, t) :: Xmove(t, v2) :: k end else Xmove(v1, v2) :: k @@ -142,8 +140,8 @@ let convert_builtin_res tyenv = function let rec constrain_builtin_arg a cl = match a, cl with - | BA x, None :: cl' -> (a, cl') - | BA x, Some mr :: cl' -> (BA (L(R mr)), cl') + | BA _, None :: cl' -> (a, cl') + | BA _, Some mr :: cl' -> (BA (L(R mr)), cl') | BA_splitlong(hi, lo), _ -> let (hi', cl1) = constrain_builtin_arg hi cl in let (lo', cl2) = constrain_builtin_arg lo cl1 in @@ -160,8 +158,8 @@ let rec constrain_builtin_args al cl = let rec constrain_builtin_res a cl = match a, cl with - | BR x, None :: cl' -> (a, cl') - | BR x, Some mr :: cl' -> (BR (L(R mr)), cl') + | BR _, None :: cl' -> (a, cl') + | BR _, Some mr :: cl' -> (BR (L(R mr)), cl') | BR_splitlong(hi, lo), _ -> let (hi', cl1) = constrain_builtin_res hi cl in let (lo', cl2) = constrain_builtin_res lo cl1 in @@ -264,7 +262,7 @@ let block_of_RTL_instr funsig tyenv = function let next_pc f = PTree.fold - (fun npc pc i -> if P.lt pc npc then npc else P.succ pc) + (fun npc pc _ -> if P.lt pc npc then npc else P.succ pc) f.RTL.fn_code P.one (* Translate an RTL function to an XTL function *) @@ -289,7 +287,7 @@ let vset_removelist vl after = List.fold_right VSet.remove vl after let vset_addlist vl after = List.fold_right VSet.add vl after let vset_addros vos after = - match vos with Coq_inl v -> VSet.add v after | Coq_inr id -> after + match vos with Coq_inl v -> VSet.add v after | Coq_inr _ -> after let rec vset_addarg a after = match a with @@ -308,34 +306,34 @@ let rec vset_removeres r after = let live_before instr after = match instr with | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) -> - if VSet.mem dst after || is_stack_reg src + if VSet.mem dst after || XTL.is_stack_reg src then VSet.add src (VSet.remove dst after) else after - | Xparmove(srcs, dsts, itmp, ftmp) -> + | Xparmove(srcs, dsts, _, _) -> vset_addlist srcs (vset_removelist dsts after) - | Xop(op, args, res) -> + | Xop(_, args, res) -> if VSet.mem res after then vset_addlist args (VSet.remove res after) else after - | Xload(chunk, addr, args, dst) -> + | Xload(_, _, args, dst) -> if VSet.mem dst after then vset_addlist args (VSet.remove dst after) else after - | Xstore(chunk, addr, args, src) -> + | Xstore(_, _, args, src) -> vset_addlist args (VSet.add src after) - | Xcall(sg, ros, args, res) -> + | Xcall(_, ros, args, res) -> vset_addlist args (vset_addros ros (vset_removelist res after)) - | Xtailcall(sg, ros, args) -> + | Xtailcall(_, ros, args) -> vset_addlist args (vset_addros ros VSet.empty) - | Xbuiltin(EF_debug _, args, res) -> + | Xbuiltin(EF_debug _, _, res) -> vset_removeres res after - | Xbuiltin(ef, args, res) -> + | Xbuiltin(_, args, res) -> vset_addargs args (vset_removeres res after) - | Xbranch s -> + | Xbranch _ -> after - | Xcond(cond, args, s1, s2) -> + | Xcond(_, args, _, _) -> List.fold_right VSet.add args after - | Xjumptable(arg, tbl) -> + | Xjumptable(arg, _) -> VSet.add arg after | Xreturn args -> vset_addlist args VSet.empty @@ -385,7 +383,7 @@ let rec dce_parmove srcs dsts after = | [], [] -> [], [] | src1 :: srcs, dst1 :: dsts -> let (srcs', dsts') = dce_parmove srcs dsts after in - if VSet.mem dst1 after || is_stack_reg src1 + if VSet.mem dst1 after || XTL.is_stack_reg src1 then (src1 :: srcs', dst1 :: dsts') else (srcs', dsts') | _, _ -> assert false @@ -399,7 +397,7 @@ let rec keep_builtin_arg after = function let dce_instr instr after k = match instr with | Xmove(src, dst) -> - if VSet.mem dst after || is_stack_reg src + if VSet.mem dst after || XTL.is_stack_reg src then instr :: k else k | Xparmove(srcs, dsts, itmp, ftmp) -> @@ -408,11 +406,11 @@ let dce_instr instr after k = | ([src], [dst]) -> Xmove(src, dst) :: k | (srcs', dsts') -> Xparmove(srcs', dsts', itmp, ftmp) :: k end - | Xop(op, args, res) -> + | Xop(_, _, res) -> if VSet.mem res after then instr :: k else k - | Xload(chunk, addr, args, dst) -> + | Xload(_, _, _, dst) -> if VSet.mem dst after then instr :: k else k @@ -431,7 +429,7 @@ let rec dce_block blk after = let dead_code_elimination f liveness = { f with fn_code = - PTree.map (fun pc blk -> snd(dce_block blk (PMap.get pc liveness))) + PTree.map (fun pc blk -> Datatypes.snd(dce_block blk (PMap.get pc liveness))) f.fn_code } @@ -454,8 +452,8 @@ let spill_costs f = let charge amount uses v = match v with - | L l -> () - | V(r, ty) -> + | L _ -> () + | V(r, _) -> let st = get_stats r in if st.cost < 0 then (* the variable must be spilled, don't change its cost *) @@ -472,21 +470,21 @@ let spill_costs f = List.iter (charge amount uses) vl in let charge_ros amount ros = - match ros with Coq_inl v -> charge amount 1 v | Coq_inr id -> () in + match ros with Coq_inl v -> charge amount 1 v | Coq_inr _ -> () in let force_stack_allocation v = match v with - | L l -> () - | V(r, ty) -> + | L _ -> () + | V(r,_) -> let st = get_stats r in assert (st.cost < max_int); st.cost <- (-1) in let charge_instr = function | Xmove(src, dst) -> - if is_stack_reg src then + if XTL.is_stack_reg src then force_stack_allocation dst - else if is_stack_reg dst then + else if XTL.is_stack_reg dst then force_stack_allocation src else begin charge 1 1 src; charge 1 1 dst @@ -501,15 +499,15 @@ let spill_costs f = charge_list 1 1 srcs; charge_list 1 1 dsts; charge max_int 0 itmp; charge max_int 0 ftmp (* temps must not be spilled *) - | Xop(op, args, res) -> + | Xop(_, args, res) -> charge_list 10 1 args; charge 10 1 res - | Xload(chunk, addr, args, dst) -> + | Xload(_, _, args, dst) -> charge_list 10 1 args; charge 10 1 dst - | Xstore(chunk, addr, args, src) -> + | Xstore(_, _, args, src) -> charge_list 10 1 args; charge 10 1 src - | Xcall(sg, vos, args, res) -> + | Xcall(_, vos, _, _) -> charge_ros 10 vos - | Xtailcall(sg, vos, args) -> + | Xtailcall(_, vos, _) -> charge_ros 10 vos | Xbuiltin(ef, args, res) -> begin match ef with @@ -528,11 +526,11 @@ let spill_costs f = charge_list 10 1 (params_of_builtin_res res) end | Xbranch _ -> () - | Xcond(cond, args, _, _) -> + | Xcond(_, args, _, _) -> charge_list 10 1 args | Xjumptable(arg, _) -> charge 10 1 arg - | Xreturn optarg -> + | Xreturn _ -> () in let charge_block blk = List.iter charge_instr blk in @@ -595,12 +593,12 @@ let add_interfs_instr g instr live = add_interfs_list g itmp srcs; add_interfs_list g itmp dsts; add_interfs_list g ftmp srcs; add_interfs_list g ftmp dsts; (* Take into account destroyed reg when accessing Incoming param *) - if List.exists (function (L(S(Incoming, _, _))) -> true | _ -> false) srcs + if List.exists (function (L(Locations.S(Incoming, _, _))) -> true | _ -> false) srcs then add_interfs_list g (vmreg temp_for_parent_frame) dsts; (* Take into account destroyed reg when initializing Outgoing arguments of type Tsingle *) if List.exists - (function (L(S(Outgoing, _, Tsingle))) -> true | _ -> false) dsts + (function (L(Locations.S(Outgoing, _, Tsingle))) -> true | _ -> false) dsts then List.iter (fun mr -> @@ -622,17 +620,17 @@ let add_interfs_instr g instr live = (vset_addlist (res :: argl) (VSet.remove res live)) end; add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op) - | Xload(chunk, addr, args, dst) -> + | Xload(chunk, addr, _, dst) -> add_interfs_def g dst live; add_interfs_destroyed g (VSet.remove dst live) (destroyed_by_load chunk addr) - | Xstore(chunk, addr, args, src) -> + | Xstore(chunk, addr, _,_) -> add_interfs_destroyed g live (destroyed_by_store chunk addr) - | Xcall(sg, vos, args, res) -> + | Xcall(_, _,_, res) -> add_interfs_destroyed g (vset_removelist res live) destroyed_at_call - | Xtailcall(sg, Coq_inl v, args) -> + | Xtailcall(_, Coq_inl v, _) -> List.iter (fun r -> IRC.add_interf g (vmreg r) v) int_callee_save_regs - | Xtailcall(sg, Coq_inr id, args) -> + | Xtailcall(_, Coq_inr _, _) -> () | Xbuiltin(ef, args, res) -> (* Interferences with live across *) @@ -646,7 +644,7 @@ let add_interfs_instr g instr live = | EF_annot_val _, [BA arg], BR res -> (* like a move *) IRC.add_pref g arg res - | EF_inline_asm(txt, sg, clob), _, _ -> + | EF_inline_asm(_, _, clob), _, _ -> let vargs = params_of_builtin_args args in (* clobbered regs interfere with res and args for GCC compatibility *) List.iter (fun c -> @@ -658,13 +656,13 @@ let add_interfs_instr g instr live = clob | _ -> () end - | Xbranch s -> + | Xbranch _ -> () - | Xcond(cond, args, s1, s2) -> + | Xcond(cond, _, _,_) -> add_interfs_destroyed g live (destroyed_by_cond cond) - | Xjumptable(arg, tbl) -> + | Xjumptable _ -> add_interfs_destroyed g live destroyed_by_jumptable - | Xreturn optarg -> + | Xreturn _ -> () let rec add_interfs_block g blk live = @@ -690,16 +688,16 @@ let find_coloring f liveness = (*********** Determination of variables that need spill code insertion *****) let is_reg alloc v = - match alloc v with R _ -> true | S _ -> false + match alloc v with R _ -> true | Locations.S _ -> false let add_tospill alloc v ts = - match alloc v with R _ -> ts | S _ -> VSet.add v ts + match alloc v with R _ -> ts | Locations.S _ -> VSet.add v ts let addlist_tospill alloc vl ts = List.fold_right (add_tospill alloc) vl ts let addros_tospill alloc ros ts = - match ros with Coq_inl v -> add_tospill alloc v ts | Coq_inr s -> ts + match ros with Coq_inl v -> add_tospill alloc v ts | Coq_inr _ -> ts let tospill_instr alloc instr ts = match instr with @@ -707,43 +705,43 @@ let tospill_instr alloc instr ts = if is_reg alloc src || is_reg alloc dst || alloc src = alloc dst then ts else VSet.add src (VSet.add dst ts) - | Xreload(src, dst) -> + | Xreload(_, dst) -> if not (is_reg alloc dst) then begin printf "Error: %a was spilled\n" PrintXTL.var dst; assert false end; ts - | Xspill(src, dst) -> + | Xspill(src, _) -> if not (is_reg alloc src) then begin printf "Error: %a was spilled\n" PrintXTL.var src; assert false end; ts - | Xparmove(srcs, dsts, itmp, ftmp) -> + | Xparmove(_, _, itmp, ftmp) -> assert (is_reg alloc itmp && is_reg alloc ftmp); ts - | Xop(op, args, res) -> + | Xop(_, args, res) -> addlist_tospill alloc args (add_tospill alloc res ts) - | Xload(chunk, addr, args, dst) -> + | Xload(_, _, args, dst) -> addlist_tospill alloc args (add_tospill alloc dst ts) - | Xstore(chunk, addr, args, src) -> + | Xstore(_, _, args, src) -> addlist_tospill alloc args (add_tospill alloc src ts) - | Xcall(sg, vos, args, res) -> + | Xcall(_, vos, _, _) -> addros_tospill alloc vos ts - | Xtailcall(sg, vos, args) -> + | Xtailcall(_, vos, _) -> addros_tospill alloc vos ts | Xbuiltin((EF_annot _ | EF_debug _), _, _) -> ts - | Xbuiltin(ef, args, res) -> + | Xbuiltin(_, args, res) -> addlist_tospill alloc (params_of_builtin_args args) (addlist_tospill alloc (params_of_builtin_res res) ts) - | Xbranch s -> + | Xbranch _ -> ts - | Xcond(cond, args, s1, s2) -> + | Xcond(_, args, _, _) -> addlist_tospill alloc args ts - | Xjumptable(arg, tbl) -> + | Xjumptable(arg, _) -> add_tospill alloc arg ts - | Xreturn optarg -> + | Xreturn _ -> ts let rec tospill_block alloc blk ts = @@ -769,13 +767,13 @@ let tospill_function f alloc = let rec find_reg_containing v = function | [] -> None - | (var, temp, date) :: eqs -> + | (var, temp, _) :: eqs -> if var = v then Some temp else find_reg_containing v eqs let add v t eqs = (v, t, 0) :: eqs let kill x eqs = - List.filter (fun (v, t, date) -> v <> x && t <> x) eqs + List.filter (fun (v, t, _) -> v <> x && t <> x) eqs let reload_var tospill eqs v = if not (VSet.mem v tospill) then @@ -862,11 +860,11 @@ let spill_instr tospill eqs instr = end else begin ([instr], kill dst eqs) end - | Xreload(src, dst) -> + | Xreload _ -> assert false - | Xspill(src, dst) -> + | Xspill _ -> assert false - | Xparmove(srcs, dsts, itmp, ftmp) -> + | Xparmove(_, dsts, _, _) -> ([instr], List.fold_right kill dsts eqs) | Xop(op, args, res) -> begin match is_two_address op args with @@ -906,22 +904,22 @@ let spill_instr tospill eqs instr = let (src', c2, eqs2) = reload_var tospill eqs1 src in (c1 @ c2 @ [Xstore(chunk, addr, args', src')], eqs2) | Xcall(sg, Coq_inl v, args, res) -> - let (v', c1, eqs1) = reload_var tospill eqs v in + let (v', c1, _) = reload_var tospill eqs v in (c1 @ [Xcall(sg, Coq_inl v', args, res)], []) - | Xcall(sg, Coq_inr id, args, res) -> + | Xcall _ -> ([instr], []) | Xtailcall(sg, Coq_inl v, args) -> - let (v', c1, eqs1) = reload_var tospill eqs v in + let (v', c1, _) = reload_var tospill eqs v in (c1 @ [Xtailcall(sg, Coq_inl v', args)], []) - | Xtailcall(sg, Coq_inr id, args) -> + | Xtailcall _ -> ([instr], []) - | Xbuiltin((EF_annot _ | EF_debug _), args, res) -> + | Xbuiltin((EF_annot _ | EF_debug _), _, _) -> ([instr], eqs) | Xbuiltin(ef, args, res) -> let (args', c1, eqs1) = reload_args tospill eqs args in let (res', c2, eqs2) = save_res tospill eqs1 res in (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2) - | Xbranch s -> + | Xbranch _ -> ([instr], eqs) | Xcond(cond, args, s1, s2) -> let (args', c1, eqs1) = reload_vars tospill eqs args in @@ -929,7 +927,7 @@ let spill_instr tospill eqs instr = | Xjumptable(arg, tbl) -> let (arg', c1, eqs1) = reload_var tospill eqs arg in (c1 @ [Xjumptable(arg', tbl)], eqs1) - | Xreturn optarg -> + | Xreturn _ -> ([instr], []) let rec spill_block tospill pc blk eqs = @@ -963,7 +961,7 @@ let spill_function f tospill round = exception Bad_LTL -let mreg_of alloc v = match alloc v with R mr -> mr | S _ -> raise Bad_LTL +let mreg_of alloc v = match alloc v with R mr -> mr | Locations.S _ -> raise Bad_LTL let mregs_of alloc vl = List.map (mreg_of alloc) vl @@ -973,11 +971,11 @@ let make_move src dst k = match src, dst with | R rsrc, R rdst -> if rsrc = rdst then k else LTL.Lop(Omove, [rsrc], rdst) :: k - | R rsrc, S(sl, ofs, ty) -> + | R rsrc, Locations.S(sl, ofs, ty) -> LTL.Lsetstack(rsrc, sl, ofs, ty) :: k - | S(sl, ofs, ty), R rdst -> + | Locations.S(sl, ofs, ty), R rdst -> LTL.Lgetstack(sl, ofs, ty, rdst) :: k - | S _, S _ -> + | Locations.S _, Locations.S _ -> if src = dst then k else raise Bad_LTL type parmove_status = To_move | Being_moved | Moved @@ -997,11 +995,11 @@ let make_parmove srcs dsts itmp ftmp k = match s, d with | R rs, R rd -> code := LTL.Lop(Omove, [rs], rd) :: !code - | R rs, S(sl, ofs, ty) -> + | R rs, Locations.S(sl, ofs, ty) -> code := LTL.Lsetstack(rs, sl, ofs, ty) :: !code - | S(sl, ofs, ty), R rd -> + | Locations.S(sl, ofs, ty), R rd -> code := LTL.Lgetstack(sl, ofs, ty, rd) :: !code - | S(sls, ofss, tys), S(sld, ofsd, tyd) -> + | Locations.S(sls, ofss, tys), Locations.S(sld, ofsd, tyd) -> let tmp = temp_for tys in (* code will be reversed at the end *) code := LTL.Lsetstack(tmp, sld, ofsd, tyd) :: @@ -1054,9 +1052,9 @@ let transl_instr alloc instr k = LTL.Lload(chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k | Xstore(chunk, addr, args, src) -> LTL.Lstore(chunk, addr, mregs_of alloc args, mreg_of alloc src) :: k - | Xcall(sg, vos, args, res) -> + | Xcall(sg, vos, _, _) -> LTL.Lcall(sg, mros_of alloc vos) :: k - | Xtailcall(sg, vos, args) -> + | Xtailcall(sg, vos, _) -> LTL.Ltailcall(sg, mros_of alloc vos) :: [] | Xbuiltin(ef, args, res) -> LTL.Lbuiltin(ef, List.map (AST.map_builtin_arg alloc) args, @@ -1067,7 +1065,7 @@ let transl_instr alloc instr k = LTL.Lcond(cond, mregs_of alloc args, s1, s2) :: [] | Xjumptable(arg, tbl) -> LTL.Ljumptable(mreg_of alloc arg, tbl) :: [] - | Xreturn optarg -> + | Xreturn _ -> LTL.Lreturn :: [] let rec transl_block alloc blk = diff --git a/backend/Splitting.ml b/backend/Splitting.ml index 17b8098d..f09da104 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -13,10 +13,8 @@ (* Live range splitting over RTL *) open Camlcoq -open Datatypes open Coqlib open Maps -open AST open Kildall open Registers open RTL @@ -75,7 +73,7 @@ module LRMap = struct let bot : t = RMap.empty - let lub_opt_range r olr1 olr2 = + let lub_opt_range _ olr1 olr2 = match olr1, olr2 with | Some lr1, Some lr2 -> unify lr1 lr2; olr1 | Some _, None -> olr1 diff --git a/backend/XTL.ml b/backend/XTL.ml index 2ddbc50a..7ff26171 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -99,11 +99,11 @@ let twin_reg r = let rec successors_block = function | Xbranch s :: _ -> [s] - | Xtailcall(sg, vos, args) :: _ -> [] - | Xcond(cond, args, s1, s2) :: _ -> [s1; s2] - | Xjumptable(arg, tbl) :: _ -> tbl + | Xtailcall(_,_,_) :: _ -> [] + | Xcond(_,_, s1, s2) :: _ -> [s1; s2] + | Xjumptable(_, tbl) :: _ -> tbl | Xreturn _:: _ -> [] - | instr :: blk -> successors_block blk + | _ :: blk -> successors_block blk | [] -> assert false (**** Type checking for XTL *) @@ -159,25 +159,25 @@ let type_instr = function | Xstore(chunk, addr, args, src) -> set_vars_type args (type_of_addressing addr); set_var_type src (type_of_chunk chunk) - | Xcall(sg, Coq_inl v, args, res) -> + | Xcall(_, Coq_inl v, _, _) -> set_var_type v Tint - | Xcall(sg, Coq_inr id, args, res) -> + | Xcall(_, Coq_inr _, _, _) -> () - | Xtailcall(sg, Coq_inl v, args) -> + | Xtailcall(_, Coq_inl v, _) -> set_var_type v Tint - | Xtailcall(sg, Coq_inr id, args) -> + | Xtailcall(_, Coq_inr _,_) -> () | Xbuiltin(ef, args, res) -> let sg = ef_sig ef in type_builtin_args args sg.sig_args; type_builtin_res res (proj_sig_res sg) - | Xbranch s -> + | Xbranch _ -> () - | Xcond(cond, args, s1, s2) -> + | Xcond(cond, args, _, _) -> set_vars_type args (type_of_condition cond) - | Xjumptable(arg, tbl) -> + | Xjumptable(arg, _) -> set_var_type arg Tint - | Xreturn args -> + | Xreturn _ -> () let type_block blk = -- cgit From 2185164c1845c30ebd4118ed5bc8d339b16663a9 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 15 Mar 2016 12:55:31 +0100 Subject: Added back invariant checks for IRC. Since the invariant checks are not currently used and they are not exported they are renamed to include a _ to avoid warning. Bug 18394 --- backend/IRC.ml | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) (limited to 'backend') diff --git a/backend/IRC.ml b/backend/IRC.ml index 8780bce3..76f194d2 100644 --- a/backend/IRC.ml +++ b/backend/IRC.ml @@ -451,6 +451,42 @@ let initialNodePartition g = | _ -> assert false in Hashtbl.iter (fun _ a -> part_node a) g.varTable +(* Check invariants *) + +let _degreeInvariant _ n = + let c = ref 0 in + iterAdjacent (fun _ -> incr c) n; + if !c <> n.degree then + failwith("degree invariant violated by " ^ name_of_node n) + +let _simplifyWorklistInvariant g n = + if n.degree < g.num_available_registers.(n.regclass) + && not (moveRelated n) + then () + else failwith("simplify worklist invariant violated by " ^ name_of_node n) + +let _freezeWorklistInvariant g n = + if n.degree < g.num_available_registers.(n.regclass) + && moveRelated n + then () + else failwith("freeze worklist invariant violated by " ^ name_of_node n) + +let _spillWorklistInvariant g n = + if n.degree >= g.num_available_registers.(n.regclass) + then () + else failwith("spill worklist invariant violated by " ^ name_of_node n) + +let _checkInvariants g = + DLinkNode.iter + (fun n -> _degreeInvariant g n; _simplifyWorklistInvariant g n) + g.simplifyWorklist; + DLinkNode.iter + (fun n -> _degreeInvariant g n; _freezeWorklistInvariant g n) + g.freezeWorklist; + DLinkNode.iter + (fun n -> _degreeInvariant g n; _spillWorklistInvariant g n) + g.spillWorklist + (* Enable moves that have become low-degree related *) let enableMoves g n = -- cgit From 272a5b812b72f4c3e409ccdbeaf3476d95c4b552 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 15 Mar 2016 15:07:47 +0100 Subject: Deactivate warning 27 and added back removed code. The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349 --- backend/CMparser.mly | 10 ++-- backend/CMtypecheck.ml | 12 ++-- backend/Fileinfo.ml | 4 +- backend/IRC.ml | 8 +-- backend/Inliningaux.ml | 2 +- backend/Linearizeaux.ml | 10 ++-- backend/PrintAsm.ml | 2 +- backend/PrintLTL.ml | 4 +- backend/PrintMach.ml | 4 +- backend/PrintRTL.ml | 4 +- backend/PrintXTL.ml | 8 +-- backend/RTLgenaux.ml | 40 +++++++------- backend/Regalloc.ml | 144 ++++++++++++++++++++++++------------------------ backend/Splitting.ml | 2 +- backend/XTL.ml | 24 ++++---- 15 files changed, 139 insertions(+), 139 deletions(-) (limited to 'backend') diff --git a/backend/CMparser.mly b/backend/CMparser.mly index b20dea38..5109749d 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -210,17 +210,17 @@ let mkmatch_aux expr cases = let ncases = List.length cases in let rec mktable n = function | [] -> assert false - | [_, _] -> [] - | (key, _) :: rem -> + | [key, action] -> [] + | (key, action) :: rem -> (coqint_of_camlint key, Nat.of_int n) :: mktable (n + 1) rem in let sw = Sswitch(false, expr, mktable 0 cases, Nat.of_int (ncases - 1)) in let rec mkblocks body n = function | [] -> assert false - | [_, action] -> + | [key, action] -> Sblock(Sseq(body, action)) - | (_, action) :: rem -> + | (key, action) :: rem -> mkblocks (Sblock(Sseq(body, Sseq(action, Sexit (Nat.of_int n))))) (n - 1) @@ -233,7 +233,7 @@ let mkmatch expr cases = let s = match cases with | [] -> Sskip (* ??? *) - | [_, action] -> action + | [key, action] -> action | _ -> mkmatch_aux c cases in prepend_seq !convert_accu s diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 399eb9bd..cd0d25dc 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -296,12 +296,12 @@ let rec type_stmt env blk ret s = | Sexit n -> if Nat.to_int n >= blk then raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n))) - | Sswitch(islong, e, _, _) -> + | Sswitch(islong, e, cases, deflt) -> unify (type_expr env [] e) (if islong then tlong else tint) | Sreturn None -> begin match ret with | None -> () - | Some _ -> raise (Error ("return without argument")) + | Some tret -> raise (Error ("return without argument")) end | Sreturn (Some e) -> begin match ret with @@ -322,9 +322,9 @@ let rec type_stmt env blk ret s = with Error s -> raise (Error (sprintf "In tail call:\n%s" s)) end - | Slabel(_, s1) -> + | Slabel(lbl, s1) -> type_stmt env blk ret s1 - | Sgoto _ -> + | Sgoto lbl -> () let rec env_of_vars idl = @@ -343,8 +343,8 @@ let type_function id f = let type_globdef (id, gd) = match gd with | Gfun(Internal f) -> type_function id f - | Gfun(External _) -> () - | Gvar _ -> () + | Gfun(External ef) -> () + | Gvar v -> () let type_program p = List.iter type_globdef p.prog_defs; p diff --git a/backend/Fileinfo.ml b/backend/Fileinfo.ml index a78a24db..0490def0 100644 --- a/backend/Fileinfo.ml +++ b/backend/Fileinfo.ml @@ -25,7 +25,7 @@ let reset_filenames () = let close_filenames () = Hashtbl.iter - (fun _ (_, fb) -> + (fun file (num, fb) -> match fb with Some b -> Printlines.close b | None -> ()) filename_info; reset_filenames() @@ -46,7 +46,7 @@ let print_file oc file = try Hashtbl.find filename_info file with Not_found -> - let (filenum, _ as res) = enter_filename file in + let (filenum, filebuf as res) = enter_filename file in fprintf oc " .file %d %S\n" filenum file; res diff --git a/backend/IRC.ml b/backend/IRC.ml index 76f194d2..d542f85e 100644 --- a/backend/IRC.ml +++ b/backend/IRC.ml @@ -114,7 +114,7 @@ let name_of_loc = function let name_of_node n = match n.var with - | V(r, _) -> sprintf "x%ld" (P.to_int32 r) + | V(r, ty) -> sprintf "x%ld" (P.to_int32 r) | L l -> name_of_loc l (* The algorithm manipulates partitions of the nodes and of the moves @@ -455,7 +455,7 @@ let initialNodePartition g = let _degreeInvariant _ n = let c = ref 0 in - iterAdjacent (fun _ -> incr c) n; + iterAdjacent (fun n -> incr c) n; if !c <> n.degree then failwith("degree invariant violated by " ^ name_of_node n) @@ -726,7 +726,7 @@ let selectSpill g = (* Find a spillable node of minimal cost *) let (n, cost) = DLinkNode.fold - (fun n (_, best_cost as best) -> + (fun n (best_node, best_cost as best) -> (* Manual inlining of [spillCost] above plus algebraic simplif *) let deg = float n.degree in let deg2 = deg *. deg in @@ -883,7 +883,7 @@ let assign_color g n = let location_of_var g v = match v with | L l -> l - | V(_, ty) -> + | V(r, ty) -> try let n = Hashtbl.find g.varTable v in let n' = getAlias n in diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 7893da89..265831a5 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -12,5 +12,5 @@ (* To be considered: heuristics based on size of function? *) -let should_inline (id: AST.ident) (_: RTL.coq_function) = +let should_inline (id: AST.ident) (f: RTL.coq_function) = C2C.atom_is_inline id diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 41a98873..46d5c3f1 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -79,13 +79,13 @@ let basic_blocks f joins = let rec do_instr_list = function | [] -> assert false | Lbranch s :: _ -> next_in_block blk minpc s - | Ltailcall _ :: _ -> end_block blk minpc - | Lcond (_, _, ifso, ifnot) :: _ -> + | Ltailcall (sig0, ros) :: _ -> end_block blk minpc + | Lcond (cond, args, ifso, ifnot) :: _ -> end_block blk minpc; start_block ifso; start_block ifnot - | Ljumptable(_, tbl) :: _ -> + | Ljumptable(arg, tbl) :: _ -> end_block blk minpc; List.iter start_block tbl | Lreturn :: _ -> end_block blk minpc - | _ :: b' -> do_instr_list b' in + | instr :: b' -> do_instr_list b' in do_instr_list b (* next_in_block: check if join point and either extend block or start block *) @@ -110,5 +110,5 @@ let flatten_blocks blks = (* Build the enumeration *) -let enumerate_aux f _ = +let enumerate_aux f reach = flatten_blocks (basic_blocks f (join_points f)) diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 6eff7c02..96aa080e 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -104,7 +104,7 @@ module Printer(Target:TARGET) = let print_globdef oc (name,gdef) = match gdef with | Gfun (Internal code) -> print_function oc name code - | Gfun (External _) -> () + | Gfun (External ef) -> () | Gvar v -> print_var oc name v module DwarfTarget: DwarfTypes.DWARF_TARGET = diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index ba28b30d..a0a08218 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -72,9 +72,9 @@ let print_instruction pp succ = function | Lstore(chunk, addr, args, src) -> fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing mreg) (addr, args) mreg src - | Lcall(_, fn) -> + | Lcall(sg, fn) -> fprintf pp "call %a" ros fn - | Ltailcall(_, fn) -> + | Ltailcall(sg, fn) -> fprintf pp "tailcall %a" ros fn | Lbuiltin(ef, args, res) -> fprintf pp "%a = %s(%a)" diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index 07ec6a1a..517f3037 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -57,9 +57,9 @@ let print_instruction pp i = (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src - | Mcall(_, fn) -> + | Mcall(sg, fn) -> fprintf pp "\tcall %a\n" ros fn - | Mtailcall(_, fn) -> + | Mtailcall(sg, fn) -> fprintf pp "\ttailcall %a\n" ros fn | Mbuiltin(ef, args, res) -> fprintf pp "\t%a = %s(%a)\n" diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index a22aa422..ba336b0a 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -61,11 +61,11 @@ let print_instruction pp (pc, i) = (PrintOp.print_addressing reg) (addr, args) reg src; print_succ pp s (pc - 1) - | Icall(_, fn, args, res, s) -> + | Icall(sg, fn, args, res, s) -> fprintf pp "%a = %a(%a)\n" reg res ros fn regs args; print_succ pp s (pc - 1) - | Itailcall(_, fn, args) -> + | Itailcall(sg, fn, args) -> fprintf pp "tailcall %a(%a)\n" ros fn regs args | Ibuiltin(ef, args, res, s) -> diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index 1bee1e15..31273f97 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -67,8 +67,8 @@ let ros pp = function let liveset pp lv = fprintf pp "{"; - VSet.iter (function V(r, _) -> fprintf pp " x%d" (P.to_int r) - | L _ -> ()) + VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r) + | L l -> ()) lv; fprintf pp " }" @@ -93,9 +93,9 @@ let print_instruction pp succ = function | Xstore(chunk, addr, args, src) -> fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing var) (addr, args) var src - | Xcall(_, fn, args, res) -> + | Xcall(sg, fn, args, res) -> fprintf pp "%a = call %a(%a)" vars res ros fn vars args - | Xtailcall(_, fn, args) -> + | Xtailcall(sg, fn, args) -> fprintf pp "tailcall %a(%a)" ros fn vars args | Xbuiltin(ef, args, res) -> fprintf pp "%a = %s(%a)" diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index fdf41897..e39d3b56 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -26,22 +26,22 @@ open CminorSel putting the bigger of the two branches in fall-through position. *) let rec size_expr = function - | Evar _ -> 0 - | Eop(_, args) -> 1 + size_exprs args - | Eload(_, _, args) -> 1 + size_exprs args + | Evar id -> 0 + | Eop(op, args) -> 1 + size_exprs args + | Eload(chunk, addr, args) -> 1 + size_exprs args | Econdition(ce, e1, e2) -> 1 + size_condexpr ce + max (size_expr e1) (size_expr e2) | Elet(e1, e2) -> size_expr e1 + size_expr e2 - | Eletvar _ -> 0 - | Ebuiltin(_, el) -> 2 + size_exprs el - | Eexternal(_, _, el) -> 5 + size_exprs el + | Eletvar n -> 0 + | Ebuiltin(ef, el) -> 2 + size_exprs el + | Eexternal(id, sg, el) -> 5 + size_exprs el and size_exprs = function | Enil -> 0 | Econs(e1, el) -> size_expr e1 + size_exprs el and size_condexpr = function - | CEcond(_, args) -> size_exprs args + | CEcond(c, args) -> size_exprs args | CEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3 | CElet(a, c) -> @@ -52,8 +52,8 @@ let size_exprlist al = List.fold_right (fun a s -> size_expr a + s) al 0 let size_builtin_args al = size_exprlist (params_of_builtin_args al) let rec size_exitexpr = function - | XEexit _ -> 0 - | XEjumptable(arg, _) -> 2 + size_expr arg + | XEexit n -> 0 + | XEjumptable(arg, tbl) -> 2 + size_expr arg | XEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_exitexpr c2 + size_exitexpr c3 | XElet(a, c) -> @@ -61,34 +61,34 @@ let rec size_exitexpr = function let rec length_exprs = function | Enil -> 0 - | Econs(_, el) -> 1 + length_exprs el + | Econs(e1, el) -> 1 + length_exprs el let size_eos = function | Coq_inl e -> size_expr e - | Coq_inr _ -> 0 + | Coq_inr id -> 0 let rec size_stmt = function | Sskip -> 0 - | Sassign(_, a) -> size_expr a - | Sstore(_, _, args, src) -> 1 + size_exprs args + size_expr src - | Scall(_, _, eos, args) -> + | Sassign(id, a) -> size_expr a + | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src + | Scall(optid, sg, eos, args) -> 3 + size_eos eos + size_exprs args + length_exprs args - | Stailcall(_, eos, args) -> + | Stailcall(sg, eos, args) -> 3 + size_eos eos + size_exprs args + length_exprs args | Sbuiltin(_, (EF_annot _ | EF_debug _), _) -> 0 - | Sbuiltin(_, _, args) -> 1 + size_builtin_args args + | Sbuiltin(optid, ef, args) -> 1 + size_builtin_args args | Sseq(s1, s2) -> size_stmt s1 + size_stmt s2 | Sifthenelse(ce, s1, s2) -> size_condexpr ce + max (size_stmt s1) (size_stmt s2) | Sloop s -> 1 + 4 * size_stmt s | Sblock s -> size_stmt s - | Sexit _ -> 1 + | Sexit n -> 1 | Sswitch xe -> size_exitexpr xe | Sreturn None -> 2 | Sreturn (Some arg) -> 2 + size_expr arg - | Slabel(_, s) -> size_stmt s - | Sgoto _ -> 1 + | Slabel(lbl, s) -> size_stmt s + | Sgoto lbl -> 1 -let more_likely (_: condexpr) (ifso: stmt) (ifnot: stmt) = +let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = size_stmt ifso > size_stmt ifnot diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index ee35d7a0..e531a34a 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -85,8 +85,8 @@ let constrain_reg v c = let rec constrain_regs vl cl = match vl, cl with | [], _ -> [] - | _ :: _, [] -> vl - | _ :: vl', Some mr1 :: cl' -> L(R mr1) :: constrain_regs vl' cl' + | v1 :: vl', [] -> vl + | v1 :: vl', Some mr1 :: cl' -> L(R mr1) :: constrain_regs vl' cl' | v1 :: vl', None :: cl' -> v1 :: constrain_regs vl' cl' let move v1 v2 k = @@ -140,8 +140,8 @@ let convert_builtin_res tyenv = function let rec constrain_builtin_arg a cl = match a, cl with - | BA _, None :: cl' -> (a, cl') - | BA _, Some mr :: cl' -> (BA (L(R mr)), cl') + | BA x, None :: cl' -> (a, cl') + | BA x, Some mr :: cl' -> (BA (L(R mr)), cl') | BA_splitlong(hi, lo), _ -> let (hi', cl1) = constrain_builtin_arg hi cl in let (lo', cl2) = constrain_builtin_arg lo cl1 in @@ -158,8 +158,8 @@ let rec constrain_builtin_args al cl = let rec constrain_builtin_res a cl = match a, cl with - | BR _, None :: cl' -> (a, cl') - | BR _, Some mr :: cl' -> (BR (L(R mr)), cl') + | BR x, None :: cl' -> (a, cl') + | BR x, Some mr :: cl' -> (BR (L(R mr)), cl') | BR_splitlong(hi, lo), _ -> let (hi', cl1) = constrain_builtin_res hi cl in let (lo', cl2) = constrain_builtin_res lo cl1 in @@ -262,7 +262,7 @@ let block_of_RTL_instr funsig tyenv = function let next_pc f = PTree.fold - (fun npc pc _ -> if P.lt pc npc then npc else P.succ pc) + (fun npc pc i -> if P.lt pc npc then npc else P.succ pc) f.RTL.fn_code P.one (* Translate an RTL function to an XTL function *) @@ -287,7 +287,7 @@ let vset_removelist vl after = List.fold_right VSet.remove vl after let vset_addlist vl after = List.fold_right VSet.add vl after let vset_addros vos after = - match vos with Coq_inl v -> VSet.add v after | Coq_inr _ -> after + match vos with Coq_inl v -> VSet.add v after | Coq_inr id -> after let rec vset_addarg a after = match a with @@ -309,31 +309,31 @@ let live_before instr after = if VSet.mem dst after || XTL.is_stack_reg src then VSet.add src (VSet.remove dst after) else after - | Xparmove(srcs, dsts, _, _) -> + | Xparmove(srcs, dsts, itmp, ftmp) -> vset_addlist srcs (vset_removelist dsts after) - | Xop(_, args, res) -> + | Xop(op, args, res) -> if VSet.mem res after then vset_addlist args (VSet.remove res after) else after - | Xload(_, _, args, dst) -> + | Xload(chunk, addr, args, dst) -> if VSet.mem dst after then vset_addlist args (VSet.remove dst after) else after - | Xstore(_, _, args, src) -> + | Xstore(chunk, addr, args, src) -> vset_addlist args (VSet.add src after) - | Xcall(_, ros, args, res) -> + | Xcall(sg, ros, args, res) -> vset_addlist args (vset_addros ros (vset_removelist res after)) - | Xtailcall(_, ros, args) -> + | Xtailcall(sg, ros, args) -> vset_addlist args (vset_addros ros VSet.empty) - | Xbuiltin(EF_debug _, _, res) -> + | Xbuiltin(EF_debug _, args, res) -> vset_removeres res after - | Xbuiltin(_, args, res) -> + | Xbuiltin(ef, args, res) -> vset_addargs args (vset_removeres res after) - | Xbranch _ -> + | Xbranch s -> after - | Xcond(_, args, _, _) -> + | Xcond(cond, args, s1, s2) -> List.fold_right VSet.add args after - | Xjumptable(arg, _) -> + | Xjumptable(arg, tbl) -> VSet.add arg after | Xreturn args -> vset_addlist args VSet.empty @@ -406,11 +406,11 @@ let dce_instr instr after k = | ([src], [dst]) -> Xmove(src, dst) :: k | (srcs', dsts') -> Xparmove(srcs', dsts', itmp, ftmp) :: k end - | Xop(_, _, res) -> + | Xop(op, args, res) -> if VSet.mem res after then instr :: k else k - | Xload(_, _, _, dst) -> + | Xload(chunk, addr, args, dst) -> if VSet.mem dst after then instr :: k else k @@ -452,8 +452,8 @@ let spill_costs f = let charge amount uses v = match v with - | L _ -> () - | V(r, _) -> + | L l -> () + | V(r, ty) -> let st = get_stats r in if st.cost < 0 then (* the variable must be spilled, don't change its cost *) @@ -470,12 +470,12 @@ let spill_costs f = List.iter (charge amount uses) vl in let charge_ros amount ros = - match ros with Coq_inl v -> charge amount 1 v | Coq_inr _ -> () in + match ros with Coq_inl v -> charge amount 1 v | Coq_inr id -> () in let force_stack_allocation v = match v with - | L _ -> () - | V(r,_) -> + | L l -> () + | V(r, ty) -> let st = get_stats r in assert (st.cost < max_int); st.cost <- (-1) in @@ -499,15 +499,15 @@ let spill_costs f = charge_list 1 1 srcs; charge_list 1 1 dsts; charge max_int 0 itmp; charge max_int 0 ftmp (* temps must not be spilled *) - | Xop(_, args, res) -> + | Xop(op, args, res) -> charge_list 10 1 args; charge 10 1 res - | Xload(_, _, args, dst) -> + | Xload(chunk, addr, args, dst) -> charge_list 10 1 args; charge 10 1 dst - | Xstore(_, _, args, src) -> + | Xstore(chunk, addr, args, src) -> charge_list 10 1 args; charge 10 1 src - | Xcall(_, vos, _, _) -> + | Xcall(sg, vos, args, res) -> charge_ros 10 vos - | Xtailcall(_, vos, _) -> + | Xtailcall(sg, vos, args) -> charge_ros 10 vos | Xbuiltin(ef, args, res) -> begin match ef with @@ -526,11 +526,11 @@ let spill_costs f = charge_list 10 1 (params_of_builtin_res res) end | Xbranch _ -> () - | Xcond(_, args, _, _) -> + | Xcond(cond, args, _, _) -> charge_list 10 1 args | Xjumptable(arg, _) -> charge 10 1 arg - | Xreturn _ -> + | Xreturn optarg -> () in let charge_block blk = List.iter charge_instr blk in @@ -620,17 +620,17 @@ let add_interfs_instr g instr live = (vset_addlist (res :: argl) (VSet.remove res live)) end; add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op) - | Xload(chunk, addr, _, dst) -> + | Xload(chunk, addr, args, dst) -> add_interfs_def g dst live; add_interfs_destroyed g (VSet.remove dst live) (destroyed_by_load chunk addr) - | Xstore(chunk, addr, _,_) -> + | Xstore(chunk, addr, args, src) -> add_interfs_destroyed g live (destroyed_by_store chunk addr) - | Xcall(_, _,_, res) -> + | Xcall(sg, vos, args, res) -> add_interfs_destroyed g (vset_removelist res live) destroyed_at_call - | Xtailcall(_, Coq_inl v, _) -> + | Xtailcall(sg, Coq_inl v, args) -> List.iter (fun r -> IRC.add_interf g (vmreg r) v) int_callee_save_regs - | Xtailcall(_, Coq_inr _, _) -> + | Xtailcall(sg, Coq_inr id, args) -> () | Xbuiltin(ef, args, res) -> (* Interferences with live across *) @@ -644,7 +644,7 @@ let add_interfs_instr g instr live = | EF_annot_val _, [BA arg], BR res -> (* like a move *) IRC.add_pref g arg res - | EF_inline_asm(_, _, clob), _, _ -> + | EF_inline_asm(txt, sg, clob), _, _ -> let vargs = params_of_builtin_args args in (* clobbered regs interfere with res and args for GCC compatibility *) List.iter (fun c -> @@ -656,13 +656,13 @@ let add_interfs_instr g instr live = clob | _ -> () end - | Xbranch _ -> + | Xbranch s -> () - | Xcond(cond, _, _,_) -> + | Xcond(cond, args, s1, s2) -> add_interfs_destroyed g live (destroyed_by_cond cond) - | Xjumptable _ -> + | Xjumptable(arg, tbl) -> add_interfs_destroyed g live destroyed_by_jumptable - | Xreturn _ -> + | Xreturn optarg -> () let rec add_interfs_block g blk live = @@ -697,7 +697,7 @@ let addlist_tospill alloc vl ts = List.fold_right (add_tospill alloc) vl ts let addros_tospill alloc ros ts = - match ros with Coq_inl v -> add_tospill alloc v ts | Coq_inr _ -> ts + match ros with Coq_inl v -> add_tospill alloc v ts | Coq_inr s -> ts let tospill_instr alloc instr ts = match instr with @@ -705,43 +705,43 @@ let tospill_instr alloc instr ts = if is_reg alloc src || is_reg alloc dst || alloc src = alloc dst then ts else VSet.add src (VSet.add dst ts) - | Xreload(_, dst) -> + | Xreload(src, dst) -> if not (is_reg alloc dst) then begin printf "Error: %a was spilled\n" PrintXTL.var dst; assert false end; ts - | Xspill(src, _) -> + | Xspill(src, dst) -> if not (is_reg alloc src) then begin printf "Error: %a was spilled\n" PrintXTL.var src; assert false end; ts - | Xparmove(_, _, itmp, ftmp) -> + | Xparmove(srcs, dsts, itmp, ftmp) -> assert (is_reg alloc itmp && is_reg alloc ftmp); ts - | Xop(_, args, res) -> + | Xop(op, args, res) -> addlist_tospill alloc args (add_tospill alloc res ts) - | Xload(_, _, args, dst) -> + | Xload(chunk, addr, args, dst) -> addlist_tospill alloc args (add_tospill alloc dst ts) - | Xstore(_, _, args, src) -> + | Xstore(chunk, addr, args, src) -> addlist_tospill alloc args (add_tospill alloc src ts) - | Xcall(_, vos, _, _) -> + | Xcall(sg, vos, args, res) -> addros_tospill alloc vos ts - | Xtailcall(_, vos, _) -> + | Xtailcall(sg, vos, args) -> addros_tospill alloc vos ts | Xbuiltin((EF_annot _ | EF_debug _), _, _) -> ts - | Xbuiltin(_, args, res) -> + | Xbuiltin(ef, args, res) -> addlist_tospill alloc (params_of_builtin_args args) (addlist_tospill alloc (params_of_builtin_res res) ts) - | Xbranch _ -> + | Xbranch s -> ts - | Xcond(_, args, _, _) -> + | Xcond(cond, args, s1, s2) -> addlist_tospill alloc args ts - | Xjumptable(arg, _) -> + | Xjumptable(arg, tbl) -> add_tospill alloc arg ts - | Xreturn _ -> + | Xreturn optarg -> ts let rec tospill_block alloc blk ts = @@ -767,13 +767,13 @@ let tospill_function f alloc = let rec find_reg_containing v = function | [] -> None - | (var, temp, _) :: eqs -> + | (var, temp, date) :: eqs -> if var = v then Some temp else find_reg_containing v eqs let add v t eqs = (v, t, 0) :: eqs let kill x eqs = - List.filter (fun (v, t, _) -> v <> x && t <> x) eqs + List.filter (fun (v, t, date) -> v <> x && t <> x) eqs let reload_var tospill eqs v = if not (VSet.mem v tospill) then @@ -860,11 +860,11 @@ let spill_instr tospill eqs instr = end else begin ([instr], kill dst eqs) end - | Xreload _ -> + | Xreload(src, dst) -> assert false - | Xspill _ -> + | Xspill(src, dst) -> assert false - | Xparmove(_, dsts, _, _) -> + | Xparmove(srcs, dsts, itmp, ftmp) -> ([instr], List.fold_right kill dsts eqs) | Xop(op, args, res) -> begin match is_two_address op args with @@ -904,22 +904,22 @@ let spill_instr tospill eqs instr = let (src', c2, eqs2) = reload_var tospill eqs1 src in (c1 @ c2 @ [Xstore(chunk, addr, args', src')], eqs2) | Xcall(sg, Coq_inl v, args, res) -> - let (v', c1, _) = reload_var tospill eqs v in + let (v', c1, eqs1) = reload_var tospill eqs v in (c1 @ [Xcall(sg, Coq_inl v', args, res)], []) - | Xcall _ -> + | Xcall(sg, Coq_inr id, args, res) -> ([instr], []) | Xtailcall(sg, Coq_inl v, args) -> - let (v', c1, _) = reload_var tospill eqs v in + let (v', c1, eqs1) = reload_var tospill eqs v in (c1 @ [Xtailcall(sg, Coq_inl v', args)], []) - | Xtailcall _ -> + | Xtailcall(sg, Coq_inr id, args) -> ([instr], []) - | Xbuiltin((EF_annot _ | EF_debug _), _, _) -> + | Xbuiltin((EF_annot _ | EF_debug _), args, res) -> ([instr], eqs) | Xbuiltin(ef, args, res) -> let (args', c1, eqs1) = reload_args tospill eqs args in let (res', c2, eqs2) = save_res tospill eqs1 res in (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2) - | Xbranch _ -> + | Xbranch s -> ([instr], eqs) | Xcond(cond, args, s1, s2) -> let (args', c1, eqs1) = reload_vars tospill eqs args in @@ -927,7 +927,7 @@ let spill_instr tospill eqs instr = | Xjumptable(arg, tbl) -> let (arg', c1, eqs1) = reload_var tospill eqs arg in (c1 @ [Xjumptable(arg', tbl)], eqs1) - | Xreturn _ -> + | Xreturn optarg -> ([instr], []) let rec spill_block tospill pc blk eqs = @@ -1052,9 +1052,9 @@ let transl_instr alloc instr k = LTL.Lload(chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k | Xstore(chunk, addr, args, src) -> LTL.Lstore(chunk, addr, mregs_of alloc args, mreg_of alloc src) :: k - | Xcall(sg, vos, _, _) -> + | Xcall(sg, vos, args, res) -> LTL.Lcall(sg, mros_of alloc vos) :: k - | Xtailcall(sg, vos, _) -> + | Xtailcall(sg, vos, args) -> LTL.Ltailcall(sg, mros_of alloc vos) :: [] | Xbuiltin(ef, args, res) -> LTL.Lbuiltin(ef, List.map (AST.map_builtin_arg alloc) args, @@ -1065,7 +1065,7 @@ let transl_instr alloc instr k = LTL.Lcond(cond, mregs_of alloc args, s1, s2) :: [] | Xjumptable(arg, tbl) -> LTL.Ljumptable(mreg_of alloc arg, tbl) :: [] - | Xreturn _ -> + | Xreturn optarg -> LTL.Lreturn :: [] let rec transl_block alloc blk = diff --git a/backend/Splitting.ml b/backend/Splitting.ml index f09da104..40f09c3d 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -73,7 +73,7 @@ module LRMap = struct let bot : t = RMap.empty - let lub_opt_range _ olr1 olr2 = + let lub_opt_range r olr1 olr2 = match olr1, olr2 with | Some lr1, Some lr2 -> unify lr1 lr2; olr1 | Some _, None -> olr1 diff --git a/backend/XTL.ml b/backend/XTL.ml index 7ff26171..2ddbc50a 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -99,11 +99,11 @@ let twin_reg r = let rec successors_block = function | Xbranch s :: _ -> [s] - | Xtailcall(_,_,_) :: _ -> [] - | Xcond(_,_, s1, s2) :: _ -> [s1; s2] - | Xjumptable(_, tbl) :: _ -> tbl + | Xtailcall(sg, vos, args) :: _ -> [] + | Xcond(cond, args, s1, s2) :: _ -> [s1; s2] + | Xjumptable(arg, tbl) :: _ -> tbl | Xreturn _:: _ -> [] - | _ :: blk -> successors_block blk + | instr :: blk -> successors_block blk | [] -> assert false (**** Type checking for XTL *) @@ -159,25 +159,25 @@ let type_instr = function | Xstore(chunk, addr, args, src) -> set_vars_type args (type_of_addressing addr); set_var_type src (type_of_chunk chunk) - | Xcall(_, Coq_inl v, _, _) -> + | Xcall(sg, Coq_inl v, args, res) -> set_var_type v Tint - | Xcall(_, Coq_inr _, _, _) -> + | Xcall(sg, Coq_inr id, args, res) -> () - | Xtailcall(_, Coq_inl v, _) -> + | Xtailcall(sg, Coq_inl v, args) -> set_var_type v Tint - | Xtailcall(_, Coq_inr _,_) -> + | Xtailcall(sg, Coq_inr id, args) -> () | Xbuiltin(ef, args, res) -> let sg = ef_sig ef in type_builtin_args args sg.sig_args; type_builtin_res res (proj_sig_res sg) - | Xbranch _ -> + | Xbranch s -> () - | Xcond(cond, args, _, _) -> + | Xcond(cond, args, s1, s2) -> set_vars_type args (type_of_condition cond) - | Xjumptable(arg, _) -> + | Xjumptable(arg, tbl) -> set_var_type arg Tint - | Xreturn _ -> + | Xreturn args -> () let type_block blk = -- cgit From 1e08d4adb241e076a96f9525fdb8359cf8845527 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 16 Mar 2016 13:51:33 +0100 Subject: Added interface for the Asmexpansion. Hide the reference used internally behind the interface and added some functions to access the needed values. Bug 18394 --- backend/Asmexpandaux.ml | 9 +++++++++ backend/Asmexpandaux.mli | 36 ++++++++++++++++++++++++++++++++++++ 2 files changed, 45 insertions(+) create mode 100644 backend/Asmexpandaux.mli (limited to 'backend') diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index 3d1dd754..13aa71d2 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -50,6 +50,15 @@ let new_label () = let set_current_function f = current_function := f; next_label := None; current_code := [] +let get_current_function_args () = + (!current_function).fn_sig.sig_args + +let is_current_function_variadic () = + (!current_function).fn_sig.sig_cc.cc_vararg + +let get_current_function_sig () = + (!current_function).fn_sig + let get_current_function () = let c = List.rev !current_code in let fn = !current_function in diff --git a/backend/Asmexpandaux.mli b/backend/Asmexpandaux.mli new file mode 100644 index 00000000..797eb10c --- /dev/null +++ b/backend/Asmexpandaux.mli @@ -0,0 +1,36 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open Asm +open AST +open BinNums + +(** Auxiliary functions for builtin expansion *) + +val emit: instruction -> unit + (* Emit an instruction *) +val new_label: unit -> label + (* Compute a fresh label *) +val is_current_function_variadic: unit -> bool + (* Test wether the current function is a variadic function *) +val get_current_function_args: unit -> typ list + (* Get the types of the current function arguments *) +val get_current_function_sig: unit -> signature + (* Get the signature of the current function *) +val set_current_function: coq_function -> unit + (* Set the current function *) +val get_current_function: unit -> coq_function + (* Get the current function *) +val expand_debug: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit + (* Expand builtin debug function. Takes the function id, the register number of the stackpointer, a + function to get the dwarf mapping of varibale names and for the expansion of simple instructions *) -- cgit