Merge branch 'master' into dwarf

8 files changed, 62 insertions, 62 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 15f80e42..b67c3cc5 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -212,11 +212,7 @@ Inductive instruction: Type :=
   | Pallocframe(sz: Z)(ofs_ra ofs_link: int)
   | Pfreeframe(sz: Z)(ofs_ra ofs_link: int)
   | Pbuiltin(ef: external_function)(args: list preg)(res: list preg)
-  | Pannot(ef: external_function)(args: list annot_param)
-
-with annot_param : Type :=
-  | APreg: preg -> annot_param
-  | APstack: memory_chunk -> Z -> annot_param.
+  | Pannot(ef: external_function)(args: list (annot_arg preg)).
 
 Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
@@ -798,20 +794,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 ESP) = 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 :=
@@ -840,8 +822,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 ESP) m args vargs ->
+      external_call ef ge vargs m t v m' ->
       step (State rs m) t
            (State (nextinstr rs) m')
   | exec_step_external:
@@ -893,16 +875,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 :=
@@ -912,32 +884,32 @@ Ltac Equalities :=
   | _ => idtac
   end.
   intros; constructor; simpl; intros.
-(* determ *)
+- (* determ *)
   inv H; inv H0; Equalities.
-  split. constructor. auto.
-  discriminate.
-  discriminate.
-  inv H11. 
-  exploit external_call_determ'. eexact H4. eexact H9. intros [A B].
++ split. constructor. auto.
++ discriminate.
++ discriminate.
++ inv H11. 
++ 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].
++ inv H12.
++ 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.
++ assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
   exploit external_call_determ'. eexact H4. eexact H9. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
-(* trace length *)
+- (* trace length *)
   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 H3. eapply external_call_trace_length; eauto.
-(* initial states *)
+- (* initial states *)
   inv H; inv H0. f_equal. congruence.
-(* final no step *)
+- (* final no step *)
   inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence.
-(* final states *)
+- (* final states *)
   inv H; inv H0. congruence.
 Qed.
 
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 9c0a76e0..2c1afc11 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -492,14 +492,6 @@ Definition transl_store (chunk: memory_chunk)
       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)
@@ -546,7 +538,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   | Mbuiltin ef args res =>
       OK (Pbuiltin ef (List.map preg_of args) (List.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)
   end.
 
 (** Translation of a code sequence *)
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index 57d7de4a..3570da2e 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -700,13 +700,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/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 7d71d1a2..0ca343fb 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -462,12 +462,14 @@ Proof.
   rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
   destruct (Int.ltu i i0); reflexivity.
 (* int ptr *)
-  destruct (Int.eq i Int.zero) eqn:?; try discriminate.
+  destruct (Int.eq i Int.zero &&
+    (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
   rewrite Heqb1; reflexivity. 
   rewrite Heqb1; reflexivity.
 (* ptr int *)
-  destruct (Int.eq i0 Int.zero) eqn:?; try discriminate.
+  destruct (Int.eq i0 Int.zero &&
+    (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
   rewrite Heqb1; reflexivity. 
   rewrite Heqb1; reflexivity.
diff --git a/ia32/Op.v b/ia32/Op.v
index 846d094f..ecc67c46 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -647,6 +647,7 @@ Definition is_trivial_op (op: operation) : bool :=
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
   | Ocmp (Ccompu _) => true
+  | Ocmp (Ccompuimm _ _) => true
   | _ => false
   end.
 
@@ -656,7 +657,7 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence.
-  destruct c; simpl; try congruence. reflexivity. 
+  destruct c; simpl; auto; congruence.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index b6aef725..74e3fbd7 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -507,3 +507,17 @@ 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 (Olea (Aglobal id ofs)) Enil => AA_addrglobal id ofs
+  | Eop (Olea (Ainstack 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/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 50688621..50f0d9b6 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -898,4 +898,20 @@ Proof.
   exists (v :: nil); split. constructor; auto. constructor. 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.
+- inv H. InvEval. simpl in H6. inv H6. constructor; auto.
+- constructor; auto.
+Qed.
+
 End CMCONSTR.
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 71e6cba6..92be0ff3 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -339,7 +339,7 @@ module Target(System: SYSTEM):TARGET =
           (int_of_string (Str.matched_group 2 txt))
       end else begin
         fprintf oc "%s annotation: " comment;
-        PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args
+        PrintAnnot.print_annot_stmt preg "%esp" oc txt targs args
       end
 
     let print_annot_val oc txt args res =