aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
Diffstat (limited to 'backend')
-rw-r--r--backend/Asmexpandaux.ml9
-rw-r--r--backend/Asmexpandaux.mli36
-rw-r--r--backend/CMlexer.mll2
-rw-r--r--backend/CMparser.mly2
-rw-r--r--backend/CMtypecheck.ml17
-rw-r--r--backend/IRC.ml31
-rw-r--r--backend/IRC.mli1
-rw-r--r--backend/Inliningaux.ml2
-rw-r--r--backend/Linearizeaux.ml3
-rw-r--r--backend/PrintAsm.ml5
-rw-r--r--backend/PrintAsm.mli2
-rw-r--r--backend/PrintAsmaux.ml1
-rw-r--r--backend/PrintCminor.ml3
-rw-r--r--backend/PrintLTL.ml3
-rw-r--r--backend/PrintMach.ml4
-rw-r--r--backend/PrintRTL.ml2
-rw-r--r--backend/PrintXTL.ml4
-rw-r--r--backend/RTLgenaux.ml2
-rw-r--r--backend/Regalloc.ml40
-rw-r--r--backend/Splitting.ml2
20 files changed, 81 insertions, 90 deletions
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 *)
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index a595311a..c82f5401 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 e712057c..7fa6500a 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/CMtypecheck.ml b/backend/CMtypecheck.ml
index 72bf9cb4..cd0d25dc 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
diff --git a/backend/IRC.ml b/backend/IRC.ml
index eb677069..d542f85e 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 *)
@@ -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,43 +449,42 @@ let initialNodePartition g =
DLinkNode.insert n g.simplifyWorklist
| Colored -> ()
| _ -> assert false in
- Hashtbl.iter part_node g.varTable
-
+ Hashtbl.iter (fun _ a -> part_node a) g.varTable
(* Check invariants *)
-let degreeInvariant g n =
+let _degreeInvariant _ 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 =
+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 =
+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 =
+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 =
+let _checkInvariants g =
DLinkNode.iter
- (fun n -> degreeInvariant g n; simplifyWorklistInvariant g n)
+ (fun n -> _degreeInvariant g n; _simplifyWorklistInvariant g n)
g.simplifyWorklist;
DLinkNode.iter
- (fun n -> degreeInvariant g n; freezeWorklistInvariant g n)
+ (fun n -> _degreeInvariant g n; _freezeWorklistInvariant g n)
g.freezeWorklist;
DLinkNode.iter
- (fun n -> degreeInvariant g n; spillWorklistInvariant g n)
+ (fun n -> _degreeInvariant g n; _spillWorklistInvariant g n)
g.spillWorklist
(* Enable moves that have become low-degree related *)
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..265831a5 100644
--- a/backend/Inliningaux.ml
+++ b/backend/Inliningaux.ml
@@ -10,8 +10,6 @@
(* *)
(* *********************************************************************)
-open Camlcoq
-
(* To be considered: heuristics based on size of function? *)
let should_inline (id: AST.ident) (f: RTL.coq_function) =
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 71ee2e56..46d5c3f1 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
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 6c1eda57..96aa080e 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
@@ -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 45c18e9a..d50e07a3 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..a0a08218 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
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index 0ce2e87b..517f3037 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
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index f2242c13..ba336b0a 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 *)
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index dd8434da..31273f97 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
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 045299d4..e39d3b56 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.
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index a5fa8cd7..e531a34a 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
@@ -94,9 +92,9 @@ let rec 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
@@ -308,7 +306,7 @@ 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) ->
@@ -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) ->
@@ -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 }
@@ -484,9 +482,9 @@ let spill_costs f =
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
@@ -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 ->
@@ -690,10 +688,10 @@ 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
@@ -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) ::
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index 17b8098d..40f09c3d 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
generated by cgit (git 2.34.1) at 2024-07-03 13:38:01 +0000