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. --- arm/Asm.v | 40 ++++++---------------------------------- 1 file changed, 6 insertions(+), 34 deletions(-) (limited to 'arm/Asm.v') diff --git a/arm/Asm.v b/arm/Asm.v index 0790c6f2..2a120dd4 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -204,11 +204,7 @@ Inductive instruction : Type := | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function *) - | Pannot: external_function -> list annot_param -> instruction (**r annotation statement *) - -with annot_param : Type := - | APreg: preg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Pannot: external_function -> list (annot_arg preg) -> instruction. (**r annotation statement *) (** The pseudo-instructions are the following: @@ -766,20 +762,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 IR13) = 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 := @@ -808,8 +790,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) (fn_code f) = 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 SP) m args vargs -> + external_call ef ge vargs m t v m' -> step (State rs m) t (State (nextinstr rs) m') | exec_step_external: forall b ef args res rs m t rs' m', @@ -860,16 +842,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 := @@ -888,8 +860,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]. @@ -898,7 +870,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. -- cgit