diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 11:39:44 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 11:39:44 +0200 |
commit | ec99800447f584e31523345469cee96977266327 (patch) | |
tree | 0d66a7d21b81b48cc9c50533a22c05e7fbf58401 /mppa_k1c/Asmblockgenproof1.v | |
parent | cd3642815d4260a9e7868fce3fb6a4a8a8ea8746 (diff) | |
download | compcert-kvx-ec99800447f584e31523345469cee96977266327.tar.gz compcert-kvx-ec99800447f584e31523345469cee96977266327.zip |
begin using shrx
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 33 |
1 files changed, 9 insertions, 24 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index bbcffbe2..a2f11154 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1593,31 +1593,16 @@ Opaque Int.eq. 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). -+ econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros; Simpl. -+ change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). econstructor; split. - eapply exec_straight_step. simpl; reflexivity. - eapply exec_straight_step. simpl; reflexivity. - eapply exec_straight_step. simpl; reflexivity. - apply exec_straight_one. simpl; reflexivity. - split; intros; Simpl. -(* - (* Ocast32signed *) - exploit cast32signed_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. split. apply B. - intros. assert (r <> PC). { destruct r; auto; contradict H; discriminate. } - apply C; auto. - *)(* - (* longofintu *) - econstructor; split. - eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. - split; intros; Simpl. (* unfold Pregmap.set; Simpl. *) destruct (PregEq.eq x0 x0). - + destruct (rs x0); auto. simpl. - assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. - rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal. - rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. - + contradict n. auto. *) + + apply exec_straight_one. simpl. eauto. + + split. + * rewrite Pregmap.gss. + subst v. + destruct (rs x0); simpl; trivial. + unfold Val.maketotal. + destruct (Int.ltu _ _); simpl; trivial. + * intros. + rewrite Pregmap.gso; trivial. - (* Oshrxlimm *) clear H. exploit Val.shrxl_shrl_2; eauto. intros E; subst v; clear EV. destruct (Int.eq n Int.zero). |