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 --- ia32/Asm.v | 55 ++++++++++++++++++++++++++--------------------------- ia32/Asmgen.v | 21 ++++++++++++-------- ia32/Asmgenproof.v | 34 ++++++++++++++++----------------- ia32/Asmgenproof1.v | 2 +- ia32/PrintAsm.ml | 12 ++++++------ ia32/Unusedglob1.ml | 6 +++--- 6 files changed, 67 insertions(+), 63 deletions(-) (limited to 'ia32') diff --git a/ia32/Asm.v b/ia32/Asm.v index 78c4c3ba..7bd17552 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 04100574..740dff8c 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 df09ca7f..fa8ce6c6 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 9ddc4639..5d3df679 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 4480f91a..3badbfc0 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 fe962e26..8332a30c 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 -- cgit