diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-01 16:24:32 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-01 16:24:32 +0200 |
commit | 26a7a6598a80c29a139c533419b38be63c88cd76 (patch) | |
tree | 1744bcaf046a59ea3ef8d64a10e3ed0e9b5a3239 /mppa_k1c/Asmblockgenproof1.v | |
parent | 807b07dce1f41dc885d7671e8567ba112966ba7b (diff) | |
download | compcert-kvx-26a7a6598a80c29a139c533419b38be63c88cd76.tar.gz compcert-kvx-26a7a6598a80c29a139c533419b38be63c88cd76.zip |
indexed2XS begin
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 40f9f08b..0cb2d83d 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -2168,6 +2168,7 @@ Lemma transl_load_memory_access_ok: Proof. intros until m. intros ADDR TR ? ?. unfold transl_load in TR. destruct addr; try contradiction. + - (* Indexed2XS*) monadInv TR. - monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto). - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split; [ instantiate (1 := (PLoadRRO _ x)); simpl; reflexivity @@ -2210,6 +2211,7 @@ Lemma transl_load_correct: /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r. Proof. intros until v; intros TR EV LOAD. destruct addr. + 1: (* Aindexed2XS *) discriminate. 2-4: exploit transl_load_memory_access_ok; eauto; try discriminate; intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; eapply transl_load_access_correct; eauto with asmgen. @@ -2293,6 +2295,7 @@ Lemma transl_store_memory_access_ok: Proof. intros until m'. intros ? TR ? ?. unfold transl_store in TR. destruct addr; try contradiction. + - (* Aindex2XS *) discriminate. - monadInv TR. destruct chunk. all: ArgsInv; eexists; eexists; eexists; split; try split; [ repeat (destruct args; try discriminate); eassumption @@ -2362,6 +2365,7 @@ Lemma transl_store_correct: /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. intros until m'; intros TR EV STORE. destruct addr. + 1: (* AIndexed2XS *) discriminate. 2-4: exploit transl_store_memory_access_ok; eauto; try discriminate; intro A; destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D); rewrite D in STORE; clear D; |