diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-04-30 13:25:56 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-04-30 13:25:56 +0200 |
| commit | 0dc240cc53b3603dc76419bebfbbadffa3958988 (patch) | |
| tree | c0f24f941654513f5e19662546f62597678e74be /mppa_k1c | |
| parent | bb64e419eb857882a6f0d102db50ca93b181ad11 (diff) | |
| download | compcert-kvx-0dc240cc53b3603dc76419bebfbbadffa3958988.tar.gz compcert-kvx-0dc240cc53b3603dc76419bebfbbadffa3958988.zip | |
Progression on LOAD sistep_correct
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/lib/RTLpathSE_theory.v | 33 |
1 files changed, 30 insertions, 3 deletions
diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index ce5e09d7..4d3373a9 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -584,7 +584,34 @@ Proof. simpl. exists r. destruct (Pos.eq_dec r r); try congruence. simpl. erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. - + (* LOAD *) admit. (* FIXME *) + + (* LOAD *) + inversion_SOME a0; intro ADD. + { inversion_SOME v; intros LOAD; simpl. + - explore_destruct; unfold ssem, ssem_local; simpl; intuition. + * unfold ssem. simpl. constructor; [|constructor]; auto. + constructor; constructor; simpl; auto. congruence. intro r0. + destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst; rewrite Regmap.gss; simpl. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + * unfold ssem. simpl. constructor; [|constructor]; auto. + constructor; constructor; simpl; auto. congruence. intro r0. + destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst; rewrite Regmap.gss; simpl. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - explore_destruct; unfold sabort, sabort_local; simpl. + * unfold sabort. simpl. left. constructor; auto. + right. right. exists r. simpl. destruct (Pos.eq_dec r r); try congruence. + simpl. erewrite seval_list_sval_inj; simpl; auto. + rewrite ADD; simpl; auto. try_simplify_someHyps. + * unfold ssem. simpl. constructor; [|constructor]; auto. + constructor; constructor; simpl; auto. congruence. intro r0. + destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. + subst; rewrite Regmap.gss; simpl. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. admit. (* FIXME - need to add default_notrap_load_value *) + } { admit. } (* inversion_SOME a0; intros ADD. { inversion_SOME v; intros LOAD; simpl. - explore_destruct; unfold ssem, ssem_local; simpl; intuition. @@ -603,7 +630,7 @@ Proof. exists r. destruct (Pos.eq_dec r r); try congruence. simpl. erewrite seval_list_sval_inj; simpl; auto. rewrite ADD; simpl; auto. } *) - + (* STORE *) + + (* STORE *) inversion_SOME a0; intros ADD. { inversion_SOME m'; intros STORE; simpl. - unfold ssem, ssem_local; simpl; intuition. @@ -620,7 +647,7 @@ Proof. left. constructor; auto. right. left. erewrite seval_list_sval_inj; simpl; auto. erewrite ADD; simpl; auto. } - + (* COND *) + + (* COND *) Local Hint Resolve is_tail_refl: core. Local Hint Unfold ssem_local: core. inversion_SOME b; intros COND. |