From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:31:26 +0100 Subject: Update the back-end proofs to the new linking framework. --- backend/Selection.v | 68 ++++++++++++++++++++++++----------------------------- 1 file changed, 31 insertions(+), 37 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index dcefdd1c..02b37c48 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -69,6 +69,8 @@ Definition store (chunk: memory_chunk) (e1 e2: expr) := Section SELECTION. +Definition globdef := AST.globdef Cminor.fundef unit. +Variable defmap: PTree.t globdef. Variable hf: helper_functions. Definition sel_constant (cst: Cminor.constant) : expr := @@ -194,17 +196,13 @@ Definition expr_is_addrof_ident (e: Cminor.expr) : option ident := | _ => None end. -Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := +Definition classify_call (e: Cminor.expr) : call_kind := match expr_is_addrof_ident e with | None => Call_default | Some id => - match Genv.find_symbol ge id with - | None => Call_imm id - | Some b => - match Genv.find_funct_ptr ge b with - | Some(External ef) => if ef_inline ef then Call_builtin ef else Call_imm id - | _ => Call_imm id - end + match defmap!id with + | Some(Gfun(External ef)) => if ef_inline ef then Call_builtin ef else Call_imm id + | _ => Call_imm id end end. @@ -279,13 +277,13 @@ Definition sel_switch_long := (** Conversion from Cminor statements to Cminorsel statements. *) -Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := +Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := match s with | Cminor.Sskip => OK Sskip | Cminor.Sassign id e => OK (Sassign id (sel_expr e)) | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs)) | Cminor.Scall optid sg fn args => - OK (match classify_call ge fn with + OK (match classify_call fn with | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef @@ -296,20 +294,20 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := OK (Sbuiltin (sel_builtin_res optid) ef (sel_builtin_args args (Machregs.builtin_constraints ef))) | Cminor.Stailcall sg fn args => - OK (match classify_call ge fn with + OK (match classify_call fn with | Call_imm id => Stailcall sg (inr _ id) (sel_exprlist args) | _ => Stailcall sg (inl _ (sel_expr fn)) (sel_exprlist args) end) | Cminor.Sseq s1 s2 => - do s1' <- sel_stmt ge s1; do s2' <- sel_stmt ge s2; + do s1' <- sel_stmt s1; do s2' <- sel_stmt s2; OK (Sseq s1' s2') | Cminor.Sifthenelse e ifso ifnot => - do ifso' <- sel_stmt ge ifso; do ifnot' <- sel_stmt ge ifnot; + do ifso' <- sel_stmt ifso; do ifnot' <- sel_stmt ifnot; OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot') | Cminor.Sloop body => - do body' <- sel_stmt ge body; OK (Sloop body') + do body' <- sel_stmt body; OK (Sloop body') | Cminor.Sblock body => - do body' <- sel_stmt ge body; OK (Sblock body') + do body' <- sel_stmt body; OK (Sblock body') | Cminor.Sexit n => OK (Sexit n) | Cminor.Sswitch false e cases dfl => let t := compile_switch Int.modulus dfl cases in @@ -324,14 +322,14 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := | Cminor.Sreturn None => OK (Sreturn None) | Cminor.Sreturn (Some e) => OK (Sreturn (Some (sel_expr e))) | Cminor.Slabel lbl body => - do body' <- sel_stmt ge body; OK (Slabel lbl body') + do body' <- sel_stmt body; OK (Slabel lbl body') | Cminor.Sgoto lbl => OK (Sgoto lbl) end. (** Conversion of functions. *) -Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := - do body' <- sel_stmt ge f.(Cminor.fn_body); +Definition sel_function (f: Cminor.function) : res function := + do body' <- sel_stmt f.(Cminor.fn_body); OK (mkfunction f.(Cminor.fn_sig) f.(Cminor.fn_params) @@ -339,41 +337,36 @@ Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := f.(Cminor.fn_stackspace) body'). -Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := - transf_partial_fundef (sel_function ge) f. +Definition sel_fundef (f: Cminor.fundef) : res fundef := + transf_partial_fundef sel_function f. End SELECTION. (** Setting up the helper functions. *) -Definition globdef := AST.globdef Cminor.fundef unit. - (** We build a partial mapping from global identifiers to their definitions, restricting ourselves to the globals we are interested in, namely - the external function declarations whose name starts with "__i64_". + the external function declarations that are marked as runtime library + helpers. This ensures that the mapping remains small and that [lookup_helper] below is efficient. *) Definition globdef_of_interest (gd: globdef) : bool := match gd with - | Gfun (External (EF_external name sg)) => String.prefix "__i64_" name + | Gfun (External (EF_runtime name sg)) => true | _ => false end. -Definition record_globdef (globs: PTree.t globdef) (id_gd: ident * globdef) := - let (id, gd) := id_gd in - if globdef_of_interest gd - then PTree.set id gd globs - else PTree.remove id globs. - -Definition record_globdefs (p: Cminor.program) : PTree.t globdef := - List.fold_left record_globdef p.(prog_defs) (PTree.empty _). +Definition record_globdefs (defmap: PTree.t globdef) : PTree.t globdef := + PTree.fold + (fun m id gd => if globdef_of_interest gd then PTree.set id gd m else m) + defmap (PTree.empty globdef). Definition lookup_helper_aux (name: String.string) (sg: signature) (res: option ident) (id: ident) (gd: globdef) := match gd with - | Gfun (External (EF_external name' sg')) => + | Gfun (External (EF_runtime name' sg')) => if String.string_dec name name' && signature_eq sg sg' then Some id else res @@ -389,8 +382,8 @@ Definition lookup_helper (globs: PTree.t globdef) Local Open Scope string_scope. -Definition get_helpers (p: Cminor.program) : res helper_functions := - let globs := record_globdefs p in +Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := + let globs := record_globdefs defmap in do i64_dtos <- lookup_helper globs "__i64_dtos" sig_f_l ; do i64_dtou <- lookup_helper globs "__i64_dtou" sig_f_l ; do i64_stod <- lookup_helper globs "__i64_stod" sig_l_f ; @@ -412,6 +405,7 @@ Definition get_helpers (p: Cminor.program) : res helper_functions := (** Conversion of programs. *) Definition sel_program (p: Cminor.program) : res program := - do hf <- get_helpers p; - transform_partial_program (sel_fundef hf (Genv.globalenv p)) p. + let dm := prog_defmap p in + do hf <- get_helpers dm; + transform_partial_program (sel_fundef dm hf) p. -- cgit