diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-07 17:49:03 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-07 17:49:03 +0100 |
| commit | 88f6f275015eaa0ab5aac58eae93d2fa5e8f6b48 (patch) | |
| tree | e0c19b0fbecd7803fb3442c52cd8ec60ce1437da /mppa_k1c/Asmblockgenproof.v | |
| parent | 747b4e21c1d31a0d8a1d273ab159f9fd87822a1e (diff) | |
| download | compcert-kvx-88f6f275015eaa0ab5aac58eae93d2fa5e8f6b48.tar.gz compcert-kvx-88f6f275015eaa0ab5aac58eae93d2fa5e8f6b48.zip | |
MBload proved
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 26 |
1 files changed, 25 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index e049ac58..8343272a 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1536,7 +1536,31 @@ Proof. Local Transparent destroyed_by_op.
destruct op; simpl; auto; congruence.
- (* MBload *)
- destruct TODO.
+ simpl in EQ0. rewrite Hheader in DXP.
+
+ assert (eval_addressing tge sp addr (map ms args) = Some a).
+ rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+ exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+ intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+ exploit Mem.loadv_extends; eauto. intros [v' [C D]].
+ exploit transl_load_correct; eauto.
+ intros [rs2 [P [Q R]]].
+
+ eapply exec_straight_body in P.
+ 2: eapply code_to_basics_id; eauto.
+ destruct P as (l & ll & TBC & CTB & EXECB).
+ exists rs2, m1, ll.
+ eexists. eexists. split. instantiate (1 := x). eauto.
+ repeat (split; auto).
+ eapply basics_to_code_app; eauto.
+ remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+ rewrite <- Hheadereq. *) subst.
+ eapply match_codestate_intro; eauto. simpl. simpl in EQ.
+
+ eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
+ simpl; congruence.
+
- (* MBstore *)
destruct TODO.
Qed.
|