MB2AB - Proof of external function step

3 files changed, 85 insertions, 13 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 4f825bf5..4a4ffc10 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -548,10 +548,10 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
 
 
 (** Assigning a register pair *)
-Definition set_pair (p: rpair breg) (v: val) (rs: bregset) : bregset :=
+Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
   match p with
-  | One r => rs#r <- v
-  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
+  | One r => rs#r <-- v
+  | Twolong rhi rlo => rs#rhi <-- (Val.hiword v) #rlo <-- (Val.loword v)
   end.
 
 (* TODO: Is it still useful ?? *)
@@ -1093,8 +1093,8 @@ Definition extcall_arguments
     (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
   list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
 
-Definition loc_external_result (sg: signature) : rpair breg :=
-  map_rpair breg_of (loc_result sg).
+Definition loc_external_result (sg: signature) : rpair preg :=
+  map_rpair preg_of (loc_result sg).
 
 (** Execution of the instruction at [rs PC]. *)
 
@@ -1134,7 +1134,7 @@ Inductive stepin: option bblock -> state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (ef_sig ef) args ->
-      rs' = (update_pregs rs (set_pair (loc_external_result (ef_sig ef) ) res rs))#PC <-- (rs RA) ->
+      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <-- (rs RA) ->
       stepin None (State rs m) t (State rs' m')
   .
 
@@ -1172,7 +1172,7 @@ Lemma exec_step_external b ef args res rs m t rs' m':
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (ef_sig ef) args ->
-      rs' = (update_pregs rs (set_pair (loc_external_result (ef_sig ef) ) res rs))#PC <-- (rs RA) ->
+      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <-- (rs RA) ->
       step (State rs m) t (State rs' m')
   .
 Proof.
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index c2a609c9..f0842c4d 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -47,7 +47,7 @@ Lemma senv_preserved:
   Senv.equiv ge tge.
 Proof (Genv.senv_match TRANSF).
 
-(*
+
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
@@ -55,6 +55,7 @@ Lemma functions_translated:
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
 Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
+(*
 Lemma functions_transl:
   forall fb f tf,
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
@@ -1079,11 +1080,27 @@ Theorem step_simulation:
   (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
 Proof.
-  induction 1; intros.
-  - destruct TODO.
+  induction 1; intros; inv MS.
   - destruct TODO.
   - destruct TODO.
-  - inv MS. inv STACKS. simpl in *.
+
+- (* external function *)
+  exploit functions_translated; eauto.
+  intros [tf [A B]]. simpl in B. inv B.
+  exploit extcall_arguments_match; eauto.
+  intros [args' [C D]].
+  exploit external_call_mem_extends; eauto.
+  intros [res' [m2' [P [Q [R S]]]]].
+  left; econstructor; split.
+  apply plus_one. eapply exec_step_external; eauto.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  econstructor; eauto.
+  unfold loc_external_result.
+  apply agree_set_other; auto.
+  apply agree_set_pair; auto.
+
+  - (* return *) 
+  inv STACKS. simpl in *.
   right. split. omega. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index 52ba9ca2..15cd88b5 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -169,7 +169,7 @@ Proof.
 Qed.
  *)
 
-(* Lemma agree_set_pair:
+Lemma agree_set_pair:
   forall sp p v v' ms rs,
   agree ms sp rs ->
   Val.lessdef v v' ->
@@ -180,7 +180,6 @@ Proof.
 - apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
   apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
 Qed.
- *)
 
 Lemma agree_undef_nondata_regs:
   forall ms sp rl rs,
@@ -255,6 +254,62 @@ Proof.
   intros. rewrite Pregmap.gso; auto with asmgen.
 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', AB.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', AB.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 (AB.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', AB.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
+Proof.
+  unfold Mach.extcall_arguments, AB.extcall_arguments; intros.
+  eapply extcall_args_match; eauto.
+Qed.
 
 (* inspired from Mach *)