From 6bb5ae7ee76bee8b8be0c99363975bafa5753c0b Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 23 Jan 2020 16:51:04 +0100 Subject: Added clause in match_inst to allow Icond reversal --- backend/Duplicateproof.v | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'backend/Duplicateproof.v') diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 67d16580..b99fadac 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -26,6 +26,9 @@ Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr, dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) -> match_inst dupmap (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot') + | match_inst_revcond: forall ifso ifso' ifnot ifnot' c lr, + dupmap!ifso' = (Some ifso) -> dupmap!ifnot' = (Some ifnot) -> + match_inst dupmap (Icond c lr ifso ifnot) (Icond (negate_condition c) lr ifnot' ifso') | match_inst_jumptable: forall ln ln' r, list_forall2 (fun n n' => (dupmap!n' = (Some n))) ln ln' -> match_inst dupmap (Ijumptable r ln) (Ijumptable r ln') @@ -464,10 +467,16 @@ Proof. (* Icond *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. - pose symbols_preserved as SYMPRES. - eexists. split. - + eapply exec_Icond; eauto. - + econstructor; eauto. destruct b; auto. + * (* match_inst_cond *) + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Icond; eauto. + + econstructor; eauto. destruct b; auto. + * (* match_inst_revcond *) + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Icond; eauto. rewrite eval_negate_condition. rewrite H0. simpl. eauto. + + econstructor; eauto. destruct b; auto. (* Ijumptable *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. -- cgit