Merge remote-tracking branch 'origin/mppa-work' into mppa-msub

4 files changed, 88 insertions, 67 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 71af4798..941796cd 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -1155,10 +1155,11 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep:
   end
 .
 
-Definition make_prologue (f:  Machblock.function) lb :=
-  (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
-         Pget GPRA RA ::b
-         storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::b lb).
+Program Definition make_prologue (f:  Machblock.function) lb :=
+  ({| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::i
+         Pget GPRA RA ::i
+         storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::i nil;
+      exit := None |} :: lb).
 
 Definition transl_function (f: Machblock.function) :=
   do lb <- transl_blocks f f.(Machblock.fn_code) true;
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 0233a3dc..c44ef3ff 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -17,6 +17,7 @@ Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.

 Require Import Op Locations Machblock Conventions Asmblock.

 Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1.

+Require Import Axioms.

 

 Module MB := Machblock.

 Module AB := Asmvliw.

@@ -1100,7 +1101,7 @@ Proof.
     destruct ep eqn:EPeq.

   (* RTMP contains parent *)

     + exploit loadind_correct. eexact EQ1.

-      instantiate (2 := rs1). rewrite DXP; eauto. congruence.

+      instantiate (2 := rs1). rewrite DXP; eauto.

       intros [rs2 [P [Q R]]].

 

       eapply exec_straight_body in P.

@@ -1121,8 +1122,8 @@ Proof.
 

   (* GPR11 does not contain parent *)

     + rewrite chunk_of_Tptr in A. 

-      exploit loadind_ptr_correct. eexact A. congruence. intros [rs2 [P [Q R]]].

-      exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto. congruence.

+      exploit loadind_ptr_correct. eexact A. intros [rs2 [P [Q R]]].

+      exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto.

       intros [rs3 [S [T U]]].

 

       exploit exec_straight_trans.

@@ -1593,6 +1594,12 @@ Proof.
     congruence.

 Qed.

 

+Lemma next_sep:

+  forall rs m rs' m', rs = rs' -> m = m' -> Next rs m = Next rs' m'.

+Proof.

+  congruence.

+Qed.

+

 Theorem step_simulation:

   forall S1 t S2, MB.step return_address_offset ge S1 t S2 ->

   forall S1' (MS: match_states S1 S1'),

@@ -1648,55 +1655,58 @@ Proof.
   intros [m3' [P Q]].

   (* Execution of function prologue *)

   monadInv EQ0. (* rewrite transl_code'_transl_code in EQ1. *)

-  set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::b

-                 Pget GPRA RA ::b

-                 storeind_ptr GPRA SP (fn_retaddr_ofs f) ::b x0) in *.

+  set (tfbody := make_prologue f x0) in *.

   set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.

-  set (rs2 := nextblock (bblock_single_inst (Pallocframe (fn_stacksize f) (fn_link_ofs f))) 

-                          (rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef)).

+  set (rs2 := rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef).

   exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto.

   intros (rs' & U' & V').

-  exploit (exec_straight_through_singleinst); eauto.

-  intro W'. remember (nextblock _ rs') as rs''.

-  exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs'' m2').

+(*   exploit (exec_straight_through_singleinst); eauto.

+  intro W'. remember (nextblock _ rs') as rs''. *)

+  exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2').

     rewrite chunk_of_Tptr in P.

     assert (rs' GPRA = rs0 RA). { apply V'. }

-    assert (rs'' GPRA = rs' GPRA). { subst. Simpl. }

     assert (rs' SP = rs2 SP). { apply V'; discriminate. }

-    assert (rs'' SP = rs' SP). { subst. Simpl. }

-    rewrite H4. rewrite H3. rewrite H6. rewrite H5.

+    rewrite H4. rewrite H3.

     (* change (rs' GPRA) with (rs0 RA). *)

     rewrite ATLR.

     change (rs2 SP) with sp. eexact P.

-    congruence. congruence.

   intros (rs3 & U & V).

-  exploit (exec_straight_through_singleinst); eauto.

-  intro W.

-  remember (nextblock _ rs3) as rs3'.

-  assert (EXEC_PROLOGUE:

+(*   exploit (exec_straight_through_singleinst); eauto.

+  intro W. *)

+  assert (EXEC_PROLOGUE: exists rs3',

             exec_straight_blocks tge tf

               tf.(fn_blocks) rs0 m'

-              x0 rs3' m3').

-  { change (fn_blocks tf) with tfbody; unfold tfbody.

-    apply exec_straight_blocks_step with rs2 m2'.

-    unfold exec_bblock. simpl exec_body. rewrite C. fold sp. simpl exec_control.

-    rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. rewrite regset_same_assign. reflexivity.

-    reflexivity.

-    eapply exec_straight_blocks_trans.

-    - eexact W'.

-    - eexact W. }

+              x0 rs3' m3'

+          /\ forall r, r <> PC -> rs3' r = rs3 r).

+  { eexists. split.

+    - change (fn_blocks tf) with tfbody; unfold tfbody.

+      econstructor; eauto. unfold exec_bblock. simpl exec_body.

+      rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F.

+      Simpl. unfold parexec_store_offset. rewrite Ptrofs.of_int64_to_int64. unfold eval_offset.

+      rewrite chunk_of_Tptr in P. Simpl. rewrite ATLR. unfold Mptr in P. assert (Archi.ptr64 = true) by auto. 2: auto. rewrite H3 in P. rewrite P.

+      simpl. apply next_sep; eauto. reflexivity.

+    - intros. destruct V' as (V'' & V'). destruct r.

+      + Simpl.

+        destruct (gpreg_eq g0 GPR16). { subst. Simpl. rewrite V; try discriminate. rewrite V''. subst rs2. Simpl. }

+        destruct (gpreg_eq g0 GPR32). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }

+        destruct (gpreg_eq g0 GPR12). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }

+        destruct (gpreg_eq g0 GPR17). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }

+        Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. { destruct g0; try discriminate. contradiction. }

+      + Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl.

+      + contradiction.

+  } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').

   exploit exec_straight_steps_2; eauto using functions_transl.

-  simpl fn_blocks. unfold make_prologue in g. simpl fn_blocks in g. unfold tfbody. simpl bblock_single_inst. omega. constructor.

+  simpl fn_blocks. simpl fn_blocks in g. omega. constructor.

   intros (ofs' & X & Y).                    

   left; exists (State rs3' m3'); split.

   eapply exec_straight_steps_1; eauto.

-  simpl fn_blocks. unfold make_prologue in g. simpl fn_blocks in g. unfold tfbody. simpl bblock_single_inst. omega.

+  simpl fn_blocks. simpl fn_blocks in g. omega.

   constructor.

   econstructor; eauto.

   rewrite X; econstructor; eauto. 

   apply agree_exten with rs2; eauto with asmgen.

   unfold rs2. 

-  apply agree_nextblock. apply agree_set_other; auto with asmgen.

+  apply agree_set_other; auto with asmgen.

   apply agree_change_sp with (parent_sp s). 

   apply agree_undef_regs with rs0. auto.

 Local Transparent destroyed_at_function_entry.

@@ -1705,17 +1715,17 @@ Local Transparent destroyed_at_function_entry.
 

   intros.

   assert (r <> RTMP). { contradict H3; rewrite H3; unfold data_preg; auto. }

-  rewrite Heqrs3'. Simpl. rewrite V. rewrite Heqrs''. Simpl. inversion V'. rewrite H6. auto.

+  rewrite Heqrs3'. Simpl. rewrite V. inversion V'. rewrite H6. auto.

   assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. }

   assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }

   (* rewrite H8; auto. *)

   contradict H3; rewrite H3; unfold data_preg; auto.

   contradict H3; rewrite H3; unfold data_preg; auto.

   contradict H3; rewrite H3; unfold data_preg; auto.

-  auto. intros. rewrite Heqrs3'. Simpl. rewrite V by auto with asmgen.

+  contradict H3; rewrite H3; unfold data_preg; auto.

+  intros. rewrite Heqrs3'. rewrite V by auto with asmgen.

   assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }

-  rewrite Heqrs''. Simpl.

-  rewrite H4 by auto with asmgen. reflexivity.

+  rewrite H4 by auto with asmgen. reflexivity. discriminate.

 - (* external function *)

   inv MS.

   exploit functions_translated; eauto.

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 86a0ff88..3c1162bd 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1969,13 +1969,12 @@ Qed.
 
 Lemma indexed_memory_access_correct:
   forall mk_instr base ofs k rs m,
-  base <> RTMP ->
   exists base' ofs' rs' ptr',
      exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m
                        (mk_instr base' ofs' ::g k) rs' m
   /\ eval_offset ofs' = OK ptr'
   /\ Val.offset_ptr rs'#base' ptr' = Val.offset_ptr rs#base ofs
-  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> rs'#r = rs#r.
 Proof.
   unfold indexed_memory_access; intros.
   (* destruct Archi.ptr64 eqn:SF. *)
@@ -2021,13 +2020,12 @@ Lemma indexed_load_access_correct:
      exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) ->
   forall (base: ireg) ofs k (rs: regset) v,
   Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
-  base <> RTMP ->
   exists rs',
      exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m
   /\ rs'#rd = v
-  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
 Proof.
-  intros until m; intros EXEC; intros until v; intros LOAD NOT31.
+  intros until m; intros EXEC; intros until v; intros LOAD.
   exploit indexed_memory_access_correct; eauto.
   intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
   econstructor; split.
@@ -2042,20 +2040,18 @@ Lemma indexed_store_access_correct:
      exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) ->
   forall (base: ireg) ofs k (rs: regset) m',
   Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
-  base <> RTMP -> r1 <> RTMP ->
   exists rs',
      exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m'
-  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> rs'#r = rs#r.
 Proof.
-  intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31'.
-  exploit indexed_memory_access_correct. instantiate (1 := base). eauto.
+  intros until m; intros EXEC; intros until m'; intros STORE.
+  exploit indexed_memory_access_correct. (* instantiate (1 := base). eauto. *)
   intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC.
   unfold exec_store_offset. unfold parexec_store_offset. rewrite PtrEq. rewrite B, C, STORE.
     eauto.
     discriminate.
-    { intro. inv H. contradiction. }
   auto.
 Qed.
 
@@ -2063,13 +2059,12 @@ Lemma loadind_correct:
   forall (base: ireg) ofs ty dst k c (rs: regset) m v,
   loadind base ofs ty dst k = OK c ->
   Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v ->
-  base <> RTMP ->
   exists rs',
      exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
   /\ rs'#(preg_of dst) = v
-  /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros until v; intros TR LOAD NOT31. 
+  intros until v; intros TR LOAD. 
   assert (A: exists mk_instr rd,
                 preg_of dst = IR rd
              /\ c = indexed_memory_access mk_instr base ofs :: k
@@ -2086,12 +2081,11 @@ Lemma storeind_correct:
   forall (base: ireg) ofs ty src k c (rs: regset) m m',
   storeind src base ofs ty k = OK c ->
   Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' ->
-  base <> RTMP ->
   exists rs',
      exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
-  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> rs'#r = rs#r.
 Proof.
-  intros until m'; intros TR STORE NOT31.
+  intros until m'; intros TR STORE.
   assert (A: exists mk_instr rr,
                 preg_of src = IR rr
              /\ c = indexed_memory_access mk_instr base ofs :: k
@@ -2102,7 +2096,6 @@ Proof.
   destruct A as (mk_instr & rr & rsEq & B & C). subst c.
   eapply indexed_store_access_correct; eauto with asmgen.
   congruence.
-  destruct rr; try discriminate. destruct src; try discriminate.
 Qed.
 
 Ltac bsimpl := unfold exec_bblock; simpl.
@@ -2139,23 +2132,21 @@ Qed.
 Lemma loadind_ptr_correct:
   forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v,
   Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v ->
-  base <> RTMP ->
   exists rs',
      exec_straight ge (loadind_ptr base ofs dst ::g k) rs m k rs' m
   /\ rs'#dst = v
-  /\ forall r, r <> PC -> r <> RTMP -> r <> dst -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.
 Proof.
   intros. eapply indexed_load_access_correct; eauto with asmgen.
-  intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H1. auto.
+  intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H0. auto.
 Qed.
 
 Lemma storeind_ptr_correct:
   forall (base: ireg) ofs (src: ireg) k (rs: regset) m m',
   Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
-  base <> RTMP -> src <> RTMP ->
   exists rs',
      exec_straight ge (storeind_ptr src base ofs ::g k) rs m k rs' m'
-  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> rs'#r = rs#r.
 Proof.
   intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen.
   intros. unfold Mptr. assert (Archi.ptr64 = true); auto.
@@ -2174,7 +2165,10 @@ Proof.
   intros until v; intros TR EV. 
   unfold transl_memory_access in TR; destruct addr; ArgsInv.
 - (* indexed *)
-  inv EV. apply indexed_memory_access_correct; eauto with asmgen.
+  inv EV. exploit indexed_memory_access_correct; eauto. intros (base' & ofs' & rs' & ptr' & EOPT & EVALOFF & VALOFF & RSEQ).
+  eexists; eexists; eexists; eexists. split; try split; try split.
+  eapply EOPT. unfold eval_offset in EVALOFF. inv EVALOFF. eauto.
+  { intros. destruct r; rewrite RSEQ; auto. }
 - (* global *)
   simpl in EV. inv EV. inv TR.  econstructor; econstructor; econstructor; econstructor; split.
   constructor. apply exec_straight_one. simpl; eauto. auto. 
@@ -2193,7 +2187,11 @@ Proof.
     destruct (Genv.find_symbol ge i); discriminate.
   + simpl. rewrite Ptrofs.add_zero; auto.
 - (* stack *)
-  inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen.
+  inv TR. inv EV. 
+  exploit indexed_memory_access_correct; eauto. intros (base' & ofs' & rs' & ptr' & EOPT & EVALOFF & VALOFF & RSEQ).
+  eexists; eexists; eexists; eexists. split; try split; try split.
+  eapply EOPT. unfold eval_offset in EVALOFF. inv EVALOFF. eauto.
+  { intros. destruct r; rewrite RSEQ; auto. }
 Qed.
 
 Lemma transl_memory_access2_correct:
@@ -2658,7 +2656,6 @@ Proof.
   exploit ((loadind_ptr_correct SP (fn_retaddr_ofs f) GPRA (Pset RA GPRA ::g Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::g k))
             rs tm).
   - rewrite <- (sp_val _ _ rs AG). simpl. eexact LRA'.
-  - congruence.
   - intros (rs1 & A1 & B1 & C1).
     assert (agree ms (Vptr stk soff) rs1) as AG1.
     + destruct AG.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 2d870c01..8a5a39cb 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -34,9 +34,22 @@ module Target (*: TARGET*) =
 
     let comment = "#"
 
-    let symbol        = elf_symbol
-    let symbol_offset = elf_symbol_offset
-    let label         = elf_label
+    let subst_symbol = function
+        "__compcert_i64_udiv" -> "__udivdi3"
+      | "__compcert_i64_sdiv" -> "__divdi3"
+      | "__compcert_i64_umod" -> "__umoddi3"
+      | "__compcert_i64_smod" -> "__moddi3"
+      | x -> x;;
+    
+    let symbol oc symb =
+      fprintf oc "%s" (subst_symbol (extern_atom symb))
+
+    let symbol_offset oc (symb, ofs) =
+      symbol oc symb;
+      let ofs = camlint64_of_ptrofs ofs in
+      if ofs <> 0L then fprintf oc " + %Ld" ofs
+
+  let label         = elf_label
 
     let print_label oc lbl = label oc (transl_label lbl)