Updating ARM port

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 41 insertions, 61 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index e689c20..13c2e57 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -146,7 +146,7 @@ Inductive instruction : Type :=
 
   (* Pseudo-instructions *)
   | Pallocframe: Z -> Z -> int -> instruction      (**r allocate new stack frame *)
-  | Pfreeframe: int -> instruction                 (**r deallocate stack frame and restore previous frame *)
+  | Pfreeframe: Z -> Z -> int -> instruction       (**r deallocate stack frame and restore previous frame *)
   | Plabel: label -> instruction                   (**r define a code label *)
   | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
   | Pbtbl: ireg -> list label -> instruction.      (**r N-way branch through a jump table *)
@@ -503,12 +503,16 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       | None => Error
       | Some m2 => OK (nextinstr (rs#IR13 <- sp)) m2
       end
-  | Pfreeframe pos =>
+  | Pfreeframe lo hi pos =>
       match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with
       | None => Error
       | Some v =>
           match rs#IR13 with
-          | Vptr stk ofs => OK (nextinstr (rs#IR13 <- v)) (Mem.free m stk)
+          | Vptr stk ofs =>
+              match Mem.free m stk lo hi with
+              | None => Error
+              | Some m' => OK (nextinstr (rs#IR13 <- v)) m'
+              end
           | _ => Error
           end
       end
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 069a08a..2a3b3f3 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -473,10 +473,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pblsymb symb :: k
   | Mtailcall sig (inl r) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe f.(fn_link_ofs) :: Pbreg (ireg_of r) :: k)
+        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+         :: Pbreg (ireg_of r) :: k)
   | Mtailcall sig (inr symb) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe f.(fn_link_ofs) :: Pbsymb symb :: k)
+        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+         :: Pbsymb symb :: k)
   | Mlabel lbl =>
       Plabel lbl :: k
   | Mgoto lbl =>
@@ -488,7 +490,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pbtbl IR14 tbl :: k
   | Mreturn =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe f.(fn_link_ofs) :: Pbreg IR14 :: k)
+        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+         :: Pbreg IR14 :: k)
   end.
 
 Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 0260feb..eec0c65 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -55,7 +55,7 @@ Lemma functions_translated:
   Genv.find_funct_ptr ge b = Some f ->
   exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Errors.OK tf.
 Proof
-  (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
+  (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
 
 Lemma functions_transl:
   forall f b,
@@ -741,7 +741,7 @@ Lemma exec_Mload_prop:
          (dst : mreg) (c : list Mach.instruction) (ms : mreg -> val)
          (m : mem) (a v : val),
   eval_addressing ge sp addr ms ## args = Some a ->
-  loadv chunk m a = Some v ->
+  Mem.loadv chunk m a = Some v ->
   exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m)
                E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
 Proof.
@@ -756,13 +756,14 @@ Proof.
   eauto; intros; reflexivity.
 Qed.
 
+Lemma storev_8_signed_unsigned:
  forall m a v,
  Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_8.
Qed.

Lemma storev_16_signed_unsigned:
  forall m a v,
  Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v.
Proof.
  intros. unfold Mem.storev. destruct a; auto.
  apply Mem.store_signed_unsigned_16.
Qed.

 Lemma exec_Mstore_prop:
   forall (s : list stackframe) (fb : block) (sp : val)
          (chunk : memory_chunk) (addr : addressing) (args : list mreg)
          (src : mreg) (c : list Mach.instruction) (ms : mreg -> val)
          (m m' : mem) (a : val),
   eval_addressing ge sp addr ms ## args = Some a ->
-  storev chunk m a (ms src) = Some m' ->
+  Mem.storev chunk m a (ms src) = Some m' ->
   exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
                   (Machconcr.State s fb sp c ms m').
 Proof.
@@ -775,8 +776,9 @@ Proof.
   destruct chunk; simpl; simpl in H6;
   try (rewrite storev_8_signed_unsigned in H0);
   try (rewrite storev_16_signed_unsigned in H0);
+  simpl;
   (eapply transl_store_int_correct || eapply transl_store_float_correct);
-  eauto; intros; reflexivity.
+  eauto; intros; simpl; auto.
 Qed.
 
 Lemma exec_Mcall_prop:
@@ -826,18 +828,7 @@ Proof.
   rewrite RA_EQ. econstructor; eauto.
 Qed.
 
-Lemma exec_Mtailcall_prop:
-  forall (s : list stackframe) (fb stk : block) (soff : int)
-         (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (f: function) (f' : block),
-  find_function_ptr ge ros ms = Some f' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-  exec_instr_prop
-          (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
-          (Callstate s f' ms (free m stk)).
-Proof.
+Lemma exec_Mtailcall_prop:
  forall (s : list stackframe) (fb stk : block) (soff : int)
         (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
  find_function_ptr ge ros ms = Some f' ->
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
  Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
  exec_instr_prop
          (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
          (Callstate s f' ms m').
Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -846,24 +837,25 @@ Proof.
          match ros with inl r => Pbreg (ireg_of r) | inr symb => Pbsymb symb end).
   assert (TR: transl_code f (Mtailcall sig ros :: c) =
               loadind_int IR13 (fn_retaddr_ofs f) IR14
-                (Pfreeframe (fn_link_ofs f) :: call_instr :: transl_code f c)).
+                (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)).
   unfold call_instr; destruct ros; auto.
   destruct (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
                 rs m (parent_ra s) 
-                (Pfreeframe f.(fn_link_ofs) :: call_instr :: transl_code f c))
+                (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c))
   as [rs1 [EXEC1 [RES1 OTH1]]].
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
   set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
   assert (EXEC2: exec_straight tge (transl_function f)
                    (transl_code f (Mtailcall sig ros :: c)) rs m
-                   (call_instr :: transl_code f c) rs2 (free m stk)).
+                   (call_instr :: transl_code f c) rs2 m').
   rewrite TR. eapply exec_straight_trans. eexact EXEC1.
   apply exec_straight_one. simpl.
   rewrite OTH1; auto with ppcgen. 
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
-  unfold load_stack in H1. simpl in H1. simpl. rewrite H1. auto. auto.
+  unfold load_stack in H1. simpl in H1. simpl. rewrite H1.
+  rewrite H3. auto. auto.
   set (rs3 := rs2#PC <- (Vptr f' Int.zero)).
-  left. exists (State rs3 (free m stk)); split.
+  left. exists (State rs3 m'); split.
   (* Execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   inv AT. exploit exec_straight_steps_2; eauto. 
@@ -878,7 +870,7 @@ Proof.
   rewrite Pregmap.gso. rewrite OTH1; auto with ppcgen.
   rewrite <- (ireg_val ms (Vptr stk soff) rs); auto. 
   destruct (ms m0); try discriminate.
-  generalize H. predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H9.
+  generalize H. predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H10.
   auto.
   decEq. auto with ppcgen. decEq. auto with ppcgen. decEq. auto with ppcgen.
   replace (symbol_offset tge i Int.zero) with (Vptr f' Int.zero). auto.
@@ -1036,34 +1028,26 @@ Opaque Zmod.  Opaque Zdiv.
   unfold rs1. apply agree_nextinstr. apply agree_set_other; auto with ppcgen.
 Qed.
 
-Lemma exec_Mreturn_prop:
-  forall (s : list stackframe) (fb stk : block) (soff : int)
-         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: function),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-  exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
-                  (Returnstate s ms (free m stk)).
-Proof.
+Lemma exec_Mreturn_prop:
  forall (s : list stackframe) (fb stk : block) (soff : int)
         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
  Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' ->
  exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
                  (Returnstate s ms m').
Proof.
   intros; red; intros; inv MS.
   assert (f0 = f) by congruence. subst f0.
   exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
                 rs m (parent_ra s)
-                (Pfreeframe f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
+                (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
   intros [rs1 [EXEC1 [RES1 OTH1]]].
   set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
   assert (EXEC2: exec_straight tge (transl_function f)
           (loadind_int IR13 (fn_retaddr_ofs f) IR14
-             (Pfreeframe (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
-          rs m (Pbreg IR14 :: transl_code f c) rs2 (free m stk)).
+             (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize)  (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
+          rs m (Pbreg IR14 :: transl_code f c) rs2 m').
   eapply exec_straight_trans. eexact EXEC1. 
   apply exec_straight_one. simpl. rewrite OTH1; try congruence.
   rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
-  unfold load_stack in H0. simpl in H0; simpl; rewrite H0. reflexivity.
+  unfold load_stack in H0. simpl in H0; simpl; rewrite H0. rewrite H2. reflexivity.
   reflexivity.
   set (rs3 := rs2#PC <- (parent_ra s)).
-  left; exists (State rs3 (free m stk)); split.
+  left; exists (State rs3 m'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   inv AT. exploit exec_straight_steps_2; eauto. 
@@ -1093,7 +1077,7 @@ Lemma exec_function_internal_prop:
   forall (s : list stackframe) (fb : block) (ms : Mach.regset)
          (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
+  Mem.alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
   let sp := Vptr stk (Int.repr (- fn_framesize f)) in
   store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
   store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
@@ -1102,7 +1086,7 @@ Lemma exec_function_internal_prop:
 Proof.
   intros; red; intros; inv MS.
   assert (WTF: wt_function f).
-    generalize (Genv.find_funct_ptr_prop wt_fundef wt_prog H); intro TY.
+    generalize (Genv.find_funct_ptr_prop wt_fundef _ _ wt_prog H); intro TY.
     inversion TY; auto.
   exploit functions_transl; eauto. intro TFIND.
   generalize (functions_transl_no_overflow _ _ H); intro NOOV.
@@ -1146,24 +1130,14 @@ Proof.
   econstructor; eauto with coqlib.
 Qed.
 
-Lemma exec_function_external_prop:
-  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
-         (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
-         (ef : external_function) (args : list val) (res : val),
-  Genv.find_funct_ptr ge fb = Some (External ef) ->
-  event_match ef args t0 res ->
-  Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
-  ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms ->
-  exec_instr_prop (Machconcr.Callstate s fb ms m)
-               t0 (Machconcr.Returnstate s ms' m).
-Proof.
+Lemma exec_function_external_prop:
  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
         (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
         (ef : external_function) (args : list val) (res : val) (m': mem),
  Genv.find_funct_ptr ge fb = Some (External ef) ->
  external_call ef args m t0 res m' ->
  Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
  ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms ->
  exec_instr_prop (Machconcr.Callstate s fb ms m)
               t0 (Machconcr.Returnstate s ms' m').
Proof.
   intros; red; intros; inv MS.
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B. 
   left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs IR14))
-                m); split.
+                m'); split.
   apply plus_one. eapply exec_step_external; eauto. 
-  eapply extcall_arguments_match; eauto. 
+  eauto. eapply extcall_arguments_match; eauto. 
   econstructor; eauto. 
   unfold loc_external_result. auto with ppcgen.
 Qed.
@@ -1209,14 +1183,14 @@ Proof.
   intros. inversion H. unfold ge0 in *.
   econstructor; split.
   econstructor.
+  eapply Genv.init_mem_transf_partial; eauto. 
   replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
      with (Vptr fb Int.zero).
-  rewrite (Genv.init_mem_transf_partial _ _ TRANSF).
   econstructor; eauto. constructor.
   split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF). 
-  rewrite symbols_preserved. unfold ge; rewrite H0. auto.
+  rewrite symbols_preserved. unfold ge; rewrite H1. auto.
 Qed.
 
 Lemma transf_final_states:
diff --git a/arm/Op.v b/arm/Op.v
index 51ce002..7a25511 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -572,8 +572,7 @@ Proof.
   destruct v; destruct chunk; exact I.
   intros until v. unfold Mem.loadv. 
   destruct addr; intros; try discriminate.
-  generalize (Mem.load_inv _ _ _ _ _ H0).
-  intros [X Y].  subst v.  apply H.
+  eapply Mem.load_type; eauto.
 Qed.
 
 End SOUNDNESS.