diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-20 11:38:31 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-20 11:38:31 +0200 |
| commit | 7b3d2c0ab46292a47256ff484b812d3d3b2846c2 (patch) | |
| tree | c04d291fbae14168fa1594e8b01adad76ad1b1ba /mppa_k1c | |
| parent | aa25ec270b651186154523ec71a3888b50994d70 (diff) | |
| download | compcert-kvx-7b3d2c0ab46292a47256ff484b812d3d3b2846c2.tar.gz compcert-kvx-7b3d2c0ab46292a47256ff484b812d3d3b2846c2.zip | |
MPPA - Added Ocast8signed and Ocast16signed
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 28 |
2 files changed, 16 insertions, 16 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 8198fa78..0adc41b5 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -271,13 +271,13 @@ Definition transl_op do rd <- ireg_of res; OK (addptrofs rd SP n k) -(*| Ocast8signed, a1 :: nil => + | Ocast8signed, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pslliw rd rs (Int.repr 24) :: Psraiw rd rd (Int.repr 24) :: k) | Ocast16signed, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pslliw rd rs (Int.repr 16) :: Psraiw rd rd (Int.repr 16) :: k) -*)| Oadd, a1 :: a2 :: nil => + | Oadd, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Paddw rd rs1 rs2 :: k) | Oaddimm n, a1 :: nil => diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index 21ff9738..44a02871 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -1214,6 +1214,20 @@ Opaque Int.eq. - (* Oaddrstack *) exploit addptrofs_correct. instantiate (1 := GPR12); auto with asmgen. intros (rs' & A & B & C). exists rs'; split; eauto. auto with asmgen. +- (* Ocast8signed *) + econstructor; split. + eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. + split; intros; Simpl. + assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. unfold getw. + destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. +- (* Ocast16signed *) + econstructor; split. + eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. + split; intros; Simpl. + assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. unfold getw. + destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. - (* Oshrximm *) clear H. exploit Val.shrx_shr_2; eauto. intros E; subst v; clear EV. destruct (Int.eq n Int.zero). @@ -1257,20 +1271,6 @@ Opaque Int.eq. - (* stackoffset *) exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C). exists rs'; split; eauto. auto with asmgen. -- (* cast8signed *) - econstructor; split. - eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. - split; intros; Simpl. - assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. - destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. -- (* cast16signed *) - econstructor; split. - eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. - split; intros; Simpl. - assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. - destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. - (* addimm *) exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen. intros (rs' & A & B & C). |