From 553714035fc08f9b145b89b3dd7c455f06e917df Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Dec 2019 21:39:20 +0100 Subject: finish merge --- backend/Duplicateproof.v | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) (limited to 'backend/Duplicateproof.v') 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. -- cgit