Change definition of match_states

Introduce agree which says that all registers *except* the PC return the
same values.
The idea behind this change is that agree can be preserved across e.g.
an Asmblock basic step, which does not update the PC.
In addition to agree, the simualation relation requires the PC to agree.
Right now the memory needs to be exactly the same which could be a
problem.

Since Asmblock's and Asm's set_pair is defined with preg it is more
difficult to show that set_pair preserves the agree relation since SP is
a preg and must not be Vundef. This commit does not solve the problem.

1 files changed, 172 insertions, 8 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 97612601..23699f4a 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -44,6 +44,12 @@ Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}.
+Record agree (rs1: regset) (rs2: regset) : Prop := mkagree {
+  agree_ir: forall r: iregsp, (rs1 r) = (rs2 r);
+  agree_fr: forall r: freg,   (rs1 r) = (rs2 r);
+  agree_cr: forall r: crbit,  (rs1 r) = (rs2 r);
+  agree_sp_def: (rs1 SP) <> Vundef;
+}.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
@@ -75,7 +81,11 @@ Lemma functions_translated:
 Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
 (* Asmblock and Asm share the same definition of state *)
-Definition match_states (s1 s2 : state) := s1 = s2.
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro rs1 rs2 m
+    (AG: agree rs1 rs2)
+    (PC: rs1 PC = rs2 PC)
+    : match_states (State rs1 m) (State rs2 m).
 
 Lemma transf_initial_states:
   forall s1, Asmblock.initial_state prog s1 ->
@@ -87,7 +97,9 @@ Proof.
   - econstructor.
     eapply (Genv.init_mem_transf_partial TRANSF); eauto.
   - rewrite (match_program_main TRANSF); rewrite symbol_addresses_preserved.
-    unfold rs; reflexivity.
+    unfold rs. unfold Vnullptr. unfold ge.
+    repeat (econstructor; eauto); simpl.
+    destruct Archi.ptr64; rewrite Pregmap.gss; discriminate.
 Qed.
 
 Lemma transf_final_states:
@@ -95,9 +107,151 @@ Lemma transf_final_states:
   match_states s1 s2 -> Asmblock.final_state s1 r -> Asm.final_state s2 r.
 Proof.
   intros s1 s2 r MATCH FINAL_s1.
-  inv FINAL_s1; inv MATCH; constructor; assumption.
+  inv FINAL_s1. inv MATCH.
+  inversion AG as (IR).
+  rewrite PC in *; rewrite IR in *;
+  constructor; trivial.
 Qed.
 
+Lemma agree_but_pc:
+  forall rs1 rs2 r,
+  r <> PC -> agree rs1 rs2 ->
+  (rs1 r) = (rs2 r).
+Proof.
+  intros rs1 rs2 r NOTPC AG.
+  inversion AG as (AGIR, AGFR, AGCR).
+  destruct r.
+  - apply AGIR.
+  - apply AGFR.
+  - apply AGCR.
+  - contradiction.
+Qed.
+
+Lemma agree_mregs:
+  forall (rs1 rs2 : regset) (r: mreg),
+  agree rs1 rs2 -> forall r: mreg, (rs1 (preg_of r)) = (rs2 (preg_of r)).
+Proof.
+  intros ? ? ? ? r. apply agree_but_pc; auto.
+  destruct r; discriminate.
+Qed.
+
+Lemma agree_iregs:
+  forall (rs1 rs2 : regset) (r: iregsp),
+  agree rs1 rs2 -> (rs1 r) = (rs2 r).
+Proof.
+  intros ? ? r. apply agree_but_pc; auto.
+  destruct r; discriminate.
+Qed.
+
+Lemma agree_fregs:
+  forall (rs1 rs2 : regset) (r: freg),
+  agree rs1 rs2 -> (rs1 r) = (rs2 r).
+Proof.
+  intros ? ? r. apply agree_but_pc; auto.
+  destruct r; discriminate.
+Qed.
+
+Lemma agree_sp:
+  forall (rs1 rs2 : regset),
+  agree rs1 rs2 -> (rs1 SP) = (rs2 SP).
+Proof.
+  intros ? ? r. apply agree_but_pc; auto.
+  discriminate.
+Qed.
+
+(* Copied and adapted from PseudoAsmblockproof *)
+Lemma extcall_arg_match ms rs m l v:
+  agree ms rs ->
+  extcall_arg ms m l v ->
+  extcall_arg rs m l v.
+Proof.
+  destruct 2.
+  - erewrite agree_mregs; eauto. constructor.
+  - econstructor; eauto. erewrite <- agree_sp; eauto.
+Qed.
+
+Local Hint Resolve extcall_arg_match: core.
+
+Lemma extcall_arg_pair_match:
+  forall ms rs m p v,
+  agree ms rs ->
+  extcall_arg_pair ms m p v ->
+  extcall_arg_pair rs m p v.
+Proof.
+  destruct 2; constructor; eauto.
+Qed.
+
+Local Hint Resolve extcall_arg_pair_match: core.
+
+Lemma extcall_args_match:
+  forall ms rs m, agree ms rs ->
+  forall ll vl,
+  list_forall2 (extcall_arg_pair ms m) ll vl ->
+  list_forall2 (extcall_arg_pair rs m) ll vl.
+Proof.
+  induction 2; constructor; eauto.
+Qed.
+
+Lemma extcall_arguments_match:
+  forall ms m rs sg args,
+  agree ms rs ->
+  extcall_arguments ms m sg args ->
+  extcall_arguments rs m sg args.
+Proof.
+  unfold extcall_arguments, extcall_arguments; intros.
+  eapply extcall_args_match; eauto.
+Qed.
+
+Lemma agree_undef_caller_save_regs_match:
+  forall rs1 rs2,
+  agree rs1 rs2 -> agree (undef_caller_save_regs rs1) (undef_caller_save_regs rs2).
+Proof.
+  intros rs1 rs2 AG.
+  unfold undef_caller_save_regs. split; auto; intros.
+  - erewrite agree_iregs; auto.
+  - erewrite agree_fregs; auto.
+  - simpl; inversion AG; assumption.
+Qed.
+
+Lemma agree_set_parallel:
+  forall rs1 rs2 r v,
+  agree rs1 rs2 ->
+  r <> SP \/ v <> Vundef -> (* TODO is the right case ever useful? *)
+  agree (rs1#r <- v) (rs2#r <- v).
+Proof.
+  intros rs1 rs2 r v AG H. split; auto.
+  (* TODO refactor repetitive proof *)
+  - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r).
+    + reflexivity.
+    + erewrite agree_but_pc; eauto. discriminate.
+  - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r).
+    + reflexivity.
+    + erewrite agree_but_pc; eauto. discriminate.
+  - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r).
+    + reflexivity.
+    + erewrite agree_but_pc; eauto. discriminate.
+  - destruct H.
+    + rewrite Pregmap.gso; inv AG; auto.
+    + destruct (PregEq.eq SP r) as [SPr | SPnotr].
+      * rewrite SPr; rewrite Pregmap.gss; assumption.
+      * rewrite Pregmap.gso; auto. inv AG; auto.
+Qed.
+
+Lemma agree_set_pair:
+  forall rs1 rs2 p v,
+  agree rs1 rs2 ->
+  (* TODO assumption that pair does not include SP *)
+  agree (set_pair p v rs1) (set_pair p v rs2).
+Proof.
+  intros rs1 rs2 p v AG.
+  destruct p; simpl.
+  - assert (r <> SP) as NOTSP. { admit. }
+    apply agree_set_parallel; auto.
+  - assert (rlo <> SP /\ rhi <> SP) as NOTSP. { admit. } destruct NOTSP.
+    apply agree_set_parallel; auto.
+    + apply agree_set_parallel; auto.
+Admitted.
+
 Lemma step_simulation s1 t s1':
   Asmblock.step lk ge s1 t s1' ->
   forall s2, match_states s1 s2 ->
@@ -107,15 +261,25 @@ Proof.
   inv STEP; simpl; exploit functions_translated; eauto;
   intros (tf0 & FINDtf & TRANSf);
   monadInv TRANSf.
-  - (* internal step *) admit.
+  - (* internal step *)
+     destruct H2. (* exec_bblock *)
+     admit.
   - (* external step *)
+    inversion MATCH as (?, ?, ?, AG, AGPC).
+    exploit external_call_symbols_preserved; eauto. apply senv_preserved.
+    exploit extcall_arguments_match; eauto.
+    intros.
     eexists; split.
     + apply plus_one.
-      rewrite <- MATCH.
-      exploit external_call_symbols_preserved; eauto. apply senv_preserved.
-      intros ?.
+      rewrite AGPC in *.
       eapply Asm.exec_step_external; eauto.
-    + econstructor; eauto.
+    + exploit agree_undef_caller_save_regs_match; eauto; intros AG'.
+      erewrite agree_iregs; eauto.
+      econstructor; auto.
+      apply agree_set_parallel.
+      apply agree_set_pair.
+      * apply agree_undef_caller_save_regs_match; auto.
+      * left. discriminate.
 Admitted.
 
 Lemma transf_program_correct: