From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 19 May 2013 09:54:40 +0000 Subject: Merge of the float32 branch: - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Allocation.v | 134 ++++++++++++++++++++++++++++++--------------------- 1 file changed, 78 insertions(+), 56 deletions(-) (limited to 'backend/Allocation.v') diff --git a/backend/Allocation.v b/backend/Allocation.v index e4d0972f..a4dd3af0 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -608,6 +608,20 @@ Definition subst_loc (l1 l2: loc) (e: eqs) : option eqs := (EqSet2.elements_between (select_loc_l l1) (select_loc_h l1) (eqs2 e)) (Some e). +(** [loc_type_compat env l e] checks that for all equations [r = l] in [e], + the type [env r] of [r] is compatible with the type of [l]. *) + +Definition sel_type (k: equation_kind) (ty: typ) : typ := + match k with + | Full => ty + | Low | High => Tint + end. + +Definition loc_type_compat (env: regenv) (l: loc) (e: eqs) : bool := + EqSet2.for_all_between + (fun q => subtype (sel_type (ekind q) (env (ereg q))) (Loc.type l)) + (select_loc_l l) (select_loc_h l) (eqs2 e). + (** [add_equations [r1...rN] [m1...mN] e] adds to [e] the [N] equations [ri = R mi [Full]]. Return [None] if the two lists have different lengths. *) @@ -628,7 +642,7 @@ Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list loc) (e: eq | nil, nil, nil => Some e | r1 :: rl, Tlong :: tyl, l1 :: l2 :: ll => add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e)) - | r1 :: rl, (Tint|Tfloat) :: tyl, l1 :: ll => + | r1 :: rl, (Tint|Tfloat|Tsingle) :: tyl, l1 :: ll => add_equations_args rl tyl ll (add_equation (Eq Full r1 l1) e) | _, _, _ => None end. @@ -752,9 +766,16 @@ Definition ros_compatible_tailcall (ros: mreg + ident) : bool := (** * The validator *) Definition destroyed_by_move (src dst: loc) := - match src with - | S sl ofs ty => destroyed_by_getstack sl - | _ => destroyed_by_op Omove + match src, dst with + | S sl ofs ty, _ => destroyed_by_getstack sl + | _, S sl ofs ty => destroyed_by_setstack ty + | _, _ => destroyed_by_op Omove + end. + +Definition well_typed_move (env: regenv) (dst: loc) (e: eqs) : bool := + match dst with + | R r => true + | S sl ofs ty => loc_type_compat env dst e end. (** Simulate the effect of a sequence of moves [mv] on a set of @@ -763,14 +784,14 @@ Definition destroyed_by_move (src dst: loc) := must hold before the sequence of moves. Return [None] if the set of equations [e] cannot hold after the sequence of moves. *) -Fixpoint track_moves (mv: moves) (e: eqs) : option eqs := +Fixpoint track_moves (env: regenv) (mv: moves) (e: eqs) : option eqs := match mv with | nil => Some e | (src, dst) :: mv => - do e1 <- track_moves mv e; - do e2 <- subst_loc dst src e1; + do e1 <- track_moves env mv e; assertion (can_undef_except dst (destroyed_by_move src dst)) e1; - Some e2 + assertion (well_typed_move env dst e1); + subst_loc dst src e1 end. (** [transfer_use_def args res args' res' undefs e] returns the set @@ -802,89 +823,89 @@ Definition kind_second_word := if big_endian then Low else High. equations that must hold "before" these instructions, or [None] if impossible. *) -Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option eqs := +Definition transfer_aux (f: RTL.function) (env: regenv) (shape: block_shape) (e: eqs) : option eqs := match shape with | BSnop mv s => - track_moves mv e + track_moves env mv e | BSmove src dst mv s => - track_moves mv (subst_reg dst src e) + track_moves env mv (subst_reg dst src e) | BSmakelong src1 src2 dst mv s => let e1 := subst_reg_kind dst High src1 Full e in let e2 := subst_reg_kind dst Low src2 Full e1 in assertion (reg_unconstrained dst e2); - track_moves mv e2 + track_moves env mv e2 | BSlowlong src dst mv s => let e1 := subst_reg_kind dst Full src Low e in assertion (reg_unconstrained dst e1); - track_moves mv e1 + track_moves env mv e1 | BShighlong src dst mv s => let e1 := subst_reg_kind dst Full src High e in assertion (reg_unconstrained dst e1); - track_moves mv e1 + track_moves env mv e1 | BSop op args res mv1 args' res' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; do e2 <- transfer_use_def args res args' res' (destroyed_by_op op) e1; - track_moves mv1 e2 + track_moves env mv1 e2 | BSopdead op args res mv s => assertion (reg_unconstrained res e); - track_moves mv e + track_moves env mv e | BSload chunk addr args dst mv1 args' dst' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1; - track_moves mv1 e2 + track_moves env mv1 e2 | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => - do e1 <- track_moves mv3 e; + do e1 <- track_moves env mv3 e; let e2 := remove_equation (Eq kind_second_word dst (R dst2')) e1 in assertion (loc_unconstrained (R dst2') e2); assertion (can_undef (destroyed_by_load Mint32 addr') e2); do e3 <- add_equations args args2' e2; - do e4 <- track_moves mv2 e3; + do e4 <- track_moves env mv2 e3; let e5 := remove_equation (Eq kind_first_word dst (R dst1')) e4 in assertion (loc_unconstrained (R dst1') e5); assertion (can_undef (destroyed_by_load Mint32 addr) e5); assertion (reg_unconstrained dst e5); do e6 <- add_equations args args1' e5; - track_moves mv1 e6 + track_moves env mv1 e6 | BSload2_1 addr args dst mv1 args' dst' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; let e2 := remove_equation (Eq kind_first_word dst (R dst')) e1 in assertion (reg_loc_unconstrained dst (R dst') e2); assertion (can_undef (destroyed_by_load Mint32 addr) e2); do e3 <- add_equations args args' e2; - track_moves mv1 e3 + track_moves env mv1 e3 | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; let e2 := remove_equation (Eq kind_second_word dst (R dst')) e1 in assertion (reg_loc_unconstrained dst (R dst') e2); assertion (can_undef (destroyed_by_load Mint32 addr') e2); do e3 <- add_equations args args' e2; - track_moves mv1 e3 + track_moves env mv1 e3 | BSloaddead chunk addr args dst mv s => assertion (reg_unconstrained dst e); - track_moves mv e + track_moves env mv e | BSstore chunk addr args src mv args' src' s => assertion (can_undef (destroyed_by_store chunk addr) e); do e1 <- add_equations (src :: args) (src' :: args') e; - track_moves mv e1 + track_moves env mv e1 | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s => assertion (can_undef (destroyed_by_store Mint32 addr') e); do e1 <- add_equations args args2' (add_equation (Eq kind_second_word src (R src2')) e); - do e2 <- track_moves mv2 e1; + do e2 <- track_moves env mv2 e1; assertion (can_undef (destroyed_by_store Mint32 addr) e2); do e3 <- add_equations args args1' (add_equation (Eq kind_first_word src (R src1')) e2); - track_moves mv1 e3 + track_moves env mv1 e3 | BScall sg ros args res mv1 ros' mv2 s => let args' := loc_arguments sg in let res' := map R (loc_result sg) in - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; do e2 <- remove_equations_res res (sig_res sg) res' e1; assertion (forallb (fun l => reg_loc_unconstrained res l e2) res'); assertion (no_caller_saves e2); do e3 <- add_equation_ros ros ros' e2; do e4 <- add_equations_args args (sig_args sg) args' e3; - track_moves mv1 e4 + track_moves env mv1 e4 | BStailcall sg ros args mv1 ros' => let args' := loc_arguments sg in assertion (tailcall_is_possible sg); @@ -892,9 +913,9 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option assertion (ros_compatible_tailcall ros'); do e1 <- add_equation_ros ros ros' empty_eqs; do e2 <- add_equations_args args (sig_args sg) args' e1; - track_moves mv1 e2 + track_moves env mv1 e2 | BSbuiltin ef args res mv1 args' res' mv2 s => - do e1 <- track_moves mv2 e; + do e1 <- track_moves env mv2 e; let args' := map R args' in let res' := map R res' in do e2 <- remove_equations_res res (sig_res (ef_sig ef)) res' e1; @@ -902,23 +923,23 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option assertion (forallb (fun l => loc_unconstrained l e2) res'); assertion (can_undef (destroyed_by_builtin ef) e2); do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2; - track_moves mv1 e3 + track_moves env mv1 e3 | BSannot txt typ args res mv1 args' s => do e1 <- add_equations_args args (annot_args_typ typ) args' e; - track_moves mv1 e1 + track_moves env mv1 e1 | BScond cond args mv args' s1 s2 => assertion (can_undef (destroyed_by_cond cond) e); do e1 <- add_equations args args' e; - track_moves mv e1 + track_moves env mv e1 | BSjumptable arg mv arg' tbl => assertion (can_undef destroyed_by_jumptable e); - track_moves mv (add_equation (Eq Full arg (R arg')) e) + track_moves env mv (add_equation (Eq Full arg (R arg')) e) | BSreturn None mv => - track_moves mv empty_eqs + track_moves env mv empty_eqs | BSreturn (Some arg) mv => let arg' := map R (loc_result (RTL.fn_sig f)) in do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs; - track_moves mv e1 + track_moves env mv e1 end. (** The main transfer function for the dataflow analysis. Like [transfer_aux], @@ -926,7 +947,7 @@ Definition transfer_aux (f: RTL.function) (shape: block_shape) (e: eqs) : option equations that must hold "after". It also handles error propagation and reporting. *) -Definition transfer (f: RTL.function) (shapes: PTree.t block_shape) +Definition transfer (f: RTL.function) (env: regenv) (shapes: PTree.t block_shape) (pc: node) (after: res eqs) : res eqs := match after with | Error _ => after @@ -934,7 +955,7 @@ Definition transfer (f: RTL.function) (shapes: PTree.t block_shape) match shapes!pc with | None => Error(MSG "At PC " :: POS pc :: MSG ": unmatched block" :: nil) | Some shape => - match transfer_aux f shape e with + match transfer_aux f env shape e with | None => Error(MSG "At PC " :: POS pc :: MSG ": invalid register allocation" :: nil) | Some e' => OK e' end @@ -1082,8 +1103,8 @@ Definition successors_block_shape (bsh: block_shape) : list node := | BSreturn optarg mv => nil end. -Definition analyze (f: RTL.function) (bsh: PTree.t block_shape) := - DS.fixpoint (PTree.map1 successors_block_shape bsh) (transfer f bsh) nil. +Definition analyze (f: RTL.function) (env: regenv) (bsh: PTree.t block_shape) := + DS.fixpoint (PTree.map1 successors_block_shape bsh) (transfer f env bsh) nil. (** * Validating and translating functions and programs *) @@ -1107,7 +1128,7 @@ Function compat_entry (rparams: list reg) (tys: list typ) (lparams: list loc) (e | nil, nil, nil => true | r1 :: rl, Tlong :: tyl, l1 :: l2 :: ll => compat_left2 r1 l1 l2 e && compat_entry rl tyl ll e - | r1 :: rl, (Tint|Tfloat) :: tyl, l1 :: ll => + | r1 :: rl, (Tint|Tfloat|Tsingle) :: tyl, l1 :: ll => compat_left r1 l1 e && compat_entry rl tyl ll e | _, _, _ => false end. @@ -1116,9 +1137,10 @@ Function compat_entry (rparams: list reg) (tys: list typ) (lparams: list loc) (e point. We also check that the RTL and LTL functions agree in signature and stack size. *) -Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function) (e1: eqs) : option unit := +Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function) + (env: regenv) (e1: eqs) : option unit := do mv <- pair_entrypoints rtl ltl; - do e2 <- track_moves mv e1; + do e2 <- track_moves env mv e1; assertion (compat_entry (RTL.fn_params rtl) (sig_args (RTL.fn_sig rtl)) (loc_parameters (RTL.fn_sig rtl)) e2); @@ -1131,10 +1153,10 @@ Local Close Scope option_monad_scope. Local Open Scope error_monad_scope. Definition check_entrypoints (rtl: RTL.function) (ltl: LTL.function) - (bsh: PTree.t block_shape) - (a: PMap.t LEq.t): res unit := - do e1 <- transfer rtl bsh (RTL.fn_entrypoint rtl) a!!(RTL.fn_entrypoint rtl); - match check_entrypoints_aux rtl ltl e1 with + (env: regenv) (bsh: PTree.t block_shape) + (a: PMap.t LEq.t): res unit := + do e1 <- transfer rtl env bsh (RTL.fn_entrypoint rtl) a!!(RTL.fn_entrypoint rtl); + match check_entrypoints_aux rtl ltl env e1 with | None => Error (msg "invalid register allocation at entry point") | Some _ => OK tt end. @@ -1143,11 +1165,11 @@ Definition check_entrypoints (rtl: RTL.function) (ltl: LTL.function) a source RTL function and an LTL function generated by the external register allocator. *) -Definition check_function (rtl: RTL.function) (ltl: LTL.function) : res unit := +Definition check_function (rtl: RTL.function) (ltl: LTL.function) (env: regenv) : res unit := let bsh := pair_codes rtl ltl in - match analyze rtl bsh with + match analyze rtl env bsh with | None => Error (msg "allocation analysis diverges") - | Some a => check_entrypoints rtl ltl bsh a + | Some a => check_entrypoints rtl ltl env bsh a end. (** [regalloc] is the external register allocator. It is written in OCaml @@ -1160,10 +1182,10 @@ Parameter regalloc: RTL.function -> res LTL.function. Definition transf_function (f: RTL.function) : res LTL.function := match type_function f with | Error m => Error m - | OK tyenv => + | OK env => match regalloc f with | Error m => Error m - | OK tf => do x <- check_function f tf; OK tf + | OK tf => do x <- check_function f tf env; OK tf end end. -- cgit