diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-21 17:19:06 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
| commit | 0a7a6ed916a95b53b63a9d4bdf1e545aacf3f82b (patch) | |
| tree | 5ec79aeecac5d38a00580d020871018ad58c1c37 /mppa_k1c | |
| parent | 3f5f3aedb19165134b45dbf6aeea877e8ab46f6f (diff) | |
| download | compcert-kvx-0a7a6ed916a95b53b63a9d4bdf1e545aacf3f82b.tar.gz compcert-kvx-0a7a6ed916a95b53b63a9d4bdf1e545aacf3f82b.zip | |
MPPA - Reactivated Omove
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 2 |
3 files changed, 7 insertions, 3 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index e6c99547..3445c898 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -378,12 +378,12 @@ Definition transl_cond_op Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with -(*| Omove, a1 :: nil => + | Omove, a1 :: nil => match preg_of res, preg_of a1 with | IR r, IR a => OK (Pmv r a :: k) | _ , _ => Error(msg "Asmgen.Omove") end -*)| Ointconst n, nil => + | Ointconst n, nil => do rd <- ireg_of res; OK (loadimm32 rd n k) | Olongconst n, nil => diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index cbf5f166..afbb2e3f 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -277,7 +277,11 @@ Remark transl_op_label: Proof. Opaque Int.eq. unfold transl_op; intros; destruct op; TailNoLabel. +(* Omove *) +- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. +(* ? *) - apply opimm32_label; intros; exact I. +(* ? *) - apply opimm64_label; intros; exact I. Qed. diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index e339a4c9..23c0478c 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -982,9 +982,9 @@ Proof. Opaque Int.eq. intros until c; intros TR EV. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl. -(* - (* move *) destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. +(* - (* intconst *) exploit loadimm32_correct; eauto. intros (rs' & A & B & C). exists rs'; split; eauto. rewrite B; auto with asmgen. |