diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-21 17:22:01 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-21 17:22:01 +0200 |
| commit | 1f46c2ef4d9080357f37ccb6aa9847ecb8def582 (patch) | |
| tree | 4bcd13321bc54607bbce261b86a5d555a182cfdc /mppa_k1c/Asmblockgenproof.v | |
| parent | bcb6ec6c7a99deb8f211b6a9ba3c6fe7565d3fcb (diff) | |
| download | compcert-kvx-1f46c2ef4d9080357f37ccb6aa9847ecb8def582.tar.gz compcert-kvx-1f46c2ef4d9080357f37ccb6aa9847ecb8def582.zip | |
MB2AB - changement du lock-step en star, cas du Returnstate fait
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 37 |
1 files changed, 27 insertions, 10 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 87b15c39..79a51d16 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -663,12 +663,6 @@ Qed. *) So, the following integer measure will suffice to rule out the unwanted behaviour. *) -Definition measure (s: Mach.state) : nat := - match s with - | Mach.State _ _ _ _ _ _ => 0%nat - | Mach.Callstate _ _ _ _ => 0%nat - | Mach.Returnstate _ _ _ => 1%nat - end. (* Remark preg_of_not_FP: forall r, negb (mreg_eq r R10) = true -> IR FP <> preg_of r. Proof. @@ -1070,6 +1064,31 @@ Local Transparent destroyed_at_function_entry. Qed. *) +Definition measure (s: MB.state) : nat := + match s with + | MB.State _ _ _ _ _ _ => 0%nat + | MB.Callstate _ _ _ _ => 0%nat + | MB.Returnstate _ _ _ => 1%nat + end. + +Axiom TODO: False. + +Theorem step_simulation: + forall S1 t S2, MB.step return_address_offset ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + (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. + - destruct TODO. + - destruct TODO. + - inv MS. inv STACKS. simpl in *. + right. split. omega. split. auto. + rewrite <- ATPC in H5. + econstructor; eauto. congruence. +Admitted. + Lemma transf_initial_states: forall st1, MB.initial_state prog st1 -> exists st2, AB.initial_state tprog st2 /\ match_states st1 st2. @@ -1103,16 +1122,14 @@ Qed. Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := Asmblockgenproof0.return_address_offset. -Axiom TODO: False. - Theorem transf_program_correct: forward_simulation (MB.semantics return_address_offset prog) (AB.semantics tprog). Proof. - eapply forward_simulation_step. + eapply forward_simulation_star with (measure := measure). - apply senv_preserved. - eexact transf_initial_states. - eexact transf_final_states. - - destruct TODO. + - exact step_simulation. Qed. (* |