Updating the PowerPC and ARM ports.

PowerPC: always use full register names to print annotations.

1 files changed, 6 insertions, 34 deletions

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.