Cleanup

1 files changed, 21 insertions, 81 deletions

diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 1abcb570..0b1123f7 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -188,16 +188,6 @@ Proof.
   apply is_label_correct_false. simpl. auto.
 Qed.
 
-(*
-Lemma transl_is_label2:
-  forall f bb ep tbb1 tbb2 lbl,
-  transl_block f bb ep = OK (tbb1::tbb2::nil) ->
-     is_label lbl tbb1 = MB.is_label lbl bb
-  /\ is_label lbl tbb2 = false.
-Proof.
-  intros. split. eapply transl_is_label; eauto. eapply transl_is_label_false2; eauto.
-Qed. *)
-
 Lemma transl_block_nonil:
   forall f c ep tc,
   transl_block f c ep = OK tc ->
@@ -285,6 +275,7 @@ Proof.
 Qed.
 
 End TRANSL_LABEL.
+
 (** A valid branch in a piece of Machblock code translates to a valid ``go to''
   transition in the generated Asmblock code. *)
 
@@ -808,38 +799,33 @@ Proof.
             + intro r. destruct r; apply V; auto.
           - eauto with asmgen. }
         { rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H11. auto. }
-    + (* MBbuiltin (contradiction) *)
+    + (* MBbuiltin *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
       
       assert (f0 = f) by congruence. subst f0.
       assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
-        eapply transf_function_no_overflow; eauto.
-        generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
-        remember (Ptrofs.add _ _) as ofs'.
-  assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
-          econstructor; eauto.
- (*        exploit return_address_offset_correct; eauto. intros; subst ra.
-        repeat eexists.
-        econstructor; eauto. econstructor. *)
+      eapply transf_function_no_overflow; eauto.
+      generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
+      remember (Ptrofs.add _ _) as ofs'.
+      assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
+      econstructor; eauto.
       
       monadInv TBC. monadInv TIC. inv H0.
       
-      
-exploit builtin_args_match; eauto. intros [vargs' [P Q]].
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2' [A [B [C D]]]]].
-  
+      exploit builtin_args_match; eauto. intros [vargs' [P Q]].
+      exploit external_call_mem_extends; eauto.
+      intros [vres' [m2' [A [B [C D]]]]].
   
-  repeat eexists. econstructor. erewrite <- sp_val by eauto.
-  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-  eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto.
-  econstructor; eauto.
-  unfold incrPC. rewrite Pregmap.gss.
-  rewrite set_res_other. rewrite undef_regs_other_2. unfold Val.offset_ptr. rewrite PCeq.
-  eauto. rewrite preg_notin_charact. intros. auto with asmgen.
-  auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
-  intros. discriminate.
+      repeat eexists. econstructor. erewrite <- sp_val by eauto.
+      eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+      eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto.
+      econstructor; eauto.
+      unfold incrPC. rewrite Pregmap.gss.
+      rewrite set_res_other. rewrite undef_regs_other_2. unfold Val.offset_ptr. rewrite PCeq.
+      eauto. rewrite preg_notin_charact. intros. auto with asmgen.
+      auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto.
+      eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
+      intros. discriminate.
     + (* MBgoto *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
       inv TBC. inv TIC. inv H0.
@@ -1373,52 +1359,6 @@ Proof.
   - econstructor.
 Qed.
 
-(* Theorem step_simulation_builtin:
-  forall t sf f sp bb bb' bb'' rs m rs' m' s'' c ef args res S1,
-  bb' = mb_remove_header bb ->
-  body_step ge sf f sp (Machblock.body bb') rs m rs' m' ->
-  bb'' = mb_remove_body bb' ->
-  MB.exit bb = Some (MBbuiltin ef args res) ->
-  exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') t s'' ->
-  match_states (Machblock.State sf f sp (bb :: c) rs m) S1 ->
-  exists S2 : state, plus (step lk) tge S1 E0 S2 /\ match_states s'' S2.
-Proof.
-  intros until S1. intros Hbb' BSTEP Hbb'' Hexit ESTEP MS.
-  inv MS. inv AT. monadInv H2. monadInv EQ.
-  rewrite Hexit in EQ0. monadInv EQ0. simpl in ESTEP.
-  rewrite Hexit in ESTEP. inv ESTEP. inv H4.
-
-  exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H1); intro NOOV.
-  exploit builtin_args_match; eauto. intros [vargs' [P Q]].
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2' [A [B [C D]]]]].
-  econstructor; split. apply plus_one.
-  simpl in H3.
-  eapply exec_step_internal. eauto. eauto.
-    eapply find_bblock_tail; eauto.
-    destruct (x3 @@ nil).
-    - eauto.
-    - eauto.
-    simpl. eauto. eexists. simpl. split; eauto.
-    econstructor.
-    erewrite <- sp_val by eauto.
-    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eauto.
-    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-    eauto.
-  econstructor; eauto.
-    instantiate (2 := tf); instantiate (1 := x0).
-    unfold incrPC. rewrite Pregmap.gss.
-    rewrite set_res_other. rewrite undef_regs_other_2.
-    rewrite <- H. simpl. econstructor; eauto.
-    eapply code_tail_next_int; eauto.
-    rewrite preg_notin_charact. intros. auto with asmgen.
-    auto with asmgen.
-    apply agree_nextblock. eapply agree_set_res; auto.
-    eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
-    congruence.
-Qed. *)
-
 (* Measure to prove finite stuttering, see the other backends *)
 Definition measure (s: MB.state) : nat :=
   match s with
@@ -1591,4 +1531,4 @@ Proof.
   - exact step_simulation.
 Qed.
 
-End PRESERVATION.
\ No newline at end of file
+End PRESERVATION.