diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 16:11:27 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 16:11:27 +0100 |
| commit | 0dc6f0aadfa95c722324b10c56768900760337a0 (patch) | |
| tree | 44a2d92e3d8c669f2da0a7aaf9d62d794e7f4314 /mppa_k1c/Asmblockdeps.v | |
| parent | 5f38e0401747a59a821852fdefb7b588a818bdcf (diff) | |
| download | compcert-kvx-0dc6f0aadfa95c722324b10c56768900760337a0.tar.gz compcert-kvx-0dc6f0aadfa95c722324b10c56768900760337a0.zip | |
Preuve de Jumptable dans Asmblockdeps.v
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 7f03c66a..dd876485 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1845,6 +1845,17 @@ Proof. - destruct c; destruct i; try discriminate. all: try (inv H0; inv MSR; inv MSW; eexists; split; [| split]; [simpl; rewrite (H0 PC); reflexivity | Simpl | intros rr; destruct rr; unfold par_nextblock; Simpl]). + (* Pjumptable *) + + simpl in H0. destruct (par_nextblock _ _ _) eqn:PNEXT; try discriminate. + destruct (list_nth_z _ _) eqn:LISTS; try discriminate. unfold par_goto_label in H0. + destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ rsr PC) eqn:NB; try discriminate. inv H0. + inv MSR; inv MSW. eexists; split; try split. + * simpl. rewrite (H0 PC). Simpl. rewrite (H0 r). unfold par_nextblock in PNEXT. rewrite Pregmap.gso in PNEXT; try discriminate. rewrite PNEXT. + rewrite LISTS. unfold goto_label_deps. rewrite LPOS. unfold par_nextblock in NB. rewrite Pregmap.gss in NB. rewrite NB. reflexivity. + * Simpl. + * intros rr; destruct rr; unfold par_nextblock; Simpl. + destruct (preg_eq g GPR62). rewrite e. Simpl. + destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl. (* Pj_l *) + simpl in H0. unfold par_goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (par_nextblock _ _ _) eqn:NB; try discriminate. inv H0. inv MSR; inv MSW. @@ -1942,6 +1953,10 @@ Proof. destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). (* Pbuiltin *) - simpl in *. rewrite (H1 PC). reflexivity. +(* Pjumptable *) + - simpl in *. rewrite (H1 PC). Simpl. rewrite (H1 r). unfold par_nextblock in H0. rewrite Pregmap.gso in H0; try discriminate. + destruct (rsr r); auto. destruct (list_nth_z _ _); auto. unfold par_goto_label in H0. unfold goto_label_deps. + destruct (label_pos _ _ _); auto. rewrite Pregmap.gss in H0. destruct (Val.offset_ptr _ _); try discriminate; auto. (* Pj_l *) - simpl in *. rewrite (H1 PC). unfold goto_label_deps. unfold par_goto_label in H0. destruct (label_pos _ _ _); auto. simpl in *. unfold par_nextblock in H0. rewrite Pregmap.gss in H0. |