Some progress in Asmblockgenproof

1 files changed, 171 insertions, 2 deletions

diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 4a35485e..a47654b8 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -167,6 +167,15 @@ Proof.
   red; intros; elim n. eapply preg_of_injective; eauto.
 Qed.
 
+Corollary agree_set_mreg_parallel:
+  forall ms sp rs r v v',
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs).
+Proof.
+  intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto.
+Qed.
+
 Lemma agree_set_other:
   forall ms sp rs r v,
   agree ms sp rs ->
@@ -184,6 +193,18 @@ Proof.
   intros. unfold incrPC. apply agree_set_other. auto. auto.
 Qed.
 
+Lemma agree_set_pair:
+  forall sp p v v' ms rs,
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs).
+Proof.
+  intros. destruct p; simpl.
+- apply agree_set_mreg_parallel; auto.
+- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
+  apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
+Qed.
+
 Lemma agree_set_res:
   forall res ms sp rs v v',
   agree ms sp rs ->
@@ -230,6 +251,23 @@ Proof.
   intros. rewrite Pregmap.gso; auto.
 Qed.
 
+Lemma agree_undef_caller_save_regs:
+  forall ms sp rs,
+  agree ms sp rs ->
+  agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs).
+Proof.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split.
+- unfold proj_sumbool; rewrite dec_eq_true. auto.
+- auto.
+- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
+  destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
++ apply list_in_map_inv in i. destruct i as (mr & A & B). 
+  assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
+  apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
++ destruct (is_callee_save r) eqn:CS; auto.
+  elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
+Qed.
+
 Lemma agree_change_sp:
   forall ms sp rs sp',
   agree ms sp rs -> sp' <> Vundef ->
@@ -262,6 +300,62 @@ Proof.
   exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto.
 Qed.
 
+(** Connection between Mach and Asm calling conventions for external
+    functions. *)
+
+Lemma extcall_arg_match:
+  forall ms sp rs m m' l v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Mach.extcall_arg ms m sp l v ->
+  exists v', extcall_arg rs m' l v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1.
+  exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto.
+  unfold Mach.load_stack in H2.
+  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
+  rewrite (sp_val _ _ _ H) in A.
+  exists v'; split; auto.
+  econstructor. eauto. assumption.
+Qed.
+
+Lemma extcall_arg_pair_match:
+  forall ms sp rs m m' p v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Mach.extcall_arg_pair ms m sp p v ->
+  exists v', extcall_arg_pair rs m' p v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1.
+- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto.
+- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1).
+  exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2).
+  exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto.
+Qed.
+
+Lemma extcall_args_match:
+  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall ll vl,
+  list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl ->
+  exists vl', list_forall2 (extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; intros.
+  exists (@nil val); split. constructor. constructor.
+  exploit extcall_arg_pair_match; eauto. intros [v1' [A B]].
+  destruct IHlist_forall2 as [vl' [C D]].
+  exists (v1' :: vl'); split; constructor; auto.
+Qed.
+
+Lemma extcall_arguments_match:
+  forall ms m m' sp rs sg args,
+  agree ms sp rs -> Mem.extends m m' ->
+  Mach.extcall_arguments ms m sp sg args ->
+  exists args', extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
+Proof.
+  unfold Mach.extcall_arguments, extcall_arguments; intros.
+  eapply extcall_args_match; eauto.
+Qed.
+
 Lemma set_res_other:
   forall r res v rs,
   data_preg r = false ->
@@ -639,9 +733,36 @@ Proof.
   intros. apply exec_straight_opt_intro. eapply exec_straight_opt_step; eauto.
 Qed.
 
+(** Like exec_straight predicate, but on blocks *)
+
+Inductive exec_straight_blocks: bblocks -> regset -> mem ->
+                                bblocks -> regset -> mem -> Prop :=
+  | exec_straight_blocks_one:
+      forall b1 c rs1 m1 rs2 m2,
+      exec_bblock lk ge fn b1 rs1 m1 E0 rs2 m2 ->
+      rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b1)) ->
+      exec_straight_blocks (b1 :: c) rs1 m1 c rs2 m2
+  | exec_straight_blocks_step:
+      forall b c rs1 m1 rs2 m2 c' rs3 m3,
+      exec_bblock lk ge fn b rs1 m1 E0 rs2 m2 ->
+      rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b)) ->
+      exec_straight_blocks c rs2 m2 c' rs3 m3 ->
+      exec_straight_blocks (b :: c) rs1 m1 c' rs3 m3.
+
+Lemma exec_straight_blocks_trans:
+  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
+  exec_straight_blocks c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight_blocks c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight_blocks c1 rs1 m1 c3 rs3 m3.
+Proof.
+  induction 1; intros.
+  eapply exec_straight_blocks_step; eauto.
+  eapply exec_straight_blocks_step; eauto.
+Qed.
+
 (** Linking exec_straight with exec_straight_blocks *)
 
-(* Lemma exec_straight_pc:
+Lemma exec_straight_pc:
   forall c c' rs1 m1 rs2 m2,
   exec_straight c rs1 m1 c' rs2 m2 ->
   rs2 PC = rs1 PC.
@@ -651,7 +772,7 @@ Proof.
   - eapply exec_basic_instr_pc; eauto.
   - rewrite (IHc c' rs3 m3 rs2 m2); auto.
     erewrite exec_basic_instr_pc; eauto.
-Qed. *)
+Qed.
 
 Lemma exec_body_pc:
   forall ge l rs1 m1 rs2 m2,
@@ -667,6 +788,54 @@ Proof.
     erewrite exec_basic_instr_pc; eauto.
 Qed.
 
+(** The following lemmas show that straight-line executions
+  (predicate [exec_straight_blocks]) correspond to correct Asm executions. *)
+
+Lemma exec_straight_steps_1:
+  forall c rs m c' rs' m',
+  exec_straight_blocks c rs m c' rs' m' ->
+  size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned ->
+  forall b ofs,
+  rs#PC = Vptr b ofs ->
+  Genv.find_funct_ptr ge b = Some (Internal fn) ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c ->
+  plus (step lk) ge (State rs m) E0 (State rs' m').
+Proof.
+  induction 1; intros.
+  apply plus_one.
+  econstructor; eauto.
+  eapply find_bblock_tail. eauto.
+  eapply plus_left'.
+  econstructor; eauto.
+  eapply find_bblock_tail. eauto.
+  apply IHexec_straight_blocks with b0 (Ptrofs.add ofs (Ptrofs.repr (size b))).
+  auto. rewrite H0. rewrite H3. reflexivity.
+  auto.
+  apply code_tail_next_int; auto.
+  traceEq.
+Qed.
+
+Lemma exec_straight_steps_2:
+  forall c rs m c' rs' m',
+  exec_straight_blocks c rs m c' rs' m' ->
+  size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned ->
+  forall b ofs,
+  rs#PC = Vptr b ofs ->
+  Genv.find_funct_ptr ge b = Some (Internal fn) ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c ->
+  exists ofs',
+     rs'#PC = Vptr b ofs'
+  /\ code_tail (Ptrofs.unsigned ofs') (fn_blocks fn) c'.
+Proof.
+  induction 1; intros.
+  exists (Ptrofs.add ofs (Ptrofs.repr (size b1))). split.
+  rewrite H0. rewrite H2. auto.
+  apply code_tail_next_int; auto.
+  apply IHexec_straight_blocks with (Ptrofs.add ofs (Ptrofs.repr (size b))).
+  auto. rewrite H0. rewrite H3. reflexivity. auto.
+  apply code_tail_next_int; auto.
+Qed.
+
 End STRAIGHTLINE.
 
 (** * Properties of the Machblock call stack *)