diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 14:40:56 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 14:40:56 +0200 |
| commit | 2b2ad7fc33fecfd77598e485ae0af82be3f23471 (patch) | |
| tree | da27efc1ef3c83fcc84ccfaf05318c5b6c98c7d5 /mppa_k1c | |
| parent | 22e78b34ca993e0ff1f79c943b16122b1067bd74 (diff) | |
| download | compcert-kvx-2b2ad7fc33fecfd77598e485ae0af82be3f23471.tar.gz compcert-kvx-2b2ad7fc33fecfd77598e485ae0af82be3f23471.zip | |
moving forward with notrap
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 32 |
1 files changed, 10 insertions, 22 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 67f02520..15655db6 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1204,30 +1204,18 @@ Local Transparent destroyed_by_op. eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
simpl; congruence.
- - simpl in EQ0. rewrite Hheader in DXP.
-
- assert (eval_addressing tge sp addr (map ms args) = None).
- rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
- exploit eval_addressing_lessdef_none. eapply preg_vals; eauto. eassumption.
- intros Haddr. rewrite (sp_val _ _ _ AG) in Haddr.
- 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.
+ - (* notrap1 cannot happen *)
+ simpl in EQ0. unfold transl_load in EQ0.
+ destruct addr; simpl in H.
+ all: unfold transl_load_rrrXS, transl_load_rrr, transl_load_rro in EQ0;
+ monadInv EQ0; unfold transl_memory_access2XS, transl_memory_access2, transl_memory_access in EQ2;
+ destruct args as [|h0 t0]; try discriminate;
+ destruct t0 as [|h1 t1]; try discriminate;
+ destruct t1 as [|h2 t2]; try discriminate.
- (* MBload notrap2 TODO *)
simpl in EQ0.
- discriminate.
+ admit.
- (* MBstore *)
simpl in EQ0. rewrite Hheader in DXP.
@@ -1253,7 +1241,7 @@ Local Transparent destroyed_by_op. eapply agree_undef_regs; eauto with asmgen.
simpl; congruence.
-Qed.
+Admitted.
Lemma exec_body_trans:
forall l l' rs0 m0 rs1 m1 rs2 m2,
|