diff options
-rw-r--r-- | backend/Duplicateproof.v | 17 |
1 files changed, 13 insertions, 4 deletions
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. |