From ad12162ff1f0d50c43afefc45e1593f27f197402 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 26 Dec 2013 15:46:54 +0000 Subject: Future-proofing: keep signature information in IA32 and PowerPC Asm, just like we already do in ARM Asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Asm_printers.ml | 8 +++---- checklink/Check.ml | 12 +++++------ ia32/Asm.v | 55 +++++++++++++++++++++++------------------------ ia32/Asmgen.v | 21 +++++++++++------- ia32/Asmgenproof.v | 34 ++++++++++++++--------------- ia32/Asmgenproof1.v | 2 +- ia32/PrintAsm.ml | 12 +++++------ ia32/Unusedglob1.ml | 6 +++--- powerpc/Asm.v | 53 ++++++++++++++++++++++----------------------- powerpc/Asmgen.v | 25 ++++++++++----------- powerpc/Asmgenproof.v | 36 +++++++++++++++---------------- powerpc/Asmgenproof1.v | 2 +- powerpc/PrintAsm.ml | 15 +++++++------ powerpc/Unusedglob1.ml | 6 +++--- 14 files changed, 146 insertions(+), 141 deletions(-) diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index 5b3abe8..c84bd55 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -137,11 +137,11 @@ let string_of_instruction = function | Pandi_ (i0, i1, c2) -> "Pandi_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" | Pandis_ (i0, i1, c2) -> "Pandis_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" | Pb (l0) -> "Pb(" ^ string_of_label l0 ^ ")" -| Pbctr -> "Pbctr" -| Pbctrl -> "Pbctrl" +| Pbctr sg -> "Pbctr" +| Pbctrl sg -> "Pbctrl" | Pbf (c0, l1) -> "Pbf(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" -| Pbl (i0) -> "Pbl(" ^ string_of_ident i0 ^ ")" -| Pbs (i0) -> "Pbs(" ^ string_of_ident i0 ^ ")" +| Pbl (i0, sg) -> "Pbl(" ^ string_of_ident i0 ^ ")" +| Pbs (i0, sg) -> "Pbs(" ^ string_of_ident i0 ^ ")" | Pblr -> "Pblr" | Pbt (c0, l1) -> "Pbt(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" | Pbtbl (i0, l1) -> "Pbtbl(" ^ string_of_ireg i0 ^ ", " ^ string_of_list string_of_label ", " l1 ^ ")" diff --git a/checklink/Check.ml b/checklink/Check.ml index 50928d2..c51e090 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -38,7 +38,7 @@ let exhaustivity = ref true let list_missing = ref false (** CompCert Asm *) -type ccode = Asm.instruction list +type ccode = Asm.coq_function let print_debug s = if !debug then print_endline (string_of_log_entry true (DEBUG(s))) @@ -1021,7 +1021,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pbctr -> + | Pbctr sg -> begin match ecode with | BCCTRx(bo, bi, lk) :: es -> OK(fw) @@ -1031,7 +1031,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pbctrl -> + | Pbctrl sg -> begin match ecode with | BCCTRx(bo, bi, lk) :: es -> OK(fw) @@ -1069,7 +1069,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= compare_code cs es (Int32.add 8l pc) | _ -> error end - | Pbl(ident) -> + | Pbl(ident, sg) -> begin match ecode with | Bx(li, aa, lk) :: es -> let dest = Int32.(add pc (mul 4l (exts li))) in @@ -1090,7 +1090,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pbs(ident) -> + | Pbs(ident, sg) -> begin match ecode with | Bx(li, aa, lk) :: es -> let dest = Int32.(add pc (mul 4l (exts li))) in @@ -2637,7 +2637,7 @@ let rec worklist_process (wl: worklist) sfw: s_framework = label_list = []; } ) - >>> compare_code ccode ecode pc + >>> compare_code ccode.fn_code ecode pc >>^ mark_covered_fun_sym_ndx ndx ) in begin match candidates with diff --git a/ia32/Asm.v b/ia32/Asm.v index 78c4c3b..7bd1755 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -181,13 +181,13 @@ Inductive instruction: Type := | Pxorpd_f (rd: freg) (**r [xor] with self = set to zero *) (** Branches and calls *) | Pjmp_l (l: label) - | Pjmp_s (symb: ident) - | Pjmp_r (r: ireg) + | Pjmp_s (symb: ident) (sg: signature) + | Pjmp_r (r: ireg) (sg: signature) | Pjcc (c: testcond)(l: label) | Pjcc2 (c1 c2: testcond)(l: label) (**r pseudo *) | Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *) - | Pcall_s (symb: ident) - | Pcall_r (r: ireg) + | Pcall_s (symb: ident) (sg: signature) + | Pcall_r (r: ireg) (sg: signature) | Pret (** Pseudo-instructions *) | Plabel(l: label) @@ -201,9 +201,8 @@ with annot_param : Type := | APstack: memory_chunk -> Z -> annot_param. Definition code := list instruction. -Definition function := code. -Definition fn_code (f: function) : code := f. -Definition fundef := AST.fundef code. +Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. +Definition fundef := AST.fundef function. Definition program := AST.program fundef unit. (** * Operational semantics *) @@ -423,8 +422,8 @@ Definition nextinstr (rs: regset) := Definition nextinstr_nf (rs: regset) : regset := nextinstr (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs). -Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := - match label_pos lbl 0 c with +Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := + match label_pos lbl 0 (fn_code f) with | None => Stuck | Some pos => match rs#PC with @@ -469,7 +468,7 @@ Definition exec_store (chunk: memory_chunk) (m: mem) but we do not need to model this precisely. *) -Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome := +Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := match i with (** Moves *) | Pmov_rr rd r1 => @@ -627,20 +626,20 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m (** Branches and calls *) | Pjmp_l lbl => - goto_label c lbl rs m - | Pjmp_s id => + goto_label f lbl rs m + | Pjmp_s id sg => Next (rs#PC <- (symbol_offset id Int.zero)) m - | Pjmp_r r => + | Pjmp_r r sg => Next (rs#PC <- (rs r)) m | Pjcc cond lbl => match eval_testcond cond rs with - | Some true => goto_label c lbl rs m + | Some true => goto_label f lbl rs m | Some false => Next (nextinstr rs) m | None => Stuck end | Pjcc2 cond1 cond2 lbl => match eval_testcond cond1 rs, eval_testcond cond2 rs with - | Some true, Some true => goto_label c lbl rs m + | Some true, Some true => goto_label f lbl rs m | Some _, Some _ => Next (nextinstr rs) m | _, _ => Stuck end @@ -649,13 +648,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Vint n => match list_nth_z tbl (Int.unsigned n) with | None => Stuck - | Some lbl => goto_label c lbl rs m + | Some lbl => goto_label f lbl rs m end | _ => Stuck end - | Pcall_s id => + | Pcall_s id sg => Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m - | Pcall_r r => + | Pcall_r r sg => Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (rs r)) m | Pret => Next (rs#PC <- (rs#RA)) m @@ -760,27 +759,27 @@ Inductive state: Type := Inductive step: state -> trace -> state -> Prop := | exec_step_internal: - forall b ofs c i rs m rs' m', + forall b ofs f i rs m rs' m', rs PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal c) -> - find_instr (Int.unsigned ofs) c = Some i -> - exec_instr c i rs m = Next rs' m' -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_instr (Int.unsigned ofs) f.(fn_code) = Some i -> + exec_instr f i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: - forall b ofs c ef args res rs m t vl rs' m', + forall b ofs f ef args res rs m t vl rs' m', rs PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal c) -> - find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> external_call' ef ge (map rs args) m t vl m' -> rs' = nextinstr_nf (set_regs res vl (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') | exec_step_annot: - forall b ofs c ef args rs m vargs t v m', + forall b ofs f ef args rs m vargs t v m', rs PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal c) -> - find_instr (Int.unsigned ofs) c = Some (Pannot ef args) -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) -> annot_arguments rs m args vargs -> external_call' ef ge vargs m t v m' -> step (State rs m) t diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 0410057..740dff8 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -496,16 +496,16 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl reg) => - do r <- ireg_of reg; OK (Pcall_r r :: k) + do r <- ireg_of reg; OK (Pcall_r r sig :: k) | Mcall sig (inr symb) => - OK (Pcall_s symb :: k) + OK (Pcall_s symb sig :: k) | Mtailcall sig (inl reg) => do r <- ireg_of reg; OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: - Pjmp_r r :: k) + Pjmp_r r sig :: k) | Mtailcall sig (inr symb) => OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: - Pjmp_s symb :: k) + Pjmp_s symb sig :: k) | Mlabel lbl => OK(Plabel lbl :: k) | Mgoto lbl => @@ -563,11 +563,16 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) -Definition transf_function (f: Mach.function) : res Asm.code := +Definition transl_function (f: Mach.function) := do c <- transl_code' f f.(Mach.fn_code) true; - if zlt (list_length_z c) Int.max_unsigned - then OK (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c) - else Error (msg "code size exceeded"). + OK (mkfunction f.(Mach.fn_sig) + (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c)). + +Definition transf_function (f: Mach.function) : res Asm.function := + do tf <- transl_function f; + if zlt Int.max_unsigned (list_length_z tf.(fn_code)) + then Error (msg "code size exceeded") + else OK tf. Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index df09ca7..fa8ce6c 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -77,10 +77,10 @@ Qed. Lemma transf_function_no_overflow: forall f tf, - transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned. + transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned. Proof. - intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); monadInv EQ0. - rewrite list_length_z_cons. omega. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); monadInv EQ0. + omega. Qed. Lemma exec_straight_exec: @@ -299,12 +299,12 @@ Lemma transl_find_label: forall lbl f tf, transf_function f = OK tf -> match Mach.find_label lbl f.(Mach.fn_code) with - | None => find_label lbl tf = None - | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc + | None => find_label lbl tf.(fn_code) = None + | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc end. Proof. - intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. - simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ; eauto. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. + monadInv EQ. simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ0; eauto. Qed. End TRANSL_LABEL. @@ -346,8 +346,8 @@ Proof. - intros. exploit transl_instr_label; eauto. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. - destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. - rewrite transl_code'_transl_code in EQ. + destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. + monadInv EQ. rewrite transl_code'_transl_code in EQ0. exists x; exists true; split; auto. unfold fn_code. repeat constructor. - exact transf_function_no_overflow. Qed. @@ -583,7 +583,7 @@ Opaque loadind. - (* Mcall *) assert (f0 = f) by congruence. subst f0. inv AT. - assert (NOOV: list_length_z tf <= Int.max_unsigned). + assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. destruct ros as [rf|fid]; simpl in H; monadInv H5. + (* Indirect call *) @@ -623,7 +623,7 @@ Opaque loadind. - (* Mtailcall *) assert (f0 = f) by congruence. subst f0. inv AT. - assert (NOOV: list_length_z tf <= Int.max_unsigned). + assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. @@ -820,7 +820,7 @@ Transparent destroyed_by_jumptable. - (* Mreturn *) assert (f0 = f) by congruence. subst f0. inv AT. - assert (NOOV: list_length_z tf <= Int.max_unsigned). + assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. @@ -844,8 +844,9 @@ Transparent destroyed_by_jumptable. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. - generalize EQ; intros EQ'. monadInv EQ'. rewrite transl_code'_transl_code in EQ0. - destruct (zlt (list_length_z x0) Int.max_unsigned); inversion EQ1. clear EQ1. + generalize EQ; intros EQ'. monadInv EQ'. + destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inv EQ1. + monadInv EQ0. rewrite transl_code'_transl_code in EQ1. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. @@ -855,14 +856,13 @@ Transparent destroyed_by_jumptable. intros [m3' [P Q]]. left; econstructor; split. apply plus_one. econstructor; eauto. - subst x; simpl. - rewrite Int.unsigned_zero. simpl. eauto. + simpl. rewrite Int.unsigned_zero. simpl. eauto. simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F. simpl in P. rewrite ATLR. rewrite P. eauto. econstructor; eauto. unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. rewrite ATPC. simpl. constructor; eauto. - subst x. unfold fn_code. eapply code_tail_next_int. rewrite list_length_z_cons. omega. + unfold fn_code. eapply code_tail_next_int. simpl in g. omega. constructor. apply agree_nextinstr. eapply agree_change_sp; eauto. Transparent destroyed_at_function_entry. diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 9ddc463..5d3df67 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -97,7 +97,7 @@ Ltac Simplifs := repeat Simplif. Section CONSTRUCTORS. Variable ge: genv. -Variable fn: code. +Variable fn: function. (** Smart constructor for moves. *) diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 4480f91..3badbfc 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -681,9 +681,9 @@ let print_instruction oc = function (** Branches and calls *) | Pjmp_l(l) -> fprintf oc " jmp %a\n" label (transl_label l) - | Pjmp_s(f) -> + | Pjmp_s(f, sg) -> fprintf oc " jmp %a\n" symbol f - | Pjmp_r(r) -> + | Pjmp_r(r, sg) -> fprintf oc " jmp *%a\n" ireg r | Pjcc(c, l) -> let l = transl_label l in @@ -698,9 +698,9 @@ let print_instruction oc = function let l = new_label() in fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r; jumptables := (l, tbl) :: !jumptables - | Pcall_s(f) -> + | Pcall_s(f, sg) -> fprintf oc " call %a\n" symbol f - | Pcall_r(r) -> + | Pcall_r(r, sg) -> fprintf oc " call *%a\n" ireg r | Pret -> fprintf oc " ret\n" @@ -758,7 +758,7 @@ let print_jumptable oc (lbl, tbl) = (fun l -> fprintf oc " .long %a\n" label (transl_label l)) tbl -let print_function oc name code = +let print_function oc name fn = Hashtbl.clear current_function_labels; float_literals := []; jumptables := []; @@ -775,7 +775,7 @@ let print_function oc name code = fprintf oc "%a:\n" symbol name; print_location oc (C2C.atom_location name); cfi_startproc oc; - List.iter (print_instruction oc) code; + List.iter (print_instruction oc) fn.fn_code; cfi_endproc oc; if target = ELF then begin fprintf oc " .type %a, @function\n" symbol name; diff --git a/ia32/Unusedglob1.ml b/ia32/Unusedglob1.ml index fe962e2..8332a30 100644 --- a/ia32/Unusedglob1.ml +++ b/ia32/Unusedglob1.ml @@ -35,10 +35,10 @@ let referenced_instr = function | Pmovzb_rm (_, a) | Pmovsb_rm (_, a) | Pmovzw_rm (_, a) | Pmovsw_rm (_, a) | Pcvtss2sd_fm (_, a) | Pcvtsd2ss_mf (a, _) | Plea (_, a) -> referenced_addr a - | Pjmp_s s -> [s] - | Pcall_s s -> [s] + | Pjmp_s(s, _) -> [s] + | Pcall_s(s, _) -> [s] | Pbuiltin(ef, args, res) -> referenced_builtin ef | _ -> [] -let code_of_function f = f +let code_of_function f = f.fn_code diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 1441929..4499f01 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -145,11 +145,11 @@ Inductive instruction : Type := | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) | Pandis_: ireg -> ireg -> constant -> instruction (**r and immediate high and set conditions *) | Pb: label -> instruction (**r unconditional branch *) - | Pbctr: instruction (**r branch to contents of register CTR *) - | Pbctrl: instruction (**r branch to contents of CTR and link *) + | Pbctr: signature -> instruction (**r branch to contents of register CTR *) + | Pbctrl: signature -> instruction (**r branch to contents of CTR and link *) | Pbf: crbit -> label -> instruction (**r branch if false *) - | Pbl: ident -> instruction (**r branch and link *) - | Pbs: ident -> instruction (**r branch to symbol *) + | Pbl: ident -> signature -> instruction (**r branch and link *) + | Pbs: ident -> signature -> instruction (**r branch to symbol *) | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) @@ -300,8 +300,7 @@ lbl: .long table[0], table[1], ... *) Definition code := list instruction. -Definition function := code. -Definition fn_code (f: function) : code := f. +Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. Definition fundef := AST.fundef function. Definition program := AST.program fundef unit. @@ -470,8 +469,8 @@ Inductive outcome: Type := Definition nextinstr (rs: regset) := rs#PC <- (Val.add rs#PC Vone). -Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) := - match label_pos lbl 0 c with +Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := + match label_pos lbl 0 (fn_code f) with | None => Stuck | Some pos => match rs#PC with @@ -551,7 +550,7 @@ Definition compare_float (rs: regset) (v1 v2: val) := must survive the execution of the pseudo-instruction. *) -Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome := +Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := match i with | Padd rd r1 r2 => Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m @@ -587,25 +586,25 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome let v := Val.and rs#r1 (const_high cst) in Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m | Pb lbl => - goto_label c lbl rs m - | Pbctr => + goto_label f lbl rs m + | Pbctr sg => Next (rs#PC <- (rs#CTR)) m - | Pbctrl => + | Pbctrl sg => Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (rs#CTR)) m | Pbf bit lbl => match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then goto_label c lbl rs m else Next (nextinstr rs) m + | Vint n => if Int.eq n Int.zero then goto_label f lbl rs m else Next (nextinstr rs) m | _ => Stuck end - | Pbl ident => + | Pbl ident sg => Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m - | Pbs ident => + | Pbs ident sg => Next (rs#PC <- (symbol_offset ident Int.zero)) m | Pblr => Next (rs#PC <- (rs#LR)) m | Pbt bit lbl => match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label c lbl rs m + | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label f lbl rs m | _ => Stuck end | Pbtbl r tbl => @@ -613,7 +612,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Vint n => match list_nth_z tbl (Int.unsigned n) with | None => Stuck - | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m + | Some lbl => goto_label f lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m end | _ => Stuck end @@ -857,27 +856,27 @@ Inductive state: Type := Inductive step: state -> trace -> state -> Prop := | exec_step_internal: - forall b ofs c i rs m rs' m', + forall b ofs f i rs m rs' m', rs PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal c) -> - find_instr (Int.unsigned ofs) c = Some i -> - exec_instr c i rs m = Next rs' m' -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_instr (Int.unsigned ofs) f.(fn_code) = Some i -> + exec_instr f i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: - forall b ofs c ef args res rs m t vl rs' m', + forall b ofs f ef args res rs m t vl rs' m', rs PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal c) -> - find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> external_call' ef ge (map rs args) m t vl m' -> rs' = nextinstr (set_regs res vl (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') | exec_step_annot: - forall b ofs c ef args rs m vargs t v m', + forall b ofs f ef args rs m vargs t v m', rs PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal c) -> - find_instr (Int.unsigned ofs) c = Some (Pannot ef args) -> + Genv.find_funct_ptr ge b = Some (Internal f) -> + find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) -> annot_arguments rs m args vargs -> external_call' ef ge vargs m t v m' -> step (State rs m) t diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index b3f0722..39c0d1b 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -623,21 +623,21 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl r) => - do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl :: k) + do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl sig :: k) | Mcall sig (inr symb) => - OK (Pbl symb :: k) + OK (Pbl symb sig :: k) | Mtailcall sig (inl r) => do r1 <- ireg_of r; OK (Pmtctr r1 :: Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR0 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pbctr :: k) + Pbctr sig :: k) | Mtailcall sig (inr symb) => OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR0 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pbs symb :: k) + Pbs symb sig :: k) | Mbuiltin ef args res => OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) | Mannot ef args => @@ -703,15 +703,16 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo Definition transl_function (f: Mach.function) := do c <- transl_code' f f.(Mach.fn_code) false; - OK (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - Pmflr GPR0 :: - Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c). - -Definition transf_function (f: Mach.function) : res Asm.code := - do c <- transl_function f; - if zlt Int.max_unsigned (list_length_z c) + OK (mkfunction f.(Mach.fn_sig) + (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + Pmflr GPR0 :: + Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c)). + +Definition transf_function (f: Mach.function) : res Asm.function := + do tf <- transl_function f; + if zlt Int.max_unsigned (list_length_z tf.(fn_code)) then Error (msg "code size exceeded") - else OK c. + else OK tf. Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 990d35d..5c99231 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -79,9 +79,9 @@ Qed. Lemma transf_function_no_overflow: forall f tf, - transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned. + transf_function f = OK tf -> list_length_z tf.(fn_code) <= Int.max_unsigned. Proof. - intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0. omega. Qed. @@ -316,11 +316,11 @@ Lemma transl_find_label: forall lbl f tf, transf_function f = OK tf -> match Mach.find_label lbl f.(Mach.fn_code) with - | None => find_label lbl tf = None - | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc + | None => find_label lbl tf.(fn_code) = None + | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc end. Proof. - intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. + intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. rewrite transl_code'_transl_code in EQ0. simpl. eapply transl_code_label; eauto. Qed. @@ -364,7 +364,7 @@ Proof. - intros. exploit transl_instr_label; eauto. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. - destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. monadInv EQ. + destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. rewrite transl_code'_transl_code in EQ0. exists x; exists false; split; auto. unfold fn_code. repeat constructor. - exact transf_function_no_overflow. @@ -607,7 +607,7 @@ Opaque loadind. - (* Mcall *) assert (f0 = f) by congruence. subst f0. inv AT. - assert (NOOV: list_length_z tf <= Int.max_unsigned). + assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. destruct ros as [rf|fid]; simpl in H; monadInv H5. + (* Indirect call *) @@ -652,7 +652,7 @@ Opaque loadind. - (* Mtailcall *) assert (f0 = f) by congruence. subst f0. inversion AT; subst. - assert (NOOV: list_length_z tf <= Int.max_unsigned). + assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. @@ -672,9 +672,9 @@ Opaque loadind. set (rs6 := rs5#PC <- (rs5 CTR)). assert (exec_straight tge tf (Pmtctr x0 :: Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 - :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr :: x) + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr sig :: x) rs0 m'0 - (Pbctr :: x) rs5 m2'). + (Pbctr sig :: x) rs5 m2'). apply exec_straight_step with rs2 m'0. simpl. rewrite H9. auto. auto. apply exec_straight_step with rs3 m'0. @@ -713,9 +713,9 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. set (rs5 := rs4#PC <- (Vptr f' Int.zero)). assert (exec_straight tge tf (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 - :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid :: x) + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid sig :: x) rs0 m'0 - (Pbs fid :: x) rs4 m2'). + (Pbs fid sig :: x) rs4 m2'). apply exec_straight_step with rs2 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite <- (sp_val _ _ _ AG). simpl. rewrite C. auto. congruence. auto. @@ -851,7 +851,7 @@ Local Transparent destroyed_by_jumptable. - (* Mreturn *) assert (f0 = f) by congruence. subst f0. inversion AT; subst. - assert (NOOV: list_length_z tf <= Int.max_unsigned). + assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. @@ -900,7 +900,7 @@ Local Transparent destroyed_by_jumptable. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Int.max_unsigned (list_length_z x0)); inversion EQ1. clear EQ1. + destruct (zlt Int.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. @@ -916,9 +916,9 @@ Local Transparent destroyed_by_jumptable. set (rs4 := nextinstr rs3). assert (EXEC_PROLOGUE: exec_straight tge x - x rs0 m' + x.(fn_code) rs0 m' x1 rs4 m3'). - rewrite <- H5 at 2. + rewrite <- H5 at 2. simpl. apply exec_straight_three with rs2 m2' rs3 m2'. unfold exec_instr. rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite F. auto. @@ -928,11 +928,11 @@ Local Transparent destroyed_by_jumptable. rewrite Int.add_zero_l. simpl in P. rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. congruence. auto. auto. auto. left; exists (State rs4 m3'); split. - eapply exec_straight_steps_1; eauto. unfold fn_code; omega. constructor. + eapply exec_straight_steps_1; eauto. omega. constructor. econstructor; eauto. change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). rewrite ATPC. simpl. constructor; eauto. - subst x. unfold fn_code. eapply code_tail_next_int. omega. + subst x; simpl in g. unfold fn_code. eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. constructor. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index d9b6cf3..e637ef8 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -183,7 +183,7 @@ Ltac Simpl := repeat Simplif. Section CONSTRUCTORS. Variable ge: genv. -Variable fn: code. +Variable fn: function. (** Properties of comparisons. *) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 764020a..87d22f2 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -668,9 +668,9 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " andis. %a, %a, %a\n" ireg r1 ireg r2 constant c | Pb lbl -> fprintf oc " b %a\n" label (transl_label lbl) - | Pbctr -> + | Pbctr sg -> fprintf oc " bctr\n" - | Pbctrl -> + | Pbctrl sg -> fprintf oc " bctrl\n" | Pbf(bit, lbl) -> if !Clflags.option_faligncondbranchs > 0 then @@ -683,9 +683,9 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " b %a\n" label (transl_label lbl); fprintf oc "%a:\n" label next end - | Pbl s -> + | Pbl(s, sg) -> fprintf oc " bl %a\n" symbol s - | Pbs s -> + | Pbs(s, sg) -> fprintf oc " b %a\n" symbol s | Pblr -> fprintf oc " blr\n" @@ -930,7 +930,7 @@ let print_instruction oc tbl pc fallthrough = function let instr_fall_through = function | Pb _ -> false - | Pbctr -> false + | Pbctr _ -> false | Pbs _ -> false | Pblr -> false | _ -> true @@ -1008,7 +1008,7 @@ let print_jumptable oc (lbl, tbl) = (fun l -> fprintf oc " .long %a\n" label (transl_label l)) tbl -let print_function oc name code = +let print_function oc name fn = Hashtbl.clear current_function_labels; float_literals := []; jumptables := []; @@ -1025,7 +1025,8 @@ let print_function oc name code = fprintf oc "%a:\n" symbol name; print_location oc (C2C.atom_location name); cfi_startproc oc; - print_instructions oc (label_positions PTree.empty 0 code) 0 true code; + print_instructions oc (label_positions PTree.empty 0 fn.fn_code) + 0 true fn.fn_code; cfi_endproc oc; fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name; diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml index fabac33..49c0774 100644 --- a/powerpc/Unusedglob1.ml +++ b/powerpc/Unusedglob1.ml @@ -31,8 +31,8 @@ let referenced_builtin ef = | _ -> [] let referenced_instr = function - | Pbl s -> [s] - | Pbs s -> [s] + | Pbl(s, _) -> [s] + | Pbs(s, _) -> [s] | Paddi(_, _, c) | Paddic(_, _, c) | Paddis(_, _, c) @@ -60,4 +60,4 @@ let referenced_instr = function | Pbuiltin(ef, _, _) -> referenced_builtin ef | _ -> [] -let code_of_function f = f +let code_of_function f = f.fn_code -- cgit v1.2.3