diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CMparser.mly | 2 | ||||
| -rw-r--r-- | backend/PrintAsm.ml | 1 | ||||
| -rw-r--r-- | backend/PrintLTL.ml | 11 | ||||
| -rw-r--r-- | backend/PrintXTL.ml | 11 | ||||
| -rw-r--r-- | backend/Regalloc.ml | 19 |
5 files changed, 20 insertions, 24 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 94b50810..64943f0b 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 diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 9292745d..1f100b7e 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -13,7 +13,6 @@ open AST open Camlcoq -open !Datatypes open DwarfPrinter open PrintAsmaux open Printf diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index a0a08218..d0557073 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -17,7 +17,6 @@ open Camlcoq open Datatypes open Maps open AST -open !Locations open LTL open PrintAST open PrintOp @@ -34,17 +33,17 @@ let rec mregs pp = function let slot pp (sl, ofs, ty) = match sl with - | Local -> + | Locations.Local -> fprintf pp "local(%ld,%s)" (camlint_of_coqint ofs) (name_of_type ty) - | Incoming -> + | Locations.Incoming -> fprintf pp "incoming(%ld,%s)" (camlint_of_coqint ofs) (name_of_type ty) - | Outgoing -> + | Locations.Outgoing -> fprintf pp "outgoing(%ld,%s)" (camlint_of_coqint ofs) (name_of_type ty) let loc pp l = match l with - | R r -> mreg pp r - | S(sl, ofs, ty) -> slot pp (sl, ofs, ty) + | Locations.R r -> mreg pp r + | Locations.S(sl, ofs, ty) -> slot pp (sl, ofs, ty) let rec locs pp = function | [] -> () diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index 31273f97..cc1f7d49 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -17,7 +17,6 @@ open Camlcoq open Datatypes open Maps open AST -open !Locations open PrintAST open PrintOp open XTL @@ -36,15 +35,15 @@ let short_name_of_type = function | Tany64 -> 'd' let loc pp = function - | R r -> mreg pp r - | S(Local, ofs, ty) -> + | Locations.R r -> mreg pp r + | Locations.S(Locations.Local, ofs, ty) -> fprintf pp "L%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) - | S(Incoming, ofs, ty) -> + | Locations.S(Locations.Incoming, ofs, ty) -> fprintf pp "I%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) - | S(Outgoing, ofs, ty) -> + | Locations.S(Locations.Outgoing, ofs, ty) -> fprintf pp "O%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) -let current_alloc = ref (None: (var -> loc) option) +let current_alloc = ref (None: (var -> Locations.loc) option) let current_liveness = ref (None: VSet.t PMap.t option) let reg pp r ty = diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 200d0237..a4710cb0 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -471,7 +471,7 @@ let rec dce_block blk after = let dead_code_elimination f liveness = { f with fn_code = - PTree.map (fun pc blk -> Datatypes.snd(dce_block blk (PMap.get pc liveness))) + PTree.map (fun pc blk -> snd(dce_block blk (PMap.get pc liveness))) f.fn_code } @@ -1171,16 +1171,15 @@ and success f alloc = end; f' -open !Errors let regalloc f = init_trace(); reset_temps(); let f1 = Splitting.rename_function f in match RTLtyping.type_function f1 with - | Error msg -> - Errors.Error(MSG (coqstring_of_camlstring "RTL code after splitting is ill-typed:") :: msg) - | OK tyenv -> + | Errors.Error msg -> + Errors.Error(Errors.MSG (coqstring_of_camlstring "RTL code after splitting is ill-typed:") :: msg) + | Errors.OK tyenv -> let f2 = function_of_RTL_function f1 tyenv in let liveness = liveness_analysis f2 in let f3 = dead_code_elimination f2 liveness in @@ -1189,12 +1188,12 @@ let regalloc f = PrintXTL.print_function !pp f3 end; try - OK(first_round f3 liveness) + Errors.OK(first_round f3 liveness) with | Timeout -> - Error(msg (coqstring_of_camlstring "Spilling fails to converge")) + Errors.Error(Errors.msg (coqstring_of_camlstring "Spilling fails to converge")) | Type_error_at pc -> - Error [MSG(coqstring_of_camlstring "Ill-typed XTL code at PC "); - POS pc] + Errors.Error [Errors.MSG(coqstring_of_camlstring "Ill-typed XTL code at PC "); + Errors.POS pc] | Bad_LTL -> - Error(msg (coqstring_of_camlstring "Bad LTL after spilling")) + Errors.Error(Errors.msg (coqstring_of_camlstring "Bad LTL after spilling")) |