Updating the PowerPC and ARM ports.

PowerPC: always use full register names to print annotations.

12 files changed, 92 insertions, 96 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.
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index de4b87fb..5a3a48e1 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -695,14 +695,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)
@@ -737,7 +729,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/arm/Asmgenproof.v b/arm/Asmgenproof.v
index c687722c..6d9b134f 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -771,13 +771,16 @@ Opaque loadind.
   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/arm/SelectOp.vp b/arm/SelectOp.vp
index 6102d82d..fea99ef5 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -489,3 +489,16 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (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 (Ainstack ofs) Enil => AA_loadstack chunk ofs
+  | _ => AA_base e
+  end.
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index c68d2277..d3c3239a 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -864,4 +864,19 @@ Proof.
   exists (v :: nil); split. eauto with evalexpr. subst. simpl. 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.
+- constructor; auto.
+Qed.
+
 End CMCONSTR.
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 =