diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-02 21:39:20 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-02 21:39:20 +0100 |
| commit | 553714035fc08f9b145b89b3dd7c455f06e917df (patch) | |
| tree | 164f3837a342000eae3addb403b7a189bb2097c6 /backend/Duplicateproof.v | |
| parent | f0c1cc8327ecf2b1e3021bce66f2d6bb0265f6c0 (diff) | |
| download | compcert-kvx-553714035fc08f9b145b89b3dd7c455f06e917df.tar.gz compcert-kvx-553714035fc08f9b145b89b3dd7c455f06e917df.zip | |
finish merge
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 39b7a353..e66a1068 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -13,8 +13,8 @@ Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop dupmap!n' = (Some n) -> match_inst dupmap (Inop n) (Inop n') | match_inst_op: forall n n' op lr r, dupmap!n' = (Some n) -> match_inst dupmap (Iop op lr r n) (Iop op lr r n') - | match_inst_load: forall n n' m a lr r, - dupmap!n' = (Some n) -> match_inst dupmap (Iload m a lr r n) (Iload m a lr r n') + | match_inst_load: forall n n' tm m a lr r, + dupmap!n' = (Some n) -> match_inst dupmap (Iload tm m a lr r n) (Iload tm m a lr r n') | match_inst_store: forall n n' m a lr r, dupmap!n' = (Some n) -> match_inst dupmap (Istore m a lr r n) (Istore m a lr r n') | match_inst_call: forall n n' s ri lr r, @@ -137,6 +137,7 @@ Proof. (* Iload *) - destruct i'; try (inversion H; fail). monadInv H. destruct x. eapply verify_is_copy_correct in EQ. + destruct (trapping_mode_eq _ _); try discriminate. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. @@ -393,6 +394,21 @@ Proof. eexists. split. + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. + econstructor; eauto. +(* Iload notrap1 *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iload_notrap1; eauto. erewrite eval_addressing_preserved; eauto. + + econstructor; eauto. +(* Iload notrap2 *) + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iload_notrap2; eauto. erewrite eval_addressing_preserved; eauto. + + econstructor; eauto. + (* Istore *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. |