From e11b3b885a6d359925b86743b89698cc6757157a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 27 Mar 2015 15:28:20 +0100 Subject: Updating the PowerPC and ARM ports. PowerPC: always use full register names to print annotations. --- powerpc/Asm.v | 42 +++++++----------------------------------- powerpc/Asmexpand.ml | 2 +- powerpc/Asmgen.v | 10 +--------- powerpc/Asmgenproof.v | 9 ++++++--- powerpc/SelectOp.vp | 15 +++++++++++++++ powerpc/SelectOpproof.v | 16 ++++++++++++++++ powerpc/TargetPrinter.ml | 7 +++++-- 7 files changed, 51 insertions(+), 50 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 18316fb0..d707b2b5 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -276,13 +276,9 @@ Inductive instruction : Type := | Pxoris: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate high *) | Plabel: label -> instruction (**r define a code label *) | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function (pseudo) *) - | Pannot: external_function -> list annot_param -> instruction (**r annotation statement (pseudo) *) + | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement (pseudo) *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) - | Pcfi_rel_offset: int -> instruction (**r .cfi_rel_offset lr debug directive *) - -with annot_param : Type := - | APreg: preg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Pcfi_rel_offset: int -> instruction. (**r .cfi_rel_offset lr debug directive *) (** The pseudo-instructions are the following: @@ -936,20 +932,6 @@ Definition extcall_arguments Definition loc_external_result (sg: signature) : list preg := map preg_of (loc_result sg). -(** Extract the values of the arguments of an annotation. *) - -Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop := - | annot_arg_reg: forall r, - annot_arg rs m (APreg r) (rs r) - | annot_arg_stack: forall chunk ofs stk base v, - rs (IR GPR1) = Vptr stk base -> - Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> - annot_arg rs m (APstack chunk ofs) v. - -Definition annot_arguments - (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop := - list_forall2 (annot_arg rs m) params args. - (** Execution of the instruction at [rs#PC]. *) Inductive state: Type := @@ -978,8 +960,8 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> 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' -> + eval_annot_args ge rs (rs GPR1) m args vargs -> + external_call ef ge vargs m t v m' -> step (State rs m) t (State (nextinstr rs) m') | exec_step_external: @@ -1031,16 +1013,6 @@ Proof. intros. red in H0; red in H1. eauto. Qed. -Remark annot_arguments_determ: - forall rs m params args1 args2, - annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. -Proof. - unfold annot_arguments. intros. revert params args1 H args2 H0. - induction 1; intros. - inv H0; auto. - inv H1. decEq; eauto. inv H; inv H4. auto. congruence. -Qed. - Lemma semantics_determinate: forall p, determinate (semantics p). Proof. Ltac Equalities := @@ -1059,8 +1031,8 @@ Ltac Equalities := exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. inv H12. - assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. - exploit external_call_determ'. eexact H5. eexact H13. intros [A B]. + assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. @@ -1069,7 +1041,7 @@ Ltac Equalities := red; intros. inv H; simpl. omega. inv H3; eapply external_call_trace_length; eauto. - inv H4; eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. inv H2; eapply external_call_trace_length; eauto. (* initial states *) inv H; inv H0. f_equal. congruence. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index c003bcd1..47895cb1 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -74,7 +74,7 @@ let _m8 = coqint_of_camlint (-8l) (* Handling of annotations *) let expand_annot_val txt targ args res = - emit (Pannot(EF_annot(txt, [AA_arg targ]), List.map (fun r -> APreg r) args)); + emit (Pannot(EF_annot(txt, [targ]), List.map (fun r -> AA_base r) args)); begin match args, res with | [IR src], [IR dst] -> if dst <> src then emit (Pmr(dst, src)) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 2bd69d91..7ee6c770 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -610,14 +610,6 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) Error (msg "Asmgen.transl_store") end. -(** Translation of arguments to annotations *) - -Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param := - match p with - | Mach.APreg r => APreg (preg_of r) - | Mach.APstack chunk ofs => APstack chunk ofs - end. - (** Translation of a Mach instruction. *) Definition transl_instr (f: Mach.function) (i: Mach.instruction) @@ -658,7 +650,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mbuiltin ef args res => OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) | Mannot ef args => - OK (Pannot ef (map transl_annot_param args) :: k) + OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) | Mlabel lbl => OK (Plabel lbl :: k) | Mgoto lbl => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index c7439c3d..27b32ba1 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -778,13 +778,16 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. inv AT. monadInv H4. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends'; eauto. + exploit annot_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. - eapply external_call_symbols_preserved'; eauto. + erewrite <- sp_val by eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. + exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 70b1feb6..618643b8 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -523,3 +523,18 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) | _ => (Aindexed Int.zero, e:::Enil) end. + +(** ** Arguments of annotations *) + +Nondetfunction annot_arg (e: expr) := + match e with + | Eop (Ointconst n) Enil => AA_int n + | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs + | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + AA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) + | Eload chunk (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs + | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs + | _ => AA_base e + end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 8311b82c..c51b650b 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -999,5 +999,21 @@ Proof. rewrite Int.add_zero. auto. Qed. +Theorem eval_annot_arg: + forall a v, + eval_expr ge sp e m nil a v -> + CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. +Proof. + intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. +- constructor. +- constructor. +- constructor. +- simpl in H5. inv H5. constructor. +- subst v. constructor; auto. +- inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- inv H. InvEval. simpl in H6. inv H6. constructor; auto. +- constructor; auto. +Qed. + End CMCONSTR. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 70aec6c0..7e460f46 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -234,9 +234,12 @@ module Target (System : SYSTEM):TARGET = let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r + (* [preg] is only used for printing annotations. + Use the full register names [rN] and [fN] to avoid + ambiguity with constants. *) let preg oc = function - | IR r -> ireg oc r - | FR r -> freg oc r + | IR r -> fprintf oc "r%s" (int_reg_name r) + | FR r -> fprintf oc "f%s" (float_reg_name r) | _ -> assert false let section oc sec = -- cgit